Numeric, ordering and equality traits (#2433)

* Adapts to https://github.com/anoma/juvix-stdlib/pull/86
* Adds a pass in `toEvalTransformations` to automatically inline all
record projection functions, regardless of the optimization level. This
is necessary to ensure that arithmetic operations and comparisons on
`Nat` or `Int` are always represented directly with the corresponding
built-in Core functions. This is generally highly desirable and required
for the Geb target.
* Adds the `inline: always` pragma which indicates that a function
should always be inlined during the mandatory inlining phase, regardless
of optimization level.

examples/demo/Demo.juvix

@@ -2,9 +2,6 @@ module Demo;
 
 -- standard library prelude
 import Stdlib.Prelude open;
--- for comparisons on natural numbers
-import Stdlib.Data.Nat.Ord open;
--- for Ordering
 
 even : Nat → Bool
   | zero := true
@@ -35,13 +32,13 @@ preorder : {A : Type} → Tree A → List A
   | (node x l r) := x :: nil ++ preorder l ++ preorder r;
 
 terminating
-sort : {A : Type} → (A → A → Ordering) → List A → List A
+sort {A} {{Ord A}} : List A → List A
-  | _ nil := nil
+  | nil := nil
-  | _ xs@(_ :: nil) := xs
+  | xs@(_ :: nil) := xs
-  | {A} cmp xs :=
+  | xs :=
     uncurry
-      (merge {{mkOrd cmp}})
+      merge
-      (both (sort cmp) (splitAt (div (length xs) 2) xs));
+      (both sort (splitAt (div (length xs) 2) xs));
 
 printNatListLn : List Nat → IO
   | nil := printStringLn "nil"
@@ -51,6 +48,6 @@ printNatListLn : List Nat → IO
 main : IO :=
   printStringLn "Hello!"
     >> printNatListLn (preorder (mirror tree))
-    >> printNatListLn (sort compare (preorder (mirror tree)))
+    >> printNatListLn (sort (preorder (mirror tree)))
     >> printNatLn (log2 3)
     >> printNatLn (log2 130);

examples/midsquare/MidSquareHash.juvix

@@ -5,7 +5,6 @@
 module MidSquareHash;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 --- `pow N` is 2 ^ N
 pow : Nat -> Nat

examples/midsquare/MidSquareHashUnrolled.juvix

@@ -6,7 +6,6 @@
 module MidSquareHashUnrolled;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 --- `powN` is 2 ^ N
 pow0 : Nat := 1;

examples/milestone/Bank/Bank.juvix

@@ -6,8 +6,6 @@ module Bank;
 import Stdlib.Prelude open;
 import Stdlib.Debug.Fail open;
 
-import Stdlib.Data.Nat.Ord open;
-
 import Stdlib.Data.Nat as Nat;
 
 Address : Type := Nat;

examples/milestone/Collatz/Collatz.juvix

@@ -1,7 +1,6 @@
 module Collatz;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 collatzNext (n : Nat) : Nat :=
   if (mod n 2 == 0) (div n 2) (3 * n + 1);

examples/milestone/TicTacToe/CLI/TicTacToe.juvix

@@ -5,7 +5,6 @@
 --- The module Logic.Game contains the game logic.
 module CLI.TicTacToe;
 
-import Stdlib.Data.Nat.Ord open;
 import Stdlib.Prelude open;
 import Logic.Game open;
 

examples/milestone/TicTacToe/Logic/Extra.juvix

@@ -1,7 +1,6 @@
 --- Some generic helper definitions.
 module Logic.Extra;
 
-import Stdlib.Data.Nat.Ord open;
 import Stdlib.Prelude open;
 
 --- Concatenates a list of strings

examples/milestone/TicTacToe/Logic/Game.juvix

@@ -4,7 +4,6 @@
 --- diagonal row is the winner. It is a solved game, with a forced draw assuming best play from both players.
 module Logic.Game;
 
-import Stdlib.Data.Nat.Ord open;
 import Stdlib.Prelude open;
 import Logic.Extra open public;
 import Logic.Board open public;

examples/milestone/TicTacToe/Logic/Square.juvix

@@ -2,7 +2,6 @@ module Logic.Square;
 
 import Stdlib.Prelude open;
 import Logic.Symbol open;
-import Stdlib.Data.Nat.Ord open;
 import Logic.Extra open;
 
 --- A square is each of the holes in a board
@@ -24,9 +23,5 @@ showSquare : Square → String
   | (occupied s) := " " ++str showSymbol s ++str " ";
 
 replace (player : Symbol) (k : Nat) : Square → Square
-  | (empty n) :=
+  | (empty n) := if (n == k) (occupied player) (empty n)
-    if
-      (n Stdlib.Data.Nat.Ord.== k)
-      (occupied player)
-      (empty n)
   | s := s;

examples/milestone/Tutorial/Tutorial.juvix

@@ -5,7 +5,5 @@ module Tutorial;
 
 -- import the standard library prelude and bring it into scope
 import Stdlib.Prelude open;
--- bring comparison operators on Nat into scope
-import Stdlib.Data.Nat.Ord open;
 
 main : IO := printStringLn "Hello world!";

juvix-stdlib

@@ -1 +1 @@
-Subproject commit adf58a7180b361a022fb53c22ad9e5274ebf6f66
+Subproject commit 9a091c5453594ac66b3b25cde0c11a54a255a9c9

src/Juvix/Compiler/Backend/Geb/Translation/FromCore.hs

@@ -58,7 +58,7 @@ fromCore :: Core.InfoTable -> (Morphism, Object)
 fromCore tab = case tab ^. Core.infoMain of
   Just sym ->
     let node = Core.lookupIdentifierNode tab sym
-        syms = reverse $ filter (/= sym) $ Core.createIdentDependencyInfo tab ^. Core.depInfoTopSort
+        syms = reverse $ filter (/= sym) $ Core.createCallGraph tab ^. Core.depInfoTopSort
         idents = map (Core.lookupIdentifierInfo tab) syms
         morph = run . runReader emptyEnv $ goIdents node idents
         obj = convertType $ Info.getNodeType node

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

@@ -1,5 +1,6 @@
 module Juvix.Compiler.Core.Data.IdentDependencyInfo where
 
+import Data.HashMap.Strict qualified as HashMap
 import Data.HashSet qualified as HashSet
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Extra.Utils
@@ -9,8 +10,8 @@ import Juvix.Compiler.Core.Language
 type IdentDependencyInfo = DependencyInfo Symbol
 
 -- | Compute the call graph
-createIdentDependencyInfo :: InfoTable -> IdentDependencyInfo
+createCallGraph :: InfoTable -> IdentDependencyInfo
-createIdentDependencyInfo tab = createDependencyInfo graph startVertices
+createCallGraph tab = createDependencyInfo graph startVertices
   where
     graph :: HashMap Symbol (HashSet Symbol)
     graph =
@@ -27,5 +28,28 @@ createIdentDependencyInfo tab = createDependencyInfo graph startVertices
     syms :: [Symbol]
     syms = maybe [] singleton (tab ^. infoMain)
 
+createSymbolDependencyInfo :: InfoTable -> IdentDependencyInfo
+createSymbolDependencyInfo tab = createDependencyInfo graph startVertices
+  where
+    graph :: HashMap Symbol (HashSet Symbol)
+    graph =
+      fmap
+        ( \IdentifierInfo {..} ->
+            getSymbols tab (lookupIdentifierNode tab _identifierSymbol)
+        )
+        (tab ^. infoIdentifiers)
+        <> foldr
+          ( \ConstructorInfo {..} ->
+              HashMap.insert _constructorInductive (getSymbols tab _constructorType)
+          )
+          mempty
+          (tab ^. infoConstructors)
+
+    startVertices :: HashSet Symbol
+    startVertices = HashSet.fromList syms
+
+    syms :: [Symbol]
+    syms = maybe [] singleton (tab ^. infoMain)
+
 recursiveIdents :: InfoTable -> HashSet Symbol
-recursiveIdents = nodesOnCycles . createIdentDependencyInfo
+recursiveIdents = nodesOnCycles . createCallGraph

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

@@ -209,20 +209,33 @@ filterByFile f t =
     matchesLocation :: Maybe Location -> Bool
     matchesLocation l = l ^? _Just . intervalFile == Just f
 
--- | Prunes the orphaned entries of identMap and indentContext, i.e., ones that
+-- | Prunes the orphaned entries of identMap, indentContext and
--- have no corresponding entries in infoIdentifiers or infoInductives
+-- infoConstructors, i.e., ones that have no corresponding entries in
+-- infoIdentifiers or infoInductives
 pruneInfoTable :: InfoTable -> InfoTable
 pruneInfoTable tab =
-  over
+  pruneIdentMap
-    identMap
+    $ over
-    ( HashMap.filter
+      infoConstructors
-        ( \case
+      ( HashMap.filter
-            IdentFun s -> HashMap.member s (tab ^. infoIdentifiers)
+          ( \ConstructorInfo {..} ->
-            IdentInd s -> HashMap.member s (tab ^. infoInductives)
+              HashMap.member _constructorInductive (tab ^. infoInductives)
-            IdentConstr tag -> HashMap.member tag (tab ^. infoConstructors)
+          )
-        )
+      )
-    )
     $ over
       identContext
       (HashMap.filterWithKey (\s _ -> HashMap.member s (tab ^. infoIdentifiers)))
       tab
+  where
+    pruneIdentMap :: InfoTable -> InfoTable
+    pruneIdentMap tab' =
+      over
+        identMap
+        ( HashMap.filter
+            ( \case
+                IdentFun s -> HashMap.member s (tab' ^. infoIdentifiers)
+                IdentInd s -> HashMap.member s (tab' ^. infoInductives)
+                IdentConstr tag -> HashMap.member tag (tab' ^. infoConstructors)
+            )
+        )
+        tab'

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

@@ -26,6 +26,7 @@ data TransformationId
   | LambdaFolding
   | LetHoisting
   | Inlining
+  | MandatoryInlining
   | FoldTypeSynonyms
   | CaseCallLifting
   | SimplifyIfs
@@ -75,7 +76,7 @@ toNormalizeTransformations :: [TransformationId]
 toNormalizeTransformations = toEvalTransformations ++ [LetRecLifting, LetFolding, UnrollRecursion]
 
 toVampIRTransformations :: [TransformationId]
-toVampIRTransformations = toEvalTransformations ++ [CheckVampIR, LetRecLifting, OptPhaseVampIR, UnrollRecursion, Normalize, LetHoisting]
+toVampIRTransformations = toEvalTransformations ++ [FilterUnreachable, CheckVampIR, LetRecLifting, OptPhaseVampIR, UnrollRecursion, Normalize, LetHoisting]
 
 toStrippedTransformations :: [TransformationId]
 toStrippedTransformations =

src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs

@@ -86,6 +86,7 @@ transformationText = \case
   LambdaFolding -> strLambdaFolding
   LetHoisting -> strLetHoisting
   Inlining -> strInlining
+  MandatoryInlining -> strMandatoryInlining
   FoldTypeSynonyms -> strFoldTypeSynonyms
   CaseCallLifting -> strCaseCallLifting
   SimplifyIfs -> strSimplifyIfs
@@ -191,6 +192,9 @@ strLambdaFolding = "lambda-folding"
 strInlining :: Text
 strInlining = "inlining"
 
+strMandatoryInlining :: Text
+strMandatoryInlining = "mandatory-inlining"
+
 strFoldTypeSynonyms :: Text
 strFoldTypeSynonyms = "fold-type-synonyms"
 

src/Juvix/Compiler/Core/Evaluator.hs

@@ -89,7 +89,7 @@ geval opts herr ctx env0 = eval' env0
           Closure env' (NLam (Lambda i' bi b)) ->
             let !v = eval' env r in evalBody i' bi env' v b
           lv
-            | opts ^. evalOptionsNormalize ->
+            | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
                 let !v = eval' env r in goNormApp i lv v
             | otherwise ->
                 evalError "invalid application" (mkApp i lv (substEnv env r))
@@ -106,7 +106,7 @@ geval opts herr ctx env0 = eval' env0
           NCtr (Constr _ tag args) ->
             branch n env args tag def bs
           v'
-            | opts ^. evalOptionsNormalize ->
+            | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
                 goNormCase env i sym v' bs def
             | otherwise ->
                 evalError "matching on non-data" (substEnv env (mkCase i sym v' bs def))
@@ -214,7 +214,7 @@ geval opts herr ctx env0 = eval' env0
                 (Just v1, Just v2) ->
                   toNode (v1 `op` v2)
                 _
-                  | opts ^. evalOptionsNormalize ->
+                  | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
                       mkBuiltinApp' opcode [vl, vr]
                   | otherwise ->
                       evalError "wrong operand type" n

src/Juvix/Compiler/Core/Extra/Utils.hs

@@ -144,6 +144,9 @@ nodeIdents f = ufoldA reassemble go
       NIdt i -> NIdt <$> f i
       n -> pure n
 
+getInductives :: Node -> HashSet Symbol
+getInductives n = HashSet.fromList (n ^.. nodeInductives)
+
 nodeInductives :: Traversal' Node Symbol
 nodeInductives f = ufoldA reassemble go
   where
@@ -151,6 +154,19 @@ nodeInductives f = ufoldA reassemble go
       NTyp ty -> NTyp <$> traverseOf typeConstrSymbol f ty
       n -> pure n
 
+getSymbols :: InfoTable -> Node -> HashSet Symbol
+getSymbols tab = gather go mempty
+  where
+    go :: HashSet Symbol -> Node -> HashSet Symbol
+    go acc = \case
+      NTyp TypeConstr {..} -> HashSet.insert _typeConstrSymbol acc
+      NIdt Ident {..} -> HashSet.insert _identSymbol acc
+      NCase Case {..} -> HashSet.insert _caseInductive acc
+      NCtr Constr {..}
+        | Just ci <- lookupConstructorInfo' tab _constrTag ->
+            HashSet.insert (ci ^. constructorInductive) acc
+      _ -> acc
+
 -- | Prism for NRec
 _NRec :: SimpleFold Node LetRec
 _NRec f = \case

src/Juvix/Compiler/Core/Transformation.hs

@@ -35,6 +35,7 @@ import Juvix.Compiler.Core.Transformation.Optimize.FilterUnreachable (filterUnre
 import Juvix.Compiler.Core.Transformation.Optimize.Inlining
 import Juvix.Compiler.Core.Transformation.Optimize.LambdaFolding
 import Juvix.Compiler.Core.Transformation.Optimize.LetFolding
+import Juvix.Compiler.Core.Transformation.Optimize.MandatoryInlining
 import Juvix.Compiler.Core.Transformation.Optimize.Phase.Eval qualified as Phase.Eval
 import Juvix.Compiler.Core.Transformation.Optimize.Phase.Exec qualified as Phase.Exec
 import Juvix.Compiler.Core.Transformation.Optimize.Phase.Geb qualified as Phase.Geb
@@ -74,6 +75,7 @@ applyTransformations ts tbl = foldM (flip appTrans) tbl ts
       LambdaFolding -> return . lambdaFolding
       LetHoisting -> return . letHoisting
       Inlining -> inlining
+      MandatoryInlining -> return . mandatoryInlining
       FoldTypeSynonyms -> return . foldTypeSynonyms
       CaseCallLifting -> return . caseCallLifting
       SimplifyIfs -> return . simplifyIfs

src/Juvix/Compiler/Core/Transformation/LetHoisting.hs

@@ -1,4 +1,4 @@
--- Moves al let expressions at the top, just after the top lambdas. This
+-- Moves all let expressions at the top, just after the top lambdas. This
 -- transformation assumes:
 -- - There are no LetRecs, Lambdas (other than the ones at the top), nor Match.
 -- - Case nodes do not have binders.

src/Juvix/Compiler/Core/Transformation/Optimize/FilterUnreachable.hs

@@ -5,10 +5,13 @@ import Juvix.Compiler.Core.Data.IdentDependencyInfo
 import Juvix.Compiler.Core.Transformation.Base
 
 filterUnreachable :: InfoTable -> InfoTable
-filterUnreachable tab = pruneInfoTable $ over infoIdentifiers goFilter tab
+filterUnreachable tab =
+  pruneInfoTable $
+    over infoInductives goFilter $
+      over infoIdentifiers goFilter tab
   where
-    depInfo = createIdentDependencyInfo tab
+    depInfo = createSymbolDependencyInfo tab
 
-    goFilter :: HashMap Symbol IdentifierInfo -> HashMap Symbol IdentifierInfo
+    goFilter :: HashMap Symbol a -> HashMap Symbol a
-    goFilter idents =
+    goFilter =
-      HashMap.filterWithKey (\sym _ -> isReachable depInfo sym) idents
+      HashMap.filterWithKey (\sym _ -> isReachable depInfo sym)

src/Juvix/Compiler/Core/Transformation/Optimize/Inlining.hs

@@ -32,6 +32,8 @@ convertNode inlineDepth recSyms tab = dmapL go
                   Just (InlinePartiallyApplied k)
                     | length args >= k ->
                         mkApps def args
+                  Just InlineAlways ->
+                    mkApps def args
                   Just InlineNever ->
                     node
                   _
@@ -48,6 +50,17 @@ convertNode inlineDepth recSyms tab = dmapL go
                   def = lookupIdentifierNode tab _identSymbol
               _ ->
                 node
+      NIdt Ident {..} ->
+        case pi of
+          Just InlineFullyApplied | argsNum == 0 -> def
+          Just (InlinePartiallyApplied 0) -> def
+          Just InlineAlways -> def
+          _ -> node
+        where
+          ii = lookupIdentifierInfo tab _identSymbol
+          pi = ii ^. identifierPragmas . pragmasInline
+          argsNum = ii ^. identifierArgsNum
+          def = lookupIdentifierNode tab _identSymbol
       -- inline zero-argument definitions automatically if inlining would result
       -- in case reduction
       NCase cs@Case {..} -> case _caseValue of

src/Juvix/Compiler/Core/Transformation/Optimize/MandatoryInlining.hs

@@ -0,0 +1,18 @@
+module Juvix.Compiler.Core.Transformation.Optimize.MandatoryInlining where
+
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Transformation.Base
+
+convertNode :: InfoTable -> Node -> Node
+convertNode tab = dmap go
+  where
+    go :: Node -> Node
+    go node = case node of
+      NIdt Ident {..}
+        | Just InlineAlways <- lookupIdentifierInfo tab _identSymbol ^. identifierPragmas . pragmasInline ->
+            lookupIdentifierNode tab _identSymbol
+      _ ->
+        node
+
+mandatoryInlining :: InfoTable -> InfoTable
+mandatoryInlining tab = mapAllNodes (convertNode tab) tab

src/Juvix/Compiler/Core/Transformation/Optimize/Phase/Eval.hs

@@ -1,11 +1,15 @@
 module Juvix.Compiler.Core.Transformation.Optimize.Phase.Eval where
 
-import Juvix.Compiler.Core.Options
 import Juvix.Compiler.Core.Transformation.Base
+import Juvix.Compiler.Core.Transformation.Optimize.CaseFolding
 import Juvix.Compiler.Core.Transformation.Optimize.LambdaFolding
 import Juvix.Compiler.Core.Transformation.Optimize.LetFolding
+import Juvix.Compiler.Core.Transformation.Optimize.MandatoryInlining
 
-optimize :: (Member (Reader CoreOptions) r) => InfoTable -> Sem r InfoTable
+optimize :: InfoTable -> Sem r InfoTable
 optimize =
-  withOptimizationLevel 1 $
+  return
-    return . letFolding . lambdaFolding
+    . caseFolding
+    . letFolding
+    . lambdaFolding
+    . mandatoryInlining

src/Juvix/Compiler/Core/Transformation/UnrollRecursion.hs

@@ -13,7 +13,7 @@ unrollRecursion tab = do
   (mp, tab') <-
     runState @(HashMap Symbol Symbol) mempty $
       execInfoTableBuilder tab $
-        forM_ (buildSCCs (createIdentDependencyInfo tab)) goSCC
+        forM_ (buildSCCs (createCallGraph tab)) goSCC
   return $ mapIdentSymbols mp $ pruneInfoTable tab'
   where
     mapIdentSymbols :: HashMap Symbol Symbol -> InfoTable -> InfoTable

src/Juvix/Compiler/Internal/Extra.hs

@@ -93,7 +93,7 @@ genFieldProjection _funDefName info fieldIx = do
         _funDefTerminating = False,
         _funDefInstance = False,
         _funDefBuiltin = Nothing,
-        _funDefPragmas = mempty,
+        _funDefPragmas = mempty {_pragmasInline = Just InlineAlways},
         _funDefBody = body',
         _funDefType = foldFunType (inductiveArgs ++ [saturatedTy]) retTy,
         ..

src/Juvix/Data/Pragmas.hs

@@ -5,7 +5,8 @@ import Juvix.Data.Yaml
 import Juvix.Prelude.Base
 
 data PragmaInline
-  = InlineNever
+  = InlineAlways
+  | InlineNever
   | InlineFullyApplied
   | InlinePartiallyApplied {_pragmaInlineArgsNum :: Int}
   deriving stock (Show, Eq, Ord, Data, Generic)
@@ -116,7 +117,7 @@ instance FromJSON Pragmas where
         return Pragmas {..}
 
       parseInline :: Parse YamlError PragmaInline
-      parseInline = parseInlineArgsNum Aeson.<|> parseInlineBool
+      parseInline = parseInlineArgsNum Aeson.<|> parseInlineBool Aeson.<|> parseInlineAlwaysNever
         where
           parseInlineArgsNum :: Parse YamlError PragmaInline
           parseInlineArgsNum = do
@@ -128,6 +129,14 @@ instance FromJSON Pragmas where
             b <- asBool
             (if b then return InlineFullyApplied else return InlineNever)
 
+          parseInlineAlwaysNever :: Parse YamlError PragmaInline
+          parseInlineAlwaysNever = do
+            txt <- asText
+            case txt of
+              "always" -> return InlineAlways
+              "never" -> return InlineNever
+              _ -> throwCustomError ("unrecognized inline specification: " <> txt)
+
       parseUnroll :: Parse YamlError PragmaUnroll
       parseUnroll = do
         _pragmaUnrollDepth <- asIntegral
@@ -209,6 +218,7 @@ instance Monoid Pragmas where
 adjustPragmaInline :: Int -> PragmaInline -> PragmaInline
 adjustPragmaInline n = \case
   InlinePartiallyApplied k -> InlinePartiallyApplied (k + n)
+  InlineAlways -> InlineAlways
   InlineNever -> InlineNever
   InlineFullyApplied -> InlineFullyApplied
 

test/Core/Transformation/Unrolling.hs

@@ -44,5 +44,5 @@ liftTest _testEval =
 checkNoRecursion :: InfoTable -> Assertion
 checkNoRecursion tab =
   when
-    (isCyclic (createIdentDependencyInfo tab))
+    (isCyclic (createCallGraph tab))
     (assertFailure "recursion detected")

tests/Compilation/positive/test006.juvix

@@ -2,7 +2,6 @@
 module test006;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 loop : Nat := loop;

tests/Compilation/positive/test012.juvix

@@ -2,7 +2,6 @@
 module test012;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 type Tree :=
   | leaf : Tree

tests/Compilation/positive/test013.juvix

@@ -2,7 +2,6 @@
 module test013;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 f : Nat → Nat → Nat
   | x :=

tests/Compilation/positive/test015.juvix

@@ -2,7 +2,6 @@
 module test015;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 f : Nat → Nat → Nat

tests/Compilation/positive/test020.juvix

@@ -2,7 +2,6 @@
 module test020;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 -- McCarthy's 91 function
 terminating

tests/Compilation/positive/test021.juvix

@@ -2,7 +2,6 @@
 module test021;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 power' : Nat → Nat → Nat → Nat

tests/Compilation/positive/test022.juvix

@@ -2,7 +2,6 @@
 module test022;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 gen : Nat → List Nat
   | zero := nil

tests/Compilation/positive/test023.juvix

@@ -2,11 +2,10 @@
 module test023;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 f : Nat → Nat
-  
+
   | x := if (x < 1) 1 (2 * x + g (sub x 1));
 
 terminating

tests/Compilation/positive/test025.juvix

@@ -2,7 +2,6 @@
 module test025;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 gcd : Nat → Nat → Nat

tests/Compilation/positive/test028.juvix

@@ -2,7 +2,6 @@
 module test028;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 type Stream :=
   | cons : Nat → (Unit → Stream) → Stream;

tests/Compilation/positive/test032.juvix

@@ -2,7 +2,6 @@
 module test032;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 split : {A : Type} → Nat → List A → List A × List A
   | zero xs := nil, xs

tests/Compilation/positive/test034.juvix

@@ -2,7 +2,6 @@
 module test034;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 sum : Nat → Nat :=
   let

tests/Compilation/positive/test049.juvix

@@ -1,9 +1,7 @@
 -- Builtin Int
 module test049;
 
-import Stdlib.Prelude open hiding {+; *; div; mod};
+import Stdlib.Prelude open;
-import Stdlib.Data.Int.Ord open;
-import Stdlib.Data.Int open;
 
 f : Int -> Nat
   | (negSuc n) := n
@@ -23,8 +21,8 @@ main : IO :=
     >> printBoolLn (-1 == -2)
     >> printBoolLn (-1 == -1)
     >> printBoolLn (1 == 1)
-    >> printBoolLn (-1 == 1)
+    >> printBoolLn (-1 == ofNat 1)
-    >> printIntLn (-1 + 1)
+    >> printIntLn (-1 + ofNat 1)
     >> printIntLn (negNat (suc zero))
     >> printIntLn
       (let
@@ -35,9 +33,9 @@ main : IO :=
       (let
         g : Int -> Int := neg;
       in g -1)
-    >> printIntLn (-2 * 2)
+    >> printIntLn (-2 * ofNat 2)
-    >> printIntLn (div 4 -2)
+    >> printIntLn (div (ofNat 4) -2)
-    >> printIntLn (2 - 2)
+    >> printIntLn (ofNat 2 - ofNat 2)
     >> printBoolLn (nonNeg 0)
     >> printBoolLn (nonNeg -1)
     >> printIntLn (mod -5 -2)
@@ -45,5 +43,5 @@ main : IO :=
     >> printBoolLn (0 <= 0)
     >> printBoolLn (0 < 1)
     >> printBoolLn (1 <= 0)
-    >> printIntLn (mod 5 -3)
+    >> printIntLn (mod (ofNat 5) -3)
-    >> printIntLn (div 5 -3);
+    >> printIntLn (div (ofNat 5) -3);

tests/Compilation/positive/test050.juvix

@@ -1,13 +1,11 @@
 -- Pattern matching with integers
 module test050;
 
-import Stdlib.Prelude open hiding {+; *; div; mod};
+import Stdlib.Prelude open;
-import Stdlib.Data.Int.Ord open;
-import Stdlib.Data.Int open;
 
 f : Int -> Int
   | (negSuc zero) := ofNat 0
   | (negSuc m@(suc n)) := ofNat n + ofNat m
-  | (ofNat n) := neg (ofNat n - 7);
+  | (ofNat n) := neg (ofNat n - ofNat 7);
 
 main : Int := f -10 - f 1 + f -1;

tests/Geb/positive/Compilation/test010.juvix

@@ -2,7 +2,6 @@
 module test010;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 f : Nat → Nat → Nat
   | x :=

tests/Geb/positive/Compilation/test012.juvix

@@ -2,7 +2,6 @@
 module test012;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 pow0 : Nat := 1;
 

tests/Geb/positive/Compilation/test016.juvix

@@ -2,7 +2,6 @@
 module test016;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 f : Nat → Nat → Nat

tests/Geb/positive/Compilation/test020.juvix

@@ -2,7 +2,6 @@
 module test020;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 f91 : Nat → Nat

tests/Geb/positive/Compilation/test021.juvix

@@ -2,7 +2,6 @@
 module test021;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 power' : Nat → Nat → Nat → Nat

tests/Geb/positive/Compilation/test022.juvix

@@ -2,11 +2,9 @@
 module test022;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 f : Nat → Nat
-  
   | x := if (x < 1) 1 (2 * x + g (sub x 1));
 
 terminating

tests/Geb/positive/Compilation/test023.juvix

@@ -2,7 +2,6 @@
 module test023;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 gcd : Nat → Nat → Nat

tests/Geb/positive/Compilation/test025.juvix

@@ -2,7 +2,6 @@
 module test025;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 pow : Nat -> Nat
   | zero := 1

tests/Geb/positive/Compilation/test026.juvix

@@ -2,7 +2,6 @@
 module test026;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 sum : Nat → Nat :=
   let

tests/Internal/Core/positive/test006.juvix

@@ -1,7 +1,6 @@
 module test006;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 loop : Nat := loop;

tests/Internal/Core/positive/test011.juvix

@@ -1,7 +1,6 @@
 module test011;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 fib' : Nat -> Nat -> Nat -> Nat
   | zero x _ := x

tests/Internal/positive/QuickSort.juvix

@@ -1,7 +1,6 @@
 module QuickSort;
 
 import Stdlib.Prelude open hiding {quickSort};
-import Stdlib.Data.Nat.Ord open;
 
 qsHelper : {A : Type} → A → List A × List A → List A
   | a (l, r) := l ++ (a :: nil) ++ r;
@@ -40,6 +39,5 @@ four : Nat := suc three;
 
 main : List Nat :=
   uniq
-    compare
+    Ord.cmp
-    (quickSort compare (flatten (gen2 three four nil)));
+    (quickSort Ord.cmp (flatten (gen2 three four nil)));
-

tests/VampIR/negative/test001.juvix

@@ -1,7 +1,6 @@
 module test001;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 {-# argnames: [a, b
                 c] #-}

tests/VampIR/positive/Compilation/test001.juvix

@@ -2,7 +2,6 @@
 module test001;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 main : Nat -> Nat
   | x := if (x == 0) 1 0;

tests/VampIR/positive/Compilation/test002.juvix

@@ -2,7 +2,6 @@
 module test002;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 type optbool :=
   | Just : Bool -> optbool

tests/VampIR/positive/Compilation/test003.juvix

@@ -2,7 +2,6 @@
 module test003;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 type enum :=
   | opt0 : enum

tests/VampIR/positive/Compilation/test006.juvix

@@ -2,7 +2,6 @@
 module test006;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 type enum :=
   | opt0 : enum

tests/VampIR/positive/Compilation/test008.juvix

@@ -2,7 +2,6 @@
 module test008;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 f : Nat → Nat → Nat
   | x :=

tests/VampIR/positive/Compilation/test010.juvix

@@ -2,7 +2,6 @@
 module test010;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 pow0 : Nat := 1;
 

tests/VampIR/positive/Compilation/test017.juvix

@@ -2,7 +2,6 @@
 module test017;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 {-# unroll: 11 #-}
 terminating

tests/VampIR/positive/Compilation/test018.juvix

@@ -2,7 +2,6 @@
 module test018;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 pow : Nat -> Nat
   | zero := 1

tests/VampIR/positive/Compilation/test021.juvix

@@ -2,7 +2,6 @@
 module test021;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 power : Nat → Nat → Nat :=
   let

tests/VampIR/positive/Compilation/test022.juvix

@@ -2,7 +2,6 @@
 module test022;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 power : Nat → Nat → Nat :=
   let

tests/VampIR/positive/Compilation/test023.juvix

@@ -2,7 +2,6 @@
 module test023;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 main : Nat → Nat → Nat
   | x y :=

tests/benchmark/ackermann/juvix/ackermann.juvix

@@ -2,7 +2,6 @@
 module ackermann;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 iter : {A : Type} → (A → A) → Nat → A → A
   | f zero := id

tests/benchmark/combinations/juvix/combinations.juvix

@@ -2,7 +2,6 @@
 module combinations;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 terminating
 go : Nat → Nat → Nat

tests/benchmark/cps/juvix/cps.juvix

@@ -2,7 +2,6 @@
 module cps;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 step : Nat → Nat → Nat → (Nat → Nat → Nat → Nat) → Nat
   | zero n _ _ := n

tests/benchmark/fibonacci/juvix/fibonacci.juvix

@@ -2,7 +2,6 @@
 module fibonacci;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 go : Nat → Nat → Nat → Nat
   | zero n _ := n

tests/benchmark/fold/juvix/fold.juvix

@@ -2,7 +2,6 @@
 module fold;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 plusMod : Nat → Nat → Nat
   | x y := mod (x + y) 268435456;

tests/benchmark/mapfold/juvix/mapfold.juvix

@@ -2,7 +2,6 @@
 module mapfold;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 run : Nat → Nat → List Nat → Nat
   | zero acc lst := acc

tests/benchmark/maybe/juvix/maybe.juvix

@@ -2,7 +2,6 @@
 module maybe;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 type Tree :=
   | leaf : Tree

tests/benchmark/mergesort/juvix/mergesort.juvix

@@ -2,7 +2,6 @@
 module mergesort;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 split_go
   : {A : Type} → List A → List A → List A → List A × List A

tests/benchmark/prime/juvix/prime.juvix

@@ -2,7 +2,6 @@
 module prime;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 checkDivisible : Nat → List Nat → Bool
   | p nil := false

tests/positive/Format.juvix

@@ -12,8 +12,6 @@ hiding -- Hide some names
 -- Bool either
 Bool; true; false; mkShow; module Show};
 
-import Stdlib.Data.Nat.Ord open;
-
 -- Lorem ipsum dolor sit amet, consectetur adipiscing elit
 terminating
 -- Comment between terminating and type sig

tests/positive/issue1731/builtinTrace.juvix

@@ -1,7 +1,6 @@
 module builtinTrace;
 
 import Stdlib.Prelude open;
-import Stdlib.Data.Nat.Ord open;
 
 builtin trace
 axiom trace : {A : Type} → A → A;

tests/smoke/Commands/dev/core.smoke.yaml

@@ -62,6 +62,7 @@ tests:
       - dev
       - core
       - from-concrete
+      - -t eta-expand-apps
       - --normalize
     args:
       - positive/Internal/Norm.juvix

tests/smoke/Commands/repl.smoke.yaml

@@ -74,11 +74,7 @@ tests:
     stdin: ":def + (+) (((+)))"
     stdout:
       contains: |
-        --- Addition for ;Nat;s.
+        + {A} {{Natural A}} : A -> A -> A := Natural.+
-        builtin nat-plus
-        + : Nat → Nat → Nat
-          | zero b := b
-          | (suc a) b := suc (a + b)
     exit-status: 0
 
   - name: repl-def-infix
@@ -89,11 +85,7 @@ tests:
     stdin: ":def +"
     stdout:
       contains: |
-        --- Addition for ;Nat;s.
+        + {A} {{Natural A}} : A -> A -> A := Natural.+
-        builtin nat-plus
-        + : Nat → Nat → Nat
-          | zero b := b
-          | (suc a) b := suc (a + b)
     exit-status: 0
 
   - name: open
@@ -454,7 +446,7 @@ tests:
     command:
       - juvix
       - repl
-    stdin: "import Stdlib.Data.Int.Ord as Int open\n1 == 1"
+    stdin: "import Stdlib.Data.Int.Ord as Int open\n1 Int.== 1"
     stdout:
       contains: "true"
     exit-status: 0
@@ -463,9 +455,9 @@ tests:
     command:
       - juvix
       - repl
-    stdin: "import Stdlib.Data.Int.Ord open\n1 == 1"
+    stdin: "import Stdlib.Data.Int.Ord open\ncompare 1 1"
     stdout:
-      contains: "true"
+      contains: "EQ"
     exit-status: 0
 
   - name: infix-constructors