From 9f0f0fa271bfa50492f2077424a90ba600e9f5a1 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 26 Nov 2024 17:33:20 +0100
Subject: [PATCH 1/7] Squashed commit of the following:

commit 432114c2de274bfb7c20e5d406e50e69ed095559
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Tue Nov 26 16:19:56 2024 +0100

    test086 -> test087

commit 8b3f47b3d5248dd47c0e93a42b97fbba4cde4d04
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Fri Nov 22 17:50:05 2024 +0100

    move

commit 7f97da93c4cedc36614de05cce333613502765b7
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Fri Nov 22 15:35:19 2024 +0100

    change order of definition

commit 094c6e934aaa704ee0a76e2679ae780fcf5cddca
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Fri Nov 22 13:39:14 2024 +0100

    add test

commit 42a3476e526174c822997472d457e5a6157900ae
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Fri Nov 22 13:13:09 2024 +0100

    refactor

commit b5fe58ff38ff78cb092466a52ebafe724d05afe4
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Fri Nov 22 11:05:24 2024 +0100

    change order of Bool constructors

commit 03210ab8005fbd54900c31e31b189d905d47e3ec
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Fri Nov 22 10:12:17 2024 +0100

    update stdlib

commit 59456dfef40db738f65659d4c32f58120bac9aad
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Thu Nov 21 19:52:23 2024 +0100

    update stdlib

commit 0f2fae6196720f65b70343e217e4e302404b7cc6
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Thu Nov 21 19:42:00 2024 +0100

    decrease clause number

commit 25325bc1791fe0360f769e64af2a081089fbd7e3
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Thu Nov 21 19:28:53 2024 +0100

    improve

commit 6fe818e2ae9a32e01c48a74a539389ebb7e50f61
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Thu Nov 21 18:53:31 2024 +0100

    fixes

commit 5858b9bd7191c91d7b996603311f93cc3861e890
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Thu Nov 21 16:59:39 2024 +0100

    derive ord

commit 6c4db73a189ee44bf6cc001172dc611ed8645120
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Wed Nov 20 18:05:12 2024 +0100

    wip
---
 .../package-base/Juvix/Builtin/V1/Bool.juvix  |   4 +-
 src/Juvix/Compiler/Builtins.hs                |   4 +
 src/Juvix/Compiler/Builtins/Ord.hs            |  25 ++
 src/Juvix/Compiler/Builtins/Ordering.hs       |   7 +
 src/Juvix/Compiler/Concrete/Data/Builtins.hs  |  24 +-
 .../Compiler/Core/Data/InfoTableBuilder.hs    |   4 +-
 src/Juvix/Compiler/Core/Pretty/Base.hs        |   2 +
 .../Compiler/Core/Translation/FromInternal.hs |  37 +--
 .../Core/Translation/Stripped/FromCore.hs     |   7 +
 src/Juvix/Compiler/Internal/Extra/Base.hs     |  33 ++-
 .../Internal/Extra/DependencyBuilder.hs       |   2 +
 src/Juvix/Compiler/Internal/Language.hs       |   5 +-
 .../Internal/Translation/FromConcrete.hs      | 264 ++++++++++++++----
 src/Juvix/Extra/Strings.hs                    |  18 ++
 src/Juvix/Prelude/Effects/Input.hs            |  10 +
 test/Compilation/Positive.hs                  |   7 +-
 tests/Compilation/positive/out/test087.out    |   5 +
 tests/Compilation/positive/test087.juvix      |  26 ++
 tests/negative/Internal/LazyBuiltin.juvix     |   4 +-
 19 files changed, 412 insertions(+), 76 deletions(-)
 create mode 100644 src/Juvix/Compiler/Builtins/Ord.hs
 create mode 100644 src/Juvix/Compiler/Builtins/Ordering.hs
 create mode 100644 tests/Compilation/positive/out/test087.out
 create mode 100644 tests/Compilation/positive/test087.juvix

diff --git a/include/package-base/Juvix/Builtin/V1/Bool.juvix b/include/package-base/Juvix/Builtin/V1/Bool.juvix
index 72e7d0616b..2795fd475f 100644
--- a/include/package-base/Juvix/Builtin/V1/Bool.juvix
+++ b/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;
diff --git a/src/Juvix/Compiler/Builtins.hs b/src/Juvix/Compiler/Builtins.hs
index dda105ea62..4e18415a4a 100644
--- a/src/Juvix/Compiler/Builtins.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Builtins/Ord.hs b/src/Juvix/Compiler/Builtins/Ord.hs
new file mode 100644
index 0000000000..5146870ef8
--- /dev/null
+++ b/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 ()
diff --git a/src/Juvix/Compiler/Builtins/Ordering.hs b/src/Juvix/Compiler/Builtins/Ordering.hs
new file mode 100644
index 0000000000..c3b1986cdb
--- /dev/null
+++ b/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 ()
diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
index 64ab634fd3..27ef4f43d3 100644
--- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs
+++ b/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,6 +512,7 @@ isIntBuiltin = \case
   BuiltinFromInt -> False
   BuiltinSeq -> False
   BuiltinIsEqual -> False
+  BuiltinOrdCompare -> False
   BuiltinMonadBind -> False
 
 isCastBuiltin :: BuiltinFunction -> Bool
@@ -502,6 +520,7 @@ 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
diff --git a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
index aabf4a5b98..b630bae9ed 100644
--- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
+++ b/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 ()
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index 0bc1b6f237..57af9cb552 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
index b85a36eb5b..c2aa512222 100644
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/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 =
diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
index c90354ad68..32c56501e0 100644
--- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs
index 8573a0916c..f85fb14257 100644
--- a/src/Juvix/Compiler/Internal/Extra/Base.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
index cdd895b7c1..c87f3030be 100644
--- a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
+++ b/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)
diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs
index 15be717869..f3e43e2a4f 100644
--- a/src/Juvix/Compiler/Internal/Language.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index edef4b6bdf..42ddd050d8 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -64,6 +64,24 @@ newtype DefaultArgsStack = DefaultArgsStack
 
 makeLenses ''DefaultArgsStack
 
