Convert Nat literals to Core integers

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

@@ -18,6 +18,7 @@ data InfoTable = InfoTable
     _infoInductives :: HashMap Symbol InductiveInfo,
     _infoConstructors :: HashMap Tag ConstructorInfo,
     _infoAxioms :: HashMap Text AxiomInfo,
+    _infoIntToNat :: Maybe Symbol,
     _infoNextSymbol :: Word,
     _infoNextTag :: Word
   }
@@ -32,6 +33,7 @@ emptyInfoTable =
       _infoInductives = mempty,
       _infoConstructors = mempty,
       _infoAxioms = mempty,
+      _infoIntToNat = Nothing,
       _infoNextSymbol = 0,
       _infoNextTag = 0
     }

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

@@ -85,3 +85,82 @@ runInfoTableBuilder tab =
         return $ HashMap.lookup txt (s ^. identMap)
       GetInfoTable ->
         get
+
+--------------------------------------------
+-- Builtin declarations
+--------------------------------------------
+
+createBuiltinConstr ::
+  Symbol ->
+  Tag ->
+  Text ->
+  Type ->
+  Maybe BuiltinConstructor ->
+  Sem r ConstructorInfo
+createBuiltinConstr sym tag nameTxt ty cblt = do
+  return $
+    ConstructorInfo
+      { _constructorName = nameTxt,
+        _constructorLocation = Nothing,
+        _constructorTag = tag,
+        _constructorType = ty,
+        _constructorArgsNum = length (typeArgs ty),
+        _constructorInductive = sym,
+        _constructorBuiltin = cblt
+      }
+
+declareInductiveBuiltins ::
+  Member InfoTableBuilder r =>
+  Text ->
+  Maybe BuiltinInductive ->
+  [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] ->
+  Sem r ()
+declareInductiveBuiltins indName blt ctrs = do
+  sym <- freshSymbol
+  let ty = mkIdent' sym
+  constrs <- mapM (\(tag, name, fty, cblt) -> createBuiltinConstr sym tag name (fty ty) cblt) ctrs
+  registerInductive
+    indName
+    ( InductiveInfo
+        { _inductiveName = indName,
+          _inductiveLocation = Nothing,
+          _inductiveSymbol = sym,
+          _inductiveKind = mkDynamic',
+          _inductiveConstructors = constrs,
+          _inductivePositive = True,
+          _inductiveParams = [],
+          _inductiveBuiltin = blt
+        }
+    )
+  mapM_ (\ci -> registerConstructor (ci ^. constructorName) ci) constrs
+
+declareIOBuiltins :: Member InfoTableBuilder r => Sem r ()
+declareIOBuiltins =
+  declareInductiveBuiltins
+    "IO"
+    Nothing
+    [ (BuiltinTag TagReturn, "return", mkPi' mkDynamic', Nothing),
+      (BuiltinTag TagBind, "bind", \ty -> mkPi' ty (mkPi' (mkPi' mkDynamic' ty) ty), Nothing),
+      (BuiltinTag TagWrite, "write", mkPi' mkDynamic', Nothing),
+      (BuiltinTag TagReadLn, "readLn", id, Nothing)
+    ]
+
+declareBoolBuiltins :: Member InfoTableBuilder r => Sem r ()
+declareBoolBuiltins =
+  declareInductiveBuiltins
+    "bool"
+    (Just BuiltinBool)
+    [ (BuiltinTag TagTrue, "true", id, Just BuiltinBoolTrue),
+      (BuiltinTag TagFalse, "false", id, Just BuiltinBoolFalse)
+    ]
+
+declareNatBuiltins :: Member InfoTableBuilder r => Sem r ()
+declareNatBuiltins = do
+  tagZero <- freshTag
+  tagSuc <- freshTag
+  declareInductiveBuiltins
+    "nat"
+    (Just BuiltinNat)
+    [ (tagZero, "zero", id, Just BuiltinNatZero),
+      (tagSuc, "suc", \x -> mkPi' x x, Just BuiltinNatSuc)
+    ]

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

@@ -17,6 +17,9 @@ convertNode tab = convert [] 0
     go levels bl node = case node of
       NVar (Var {..}) ->
         End' (mkVar _varInfo (_varIndex + length (filter (\x -> x >= bl - _varIndex) levels)))
+      NApp (App _ (NIdt (Ident {..})) l)
+        | Just _identSymbol == tab ^. infoIntToNat ->
+            End' (convert levels bl l)
       NApp (App _ (NApp (App _ (NIdt (Ident {..})) l)) r) ->
         Recur' (levels, convertIdentApp node (\op -> mkBuiltinApp _identInfo op [l, r]) _identSymbol)
       NApp (App _ (NIdt (Ident {..})) l) ->
@@ -90,4 +93,11 @@ convertNode tab = convert [] 0
             _ -> node
 
 natToInt :: InfoTable -> InfoTable
-natToInt tab = mapT (const (convertNode tab)) tab
+natToInt tab = mapT (const (convertNode tab')) tab'
+  where
+    tab' =
+      case tab ^. infoIntToNat of
+        Just sym ->
+          tab {_identContext = HashMap.insert sym (mkLambda' (mkVar' 0)) (tab ^. identContext)}
+        Nothing ->
+          tab

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

@@ -28,21 +28,69 @@ isExplicit = (== Internal.Explicit) . (^. Internal.patternArgIsImplicit)
 mkIdentIndex :: Name -> Text
 mkIdentIndex = show . (^. Internal.nameId . Internal.unNameId)
 
+setupIntToNat :: Symbol -> InfoTable -> InfoTable
+setupIntToNat sym tab =
+  tab
+    { _infoIdentifiers = HashMap.insert sym ii (tab ^. infoIdentifiers),
+      _identContext = HashMap.insert sym node (tab ^. identContext),
+      _infoIntToNat = Just sym
+    }
+  where
+    ii =
+      IdentifierInfo
+        { _identifierSymbol = sym,
+          _identifierName = "intToNat",
+          _identifierLocation = Nothing,
+          _identifierArgsNum = 1,
+          _identifierArgsInfo =
+            [ ArgumentInfo
+                { _argumentName = "x",
+                  _argumentLocation = Nothing,
+                  _argumentType = mkTypePrim' (PrimInteger $ PrimIntegerInfo Nothing Nothing),
+                  _argumentIsImplicit = Explicit
+                }
+            ],
+          _identifierType = mkDynamic',
+          _identifierIsExported = False,
+          _identifierBuiltin = Nothing
+        }
+    node =
+      case (tagZeroM, tagSucM, boolSymM) of
+        (Just tagZero, Just tagSuc, Just boolSym) ->
+          mkLambda' $
+            mkIf'
+              boolSym
+              (mkBuiltinApp' OpEq [mkVar' 0, mkConstant' (ConstInteger 0)])
+              (mkConstr (setInfoName "zero" mempty) tagZero [])
+              (mkConstr (setInfoName "suc" mempty) tagSuc [mkApp' (mkIdent' sym) (mkBuiltinApp' OpIntSub [mkVar' 0, mkConstant' (ConstInteger 1)])])
+        _ ->
+          mkLambda' $ mkVar' 0
+    tagZeroM = fmap ((^. constructorTag) . fst) $ uncons $ filter (\ci -> ci ^. constructorBuiltin == Just BuiltinNatZero) $ HashMap.elems (tab ^. infoConstructors)
+    tagSucM = fmap ((^. constructorTag) . fst) $ uncons $ filter (\ci -> ci ^. constructorBuiltin == Just BuiltinNatSuc) $ HashMap.elems (tab ^. infoConstructors)
+    boolSymM = fmap ((^. inductiveSymbol) . fst) $ uncons $ filter (\ind -> ind ^. inductiveBuiltin == Just BuiltinBool) $ HashMap.elems (tab ^. infoInductives)
+
 fromInternal :: Internal.InternalTypedResult -> Sem k CoreResult
 fromInternal i = do
-  (res, _) <- runInfoTableBuilder emptyInfoTable (runReader (i ^. InternalTyped.resultIdenTypes) f)
+  (res, _) <- runInfoTableBuilder tab0 (runReader (i ^. InternalTyped.resultIdenTypes) f)
   return $
     CoreResult
-      { _coreResultTable = res,
+      { _coreResultTable = setupIntToNat intToNatSym res,
         _coreResultInternalTypedResult = i
       }
   where
+    tab0 :: InfoTable
+    tab0 = emptyInfoTable {_infoIntToNat = Just intToNatSym, _infoNextSymbol = intToNatSym + 1}
+
+    intToNatSym :: Symbol
+    intToNatSym = 0
+
     f :: Members '[InfoTableBuilder, Reader InternalTyped.TypesTable] r => Sem r ()
     f = do
+      declareIOBuiltins
       let resultModules = toList (i ^. InternalTyped.resultModules)
-      runNameIdGen (runReader (Internal.buildTable resultModules) (mapM_ coreModule resultModules))
+      runReader (Internal.buildTable resultModules) (mapM_ coreModule resultModules)
       where
-        coreModule :: Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, NameIdGen] r => Internal.Module -> Sem r ()
+        coreModule :: Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r => Internal.Module -> Sem r ()
         coreModule m = do
           registerInductiveDefs m
           registerFunctionDefs m
@@ -86,14 +134,14 @@ registerInductiveDefsBody body = mapM_ go (body ^. Internal.moduleStatements)
 
 registerFunctionDefs ::
   forall r.
-  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, NameIdGen, Reader Internal.InfoTable] r =>
+  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r =>
   Internal.Module ->
   Sem r ()
 registerFunctionDefs m = registerFunctionDefsBody (m ^. Internal.moduleBody)
 
 registerFunctionDefsBody ::
   forall r.
-  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, NameIdGen, Reader Internal.InfoTable] r =>
+  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r =>
   Internal.ModuleBody ->
   Sem r ()
 registerFunctionDefsBody body = mapM_ go (body ^. Internal.moduleStatements)
@@ -173,7 +221,7 @@ goConstructor sym ctor = do
 
 goMutualBlock ::
   forall r.
-  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, NameIdGen, Reader Internal.InfoTable] r =>
+  Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r =>
   Internal.MutualBlock ->
   Sem r ()
 goMutualBlock m = do
@@ -188,7 +236,7 @@ goMutualBlock m = do
 
 goFunctionDefIden ::
   forall r.
-  Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, NameIdGen] r =>
+  Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable] r =>
   (Internal.FunctionDef, Symbol) ->
   Sem r ()
 goFunctionDefIden (f, sym) = do
