Deriving Ord

include/package-base/Juvix/Builtin/V1/Bool.juvix

@@ -3,5 +3,5 @@ module Juvix.Builtin.V1.Bool;
 --- Inductive definition of booleans.
 builtin bool
 type Bool :=
-  | true
-  | false;
+  | false
+  | true;

src/Juvix/Compiler/Builtins.hs

@@ -2,6 +2,8 @@ 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.Ordering,
     module Juvix.Compiler.Builtins.Int,
     module Juvix.Compiler.Builtins.Bool,
     module Juvix.Compiler.Builtins.List,
@@ -33,4 +35,6 @@ 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.Ordering
 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 ()
+
+checkOrdCompare :: FunctionDef -> Sem r ()
+checkOrdCompare _ = return ()

src/Juvix/Compiler/Builtins/Ordering.hs

@@ -0,0 +1,7 @@
+module Juvix.Compiler.Builtins.Ordering where
+
+import Juvix.Compiler.Internal.Extra
+import Juvix.Prelude
+
+checkOrderingDef :: forall r. InductiveDef -> Sem r ()
+checkOrderingDef _d = return ()

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

@@ -50,7 +50,7 @@ instance Pretty BuiltinPrim where
 builtinConstructors :: BuiltinInductive -> [BuiltinConstructor]
 builtinConstructors = \case
   BuiltinNat -> [BuiltinNatZero, BuiltinNatSuc]
-  BuiltinBool -> [BuiltinBoolTrue, BuiltinBoolFalse]
+  BuiltinBool -> [BuiltinBoolFalse, BuiltinBoolTrue]
   BuiltinInt -> [BuiltinIntOfNat, BuiltinIntNegSuc]
   BuiltinList -> [BuiltinListNil, BuiltinListCons]
   BuiltinMaybe -> [BuiltinMaybeNothing, BuiltinMaybeJust]
@@ -60,6 +60,8 @@ builtinConstructors = \case
   BuiltinAnomaResource -> [BuiltinMkAnomaResource]
   BuiltinAnomaAction -> [BuiltinMkAnomaAction]
   BuiltinEq -> [BuiltinMkEq]
+  BuiltinOrd -> [BuiltinMkOrd]
+  BuiltinOrdering -> [BuiltinOrderingLT, BuiltinOrderingEQ, BuiltinOrderingGT]
 
 data BuiltinInductive
   = BuiltinNat
@@ -69,6 +71,8 @@ data BuiltinInductive
   | BuiltinMaybe
   | BuiltinPair
   | BuiltinEq
+  | BuiltinOrd
+  | BuiltinOrdering
   | BuiltinPoseidonState
   | BuiltinEcPoint
   | BuiltinAnomaResource
@@ -90,6 +94,8 @@ instance Pretty BuiltinInductive where
     BuiltinMaybe -> Str.maybe_
     BuiltinPair -> Str.pair
     BuiltinEq -> Str.eq
+    BuiltinOrd -> Str.ord
+    BuiltinOrdering -> Str.ordering
     BuiltinPoseidonState -> Str.cairoPoseidonState
     BuiltinEcPoint -> Str.cairoEcPoint
     BuiltinAnomaResource -> Str.anomaResource
@@ -113,17 +119,25 @@ instance Pretty BuiltinConstructor where
     BuiltinMkAnomaResource -> Str.anomaMkResource
     BuiltinMkAnomaAction -> Str.anomaMkAction
     BuiltinMkEq -> Str.mkEq
+    BuiltinMkOrd -> Str.mkOrd
+    BuiltinOrderingLT -> Str.lt
+    BuiltinOrderingEQ -> Str.eq
+    BuiltinOrderingGT -> Str.gt
 
 data BuiltinConstructor
   = BuiltinNatZero
   | BuiltinNatSuc
   | BuiltinBoolTrue
   | BuiltinBoolFalse
+  | BuiltinOrderingLT
+  | BuiltinOrderingEQ
+  | BuiltinOrderingGT
   | BuiltinIntOfNat
   | BuiltinIntNegSuc
   | BuiltinListNil
   | BuiltinListCons
   | BuiltinMkEq
+  | BuiltinMkOrd
   | BuiltinMaybeNothing
   | BuiltinMaybeJust
   | BuiltinPairConstr
@@ -167,6 +181,7 @@ data BuiltinFunction
   | BuiltinIntLt
   | BuiltinFromNat
   | BuiltinIsEqual
+  | BuiltinOrdCompare
   | BuiltinFromInt
   | BuiltinSeq
   | BuiltinMonadBind
@@ -209,6 +224,7 @@ instance Pretty BuiltinFunction where
     BuiltinFromInt -> Str.fromInt
     BuiltinSeq -> Str.builtinSeq
     BuiltinIsEqual -> Str.isEqual
+    BuiltinOrdCompare -> Str.compare
     BuiltinMonadBind -> Str.builtinMonadBind
 
 data BuiltinAxiom
@@ -441,6 +457,7 @@ isNatBuiltin = \case
   BuiltinNatLt -> True
   BuiltinNatEq -> True
   --
+  BuiltinOrdCompare -> False
   BuiltinIsEqual -> False
   BuiltinAssert -> False
   BuiltinBoolIf -> False
@@ -495,13 +512,15 @@ isIntBuiltin = \case
   BuiltinFromInt -> False
   BuiltinSeq -> False
   BuiltinIsEqual -> False
+  BuiltinOrdCompare -> False
   BuiltinMonadBind -> False
 
 isCastBuiltin :: BuiltinFunction -> Bool
 isCastBuiltin = \case
   BuiltinFromNat -> True
   BuiltinFromInt -> True
   --
+  BuiltinOrdCompare -> False
   BuiltinIsEqual -> False
   BuiltinAssert -> False
   BuiltinIntEq -> False
@@ -543,6 +562,7 @@ isIgnoredBuiltin f
         .&&. (not . isCastBuiltin)
         .&&. (/= BuiltinMonadBind)
         .&&. (/= BuiltinIsEqual)
+        .&&. (/= BuiltinOrdCompare)
         $ f
 
     explicit :: Bool
@@ -575,6 +595,8 @@ isIgnoredBuiltin f
       BuiltinNatEq -> False
       -- Eq
       BuiltinIsEqual -> False
+      -- Ord
+      BuiltinOrdCompare -> False
       -- Monad
       BuiltinMonadBind -> False
       -- Ignored

src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs

@@ -269,8 +269,8 @@ declareBoolBuiltins =
   declareInductiveBuiltins
     "Bool"
     (Just (BuiltinTypeInductive BuiltinBool))
