wip

src/Juvix/Compiler/Builtins.hs

@@ -2,6 +2,7 @@ module Juvix.Compiler.Builtins
   ( module Juvix.Compiler.Builtins.Nat,
     module Juvix.Compiler.Builtins.IO,
     module Juvix.Compiler.Builtins.Eq,
+    module Juvix.Compiler.Builtins.Ord,
     module Juvix.Compiler.Builtins.Int,
     module Juvix.Compiler.Builtins.Bool,
     module Juvix.Compiler.Builtins.List,
@@ -33,4 +34,5 @@ import Juvix.Compiler.Builtins.List
 import Juvix.Compiler.Builtins.Maybe
 import Juvix.Compiler.Builtins.Monad
 import Juvix.Compiler.Builtins.Nat
+import Juvix.Compiler.Builtins.Ord
 import Juvix.Compiler.Builtins.String

src/Juvix/Compiler/Builtins/Ord.hs

@@ -0,0 +1,25 @@
+module Juvix.Compiler.Builtins.Ord where
+
+import Juvix.Compiler.Internal.Builtins
+import Juvix.Compiler.Internal.Extra
+import Juvix.Prelude
+import Juvix.Prelude.Pretty
+
+checkOrdDef :: forall r. (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r ()
+checkOrdDef d = do
+  let err :: forall a. Text -> Sem r a
+      err = builtinsErrorText (getLoc d)
+  let eqTxt = prettyText BuiltinOrd
+  unless (isSmallUniverse' (d ^. inductiveType)) (err (eqTxt <> " should be in the small universe"))
+  case d ^. inductiveParameters of
+    [_] -> return ()
+    _ -> err (eqTxt <> " should have exactly one type parameter")
+  case d ^. inductiveConstructors of
+    [c1] -> checkMkOrd c1
+    _ -> err (eqTxt <> " should have exactly two constructors")
+
+checkMkOrd :: ConstructorDef -> Sem r ()
+checkMkOrd _ = return ()
+
+checkIsOrd :: FunctionDef -> Sem r ()
+checkIsOrd _ = return ()

src/Juvix/Compiler/Concrete/Data/Builtins.hs

@@ -60,6 +60,7 @@ builtinConstructors = \case
   BuiltinAnomaResource -> [BuiltinMkAnomaResource]
   BuiltinAnomaAction -> [BuiltinMkAnomaAction]
   BuiltinEq -> [BuiltinMkEq]
+  BuiltinOrd -> [BuiltinMkOrd]
 
 data BuiltinInductive
   = BuiltinNat
@@ -69,6 +70,7 @@ data BuiltinInductive
   | BuiltinMaybe
   | BuiltinPair
   | BuiltinEq
+  | BuiltinOrd
   | BuiltinPoseidonState
   | BuiltinEcPoint
   | BuiltinAnomaResource
@@ -90,6 +92,7 @@ instance Pretty BuiltinInductive where
     BuiltinMaybe -> Str.maybe_
     BuiltinPair -> Str.pair
     BuiltinEq -> Str.eq
+    BuiltinOrd -> Str.ord
     BuiltinPoseidonState -> Str.cairoPoseidonState
     BuiltinEcPoint -> Str.cairoEcPoint
     BuiltinAnomaResource -> Str.anomaResource
@@ -113,6 +116,7 @@ instance Pretty BuiltinConstructor where
     BuiltinMkAnomaResource -> Str.anomaMkResource
     BuiltinMkAnomaAction -> Str.anomaMkAction
     BuiltinMkEq -> Str.mkEq
+    BuiltinMkOrd -> Str.mkOrd
 
 data BuiltinConstructor
   = BuiltinNatZero
@@ -124,6 +128,7 @@ data BuiltinConstructor
   | BuiltinListNil
   | BuiltinListCons
   | BuiltinMkEq
+  | BuiltinMkOrd
   | BuiltinMaybeNothing
   | BuiltinMaybeJust
   | BuiltinPairConstr

src/Juvix/Compiler/Core/Pretty/Base.hs

@@ -654,6 +654,7 @@ instance PrettyCode InfoTable where
               BuiltinAnomaAction -> True
               BuiltinList -> False
               BuiltinEq -> False
+              BuiltinOrd -> False
               BuiltinMaybe -> False
               BuiltinNat -> False
               BuiltinInt -> False

src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs

@@ -200,6 +200,7 @@ checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go
       BuiltinAnomaResource -> return ()
       BuiltinAnomaAction -> return ()
       BuiltinEq -> return ()
+      BuiltinOrd -> return ()
 
     addInductiveStartNode :: Sem r ()
     addInductiveStartNode = addStartNode (i ^. inductiveName)

src/Juvix/Compiler/Internal/Language.hs

@@ -33,7 +33,9 @@ newtype PreLetStatement
   = PreLetFunctionDef FunctionDef
 
 -- | Traits that support builtin deriving
-data DerivingTrait = DerivingEq
+data DerivingTrait
+  = DerivingEq
+  | DerivingOrd
   deriving stock (Generic, Data, Bounded, Enum, Show)
 
 derivingTraitFromBuiltinMap :: HashMap BuiltinPrim DerivingTrait
@@ -46,6 +48,7 @@ instance IsBuiltin DerivingTrait where
   toBuiltinPrim :: DerivingTrait -> BuiltinPrim
   toBuiltinPrim = \case
     DerivingEq -> toBuiltinPrim BuiltinEq
+    DerivingOrd -> toBuiltinPrim BuiltinOrd
 
 instance Pretty DerivingTrait where
   pretty = pretty . toBuiltinPrim

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -447,6 +447,7 @@ deriveTrait ::
   Sem r Internal.FunctionDef
 deriveTrait = \case
   Internal.DerivingEq -> deriveEq
+  Internal.DerivingOrd -> deriveOrd
 
 findDerivingTrait ::
   forall r.
@@ -536,6 +537,42 @@ throwDerivingWrongForm ret = do
           _derivingTypeSupportedBuiltins
         }
 
+deriveOrd ::
+  forall r.
+  ( Members
+      '[ Reader S.InfoTable,
+         Reader Internal.InfoTable,
+         State LocalTable,
+         NameIdGen,
+         Error ScoperError,
+         Reader DefaultArgsStack,
+         Reader Pragmas
+       ]
+      r
+  ) =>
+  DerivingArgs ->
+  Sem r Internal.FunctionDef
+deriveOrd DerivingArgs {..} = do
+  arg <- getArg
+  argsInfo <- goArgsInfo _derivingInstanceName
+  mkOrd <- getBuiltin (getLoc eqName) BuiltinMkOrd
+  let cmp = undefined
+      body = mkEq Internal.@@ cmp
+      ty = Internal.foldFunType _derivingParameters (Internal.foldApplication (Internal.toExpression eqName) args)
+  pragmas' <- goPragmas _derivingPragmas
+  return
+    Internal.FunctionDef
+      { _funDefTerminating = False,
+        _funDefIsInstanceCoercion = Just Internal.IsInstanceCoercionInstance,
+        _funDefPragmas = pragmas',
+        _funDefArgsInfo = argsInfo,
+        _funDefDocComment = Nothing,
+        _funDefName = _derivingInstanceName,
+        _funDefType = ty,
+        _funDefBody = body,
+        _funDefBuiltin = Nothing
+      }
+
 deriveEq ::
   forall r.
   ( Members
@@ -808,6 +845,7 @@ checkBuiltinInductive ::
 checkBuiltinInductive d b = localBuiltins $ case b of
   BuiltinNat -> checkNatDef d
   BuiltinEq -> checkEqDef d
+  BuiltinEq -> checkOrdDef d
   BuiltinBool -> checkBoolDef d
   BuiltinInt -> checkIntDef d
   BuiltinList -> checkListDef d

src/Juvix/Extra/Strings.hs

@@ -548,6 +548,9 @@ isEqual = "isEqual"
 eq :: (IsString s) => s
 eq = "eq"
 
+ord :: (IsString s) => s
+ord = "ord"
+
 assert_ :: (IsString s) => s
 assert_ = "assert"
 
@@ -1154,6 +1157,9 @@ anomaMkAction = "mkAction"
 mkEq :: (IsString s) => s
 mkEq = "mkEq"
 
+mkOrd :: (IsString s) => s
+mkOrd = "mkOrd"
+
 rustFn :: (IsString s) => s
 rustFn = "fn"