From ed20e7ebd032b5d3a056e48c4e478b6c266d9035 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 21 Feb 2024 13:44:17 +0100 Subject: [PATCH] refactor toStripped pipeline --- app/Commands/Dev/Core/Compile/Base.hs | 3 ++- app/Commands/Dev/Core/Strip.hs | 2 +- src/Juvix/Compiler/Core/Data.hs | 2 ++ .../Compiler/Core/Data/TransformationId.hs | 16 +++++++------ .../Core/Data/TransformationId/Strings.hs | 6 +++++ src/Juvix/Compiler/Core/Pipeline.hs | 16 ++++--------- src/Juvix/Compiler/Core/Transformation.hs | 2 ++ .../Core/Transformation/Check/Anoma.hs | 13 +++++++++++ .../Core/Transformation/Check/Base.hs | 16 +++++++++++++ src/Juvix/Compiler/Pipeline.hs | 23 ++++++++++++------- test/Compilation/Base.hs | 2 +- test/Core/Asm/Base.hs | 3 ++- test/Core/Compile/Base.hs | 3 ++- test/Core/Transformation/Pipeline.hs | 2 +- test/VampIR/Compilation/Base.hs | 1 - 15 files changed, 76 insertions(+), 34 deletions(-) create mode 100644 src/Juvix/Compiler/Core/Transformation/Check/Anoma.hs diff --git a/app/Commands/Dev/Core/Compile/Base.hs b/app/Commands/Dev/Core/Compile/Base.hs index 8d2f35f264..8bde3be72c 100644 --- a/app/Commands/Dev/Core/Compile/Base.hs +++ b/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' diff --git a/app/Commands/Dev/Core/Strip.hs b/app/Commands/Dev/Core/Strip.hs index dd0b3dd53b..92b5c0d6ae 100644 --- a/app/Commands/Dev/Core/Strip.hs +++ b/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') diff --git a/src/Juvix/Compiler/Core/Data.hs b/src/Juvix/Compiler/Core/Data.hs index 42ff0f294b..c1dd71d7f7 100644 --- a/src/Juvix/Compiler/Core/Data.hs +++ b/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 diff --git a/src/Juvix/Compiler/Core/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs index d881a152e6..c73c158668 100644 --- a/src/Juvix/Compiler/Core/Data/TransformationId.hs +++ b/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,6 +127,7 @@ instance PipelineId' TransformationId PipelineId where PipelineGeb -> strGebPipeline PipelineVampIR -> strVampIRPipeline PipelineStripped -> strStrippedPipeline + PipelineExec -> strExecPipeline pipeline :: PipelineId -> [TransformationId] pipeline = \case @@ -134,4 +135,5 @@ instance PipelineId' TransformationId PipelineId where PipelineNormalize -> toNormalizeTransformations PipelineGeb -> toGebTransformations PipelineVampIR -> toVampIRTransformations - PipelineStripped -> toStrippedTransformations + PipelineStripped -> toStrippedTransformations Identity + PipelineExec -> toStrippedTransformations CheckExec diff --git a/src/Juvix/Compiler/Core/Data/TransformationId/Strings.hs b/src/Juvix/Compiler/Core/Data/TransformationId/Strings.hs index 7f98fadf4c..20a3a61e05 100644 --- a/src/Juvix/Compiler/Core/Data/TransformationId/Strings.hs +++ b/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" diff --git a/src/Juvix/Compiler/Core/Pipeline.hs b/src/Juvix/Compiler/Core/Pipeline.hs index 9e99c06181..2395c23e3d 100644 --- a/src/Juvix/Compiler/Core/Pipeline.hs +++ b/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 diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs index 8ed69f529a..397e8c24a2 100644 --- a/src/Juvix/Compiler/Core/Transformation.hs +++ b/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 diff --git a/src/Juvix/Compiler/Core/Transformation/Check/Anoma.hs b/src/Juvix/Compiler/Core/Transformation/Check/Anoma.hs new file mode 100644 index 0000000000..ebd1931f0e --- /dev/null +++ b/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 diff --git a/src/Juvix/Compiler/Core/Transformation/Check/Base.hs b/src/Juvix/Compiler/Core/Transformation/Check/Base.hs index 07e10c881b..87da4b4269 100644 --- a/src/Juvix/Compiler/Core/Transformation/Check/Base.hs +++ b/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. diff --git a/src/Juvix/Compiler/Pipeline.hs b/src/Juvix/Compiler/Pipeline.hs index 54a6caeedf..faeacd4c5d 100644 --- a/src/Juvix/Compiler/Pipeline.hs +++ b/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 diff --git a/test/Compilation/Base.hs b/test/Compilation/Base.hs index 1bfa52822f..5c673efab1 100644 --- a/test/Compilation/Base.hs +++ b/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" diff --git a/test/Core/Asm/Base.hs b/test/Core/Asm/Base.hs index 521530031a..22de08843a 100644 --- a/test/Core/Asm/Base.hs +++ b/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 diff --git a/test/Core/Compile/Base.hs b/test/Core/Compile/Base.hs index dd6f67384e..be6b8cffa7 100644 --- a/test/Core/Compile/Base.hs +++ b/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 diff --git a/test/Core/Transformation/Pipeline.hs b/test/Core/Transformation/Pipeline.hs index 12845f6b5c..b92fa5bb07 100644 --- a/test/Core/Transformation/Pipeline.hs +++ b/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 = diff --git a/test/VampIR/Compilation/Base.hs b/test/VampIR/Compilation/Base.hs index 70e676dc42..8e974dfdb0 100644 --- a/test/VampIR/Compilation/Base.hs +++ b/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