Give a proper type to literal natural numbers

examples/milestone/ValidityPredicates/Anoma/Base.juvix

@@ -36,7 +36,7 @@ open import Data.Int.Ops;
 import Stdlib.Data.String.Ord;
 
 from-int : Int → Maybe Int;
-from-int i ≔ if (i < 0) nothing (just i);
+from-int i ≔ if (i < Int_0) nothing (just i);
 
 from-string : String → Maybe String;
 from-string s ≔ if (s Stdlib.Data.String.Ord.== "") nothing (just s);
@@ -73,6 +73,6 @@ is-balance-key : String → String → Maybe String;
 is-balance-key token key ≔ from-string (isBalanceKey token key);
 
 unwrap-default : Maybe Int → Int;
-unwrap-default ≔ maybe 0 id;
+unwrap-default ≔ maybe Int_0 id;
 
 end;

examples/milestone/ValidityPredicates/Data/Int.juvix

@@ -6,4 +6,14 @@ compile Int {
   c ↦ "int";
 };
 
+axiom Int_0 : Int;
+compile Int_0 {
+  c ↦ "0";
+};
+
+axiom Int_1 : Int;
+compile Int_1 {
+  c ↦ "1";
+};
+
 end;

examples/milestone/ValidityPredicates/SimpleFungibleToken.juvix

@@ -9,7 +9,7 @@ import Data.Int.Ops;
 -- Misc
 
 pair-from-optionString : (String → Int × Bool) → Maybe String → Int × Bool;
-pair-from-optionString ≔ maybe (0 , false);
+pair-from-optionString ≔ maybe (Int_0 , false);
 
 -- Validity Predicate
 
@@ -19,7 +19,7 @@ change-from-key key ≔ unwrap-default (read-post key) Data.Int.Ops.- unwrap-def
 check-vp : List String → String → Int → String → Int × Bool;
 check-vp verifiers key change owner ≔
     if
-        (change-from-key key Data.Int.Ops.< 0)
+        (change-from-key key Data.Int.Ops.< Int_0)
         -- make sure the spender approved the transaction
         (change Data.Int.Ops.+ (change-from-key key), elem (Stdlib.Data.String.Ord.==) owner verifiers)
         (change Data.Int.Ops.+ (change-from-key key),  true);
@@ -29,16 +29,16 @@ check-keys token verifiers (change , is-success) key ≔
     if
         is-success
         (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key))
-        (0 , false);
+        (Int_0 , false);
 
 check-result : Int × Bool → Bool;
-check-result (change , all-checked) ≔ (change Data.Int.Ops.== 0) && all-checked;
+check-result (change , all-checked) ≔ (change Data.Int.Ops.== Int_0) && all-checked;
 
 vp : String → List String → List String → Bool;
 vp token keys-changed verifiers ≔
     check-result
         (foldl
             (check-keys token verifiers)
-            (0 , true)
+            (Int_0 , true)
             keys-changed);
 end;

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

@@ -5,6 +5,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal
 where
 
 import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Internal.Language
 import Juvix.Compiler.Internal.Translation.FromAbstract.Data.Context
 import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as ArityChecking
@@ -31,7 +32,7 @@ arityChecking res@InternalResult {..} =
     table = buildTable _resultModules
 
 typeChecking ::
-  Members '[Error JuvixError, NameIdGen] r =>
+  Members '[Error JuvixError, NameIdGen, Builtins] r =>
   ArityChecking.InternalArityResult ->
   Sem r InternalTypedResult
 typeChecking res@ArityChecking.InternalArityResult {..} =

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs

@@ -100,7 +100,7 @@ guessArity ::
 guessArity = \case
   ExpressionHole {} -> return Nothing
   ExpressionFunction {} -> return (Just ArityUnit)