@@ -470,7 +518,9 @@ goExpression' ::
   Internal.Expression ->
   Sem r Node
 goExpression' = \case
-  Internal.ExpressionLiteral l -> return (goLiteral l)
+  Internal.ExpressionLiteral l -> do
+    tab <- getInfoTable
+    return (goLiteral (fromJust $ tab ^. infoIntToNat) l)
   Internal.ExpressionIden i -> case i of
     Internal.IdenVar n -> do
       k <- HashMap.lookupDefault impossible id_ <$> asks (^. indexTableVars)
@@ -568,10 +618,10 @@ goApplication a = do
         _ -> app
     _ -> app
 
-goLiteral :: LiteralLoc -> Node
-goLiteral l = case l ^. withLocParam of
+goLiteral :: Symbol -> LiteralLoc -> Node
+goLiteral intToNat l = case l ^. withLocParam of
   Internal.LitString s -> mkLitConst (ConstString s)
-  Internal.LitInteger i -> mkLitConst (ConstInteger i)
+  Internal.LitInteger i -> mkApp' (mkIdent' intToNat) (mkLitConst (ConstInteger i))
   where
     mkLitConst :: ConstantValue -> Node
     mkLitConst = mkConstant (Info.singleton (LocationInfo (l ^. withLocInt)))

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

