Conversion of Nat representation to JuvixCore integers (#1661)

* nat to int wip

* nat to int wip

* fix condition

* nats in core

* bugfixes

* tests

* make ormolu happy

* fix case

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

@@ -1,6 +1,6 @@
 module Juvix.Compiler.Core.Data.BinderList where
 
-import Juvix.Compiler.Core.Language hiding (cons, lookup, uncons)
+import Juvix.Compiler.Core.Language hiding (cons, drop, lookup, uncons)
 import Juvix.Prelude qualified as Prelude
 
 -- | if we have \x\y. b, the binderlist in b is [y, x]
@@ -14,11 +14,11 @@ makeLenses ''BinderList
 fromList :: [a] -> BinderList a
 fromList l = BinderList (length l) l
 
-drop' :: Int -> BinderList a -> BinderList a
+drop :: Int -> BinderList a -> BinderList a
-drop' k (BinderList n l) = BinderList (n - k) (dropExact k l)
+drop k (BinderList n l) = BinderList (n - k) (dropExact k l)
 
-tail' :: BinderList a -> BinderList a
+tail :: BinderList a -> BinderList a
-tail' = snd . fromJust . uncons
+tail = snd . fromJust . uncons
 
 uncons :: BinderList a -> Maybe (a, BinderList a)
 uncons l = second helper <$> Prelude.uncons (l ^. blMap)
@@ -60,7 +60,7 @@ lookupsSortedRev bl = go [] 0 bl
       (v : vs) ->
         let skipped = v ^. varIndex - off
             off' = off + skipped
-            ctx' = drop' skipped ctx
+            ctx' = drop skipped ctx
          in go ((v, head' ctx') : acc) off' ctx' vs
     head' :: BinderList a -> a
     head' = lookup 0

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

@@ -1,5 +1,10 @@
-module Juvix.Compiler.Core.Data.InfoTable where
+module Juvix.Compiler.Core.Data.InfoTable
+  ( module Juvix.Compiler.Core.Data.InfoTable,
+    module Juvix.Compiler.Concrete.Data.Builtins,
+  )
+where
 
+import Juvix.Compiler.Concrete.Data.Builtins
 import Juvix.Compiler.Core.Language
 
 type IdentContext = HashMap Symbol Node
@@ -43,7 +48,8 @@ data IdentifierInfo = IdentifierInfo
     _identifierType :: Type,
     _identifierArgsNum :: Int,
     _identifierArgsInfo :: [ArgumentInfo],
-    _identifierIsExported :: Bool
+    _identifierIsExported :: Bool,
+    _identifierBuiltin :: Maybe BuiltinFunction
   }
 
 data ArgumentInfo = ArgumentInfo
@@ -60,7 +66,8 @@ data InductiveInfo = InductiveInfo
     _inductiveKind :: Type,
     _inductiveConstructors :: [ConstructorInfo],
     _inductiveParams :: [ParameterInfo],
-    _inductivePositive :: Bool
+    _inductivePositive :: Bool,
+    _inductiveBuiltin :: Maybe BuiltinInductive
   }
 
 data ConstructorInfo = ConstructorInfo
@@ -69,7 +76,8 @@ data ConstructorInfo = ConstructorInfo
     _constructorTag :: Tag,
     _constructorType :: Type,
     _constructorArgsNum :: Int,
-    _constructorInductive :: Symbol
+    _constructorInductive :: Symbol,
+    _constructorBuiltin :: Maybe BuiltinConstructor
   }
 
 data ParameterInfo = ParameterInfo

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

@@ -24,6 +24,21 @@ getConstructorInfo tag = do
   tab <- getInfoTable
   return $ fromJust (HashMap.lookup tag (tab ^. infoConstructors))
 
+getInductiveInfo :: Member InfoTableBuilder r => Symbol -> Sem r InductiveInfo
+getInductiveInfo sym = do
+  tab <- getInfoTable
+  return $ fromJust (HashMap.lookup sym (tab ^. infoInductives))
+
+getIdentifierInfo :: Member InfoTableBuilder r => Symbol -> Sem r IdentifierInfo
+getIdentifierInfo sym = do
+  tab <- getInfoTable
+  return $ fromJust (HashMap.lookup sym (tab ^. infoIdentifiers))
+
+getBoolSymbol :: Member InfoTableBuilder r => Sem r Symbol
+getBoolSymbol = do
+  ci <- getConstructorInfo (BuiltinTag TagTrue)
+  return $ ci ^. constructorInductive
+
 checkSymbolDefined :: Member InfoTableBuilder r => Symbol -> Sem r Bool
 checkSymbolDefined sym = do
   tab <- getInfoTable

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

@@ -7,5 +7,6 @@ data TransformationId
   | TopEtaExpand
   | RemoveTypeArgs
   | MoveApps
+  | NatToInt
   | Identity
   deriving stock (Data)

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

@@ -46,6 +46,7 @@ pcompletions = do
       Identity -> strIdentity
       RemoveTypeArgs -> strRemoveTypeArgs
       MoveApps -> strMoveApps
+      NatToInt -> strNatToInt
 
 lexeme :: MonadParsec e Text m => m a -> m a
 lexeme = L.lexeme L.hspace
@@ -63,6 +64,7 @@ transformation =
     <|> symbol strTopEtaExpand $> TopEtaExpand
     <|> symbol strRemoveTypeArgs $> RemoveTypeArgs
     <|> symbol strMoveApps $> MoveApps
+    <|> symbol strNatToInt $> NatToInt
 
 allStrings :: [Text]
 allStrings =
@@ -87,3 +89,6 @@ strRemoveTypeArgs = "remove-type-args"
 
 strMoveApps :: Text
 strMoveApps = "move-apps"
+
+strNatToInt :: Text
+strNatToInt = "nat-to-int"

src/Juvix/Compiler/Core/Evaluator.hs

