Track builtins in the Core InfoTable (#1782)

This PR adds a new field `infoBuiltins : HashMap BuiltinPrim IdentKind`
to the Core InfoTable. This is used to register builtin inductive,
constructors and functions against their corresponding Core
symbols/tags.

The point of doing this is to make it easier to lookup the Infos for
builtins during the internal to core translation:
https://github.com/anoma/juvix/blob/d91241a685fae5e31cd5594653545664c23b768c/src/Juvix/Compiler/Core/Translation/FromInternal.hs#L65

This is one proposed approach, I think Jan mentioned using the Builtins
effect for this but it doesn't seem appropriate to expose the
registration function from the Builtins effect at this part of the code.
Perhaps I misunderstood, if so I'm happy to revisit this refactor.

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

@@ -4,6 +4,7 @@ module Juvix.Compiler.Core.Data.InfoTable
   )
 where
 
+import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Concrete.Data.Builtins
 import Juvix.Compiler.Core.Language
 
@@ -20,7 +21,8 @@ data InfoTable = InfoTable
     _infoAxioms :: HashMap Text AxiomInfo,
     _infoIntToNat :: Maybe Symbol,
     _infoNextSymbol :: Word,
-    _infoNextTag :: Word
+    _infoNextTag :: Word,
+    _infoBuiltins :: HashMap BuiltinPrim IdentKind
   }
 
 emptyInfoTable :: InfoTable
@@ -35,7 +37,8 @@ emptyInfoTable =
       _infoAxioms = mempty,
       _infoIntToNat = Nothing,
       _infoNextSymbol = 1,
-      _infoNextTag = 0
+      _infoNextTag = 0,
+      _infoBuiltins = mempty
     }
 
 data IdentKind
@@ -102,3 +105,36 @@ makeLenses ''InductiveInfo
 makeLenses ''ConstructorInfo
 makeLenses ''ParameterInfo
 makeLenses ''AxiomInfo
+
+lookupBuiltinInductive :: InfoTable -> BuiltinInductive -> Maybe InductiveInfo
+lookupBuiltinInductive tab b = (HashMap.!) (tab ^. infoInductives) . indSym <$> idenKind
+  where
+    idenKind :: Maybe IdentKind
+    idenKind = HashMap.lookup (BuiltinsInductive b) (tab ^. infoBuiltins)
+
+    indSym :: IdentKind -> Symbol
+    indSym = \case
+      IdentInd s -> s
+      _ -> error "core infotable: expected inductive identifier"
+
+lookupBuiltinConstructor :: InfoTable -> BuiltinConstructor -> Maybe ConstructorInfo
+lookupBuiltinConstructor tab b = (HashMap.!) (tab ^. infoConstructors) . ctorTag <$> idenKind
+  where
+    idenKind :: Maybe IdentKind
+    idenKind = HashMap.lookup (BuiltinsConstructor b) (tab ^. infoBuiltins)
+
+    ctorTag :: IdentKind -> Tag
+    ctorTag = \case
+      IdentConstr t -> t
+      _ -> error "core infotable: expected constructor identifier"
+
+lookupBuiltinFunction :: InfoTable -> BuiltinFunction -> Maybe IdentifierInfo
+lookupBuiltinFunction tab b = (HashMap.!) (tab ^. infoIdentifiers) . funSym <$> idenKind
+  where
+    idenKind :: Maybe IdentKind
+    idenKind = HashMap.lookup (BuiltinsFunction b) (tab ^. infoBuiltins)
+
+    funSym :: IdentKind -> Symbol
+    funSym = \case
+      IdentFun s -> s
+      _ -> error "core infotable: expected function identifier"

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

@@ -63,14 +63,29 @@ runInfoTableBuilder tab =
         modify' (over infoNextTag (+ 1))
         return (UserTag (s ^. infoNextTag))
       RegisterIdent idt ii -> do
-        modify' (over infoIdentifiers (HashMap.insert (ii ^. identifierSymbol) ii))
-        modify' (over identMap (HashMap.insert idt (IdentFun (ii ^. identifierSymbol))))
+        let sym = ii ^. identifierSymbol
+        let identKind = IdentFun (ii ^. identifierSymbol)
+        whenJust
+          (ii ^. identifierBuiltin)
+          (\b -> modify' (over infoBuiltins (HashMap.insert (BuiltinsFunction b) identKind)))
+        modify' (over infoIdentifiers (HashMap.insert sym ii))
+        modify' (over identMap (HashMap.insert idt identKind))
       RegisterConstructor idt ci -> do
-        modify' (over infoConstructors (HashMap.insert (ci ^. constructorTag) ci))
-        modify' (over identMap (HashMap.insert idt (IdentConstr (ci ^. constructorTag))))
+        let tag = ci ^. constructorTag
+        let identKind = IdentConstr tag
+        whenJust
+          (ci ^. constructorBuiltin)
+          (\b -> modify' (over infoBuiltins (HashMap.insert (BuiltinsConstructor b) identKind)))
+        modify' (over infoConstructors (HashMap.insert tag ci))
+        modify' (over identMap (HashMap.insert idt identKind))
       RegisterInductive idt ii -> do
-        modify' (over infoInductives (HashMap.insert (ii ^. inductiveSymbol) ii))
-        modify' (over identMap (HashMap.insert idt (IdentInd (ii ^. inductiveSymbol))))
+        let sym = ii ^. inductiveSymbol
+        let identKind = IdentInd sym
+        whenJust
+          (ii ^. inductiveBuiltin)
+          (\b -> modify' (over infoBuiltins (HashMap.insert (BuiltinsInductive b) identKind)))
+        modify' (over infoInductives (HashMap.insert sym ii))
+        modify' (over identMap (HashMap.insert idt identKind))
       RegisterIdentNode sym node ->
         modify' (over identContext (HashMap.insert sym node))
       RegisterMain sym -> do

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

@@ -62,9 +62,9 @@ setupIntToNat sym tab =
               (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)
+    tagZeroM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatZero
+    tagSucM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatSuc
+    boolSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinBool
 
 fromInternal :: Internal.InternalTypedResult -> Sem k CoreResult
 fromInternal i = do