@@ -43,92 +43,13 @@ guardSymbolNotDefined sym err = do
   b <- lift $ checkSymbolDefined sym
   when b err
 
-createBuiltinConstr ::
-  Symbol ->
-  Tag ->
-  Text ->
-  Type ->
-  Interval ->
-  Maybe BuiltinConstructor ->
-  Sem r ConstructorInfo
-createBuiltinConstr sym tag nameTxt ty i cblt = do
-  return $
-    ConstructorInfo
-      { _constructorName = nameTxt,
-        _constructorLocation = Just i,
-        _constructorTag = tag,
-        _constructorType = ty,
-        _constructorArgsNum = length (typeArgs ty),
-        _constructorInductive = sym,
-        _constructorBuiltin = cblt
-      }
-
-declareInductiveBuiltins ::
-  Member InfoTableBuilder r =>
-  Text ->
-  Maybe BuiltinInductive ->
-  [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] ->
-  ParsecS r ()
-declareInductiveBuiltins indName blt ctrs = do
-  loc <- curLoc
-  let i = mkInterval loc loc
-  sym <- lift freshSymbol
-  let ty = mkIdent' sym
-  constrs <- lift $ mapM (\(tag, name, fty, cblt) -> createBuiltinConstr sym tag name (fty ty) i cblt) ctrs
-  lift $
-    registerInductive
-      indName
-      ( InductiveInfo
-          { _inductiveName = indName,
-            _inductiveLocation = Just i,
-            _inductiveSymbol = sym,
-            _inductiveKind = mkDynamic',
-            _inductiveConstructors = constrs,
-            _inductivePositive = True,
-            _inductiveParams = [],
-            _inductiveBuiltin = blt
-          }
-      )
-  lift $ mapM_ (\ci -> registerConstructor (ci ^. constructorName) ci) constrs
-
-declareIOBuiltins :: Member InfoTableBuilder r => ParsecS r ()
-declareIOBuiltins =
-  declareInductiveBuiltins
-    "IO"
-    Nothing
-    [ (BuiltinTag TagReturn, "return", mkPi' mkDynamic', Nothing),
-      (BuiltinTag TagBind, "bind", \ty -> mkPi' ty (mkPi' (mkPi' mkDynamic' ty) ty), Nothing),
-      (BuiltinTag TagWrite, "write", mkPi' mkDynamic', Nothing),
-      (BuiltinTag TagReadLn, "readLn", id, Nothing)
-    ]
-
-declareBoolBuiltins :: Member InfoTableBuilder r => ParsecS r ()
-declareBoolBuiltins =
-  declareInductiveBuiltins
-    "bool"
-    (Just BuiltinBool)
-    [ (BuiltinTag TagTrue, "true", id, Just BuiltinBoolTrue),
-      (BuiltinTag TagFalse, "false", id, Just BuiltinBoolFalse)
-    ]
-
-declareNatBuiltins :: Member InfoTableBuilder r => ParsecS r ()
-declareNatBuiltins = do
-  tagZero <- lift freshTag
-  tagSuc <- lift freshTag
-  declareInductiveBuiltins
-    "nat"
-    (Just BuiltinNat)
-    [ (tagZero, "zero", id, Just BuiltinNatZero),
-      (tagSuc, "suc", \x -> mkPi' x x, Just BuiltinNatSuc)
-    ]
-
 parseToplevel ::
   Member InfoTableBuilder r =>
   ParsecS r (Maybe Node)
 parseToplevel = do
-  declareIOBuiltins
-  declareBoolBuiltins
-  declareNatBuiltins
+  lift declareIOBuiltins
+  lift declareBoolBuiltins
+  lift declareNatBuiltins
   space
   P.endBy statement (kw kwSemicolon)
   r <- optional expression

test/Internal/Eval/Positive.hs

@@ -100,12 +100,12 @@ tests =
       $(mkRelFile "NatMatch2.juvix")
       $(mkRelFile "out/NatMatch2.out"),
     PosTest
-      "Literal integer is Core integer"
+      "Literal Nat"
       $(mkRelDir ".")
       $(mkRelFile "LitInteger.juvix")
       $(mkRelFile "out/LitInteger.out"),
     PosTest
-      "Literal integer is Core string"
+      "Literal String"
       $(mkRelDir ".")
       $(mkRelFile "LitString.juvix")
       $(mkRelFile "out/LitString.out"),

tests/CLI/Commands/repl.test

@@ -90,3 +90,9 @@ $ juvix repl tests/Internal/positive/BuiltinBool.juvix
 $ juvix repl
 > /\//
 >= 0
+
+<
+1 + 2
+$ juvix repl
+> /Stdlib.Prelude> suc \(suc \(suc zero\)\)/
+>= 0

tests/Internal/positive/LitInteger.juvix

@@ -3,7 +3,7 @@ module LitInteger;
 open import Stdlib.Prelude public;
 
 main : Nat;
-main := 1;
+main := 1 + 2;
 
 nilNat : List Nat;
 nilNat := nil;

tests/Internal/positive/out/LitInteger.out

@@ -1 +1 @@
-1
+suc (suc (suc zero))