-  ExpressionLiteral {} -> return (Just arityLiteral)
+  ExpressionLiteral l -> return (Just (arityLiteral l))
   ExpressionApplication a -> appHelper a
   ExpressionIden i -> idenHelper i
   ExpressionUniverse {} -> return (Just arityUniverse)
@@ -133,18 +133,20 @@ guessArity = \case
           ExpressionUniverse {} -> return (Just arityUniverse)
           ExpressionApplication {} -> impossible
           ExpressionFunction {} -> return (Just ArityUnit)
-          ExpressionLiteral {} -> return (Just arityLiteral)
+          ExpressionLiteral l -> return (Just (arityLiteral l))
           ExpressionIden i -> idenHelper i
           ExpressionLambda {} -> lambda
 
 -- | The arity of all literals is assumed to be: {} -> 1
-arityLiteral :: Arity
-arityLiteral =
-  ArityFunction
-    FunctionArity
-      { _functionArityLeft = ParamImplicit,
-        _functionArityRight = ArityUnit
-      }
+arityLiteral :: LiteralLoc -> Arity
+arityLiteral (WithLoc _ l) = case l of
+  LitInteger {} -> ArityUnit
+  LitString {} ->
+    ArityFunction
+      FunctionArity
+        { _functionArityLeft = ParamImplicit,
+          _functionArityRight = ArityUnit
+        }
 
 arityUniverse :: Arity
 arityUniverse = ArityUnit
@@ -336,7 +338,7 @@ checkExpression hintArity expr = case expr of
       args' :: [(IsImplicit, Expression)] <- case fun of
         ExpressionHole {} -> mapM (secondM (checkExpression ArityUnknown)) args
         ExpressionIden i -> idenArity i >>= helper (getLoc i)
-        ExpressionLiteral l -> helper (getLoc l) arityLiteral
+        ExpressionLiteral l -> helper (getLoc l) (arityLiteral l)
         ExpressionUniverse l -> helper (getLoc l) arityUniverse
         ExpressionLambda {} -> lambda
         ExpressionFunction f ->

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs

@@ -5,6 +5,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Ch
 where
 
 import Data.HashMap.Strict qualified as HashMap
+import Juvix.Compiler.Builtins.Effect
 import Juvix.Compiler.Internal.Data.LocalVars
 import Juvix.Compiler.Internal.Extra
 import Juvix.Compiler.Internal.Pretty
@@ -22,7 +23,7 @@ registerConstructor ctr = do
   modify (HashMap.insert (ctr ^. inductiveConstructorName) ty)
 
 checkModule ::
-  Members '[Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example] r =>
+  Members '[Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r =>
   Module ->
   Sem r Module
 checkModule Module {..} = do
@@ -35,7 +36,7 @@ checkModule Module {..} = do
       }
 
 checkModuleBody ::
-  Members '[Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example] r =>
+  Members '[Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r =>
   ModuleBody ->
   Sem r ModuleBody
 checkModuleBody ModuleBody {..} = do
@@ -46,13 +47,13 @@ checkModuleBody ModuleBody {..} = do
       }
 
 checkInclude ::
-  Members '[Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example] r =>
+  Members '[Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r =>
   Include ->
   Sem r Include
 checkInclude = traverseOf includeModule checkModule
 
 checkStatement ::
-  Members '[Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example] r =>
+  Members '[Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r =>
   Statement ->
   Sem r Statement
 checkStatement s = case s of
@@ -66,7 +67,7 @@ checkStatement s = case s of
 
 checkInductiveDef ::
   forall r.
-  Members '[Reader EntryPoint, Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, State NegativeTypeParameters, Output Example] r =>
+  Members '[Reader EntryPoint, Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, State NegativeTypeParameters, Output Example, Builtins] r =>
   InductiveDef ->
   Sem r InductiveDef
 -- checkInductiveDef (InductiveDef name built params constrs pos) = runInferenceDef $ do
@@ -127,7 +128,7 @@ withEmptyVars :: Sem (Reader LocalVars : r) a -> Sem r a
 withEmptyVars = runReader emptyLocalVars
 
 checkFunctionDef ::