@@ -70,10 +70,10 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
         let !vs' = map (eval' env' . (^. letItemValue)) (toList vs)
             !env' = revAppend vs' env
          in foldr GHC.pseq (eval' env' b) vs'
-      NCase (Case i v bs def) ->
+      NCase (Case i sym v bs def) ->
         case eval' env v of
           NCtr (Constr _ tag args) -> branch n env args tag def bs
-          v' -> evalError "matching on non-data" (substEnv env (mkCase i v' bs def))
+          v' -> evalError "matching on non-data" (substEnv env (mkCase i sym v' bs def))
       NMatch (Match _ vs bs) ->
         let !vs' = map' (eval' env) (toList vs)
          in match n env vs' bs

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

@@ -55,6 +55,9 @@ mkLambda i bi b = NLam (Lambda i bi b)
 mkLambda' :: Node -> Node
 mkLambda' = mkLambda Info.empty emptyBinder
 
+mkLambdaTy :: Node -> Node -> Node
+mkLambdaTy ty = mkLambda Info.empty (Binder "?" Nothing ty)
+
 mkLetItem' :: Node -> LetItem
 mkLetItem' = LetItem emptyBinder
 
@@ -70,10 +73,10 @@ mkLetRec i vs b = NRec (LetRec i vs b)
 mkLetRec' :: NonEmpty Node -> Node -> Node
 mkLetRec' = mkLetRec Info.empty . fmap mkLetItem'
 
-mkCase :: Info -> Node -> [CaseBranch] -> Maybe Node -> Node
+mkCase :: Info -> Symbol -> Node -> [CaseBranch] -> Maybe Node -> Node
-mkCase i v bs def = NCase (Case i v bs def)
+mkCase i sym v bs def = NCase (Case i sym v bs def)
 
-mkCase' :: Node -> [CaseBranch] -> Maybe Node -> Node
+mkCase' :: Symbol -> Node -> [CaseBranch] -> Maybe Node -> Node
 mkCase' = mkCase Info.empty
 
 mkMatch :: Info -> NonEmpty Node -> [MatchBranch] -> Node
@@ -82,8 +85,8 @@ mkMatch i vs bs = NMatch (Match i vs bs)
 mkMatch' :: NonEmpty Node -> [MatchBranch] -> Node
 mkMatch' = mkMatch Info.empty
 
-mkIf :: Info -> Node -> Node -> Node -> Node
+mkIf :: Info -> Symbol -> Node -> Node -> Node -> Node
-mkIf i v b1 b2 = mkCase i v [br] (Just b2)
+mkIf i sym v b1 b2 = mkCase i sym v [br] (Just b2)
   where
     br =
       CaseBranch
@@ -94,7 +97,7 @@ mkIf i v b1 b2 = mkCase i v [br] (Just b2)
           _caseBranchBody = b1
         }
 
-mkIf' :: Node -> Node -> Node -> Node
+mkIf' :: Symbol -> Node -> Node -> Node -> Node
 mkIf' = mkIf Info.empty
 
 {------------------------------------------------------------------------}
@@ -480,7 +483,7 @@ destruct = \case
                   ]
            in mkLetRec i' items' (b' ^. childNode)
       }
-  NCase (Case i v brs mdef) ->
+  NCase (Case i sym v brs mdef) ->
     let branchChildren :: [([Binder], NodeChild)]
         branchChildren =
           [ (binders, manyBinders binders (br ^. caseBranchBody))
@@ -520,7 +523,7 @@ destruct = \case
                 _nodeSubinfos = map (^. caseBranchInfo) brs,
                 _nodeChildren = noBinders v : allNodes,
                 _nodeReassemble = someChildrenI $ \i' is' (v' :| allNodes') ->
-                  mkCase i' (v' ^. childNode) (mkBranches is' allNodes') Nothing
+                  mkCase i' sym (v' ^. childNode) (mkBranches is' allNodes') Nothing
               }
           Just def ->
             NodeDetails
@@ -528,7 +531,7 @@ destruct = \case
                 _nodeSubinfos = map (^. caseBranchInfo) brs,
                 _nodeChildren = noBinders v : noBinders def : allNodes,
                 _nodeReassemble = twoManyChildrenI $ \i' is' v' def' allNodes' ->
-                  mkCase i' (v' ^. childNode) (mkBranches is' allNodes') (Just (def' ^. childNode))
+                  mkCase i' sym (v' ^. childNode) (mkBranches is' allNodes') (Just (def' ^. childNode))
               }
   NMatch (Match i vs branches) ->
     let allNodes :: [NodeChild]

src/Juvix/Compiler/Core/Extra/Recursors/Map.hs

@@ -112,6 +112,14 @@ fromRecur c =
 fromPair :: Functor g => d -> g (c, Node) -> g (Recur' (c, d))
 fromPair d = fmap (\(c, x) -> Recur' ((c, d), x))
 
+fromRecur' :: Functor g => d -> g (Recur' c) -> g (Recur' (c, d))
+fromRecur' d =
+  fmap
+    ( \case
+        End' x -> End' x
+        Recur' (c, x) -> Recur' ((c, d), x)
+    )
+
 nodeMapG' ::
   Monad m =>
   Sing dir ->

src/Juvix/Compiler/Core/Extra/Recursors/Map/Named.hs

@@ -6,21 +6,21 @@ import Juvix.Compiler.Core.Extra.Recursors.Map
 import Juvix.Compiler.Core.Extra.Recursors.Parameters
 
 dmapLRM :: Monad m => (BinderList Binder -> Node -> m Recur) -> Node -> m Node
-dmapLRM f = nodeMapG' STopDown binderInfoCollector (\bi -> fromRecur bi . f bi)
+dmapLRM f = dmapLRM' (mempty, f)
 
 dmapLM :: Monad m => (BinderList Binder -> Node -> m Node) -> Node -> m Node
-dmapLM f = nodeMapG' STopDown binderInfoCollector (\bi -> fromSimple bi . f bi)
+dmapLM f = dmapLM' (mempty, f)
 
 umapLM :: Monad m => (BinderList Binder -> Node -> m Node) -> Node -> m Node
 umapLM f = nodeMapG' SBottomUp binderInfoCollector f
 
-dmapNRM :: Monad m => (Index -> Node -> m Recur) -> Node -> m Node
+dmapNRM :: Monad m => (Level -> Node -> m Recur) -> Node -> m Node
-dmapNRM f = nodeMapG' STopDown binderNumCollector (\bi -> fromRecur bi . f bi)
+dmapNRM f = dmapNRM' (0, f)
 
-dmapNM :: Monad m => (Index -> Node -> m Node) -> Node -> m Node
+dmapNM :: Monad m => (Level -> Node -> m Node) -> Node -> m Node
-dmapNM f = nodeMapG' STopDown binderNumCollector (\bi -> fromSimple bi . f bi)
+dmapNM f = dmapNM' (0, f)
 
-umapNM :: Monad m => (Index -> Node -> m Node) -> Node -> m Node
+umapNM :: Monad m => (Level -> Node -> m Node) -> Node -> m Node
 umapNM f = nodeMapG' SBottomUp binderNumCollector f
 
 dmapRM :: Monad m => (Node -> m Recur) -> Node -> m Node
@@ -41,13 +41,13 @@ dmapLM' f = nodeMapG' STopDown (binderInfoCollector' (fst f)) (\bi -> fromSimple
 umapLM' :: Monad m => (BinderList Binder, BinderList Binder -> Node -> m Node) -> Node -> m Node
 umapLM' f = nodeMapG' SBottomUp (binderInfoCollector' (fst f)) (snd f)
 
-dmapNRM' :: Monad m => (Index, Index -> Node -> m Recur) -> Node -> m Node
+dmapNRM' :: Monad m => (Level, Level -> Node -> m Recur) -> Node -> m Node
 dmapNRM' f = nodeMapG' STopDown (binderNumCollector' (fst f)) (\bi -> fromRecur bi . snd f bi)
 
-dmapNM' :: Monad m => (Index, Index -> Node -> m Node) -> Node -> m Node
+dmapNM' :: Monad m => (Level, Level -> Node -> m Node) -> Node -> m Node
 dmapNM' f = nodeMapG' STopDown (binderNumCollector' (fst f)) (\bi -> fromSimple bi . snd f bi)
 
-umapNM' :: Monad m => (Index, Index -> Node -> m Node) -> Node -> m Node
+umapNM' :: Monad m => (Level, Level -> Node -> m Node) -> Node -> m Node
 umapNM' f = nodeMapG' SBottomUp (binderNumCollector' (fst f)) (snd f)
 
 dmapLR :: (BinderList Binder -> Node -> Recur) -> Node -> Node
@@ -59,13 +59,13 @@ dmapL f = runIdentity . dmapLM (embedIden f)
 umapL :: (BinderList Binder -> Node -> Node) -> Node -> Node
 umapL f = runIdentity . umapLM (embedIden f)
 
-dmapNR :: (Index -> Node -> Recur) -> Node -> Node
+dmapNR :: (Level -> Node -> Recur) -> Node -> Node
 dmapNR f = runIdentity . dmapNRM (embedIden f)
 
-dmapN :: (Index -> Node -> Node) -> Node -> Node
+dmapN :: (Level -> Node -> Node) -> Node -> Node
 dmapN f = runIdentity . dmapNM (embedIden f)
 
-umapN :: (Index -> Node -> Node) -> Node -> Node
+umapN :: (Level -> Node -> Node) -> Node -> Node
 umapN f = runIdentity . umapNM (embedIden f)
 
 dmapR :: (Node -> Recur) -> Node -> Node
@@ -86,28 +86,46 @@ dmapL' f = runIdentity . dmapLM' (embedIden f)
 umapL' :: (BinderList Binder, BinderList Binder -> Node -> Node) -> Node -> Node
 umapL' f = runIdentity . umapLM' (embedIden f)
 
-dmapNR' :: (Index, Index -> Node -> Recur) -> Node -> Node
+dmapNR' :: (Level, Level -> Node -> Recur) -> Node -> Node
 dmapNR' f = runIdentity . dmapNRM' (embedIden f)
 
-dmapN' :: (Index, Index -> Node -> Node) -> Node -> Node
+dmapN' :: (Level, Level -> Node -> Node) -> Node -> Node
 dmapN' f = runIdentity . dmapNM' (embedIden f)
 
-umapN' :: (Index, Index -> Node -> Node) -> Node -> Node
+umapN' :: (Level, Level -> Node -> Node) -> Node -> Node
 umapN' f = runIdentity . umapNM' (embedIden f)
 
-dmapCLM :: Monad m => (c -> BinderList Binder -> Node -> m (c, Node)) -> c -> Node -> m Node
+dmapCLM' :: Monad m => (BinderList Binder, c -> BinderList Binder -> Node -> m (c, Node)) -> c -> Node -> m Node
-dmapCLM f ini = nodeMapG' STopDown (pairCollector (identityCollector ini) binderInfoCollector) (\(c, bi) -> fromPair bi . f c bi)
+dmapCLM' f ini = nodeMapG' STopDown (pairCollector (identityCollector ini) (binderInfoCollector' (fst f))) (\(c, bi) -> fromPair bi . snd f c bi)
 
-dmapCNM :: Monad m => (c -> Index -> Node -> m (c, Node)) -> c -> Node -> m Node
+dmapCLRM' :: Monad m => (BinderList Binder, c -> BinderList Binder -> Node -> m (Recur' c)) -> c -> Node -> m Node
+dmapCLRM' f ini = nodeMapG' STopDown (pairCollector (identityCollector ini) (binderInfoCollector' (fst f))) (\(c, bi) -> fromRecur' bi . snd f c bi)
+
+dmapCNRM' :: Monad m => (Level, c -> Level -> Node -> m (Recur' c)) -> c -> Node -> m Node
+dmapCNRM' f ini = nodeMapG' STopDown (pairCollector (identityCollector ini) (binderNumCollector' (fst f))) (\(c, bi) -> fromRecur' bi . snd f c bi)
+
+dmapCLM :: Monad m => (c -> BinderList Binder -> Node -> m (c, Node)) -> c -> Node -> m Node
+dmapCLM f = dmapCLM' (mempty, f)
+
+dmapCNM :: Monad m => (c -> Level -> Node -> m (c, Node)) -> c -> Node -> m Node
 dmapCNM f ini = nodeMapG' STopDown (pairCollector (identityCollector ini) binderNumCollector) (\(c, bi) -> fromPair bi . f c bi)
 
 dmapCM :: Monad m => (c -> Node -> m (c, Node)) -> c -> Node -> m Node
 dmapCM f ini = nodeMapG' STopDown (identityCollector ini) (\c -> fmap Recur' . f c)
 
+dmapCL' :: (BinderList Binder, c -> BinderList Binder -> Node -> (c, Node)) -> c -> Node -> Node
+dmapCL' f ini = runIdentity . dmapCLM' (embedIden f) ini
+
+dmapCLR' :: (BinderList Binder, c -> BinderList Binder -> Node -> Recur' c) -> c -> Node -> Node
+dmapCLR' f ini = runIdentity . dmapCLRM' (embedIden f) ini
+
+dmapCNR' :: (Level, c -> Level -> Node -> Recur' c) -> c -> Node -> Node
+dmapCNR' f ini = runIdentity . dmapCNRM' (embedIden f) ini
+
 dmapCL :: (c -> BinderList Binder -> Node -> (c, Node)) -> c -> Node -> Node
 dmapCL f ini = runIdentity . dmapCLM (embedIden f) ini
 
-dmapCN :: (c -> Index -> Node -> (c, Node)) -> c -> Node -> Node
+dmapCN :: (c -> Level -> Node -> (c, Node)) -> c -> Node -> Node
 dmapCN f ini = runIdentity . dmapCNM (embedIden f) ini
 
 dmapC :: (c -> Node -> (c, Node)) -> c -> Node -> Node

src/Juvix/Compiler/Core/Extra/Stripped/Base.hs

@@ -52,5 +52,5 @@ mkLet i v b = NLet (Let i item b)
 mkLet' :: Node -> Node -> Node
 mkLet' = mkLet (LetInfo "" Nothing TyDynamic)
 
-mkCase :: CaseInfo -> Node -> [CaseBranch] -> Maybe Node -> Node
+mkCase :: CaseInfo -> Symbol -> Node -> [CaseBranch] -> Maybe Node -> Node
-mkCase ci v bs def = NCase (Case ci v bs def)
+mkCase ci sym v bs def = NCase (Case ci sym v bs def)

src/Juvix/Compiler/Core/Keywords.hs

@@ -10,6 +10,7 @@ import Juvix.Data.Keyword.All
   ( kwAny,
     kwAssign,
     kwBind,
+    kwBuiltin,
     kwCase,
     kwColon,
     kwComma,
@@ -52,6 +53,7 @@ allKeywordStrings = keywordsStrings allKeywords
 allKeywords :: [Keyword]
 allKeywords =
   [ kwAssign,
+    kwBuiltin,
     kwLet,
     kwLetRec,
     kwIn,

src/Juvix/Compiler/Core/Language/Nodes.hs

@@ -114,6 +114,7 @@ data LetRec' i a ty = LetRec
 -- branches default`. `Case` is lazy: only the selected branch is evaluated.
 data Case' i bi a = Case
   { _caseInfo :: i,
+    _caseInductive :: Symbol,
     _caseValue :: !a,
     _caseBranches :: ![CaseBranch' bi a],
     _caseDefault :: !(Maybe a)
@@ -338,7 +339,7 @@ instance Eq a => Eq (Constr' i a) where
   (Constr _ tag1 args1) == (Constr _ tag2 args2) = tag1 == tag2 && args1 == args2
 
 instance Eq a => Eq (Case' i bi a) where
-  (Case _ v1 bs1 def1) == (Case _ v2 bs2 def2) = v1 == v2 && bs1 == bs2 && def1 == def2
+  (Case _ sym1 v1 bs1 def1) == (Case _ sym2 v2 bs2 def2) = sym1 == sym2 && v1 == v2 && bs1 == bs2 && def1 == def2
 
 instance Eq a => Eq (CaseBranch' i a) where
   (==) =

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

@@ -158,7 +158,19 @@ ppCodeLet' name mty lt = do
   return $ kwLet <+> n' <> tty <+> kwAssign <+> v' <+> kwIn <> line <> b'
 
 ppCodeCase' :: (PrettyCode a, Member (Reader Options) r) => [[Text]] -> [Text] -> Case' i bi a -> Sem r (Doc Ann)
-ppCodeCase' branchBinderNames branchTagNames Case {..} = do
+ppCodeCase' branchBinderNames branchTagNames Case {..} =
+  case _caseBranches of
+    [CaseBranch _ (BuiltinTag TagTrue) _ _ br1, CaseBranch _ (BuiltinTag TagTrue) _ _ br2] -> do
+      br1' <- ppCode br1
+      br2' <- ppCode br2
+      v <- ppCode _caseValue
+      return $ kwIf <+> v <+> kwThen <+> br1' <+> kwElse <+> br2'
+    [CaseBranch _ (BuiltinTag TagTrue) _ _ br1] | isJust _caseDefault -> do
+      br1' <- ppCode br1
+      br2' <- ppCode (fromJust _caseDefault)
+      v <- ppCode _caseValue
+      return $ kwIf <+> v <+> kwThen <+> br1' <+> kwElse <+> br2'
+    _ -> do
       let branchBodies = map (^. caseBranchBody) _caseBranches
       bns <- mapM (mapM (ppName KNameLocal)) branchBinderNames
       cns <- mapM (ppName KNameConstructor) branchTagNames
@@ -505,6 +517,15 @@ kwMatch = keyword Str.match_
 kwWith :: Doc Ann
 kwWith = keyword Str.with_
 
+kwIf :: Doc Ann
+kwIf = keyword Str.if_
+
+kwThen :: Doc Ann
+kwThen = keyword Str.then_
+
+kwElse :: Doc Ann
+kwElse = keyword Str.else_
+
 kwDefault :: Doc Ann
 kwDefault = keyword Str.underscore
 

src/Juvix/Compiler/Core/Transformation.hs

@@ -14,6 +14,7 @@ import Juvix.Compiler.Core.Transformation.Eta
 import Juvix.Compiler.Core.Transformation.Identity
 import Juvix.Compiler.Core.Transformation.LambdaLifting
 import Juvix.Compiler.Core.Transformation.MoveApps
+import Juvix.Compiler.Core.Transformation.NatToInt
 import Juvix.Compiler.Core.Transformation.RemoveTypeArgs
 import Juvix.Compiler.Core.Transformation.TopEtaExpand
 
@@ -27,3 +28,4 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
       TopEtaExpand -> topEtaExpand
       RemoveTypeArgs -> removeTypeArgs
       MoveApps -> moveApps
+      NatToInt -> natToInt

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

@@ -57,7 +57,8 @@ lambdaLiftNode aboveBl top =
                 _identifierType = typeFromArgs argsInfo,
                 _identifierArgsNum = length allfreevars,
                 _identifierArgsInfo = argsInfo,
-                _identifierIsExported = False
+                _identifierIsExported = False,
+                _identifierBuiltin = Nothing
               }
           registerIdentNode f fBody'
           let fApp = mkApps' (mkIdent mempty f) (map NVar allfreevars)
@@ -117,7 +118,8 @@ lambdaLiftNode aboveBl top =
                             _identifierType = typeFromArgs argsInfo,
                             _identifierArgsNum = length recItemsFreeVars,
                             _identifierArgsInfo = argsInfo,
-                            _identifierIsExported = False
+                            _identifierIsExported = False,
+                            _identifierBuiltin = Nothing
                           }
                     | (sym, (itemBinder, b)) <- zipExact topSyms (zipExact letRecBinders' liftedDefs)
                   ]

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

@@ -0,0 +1,93 @@
+module Juvix.Compiler.Core.Transformation.NatToInt (natToInt) where
+
+import Data.HashMap.Strict qualified as HashMap
+import Data.List qualified as List
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Info qualified as Info
+import Juvix.Compiler.Core.Info.NameInfo
+import Juvix.Compiler.Core.Transformation.Base
+
+convertNode :: InfoTable -> Node -> Node
+convertNode tab = convert [] 0
+  where
+    convert :: [Level] -> Level -> Node -> Node
+    convert levels bl node = dmapCNR' (bl, go) levels node
+
+    go :: [Level] -> Level -> Node -> Recur' [Level]
+    go levels bl node = case node of
+      NVar (Var {..}) ->
+        End' (mkVar _varInfo (_varIndex + length (filter (\x -> x >= bl - _varIndex) levels)))
+      NApp (App _ (NApp (App _ (NIdt (Ident {..})) l)) r) ->
+        Recur' (levels, convertIdentApp node (\op -> mkBuiltinApp _identInfo op [l, r]) _identSymbol)
+      NApp (App _ (NIdt (Ident {..})) l) ->
+        Recur' (levels, convertIdentApp node (\op -> mkLambdaTy mkTypeInteger' $ mkBuiltinApp _identInfo op [l, mkVar' 0]) _identSymbol)
+      NIdt (Ident {..}) ->
+        Recur'
+          ( levels,
+            convertIdentApp
+              node
+              ( \op ->
+                  mkLambdaTy mkTypeInteger' $
+                    mkLambdaTy mkTypeInteger' $
+                      mkBuiltinApp _identInfo op [mkVar' 1, mkVar' 0]
+              )
+              _identSymbol
+          )
+      NCtr (Constr {..}) ->
+        let ci = fromJust $ HashMap.lookup _constrTag (tab ^. infoConstructors)
+         in case ci ^. constructorBuiltin of
+              Just BuiltinNatZero ->
+                Recur' (levels, mkConstant _constrInfo (ConstInteger 0))
+              Just BuiltinNatSuc ->
+                Recur' (levels, mkBuiltinApp _constrInfo OpIntAdd (_constrArgs ++ [mkConstant' (ConstInteger 1)]))
+              _ -> Recur' (levels, node)
+      NCase (Case {..}) ->
+        let ii = fromJust $ HashMap.lookup _caseInductive (tab ^. infoInductives)
+         in case ii ^. inductiveBuiltin of
+              Just BuiltinNat ->
+                case _caseBranches of
+                  [br] -> makeIf br (maybeBranch _caseDefault)
+                  [br1, br2] ->
+                    if
+                        | br1 ^. caseBranchBindersNum == 1 && br2 ^. caseBranchBindersNum == 0 ->
+                            makeIf br1 (br2 ^. caseBranchBody)
+                        | br2 ^. caseBranchBindersNum == 1 && br1 ^. caseBranchBindersNum == 0 ->
+                            makeIf br2 (br1 ^. caseBranchBody)
+                        | otherwise ->
+                            impossible
+                  [] -> Recur' (levels, fromJust _caseDefault)
+                  _ -> impossible
+              _ -> Recur' (levels, node)
+        where
+          makeIf :: CaseBranch -> Node -> Recur' [Level]
+          makeIf CaseBranch {..} br =
+            let ci = fromJust $ HashMap.lookup (BuiltinTag TagTrue) (tab ^. infoConstructors)
+                sym = ci ^. constructorInductive
+             in case _caseBranchBindersNum of
+                  0 ->
+                    Recur' (levels, mkIf _caseInfo sym (mkBuiltinApp' OpEq [_caseValue, mkConstant' (ConstInteger 0)]) _caseBranchBody br)
+                  1 ->
+                    End' $
+                      mkLet mempty (emptyBinder {_binderName = name}) (mkBuiltinApp' OpIntSub [convert levels bl _caseValue, mkConstant' (ConstInteger 1)]) $
+                        mkIf
+                          _caseInfo
+                          sym
+                          (mkBuiltinApp' OpIntLe [mkConstant' (ConstInteger 0), mkVar (Info.singleton (NameInfo name)) 0])
+                          (convert levels (bl + 1) _caseBranchBody)
+                          (convert (bl : levels) bl br)
+                    where
+                      name = List.head _caseBranchBinders ^. binderName
+                  _ -> impossible
+          maybeBranch :: Maybe Node -> Node
+          maybeBranch = fromMaybe (mkBuiltinApp' OpFail [mkConstant' (ConstString "no matching branch")])
+      _ -> Recur' (levels, node)
+
+    convertIdentApp :: Node -> (BuiltinOp -> Node) -> Symbol -> Node
+    convertIdentApp node f sym =
+      let ii = fromJust $ HashMap.lookup sym (tab ^. infoIdentifiers)
+       in case ii ^. identifierBuiltin of
+            Just BuiltinNatPlus -> f OpIntAdd
+            _ -> node
+
+natToInt :: InfoTable -> InfoTable
+natToInt tab = mapT (const (convertNode tab)) tab

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

@@ -49,7 +49,7 @@ convertNode tab = convert mempty
             args' = filterArgs ty _constrArgs
          in End (mkConstr _constrInfo _constrTag (map (convert vars) args'))
       NCase (Case {..}) ->
-        End (mkCase _caseInfo (convert vars _caseValue) (map convertBranch _caseBranches) (fmap (convert vars) _caseDefault))
+        End (mkCase _caseInfo _caseInductive (convert vars _caseValue) (map convertBranch _caseBranches) (fmap (convert vars) _caseDefault))
         where
           convertBranch :: CaseBranch -> CaseBranch
           convertBranch br@CaseBranch {..} =

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

@@ -121,7 +121,8 @@ goInductiveDef i = do
             _inductiveKind = mkDynamic',
             _inductiveConstructors = ctorInfos,
             _inductiveParams = [],
-            _inductivePositive = i ^. Internal.inductivePositive
+            _inductivePositive = i ^. Internal.inductivePositive,
+            _inductiveBuiltin = i ^. Internal.inductiveBuiltin
           }
   registerInductive (mkIdentIndex (i ^. Internal.inductiveName)) info
 
@@ -132,7 +133,8 @@ goConstructor ::
   Internal.InductiveConstructorDef ->
   Sem r ConstructorInfo
 goConstructor sym ctor = do
-  tag <- mBuiltin >>= ctorTag
+  mblt <- mBuiltin
+  tag <- ctorTag mblt
   ty <- ctorType
   let info =
         ConstructorInfo
@@ -141,7 +143,8 @@ goConstructor sym ctor = do
             _constructorTag = tag,
             _constructorType = ty,
             _constructorArgsNum = length (ctor ^. Internal.inductiveConstructorParameters),
-            _constructorInductive = sym
+            _constructorInductive = sym,
+            _constructorBuiltin = mblt
           }
   registerConstructor (mkIdentIndex (ctor ^. Internal.inductiveConstructorName)) info
   return info
@@ -198,7 +201,8 @@ goFunctionDefIden (f, sym) = do
             _identifierType = funTy,
             _identifierArgsNum = 0,
             _identifierArgsInfo = [],
-            _identifierIsExported = False
+            _identifierIsExported = False,
+            _identifierBuiltin = f ^. Internal.funDefBuiltin
           }
   registerIdent (mkIdentIndex (f ^. Internal.funDefName)) info
   when (f ^. Internal.funDefName . Internal.nameText == Str.main) (registerMain sym)
@@ -286,7 +290,8 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
                 _inductiveKind = mkDynamic',
                 _inductiveConstructors = [],
                 _inductiveParams = [],
-                _inductivePositive = False
+                _inductivePositive = False,
+                _inductiveBuiltin = Nothing
               }
       registerInductive (mkIdentIndex (a ^. Internal.axiomName)) info
 
@@ -307,7 +312,8 @@ goAxiomDef a = case a ^. Internal.axiomBuiltin >>= builtinBody of
               _identifierType = ty,
               _identifierArgsNum = 0,
               _identifierArgsInfo = [],
-              _identifierIsExported = False
+              _identifierIsExported = False,
+              _identifierBuiltin = Nothing
             }
     registerIdent (mkIdentIndex (a ^. Internal.axiomName)) info
     registerIdentNode sym body
@@ -554,9 +560,10 @@ goApplication a = do
       funInfo <- HashMap.lookupDefault impossible n <$> asks (^. Internal.infoFunctions)
       case funInfo ^. Internal.functionInfoDef . Internal.funDefBuiltin of
         Just Internal.BuiltinBoolIf -> do
+          sym <- getBoolSymbol
           as <- exprArgs
           case as of
-            (v : b1 : b2 : xs) -> return (mkApps' (mkIf' v b1 b2) xs)
+            (v : b1 : b2 : xs) -> return (mkApps' (mkIf' sym v b1 b2) xs)
             _ -> error "if must be called with 3 arguments"
         _ -> app
     _ -> app

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

@@ -45,34 +45,36 @@ guardSymbolNotDefined sym err = do
 
 createBuiltinConstr ::
   Symbol ->
-  BuiltinDataTag ->
+  Tag ->
   Text ->
   Type ->
   Interval ->
+  Maybe BuiltinConstructor ->
   Sem r ConstructorInfo
-createBuiltinConstr sym btag nameTxt ty i = do
+createBuiltinConstr sym tag nameTxt ty i cblt = do
-  let n = builtinConstrArgsNum btag
   return $
     ConstructorInfo
       { _constructorName = nameTxt,
         _constructorLocation = Just i,
-        _constructorTag = BuiltinTag btag,
+        _constructorTag = tag,
         _constructorType = ty,
-        _constructorArgsNum = n,
+        _constructorArgsNum = length (typeArgs ty),
-        _constructorInductive = sym
+        _constructorInductive = sym,
+        _constructorBuiltin = cblt
       }
 
 declareInductiveBuiltins ::
   Member InfoTableBuilder r =>
   Text ->
-  [(BuiltinDataTag, Text, Type -> Type)] ->
+  Maybe BuiltinInductive ->
+  [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] ->
   ParsecS r ()
-declareInductiveBuiltins indName ctrs = do
+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) -> createBuiltinConstr sym tag name (fty ty) i) ctrs
+  constrs <- lift $ mapM (\(tag, name, fty, cblt) -> createBuiltinConstr sym tag name (fty ty) i cblt) ctrs
   lift $
     registerInductive
       indName
@@ -83,7 +85,8 @@ declareInductiveBuiltins indName ctrs = do
             _inductiveKind = mkDynamic',
             _inductiveConstructors = constrs,
             _inductivePositive = True,
-            _inductiveParams = []
+            _inductiveParams = [],
+            _inductiveBuiltin = blt
           }
       )
   lift $ mapM_ (\ci -> registerConstructor (ci ^. constructorName) ci) constrs
@@ -92,18 +95,31 @@ declareIOBuiltins :: Member InfoTableBuilder r => ParsecS r ()
 declareIOBuiltins =
   declareInductiveBuiltins
     "IO"
-    [ (TagReturn, "return", mkPi' mkDynamic'),
+    Nothing
-      (TagBind, "bind", \ty -> mkPi' ty (mkPi' (mkPi' mkDynamic' ty) ty)),
+    [ (BuiltinTag TagReturn, "return", mkPi' mkDynamic', Nothing),
-      (TagWrite, "write", mkPi' mkDynamic'),
+      (BuiltinTag TagBind, "bind", \ty -> mkPi' ty (mkPi' (mkPi' mkDynamic' ty) ty), Nothing),
-      (TagReadLn, "readLn", id)
+      (BuiltinTag TagWrite, "write", mkPi' mkDynamic', Nothing),
+      (BuiltinTag TagReadLn, "readLn", id, Nothing)
     ]
 
 declareBoolBuiltins :: Member InfoTableBuilder r => ParsecS r ()
 declareBoolBuiltins =
   declareInductiveBuiltins
     "bool"
-    [ (TagTrue, "true", id),
+    (Just BuiltinBool)
-      (TagFalse, "false", id)
+    [ (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 ::
@@ -112,6 +128,7 @@ parseToplevel ::
 parseToplevel = do
   declareIOBuiltins
   declareBoolBuiltins
+  declareNatBuiltins
   space
   P.endBy statement (kw kwSemicolon)
   r <- optional expression
@@ -121,11 +138,23 @@ parseToplevel = do
 statement ::
   Member InfoTableBuilder r =>
   ParsecS r ()
-statement = statementDef <|> statementInductive
+statement = statementBuiltin <|> void statementDef <|> statementInductive
+
+statementBuiltin ::
+  Member InfoTableBuilder r =>
+  ParsecS r ()
+statementBuiltin = do
+  off <- P.getOffset
+  kw kwBuiltin
+  sym <- statementDef
+  ii <- lift $ getIdentifierInfo sym
+  case ii ^. identifierName of
+    "plus" -> lift $ registerIdent (ii ^. identifierName) ii {_identifierBuiltin = Just BuiltinNatPlus}
+    _ -> parseFailure off "unrecorgnized builtin definition"
 
 statementDef ::
   Member InfoTableBuilder r =>
-  ParsecS r ()
+  ParsecS r Symbol
 statementDef = do
   kw kwDef
   off <- P.getOffset
@@ -140,6 +169,7 @@ statementDef = do
       let fi = fromMaybe impossible $ HashMap.lookup sym (tab ^. infoIdentifiers)
           ty = fi ^. identifierType
       parseDefinition sym ty
+      return sym
     Just IdentInd {} ->
       parseFailure off ("duplicate identifier: " ++ fromText txt)
     Just IdentConstr {} ->
@@ -156,10 +186,12 @@ statementDef = do
                 _identifierType = ty,
                 _identifierArgsNum = 0,
                 _identifierArgsInfo = [],
-                _identifierIsExported = False
+                _identifierIsExported = False,
+                _identifierBuiltin = Nothing
               }
       lift $ registerIdent txt info
       void $ optional (parseDefinition sym ty)
+      return sym
 
 parseDefinition ::
   Member InfoTableBuilder r =>
@@ -208,7 +240,8 @@ statementInductive = do
             _inductiveKind = fromMaybe (mkUniv' 0) mty,
             _inductiveConstructors = [],
             _inductiveParams = [],
-            _inductivePositive = True
+            _inductivePositive = True,
+            _inductiveBuiltin = Nothing
           }
   lift $ registerInductive txt ii
   ctrs <- braces $ P.sepEndBy (constrDecl sym) (kw kwSemicolon)
@@ -233,7 +266,8 @@ constrDecl symInd = do
             _constructorTag = tag,
             _constructorArgsNum = length (typeArgs ty),
             _constructorType = ty,
-            _constructorInductive = symInd
+            _constructorInductive = symInd,
+            _constructorBuiltin = Nothing
           }
   lift $ registerConstructor txt ci
   return ci
@@ -742,11 +776,23 @@ exprCase' off value varsNum vars = do
   bs <- P.sepEndBy (caseBranchP varsNum vars) (kw kwSemicolon)
   let bss = map fromLeft' $ filter isLeft bs
   let def' = map fromRight' $ filter isRight bs
+  case bss of
+    CaseBranch {..} : _ -> do
+      ci <- lift $ getConstructorInfo _caseBranchTag
+      let sym = ci ^. constructorInductive
       case def' of
         [def] ->
-      return $ mkCase' value bss (Just def)
+          return $ mkCase' sym value bss (Just def)
         [] ->
-      return $ mkCase' value bss Nothing
+          return $ mkCase' sym value bss Nothing
+        _ ->
+          parseFailure off "multiple default branches"
+    [] ->
+      case def' of
+        [_] ->
+          parseFailure off "case with only the default branch not allowed"
+        [] ->
+          parseFailure off "case without branches not allowed"
         _ ->
           parseFailure off "multiple default branches"
 
@@ -818,7 +864,8 @@ exprIf varsNum vars = do
   br1 <- bracedExpr varsNum vars
   kw kwElse
   br2 <- bracedExpr varsNum vars
-  return $ mkIf Info.empty value br1 br2
+  sym <- lift getBoolSymbol
+  return $ mkIf mempty sym value br1 br2
 
 exprMatch ::
   Member InfoTableBuilder r =>

test/Core/Eval/Positive.hs

@@ -259,5 +259,10 @@ tests =
       "Applications with lets and cases in function position"
       "."
       "test046.jvc"
-      "out/test046.out"
+      "out/test046.out",
+    PosTest
+      "Builtin natural numbers"
+      "."
+      "test047.jvc"
+      "out/test047.out"
   ]

test/Core/Transformation.hs

@@ -3,7 +3,7 @@ module Core.Transformation where
 import Base
 import Core.Transformation.Identity qualified as Identity
 import Core.Transformation.Lifting qualified as Lifting
-import Core.Transformation.RemoveTypeArgs qualified as RemoveTypeArgs
+import Core.Transformation.Pipeline qualified as Pipeline
 import Core.Transformation.TopEtaExpand qualified as TopEtaExpand
 
 allTests :: TestTree
@@ -13,5 +13,5 @@ allTests =
     [ Identity.allTests,
       TopEtaExpand.allTests,
       Lifting.allTests,
-      RemoveTypeArgs.allTests
+      Pipeline.allTests
     ]

test/Core/Transformation/Pipeline.hs

@@ -1,4 +1,4 @@
-module Core.Transformation.RemoveTypeArgs (allTests) where
+module Core.Transformation.Pipeline (allTests) where
 
 import Base
 import Core.Eval.Positive qualified as Eval
@@ -6,10 +6,10 @@ import Core.Transformation.Base
 import Juvix.Compiler.Core.Transformation
 
 allTests :: TestTree
-allTests = testGroup "Move applications and remove type arguments" (map liftTest Eval.tests)
+allTests = testGroup "Transformation pipeline" (map liftTest Eval.tests)
 
 pipe :: [TransformationId]
-pipe = [LambdaLifting, MoveApps, RemoveTypeArgs]
+pipe = [NatToInt, LambdaLifting, MoveApps, RemoveTypeArgs, TopEtaExpand]
 
 liftTest :: Eval.PosTest -> TestTree
 liftTest _testEval =

tests/Core/positive/out/test047.out

@@ -0,0 +1,3 @@
+3
+136
+true

tests/Core/positive/test029.jvc

@@ -9,11 +9,11 @@ def snd := \p case p of { pair _ x := x };
 
 def compose := \f \g \x f (g x);
 
-def zero := \f \x x;
+def czero := \f \x x;
 
 def num := \n
   if n = 0 then
-    zero
+    czero
   else
     \f compose f (num (n - 1) f);
 
@@ -32,7 +32,7 @@ def pred := \n
           pair (fst x) (succ (snd x))
         else
           pair (succ (fst x)) (succ (snd x)))
-      (pair zero zero)
+      (pair czero czero)
   );
 
 def toInt := \n n (+ 1) 0;
@@ -41,11 +41,11 @@ def writeLn := \x write x >> write "\n";
 
 def fib := \n
   if isZero n then
-    zero
+    czero
   else
     let n' := pred n in
     if isZero n' then
-      succ zero
+      succ czero
     else
       add (fib n') (fib (pred n'));
 

tests/Core/positive/test046.jvc

@@ -5,7 +5,7 @@ inductive list {
   cons : any -> list -> list;
 };
 
-def f := \l (case l of { cons x _ := x; nil := \x x } ) (let y := \x x in (let z := \x x in case l of { _ := \x x } z) y) 7;
+def f := \l (case l of { cons x _ := x; nil := \x x } ) (let y := \x x in (let z := \x x in case l of { cons _ _ := \x x } z) y) 7;
 
 def main := f (cons (\x \y x y + 2) nil);
 

tests/Core/positive/test047.jvc

@@ -0,0 +1,38 @@
+-- builtin natural numbers
+
+builtin def plus := \x \y case x of {
+  zero := y;
+  suc x' := suc (plus x' y);
+};
+
+def from_int := \n if n = 0 then zero else suc (from_int (n - 1));
+
+def to_int := \x case x of {
+  suc x' := to_int x' + 1;
+  zero := 0;
+};
+
+def even := \x case x of {
+  suc x' := case x' of {
+    zero := false;
+    suc y := even y;
+  };
+  _ := true;
+};
+
+def f := \x case x of {
+  suc x' := (\z case z of {
+    zero := even x';
+    suc y := f y;
+  }) x';
+  _ := even x;
+};
+
+def writeLn := \x write x >> write "\n";
+
+def main :=
+  writeLn (to_int (if even (from_int 124) then plus (suc zero) (suc (suc zero)) else zero)) >>
+  writeLn (to_int (plus (from_int 126) (from_int 10))) >>
+  writeLn (f (from_int 65));
+
+main