Fix bug with unregistered builtin bool

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

@@ -23,49 +23,6 @@ import Juvix.Extra.Strings qualified as Str
 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 = freshIdentName tab "intToNat",
-          _identifierLocation = Nothing,
-          _identifierArgsNum = 1,
-          _identifierArgsInfo =
-            [ ArgumentInfo
-                { _argumentName = "x",
-                  _argumentLocation = Nothing,
-                  _argumentType = mkTypePrim' (PrimInteger $ PrimIntegerInfo Nothing Nothing),
-                  _argumentIsImplicit = Explicit
-                }
-            ],
-          _identifierType = mkPi' mkTypeInteger' targetType,
-          _identifierIsExported = False,
-          _identifierBuiltin = Nothing
-        }
-    node =
-      case (tagZeroM, tagSucM, boolSymM) of
-        (Just tagZero, Just tagSuc, Just boolSym) ->
-          mkLambda' mkTypeInteger' $
-            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' mkTypeInteger' $ mkVar' 0
-    targetType = maybe mkTypeInteger' (\s -> mkTypeConstr (setInfoName "Nat" mempty) s []) natSymM
-    tagZeroM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatZero
-    tagSucM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatSuc
-    boolSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinBool
-    natSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinNat
-
 fromInternal :: Internal.InternalTypedResult -> Sem k CoreResult
 fromInternal i = do
   (res, _) <- runInfoTableBuilder tab0 (evalState (i ^. InternalTyped.resultFunctions) (runReader (i ^. InternalTyped.resultIdenTypes) f))
@@ -85,6 +42,53 @@ fromInternal i = do
     f = do
       let resultModules = toList (i ^. InternalTyped.resultModules)
       runReader (Internal.buildTable resultModules) (mapM_ goModule resultModules)
+      tab <- getInfoTable
+      when
+        (isNothing (lookupBuiltinInductive tab BuiltinBool))
+        declareBoolBuiltins
+
+    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 = freshIdentName tab "intToNat",
+              _identifierLocation = Nothing,
+              _identifierArgsNum = 1,
+              _identifierArgsInfo =
+                [ ArgumentInfo
+                    { _argumentName = "x",
+                      _argumentLocation = Nothing,
+                      _argumentType = mkTypePrim' (PrimInteger $ PrimIntegerInfo Nothing Nothing),
+                      _argumentIsImplicit = Explicit
+                    }
+                ],
+              _identifierType = mkPi' mkTypeInteger' targetType,
+              _identifierIsExported = False,
+              _identifierBuiltin = Nothing
+            }
+        node =
+          case (tagZeroM, tagSucM, boolSymM) of
+            (Just tagZero, Just tagSuc, Just boolSym) ->
+              mkLambda' mkTypeInteger' $
+                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' mkTypeInteger' $ mkVar' 0
+        targetType = maybe mkTypeInteger' (\s -> mkTypeConstr (setInfoName "Nat" mempty) s []) natSymM
+        tagZeroM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatZero
+        tagSucM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatSuc
+        boolSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinBool
+        natSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinNat
 
 fromInternalExpression :: CoreResult -> Internal.Expression -> Sem r Node
 fromInternalExpression res exp = do

test/Compilation/Positive.hs

@@ -279,5 +279,10 @@ tests =
       $(mkRelDir ".")
       $(mkRelFile "test044.juvix")
       $(mkRelFile "out/test044.out")
-      "a\n"
+      "a\n",
+    posTest
+      "Implicit builtin bool"
+      $(mkRelDir ".")
+      $(mkRelFile "test045.juvix")
+      $(mkRelFile "out/test045.out")
   ]

tests/Compilation/positive/out/test045.out

@@ -0,0 +1 @@
+4

tests/Compilation/positive/test045.juvix

@@ -0,0 +1,16 @@
+-- implicit builtin bool
+-- Builtin nat requires builtin bool when translated to integers, because 
+-- matching is translated to comparison operators and cases on booleans.
+module test045;
+  builtin nat type Nat :=
+    | zero : Nat
+    | suc : Nat → Nat;
+
+  infixl 6 +;
+  + : Nat → Nat → Nat;
+  + zero b := b;
+  + (suc a) b := suc (a + b);
+
+  main : Nat;
+  main := 1 + 3;
+end;