-  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example] r =>
+  Members '[Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r =>
   FunctionDef ->
   Sem r FunctionDef
 checkFunctionDef FunctionDef {..} = do
@@ -145,15 +146,15 @@ checkFunctionDef FunctionDef {..} = do
   readerState @FunctionsTable (traverseOf funDefExamples (mapM checkExample) funDef)
 
 checkIsType ::
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins] r =>
   Interval ->
   Expression ->
   Sem r Expression
 checkIsType = checkExpression . smallUniverseE
 
 checkFunctionDefType ::
   forall r.
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins] r =>
   Expression ->
   Sem r Expression
 checkFunctionDefType ty = do
@@ -165,7 +166,7 @@ checkFunctionDefType ty = do
     go h = freshMetavar h
 
 checkExample ::
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Output Example, State TypesTable] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Output Example, State TypesTable] r =>
   Example ->
   Sem r Example
 checkExample e = do
@@ -174,7 +175,7 @@ checkExample e = do
   return e'
 
 checkExpression ::
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, Builtins, NameIdGen, Reader LocalVars, Inference] r =>
   Expression ->
   Expression ->
   Sem r Expression
@@ -194,21 +195,13 @@ checkExpression expectedTy e = do
         )
 
 checkFunctionParameter ::
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins] r =>
   FunctionParameter ->
   Sem r FunctionParameter
 checkFunctionParameter (FunctionParameter mv i e) = do
   e' <- checkIsType (getLoc e) e
   return (FunctionParameter mv i e')
 
--- checkInductiveDef ::
---   Members '[Reader InfoTable, Error TypeCheckerError, State NegativeTypeParameters, Reader EntryPoint] r =>
---   InductiveDef ->
---   Sem r ()
--- checkInductiveDef ty@InductiveDef {..} = do
---   checkPositivity ty
---   mapM_ (checkConstructorDef ty) _inductiveConstructors
-
 checkConstructorDef ::
   Members
     '[ Reader EntryPoint,
@@ -251,7 +244,7 @@ checkConstructorReturnType indType ctor = do
     )
 
 inferExpression ::
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Builtins, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference] r =>
   Expression ->
   Sem r Expression
 inferExpression = fmap (^. typedExpression) . inferExpression'
@@ -262,7 +255,7 @@ lookupVar v = HashMap.lookupDefault err v <$> asks (^. localTypes)
     err = error $ "internal error: could not find var " <> ppTrace v
 
 checkFunctionClauseBody ::
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Builtins, Inference] r =>
   LocalVars ->
   Expression ->
   Expression ->
@@ -272,7 +265,7 @@ checkFunctionClauseBody locals expectedTy body =
 
 checkFunctionClause ::
   forall r.
-  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Error TypeCheckerError, NameIdGen, Builtins, Inference] r =>
   Expression ->
   FunctionClause ->
   Sem r FunctionClause
@@ -457,9 +450,20 @@ freshHole l = do
   freshMetavar h
   return h
 
+literalType :: Members '[NameIdGen, Builtins] r => LiteralLoc -> Sem r TypedExpression
+literalType lit@(WithLoc i l) = case l of
+  LitInteger {} -> do
+    nat <- getBuiltinName i BuiltinNatural
+    return
+      TypedExpression
+        { _typedExpression = ExpressionLiteral lit,
+          _typedType = ExpressionIden (IdenInductive nat)
+        }
+  LitString {} -> literalMagicType lit
+
 -- | Returns {A : Expression} → A
-literalType :: Members '[NameIdGen] r => LiteralLoc -> Sem r TypedExpression
-literalType l = do
+literalMagicType :: Members '[NameIdGen] r => LiteralLoc -> Sem r TypedExpression
+literalMagicType l = do
   uid <- freshNameId
   let strA :: Text
       strA = "A"
