fix translation to stripped

anoma · Jun 30, 2023 · 062a321 · 062a321
1 parent 87f4297
commit 062a321
Show file tree

Hide file tree

Showing 3 changed files with 71 additions and 11 deletions.
diff --git a/src/Juvix/Compiler/Asm/Translation/FromCore.hs b/src/Juvix/Compiler/Asm/Translation/FromCore.hs
@@ -19,9 +19,9 @@ fromCore :: Core.InfoTable -> InfoTable
 fromCore tab =
   InfoTable
     { _infoMainFunction = tab ^. Core.infoMain,
-      _infoFunctions = fmap (genCode tab) (tab ^. Core.infoFunctions),
-      _infoInductives = fmap translateInductiveInfo (tab ^. Core.infoInductives),
-      _infoConstrs = fmap translateConstructorInfo (tab ^. Core.infoConstructors)
+      _infoFunctions = genCode tab <$> tab ^. Core.infoFunctions,
+      _infoInductives = translateInductiveInfo <$> tab ^. Core.infoInductives,
+      _infoConstrs = translateConstructorInfo <$> tab ^. Core.infoConstructors
     }
 
 -- Generate code for a single function.

diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@@ -138,7 +138,7 @@ preInductiveDef i = do
             _inductiveConstructors = [],
             _inductiveParams = params,
             _inductivePositive = i ^. Internal.inductivePositive,
-            _inductiveBuiltin = fmap BuiltinTypeInductive (i ^. Internal.inductiveBuiltin),
+            _inductiveBuiltin = BuiltinTypeInductive <$> i ^. Internal.inductiveBuiltin,
             _inductivePragmas = i ^. Internal.inductivePragmas,
             _inductiveName
           }
@@ -163,7 +163,8 @@ goInductiveDef PreInductiveDef {..} = do
       idx = mkIdentIndex (i ^. Internal.inductiveName)
       sym = info ^. inductiveSymbol
   ctorInfos <- mapM (goConstructor sym) (i ^. Internal.inductiveConstructors)
-  registerInductive idx info {_inductiveConstructors = map (^. constructorTag) ctorInfos}
+  let ctorTags = map (^. constructorTag) ctorInfos
+  registerInductive idx (set inductiveConstructors ctorTags info)
 
 goConstructor ::
   forall r.

diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
@@ -20,13 +20,72 @@ fromCore tab =
   where
     tab' =
       tab
-        { _infoIdentifiers = HashMap.filter (\ii -> isNothing (ii ^. identifierBuiltin)) (tab ^. infoIdentifiers),
-          _infoInductives = HashMap.filter (\ii -> isNothing (ii ^. inductiveBuiltin) || isIO (ii ^. inductiveBuiltin)) (tab ^. infoInductives),
-          _infoConstructors = HashMap.filter (\ci -> isNothing (ci ^. constructorBuiltin)) (tab ^. infoConstructors)
+        { _infoIdentifiers = HashMap.filter (maybe True shouldKeepFunction . (^. identifierBuiltin)) (tab ^. infoIdentifiers),
+          _infoInductives = HashMap.filter (maybe True shouldKeepType . (^. inductiveBuiltin)) (tab ^. infoInductives),
+          _infoConstructors = HashMap.filter (maybe True shouldKeepConstructor . (^. constructorBuiltin)) (tab ^. infoConstructors)
         }
-    isIO :: Maybe BuiltinType -> Bool
-    isIO (Just (BuiltinTypeAxiom BuiltinIO)) = True
-    isIO _ = False
+    shouldKeepFunction :: BuiltinFunction -> Bool
+    shouldKeepFunction = \case
+      BuiltinNatPlus -> False
+      BuiltinNatSub -> False
+      BuiltinNatMul -> False
+      BuiltinNatUDiv -> False
+      BuiltinNatDiv -> False
+      BuiltinNatMod -> False
+      BuiltinNatLe -> False
+      BuiltinNatLt -> False
+      BuiltinNatEq -> False
+      BuiltinBoolIf -> False
+      BuiltinBoolOr -> False
+      BuiltinBoolAnd -> False
+      BuiltinIntEq -> False
+      BuiltinIntPlus -> False
+      BuiltinIntSubNat -> False
+      BuiltinIntNegNat -> False
+      BuiltinIntNeg -> False
+      BuiltinIntMul -> False
+      BuiltinIntDiv -> False
+      BuiltinIntMod -> False
+      BuiltinIntSub -> False
+      BuiltinIntNonNeg -> False
+      BuiltinIntLe -> False
+      BuiltinIntLt -> False
+      BuiltinSeq -> False
+
+    shouldKeepConstructor :: BuiltinConstructor -> Bool
+    shouldKeepConstructor = \case
+      BuiltinListNil -> True
+      BuiltinListCons -> True
+      BuiltinNatZero -> False
+      BuiltinNatSuc -> False
+      BuiltinBoolTrue -> False
+      BuiltinBoolFalse -> False
+      BuiltinIntOfNat -> False
+      BuiltinIntNegSuc -> False
+
+    shouldKeepType :: BuiltinType -> Bool
+    shouldKeepType = \case
+      BuiltinTypeAxiom a -> case a of
+        BuiltinIO -> True
+        BuiltinNatPrint -> False
+        BuiltinNatToString -> False
+        BuiltinStringPrint -> False
+        BuiltinStringConcat -> False
+        BuiltinStringEq -> False
+        BuiltinStringToNat -> False
+        BuiltinBoolPrint -> False
+        BuiltinString -> False
+        BuiltinIOSequence -> False
+        BuiltinIOReadline -> False
+        BuiltinTrace -> False
+        BuiltinFail -> False
+        BuiltinIntToString -> False
+        BuiltinIntPrint -> False
+      BuiltinTypeInductive i -> case i of
+        BuiltinList -> True
+        BuiltinNat -> False
+        BuiltinInt -> False
+        BuiltinBool -> False
 
 translateFunctionInfo :: InfoTable -> IdentifierInfo -> Stripped.FunctionInfo
 translateFunctionInfo tab IdentifierInfo {..} =