refactor toStripped pipeline

app/Commands/Dev/Core/Compile/Base.hs

@@ -9,6 +9,7 @@ import Juvix.Compiler.Backend.C qualified as C
 import Juvix.Compiler.Backend.Geb qualified as Geb
 import Juvix.Compiler.Backend.VampIR.Translation qualified as VampIR
 import Juvix.Compiler.Core.Data.Module qualified as Core
+import Juvix.Compiler.Core.Data.TransformationId qualified as Core
 import Juvix.Compiler.Nockma.Pretty qualified as Nockma
 import Juvix.Compiler.Reg.Pretty qualified as Reg
 import Juvix.Compiler.Tree.Pretty qualified as Tree
@@ -136,7 +137,7 @@ runTreePipeline pa@PipelineArg {..} = do
   r <-
     runReader entryPoint
       . runError @JuvixError
-      . coreToTree
+      . coreToTree Core.Identity
       $ _pipelineArgModule
   tab' <- getRight r
   let code = Tree.ppPrint tab' tab'

app/Commands/Dev/Core/Strip.hs

@@ -15,7 +15,7 @@ runCommand opts = do
   let r =
         run $
           runReader (project gopts) $
-            runError @JuvixError (Core.toStripped' (Core.moduleFromInfoTable tab) :: Sem '[Error JuvixError, Reader Core.CoreOptions] Core.Module)
+            runError @JuvixError (Core.toStripped' Core.Identity (Core.moduleFromInfoTable tab) :: Sem '[Error JuvixError, Reader Core.CoreOptions] Core.Module)
   tab' <- getRight $ mapLeft JuvixError $ mapRight (Stripped.fromCore . Core.computeCombinedInfoTable) r
   unless (project opts ^. coreStripNoPrint) $ do
     renderStdOut (Core.ppOut opts tab')

src/Juvix/Compiler/Core/Data.hs

@@ -2,9 +2,11 @@ module Juvix.Compiler.Core.Data
   ( module Juvix.Compiler.Core.Data.InfoTable,
     module Juvix.Compiler.Core.Data.InfoTableBuilder,
     module Juvix.Compiler.Core.Data.Module,
+    module Juvix.Compiler.Core.Data.TransformationId,
   )
 where
 
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Data.InfoTableBuilder
 import Juvix.Compiler.Core.Data.Module
+import Juvix.Compiler.Core.Data.TransformationId

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

@@ -24,6 +24,7 @@ data TransformationId
   | CheckGeb
   | CheckExec
   | CheckVampIR
+  | CheckAnoma
   | Normalize
   | LetFolding
   | LambdaFolding
@@ -51,6 +52,7 @@ data PipelineId
   | PipelineGeb
   | PipelineVampIR
   | PipelineStripped
+  | PipelineExec
   deriving stock (Data, Bounded, Enum)
 
 type TransformationLikeId = TransformationLikeId' TransformationId PipelineId
@@ -67,12 +69,9 @@ toNormalizeTransformations = [CombineInfoTables, LetRecLifting, LetFolding, Unro
 toVampIRTransformations :: [TransformationId]
 toVampIRTransformations = [CombineInfoTables, FilterUnreachable, CheckVampIR, LetRecLifting, OptPhaseVampIR, UnrollRecursion, Normalize, LetHoisting]
 
-toStrippedTransformations :: [TransformationId]
-toStrippedTransformations =
-  [CombineInfoTables, FilterUnreachable, LambdaLetRecLifting, TopEtaExpand, OptPhaseExec, MoveApps, RemoveTypeArgs]
-
-toExecTransformations :: [TransformationId]
-toExecTransformations = [CheckExec]
+toStrippedTransformations :: TransformationId -> [TransformationId]
+toStrippedTransformations checkId =
+  [CombineInfoTables, FilterUnreachable, checkId, LambdaLetRecLifting, TopEtaExpand, OptPhaseExec, MoveApps, RemoveTypeArgs]
 
 toGebTransformations :: [TransformationId]
 toGebTransformations = [CombineInfoTables, FilterUnreachable, CheckGeb, LetRecLifting, OptPhaseGeb, UnrollRecursion, FoldTypeSynonyms, ComputeTypeInfo]
@@ -99,6 +98,7 @@ instance TransformationId' TransformationId where
     CheckGeb -> strCheckGeb
     CheckExec -> strCheckExec
     CheckVampIR -> strCheckVampIR
+    CheckAnoma -> strCheckAnoma
     Normalize -> strNormalize
     LetFolding -> strLetFolding
     LambdaFolding -> strLambdaFolding
@@ -127,11 +127,13 @@ instance PipelineId' TransformationId PipelineId where
     PipelineGeb -> strGebPipeline
     PipelineVampIR -> strVampIRPipeline
     PipelineStripped -> strStrippedPipeline
+    PipelineExec -> strExecPipeline
 
   pipeline :: PipelineId -> [TransformationId]
   pipeline = \case
     PipelineStored -> toStoredTransformations
     PipelineNormalize -> toNormalizeTransformations
     PipelineGeb -> toGebTransformations
     PipelineVampIR -> toVampIRTransformations
-    PipelineStripped -> toStrippedTransformations
+    PipelineStripped -> toStrippedTransformations Identity
+    PipelineExec -> toStrippedTransformations CheckExec

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

@@ -20,6 +20,9 @@ strVampIRPipeline = "pipeline-vampir"
 strStrippedPipeline :: Text
 strStrippedPipeline = "pipeline-stripped"
 
+strExecPipeline :: Text
+strExecPipeline = "pipeline-exec"
+
 strLifting :: Text
 strLifting = "lifting"
 
@@ -77,6 +80,9 @@ strCheckExec = "check-exec"
 strCheckVampIR :: Text
 strCheckVampIR = "check-vampir"
 
+strCheckAnoma :: Text
+strCheckAnoma = "check-anoma"
+
 strNormalize :: Text
 strNormalize = "normalize"
 

src/Juvix/Compiler/Core/Pipeline.hs

@@ -21,19 +21,11 @@ toStored = mapReader fromEntryPoint . applyTransformations toStoredTransformatio
 
 -- | Perform transformations on stored Core necessary before the translation to
 -- Core.Stripped
-toStripped' :: (Members '[Error JuvixError, Reader CoreOptions] r) => Module -> Sem r Module
-toStripped' = applyTransformations toStrippedTransformations
+toStripped' :: (Members '[Error JuvixError, Reader CoreOptions] r) => TransformationId -> Module -> Sem r Module
+toStripped' checkId = applyTransformations (toStrippedTransformations checkId)
 