@@ -491,7 +495,7 @@ literalType l = do
 
 inferExpression' ::
   forall r.
-  Members '[Reader InfoTable, Reader FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference] r =>
+  Members '[Reader InfoTable, Reader FunctionsTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Builtins] r =>
   Expression ->
   Sem r TypedExpression
 inferExpression' e = case e of

src/Juvix/Compiler/Pipeline.hs

@@ -152,7 +152,7 @@ pipelineAbstract ::
 pipelineAbstract = mapError (JuvixError @Scoper.ScoperError) . Abstract.fromConcrete
 
 pipelineInternalTyped ::
-  Members '[Files, NameIdGen, Error JuvixError] r =>
+  Members '[Files, NameIdGen, Error JuvixError, Builtins] r =>
   Internal.InternalArityResult ->
   Sem r Internal.InternalTypedResult
 pipelineInternalTyped =

tests/positive/FullExamples/MonoSimpleFungibleToken.juvix

@@ -69,6 +69,11 @@ compile Int {
   ghc ↦ "Int";
 };
 
+axiom Int_0 : Int;
+compile Int_0 {
+  ghc ↦ "0";
+};
+
 axiom lt : Int → Int → BackendBool;
 compile lt {
   ghc ↦ "(<)";
@@ -156,7 +161,7 @@ if-optionInt true x _ ≔ x;
 if-optionInt false _ y ≔ y;
 
 from-int : Int → OptionInt;
-from-int i ≔ if-optionInt (i < 0) NothingInt (JustInt i);
+from-int i ≔ if-optionInt (i < Int_0) NothingInt (JustInt i);
 
 maybe-int : Int → OptionInt → Int;
 maybe-int d NothingInt ≔ d;
@@ -175,7 +180,7 @@ from-string : String → OptionString;
 from-string s ≔ if-optionString (s ==String "") NothingString (JustString s);
 
 pair-from-optionString : (String → PairIntBool) → OptionString → PairIntBool;
-pair-from-optionString _ NothingString ≔ MakePair 0 false;
+pair-from-optionString _ NothingString ≔ MakePair Int_0 false;
 pair-from-optionString f (JustString o) ≔ f o;
 
 --------------------------------------------------------------------------------
@@ -215,7 +220,7 @@ is-balance-key : String → String → OptionString;
 is-balance-key token key ≔ from-string (isBalanceKey token key);
 
 unwrap-default : OptionInt → Int;
-unwrap-default o ≔ maybe-int 0 o;
+unwrap-default o ≔ maybe-int Int_0 o;
 
 --------------------------------------------------------------------------------
 -- Validity Predicate
@@ -227,7 +232,7 @@ change-from-key key ≔ unwrap-default (read-post key) - unwrap-default (read-pr
 check-vp : ListString → String → Int → String → PairIntBool;
 check-vp verifiers key change owner ≔
     if-pairIntBool
-        (change-from-key key < 0)
+        (change-from-key key < Int_0)
         -- make sure the spender approved the transaction
         (MakePair (change + (change-from-key key)) (elem owner verifiers))
         (MakePair (change + (change-from-key key)) true);
@@ -237,17 +242,17 @@ check-keys token verifiers (MakePair change is-success) key ≔
     if-pairIntBool
         is-success
         (pair-from-optionString (check-vp verifiers key change) (is-balance-key token key))
-        (MakePair 0 false);
+        (MakePair Int_0 false);
 
 check-result : PairIntBool → Bool;
-check-result (MakePair change all-checked) ≔ (change ==Int 0) && all-checked;
+check-result (MakePair change all-checked) ≔ (change ==Int Int_0) && all-checked;
 
 vp : String → ListString → ListString → Bool;
 vp token keys-changed verifiers ≔
     check-result
         (foldl
             (check-keys token verifiers)
-            (MakePair 0 true)
+            (MakePair Int_0 true)
             keys-changed);
 
 --------------------------------------------------------------------------------