-    [ (BuiltinTag TagTrue, "true", const mkTypeBool', Just BuiltinBoolTrue),
-      (BuiltinTag TagFalse, "false", const mkTypeBool', Just BuiltinBoolFalse)
+    [ (BuiltinTag TagFalse, "false", const mkTypeBool', Just BuiltinBoolFalse),
+      (BuiltinTag TagTrue, "true", const mkTypeBool', Just BuiltinBoolTrue)
     ]
 
 declareNatBuiltins :: (Member InfoTableBuilder r) => Sem r ()

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

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

src/Juvix/Compiler/Core/Translation/FromInternal.hs

@@ -215,23 +215,28 @@ goConstructor sym ctor = do
 
     ctorTag :: Maybe Internal.BuiltinConstructor -> Sem r Tag
     ctorTag = \case
-      Just Internal.BuiltinBoolTrue -> return (BuiltinTag TagTrue)
-      Just Internal.BuiltinBoolFalse -> return (BuiltinTag TagFalse)
-      Just Internal.BuiltinMkEq -> freshTag
-      Just Internal.BuiltinNatZero -> freshTag
-      Just Internal.BuiltinNatSuc -> freshTag
-      Just Internal.BuiltinIntOfNat -> freshTag
-      Just Internal.BuiltinIntNegSuc -> freshTag
-      Just Internal.BuiltinListNil -> freshTag
-      Just Internal.BuiltinListCons -> freshTag
-      Just Internal.BuiltinMaybeNothing -> freshTag
-      Just Internal.BuiltinMaybeJust -> freshTag
-      Just Internal.BuiltinPairConstr -> freshTag
-      Just Internal.BuiltinMkPoseidonState -> freshTag
-      Just Internal.BuiltinMkEcPoint -> freshTag
-      Just Internal.BuiltinMkAnomaAction -> freshTag
-      Just Internal.BuiltinMkAnomaResource -> freshTag
       Nothing -> freshTag
+      Just b -> case b of
+        Internal.BuiltinBoolTrue -> return (BuiltinTag TagTrue)
+        Internal.BuiltinBoolFalse -> return (BuiltinTag TagFalse)
+        Internal.BuiltinMkEq -> freshTag
+        Internal.BuiltinNatZero -> freshTag
+        Internal.BuiltinNatSuc -> freshTag
+        Internal.BuiltinIntOfNat -> freshTag
+        Internal.BuiltinIntNegSuc -> freshTag
+        Internal.BuiltinListNil -> freshTag
+        Internal.BuiltinListCons -> freshTag
+        Internal.BuiltinMaybeNothing -> freshTag
+        Internal.BuiltinMaybeJust -> freshTag
+        Internal.BuiltinPairConstr -> freshTag
+        Internal.BuiltinMkPoseidonState -> freshTag
+        Internal.BuiltinMkEcPoint -> freshTag
+        Internal.BuiltinMkAnomaAction -> freshTag
+        Internal.BuiltinMkAnomaResource -> freshTag
+        Internal.BuiltinMkOrd -> freshTag
+        Internal.BuiltinOrderingLT -> freshTag
+        Internal.BuiltinOrderingGT -> freshTag
+        Internal.BuiltinOrderingEQ -> freshTag
 
     ctorType :: Sem r Type
     ctorType =

src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs

@@ -55,6 +55,7 @@ fromCore fsize tab =
       BuiltinIntLt -> False
       BuiltinSeq -> False
       BuiltinIsEqual -> False
+      BuiltinOrdCompare -> False
       BuiltinMonadBind -> True -- TODO revise
       BuiltinFromNat -> True
       BuiltinFromInt -> True
@@ -64,6 +65,10 @@ fromCore fsize tab =
       BuiltinListNil -> True
       BuiltinListCons -> True
       BuiltinMkEq -> True
+      BuiltinMkOrd -> True
+      BuiltinOrderingLT -> True
+      BuiltinOrderingGT -> True
+      BuiltinOrderingEQ -> True
       BuiltinMkPoseidonState -> True
       BuiltinMkEcPoint -> True
       BuiltinMaybeNothing -> True
@@ -146,6 +151,8 @@ fromCore fsize tab =
         BuiltinEq -> True
         BuiltinMaybe -> True
         BuiltinPair -> True
+        BuiltinOrd -> True
+        BuiltinOrdering -> True
         BuiltinPoseidonState -> True
         BuiltinEcPoint -> True
         BuiltinNat -> False

src/Juvix/Compiler/Internal/Data/InfoTable.hs

@@ -263,5 +263,15 @@ mkConstructorEntries d =
       let _constructorInfoType = c ^. inductiveConstructorType,
       let _constructorInfoName = c ^. inductiveConstructorName,
       let _constructorInfoTrait = d ^. inductiveTrait,
-      let _constructorInfoRecord = c ^. inductiveConstructorIsRecord
+      let _constructorInfoRecord = c ^. inductiveConstructorIsRecord,
+      let _constructorSelfRecursiveArgs = selfRecursiveArgs (c ^. inductiveConstructorType)
   ]
+  where
+    selfRecursiveArgs :: Expression -> [Bool]
+    selfRecursiveArgs constrTy = constructorArgs constrTy ^.. each . paramType . to (== ty)
+      where
+        ty :: Expression
+        ty =
+          foldExplicitApplication
+            (toExpression (d ^. inductiveName))
+            (d ^.. inductiveParameters . each . inductiveParamName . to toExpression)

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

@@ -383,6 +383,14 @@ unfoldLambdaClauses t = do
       mkClause LambdaClause {..} = first (appendList _lambdaPatterns) (unfoldLambda _lambdaBody)
   return (mkClause <$> _lambdaClauses)
 
+mkLambda :: NonEmpty LambdaClause -> Expression
+mkLambda c =
+  ExpressionLambda
+    Lambda
+      { _lambdaType = Nothing,
+        _lambdaClauses = c
+      }
+
 -- Unfolds *single* clause lambdas
 unfoldLambda :: Expression -> ([PatternArg], Expression)
 unfoldLambda t = case t of
@@ -525,6 +533,9 @@ instance IsExpression Iden where
 instance IsExpression Expression where
   toExpression = id
 
+instance IsExpression Case where
+  toExpression = ExpressionCase
+
 instance IsExpression Hole where
   toExpression = ExpressionHole
 
@@ -655,10 +666,30 @@ freshVar _nameLoc n = do
         _nameLoc
       }
 
+mkCaseBranch :: PatternArg -> Expression -> CaseBranch
+mkCaseBranch pat body =
+  CaseBranch
+    { _caseBranchPattern = pat,
+      _caseBranchRhs = CaseBranchRhsExpression body
+    }
+
+mkCase :: Expression -> NonEmpty CaseBranch -> Expression
+mkCase cexpr clauses =
+  toExpression
+    Case
+      { _caseExpression = cexpr,
+        _caseBranches = clauses,
+        _caseExpressionType = Nothing,
+        _caseExpressionWholeType = Nothing
+      }
+
+mkVarPattern :: VarName -> IsImplicit -> PatternArg
+mkVarPattern var impl = PatternArg impl Nothing (PatternVariable var)
+
 genWildcard :: forall r'. (Members '[NameIdGen] r') => Interval -> IsImplicit -> Sem r' PatternArg
 genWildcard loc impl = do
   var <- varFromWildcard (Wildcard loc)
-  return (PatternArg impl Nothing (PatternVariable var))
+  return (mkVarPattern var impl)
 
 freshInstanceHole :: (Members '[NameIdGen] r) => Interval -> Sem r InstanceHole
 freshInstanceHole l = mkInstanceHole l <$> freshNameId
@@ -790,6 +821,13 @@ isSmallUniverse' = \case
 isTypeConstructor :: Expression -> Bool
 isTypeConstructor = isSmallUniverse' . snd . unfoldFunType
 
+explicitApplicationArg :: (IsExpression expr) => expr -> ApplicationArg
+explicitApplicationArg e =
+  ApplicationArg
+    { _appArgIsImplicit = Explicit,
+      _appArg = toExpression e
+    }
+
 explicitPatternArg :: Pattern -> PatternArg
 explicitPatternArg _patternArgPattern =
   PatternArg

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

@@ -200,6 +200,8 @@ checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go
       BuiltinAnomaResource -> return ()
       BuiltinAnomaAction -> return ()
       BuiltinEq -> return ()
+      BuiltinOrd -> return ()
+      BuiltinOrdering -> 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