+data EqBuiltins = EqBuiltins
+  { _eqBuiltinIsEqual :: Internal.Name,
+    _eqBuiltinTrue :: Internal.Name,
+    _eqBuiltinFalse :: Internal.Name,
+    _eqBuiltinAnd :: Internal.Name
+  }
+
+makeLenses ''EqBuiltins
+
+data OrdBuiltins = OrdBuiltins
+  { _ordBuiltinCompare :: Internal.Name,
+    _ordBuiltinLt :: Internal.Name,
+    _ordBuiltinEq :: Internal.Name,
+    _ordBuiltinGt :: Internal.Name
+  }
+
+makeLenses ''OrdBuiltins
+
 data DerivingArgs = DerivingArgs
   { _derivingPragmas :: Maybe ParsedPragmas,
     _derivingInstanceName :: Internal.FunctionName,
@@ -295,7 +313,7 @@ goModuleBody stmts = evalState emptyLocalTable $ do
   funs :: [Indexed Internal.PreStatement] <-
     concat
       <$> sequence
-        [ return . map (Indexed i . Internal.PreFunctionDef) =<< defs
+        [ map (Indexed i . Internal.PreFunctionDef) <$> defs
           | Indexed i s <- ss,
             let defs = mkFunctionLike s
         ]
@@ -312,8 +330,8 @@ goModuleBody stmts = evalState emptyLocalTable $ do
     mkFunctionLike :: Statement 'Scoped -> Sem (State LocalTable ': r) [Internal.FunctionDef]
     mkFunctionLike s = case s of
       StatementFunctionDef d -> goFunctionDef d
-      StatementProjectionDef d -> goProjectionDef d >>= return . pure
-      StatementDeriving d -> goDeriving d >>= return . pure
+      StatementProjectionDef d -> pure <$> goProjectionDef d
+      StatementDeriving d -> pure <$> goDeriving d
       StatementSyntax {} -> return []
       StatementImport {} -> return []
       StatementInductive {} -> return []
@@ -447,6 +465,7 @@ deriveTrait ::
   Sem r Internal.FunctionDef
 deriveTrait = \case
   Internal.DerivingEq -> deriveEq
+  Internal.DerivingOrd -> deriveOrd
 
 findDerivingTrait ::
   forall r.
@@ -510,6 +529,14 @@ getDefinedConstructor ind = do
   tbl2 <- asks (^. infoConstructors . at ind)
   return (fromJust (tbl1 <|> tbl2))
 
+getDefinedInductiveConstructors ::
+  (Members '[Reader Internal.InfoTable, State LocalTable] r) =>
+  Internal.InductiveName ->
+  Sem r [ConstructorInfo]
+getDefinedInductiveConstructors d = do
+  i <- getDefinedInductive d
+  mapM getDefinedConstructor (i ^. Internal.inductiveInfoConstructors)
+
 getDefinedInductive ::
   (Members '[Reader Internal.InfoTable, State LocalTable] r) =>
   Internal.InductiveName ->
@@ -536,6 +563,148 @@ 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 <- derivingGetConstrs ret args
+  argsInfo <- goArgsInfo _derivingInstanceName
+  let loc = getLoc ordName
+  mkOrd <- getBuiltin loc BuiltinMkOrd
+  bcmp <- getBuiltin loc BuiltinOrdCompare
+  blt <- getBuiltin loc BuiltinOrderingLT
+  bgt <- getBuiltin loc BuiltinOrderingGT
+  beq <- getBuiltin loc BuiltinOrderingEQ
+  let bs =
+        OrdBuiltins
+          { _ordBuiltinCompare = bcmp,
+            _ordBuiltinLt = blt,
+            _ordBuiltinGt = bgt,
+            _ordBuiltinEq = beq
+          }
+  lam <- genOrdCompare (getLoc _derivingInstanceName) bs arg
+  let ty = Internal.foldFunType _derivingParameters ret
+      body = mkOrd Internal.@@ lam
+  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
+      }
+  where
+    ret :: Internal.Expression
+    ret = Internal.foldApplication (Internal.toExpression ordName) args
+
+    ordName :: Internal.InductiveName
+    args :: [Internal.ApplicationArg]
+    (ordName, args) = _derivingReturnType
+
+genOrdCompare ::
+  forall r.
+  (Members '[NameIdGen] r) =>
+  Interval ->
+  OrdBuiltins ->
+  [ConstructorInfo] ->
+  Sem r Internal.Expression
+genOrdCompare loc bs cs = do
+  res <-
+    fmap nonEmpty
+      . execOutputList
+      . runInputList cs
+      $ repeatOnInput go
+  Internal.mkLambda <$> case res of
+    Nothing -> pure <$> emptyTypeClause
+    Just l -> return l
+  where
+    emptyTypeClause :: Sem r Internal.LambdaClause
+    emptyTypeClause = do
+      w1 <- Internal.genWildcard loc Explicit
+      w2 <- Internal.genWildcard loc Explicit
+      return
+        Internal.LambdaClause
+          { _lambdaBody = Internal.toExpression (bs ^. ordBuiltinEq),
+            _lambdaPatterns = w1 :| [w2]
+          }
+
+    go :: (Members '[NameIdGen, Output Internal.LambdaClause, Input ConstructorInfo] r') => ConstructorInfo -> Sem r' ()
+    go c = do
+      isLast <- isEndOfInput @ConstructorInfo
+      let mkPat = Internal.genConstructorPattern loc Explicit c
+      (p1, v1) <- mkPat
+      (p2, v2) <- mkPat
+      lord <- lexOrder (zipExact v1 v2)
+      let sameConstr =
+            Internal.LambdaClause
+              { _lambdaPatterns = p1 :| [p2],
+                _lambdaBody = lord
+              }
+      output sameConstr
+      unless isLast $ do
+        p3 <- fst <$> mkPat
+        w3 <- Internal.genWildcard loc Explicit
+        output
+          Internal.LambdaClause
+            { _lambdaPatterns = p3 :| [w3],
+              _lambdaBody = Internal.toExpression (bs ^. ordBuiltinLt)
+            }
+        p4 <- fst <$> mkPat
+        w4 <- Internal.genWildcard loc Explicit
+        output
+          Internal.LambdaClause
+            { _lambdaPatterns = w4 :| [p4],
+              _lambdaBody = Internal.toExpression (bs ^. ordBuiltinGt)
+            }
+
+    lexOrder :: forall r'. (Members '[NameIdGen] r') => [(Internal.VarName, Internal.VarName)] -> Sem r' Internal.Expression
+    lexOrder = lexgo
+      where
+        cmp :: Internal.VarName -> Internal.VarName -> Internal.Expression
+        cmp a b = (bs ^. ordBuiltinCompare) Internal.@@ a Internal.@@ b
+
+        lexgo :: [(Internal.VarName, Internal.VarName)] -> Sem r' Internal.Expression
+        lexgo = \case
+          [] -> return (Internal.toExpression (bs ^. ordBuiltinEq))
+          (x, x') : vs
+            | null vs -> return (cmp x x')
+            | otherwise -> do
+                v <- Internal.freshVar loc "ltGt"
+                let pv = Internal.mkVarPattern v Explicit
+                    mkPat :: Internal.Name -> Internal.PatternArg
+                    mkPat p = Internal.mkConstructorVarPattern Explicit p []
+                    branchNEq = Internal.mkCaseBranch pv (Internal.toExpression v)
+                branchEq <- Internal.mkCaseBranch (mkPat (bs ^. ordBuiltinEq)) <$> lexgo vs
+                let branches = branchEq :| [branchNEq]
+                return (Internal.mkCase (cmp x x') branches)
+
+derivingGetConstrs ::
+  (Members '[Error ScoperError, State LocalTable, Reader S.InfoTable, Reader Internal.InfoTable] r) =>
+  Internal.Expression ->
+  [Internal.ApplicationArg] ->
+  Sem r [Internal.ConstructorInfo]
+derivingGetConstrs retTy args = runFailDefaultM (throwDerivingWrongForm retTy) $ do
+  [Internal.ApplicationArg Explicit a] <- return args
+  Internal.ExpressionIden (Internal.IdenInductive ind) <- return (fst (Internal.unfoldExpressionApp a))
+  getDefinedInductiveConstructors ind
+
 deriveEq ::
   forall r.
   ( Members
@@ -557,7 +726,7 @@ deriveEq DerivingArgs {..} = do
   argsInfo <- goArgsInfo _derivingInstanceName
   lamName <- Internal.freshFunVar (getLoc _derivingInstanceName) ("eq__" <> _derivingInstanceName ^. Internal.nameText)
   let lam = Internal.ExpressionIden (Internal.IdenFunction lamName)
-  lamFun <- eqLambda lam indInfo argty
+  lamFun <- eqLambda lam argty
   lamTy <- Internal.ExpressionHole <$> Internal.freshHole (getLoc _derivingInstanceName)
   let lamDef =
         Internal.FunctionDef
@@ -615,59 +784,57 @@ deriveEq DerivingArgs {..} = do
         toAppArg :: Internal.InductiveParameter -> Internal.ApplicationArg
         toAppArg p = Internal.ApplicationArg Explicit (Internal.toExpression (p ^. Internal.inductiveParamName))
 
-    eqLambda :: Internal.Expression -> Internal.InductiveInfo -> Internal.Expression -> Sem r Internal.Expression
-    eqLambda lam d argty = do
+    eqLambda :: Internal.Expression -> Internal.Expression -> Sem r Internal.Expression
+    eqLambda recDef argty = do
       let loc = getLoc eqName
       band <- getBuiltin loc BuiltinBoolAnd
       btrue <- getBuiltin loc BuiltinBoolTrue
       bfalse <- getBuiltin loc BuiltinBoolFalse
       bisEqual <- getBuiltin loc BuiltinIsEqual
-      case nonEmpty (d ^. Internal.inductiveInfoConstructors) of
+      constrs <- derivingGetConstrs ret args
+      let bs =
+            EqBuiltins
+              { _eqBuiltinTrue = btrue,
+                _eqBuiltinFalse = bfalse,
+                _eqBuiltinIsEqual = bisEqual,
+                _eqBuiltinAnd = band
+              }
+      case nonEmpty constrs of
         Nothing -> return (Internal.toExpression btrue)
         Just cs -> do
-          cl' <- mapM (lambdaClause band btrue bisEqual) cs
+          cl' <- mapM (lambdaClause bs) cs
           defaultCl' <-
             if
-                | notNull (NonEmpty.tail cs) -> Just <$> defaultLambdaClause bfalse
+                | notNull (NonEmpty.tail cs) -> Just <$> defaultLambdaClause bs
                 | otherwise -> return Nothing
-          return
-            ( Internal.ExpressionLambda
-                Internal.Lambda
-                  { _lambdaType = Nothing,
-                    _lambdaClauses = snocNonEmptyMaybe cl' defaultCl'
-                  }
-            )
+          return $
+            Internal.ExpressionLambda
+              Internal.Lambda
+                { _lambdaType = Nothing,
+                  _lambdaClauses = snocNonEmptyMaybe cl' defaultCl'
+                }
       where
-        defaultLambdaClause :: Internal.Name -> Sem r Internal.LambdaClause
-        defaultLambdaClause btrue = do
+        defaultLambdaClause :: EqBuiltins -> Sem r Internal.LambdaClause
+        defaultLambdaClause bs = do
           let loc = getLoc eqName
           p1 <- Internal.genWildcard loc Internal.Explicit
           p2 <- Internal.genWildcard loc Internal.Explicit
           return
             Internal.LambdaClause
               { _lambdaPatterns = p1 :| [p2],
-                _lambdaBody = Internal.toExpression btrue
+                _lambdaBody = Internal.toExpression (bs ^. eqBuiltinFalse)
               }
 
         lambdaClause ::
-          Internal.FunctionName ->
-          Internal.FunctionName ->
-          Internal.FunctionName ->
-          Internal.ConstructorName ->
+          EqBuiltins ->
+          Internal.ConstructorInfo ->
           Sem r Internal.LambdaClause
-        lambdaClause band btrue bisEqual c = do
+        lambdaClause bs cinfo = do
           argsRecursive :: [Bool] <- getRecursiveArgs
-          numArgs :: [IsImplicit] <- getNumArgs
           let loc = getLoc _derivingInstanceName
-              mkpat :: Sem r ([Internal.VarName], Internal.PatternArg)
-              mkpat = runOutputList . runStreamOf allWords $ do
-                xs :: [(IsImplicit, Internal.VarName)] <- forM numArgs $ \impl -> do
-                  v <- yield >>= Internal.freshVar loc
-                  output v
-                  return (impl, v)
-                return (Internal.mkConstructorVarPattern Explicit c xs)
-          (v1, p1) <- mkpat
-          (v2, p2) <- mkpat
+              mkpat = Internal.genConstructorPattern loc Explicit cinfo
+          (p1, v1) <- mkpat
+          (p2, v2) <- mkpat
           return
             Internal.LambdaClause
               { _lambdaPatterns = p1 :| [p2],
@@ -676,34 +843,28 @@ deriveEq DerivingArgs {..} = do
           where
             allEq :: (Internal.IsExpression expr) => [(expr, expr, Bool)] -> Internal.Expression
             allEq k = case nonEmpty k of
-              Nothing -> Internal.toExpression btrue
+              Nothing -> Internal.toExpression (bs ^. eqBuiltinTrue)
               Just l -> mkAnds (fmap (uncurry3 mkEq) l)
 
             mkAnds :: (Internal.IsExpression expr) => NonEmpty expr -> Internal.Expression
             mkAnds = foldl1 mkAnd . fmap Internal.toExpression
 
             mkAnd :: (Internal.IsExpression expr) => expr -> expr -> Internal.Expression
-            mkAnd a b = band Internal.@@ a Internal.@@ b
+            mkAnd a b = (bs ^. eqBuiltinAnd) Internal.@@ a Internal.@@ b
 
             mkEq :: (Internal.IsExpression expr) => expr -> expr -> Bool -> Internal.Expression
             mkEq a b isRec
-              | isRec = lam Internal.@@ a Internal.@@ b
-              | otherwise = bisEqual Internal.@@ a Internal.@@ b
-
-            getNumArgs :: Sem r [IsImplicit]
-            getNumArgs = do
-              def <- getDefinedConstructor c
-              return $
-                def
-                  ^.. Internal.constructorInfoType
-                    . to Internal.constructorArgs
-                    . each
-                    . Internal.paramImplicit
+              | isRec = recDef Internal.@@ a Internal.@@ b
+              | otherwise = (bs ^. eqBuiltinIsEqual) Internal.@@ a Internal.@@ b
 
             getRecursiveArgs :: Sem r [Bool]
             getRecursiveArgs = do
-              def <- getDefinedConstructor c
-              let argTypes = map (^. Internal.paramType) $ Internal.constructorArgs (def ^. Internal.constructorInfoType)
+              let argTypes =
+                    cinfo
+                      ^.. Internal.constructorInfoType
+                        . to Internal.constructorArgs
+                        . each
+                        . Internal.paramType
               return $ map (== argty) argTypes
 
 goFunctionDef ::
@@ -850,6 +1011,8 @@ checkBuiltinInductive ::
 checkBuiltinInductive d b = localBuiltins $ case b of
   BuiltinNat -> checkNatDef d
   BuiltinEq -> checkEqDef d
+  BuiltinOrdering -> checkOrderingDef d
+  BuiltinOrd -> checkOrdDef d
   BuiltinBool -> checkBoolDef d
   BuiltinInt -> checkIntDef d
   BuiltinList -> checkListDef d
@@ -873,6 +1036,7 @@ checkBuiltinFunction ::
 checkBuiltinFunction d f = localBuiltins $ case f of
   BuiltinAssert -> checkAssert d
   BuiltinIsEqual -> checkIsEq d
+  BuiltinOrdCompare -> checkOrdCompare d
   BuiltinNatPlus -> checkNatPlus d
   BuiltinNatSub -> checkNatSub d
   BuiltinNatMul -> checkNatMul d
diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs
index bc5ee62bfd..a3ca02cbb2 100644
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@@ -545,9 +545,24 @@ sseq_ = "seq"
 isEqual :: (IsString s) => s
 isEqual = "isEqual"
 
+compare :: (IsString s) => s
+compare = "compare"
+
+lt :: (IsString s) => s
+lt = "lt"
+
+gt :: (IsString s) => s
+gt = "gt"
+
 eq :: (IsString s) => s
 eq = "eq"
 
+ord :: (IsString s) => s
+ord = "ord"
+
+ordering :: (IsString s) => s
+ordering = "ordering"
+
 assert_ :: (IsString s) => s
 assert_ = "assert"
 
@@ -1154,6 +1169,9 @@ anomaMkAction = "mkAction"
 mkEq :: (IsString s) => s
 mkEq = "mkEq"
 
+mkOrd :: (IsString s) => s
+mkOrd = "mkOrd"
+
 rustFn :: (IsString s) => s
 rustFn = "fn"
 
diff --git a/src/Juvix/Prelude/Effects/Input.hs b/src/Juvix/Prelude/Effects/Input.hs
index 8cc4edf4a5..d2f1f6fe25 100644
--- a/src/Juvix/Prelude/Effects/Input.hs
+++ b/src/Juvix/Prelude/Effects/Input.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
 module Juvix.Prelude.Effects.Input
   ( Input,
     input,
@@ -5,6 +7,8 @@ module Juvix.Prelude.Effects.Input
     inputWhile,
     peekInput,
     runInputList,
+    repeatOnInput,
+    isEndOfInput,
   )
 where
 
@@ -43,5 +47,11 @@ peekInput = do
 runInputList :: [i] -> Sem (Input i ': r) a -> Sem r a
 runInputList = evalStaticRep . Input
 
+isEndOfInput :: forall i r. (Members '[Input i] r) => Sem r Bool
+isEndOfInput = isNothing <$> peekInput @i
+
+repeatOnInput :: (Members '[Input i] r) => (i -> Sem r a) -> Sem r ()
+repeatOnInput m = whenJustM input (m >=> const (repeatOnInput m))
+
 inputJust :: (Members '[Input i] r) => Sem r i
 inputJust = fromMaybe (error "inputJust") <$> input
diff --git a/test/Compilation/Positive.hs b/test/Compilation/Positive.hs
index 3a46fc3a69..1fbdc9d630 100644
--- a/test/Compilation/Positive.hs
+++ b/test/Compilation/Positive.hs
@@ -505,5 +505,10 @@ tests =
         "Test086: Patterns in definitions"
         $(mkRelDir ".")
         $(mkRelFile "test086.juvix")
-        $(mkRelFile "out/test086.out")
+        $(mkRelFile "out/test086.out"),
+      posTest
+        "Test087: Deriving Ord"
+        $(mkRelDir ".")
+        $(mkRelFile "test087.juvix")
+        $(mkRelFile "out/test087.out")
     ]
diff --git a/tests/Compilation/positive/out/test087.out b/tests/Compilation/positive/out/test087.out
new file mode 100644
index 0000000000..df0c967608
--- /dev/null
+++ b/tests/Compilation/positive/out/test087.out
@@ -0,0 +1,5 @@
+Equal
+LessThan
+GreaterThan
+LessThan
+GreaterThan
diff --git a/tests/Compilation/positive/test087.juvix b/tests/Compilation/positive/test087.juvix
new file mode 100644
index 0000000000..0e996b6487
--- /dev/null
+++ b/tests/Compilation/positive/test087.juvix
@@ -0,0 +1,26 @@
+-- Deriving Ord
+module test087;
+
+import Stdlib.Data.Fixity open;
+import Stdlib.Data.Bool open;
+import Stdlib.Data.Pair open;
+import Stdlib.Trait.Ord open;
+import Stdlib.System.IO open;
+
+syntax alias compare := Ord.cmp;
+
+type T :=
+  | One
+  | Two
+  | Three
+  | Four;
+
+deriving instance
+ordT : Ord T;
+
+main : IO :=
+  printLn (compare One One)
+    >>> printLn (compare One Two)
+    >>> printLn (compare Two One)
+    >>> printLn (compare (One, One) (One, Three))
+    >>> printLn (compare (Four, Four) (Four, Three));
diff --git a/tests/negative/Internal/LazyBuiltin.juvix b/tests/negative/Internal/LazyBuiltin.juvix
index cb23733771..b34d3ea33c 100644
--- a/tests/negative/Internal/LazyBuiltin.juvix
+++ b/tests/negative/Internal/LazyBuiltin.juvix
@@ -2,8 +2,8 @@ module LazyBuiltin;
 
 builtin bool
 type Bool :=
-  | true : Bool
-  | false : Bool;
+  | false : Bool
+  | true : Bool;
 
 builtin bool-if
 ite : {A : Type} -> Bool -> A -> A -> A

From 499de4f570c5d5420147304a0e4e89cd1098a8ca Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 26 Nov 2024 19:54:43 +0100
Subject: [PATCH 2/7] extract common

---
 src/Juvix/Compiler/Internal/Extra/Base.hs     |   7 +
 .../Internal/Translation/FromConcrete.hs      | 221 +++++++++++++++---
 2 files changed, 200 insertions(+), 28 deletions(-)

diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs
index f85fb14257..faec8aee0f 100644
--- a/src/Juvix/Compiler/Internal/Extra/Base.hs
+++ b/src/Juvix/Compiler/Internal/Extra/Base.hs
@@ -821,6 +821,13 @@ isSmallUniverse' = \case
 isTypeConstructor :: Expression -> Bool
 isTypeConstructor = isSmallUniverse' . snd . unfoldFunType
 
+explicitApplicationArg :: Expression -> ApplicationArg
+explicitApplicationArg e =
+  ApplicationArg
+    { _appArgIsImplicit = Explicit,
+      _appArg = e
+    }
+
 explicitPatternArg :: Pattern -> PatternArg
 explicitPatternArg _patternArgPattern =
   PatternArg
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index 42ddd050d8..d5f68875c7 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -705,6 +705,189 @@ derivingGetConstrs retTy args = runFailDefaultM (throwDerivingWrongForm retTy) $
   Internal.ExpressionIden (Internal.IdenInductive ind) <- return (fst (Internal.unfoldExpressionApp a))
   getDefinedInductiveConstructors ind
 
+deriveRecursiveBinaryFunction ::
+  (Members '[NameIdGen] r) =>
+  Text ->
+  Internal.Name ->
+  DerivingArgs ->
+  ( ( Internal.ConstructorInfo ->
+      [(Internal.ApplicationArg, Internal.ApplicationArg)] ->
+      [Internal.Expression]
+    ) ->
+    Sem r Internal.Expression
+  ) ->
+  Sem r (Internal.Name, Internal.LetClause)
+deriveRecursiveBinaryFunction label nonSelfRec DerivingArgs {..} mkLamDef = do
+  let instName = _derivingInstanceName
+      loc = getLoc instName
+  recDefName <- Internal.freshFunVar loc (label <> "__" <> instName ^. Internal.nameText)
+  let rfun isRec
+        | isRec = recDefName
+        | otherwise = nonSelfRec
+      mkRecCall cinfo recArgs =
+        let selfRecArgs :: [Bool]
+            selfRecArgs =
+              let argTypes =
+                    cinfo
+                      ^.. Internal.constructorInfoType
+                        . to Internal.constructorArgs
+                        . each
+                        . Internal.paramType
+               in map (== ret) argTypes
+         in [ Internal.foldApplication (Internal.toExpression (rfun isRec)) [arg1, arg2]
+              | ((arg1, arg2), isRec) <- zipExact recArgs selfRecArgs
+            ]
+
+  lamBody <- mkLamDef mkRecCall
+  lamTy <- Internal.ExpressionHole <$> Internal.freshHole (getLoc _derivingInstanceName)
+  let lamDef =
+        Internal.FunctionDef
+          { _funDefTerminating = False,
+            _funDefIsInstanceCoercion = Nothing,
+            _funDefPragmas = mempty,
+            _funDefArgsInfo = [],
+            _funDefDocComment = Nothing,
+            _funDefName = recDefName,
+            _funDefType = lamTy,
+            _funDefBody = lamBody,
+            _funDefBuiltin = Nothing
+          }
+  return (recDefName, Internal.LetMutualBlock (Internal.MutualBlockLet (pure lamDef)))
+  where
+    ret :: Internal.Expression
+    ret = Internal.foldApplication (Internal.toExpression eqName) args
+
+    eqName :: Internal.InductiveName
+    args :: [Internal.ApplicationArg]
+    (eqName, args) = _derivingReturnType
+
+deriveEq2 ::
+  forall r.
+  ( Members
+      '[ Reader S.InfoTable,
+         Reader Internal.InfoTable,
+         State LocalTable,
+         NameIdGen,
+         Error ScoperError,
+         Reader DefaultArgsStack,
+         Reader Pragmas
+       ]
+      r
+  ) =>
+  DerivingArgs ->
+  Sem r Internal.FunctionDef
+deriveEq2 der@DerivingArgs {..} = do
+  argsInfo <- goArgsInfo _derivingInstanceName
+  bs <- mkBuiltins
+  (recDefName, mutblock :: Internal.LetClause) <-
+    deriveRecursiveBinaryFunction "eq" (bs ^. eqBuiltinIsEqual) der (eqLambda bs)
+  mkEq <- getBuiltin (getLoc eqName) BuiltinMkEq
+  let body =
+        Internal.ExpressionLet
+          Internal.Let
+            { _letClauses = pure mutblock,
+              _letExpression = mkEq Internal.@@ recDefName
+            }
+      ty = Internal.foldFunType _derivingParameters ret
+  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
+      }
+  where
+    ret :: Internal.Expression
+    ret = Internal.foldApplication (Internal.toExpression eqName) args
+
+    eqName :: Internal.InductiveName
+    args :: [Internal.ApplicationArg]
+    (eqName, args) = _derivingReturnType
+
+    mkBuiltins :: Sem r EqBuiltins
+    mkBuiltins = do
+      let loc = getLoc eqName
+      band <- getBuiltin loc BuiltinBoolAnd
+      btrue <- getBuiltin loc BuiltinBoolTrue
+      bfalse <- getBuiltin loc BuiltinBoolFalse
+      bisEqual <- getBuiltin loc BuiltinIsEqual
+      return
+        EqBuiltins
+          { _eqBuiltinTrue = btrue,
+            _eqBuiltinFalse = bfalse,
+            _eqBuiltinIsEqual = bisEqual,
+            _eqBuiltinAnd = band
+          }
+
+    eqLambda ::
+      EqBuiltins ->
+      ( Internal.ConstructorInfo ->
+        [(Internal.ApplicationArg, Internal.ApplicationArg)] ->
+        [Internal.Expression]
+      ) ->
+      Sem r Internal.Expression
+    eqLambda bs recCalls = do
+      constrs <- derivingGetConstrs ret args
+      case nonEmpty constrs of
+        Nothing -> return (Internal.toExpression (bs ^. eqBuiltinTrue))
+        Just cs -> do
+          cl' <- mapM lambdaClause cs
+          defaultCl' <-
+            if
+                | notNull (NonEmpty.tail cs) -> Just <$> defaultLambdaClause
+                | otherwise -> return Nothing
+          return $
+            Internal.ExpressionLambda
+              Internal.Lambda
+                { _lambdaType = Nothing,
+                  _lambdaClauses = snocNonEmptyMaybe cl' defaultCl'
+                }
+      where
+        defaultLambdaClause :: Sem r Internal.LambdaClause
+        defaultLambdaClause = do
+          let loc = getLoc eqName
+          p1 <- Internal.genWildcard loc Internal.Explicit
+          p2 <- Internal.genWildcard loc Internal.Explicit
+          return
+            Internal.LambdaClause
+              { _lambdaPatterns = p1 :| [p2],
+                _lambdaBody = Internal.toExpression (bs ^. eqBuiltinFalse)
+              }
+
+        lambdaClause ::
+          Internal.ConstructorInfo ->
+          Sem r Internal.LambdaClause
+        lambdaClause cinfo = do
+          let loc = getLoc _derivingInstanceName
+              mkpat = Internal.genConstructorPattern loc Explicit cinfo
+          (p1, v1) <- mkpat
+          (p2, v2) <- mkpat
+          return
+            Internal.LambdaClause
+              { _lambdaPatterns = p1 :| [p2],
+                _lambdaBody = allEq (zipExact v1 v2)
+              }
+          where
+            allEq :: (Internal.IsExpression expr) => [(expr, expr)] -> Internal.Expression
+            allEq k = case nonEmpty (recCalls cinfo kargs) of
+              Nothing -> Internal.toExpression (bs ^. eqBuiltinTrue)
+              Just l -> mkAnds l
+              where
+                kargs :: [(Internal.ApplicationArg, Internal.ApplicationArg)]
+                kargs = map (over both (Internal.explicitApplicationArg . Internal.toExpression)) k
+
+            mkAnds :: (Internal.IsExpression expr) => NonEmpty expr -> Internal.Expression
+            mkAnds = foldl1 mkAnd . fmap Internal.toExpression
+
+            mkAnd :: (Internal.IsExpression expr) => expr -> expr -> Internal.Expression
+            mkAnd a b = (bs ^. eqBuiltinAnd) Internal.@@ a Internal.@@ b
+
 deriveEq ::
   forall r.
   ( Members
@@ -721,12 +904,9 @@ deriveEq ::
   DerivingArgs ->
   Sem r Internal.FunctionDef
 deriveEq DerivingArgs {..} = do
-  indInfo <- getIndInfo
-  let argty = getArgType indInfo
   argsInfo <- goArgsInfo _derivingInstanceName
-  lamName <- Internal.freshFunVar (getLoc _derivingInstanceName) ("eq__" <> _derivingInstanceName ^. Internal.nameText)
-  let lam = Internal.ExpressionIden (Internal.IdenFunction lamName)
-  lamFun <- eqLambda lam argty
+  recDefName <- Internal.freshFunVar (getLoc _derivingInstanceName) ("eq__" <> _derivingInstanceName ^. Internal.nameText)
+  lamFun <- eqLambda (Internal.toExpression recDefName)
   lamTy <- Internal.ExpressionHole <$> Internal.freshHole (getLoc _derivingInstanceName)
   let lamDef =
         Internal.FunctionDef
@@ -735,7 +915,7 @@ deriveEq DerivingArgs {..} = do
             _funDefPragmas = mempty,
             _funDefArgsInfo = [],
             _funDefDocComment = Nothing,
-            _funDefName = lamName,
+            _funDefName = recDefName,
             _funDefType = lamTy,
             _funDefBody = lamFun,
             _funDefBuiltin = Nothing
@@ -746,7 +926,7 @@ deriveEq DerivingArgs {..} = do
         Internal.ExpressionLet
           Internal.Let
             { _letClauses = pure (Internal.LetMutualBlock (Internal.MutualBlockLet (pure lamDef))),
-              _letExpression = mkEq Internal.@@ lam
+              _letExpression = mkEq Internal.@@ recDefName
             }
       ty = Internal.foldFunType _derivingParameters ret
   return
@@ -769,23 +949,8 @@ deriveEq DerivingArgs {..} = do
     args :: [Internal.ApplicationArg]
     (eqName, args) = _derivingReturnType
 
-    getIndInfo :: Sem r Internal.InductiveInfo
-    getIndInfo = runFailDefaultM (throwDerivingWrongForm ret) $ do
-      [Internal.ApplicationArg Explicit a] <- return args
-      Internal.ExpressionIden (Internal.IdenInductive ind) <- return (fst (Internal.unfoldExpressionApp a))
-      getDefinedInductive ind
-
-    getArgType :: Internal.InductiveInfo -> Internal.Expression
-    getArgType indInfo =
-      Internal.foldApplication
-        (Internal.toExpression (indInfo ^. Internal.inductiveInfoName))
-        (map toAppArg (indInfo ^. Internal.inductiveInfoParameters))
-      where
-        toAppArg :: Internal.InductiveParameter -> Internal.ApplicationArg
-        toAppArg p = Internal.ApplicationArg Explicit (Internal.toExpression (p ^. Internal.inductiveParamName))
-
-    eqLambda :: Internal.Expression -> Internal.Expression -> Sem r Internal.Expression
-    eqLambda recDef argty = do
+    eqLambda :: Internal.Expression -> Sem r Internal.Expression
+    eqLambda recDef = do
       let loc = getLoc eqName
       band <- getBuiltin loc BuiltinBoolAnd
       btrue <- getBuiltin loc BuiltinBoolTrue
@@ -830,7 +995,7 @@ deriveEq DerivingArgs {..} = do
           Internal.ConstructorInfo ->
           Sem r Internal.LambdaClause
         lambdaClause bs cinfo = do
-          argsRecursive :: [Bool] <- getRecursiveArgs
+          let argsRecursive :: [Bool] = getRecursiveArgs
           let loc = getLoc _derivingInstanceName
               mkpat = Internal.genConstructorPattern loc Explicit cinfo
           (p1, v1) <- mkpat
@@ -857,15 +1022,15 @@ deriveEq DerivingArgs {..} = do
               | isRec = recDef Internal.@@ a Internal.@@ b
               | otherwise = (bs ^. eqBuiltinIsEqual) Internal.@@ a Internal.@@ b
 
-            getRecursiveArgs :: Sem r [Bool]
-            getRecursiveArgs = do
+            getRecursiveArgs :: [Bool]
+            getRecursiveArgs =
               let argTypes =
                     cinfo
                       ^.. Internal.constructorInfoType
                         . to Internal.constructorArgs
                         . each
                         . Internal.paramType
-              return $ map (== argty) argTypes
+               in map (== ret) argTypes
 
 goFunctionDef ::
   forall r.

From 0e0b91022f2128e6565f849b04994b1b1362af54 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 26 Nov 2024 19:55:23 +0100
Subject: [PATCH 3/7] remove old

---
 .../Internal/Translation/FromConcrete.hs      | 148 +-----------------
 1 file changed, 2 insertions(+), 146 deletions(-)

diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index d5f68875c7..80e3678a7f 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -761,7 +761,7 @@ deriveRecursiveBinaryFunction label nonSelfRec DerivingArgs {..} mkLamDef = do
     args :: [Internal.ApplicationArg]
     (eqName, args) = _derivingReturnType
 
-deriveEq2 ::
+deriveEq ::
   forall r.
   ( Members
       '[ Reader S.InfoTable,
@@ -776,7 +776,7 @@ deriveEq2 ::
   ) =>
   DerivingArgs ->
   Sem r Internal.FunctionDef
-deriveEq2 der@DerivingArgs {..} = do
+deriveEq der@DerivingArgs {..} = do
   argsInfo <- goArgsInfo _derivingInstanceName
   bs <- mkBuiltins
   (recDefName, mutblock :: Internal.LetClause) <-
@@ -888,150 +888,6 @@ deriveEq2 der@DerivingArgs {..} = do
             mkAnd :: (Internal.IsExpression expr) => expr -> expr -> Internal.Expression
             mkAnd a b = (bs ^. eqBuiltinAnd) Internal.@@ a Internal.@@ b
 
-deriveEq ::
-  forall r.
-  ( Members
-      '[ Reader S.InfoTable,
-         Reader Internal.InfoTable,
-         State LocalTable,
-         NameIdGen,
-         Error ScoperError,
-         Reader DefaultArgsStack,
-         Reader Pragmas
-       ]
-      r
-  ) =>
-  DerivingArgs ->
-  Sem r Internal.FunctionDef
-deriveEq DerivingArgs {..} = do
-  argsInfo <- goArgsInfo _derivingInstanceName
-  recDefName <- Internal.freshFunVar (getLoc _derivingInstanceName) ("eq__" <> _derivingInstanceName ^. Internal.nameText)
-  lamFun <- eqLambda (Internal.toExpression recDefName)
-  lamTy <- Internal.ExpressionHole <$> Internal.freshHole (getLoc _derivingInstanceName)
-  let lamDef =
-        Internal.FunctionDef
-          { _funDefTerminating = False,
-            _funDefIsInstanceCoercion = Nothing,
-            _funDefPragmas = mempty,
-            _funDefArgsInfo = [],
-            _funDefDocComment = Nothing,
-            _funDefName = recDefName,
-            _funDefType = lamTy,
-            _funDefBody = lamFun,
-            _funDefBuiltin = Nothing
-          }
-  mkEq <- getBuiltin (getLoc eqName) BuiltinMkEq
-  pragmas' <- goPragmas _derivingPragmas
-  let body =
-        Internal.ExpressionLet
-          Internal.Let
-            { _letClauses = pure (Internal.LetMutualBlock (Internal.MutualBlockLet (pure lamDef))),
-              _letExpression = mkEq Internal.@@ recDefName
-            }
-      ty = Internal.foldFunType _derivingParameters ret
-  return
-    Internal.FunctionDef
-      { _funDefTerminating = False,
-        _funDefIsInstanceCoercion = Just Internal.IsInstanceCoercionInstance,
-        _funDefPragmas = pragmas',
-        _funDefArgsInfo = argsInfo,
-        _funDefDocComment = Nothing,
-        _funDefName = _derivingInstanceName,
-        _funDefType = ty,
-        _funDefBody = body,
-        _funDefBuiltin = Nothing
-      }
-  where
-    ret :: Internal.Expression
-    ret = Internal.foldApplication (Internal.toExpression eqName) args
-
-    eqName :: Internal.InductiveName
-    args :: [Internal.ApplicationArg]
-    (eqName, args) = _derivingReturnType
-
-    eqLambda :: Internal.Expression -> Sem r Internal.Expression
-    eqLambda recDef = do
-      let loc = getLoc eqName
-      band <- getBuiltin loc BuiltinBoolAnd
-      btrue <- getBuiltin loc BuiltinBoolTrue
-      bfalse <- getBuiltin loc BuiltinBoolFalse
-      bisEqual <- getBuiltin loc BuiltinIsEqual
-      constrs <- derivingGetConstrs ret args
-      let bs =
-            EqBuiltins
-              { _eqBuiltinTrue = btrue,
-                _eqBuiltinFalse = bfalse,
-                _eqBuiltinIsEqual = bisEqual,
-                _eqBuiltinAnd = band
-              }
-      case nonEmpty constrs of
-        Nothing -> return (Internal.toExpression btrue)
-        Just cs -> do
-          cl' <- mapM (lambdaClause bs) cs
-          defaultCl' <-
-            if
-                | notNull (NonEmpty.tail cs) -> Just <$> defaultLambdaClause bs
-                | otherwise -> return Nothing
-          return $
-            Internal.ExpressionLambda
-              Internal.Lambda
-                { _lambdaType = Nothing,
-                  _lambdaClauses = snocNonEmptyMaybe cl' defaultCl'
-                }
-      where
-        defaultLambdaClause :: EqBuiltins -> Sem r Internal.LambdaClause
-        defaultLambdaClause bs = do
-          let loc = getLoc eqName
-          p1 <- Internal.genWildcard loc Internal.Explicit
-          p2 <- Internal.genWildcard loc Internal.Explicit
-          return
-            Internal.LambdaClause
-              { _lambdaPatterns = p1 :| [p2],
-                _lambdaBody = Internal.toExpression (bs ^. eqBuiltinFalse)
-              }
-
-        lambdaClause ::
-          EqBuiltins ->
-          Internal.ConstructorInfo ->
-          Sem r Internal.LambdaClause
-        lambdaClause bs cinfo = do
-          let argsRecursive :: [Bool] = getRecursiveArgs
-          let loc = getLoc _derivingInstanceName
-              mkpat = Internal.genConstructorPattern loc Explicit cinfo
-          (p1, v1) <- mkpat
-          (p2, v2) <- mkpat
-          return
-            Internal.LambdaClause
-              { _lambdaPatterns = p1 :| [p2],
-                _lambdaBody = allEq (zip3Exact v1 v2 argsRecursive)
-              }
-          where
-            allEq :: (Internal.IsExpression expr) => [(expr, expr, Bool)] -> Internal.Expression
-            allEq k = case nonEmpty k of
-              Nothing -> Internal.toExpression (bs ^. eqBuiltinTrue)
-              Just l -> mkAnds (fmap (uncurry3 mkEq) l)
-
-            mkAnds :: (Internal.IsExpression expr) => NonEmpty expr -> Internal.Expression
-            mkAnds = foldl1 mkAnd . fmap Internal.toExpression
-
-            mkAnd :: (Internal.IsExpression expr) => expr -> expr -> Internal.Expression
-            mkAnd a b = (bs ^. eqBuiltinAnd) Internal.@@ a Internal.@@ b
-
-            mkEq :: (Internal.IsExpression expr) => expr -> expr -> Bool -> Internal.Expression
-            mkEq a b isRec
-              | isRec = recDef Internal.@@ a Internal.@@ b
-              | otherwise = (bs ^. eqBuiltinIsEqual) Internal.@@ a Internal.@@ b
-
-            getRecursiveArgs :: [Bool]
-            getRecursiveArgs =
-              let argTypes =
-                    cinfo
-                      ^.. Internal.constructorInfoType
-                        . to Internal.constructorArgs
-                        . each
-                        . Internal.paramType
-               in map (== ret) argTypes
-
 goFunctionDef ::
   forall r.
   (Members '[Reader DefaultArgsStack, Reader Pragmas, Error ScoperError, NameIdGen, Reader S.InfoTable] r) =>

From 78dec074a8e23dc946eda21e21359eb2b4191066 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Tue, 26 Nov 2024 20:29:34 +0100
Subject: [PATCH 4/7] refactor ord

---
 juvix-stdlib                                  |   2 +-
 src/Juvix/Compiler/Internal/Extra/Base.hs     |   4 +-
 .../Internal/Translation/FromConcrete.hs      | 238 +++++++++---------
 3 files changed, 128 insertions(+), 116 deletions(-)

diff --git a/juvix-stdlib b/juvix-stdlib
index a6abb99562..9534bd214d 160000
--- a/juvix-stdlib
+++ b/juvix-stdlib
@@ -1 +1 @@
-Subproject commit a6abb9956261f152cea5b14a0d31a9cce6c1957f
+Subproject commit 9534bd214df2983f4f5918ddcff3703f63bd1de1
diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs
index faec8aee0f..f8a3c4f930 100644
--- a/src/Juvix/Compiler/Internal/Extra/Base.hs
+++ b/src/Juvix/Compiler/Internal/Extra/Base.hs
@@ -821,11 +821,11 @@ isSmallUniverse' = \case
 isTypeConstructor :: Expression -> Bool
 isTypeConstructor = isSmallUniverse' . snd . unfoldFunType
 
-explicitApplicationArg :: Expression -> ApplicationArg
+explicitApplicationArg :: (IsExpression expr) => expr -> ApplicationArg
 explicitApplicationArg e =
   ApplicationArg
     { _appArgIsImplicit = Explicit,
-      _appArg = e
+      _appArg = toExpression e
     }
 
 explicitPatternArg :: Pattern -> PatternArg
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index 80e3678a7f..36ccfe6075 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -74,8 +74,7 @@ data EqBuiltins = EqBuiltins
 makeLenses ''EqBuiltins
 
 data OrdBuiltins = OrdBuiltins
-  { _ordBuiltinCompare :: Internal.Name,
-    _ordBuiltinLt :: Internal.Name,
+  { _ordBuiltinLt :: Internal.Name,
     _ordBuiltinEq :: Internal.Name,
     _ordBuiltinGt :: Internal.Name
   }
@@ -578,7 +577,7 @@ deriveOrd ::
   ) =>
   DerivingArgs ->
   Sem r Internal.FunctionDef
-deriveOrd DerivingArgs {..} = do
+deriveOrd der@DerivingArgs {..} = do
   arg <- derivingGetConstrs ret args
   argsInfo <- goArgsInfo _derivingInstanceName
   let loc = getLoc ordName
@@ -589,14 +588,18 @@ deriveOrd DerivingArgs {..} = do
   beq <- getBuiltin loc BuiltinOrderingEQ
   let bs =
         OrdBuiltins
-          { _ordBuiltinCompare = bcmp,
-            _ordBuiltinLt = blt,
+          { _ordBuiltinLt = blt,
             _ordBuiltinGt = bgt,
             _ordBuiltinEq = beq
           }
-  lam <- genOrdCompare (getLoc _derivingInstanceName) bs arg
-  let ty = Internal.foldFunType _derivingParameters ret
-      body = mkOrd Internal.@@ lam
+  (recName, mutblock) <- deriveRecursiveBinaryFunction "ord" bcmp der (genOrdCompare (getLoc _derivingInstanceName) bs arg)
+  let body =
+        Internal.ExpressionLet
+          Internal.Let
+            { _letClauses = pure mutblock,
+              _letExpression = mkOrd Internal.@@ recName
+            }
+      ty = Internal.foldFunType _derivingParameters ret
   pragmas' <- goPragmas _derivingPragmas
   return
     Internal.FunctionDef
@@ -618,82 +621,98 @@ deriveOrd DerivingArgs {..} = do
     args :: [Internal.ApplicationArg]
     (ordName, args) = _derivingReturnType
 
-genOrdCompare ::
-  forall r.
-  (Members '[NameIdGen] r) =>
-  Interval ->
-  OrdBuiltins ->
-  [ConstructorInfo] ->
-  Sem r Internal.Expression
-genOrdCompare loc bs cs = do
-  res <-
-    fmap nonEmpty
-      . execOutputList
-      . runInputList cs
-      $ repeatOnInput go
-  Internal.mkLambda <$> case res of
-    Nothing -> pure <$> emptyTypeClause
-    Just l -> return l
-  where
-    emptyTypeClause :: Sem r Internal.LambdaClause
-    emptyTypeClause = do
-      w1 <- Internal.genWildcard loc Explicit
-      w2 <- Internal.genWildcard loc Explicit
-      return
-        Internal.LambdaClause
-          { _lambdaBody = Internal.toExpression (bs ^. ordBuiltinEq),
-            _lambdaPatterns = w1 :| [w2]
-          }
-
-    go :: (Members '[NameIdGen, Output Internal.LambdaClause, Input ConstructorInfo] r') => ConstructorInfo -> Sem r' ()
-    go c = do
-      isLast <- isEndOfInput @ConstructorInfo
-      let mkPat = Internal.genConstructorPattern loc Explicit c
-      (p1, v1) <- mkPat
-      (p2, v2) <- mkPat
-      lord <- lexOrder (zipExact v1 v2)
-      let sameConstr =
+    genOrdCompare ::
+      forall r'.
+      (Members '[NameIdGen] r') =>
+      Interval ->
+      OrdBuiltins ->
+      [ConstructorInfo] ->
+      (Bool -> Internal.ApplicationArg -> Internal.ApplicationArg -> Internal.Expression) ->
+      Sem r' Internal.Expression
+    genOrdCompare loc bs cs recCmp = do
+      res <-
+        fmap nonEmpty
+          . execOutputList
+          . runInputList cs
+          $ repeatOnInput go
+      Internal.mkLambda <$> case res of
+        Nothing -> pure <$> emptyTypeClause
+        Just l -> return l
+      where
+        emptyTypeClause :: Sem r' Internal.LambdaClause
+        emptyTypeClause = do
+          w1 <- Internal.genWildcard loc Explicit
+          w2 <- Internal.genWildcard loc Explicit
+          return
             Internal.LambdaClause
-              { _lambdaPatterns = p1 :| [p2],
-                _lambdaBody = lord
+              { _lambdaBody = Internal.toExpression (bs ^. ordBuiltinEq),
+                _lambdaPatterns = w1 :| [w2]
               }
-      output sameConstr
-      unless isLast $ do
-        p3 <- fst <$> mkPat
-        w3 <- Internal.genWildcard loc Explicit
-        output
-          Internal.LambdaClause
-            { _lambdaPatterns = p3 :| [w3],
-              _lambdaBody = Internal.toExpression (bs ^. ordBuiltinLt)
-            }
-        p4 <- fst <$> mkPat
-        w4 <- Internal.genWildcard loc Explicit
-        output
-          Internal.LambdaClause
-            { _lambdaPatterns = w4 :| [p4],
-              _lambdaBody = Internal.toExpression (bs ^. ordBuiltinGt)
-            }
 
-    lexOrder :: forall r'. (Members '[NameIdGen] r') => [(Internal.VarName, Internal.VarName)] -> Sem r' Internal.Expression
-    lexOrder = lexgo
-      where
-        cmp :: Internal.VarName -> Internal.VarName -> Internal.Expression
-        cmp a b = (bs ^. ordBuiltinCompare) Internal.@@ a Internal.@@ b
-
-        lexgo :: [(Internal.VarName, Internal.VarName)] -> Sem r' Internal.Expression
-        lexgo = \case
-          [] -> return (Internal.toExpression (bs ^. ordBuiltinEq))
-          (x, x') : vs
-            | null vs -> return (cmp x x')
-            | otherwise -> do
-                v <- Internal.freshVar loc "ltGt"
-                let pv = Internal.mkVarPattern v Explicit
-                    mkPat :: Internal.Name -> Internal.PatternArg
-                    mkPat p = Internal.mkConstructorVarPattern Explicit p []
-                    branchNEq = Internal.mkCaseBranch pv (Internal.toExpression v)
-                branchEq <- Internal.mkCaseBranch (mkPat (bs ^. ordBuiltinEq)) <$> lexgo vs
-                let branches = branchEq :| [branchNEq]
-                return (Internal.mkCase (cmp x x') branches)
+        go ::
+          (Members '[NameIdGen, Output Internal.LambdaClause, Input ConstructorInfo] r'') =>
+          ConstructorInfo ->
+          Sem r'' ()
+        go c = do
+          isLast <- isEndOfInput @ConstructorInfo
+          let mkPat = Internal.genConstructorPattern loc Explicit c
+          (p1, v1) <- mkPat
+          (p2, v2) <- mkPat
+          let selfRecArgs :: [Bool]
+              selfRecArgs =
+                c
+                  ^.. Internal.constructorInfoType
+                    . to Internal.constructorArgs
+                    . each
+                    . Internal.paramType
+                    . to (== ret)
+          lord <- lexOrder (zip3Exact selfRecArgs v1 v2)
+          let sameConstr =
+                Internal.LambdaClause
+                  { _lambdaPatterns = p1 :| [p2],
+                    _lambdaBody = lord
+                  }
+          output sameConstr
+          unless isLast $ do
+            p3 <- fst <$> mkPat
+            w3 <- Internal.genWildcard loc Explicit
+            output
+              Internal.LambdaClause
+                { _lambdaPatterns = p3 :| [w3],
+                  _lambdaBody = Internal.toExpression (bs ^. ordBuiltinLt)
+                }
+            p4 <- fst <$> mkPat
+            w4 <- Internal.genWildcard loc Explicit
+            output
+              Internal.LambdaClause
+                { _lambdaPatterns = w4 :| [p4],
+                  _lambdaBody = Internal.toExpression (bs ^. ordBuiltinGt)
+                }
+
+        lexOrder ::
+          forall r''.
+          (Members '[NameIdGen] r'') =>
+          [(Bool, Internal.VarName, Internal.VarName)] ->
+          Sem r'' Internal.Expression
+        lexOrder = lexgo
+          where
+            cmp :: Bool -> Internal.VarName -> Internal.VarName -> Internal.Expression
+            cmp isRec a b = recCmp isRec (Internal.explicitApplicationArg a) (Internal.explicitApplicationArg b)
+
+            lexgo :: [(Bool, Internal.VarName, Internal.VarName)] -> Sem r'' Internal.Expression
+            lexgo = \case
+              [] -> return (Internal.toExpression (bs ^. ordBuiltinEq))
+              (isRec, x, x') : vs
+                | null vs -> return (cmp isRec x x')
+                | otherwise -> do
+                    v <- Internal.freshVar loc "ltGt"
+                    let pv = Internal.mkVarPattern v Explicit
+                        mkPat :: Internal.Name -> Internal.PatternArg
+                        mkPat p = Internal.mkConstructorVarPattern Explicit p []
+                        branchNEq = Internal.mkCaseBranch pv (Internal.toExpression v)
+                    branchEq <- Internal.mkCaseBranch (mkPat (bs ^. ordBuiltinEq)) <$> lexgo vs
+                    let branches = branchEq :| [branchNEq]
+                    return (Internal.mkCase (cmp isRec x x') branches)
 
 derivingGetConstrs ::
   (Members '[Error ScoperError, State LocalTable, Reader S.InfoTable, Reader Internal.InfoTable] r) =>
@@ -710,9 +729,10 @@ deriveRecursiveBinaryFunction ::
   Text ->
   Internal.Name ->
   DerivingArgs ->
-  ( ( Internal.ConstructorInfo ->
-      [(Internal.ApplicationArg, Internal.ApplicationArg)] ->
-      [Internal.Expression]
+  ( ( Bool -> -- isSelfRecursive
+      Internal.ApplicationArg ->
+      Internal.ApplicationArg ->
+      Internal.Expression
     ) ->
     Sem r Internal.Expression
   ) ->
@@ -724,20 +744,7 @@ deriveRecursiveBinaryFunction label nonSelfRec DerivingArgs {..} mkLamDef = do
   let rfun isRec
         | isRec = recDefName
         | otherwise = nonSelfRec
-      mkRecCall cinfo recArgs =
-        let selfRecArgs :: [Bool]
-            selfRecArgs =
-              let argTypes =
-                    cinfo
-                      ^.. Internal.constructorInfoType
-                        . to Internal.constructorArgs
-                        . each
-                        . Internal.paramType
-               in map (== ret) argTypes
-         in [ Internal.foldApplication (Internal.toExpression (rfun isRec)) [arg1, arg2]
-              | ((arg1, arg2), isRec) <- zipExact recArgs selfRecArgs
-            ]
-
+      mkRecCall isRec arg1 arg2 = Internal.foldApplication (Internal.toExpression (rfun isRec)) [arg1, arg2]
   lamBody <- mkLamDef mkRecCall
   lamTy <- Internal.ExpressionHole <$> Internal.freshHole (getLoc _derivingInstanceName)
   let lamDef =
@@ -753,13 +760,6 @@ deriveRecursiveBinaryFunction label nonSelfRec DerivingArgs {..} mkLamDef = do
             _funDefBuiltin = Nothing
           }
   return (recDefName, Internal.LetMutualBlock (Internal.MutualBlockLet (pure lamDef)))
-  where
-    ret :: Internal.Expression
-    ret = Internal.foldApplication (Internal.toExpression eqName) args
-
-    eqName :: Internal.InductiveName
-    args :: [Internal.ApplicationArg]
-    (eqName, args) = _derivingReturnType
 
 deriveEq ::
   forall r.
@@ -827,12 +827,13 @@ deriveEq der@DerivingArgs {..} = do
 
     eqLambda ::
       EqBuiltins ->
-      ( Internal.ConstructorInfo ->
-        [(Internal.ApplicationArg, Internal.ApplicationArg)] ->
-        [Internal.Expression]
+      ( Bool ->
+        Internal.ApplicationArg ->
+        Internal.ApplicationArg ->
+        Internal.Expression
       ) ->
       Sem r Internal.Expression
-    eqLambda bs recCalls = do
+    eqLambda bs recCall = do
       constrs <- derivingGetConstrs ret args
       case nonEmpty constrs of
         Nothing -> return (Internal.toExpression (bs ^. eqBuiltinTrue))
@@ -875,12 +876,23 @@ deriveEq der@DerivingArgs {..} = do
               }
           where
             allEq :: (Internal.IsExpression expr) => [(expr, expr)] -> Internal.Expression
-            allEq k = case nonEmpty (recCalls cinfo kargs) of
-              Nothing -> Internal.toExpression (bs ^. eqBuiltinTrue)
-              Just l -> mkAnds l
+            allEq k =
+              let rargs = [recCall r a b | ((a, b), r) <- zipExact kargs selfRecArgs]
+               in case nonEmpty rargs of
+                    Nothing -> Internal.toExpression (bs ^. eqBuiltinTrue)
+                    Just l -> mkAnds l
               where
                 kargs :: [(Internal.ApplicationArg, Internal.ApplicationArg)]
-                kargs = map (over both (Internal.explicitApplicationArg . Internal.toExpression)) k
+                kargs = map (over both Internal.explicitApplicationArg) k
+
+                selfRecArgs :: [Bool]
+                selfRecArgs =
+                  cinfo
+                    ^.. Internal.constructorInfoType
+                      . to Internal.constructorArgs
+                      . each
+                      . Internal.paramType
+                      . to (== ret)
 
             mkAnds :: (Internal.IsExpression expr) => NonEmpty expr -> Internal.Expression
             mkAnds = foldl1 mkAnd . fmap Internal.toExpression

From 9fea5f8bc2714f88c02b4dd58258600a88e54234 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 27 Nov 2024 18:07:21 +0100
Subject: [PATCH 5/7] debug

---
 .../Internal/Translation/FromConcrete.hs      | 55 ++++++++++++-------
 tests/Compilation/positive/test087.juvix      | 11 +++-
 2 files changed, 44 insertions(+), 22 deletions(-)

diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index 36ccfe6075..a224f20bee 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -28,7 +28,7 @@ import Juvix.Compiler.Internal.Data.NameDependencyInfo qualified as Internal
 import Juvix.Compiler.Internal.Extra (mkLetClauses)
 import Juvix.Compiler.Internal.Extra qualified as Internal
 import Juvix.Compiler.Internal.Extra.DependencyBuilder
-import Juvix.Compiler.Internal.Language (varFromWildcard)
+import Juvix.Compiler.Internal.Pretty qualified as I
 import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context
 import Juvix.Compiler.Internal.Translation.FromConcrete.NamedArguments
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
@@ -578,7 +578,7 @@ deriveOrd ::
   DerivingArgs ->
   Sem r Internal.FunctionDef
 deriveOrd der@DerivingArgs {..} = do
-  arg <- derivingGetConstrs ret args
+  (constrs, subjectTy) <- derivingGetConstrs fullret args
   argsInfo <- goArgsInfo _derivingInstanceName
   let loc = getLoc ordName
   mkOrd <- getBuiltin loc BuiltinMkOrd
@@ -592,14 +592,14 @@ deriveOrd der@DerivingArgs {..} = do
             _ordBuiltinGt = bgt,
             _ordBuiltinEq = beq
           }
-  (recName, mutblock) <- deriveRecursiveBinaryFunction "ord" bcmp der (genOrdCompare (getLoc _derivingInstanceName) bs arg)
+  (recName, mutblock) <- deriveRecursiveBinaryFunction "ord" bcmp der (genOrdCompare (getLoc _derivingInstanceName) bs subjectTy constrs)
   let body =
         Internal.ExpressionLet
           Internal.Let
             { _letClauses = pure mutblock,
               _letExpression = mkOrd Internal.@@ recName
             }
-      ty = Internal.foldFunType _derivingParameters ret
+      ty = Internal.foldFunType _derivingParameters fullret
   pragmas' <- goPragmas _derivingPragmas
   return
     Internal.FunctionDef
@@ -614,8 +614,8 @@ deriveOrd der@DerivingArgs {..} = do
         _funDefBuiltin = Nothing
       }
   where
-    ret :: Internal.Expression
-    ret = Internal.foldApplication (Internal.toExpression ordName) args
+    fullret :: Internal.Expression
+    fullret = Internal.foldApplication (Internal.toExpression ordName) args
 
     ordName :: Internal.InductiveName
     args :: [Internal.ApplicationArg]
@@ -626,10 +626,11 @@ deriveOrd der@DerivingArgs {..} = do
       (Members '[NameIdGen] r') =>
       Interval ->
       OrdBuiltins ->
+      Internal.Expression ->
       [ConstructorInfo] ->
       (Bool -> Internal.ApplicationArg -> Internal.ApplicationArg -> Internal.Expression) ->
       Sem r' Internal.Expression
-    genOrdCompare loc bs cs recCmp = do
+    genOrdCompare loc bs subjectTy cs recCmp = do
       res <-
         fmap nonEmpty
           . execOutputList
@@ -658,14 +659,24 @@ deriveOrd der@DerivingArgs {..} = do
           let mkPat = Internal.genConstructorPattern loc Explicit c
           (p1, v1) <- mkPat
           (p2, v2) <- mkPat
-          let selfRecArgs :: [Bool]
-              selfRecArgs =
+          let tmp =
                 c
                   ^.. Internal.constructorInfoType
                     . to Internal.constructorArgs
                     . each
                     . Internal.paramType
-                    . to (== ret)
+
+          let selfRecArgs :: [Bool]
+              selfRecArgs =
+                trace
+                  ("fullret " <> I.ppTrace fullret <> "\nargs = " <> I.ppTrace ((^. Internal.appArg) <$> args))
+                  tmp
+                  ^.. each
+                    . to (== subjectTy)
+          traceM ("cargs = " <> I.ppTrace tmp)
+          traceM ("selfrecargs = " <> prettyText selfRecArgs)
+          traceM ("subjectTy = " <> I.ppTrace subjectTy)
+          traceM "\n\n"
           lord <- lexOrder (zip3Exact selfRecArgs v1 v2)
           let sameConstr =
                 Internal.LambdaClause
@@ -718,11 +729,12 @@ derivingGetConstrs ::
   (Members '[Error ScoperError, State LocalTable, Reader S.InfoTable, Reader Internal.InfoTable] r) =>
   Internal.Expression ->
   [Internal.ApplicationArg] ->
-  Sem r [Internal.ConstructorInfo]
+  Sem r ([Internal.ConstructorInfo], Internal.Expression)
 derivingGetConstrs retTy args = runFailDefaultM (throwDerivingWrongForm retTy) $ do
   [Internal.ApplicationArg Explicit a] <- return args
   Internal.ExpressionIden (Internal.IdenInductive ind) <- return (fst (Internal.unfoldExpressionApp a))
-  getDefinedInductiveConstructors ind
+  cs <- getDefinedInductiveConstructors ind
+  return (cs, a)
 
 deriveRecursiveBinaryFunction ::
   (Members '[NameIdGen] r) =>
@@ -788,7 +800,7 @@ deriveEq der@DerivingArgs {..} = do
             { _letClauses = pure mutblock,
               _letExpression = mkEq Internal.@@ recDefName
             }
-      ty = Internal.foldFunType _derivingParameters ret
+      ty = Internal.foldFunType _derivingParameters fullret
   pragmas' <- goPragmas _derivingPragmas
   return
     Internal.FunctionDef
@@ -803,8 +815,8 @@ deriveEq der@DerivingArgs {..} = do
         _funDefBuiltin = Nothing
       }
   where
-    ret :: Internal.Expression
-    ret = Internal.foldApplication (Internal.toExpression eqName) args
+    fullret :: Internal.Expression
+    fullret = Internal.foldApplication (Internal.toExpression eqName) args
 
     eqName :: Internal.InductiveName
     args :: [Internal.ApplicationArg]
@@ -834,11 +846,11 @@ deriveEq der@DerivingArgs {..} = do
       ) ->
       Sem r Internal.Expression
     eqLambda bs recCall = do
-      constrs <- derivingGetConstrs ret args
+      (constrs, subjectTy) <- derivingGetConstrs fullret args
       case nonEmpty constrs of
         Nothing -> return (Internal.toExpression (bs ^. eqBuiltinTrue))
         Just cs -> do
-          cl' <- mapM lambdaClause cs
+          cl' <- mapM (lambdaClause subjectTy) cs
           defaultCl' <-
             if
                 | notNull (NonEmpty.tail cs) -> Just <$> defaultLambdaClause
@@ -862,9 +874,10 @@ deriveEq der@DerivingArgs {..} = do
               }
 
         lambdaClause ::
+          Internal.Expression ->
           Internal.ConstructorInfo ->
           Sem r Internal.LambdaClause
-        lambdaClause cinfo = do
+        lambdaClause subjectTy cinfo = do
           let loc = getLoc _derivingInstanceName
               mkpat = Internal.genConstructorPattern loc Explicit cinfo
           (p1, v1) <- mkpat
@@ -892,7 +905,7 @@ deriveEq der@DerivingArgs {..} = do
                       . to Internal.constructorArgs
                       . each
                       . Internal.paramType
-                      . to (== ret)
+                      . to (== subjectTy)
 
             mkAnds :: (Internal.IsExpression expr) => NonEmpty expr -> Internal.Expression
             mkAnds = foldl1 mkAnd . fmap Internal.toExpression
@@ -962,7 +975,7 @@ argToPattern arg@SigArg {..} = do
       _patternArgName :: Maybe Internal.Name = Nothing
       noName = goWildcard (Wildcard (getLoc arg))
       goWildcard w = do
-        _patternArgPattern <- Internal.PatternVariable <$> varFromWildcard w
+        _patternArgPattern <- Internal.PatternVariable <$> Internal.varFromWildcard w
         return Internal.PatternArg {..}
       mk :: Concrete.Argument 'Scoped -> Sem r Internal.PatternArg
       mk = \case
@@ -1972,7 +1985,7 @@ goPattern p = case p of
   PatternApplication a -> Internal.PatternConstructorApp <$> goPatternApplication a
   PatternInfixApplication a -> Internal.PatternConstructorApp <$> goInfixPatternApplication a
   PatternPostfixApplication a -> Internal.PatternConstructorApp <$> goPostfixPatternApplication a
-  PatternWildcard i -> Internal.PatternVariable <$> varFromWildcard i
+  PatternWildcard i -> Internal.PatternVariable <$> Internal.varFromWildcard i
   PatternRecord i -> goRecordPattern i
   PatternEmpty {} -> error "unsupported empty pattern"
 
diff --git a/tests/Compilation/positive/test087.juvix b/tests/Compilation/positive/test087.juvix
index 0e996b6487..4f3e9347d8 100644
--- a/tests/Compilation/positive/test087.juvix
+++ b/tests/Compilation/positive/test087.juvix
@@ -18,9 +18,18 @@ type T :=
 deriving instance
 ordT : Ord T;
 
+type Tree (A : Type) :=
+  | leaf
+  | node (Tree A) A (Tree A);
+
+deriving instance
+ordTree {A} {{Ord A}} : Ord (Tree A);
+
 main : IO :=
   printLn (compare One One)
     >>> printLn (compare One Two)
     >>> printLn (compare Two One)
     >>> printLn (compare (One, One) (One, Three))
-    >>> printLn (compare (Four, Four) (Four, Three));
+    >>> printLn (compare (Four, Four) (Four, Three))
+    >>> printLn
+      (compare (node leaf Four leaf) (node (node leaf One leaf) Two leaf));

From f5e92a72f3ba147567333ec60afb8be49c941587 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 27 Nov 2024 22:02:08 +0100
Subject: [PATCH 6/7] store self recursive args in constructor info

---
 src/Juvix/Compiler/Internal/Data/InfoTable.hs | 12 +++-
 .../Internal/Translation/FromConcrete.hs      | 58 +++++--------------
 .../Compiler/Store/Internal/Data/InfoTable.hs |  1 +
 3 files changed, 28 insertions(+), 43 deletions(-)

diff --git a/src/Juvix/Compiler/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Internal/Data/InfoTable.hs
index e2c936e915..48d818d06b 100644
--- a/src/Juvix/Compiler/Internal/Data/InfoTable.hs
+++ b/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)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index a224f20bee..e812525deb 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -28,7 +28,6 @@ import Juvix.Compiler.Internal.Data.NameDependencyInfo qualified as Internal
 import Juvix.Compiler.Internal.Extra (mkLetClauses)
 import Juvix.Compiler.Internal.Extra qualified as Internal
 import Juvix.Compiler.Internal.Extra.DependencyBuilder
-import Juvix.Compiler.Internal.Pretty qualified as I
 import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context
 import Juvix.Compiler.Internal.Translation.FromConcrete.NamedArguments
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
@@ -578,7 +577,7 @@ deriveOrd ::
   DerivingArgs ->
   Sem r Internal.FunctionDef
 deriveOrd der@DerivingArgs {..} = do
-  (constrs, subjectTy) <- derivingGetConstrs fullret args
+  constrs <- derivingGetConstrs ret args
   argsInfo <- goArgsInfo _derivingInstanceName
   let loc = getLoc ordName
   mkOrd <- getBuiltin loc BuiltinMkOrd
@@ -592,14 +591,14 @@ deriveOrd der@DerivingArgs {..} = do
             _ordBuiltinGt = bgt,
             _ordBuiltinEq = beq
           }
-  (recName, mutblock) <- deriveRecursiveBinaryFunction "ord" bcmp der (genOrdCompare (getLoc _derivingInstanceName) bs subjectTy constrs)
+  (recName, mutblock) <- deriveRecursiveBinaryFunction "ord" bcmp der (genOrdCompare (getLoc _derivingInstanceName) bs constrs)
   let body =
         Internal.ExpressionLet
           Internal.Let
             { _letClauses = pure mutblock,
               _letExpression = mkOrd Internal.@@ recName
             }
-      ty = Internal.foldFunType _derivingParameters fullret
+      ty = Internal.foldFunType _derivingParameters ret
   pragmas' <- goPragmas _derivingPragmas
   return
     Internal.FunctionDef
@@ -614,8 +613,8 @@ deriveOrd der@DerivingArgs {..} = do
         _funDefBuiltin = Nothing
       }
   where
-    fullret :: Internal.Expression
-    fullret = Internal.foldApplication (Internal.toExpression ordName) args
+    ret :: Internal.Expression
+    ret = Internal.foldApplication (Internal.toExpression ordName) args
 
     ordName :: Internal.InductiveName
     args :: [Internal.ApplicationArg]
@@ -626,11 +625,10 @@ deriveOrd der@DerivingArgs {..} = do
       (Members '[NameIdGen] r') =>
       Interval ->
       OrdBuiltins ->
-      Internal.Expression ->
       [ConstructorInfo] ->
       (Bool -> Internal.ApplicationArg -> Internal.ApplicationArg -> Internal.Expression) ->
       Sem r' Internal.Expression
-    genOrdCompare loc bs subjectTy cs recCmp = do
+    genOrdCompare loc bs cs recCmp = do
       res <-
         fmap nonEmpty
           . execOutputList
@@ -659,24 +657,8 @@ deriveOrd der@DerivingArgs {..} = do
           let mkPat = Internal.genConstructorPattern loc Explicit c
           (p1, v1) <- mkPat
           (p2, v2) <- mkPat
-          let tmp =
-                c
-                  ^.. Internal.constructorInfoType
-                    . to Internal.constructorArgs
-                    . each
-                    . Internal.paramType
-
           let selfRecArgs :: [Bool]
-              selfRecArgs =
-                trace
-                  ("fullret " <> I.ppTrace fullret <> "\nargs = " <> I.ppTrace ((^. Internal.appArg) <$> args))
-                  tmp
-                  ^.. each
-                    . to (== subjectTy)
-          traceM ("cargs = " <> I.ppTrace tmp)
-          traceM ("selfrecargs = " <> prettyText selfRecArgs)
-          traceM ("subjectTy = " <> I.ppTrace subjectTy)
-          traceM "\n\n"
+              selfRecArgs = c ^. constructorSelfRecursiveArgs
           lord <- lexOrder (zip3Exact selfRecArgs v1 v2)
           let sameConstr =
                 Internal.LambdaClause
@@ -729,12 +711,11 @@ derivingGetConstrs ::
   (Members '[Error ScoperError, State LocalTable, Reader S.InfoTable, Reader Internal.InfoTable] r) =>
   Internal.Expression ->
   [Internal.ApplicationArg] ->
-  Sem r ([Internal.ConstructorInfo], Internal.Expression)
+  Sem r [Internal.ConstructorInfo]
 derivingGetConstrs retTy args = runFailDefaultM (throwDerivingWrongForm retTy) $ do
   [Internal.ApplicationArg Explicit a] <- return args
   Internal.ExpressionIden (Internal.IdenInductive ind) <- return (fst (Internal.unfoldExpressionApp a))
-  cs <- getDefinedInductiveConstructors ind
-  return (cs, a)
+  getDefinedInductiveConstructors ind
 
 deriveRecursiveBinaryFunction ::
   (Members '[NameIdGen] r) =>
@@ -800,7 +781,7 @@ deriveEq der@DerivingArgs {..} = do
             { _letClauses = pure mutblock,
               _letExpression = mkEq Internal.@@ recDefName
             }
-      ty = Internal.foldFunType _derivingParameters fullret
+      ty = Internal.foldFunType _derivingParameters ret
   pragmas' <- goPragmas _derivingPragmas
   return
     Internal.FunctionDef
@@ -815,8 +796,8 @@ deriveEq der@DerivingArgs {..} = do
         _funDefBuiltin = Nothing
       }
   where
-    fullret :: Internal.Expression
-    fullret = Internal.foldApplication (Internal.toExpression eqName) args
+    ret :: Internal.Expression
+    ret = Internal.foldApplication (Internal.toExpression eqName) args
 
     eqName :: Internal.InductiveName
     args :: [Internal.ApplicationArg]
@@ -846,11 +827,11 @@ deriveEq der@DerivingArgs {..} = do
       ) ->
       Sem r Internal.Expression
     eqLambda bs recCall = do
-      (constrs, subjectTy) <- derivingGetConstrs fullret args
+      constrs <- derivingGetConstrs ret args
       case nonEmpty constrs of
         Nothing -> return (Internal.toExpression (bs ^. eqBuiltinTrue))
         Just cs -> do
-          cl' <- mapM (lambdaClause subjectTy) cs
+          cl' <- mapM lambdaClause cs
           defaultCl' <-
             if
                 | notNull (NonEmpty.tail cs) -> Just <$> defaultLambdaClause
@@ -874,10 +855,9 @@ deriveEq der@DerivingArgs {..} = do
               }
 
         lambdaClause ::
-          Internal.Expression ->
           Internal.ConstructorInfo ->
           Sem r Internal.LambdaClause
-        lambdaClause subjectTy cinfo = do
+        lambdaClause cinfo = do
           let loc = getLoc _derivingInstanceName
               mkpat = Internal.genConstructorPattern loc Explicit cinfo
           (p1, v1) <- mkpat
@@ -899,13 +879,7 @@ deriveEq der@DerivingArgs {..} = do
                 kargs = map (over both Internal.explicitApplicationArg) k
 
                 selfRecArgs :: [Bool]
-                selfRecArgs =
-                  cinfo
-                    ^.. Internal.constructorInfoType
-                      . to Internal.constructorArgs
-                      . each
-                      . Internal.paramType
-                      . to (== subjectTy)
+                selfRecArgs = cinfo ^. Internal.constructorSelfRecursiveArgs
 
             mkAnds :: (Internal.IsExpression expr) => NonEmpty expr -> Internal.Expression
             mkAnds = foldl1 mkAnd . fmap Internal.toExpression
diff --git a/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs b/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs
index 71c71145a9..47ed0b90c7 100644
--- a/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs
+++ b/src/Juvix/Compiler/Store/Internal/Data/InfoTable.hs
@@ -9,6 +9,7 @@ data ConstructorInfo = ConstructorInfo
     _constructorInfoType :: Expression,
     _constructorInfoInductive :: InductiveName,
     _constructorInfoName :: ConstructorName,
+    _constructorSelfRecursiveArgs :: [Bool],
     _constructorInfoBuiltin :: Maybe BuiltinConstructor,
     _constructorInfoTrait :: Bool,
     _constructorInfoRecord :: Bool

From 1cdcb02fb4b6fb132e8ff94b39850be72ea9515e Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Thu, 28 Nov 2024 09:38:11 +0100
Subject: [PATCH 7/7] extend test

---
 tests/Compilation/positive/out/test087.out |  3 +++
 tests/Compilation/positive/test087.juvix   | 10 +++++++++-
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/tests/Compilation/positive/out/test087.out b/tests/Compilation/positive/out/test087.out
index df0c967608..b686bb0401 100644
--- a/tests/Compilation/positive/out/test087.out
+++ b/tests/Compilation/positive/out/test087.out
@@ -3,3 +3,6 @@ LessThan
 GreaterThan
 LessThan
 GreaterThan
+LessThan
+GreaterThan
+Equal
diff --git a/tests/Compilation/positive/test087.juvix b/tests/Compilation/positive/test087.juvix
index 4f3e9347d8..2252dce3a6 100644
--- a/tests/Compilation/positive/test087.juvix
+++ b/tests/Compilation/positive/test087.juvix
@@ -32,4 +32,12 @@ main : IO :=
     >>> printLn (compare (One, One) (One, Three))
     >>> printLn (compare (Four, Four) (Four, Three))
     >>> printLn
-      (compare (node leaf Four leaf) (node (node leaf One leaf) Two leaf));
+      (compare (node leaf Four leaf) (node (node leaf One leaf) Two leaf))
+    >>> printLn
+      (compare
+        (node (node leaf One leaf) Four leaf)
+        (node (node leaf One leaf) Two leaf))
+    >>> printLn
+      (compare
+        (node (node leaf One leaf) Four leaf)
+        (node (node leaf One leaf) Four leaf));