-toStripped :: (Members '[Error JuvixError, Reader EntryPoint] r) => Module -> Sem r Module
-toStripped = mapReader fromEntryPoint . applyTransformations toStrippedTransformations
-
--- | Perform transformations on stored Core necessary before translation to
--- Core.Stripped of programs intended to be executable
-toExec' :: (Members '[Error JuvixError, Reader CoreOptions] r) => Module -> Sem r Module
-toExec' = applyTransformations toExecTransformations
-
-toExec :: (Members '[Error JuvixError, Reader EntryPoint] r) => Module -> Sem r Module
-toExec = mapReader fromEntryPoint . toExec'
+toStripped :: (Members '[Error JuvixError, Reader EntryPoint] r) => TransformationId -> Module -> Sem r Module
+toStripped checkId = mapReader fromEntryPoint . applyTransformations (toStrippedTransformations checkId)
 
 -- | Perform transformations on stored Core necessary before the translation to GEB
 toGeb' :: (Members '[Error JuvixError, Reader CoreOptions] r) => Module -> Sem r Module

src/Juvix/Compiler/Core/Transformation.hs

@@ -13,6 +13,7 @@ import Juvix.Compiler.Core.Data.TransformationId
 import Juvix.Compiler.Core.Error
 import Juvix.Compiler.Core.Options
 import Juvix.Compiler.Core.Transformation.Base
+import Juvix.Compiler.Core.Transformation.Check.Anoma
 import Juvix.Compiler.Core.Transformation.Check.Exec
 import Juvix.Compiler.Core.Transformation.Check.Geb
 import Juvix.Compiler.Core.Transformation.Check.VampIR
@@ -75,6 +76,7 @@ applyTransformations ts tbl = foldM (flip appTrans) tbl ts
       CheckGeb -> mapError (JuvixError @CoreError) . checkGeb
       CheckExec -> mapError (JuvixError @CoreError) . checkExec
       CheckVampIR -> mapError (JuvixError @CoreError) . checkVampIR
+      CheckAnoma -> mapError (JuvixError @CoreError) . checkAnoma
       Normalize -> return . normalize
       LetFolding -> return . letFolding
       LambdaFolding -> return . lambdaFolding

src/Juvix/Compiler/Core/Transformation/Check/Anoma.hs

@@ -0,0 +1,13 @@
+module Juvix.Compiler.Core.Transformation.Check.Anoma where
+
+import Juvix.Compiler.Core.Error
+import Juvix.Compiler.Core.Extra
+import Juvix.Compiler.Core.Transformation.Base
+import Juvix.Compiler.Core.Transformation.Check.Base
+
+checkAnoma :: forall r. (Member (Error CoreError) r) => Module -> Sem r Module
+checkAnoma md =
+  checkMainExists md
+    >> checkNoAxioms md
+    >> mapAllNodesM checkNoIO md
+    >> mapAllNodesM (checkBuiltins' [OpStrConcat, OpStrToInt, OpShow] [PrimString]) md

src/Juvix/Compiler/Core/Transformation/Check/Base.hs

@@ -70,6 +70,22 @@ checkBuiltins allowUntypedFail = dmapRM go
           _ -> return $ Recur node
       _ -> return $ Recur node
 
+checkBuiltins' :: forall r. (Member (Error CoreError) r) => [BuiltinOp] -> [Primitive] -> Node -> Sem r Node
+checkBuiltins' unsupportedOps unsupportedTypes = dmapRM go
+  where
+    go :: Node -> Sem r Recur
+    go node = case node of
+      NPrim TypePrim {..}
+        | _typePrimPrimitive `elem` unsupportedTypes ->
+            throw $ unsupportedError "type" node (getInfoLocation _typePrimInfo)
+      NBlt BuiltinApp {..}
+        | _builtinAppOp `elem` unsupportedOps ->
+            throw $ unsupportedError "operation" node (getInfoLocation _builtinAppInfo)
+        | otherwise -> case _builtinAppOp of
+            OpFail -> return $ End node
+            _ -> return $ Recur node
+      _ -> return $ Recur node
+
 -- | Checks that the root of the node is not `Bottom`. Currently the only way we
 -- create `Bottom` is when translating axioms that are not builtin. Hence it is
 -- enough to check the root only.

src/Juvix/Compiler/Pipeline.hs

@@ -130,15 +130,22 @@ upToCoreTypecheck ::
 upToCoreTypecheck =
   upToCore >>= \r -> Core.toTypechecked (r ^. Core.coreResultModule) >>= \md -> return r {Core._coreResultModule = md}
 
+--------------------------------------------------------------------------------
+-- Workflows from stripped Core
+--------------------------------------------------------------------------------
+
+strippedCoreToTree :: Core.Module -> Sem r Tree.InfoTable
+strippedCoreToTree = return . Tree.fromCore . Stripped.fromCore . Core.computeCombinedInfoTable
+
 --------------------------------------------------------------------------------
 -- Workflows from stored Core
 --------------------------------------------------------------------------------
 
-storedCoreToTree :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r Tree.InfoTable
-storedCoreToTree = Core.toStripped >=> return . Tree.fromCore . Stripped.fromCore . Core.computeCombinedInfoTable
+storedCoreToTree :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.TransformationId -> Core.Module -> Sem r Tree.InfoTable
+storedCoreToTree checkId = Core.toStripped checkId >=> strippedCoreToTree
 
 storedCoreToAsm :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r Asm.InfoTable
-storedCoreToAsm = storedCoreToTree >=> treeToAsm
+storedCoreToAsm = storedCoreToTree Core.CheckExec >=> treeToAsm
 
 storedCoreToReg :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r Reg.InfoTable
 storedCoreToReg = storedCoreToAsm >=> asmToReg
@@ -159,8 +166,8 @@ storedCoreToVampIR' = Core.toVampIR' >=> return . VampIR.fromCore' False . Core.
 -- Workflows from Core
 --------------------------------------------------------------------------------
 
-coreToTree :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r Tree.InfoTable
-coreToTree = Core.toStored >=> storedCoreToTree
+coreToTree :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.TransformationId -> Core.Module -> Sem r Tree.InfoTable
+coreToTree checkId = Core.toStored >=> storedCoreToTree checkId
 
 coreToAsm :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r Asm.InfoTable
 coreToAsm = Core.toStored >=> storedCoreToAsm
@@ -169,13 +176,13 @@ coreToReg :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -
 coreToReg = Core.toStored >=> storedCoreToReg
 
 coreToNockma :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r (Nockma.Cell Natural)
-coreToNockma = Core.toExec >=> coreToTree >=> treeToNockma
+coreToNockma = coreToTree Core.CheckAnoma >=> treeToNockma
 
 coreToAnoma :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r (Nockma.Cell Natural)
-coreToAnoma = coreToTree >=> treeToAnoma
+coreToAnoma = coreToTree Core.CheckAnoma >=> treeToAnoma
 
 coreToMiniC :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r C.MiniCResult
-coreToMiniC = Core.toExec >=> coreToAsm >=> asmToMiniC
+coreToMiniC = coreToAsm >=> asmToMiniC
 
 coreToGeb :: (Members '[Error JuvixError, Reader EntryPoint] r) => Geb.ResultSpec -> Core.Module -> Sem r Geb.Result
 coreToGeb spec = Core.toStored >=> storedCoreToGeb spec

test/Compilation/Base.hs

@@ -51,6 +51,6 @@ compileErrorAssertion root' mainFile step = do
   step "Translate to JuvixCore"
   entryPoint <- testDefaultEntryPointIO root' mainFile
   PipelineResult {..} <- snd <$> testRunIO entryPoint upToCore
-  case run $ runReader Core.defaultCoreOptions $ runError @JuvixError $ Core.toStored' (_pipelineResult ^. Core.coreResultModule) >>= Core.toExec' >>= Core.toStripped' of
+  case run $ runReader Core.defaultCoreOptions $ runError @JuvixError $ Core.toStored' (_pipelineResult ^. Core.coreResultModule) >>= Core.toStripped' Core.CheckExec of
     Left _ -> assertBool "" True
     Right _ -> assertFailure "no error"

test/Core/Asm/Base.hs

@@ -6,6 +6,7 @@ import Core.Eval.Base
 import Core.Eval.Positive qualified as Eval
 import Juvix.Compiler.Asm.Translation.FromTree qualified as Asm
 import Juvix.Compiler.Core.Data.Module (computeCombinedInfoTable, moduleFromInfoTable)
+import Juvix.Compiler.Core.Data.TransformationId
 import Juvix.Compiler.Core.Options
 import Juvix.Compiler.Core.Pipeline
 import Juvix.Compiler.Core.Translation.FromSource
@@ -51,7 +52,7 @@ coreAsmAssertion mainFile expectedFile step = do
       assertEqDiffText ("Check: EVAL output = " <> toFilePath expectedFile) "" expected
     Right (tabIni, Just node) -> do
       step "Translate"
-      case run $ runReader defaultCoreOptions $ runError $ toStored' >=> toStripped' $ moduleFromInfoTable $ setupMainFunction defaultModuleId tabIni node of
+      case run $ runReader defaultCoreOptions $ runError $ toStored' >=> toStripped' Identity $ moduleFromInfoTable $ setupMainFunction defaultModuleId tabIni node of
         Left err -> assertFailure (show (pretty (fromJuvixError @GenericError err)))
         Right m -> do
           let tab = Asm.fromTree $ Tree.fromCore $ Stripped.fromCore $ computeCombinedInfoTable m

test/Core/Compile/Base.hs

@@ -8,6 +8,7 @@ import GHC.Base (seq)
 import Juvix.Compiler.Asm.Pretty qualified as Asm
 import Juvix.Compiler.Asm.Translation.FromTree qualified as Asm
 import Juvix.Compiler.Core.Data.Module
+import Juvix.Compiler.Core.Data.TransformationId
 import Juvix.Compiler.Core.Extra.Utils
 import Juvix.Compiler.Core.Options
 import Juvix.Compiler.Core.Pipeline
@@ -48,7 +49,7 @@ coreCompileAssertion' ::
   Assertion
 coreCompileAssertion' optLevel tab mainFile expectedFile stdinText step = do
   step "Translate to JuvixAsm"
-  case run . runReader opts . runError $ toStored' (moduleFromInfoTable tab) >>= toStripped' of
+  case run . runReader opts . runError $ toStored' (moduleFromInfoTable tab) >>= toStripped' CheckExec of
     Left err -> assertFailure (show (pretty (fromJuvixError @GenericError err)))
     Right m -> do
       let tab0 = computeCombinedInfoTable m

test/Core/Transformation/Pipeline.hs

@@ -9,7 +9,7 @@ allTests :: TestTree
 allTests = testGroup "Transformation pipeline (to Stripped)" (map liftTest Eval.compilableTests)
 
 pipe :: [TransformationId]
-pipe = toStoredTransformations ++ toStrippedTransformations
+pipe = toStoredTransformations ++ toStrippedTransformations Identity
 
 liftTest :: Eval.PosTest -> TestTree
 liftTest _testEval =

test/VampIR/Compilation/Base.hs

@@ -3,7 +3,6 @@ module VampIR.Compilation.Base where
 import Base
 import Core.VampIR.Base (coreVampIRAssertion')
 import Juvix.Compiler.Core
-import Juvix.Compiler.Core.Data.TransformationId
 import VampIR.Core.Base (VampirBackend (..), vampirAssertion')
 
 vampirCompileAssertion :: Path Abs Dir -> Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion