From f2298bd67464d595d1e6ec46b227c17b4a18871d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=C5=81ukasz=20Czajka?= <62751+lukaszcz@users.noreply.github.com> Date: Mon, 9 Jan 2023 18:21:30 +0100 Subject: [PATCH] JuvixCore to JuvixAsm translation (#1665) An implementation of the translation from JuvixCore to JuvixAsm. After merging this PR, the only remaining step to complete the basic compilation pipeline (#1556) is the compilation of complex pattern matching (#1531). * Fixes several bugs in lambda-lifting. * Fixes several bugs in the RemoveTypeArgs transformation. * Fixes several bugs in the TopEtaExpand transformation. * Adds the ConvertBuiltinTypes transformation which converts the builtin bool inductive type to Core primitive bool. * Adds the `juvix dev core strip` command. * Adds the `juvix dev core asm` command. * Adds the `juvix dev core compile` command. * Adds two groups of tests: - JuvixCore to JuvixAsm translation: translate JuvixCore tests to JuvixAsm and run the results with the JuvixAsm interpreter, - JuvixCore compilation: compile JuvixCore tests to native code and WASM and execute the results. * Closes #1520 * Closes #1549 --- app/AsmInterpreter.hs | 37 ++++ app/Commands/Dev/Asm/Run.hs | 34 +--- app/Commands/Dev/Core.hs | 6 + app/Commands/Dev/Core/Asm.hs | 24 +++ app/Commands/Dev/Core/Asm/Options.hs | 21 ++ app/Commands/Dev/Core/Compile.hs | 43 ++++ app/Commands/Dev/Core/Compile/Options.hs | 13 ++ app/Commands/Dev/Core/Options.hs | 38 +++- app/Commands/Dev/Core/Read.hs | 9 +- app/Commands/Dev/Core/Strip.hs | 20 ++ app/Commands/Dev/Core/Strip/Options.hs | 30 +++ app/Commands/Extra/Compile/Options.hs | 2 +- app/CommonOptions.hs | 11 ++ runtime/src/juvix/api.h | 2 +- src/Juvix/Compiler/Asm/Extra/Type.hs | 29 ++- src/Juvix/Compiler/Asm/Pretty/Base.hs | 15 +- .../Compiler/Asm/Translation/FromCore.hs | 184 ++++++++++++----- .../Compiler/Core/Data/InfoTableBuilder.hs | 6 +- .../Compiler/Core/Data/Stripped/InfoTable.hs | 2 + .../Compiler/Core/Data/TransformationId.hs | 1 + .../Core/Data/TransformationId/Parser.hs | 9 +- src/Juvix/Compiler/Core/Extra/Base.hs | 22 ++- .../Compiler/Core/Extra/Stripped/Base.hs | 23 +-- src/Juvix/Compiler/Core/Language.hs | 4 +- src/Juvix/Compiler/Core/Language/Nodes.hs | 20 +- src/Juvix/Compiler/Core/Language/Stripped.hs | 27 +-- .../Compiler/Core/Language/Stripped/Type.hs | 10 +- src/Juvix/Compiler/Core/Pipeline.hs | 16 ++ src/Juvix/Compiler/Core/Pretty/Base.hs | 24 ++- src/Juvix/Compiler/Core/Transformation.hs | 2 + .../Transformation/ConvertBuiltinTypes.hs | 50 +++++ .../Core/Transformation/LambdaLifting.hs | 56 +++--- .../Core/Transformation/RemoveTypeArgs.hs | 7 +- .../Core/Transformation/TopEtaExpand.hs | 4 +- .../Compiler/Core/Translation/FromInternal.hs | 2 +- .../Compiler/Core/Translation/FromSource.hs | 29 +++ .../Core/Translation/Stripped/FromCore.hs | 187 +++++++++++++++++- src/Juvix/Compiler/Pipeline.hs | 6 + src/Juvix/Compiler/Reg/Extra.hs | 2 +- src/Juvix/Extra/Strings.hs | 2 +- test/Asm/Compile/Base.hs | 32 +-- test/Asm/Run/Base.hs | 58 +++--- test/Core.hs | 4 +- test/Core/Asm.hs | 7 + test/Core/Asm/Base.hs | 53 +++++ test/Core/Asm/Positive.hs | 20 ++ test/Core/Compile.hs | 7 + test/Core/Compile/Base.hs | 53 +++++ test/Core/Compile/Positive.hs | 27 +++ test/Core/Eval/Base.hs | 5 +- test/Core/Eval/Positive.hs | 3 + test/Core/Transformation/Pipeline.hs | 3 +- tests/Core/positive/out/test009.out | 3 +- tests/Core/positive/out/test017.out | 1 - tests/Core/positive/out/test023.out | 9 +- tests/Core/positive/out/test026.out | 2 - tests/Core/positive/out/test030.out | 1 - tests/Core/positive/out/test031.out | 2 +- tests/Core/positive/out/test032.out | 2 +- tests/Core/positive/test009.jvc | 3 +- tests/Core/positive/test012.jvc | 2 +- tests/Core/positive/test017.jvc | 3 +- tests/Core/positive/test023.jvc | 9 +- tests/Core/positive/test026.jvc | 4 +- tests/Core/positive/test030.jvc | 35 ++-- tests/Core/positive/test031.jvc | 2 +- tests/Core/positive/test032.jvc | 2 +- tests/Core/positive/test040.jvc | 20 +- tests/Core/positive/test042.jvc | 4 +- tests/Core/positive/test043.jvc | 4 +- tests/Core/positive/test044.jvc | 2 +- 71 files changed, 1108 insertions(+), 303 deletions(-) create mode 100644 app/AsmInterpreter.hs create mode 100644 app/Commands/Dev/Core/Asm.hs create mode 100644 app/Commands/Dev/Core/Asm/Options.hs create mode 100644 app/Commands/Dev/Core/Compile.hs create mode 100644 app/Commands/Dev/Core/Compile/Options.hs create mode 100644 app/Commands/Dev/Core/Strip.hs create mode 100644 app/Commands/Dev/Core/Strip/Options.hs create mode 100644 src/Juvix/Compiler/Core/Pipeline.hs create mode 100644 src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs create mode 100644 test/Core/Asm.hs create mode 100644 test/Core/Asm/Base.hs create mode 100644 test/Core/Asm/Positive.hs create mode 100644 test/Core/Compile.hs create mode 100644 test/Core/Compile/Base.hs create mode 100644 test/Core/Compile/Positive.hs diff --git a/app/AsmInterpreter.hs b/app/AsmInterpreter.hs new file mode 100644 index 0000000000..10e58f588f --- /dev/null +++ b/app/AsmInterpreter.hs @@ -0,0 +1,37 @@ +module AsmInterpreter where + +import App +import CommonOptions +import Juvix.Compiler.Asm.Data.InfoTable qualified as Asm +import Juvix.Compiler.Asm.Extra qualified as Asm +import Juvix.Compiler.Asm.Interpreter qualified as Asm +import Juvix.Compiler.Asm.Pretty qualified as Asm +import Juvix.Compiler.Asm.Transformation.Validate qualified as Asm + +runAsm :: forall r. Members '[Embed IO, App] r => Bool -> Asm.InfoTable -> Sem r () +runAsm bValidate tab = + let v = if bValidate then Asm.validate' tab else Nothing + in case v of + Just err -> + exitJuvixError (JuvixError err) + Nothing -> + case tab ^. Asm.infoMainFunction of + Just sym -> do + r <- doRun tab (Asm.getFunInfo tab sym) + case r of + Left err -> + exitJuvixError (JuvixError err) + Right Asm.ValVoid -> + return () + Right val -> do + renderStdOut (Asm.ppOut (Asm.defaultOptions tab) val) + embed (putStrLn "") + Nothing -> + exitMsg (ExitFailure 1) "no 'main' function" + where + doRun :: + Asm.InfoTable -> + Asm.FunctionInfo -> + Sem r (Either Asm.AsmError Asm.Val) + doRun tab' funInfo = + embed $ Asm.catchRunErrorIO (Asm.runCodeIO tab' funInfo) diff --git a/app/Commands/Dev/Asm/Run.hs b/app/Commands/Dev/Asm/Run.hs index 89e232b73d..65f2a6fadf 100644 --- a/app/Commands/Dev/Asm/Run.hs +++ b/app/Commands/Dev/Asm/Run.hs @@ -1,13 +1,8 @@ module Commands.Dev.Asm.Run where +import AsmInterpreter import Commands.Base import Commands.Dev.Asm.Run.Options -import Juvix.Compiler.Asm.Data.InfoTable qualified as Asm -import Juvix.Compiler.Asm.Error qualified as Asm -import Juvix.Compiler.Asm.Extra qualified as Asm -import Juvix.Compiler.Asm.Interpreter qualified as Asm -import Juvix.Compiler.Asm.Pretty qualified as Asm -import Juvix.Compiler.Asm.Transformation.Validate qualified as Asm import Juvix.Compiler.Asm.Translation.FromSource qualified as Asm runCommand :: forall r. Members '[Embed IO, App] r => AsmRunOptions -> Sem r () @@ -16,32 +11,7 @@ runCommand opts = do s <- embed (readFile (toFilePath afile)) case Asm.runParser (toFilePath afile) s of Left err -> exitJuvixError (JuvixError err) - Right tab -> - let v = if opts ^. asmRunNoValidate then Nothing else Asm.validate' tab - in case v of - Just err -> - exitJuvixError (JuvixError err) - Nothing -> - case tab ^. Asm.infoMainFunction of - Just sym -> do - r <- doRun tab (Asm.getFunInfo tab sym) - case r of - Left err -> - exitJuvixError (JuvixError err) - Right Asm.ValVoid -> - return () - Right val -> do - renderStdOut (Asm.ppOut (Asm.defaultOptions tab) val) - embed (putStrLn "") - Nothing -> - exitMsg (ExitFailure 1) "no 'main' function" + Right tab -> runAsm (not (opts ^. asmRunNoValidate)) tab where file :: SomeBase File file = opts ^. asmRunInputFile . pathPath - - doRun :: - Asm.InfoTable -> - Asm.FunctionInfo -> - Sem r (Either Asm.AsmError Asm.Val) - doRun tab funInfo = - embed $ Asm.catchRunErrorIO (Asm.runCodeIO tab funInfo) diff --git a/app/Commands/Dev/Core.hs b/app/Commands/Dev/Core.hs index 481beae4cd..9d31f29e9d 100644 --- a/app/Commands/Dev/Core.hs +++ b/app/Commands/Dev/Core.hs @@ -1,13 +1,19 @@ module Commands.Dev.Core where import Commands.Base +import Commands.Dev.Core.Asm as Asm +import Commands.Dev.Core.Compile as Compile import Commands.Dev.Core.Eval as Eval import Commands.Dev.Core.Options import Commands.Dev.Core.Read as Read import Commands.Dev.Core.Repl as Repl +import Commands.Dev.Core.Strip as Strip runCommand :: forall r. Members '[Embed IO, App] r => CoreCommand -> Sem r () runCommand = \case Repl opts -> Repl.runCommand opts Eval opts -> Eval.runCommand opts Read opts -> Read.runCommand opts + Strip opts -> Strip.runCommand opts + CoreAsm opts -> Asm.runCommand opts + CoreCompile opts -> Compile.runCommand opts diff --git a/app/Commands/Dev/Core/Asm.hs b/app/Commands/Dev/Core/Asm.hs new file mode 100644 index 0000000000..d5badae050 --- /dev/null +++ b/app/Commands/Dev/Core/Asm.hs @@ -0,0 +1,24 @@ +module Commands.Dev.Core.Asm where + +import AsmInterpreter +import Commands.Base +import Commands.Dev.Core.Asm.Options +import Juvix.Compiler.Asm.Pretty qualified as Asm +import Juvix.Compiler.Asm.Translation.FromCore qualified as Asm +import Juvix.Compiler.Core.Pipeline qualified as Core +import Juvix.Compiler.Core.Translation.FromSource qualified as Core +import Juvix.Compiler.Core.Translation.Stripped.FromCore qualified as Stripped + +runCommand :: forall r a. (Members '[Embed IO, App] r, CanonicalProjection a CoreAsmOptions) => a -> Sem r () +runCommand opts = do + inputFile :: Path Abs File <- someBaseToAbs' sinputFile + s' <- embed (readFile $ toFilePath inputFile) + tab <- getRight (mapLeft JuvixError (Core.runParserMain (toFilePath inputFile) Core.emptyInfoTable s')) + let tab' = Asm.fromCore $ Stripped.fromCore (Core.toStripped tab) + if + | project opts ^. coreAsmPrint -> + renderStdOut (Asm.ppOutDefault tab' tab') + | otherwise -> runAsm True tab' + where + sinputFile :: SomeBase File + sinputFile = project opts ^. coreAsmInputFile . pathPath diff --git a/app/Commands/Dev/Core/Asm/Options.hs b/app/Commands/Dev/Core/Asm/Options.hs new file mode 100644 index 0000000000..bff4f8e793 --- /dev/null +++ b/app/Commands/Dev/Core/Asm/Options.hs @@ -0,0 +1,21 @@ +module Commands.Dev.Core.Asm.Options where + +import CommonOptions + +data CoreAsmOptions = CoreAsmOptions + { _coreAsmPrint :: Bool, + _coreAsmInputFile :: AppPath File + } + deriving stock (Data) + +makeLenses ''CoreAsmOptions + +parseCoreAsmOptions :: Parser CoreAsmOptions +parseCoreAsmOptions = do + _coreAsmPrint <- + switch + ( long "print" + <> help "print the generated JuvixAsm code instead of running it" + ) + _coreAsmInputFile <- parseInputJuvixCoreFile + pure CoreAsmOptions {..} diff --git a/app/Commands/Dev/Core/Compile.hs b/app/Commands/Dev/Core/Compile.hs new file mode 100644 index 0000000000..8fb5630526 --- /dev/null +++ b/app/Commands/Dev/Core/Compile.hs @@ -0,0 +1,43 @@ +module Commands.Dev.Core.Compile where + +import Commands.Base +import Commands.Dev.Core.Compile.Options +import Commands.Extra.Compile qualified as Compile +import Data.Text.IO qualified as TIO +import Juvix.Compiler.Asm.Options qualified as Asm +import Juvix.Compiler.Backend qualified as Backend +import Juvix.Compiler.Backend.C qualified as C +import Juvix.Compiler.Core.Data.InfoTable qualified as Core +import Juvix.Compiler.Core.Translation.FromSource qualified as Core + +runCommand :: forall r. Members '[Embed IO, App] r => CoreCompileOptions -> Sem r () +runCommand opts = do + file <- getFile + s <- embed (readFile (toFilePath file)) + tab <- getRight (mapLeft JuvixError (Core.runParserMain (toFilePath file) Core.emptyInfoTable s)) + C.MiniCResult {..} <- getRight (run (runError (coreToMiniC asmOpts tab :: Sem '[Error JuvixError] C.MiniCResult))) + buildDir <- askBuildDir + ensureDir buildDir + cFile <- inputCFile file + embed $ TIO.writeFile (toFilePath cFile) _resultCCode + Compile.runCommand opts {_compileInputFile = AppPath (Abs cFile) False} + where + getFile :: Sem r (Path Abs File) + getFile = someBaseToAbs' (opts ^. compileInputFile . pathPath) + + asmOpts :: Asm.Options + asmOpts = Asm.makeOptions (asmTarget (opts ^. compileTarget)) (opts ^. compileDebug) + + asmTarget :: CompileTarget -> Backend.Target + asmTarget = \case + TargetWasm32Wasi -> Backend.TargetCWasm32Wasi + TargetNative64 -> Backend.TargetCNative64 + TargetC -> Backend.TargetCWasm32Wasi + +inputCFile :: Members '[App] r => Path Abs File -> Sem r (Path Abs File) +inputCFile inputFileCompile = do + buildDir <- askBuildDir + return (buildDir outputMiniCFile) + where + outputMiniCFile :: Path Rel File + outputMiniCFile = replaceExtension' ".c" (filename inputFileCompile) diff --git a/app/Commands/Dev/Core/Compile/Options.hs b/app/Commands/Dev/Core/Compile/Options.hs new file mode 100644 index 0000000000..1f40e5a83f --- /dev/null +++ b/app/Commands/Dev/Core/Compile/Options.hs @@ -0,0 +1,13 @@ +module Commands.Dev.Core.Compile.Options + ( module Commands.Dev.Core.Compile.Options, + module Commands.Extra.Compile.Options, + ) +where + +import Commands.Extra.Compile.Options +import CommonOptions + +type CoreCompileOptions = CompileOptions + +parseCoreCompileOptions :: Parser CoreCompileOptions +parseCoreCompileOptions = parseCompileOptions diff --git a/app/Commands/Dev/Core/Options.hs b/app/Commands/Dev/Core/Options.hs index fa90e8eb8e..6ff66d78f0 100644 --- a/app/Commands/Dev/Core/Options.hs +++ b/app/Commands/Dev/Core/Options.hs @@ -1,14 +1,20 @@ module Commands.Dev.Core.Options where +import Commands.Dev.Core.Asm.Options +import Commands.Dev.Core.Compile.Options import Commands.Dev.Core.Eval.Options import Commands.Dev.Core.Read.Options import Commands.Dev.Core.Repl.Options +import Commands.Dev.Core.Strip.Options import CommonOptions data CoreCommand = Repl CoreReplOptions | Eval CoreEvalOptions | Read CoreReadOptions + | Strip CoreStripOptions + | CoreAsm CoreAsmOptions + | CoreCompile CoreCompileOptions deriving stock (Data) parseCoreCommand :: Parser CoreCommand @@ -17,7 +23,10 @@ parseCoreCommand = mconcat [ commandRepl, commandEval, - commandRead + commandRead, + commandStrip, + commandAsm, + commandCompile ] where commandRepl :: Mod CommandFields CoreCommand @@ -29,6 +38,15 @@ parseCoreCommand = commandRead :: Mod CommandFields CoreCommand commandRead = command "read" readInfo + commandStrip :: Mod CommandFields CoreCommand + commandStrip = command "strip" stripInfo + + commandAsm :: Mod CommandFields CoreCommand + commandAsm = command "asm" asmInfo + + commandCompile :: Mod CommandFields CoreCommand + commandCompile = command "compile" compileInfo + replInfo :: ParserInfo CoreCommand replInfo = info @@ -46,3 +64,21 @@ parseCoreCommand = info (Read <$> parseCoreReadOptions) (progDesc "Read a JuvixCore file, transform it, and pretty print it") + + stripInfo :: ParserInfo CoreCommand + stripInfo = + info + (Strip <$> parseCoreStripOptions) + (progDesc "Translate a JuvixCore file to Core.Stripped and pretty print the result") + + asmInfo :: ParserInfo CoreCommand + asmInfo = + info + (CoreAsm <$> parseCoreAsmOptions) + (progDesc "Translate a JuvixCore file to JuvixAsm and run the result") + + compileInfo :: ParserInfo CoreCommand + compileInfo = + info + (CoreCompile <$> parseCoreCompileOptions) + (progDesc "Compile a JuvixCore file to native code or WebAssembly") diff --git a/app/Commands/Dev/Core/Read.hs b/app/Commands/Dev/Core/Read.hs index 609c71dd70..668752e7a8 100644 --- a/app/Commands/Dev/Core/Read.hs +++ b/app/Commands/Dev/Core/Read.hs @@ -12,12 +12,12 @@ runCommand :: forall r a. (Members '[Embed IO, App] r, CanonicalProjection a Eva runCommand opts = do inputFile :: Path Abs File <- someBaseToAbs' sinputFile s' <- embed . readFile . toFilePath $ inputFile - (tab, mnode) <- getRight (mapLeft JuvixError (Core.runParser (toFilePath inputFile) Core.emptyInfoTable s')) + tab <- getRight (mapLeft JuvixError (Core.runParserMain (toFilePath inputFile) Core.emptyInfoTable s')) let tab' = Core.applyTransformations (project opts ^. coreReadTransformations) tab embed (Scoper.scopeTrace tab') unless (project opts ^. coreReadNoPrint) $ do renderStdOut (Core.ppOut opts tab') - whenJust mnode $ doEval tab' + whenJust (tab' ^. Core.infoMain) $ \sym -> doEval tab' (fromJust $ tab' ^. Core.identContext . at sym) where doEval :: Core.InfoTable -> Core.Node -> Sem r () doEval tab' node = @@ -27,9 +27,6 @@ runCommand opts = do embed (putStrLn "| Eval |") embed (putStrLn "--------------------------------") Eval.evalAndPrint opts tab' node - | otherwise -> do - embed (putStrLn "-- Node") - renderStdOut (Core.ppOut opts node) - embed (putStrLn "") + | otherwise -> return () sinputFile :: SomeBase File sinputFile = project opts ^. coreReadInputFile . pathPath diff --git a/app/Commands/Dev/Core/Strip.hs b/app/Commands/Dev/Core/Strip.hs new file mode 100644 index 0000000000..ff110644a7 --- /dev/null +++ b/app/Commands/Dev/Core/Strip.hs @@ -0,0 +1,20 @@ +module Commands.Dev.Core.Strip where + +import Commands.Base +import Commands.Dev.Core.Strip.Options +import Juvix.Compiler.Core.Pipeline qualified as Core +import Juvix.Compiler.Core.Pretty qualified as Core +import Juvix.Compiler.Core.Translation.FromSource qualified as Core +import Juvix.Compiler.Core.Translation.Stripped.FromCore qualified as Stripped + +runCommand :: forall r a. (Members '[Embed IO, App] r, CanonicalProjection a Core.Options, CanonicalProjection a CoreStripOptions) => a -> Sem r () +runCommand opts = do + inputFile :: Path Abs File <- someBaseToAbs' sinputFile + s' <- embed (readFile $ toFilePath inputFile) + (tab, _) <- getRight (mapLeft JuvixError (Core.runParser (toFilePath inputFile) Core.emptyInfoTable s')) + let tab' = Stripped.fromCore (Core.toStripped tab) + unless (project opts ^. coreStripNoPrint) $ do + renderStdOut (Core.ppOut opts tab') + where + sinputFile :: SomeBase File + sinputFile = project opts ^. coreStripInputFile . pathPath diff --git a/app/Commands/Dev/Core/Strip/Options.hs b/app/Commands/Dev/Core/Strip/Options.hs new file mode 100644 index 0000000000..f55213af37 --- /dev/null +++ b/app/Commands/Dev/Core/Strip/Options.hs @@ -0,0 +1,30 @@ +module Commands.Dev.Core.Strip.Options where + +import CommonOptions +import Juvix.Compiler.Core.Pretty.Options qualified as Core + +data CoreStripOptions = CoreStripOptions + { _coreStripShowDeBruijn :: Bool, + _coreStripNoPrint :: Bool, + _coreStripInputFile :: AppPath File + } + deriving stock (Data) + +makeLenses ''CoreStripOptions + +instance CanonicalProjection CoreStripOptions Core.Options where + project c = + Core.defaultOptions + { Core._optShowDeBruijnIndices = c ^. coreStripShowDeBruijn + } + +parseCoreStripOptions :: Parser CoreStripOptions +parseCoreStripOptions = do + _coreStripShowDeBruijn <- optDeBruijn + _coreStripNoPrint <- + switch + ( long "no-print" + <> help "do not print the stripped code" + ) + _coreStripInputFile <- parseInputJuvixCoreFile + pure CoreStripOptions {..} diff --git a/app/Commands/Extra/Compile/Options.hs b/app/Commands/Extra/Compile/Options.hs index e830753f90..6536ce94e5 100644 --- a/app/Commands/Extra/Compile/Options.hs +++ b/app/Commands/Extra/Compile/Options.hs @@ -42,7 +42,7 @@ parseCompileOptions = do ) _compileTarget <- optCompileTarget _compileOutputFile <- optional parseGenericOutputFile - _compileInputFile <- parseInputCFile + _compileInputFile <- parseGenericInputFile pure CompileOptions {..} optCompileTarget :: Parser CompileTarget diff --git a/app/CommonOptions.hs b/app/CommonOptions.hs index 43055339b9..7bc112622e 100644 --- a/app/CommonOptions.hs +++ b/app/CommonOptions.hs @@ -69,6 +69,17 @@ parseInputCFile = do ) pure AppPath {_pathIsInput = True, ..} +parseGenericInputFile :: Parser (AppPath File) +parseGenericInputFile = do + _pathPath <- + argument + someFileOpt + ( metavar "INPUT_FILE" + <> help "Path to input file" + <> action "file" + ) + pure AppPath {_pathIsInput = True, ..} + parseGenericOutputFile :: Parser (AppPath File) parseGenericOutputFile = do _pathPath <- diff --git a/runtime/src/juvix/api.h b/runtime/src/juvix/api.h index a837554812..aa0c48130f 100644 --- a/runtime/src/juvix/api.h +++ b/runtime/src/juvix/api.h @@ -29,7 +29,7 @@ io_print_toplevel(juvix_result); // Temporary vars -#define DECL_TMP(k) word_t juvix_tmp_##k +#define DECL_TMP(k) UNUSED word_t juvix_tmp_##k #define TMP(k) juvix_tmp_##k // Value stack temporary vars diff --git a/src/Juvix/Compiler/Asm/Extra/Type.hs b/src/Juvix/Compiler/Asm/Extra/Type.hs index e21e6e5dd4..8b2d95d46f 100644 --- a/src/Juvix/Compiler/Asm/Extra/Type.hs +++ b/src/Juvix/Compiler/Asm/Extra/Type.hs @@ -26,6 +26,7 @@ mkTypeFun args tgt = case args of unfoldType :: Type -> ([Type], Type) unfoldType ty = (typeArgs ty, typeTarget ty) +-- converts e.g. `A -> B -> C -> D` to `(A, B, C) -> D` where `D` is an atom uncurryType :: Type -> Type uncurryType ty = case typeArgs ty of [] -> @@ -34,6 +35,16 @@ uncurryType ty = case typeArgs ty of let ty' = uncurryType (typeTarget ty) in mkTypeFun (tyargs ++ typeArgs ty') (typeTarget ty') +-- converts e.g. `(A, B, C) -> (D, E) -> F` to `A -> B -> C -> D -> E -> F` +-- where `F` is an atom +curryType :: Type -> Type +curryType ty = case typeArgs ty of + [] -> + ty + tyargs -> + let ty' = curryType (typeTarget ty) + in foldr (\tyarg ty'' -> mkTypeFun [tyarg] ty'') (typeTarget ty') tyargs + unifyTypes :: forall r. Members '[Error AsmError, Reader (Maybe Location), Reader InfoTable] r => Type -> Type -> Sem r Type unifyTypes ty1 ty2 = case (ty1, ty2) of (TyDynamic, x) -> return x @@ -95,7 +106,23 @@ unifyTypes ty1 ty2 = case (ty1, ty2) of throw $ AsmError loc ("not unifiable: " <> ppTrace tab ty1 <> ", " <> ppTrace tab ty2) unifyTypes' :: Member (Error AsmError) r => Maybe Location -> InfoTable -> Type -> Type -> Sem r Type -unifyTypes' loc tab ty1 ty2 = runReader loc $ runReader tab $ unifyTypes ty1 ty2 +unifyTypes' loc tab ty1 ty2 = + runReader loc $ + runReader tab $ + -- The `if` is to ensure correct behaviour with dynamic type targets. E.g. + -- `(A, B) -> *` should unify with `A -> B -> C -> D`. + if + | tgt1 == TyDynamic && tgt2 == TyDynamic -> + unifyTypes (curryType ty1) (curryType ty2) + | tgt1 == TyDynamic -> + unifyTypes (uncurryType ty1) ty2 + | tgt2 == TyDynamic -> + unifyTypes ty1 (uncurryType ty2) + | otherwise -> + unifyTypes ty1 ty2 + where + tgt1 = typeTarget (uncurryType ty1) + tgt2 = typeTarget (uncurryType ty2) isSubtype :: Type -> Type -> Bool isSubtype ty1 ty2 = case (ty1, ty2) of diff --git a/src/Juvix/Compiler/Asm/Pretty/Base.hs b/src/Juvix/Compiler/Asm/Pretty/Base.hs index 277191e028..dbb2c3b5a3 100644 --- a/src/Juvix/Compiler/Asm/Pretty/Base.hs +++ b/src/Juvix/Compiler/Asm/Pretty/Base.hs @@ -338,6 +338,18 @@ instance PrettyCode FunctionInfo where <+> targetty <+> braces' c +ppFunSig :: Member (Reader Options) r => FunctionInfo -> Sem r (Doc Ann) +ppFunSig FunctionInfo {..} = do + argtys <- mapM ppCode (typeArgs _functionType) + targetty <- ppCode (typeTarget _functionType) + return $ + keyword Str.function + <+> annotate (AnnKind KNameFunction) (pretty _functionName) + <> encloseSep lparen rparen ", " argtys + <+> colon + <+> targetty + <> semi + instance PrettyCode ConstructorInfo where ppCode ConstructorInfo {..} = do ty <- ppCode _constructorType @@ -351,8 +363,9 @@ instance PrettyCode InductiveInfo where instance PrettyCode InfoTable where ppCode InfoTable {..} = do inds <- mapM ppCode (HashMap.elems _infoInductives) + funsigs <- mapM ppFunSig (HashMap.elems _infoFunctions) funs <- mapM ppCode (HashMap.elems _infoFunctions) - return $ vcat (map (<> line) inds) <> line <> vcat (map (<> line) funs) + return $ vcat (map (<> line) inds) <> line <> vcat funsigs <> line <> line <> vcat (map (<> line) funs) {--------------------------------------------------------------------------------} {- helper functions -} diff --git a/src/Juvix/Compiler/Asm/Translation/FromCore.hs b/src/Juvix/Compiler/Asm/Translation/FromCore.hs index fdd16bc347..87f05cf86f 100644 --- a/src/Juvix/Compiler/Asm/Translation/FromCore.hs +++ b/src/Juvix/Compiler/Asm/Translation/FromCore.hs @@ -1,12 +1,14 @@ -module Juvix.Compiler.Asm.Translation.FromCore where +module Juvix.Compiler.Asm.Translation.FromCore (fromCore) where import Data.DList qualified as DL import Data.HashMap.Strict qualified as HashMap import Juvix.Compiler.Asm.Data.InfoTable import Juvix.Compiler.Asm.Extra.Base +import Juvix.Compiler.Asm.Extra.Type import Juvix.Compiler.Asm.Language import Juvix.Compiler.Core.Data.BinderList qualified as BL import Juvix.Compiler.Core.Data.Stripped.InfoTable qualified as Core +import Juvix.Compiler.Core.Extra.Stripped.Base qualified as Core import Juvix.Compiler.Core.Language.Stripped qualified as Core type BinderList = BL.BinderList @@ -14,6 +16,15 @@ type BinderList = BL.BinderList -- DList for O(1) snoc and append type Code' = DL.DList Command +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) + } + -- Generate code for a single function. genCode :: Core.InfoTable -> Core.FunctionInfo -> FunctionInfo genCode infoTable fi = @@ -37,9 +48,6 @@ genCode infoTable fi = _functionMaxValueStackHeight = -1 } where - unimplemented :: forall a. a - unimplemented = error "not yet implemented" - -- Assumption: the BinderList does not contain references to the value stack -- (directly or indirectly). go :: Bool -> Int -> BinderList Value -> Core.Node -> Code' @@ -80,7 +88,11 @@ genCode infoTable fi = DL.singleton $ mkInstr $ Push (ConstInt i) - _ -> unimplemented + Core.Constant _ (Core.ConstString s) -> + snocReturn isTail $ + DL.singleton $ + mkInstr $ + Push (ConstString s) goApps :: Bool -> Int -> BinderList Value -> Core.Apps -> Code' goApps isTail tempSize refs (Core.Apps {..}) = @@ -105,35 +117,21 @@ genCode infoTable fi = -- (with Call) and then use CallClosures or -- TailCallClosures on the result with the remaining -- arguments. - unimplemented - where - argsNum = getArgsNum _identSymbol - Core.FunVar Core.Var {..} -> - if - | argsNum > suppliedArgsNum -> - snocReturn isTail $ - DL.snoc - ( DL.snoc - (DL.concat (map (go False tempSize refs) suppliedArgs)) - (mkInstr $ Push (BL.lookup _varIndex refs)) - ) - (mkInstr $ ExtendClosure (InstrExtendClosure suppliedArgsNum)) - | argsNum == suppliedArgsNum -> DL.snoc ( DL.snoc (DL.concat (map (go False tempSize refs) suppliedArgs)) - (mkInstr $ Push (BL.lookup _varIndex refs)) + (mkInstr $ Call (InstrCall (CallFun _identSymbol) argsNum)) ) - (mkInstr $ (if isTail then TailCall else Call) (InstrCall CallClosure argsNum)) - | otherwise -> - -- Here use CallClosures or TailCallClosures. - unimplemented + (mkInstr $ (if isTail then TailCallClosures else CallClosures) (InstrCallClosures (suppliedArgsNum - argsNum))) where - argsNum :: Int - argsNum = case _varInfo ^. Core.varInfoType of - Core.TyDynamic -> -1 - ty -> Core.typeArgsNum ty - + argsNum = getArgsNum _identSymbol + Core.FunVar Core.Var {..} -> + DL.snoc + ( DL.snoc + (DL.concat (map (go False tempSize refs) suppliedArgs)) + (mkInstr $ Push (BL.lookup _varIndex refs)) + ) + (mkInstr $ (if isTail then TailCallClosures else CallClosures) (InstrCallClosures suppliedArgsNum)) goBuiltinApp :: Bool -> Int -> BinderList Value -> Core.BuiltinApp -> Code' goBuiltinApp isTail tempSize refs (Core.BuiltinApp {..}) = snocReturn isTail $ @@ -167,18 +165,50 @@ genCode infoTable fi = goCase :: Bool -> Int -> BinderList Value -> Core.Case -> Code' goCase isTail tempSize refs (Core.Case {..}) = - -- TODO: special case for if-then-else (use Branch instead of Case) - DL.snoc - (go False tempSize refs _caseValue) - ( Case $ - CmdCase - { _cmdCaseInfo = emptyInfo, - _cmdCaseInductive = _caseInfo ^. Core.caseInfoInductive, - _cmdCaseBranches = compileCaseBranches _caseBranches, - _cmdCaseDefault = fmap compileCaseDefault _caseDefault - } - ) + case _caseBranches of + [br@Core.CaseBranch {..}] + | _caseBranchTag == Core.BuiltinTag Core.TagTrue -> + compileIf _caseValue (br ^. Core.caseBranchBody) (fromMaybe branchFailure _caseDefault) + [br@Core.CaseBranch {..}] + | _caseBranchTag == Core.BuiltinTag Core.TagFalse -> + compileIf _caseValue (fromMaybe branchFailure _caseDefault) (br ^. Core.caseBranchBody) + [br1, br2] + | br1 ^. Core.caseBranchTag == Core.BuiltinTag Core.TagTrue + && br2 ^. Core.caseBranchTag == Core.BuiltinTag Core.TagFalse -> + compileIf _caseValue (br1 ^. Core.caseBranchBody) (br2 ^. Core.caseBranchBody) + | br1 ^. Core.caseBranchTag == Core.BuiltinTag Core.TagFalse + && br2 ^. Core.caseBranchTag == Core.BuiltinTag Core.TagTrue -> + compileIf _caseValue (br2 ^. Core.caseBranchBody) (br1 ^. Core.caseBranchBody) + _ -> + DL.snoc + (go False tempSize refs _caseValue) + ( Case $ + CmdCase + { _cmdCaseInfo = emptyInfo, + _cmdCaseInductive = _caseInductive, + _cmdCaseBranches = compileCaseBranches _caseBranches, + _cmdCaseDefault = fmap compileCaseDefault _caseDefault + } + ) where + compileIf :: Core.Node -> Core.Node -> Core.Node -> Code' + compileIf value br1 br2 = + DL.snoc + (go False tempSize refs value) + ( Branch $ + CmdBranch + { _cmdBranchInfo = emptyInfo, + _cmdBranchTrue = DL.toList $ go isTail tempSize refs br1, + _cmdBranchFalse = DL.toList $ go isTail tempSize refs br2 + } + ) + + branchFailure :: Core.Node + branchFailure = + Core.mkBuiltinApp + Core.OpFail + [Core.mkConstant (Core.ConstString "illegal `if` branch")] + compileCaseBranches :: [Core.CaseBranch] -> [CaseBranch] compileCaseBranches branches = map @@ -232,10 +262,12 @@ genCode infoTable fi = Core.OpIntSub -> mkBinop IntSub Core.OpIntMul -> mkBinop IntMul Core.OpIntDiv -> mkBinop IntDiv + Core.OpIntMod -> mkBinop IntMod Core.OpIntLt -> mkBinop IntLt Core.OpIntLe -> mkBinop IntLe Core.OpEq -> mkBinop ValEq - _ -> unimplemented + Core.OpTrace -> mkInstr Trace + Core.OpFail -> mkInstr Failure getArgsNum :: Symbol -> Int getArgsNum sym = @@ -252,9 +284,69 @@ genCode infoTable fi = snocPopTemp False code = DL.snoc code (mkInstr PopTemp) snocPopTemp True code = code - convertType :: Int -> Core.Type -> Type - convertType = unimplemented - --- Be mindful that JuvixAsm types are explicitly uncurried, while --- Core.Stripped types are always curried. If a function takes `n` arguments +-- | Be mindful that JuvixAsm types are explicitly uncurried, while +-- Core.Stripped types are always curried. If a function takes `n` arguments, -- then the first `n` arguments should be uncurried in its JuvixAsm type. +convertType :: Int -> Core.Type -> Type +convertType argsNum ty = + case ty of + Core.TyDynamic -> + TyDynamic + Core.TyPrim x -> + convertPrimitiveType x + Core.TyApp Core.TypeApp {..} -> + TyInductive (TypeInductive _typeAppSymbol) + Core.TyFun {} -> + let (tgt, tyargs) = Core.unfoldType ty + tyargs' = map convertNestedType tyargs + tgt' = convertType 0 tgt + in mkTypeFun (take argsNum tyargs') (mkTypeFun (drop argsNum tyargs') tgt') + +convertPrimitiveType :: Core.Primitive -> Type +convertPrimitiveType = \case + Core.PrimInteger Core.PrimIntegerInfo {..} -> + TyInteger (TypeInteger _infoMinValue _infoMaxValue) + Core.PrimBool Core.PrimBoolInfo {..} -> + TyBool (TypeBool _infoTrueTag _infoFalseTag) + Core.PrimString -> + TyString + +-- | `convertNestedType` ensures that the conversion of a type with Dynamic in the +-- target is curried. The result of `convertType 0 ty` is always uncurried. +convertNestedType :: Core.Type -> Type +convertNestedType ty = + case ty of + Core.TyFun {} -> + let (tgt, tyargs) = Core.unfoldType ty + in case tgt of + Core.TyDynamic -> + curryType (convertType 0 ty) + _ -> + mkTypeFun (map convertNestedType tyargs) (convertType 0 tgt) + _ -> + convertType 0 ty + +translateInductiveInfo :: Core.InductiveInfo -> InductiveInfo +translateInductiveInfo ii = + InductiveInfo + { _inductiveName = ii ^. Core.inductiveName, + _inductiveLocation = ii ^. Core.inductiveLocation, + _inductiveSymbol = ii ^. Core.inductiveSymbol, + _inductiveKind = convertType 0 (ii ^. Core.inductiveKind), + _inductiveConstructors = map translateConstructorInfo (ii ^. Core.inductiveConstructors), + _inductiveRepresentation = IndRepStandard + } + +translateConstructorInfo :: Core.ConstructorInfo -> ConstructorInfo +translateConstructorInfo ci = + ConstructorInfo + { _constructorName = ci ^. Core.constructorName, + _constructorLocation = ci ^. Core.constructorLocation, + _constructorTag = ci ^. Core.constructorTag, + _constructorArgsNum = length (typeArgs ty), + _constructorType = ty, + _constructorInductive = ci ^. Core.constructorInductive, + _constructorRepresentation = MemRepConstr + } + where + ty = convertType 0 (ci ^. Core.constructorType) diff --git a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs index 0cfe5830a3..cdc901005d 100644 --- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs +++ b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs @@ -117,7 +117,7 @@ declareInductiveBuiltins :: Sem r () declareInductiveBuiltins indName blt ctrs = do sym <- freshSymbol - let ty = mkIdent' sym + let ty = mkTypeConstr' sym [] constrs <- mapM (\(tag, name, fty, cblt) -> createBuiltinConstr sym tag name (fty ty) cblt) ctrs registerInductive indName @@ -150,8 +150,8 @@ declareBoolBuiltins = declareInductiveBuiltins "bool" (Just BuiltinBool) - [ (BuiltinTag TagTrue, "true", id, Just BuiltinBoolTrue), - (BuiltinTag TagFalse, "false", id, Just BuiltinBoolFalse) + [ (BuiltinTag TagTrue, "true", const mkTypeBool', Just BuiltinBoolTrue), + (BuiltinTag TagFalse, "false", const mkTypeBool', Just BuiltinBoolFalse) ] declareNatBuiltins :: Member InfoTableBuilder r => Sem r () diff --git a/src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs b/src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs index f0af1b41f2..4315652d33 100644 --- a/src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs +++ b/src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs @@ -32,6 +32,7 @@ data ArgumentInfo = ArgumentInfo data InductiveInfo = InductiveInfo { _inductiveName :: Text, _inductiveLocation :: Maybe Location, + _inductiveSymbol :: Symbol, _inductiveKind :: Type, _inductiveConstructors :: [ConstructorInfo], _inductiveParams :: [ParameterInfo] @@ -40,6 +41,7 @@ data InductiveInfo = InductiveInfo data ConstructorInfo = ConstructorInfo { _constructorName :: Text, _constructorLocation :: Maybe Location, + _constructorInductive :: Symbol, _constructorTag :: Tag, _constructorType :: Type } diff --git a/src/Juvix/Compiler/Core/Data/TransformationId.hs b/src/Juvix/Compiler/Core/Data/TransformationId.hs index 6c8033b80f..073307195c 100644 --- a/src/Juvix/Compiler/Core/Data/TransformationId.hs +++ b/src/Juvix/Compiler/Core/Data/TransformationId.hs @@ -8,5 +8,6 @@ data TransformationId | RemoveTypeArgs | MoveApps | NatToInt + | ConvertBuiltinTypes | Identity deriving stock (Data) diff --git a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs index 668a7116c1..195185cc2c 100644 --- a/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs +++ b/src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs @@ -47,6 +47,7 @@ pcompletions = do RemoveTypeArgs -> strRemoveTypeArgs MoveApps -> strMoveApps NatToInt -> strNatToInt + ConvertBuiltinTypes -> strConvertBuiltinTypes lexeme :: MonadParsec e Text m => m a -> m a lexeme = L.lexeme L.hspace @@ -65,6 +66,7 @@ transformation = <|> symbol strRemoveTypeArgs $> RemoveTypeArgs <|> symbol strMoveApps $> MoveApps <|> symbol strNatToInt $> NatToInt + <|> symbol strConvertBuiltinTypes $> ConvertBuiltinTypes allStrings :: [Text] allStrings = @@ -72,7 +74,9 @@ allStrings = strTopEtaExpand, strIdentity, strRemoveTypeArgs, - strMoveApps + strMoveApps, + strNatToInt, + strConvertBuiltinTypes ] strLifting :: Text @@ -92,3 +96,6 @@ strMoveApps = "move-apps" strNatToInt :: Text strNatToInt = "nat-to-int" + +strConvertBuiltinTypes :: Text +strConvertBuiltinTypes = "convert-builtin-types" diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs index 206d9b3737..0a49bc2613 100644 --- a/src/Juvix/Compiler/Core/Extra/Base.hs +++ b/src/Juvix/Compiler/Core/Extra/Base.hs @@ -107,7 +107,7 @@ mkPi :: Info -> Binder -> Type -> Type mkPi i bi b = NPi (Pi i bi b) mkPi' :: Type -> Type -> Type -mkPi' = mkPi Info.empty . Binder "" Nothing +mkPi' = mkPi Info.empty . Binder "?" Nothing mkPis :: [Binder] -> Type -> Type mkPis tys ty = foldr (mkPi mempty) ty tys @@ -260,6 +260,26 @@ unfoldLambdas = first reverse . unfoldLambdasRev unfoldLambdas' :: Node -> (Int, Node) unfoldLambdas' = first length . unfoldLambdas +isType :: Node -> Bool +isType = \case + NPi {} -> True + NUniv {} -> True + NPrim {} -> True + NTyp {} -> True + NDyn {} -> True + NVar {} -> False + NIdt {} -> False + NCst {} -> False + NApp {} -> False + NBlt {} -> False + NCtr {} -> False + NLam {} -> False + NLet {} -> False + NRec {} -> False + NCase {} -> False + NMatch {} -> False + Closure {} -> False + {------------------------------------------------------------------------} {- functions on Pattern -} diff --git a/src/Juvix/Compiler/Core/Extra/Stripped/Base.hs b/src/Juvix/Compiler/Core/Extra/Stripped/Base.hs index 80e9a73bf6..26405c230b 100644 --- a/src/Juvix/Compiler/Core/Extra/Stripped/Base.hs +++ b/src/Juvix/Compiler/Core/Extra/Stripped/Base.hs @@ -29,28 +29,15 @@ mkBuiltinApp op args = NBlt (BuiltinApp () op args) mkConstr :: ConstrInfo -> Tag -> [Node] -> Node mkConstr i tag args = NCtr (Constr i tag args) -mkConstr' :: Symbol -> Tag -> [Node] -> Node -mkConstr' sym = mkConstr (ConstrInfo "" Nothing TyDynamic sym) - -mkLet :: LetInfo -> Node -> Node -> Node -mkLet i v b = NLet (Let i item b) +mkLet :: Binder -> Node -> Node -> Node +mkLet binder value body = NLet (Let () item body) where - binder :: Binder - binder = - Binder - { _binderName = i ^. letInfoBinderName, - _binderLocation = i ^. letInfoBinderLocation, - _binderType = i ^. letInfoBinderType - } item :: LetItem item = LetItem { _letItemBinder = binder, - _letItemValue = v + _letItemValue = value } -mkLet' :: Node -> Node -> Node -mkLet' = mkLet (LetInfo "" Nothing TyDynamic) - -mkCase :: CaseInfo -> Symbol -> Node -> [CaseBranch] -> Maybe Node -> Node -mkCase ci sym v bs def = NCase (Case ci sym v bs def) +mkCase :: Symbol -> Node -> [CaseBranch] -> Maybe Node -> Node +mkCase sym v bs def = NCase (Case () sym v bs def) diff --git a/src/Juvix/Compiler/Core/Language.hs b/src/Juvix/Compiler/Core/Language.hs index 0b87d4c6dc..7410800f0a 100644 --- a/src/Juvix/Compiler/Core/Language.hs +++ b/src/Juvix/Compiler/Core/Language.hs @@ -35,9 +35,9 @@ type Let = Let' Info Node Type type LetRec = LetRec' Info Node Type -type Case = Case' Info Info Node +type Case = Case' Info Info Node Type -type CaseBranch = CaseBranch' Info Node +type CaseBranch = CaseBranch' Info Node Type type Match = Match' Info Node diff --git a/src/Juvix/Compiler/Core/Language/Nodes.hs b/src/Juvix/Compiler/Core/Language/Nodes.hs index 93a864dcd1..080bfc71a3 100644 --- a/src/Juvix/Compiler/Core/Language/Nodes.hs +++ b/src/Juvix/Compiler/Core/Language/Nodes.hs @@ -48,7 +48,7 @@ data App' i a = App _appRight :: !a } -data Apps' f i a = Apps +data Apps' i f a = Apps { _appsInfo :: i, _appsFun :: !f, _appsArgs :: ![a] @@ -103,7 +103,7 @@ data LetItem' a ty = LetItem -- | Represents a block of mutually recursive local definitions. Both in the -- body and in the values `length _letRecValues` implicit binders are introduced -- which hold the functions/values being defined. --- the last item _letRecValues will have have index $0 in the body. +-- the last item in _letRecValues will have have index $0 in the body. data LetRec' i a ty = LetRec { _letRecInfo :: i, _letRecValues :: !(NonEmpty (LetItem' a ty)), @@ -112,21 +112,21 @@ data LetRec' i a ty = LetRec -- | One-level case matching on the tag of a data constructor: `Case value -- branches default`. `Case` is lazy: only the selected branch is evaluated. -data Case' i bi a = Case +data Case' i bi a ty = Case { _caseInfo :: i, _caseInductive :: Symbol, _caseValue :: !a, - _caseBranches :: ![CaseBranch' bi a], + _caseBranches :: ![CaseBranch' bi a ty], _caseDefault :: !(Maybe a) } -- | `CaseBranch tag binders bindersNum branch` -- - `binders` are the arguments of the constructor tagged with `tag`, -- length of `binders` is equal to `bindersNum` -data CaseBranch' i a = CaseBranch +data CaseBranch' i a ty = CaseBranch { _caseBranchInfo :: i, _caseBranchTag :: !Tag, - _caseBranchBinders :: [Binder' a], + _caseBranchBinders :: [Binder' ty], _caseBranchBindersNum :: !Int, _caseBranchBody :: !a } @@ -248,7 +248,7 @@ instance HasAtomicity (Let' i a ty) where instance HasAtomicity (LetRec' i a ty) where atomicity _ = Aggregate lambdaFixity -instance HasAtomicity (Case' i bi a) where +instance HasAtomicity (Case' i bi a ty) where atomicity _ = Aggregate lambdaFixity instance HasAtomicity (Match' i a) where @@ -329,7 +329,7 @@ instance Eq (Constant' i) where instance Eq a => Eq (App' i a) where (App _ l1 r1) == (App _ l2 r2) = l1 == l2 && r1 == r2 -instance (Eq f, Eq a) => Eq (Apps' f i a) where +instance (Eq f, Eq a) => Eq (Apps' i f a) where (Apps _ op1 args1) == (Apps _ op2 args2) = op1 == op2 && args1 == args2 instance Eq a => Eq (BuiltinApp' i a) where @@ -338,10 +338,10 @@ instance Eq a => Eq (BuiltinApp' i a) where instance Eq a => Eq (Constr' i a) where (Constr _ tag1 args1) == (Constr _ tag2 args2) = tag1 == tag2 && args1 == args2 -instance Eq a => Eq (Case' i bi a) where +instance Eq a => Eq (Case' i bi a ty) where (Case _ sym1 v1 bs1 def1) == (Case _ sym2 v2 bs2 def2) = sym1 == sym2 && v1 == v2 && bs1 == bs2 && def1 == def2 -instance Eq a => Eq (CaseBranch' i a) where +instance Eq a => Eq (CaseBranch' i a ty) where (==) = eqOn (^. caseBranchTag) ..&&.. eqOn (^. caseBranchBody) diff --git a/src/Juvix/Compiler/Core/Language/Stripped.hs b/src/Juvix/Compiler/Core/Language/Stripped.hs index 947836b417..9510b50d3c 100644 --- a/src/Juvix/Compiler/Core/Language/Stripped.hs +++ b/src/Juvix/Compiler/Core/Language/Stripped.hs @@ -29,24 +29,11 @@ data IdentInfo = IdentInfo data ConstrInfo = ConstrInfo { _constrInfoName :: Text, _constrInfoLocation :: Maybe Location, - _constrInfoType :: Type, - _constrInfoInductive :: Symbol - } - -data LetInfo = LetInfo - { _letInfoBinderName :: Text, - _letInfoBinderLocation :: Maybe Location, - _letInfoBinderType :: Type - } - -newtype CaseInfo = CaseInfo - { _caseInfoInductive :: Symbol + _constrInfoType :: Type } data CaseBranchInfo = CaseBranchInfo - { _caseBranchInfoBinderNames :: [Text], - _caseBranchInfoBinderTypes :: [Type], - _caseBranchInfoConstrName :: Text, + { _caseBranchInfoConstrName :: Text, _caseBranchInfoConstrType :: Type } @@ -58,7 +45,7 @@ type Ident = Ident' IdentInfo type Constant = Constant' () -type Apps = Apps' Fun () Node +type Apps = Apps' () Fun Node data Fun = FunVar Var @@ -73,11 +60,11 @@ type Binder = Binder' Type type LetItem = LetItem' Node Type -type Let = Let' LetInfo Node Type +type Let = Let' () Node Type -type Case = Case' CaseInfo CaseBranchInfo Node +type Case = Case' () CaseBranchInfo Node Type -type CaseBranch = CaseBranch' CaseBranchInfo Node +type CaseBranch = CaseBranch' CaseBranchInfo Node Type {---------------------------------------------------------------------------------} @@ -106,6 +93,4 @@ instance HasAtomicity Node where makeLenses ''VarInfo makeLenses ''IdentInfo makeLenses ''ConstrInfo -makeLenses ''LetInfo -makeLenses ''CaseInfo makeLenses ''CaseBranchInfo diff --git a/src/Juvix/Compiler/Core/Language/Stripped/Type.hs b/src/Juvix/Compiler/Core/Language/Stripped/Type.hs index 31a81c6fa0..26a0c55b14 100644 --- a/src/Juvix/Compiler/Core/Language/Stripped/Type.hs +++ b/src/Juvix/Compiler/Core/Language/Stripped/Type.hs @@ -57,10 +57,10 @@ typeArgs = snd . unfoldType typeTarget :: Type -> Type typeTarget = fst . unfoldType -targetIsDynamic :: Type -> Bool -targetIsDynamic ty = typeTarget ty == TyDynamic - --- the number of arguments is statically determinable only if the target is not --- Dynamic typeArgsNum :: Type -> Int typeArgsNum = length . typeArgs + +mkFunType :: [Type] -> Type -> Type +mkFunType tyargs target = case tyargs of + [] -> target + ty : tyargs' -> TyFun (TypeFun ty (mkFunType tyargs' target)) diff --git a/src/Juvix/Compiler/Core/Pipeline.hs b/src/Juvix/Compiler/Core/Pipeline.hs new file mode 100644 index 0000000000..ae4ce79f86 --- /dev/null +++ b/src/Juvix/Compiler/Core/Pipeline.hs @@ -0,0 +1,16 @@ +module Juvix.Compiler.Core.Pipeline + ( module Juvix.Compiler.Core.Pipeline, + module Juvix.Compiler.Core.Data.InfoTable, + ) +where + +import Juvix.Compiler.Core.Data.InfoTable +import Juvix.Compiler.Core.Transformation + +toStrippedTransformations :: [TransformationId] +toStrippedTransformations = [NatToInt, ConvertBuiltinTypes, LambdaLifting, MoveApps, TopEtaExpand, RemoveTypeArgs] + +-- | Perform transformations on Core necessary before the translation to +-- Core.Stripped +toStripped :: InfoTable -> InfoTable +toStripped = applyTransformations toStrippedTransformations diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index 6eed97173a..aff901e084 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -93,7 +93,7 @@ instance PrettyCode Stripped.Fun where Stripped.FunVar x -> ppCodeVar' (x ^. (varInfo . Stripped.varInfoName)) x Stripped.FunIdent x -> ppName KNameLocal (x ^. (identInfo . Stripped.identInfoName)) -instance (PrettyCode f, PrettyCode a, HasAtomicity a) => PrettyCode (Apps' f i a) where +instance (PrettyCode f, PrettyCode a, HasAtomicity a) => PrettyCode (Apps' i f a) where ppCode Apps {..} = do args' <- mapM (ppRightExpression appFixity) _appsArgs n' <- ppCode _appsFun @@ -155,9 +155,9 @@ ppCodeLet' name mty lt = do mempty <+> kwColon <+> ty Nothing -> mempty - return $ kwLet <+> n' <> tty <+> kwAssign <+> v' <+> kwIn <> line <> b' + return $ kwLet <+> n' <> tty <+> kwAssign <+> v' <+> kwIn <+> b' -ppCodeCase' :: (PrettyCode a, Member (Reader Options) r) => [[Text]] -> [Text] -> Case' i bi a -> Sem r (Doc Ann) +ppCodeCase' :: (PrettyCode a, Member (Reader Options) r) => [[Text]] -> [Text] -> Case' i bi a ty -> Sem r (Doc Ann) ppCodeCase' branchBinderNames branchTagNames Case {..} = case _caseBranches of [CaseBranch _ (BuiltinTag TagTrue) _ _ br1, CaseBranch _ (BuiltinTag TagTrue) _ _ br2] -> do @@ -288,7 +288,7 @@ instance PrettyCode Node where NPi Pi {..} -> let piType = _piBinder ^. binderType in case _piBinder ^. binderName of - "" -> do + "?" -> do ty <- ppLeftExpression funFixity piType b <- ppRightExpression funFixity _piBody return $ ty <+> kwArrow <+> b @@ -342,11 +342,11 @@ instance PrettyCode Stripped.Node where let name = x ^. (constrInfo . Stripped.constrInfoName) in ppCodeConstr' name x Stripped.NLet x -> - let name = x ^. (letInfo . Stripped.letInfoBinderName) - ty = x ^. (letInfo . Stripped.letInfoBinderType) + let name = x ^. (letItem . letItemBinder . binderName) + ty = x ^. (letItem . letItemBinder . binderType) in ppCode ty >>= \tty -> ppCodeLet' name (Just tty) x Stripped.NCase x@Stripped.Case {..} -> - let branchBinderNames = map (^. (caseBranchInfo . Stripped.caseBranchInfoBinderNames)) _caseBranches + let branchBinderNames = map (map (^. binderName) . (^. caseBranchBinders)) _caseBranches branchTagNames = map (^. (caseBranchInfo . Stripped.caseBranchInfoConstrName)) _caseBranches in ppCodeCase' branchBinderNames branchTagNames x @@ -392,6 +392,13 @@ instance PrettyCode InfoTable where ctrs <- mapM (fmap (<> semi) . ppCode) (ii ^. inductiveConstructors) return (kwInductive <+> name <+> braces (line <> indent' (vsep ctrs) <> line)) +instance PrettyCode Stripped.ArgumentInfo where + ppCode :: Member (Reader Options) r => Stripped.ArgumentInfo -> Sem r (Doc Ann) + ppCode Stripped.ArgumentInfo {..} = do + name <- ppName KNameLocal _argumentName + ty <- ppCode _argumentType + return $ name <+> colon <+> ty + instance PrettyCode Stripped.InfoTable where ppCode :: forall r. Member (Reader Options) r => Stripped.InfoTable -> Sem r (Doc Ann) ppCode tbl = do @@ -406,8 +413,9 @@ instance PrettyCode Stripped.InfoTable where ppDef :: Symbol -> Stripped.FunctionInfo -> Sem r (Doc Ann) ppDef _ fi = do sym' <- ppName KNameFunction (fi ^. Stripped.functionName) + args <- mapM ppCode (fi ^. Stripped.functionArgsInfo) body' <- ppCode (fi ^. Stripped.functionBody) - return (kwDef <+> sym' <+> kwAssign <+> body') + return (kwDef <+> sym' <> encloseSep lparen rparen ", " args <+> kwAssign <+> body') instance PrettyCode a => PrettyCode (NonEmpty a) where ppCode x = ppCode (toList x) diff --git a/src/Juvix/Compiler/Core/Transformation.hs b/src/Juvix/Compiler/Core/Transformation.hs index b1e1928444..b4f8988d7d 100644 --- a/src/Juvix/Compiler/Core/Transformation.hs +++ b/src/Juvix/Compiler/Core/Transformation.hs @@ -10,6 +10,7 @@ where import Juvix.Compiler.Core.Data.TransformationId import Juvix.Compiler.Core.Transformation.Base +import Juvix.Compiler.Core.Transformation.ConvertBuiltinTypes import Juvix.Compiler.Core.Transformation.Eta import Juvix.Compiler.Core.Transformation.Identity import Juvix.Compiler.Core.Transformation.LambdaLifting @@ -29,3 +30,4 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts RemoveTypeArgs -> removeTypeArgs MoveApps -> moveApps NatToInt -> natToInt + ConvertBuiltinTypes -> convertBuiltinTypes diff --git a/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs b/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs new file mode 100644 index 0000000000..a731ce8b3e --- /dev/null +++ b/src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs @@ -0,0 +1,50 @@ +module Juvix.Compiler.Core.Transformation.ConvertBuiltinTypes + ( convertBuiltinTypes, + module Juvix.Compiler.Core.Transformation.Base, + ) +where + +import Juvix.Compiler.Core.Extra +import Juvix.Compiler.Core.Transformation.Base + +convertNode :: InfoTable -> Node -> Node +convertNode tab = umap go + where + go :: Node -> Node + go node = case node of + NTyp TypeConstr {..} -> + case ii ^. inductiveBuiltin of + Just BuiltinBool -> mkTypeBool' + _ -> node + where + ii = fromJust $ tab ^. infoInductives . at _typeConstrSymbol + _ -> node + +convertIdent :: InfoTable -> IdentifierInfo -> IdentifierInfo +convertIdent tab ii = + ii + { _identifierType = convertNode tab (ii ^. identifierType), + _identifierArgsInfo = map (over argumentType (convertNode tab)) (ii ^. identifierArgsInfo) + } + +convertConstructor :: InfoTable -> ConstructorInfo -> ConstructorInfo +convertConstructor tab = over constructorType (convertNode tab) + +convertInductive :: InfoTable -> InductiveInfo -> InductiveInfo +convertInductive tab ii = + ii + { _inductiveKind = convertNode tab (ii ^. inductiveKind), + _inductiveParams = map (over paramKind (convertNode tab)) (ii ^. inductiveParams), + _inductiveConstructors = map (convertConstructor tab) (ii ^. inductiveConstructors) + } + +convertAxiom :: InfoTable -> AxiomInfo -> AxiomInfo +convertAxiom tab = over axiomType (convertNode tab) + +convertBuiltinTypes :: InfoTable -> InfoTable +convertBuiltinTypes tab = + mapAxioms (convertAxiom tab) $ + mapInductives (convertInductive tab) $ + mapConstructors (convertConstructor tab) $ + mapIdents (convertIdent tab) $ + mapT (const (convertNode tab)) tab diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs index 26afc4ffd6..7929b72bcd 100644 --- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs +++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs @@ -7,6 +7,7 @@ where import Juvix.Compiler.Core.Data.BinderList qualified as BL import Juvix.Compiler.Core.Data.InfoTableBuilder import Juvix.Compiler.Core.Extra +import Juvix.Compiler.Core.Info.NameInfo import Juvix.Compiler.Core.Pretty import Juvix.Compiler.Core.Transformation.Base @@ -45,7 +46,7 @@ lambdaLiftNode aboveBl top = allfreevars :: [Var] allfreevars = map fst freevarsAssocs argsInfo :: [ArgumentInfo] - argsInfo = map (argumentInfoFromBinder . snd) freevarsAssocs + argsInfo = map (argumentInfoFromBinder . (^. lambdaLhsBinder)) (fst (unfoldLambdas fBody')) f <- freshSymbol let name = uniqueName "lambda" f registerIdent @@ -55,13 +56,13 @@ lambdaLiftNode aboveBl top = _identifierName = name, _identifierLocation = Nothing, _identifierType = typeFromArgs argsInfo, - _identifierArgsNum = length allfreevars, + _identifierArgsNum = length argsInfo, _identifierArgsInfo = argsInfo, _identifierIsExported = False, _identifierBuiltin = Nothing } registerIdentNode f fBody' - let fApp = mkApps' (mkIdent mempty f) (map NVar allfreevars) + let fApp = mkApps' (mkIdent (setInfoName name mempty) f) (map NVar allfreevars) return (End fApp) goLetRec :: LetRec -> Sem r Recur @@ -73,9 +74,13 @@ lambdaLiftNode aboveBl top = letRecBinders' :: [Binder] <- mapM (lambdaLiftBinder bl) (letr ^.. letRecValues . each . letItemBinder) let bl' :: BinderList Binder -- the reverse is necessary because the last item in letRecBinders has index 0 - bl' = BL.prependRev (reverse letRecBinders') bl + bl' = BL.prependRev letRecBinders' bl topSyms :: [Symbol] <- forM defs (const freshSymbol) + let topNames :: [Text] + topNames = zipWithExact uniqueName (map (^. binderName) letRecBinders') topSyms + topSymsWithName = zipExact topSyms topNames + let recItemsFreeVars :: [(Var, Binder)] recItemsFreeVars = mapMaybe helper (concatMap (freeVarsCtx' bl') defs) where @@ -86,14 +91,14 @@ lambdaLiftNode aboveBl top = where idx' = (v ^. varIndex) - ndefs + letItems :: [Node] + letItems = + [ mkApps' (mkIdent (setInfoName name mempty) sym) (map (NVar . fst) recItemsFreeVars) + | (sym, name) <- topSymsWithName + ] + subsCalls :: Node -> Node - subsCalls = - substs - ( reverse - [ mkApps' (mkIdent' sym) (map (NVar . fst) recItemsFreeVars) - | sym <- topSyms - ] - ) + subsCalls = substs (reverse letItems) -- NOTE that we are first substituting the calls and then performing -- lambda lifting. This is a tradeoff. We have slower compilation but -- slightly faster execution time, since it minimizes the number of @@ -106,8 +111,8 @@ lambdaLiftNode aboveBl top = [ do let topBody = captureFreeVars (map (first (^. varIndex)) recItemsFreeVars) b argsInfo :: [ArgumentInfo] - argsInfo = map (argumentInfoFromBinder . snd) recItemsFreeVars - name = uniqueName (itemBinder ^. binderName) sym + argsInfo = + map (argumentInfoFromBinder . (^. lambdaLhsBinder)) (fst (unfoldLambdas topBody)) registerIdentNode sym topBody registerIdent name @@ -116,34 +121,31 @@ lambdaLiftNode aboveBl top = _identifierName = name, _identifierLocation = itemBinder ^. binderLocation, _identifierType = typeFromArgs argsInfo, - _identifierArgsNum = length recItemsFreeVars, + _identifierArgsNum = length argsInfo, _identifierArgsInfo = argsInfo, _identifierIsExported = False, _identifierBuiltin = Nothing } - | (sym, (itemBinder, b)) <- zipExact topSyms (zipExact letRecBinders' liftedDefs) + | ((sym, name), (itemBinder, b)) <- zipExact topSymsWithName (zipExact letRecBinders' liftedDefs) ] - letItems :: [Node] - letItems = - let fv = recItemsFreeVars - in [ mkApps' (mkIdent' s) (map (NVar . fst) fv) - | s <- topSyms - ] declareTopSyms let -- TODO it can probably be simplified - shiftHelper :: Node -> NonEmpty Node -> Node + shiftHelper :: Node -> NonEmpty (Node, Binder) -> Node shiftHelper b = goShift 0 where - goShift :: Int -> NonEmpty Node -> Node + goShift :: Int -> NonEmpty (Node, Binder) -> Node goShift k = \case - x :| yys -> case yys of + (x, bnd) :| yys -> case yys of [] - | k == ndefs - 1 -> mkLet' (shift k x) b + | k == ndefs - 1 -> mkLet mempty bnd' (shift k x) b | otherwise -> impossible - (y : ys) -> mkLet' (shift k x) (goShift (k + 1) (y :| ys)) + (y : ys) -> mkLet mempty bnd' (shift k x) (goShift (k + 1) (y :| ys)) + where + bnd' = over binderType (shift k . subsCalls . shift (-ndefs)) bnd + -- TODO: the types should also be lambda-lifted let res :: Node - res = shiftHelper body' (nonEmpty' letItems) + res = shiftHelper body' (nonEmpty' (zipExact letItems letRecBinders')) return (Recur res) lambdaLifting :: InfoTable -> InfoTable diff --git a/src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs b/src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs index f816ded695..d933626dcb 100644 --- a/src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs +++ b/src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs @@ -87,12 +87,17 @@ convertIdent :: InfoTable -> IdentifierInfo -> IdentifierInfo convertIdent tab ii = ii { _identifierType = ty', - _identifierArgsInfo = map (over argumentType (convertNode tab) . fst) $ filter (not . isTypeConstr . snd) (zipExact (ii ^. identifierArgsInfo) tyargs), + _identifierArgsInfo = + map (uncurry (set argumentType)) $ + zipExact tyargs' $ + map fst $ + filter (not . isTypeConstr . snd) (zipExact (ii ^. identifierArgsInfo) tyargs), _identifierArgsNum = length (typeArgs ty') } where tyargs = typeArgs (ii ^. identifierType) ty' = convertNode tab (ii ^. identifierType) + tyargs' = typeArgs ty' convertConstructor :: InfoTable -> ConstructorInfo -> ConstructorInfo convertConstructor tab ci = diff --git a/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs b/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs index 1416366ff6..822fb6ef69 100644 --- a/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs +++ b/src/Juvix/Compiler/Core/Transformation/TopEtaExpand.hs @@ -22,9 +22,9 @@ topEtaExpand info = run (mapT' go info) NLam l -> NLam <$> traverseOf lambdaBody (skipLambdas as) l _ -> do let newArgsInfo :: [ArgumentInfo] - newArgsInfo = map toArgumentInfo as + newArgsInfo = map toArgumentInfo args overIdentArgsInfo sym (++ newArgsInfo) - return (expand node (reverse args)) + return (expand node args) toArgumentInfo :: PiLhs -> ArgumentInfo toArgumentInfo pi = ArgumentInfo diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs index 6ff592c7c5..e66b9a2620 100644 --- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs +++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs @@ -576,7 +576,7 @@ goFunction (params, returnTypeExpr) = foldr f (goExpression returnTypeExpr) para where f :: Internal.FunctionParameter -> Sem r Node -> Sem r Node f param acc = do - paramBinder <- Binder (maybe "" (^. nameText) $ param ^. Internal.paramName) (fmap (^. nameLoc) $ param ^. Internal.paramName) <$> goExpression (param ^. Internal.paramType) + paramBinder <- Binder (maybe "?" (^. nameText) $ param ^. Internal.paramName) (fmap (^. nameLoc) $ param ^. Internal.paramName) <$> goExpression (param ^. Internal.paramType) case param ^. Internal.paramName of Nothing -> mkPi mempty paramBinder <$> acc Just vn -> mkPi mempty paramBinder <$> localAddName vn acc diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs index a4005dbad0..4bf264e459 100644 --- a/src/Juvix/Compiler/Core/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs @@ -34,6 +34,35 @@ runParser fileName tab input = (_, Left err) -> Left (ParserError err) (tbl, Right r) -> Right (tbl, r) +runParserMain :: FilePath -> InfoTable -> Text -> Either ParserError InfoTable +runParserMain fileName tab input = + case runParser fileName tab input of + Left err -> Left err + Right (tab', Nothing) -> Right tab' + Right (tab', Just node) -> Right $ setupMainFunction tab' node + +setupMainFunction :: InfoTable -> Node -> InfoTable +setupMainFunction tab node = + tab + { _infoMain = Just sym, + _identContext = HashMap.insert sym node (tab ^. identContext), + _infoIdentifiers = HashMap.insert sym info (tab ^. infoIdentifiers), + _infoNextSymbol = tab ^. infoNextSymbol + 1 + } + where + sym = tab ^. infoNextSymbol + info = + IdentifierInfo + { _identifierName = "main", + _identifierLocation = Nothing, + _identifierSymbol = sym, + _identifierArgsNum = 0, + _identifierArgsInfo = [], + _identifierType = mkDynamic', + _identifierBuiltin = Nothing, + _identifierIsExported = True + } + guardSymbolNotDefined :: Member InfoTableBuilder r => Symbol -> diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs index f9326760b3..71e0922fbb 100644 --- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs +++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs @@ -1,16 +1,193 @@ -module Juvix.Compiler.Core.Translation.Stripped.FromCore where +module Juvix.Compiler.Core.Translation.Stripped.FromCore (fromCore) where +import Data.HashMap.Strict qualified as HashMap import Juvix.Compiler.Core.Data.InfoTable import Juvix.Compiler.Core.Data.Stripped.InfoTable qualified as Stripped +import Juvix.Compiler.Core.Extra import Juvix.Compiler.Core.Extra.Stripped.Base qualified as Stripped +import Juvix.Compiler.Core.Info.LocationInfo +import Juvix.Compiler.Core.Info.NameInfo import Juvix.Compiler.Core.Language import Juvix.Compiler.Core.Language.Stripped qualified as Stripped -fromMain :: InfoTable -> Stripped.InfoTable -fromMain = error "not yet implemented" +fromCore :: InfoTable -> Stripped.InfoTable +fromCore tab = + Stripped.InfoTable + { _infoMain = tab ^. infoMain, + _infoFunctions = fmap (translateFunctionInfo tab) (tab ^. infoIdentifiers), + _infoInductives = fmap translateInductiveInfo (tab ^. infoInductives), + _infoConstructors = fmap translateConstructorInfo (tab ^. infoConstructors) + } + +translateFunctionInfo :: InfoTable -> IdentifierInfo -> Stripped.FunctionInfo +translateFunctionInfo tab IdentifierInfo {..} = + Stripped.FunctionInfo + { _functionName = _identifierName, + _functionLocation = _identifierLocation, + _functionSymbol = _identifierSymbol, + _functionBody = + translateFunction + _identifierArgsNum + (fromJust $ HashMap.lookup _identifierSymbol (tab ^. identContext)), + _functionType = translateType _identifierType, + _functionArgsNum = _identifierArgsNum, + _functionArgsInfo = map translateArgInfo _identifierArgsInfo, + _functionIsExported = _identifierIsExported + } + +translateArgInfo :: ArgumentInfo -> Stripped.ArgumentInfo +translateArgInfo ArgumentInfo {..} = + Stripped.ArgumentInfo + { _argumentName = _argumentName, + _argumentLocation = _argumentLocation, + _argumentType = translateType _argumentType + } + +translateInductiveInfo :: InductiveInfo -> Stripped.InductiveInfo +translateInductiveInfo InductiveInfo {..} = + Stripped.InductiveInfo + { _inductiveName = _inductiveName, + _inductiveLocation = _inductiveLocation, + _inductiveSymbol = _inductiveSymbol, + _inductiveKind = translateType _inductiveKind, + _inductiveConstructors = map translateConstructorInfo _inductiveConstructors, + _inductiveParams = map translateParamInfo _inductiveParams + } + +translateParamInfo :: ParameterInfo -> Stripped.ParameterInfo +translateParamInfo ParameterInfo {..} = + Stripped.ParameterInfo + { _paramName = _paramName, + _paramLocation = _paramLocation, + _paramKind = translateType _paramKind, + _paramIsImplicit = _paramIsImplicit + } + +translateConstructorInfo :: ConstructorInfo -> Stripped.ConstructorInfo +translateConstructorInfo ConstructorInfo {..} = + Stripped.ConstructorInfo + { _constructorName = _constructorName, + _constructorLocation = _constructorLocation, + _constructorInductive = _constructorInductive, + _constructorTag = _constructorTag, + _constructorType = translateType _constructorType + } + +translateFunction :: Int -> Node -> Stripped.Node +translateFunction argsNum node = + let (k, body) = unfoldLambdas' node + in if + | k /= argsNum -> error "wrong number of arguments" + | otherwise -> translateNode body translateNode :: Node -> Stripped.Node -translateNode _ = Stripped.mkVar' 0 +translateNode node = case node of + NVar v -> + Stripped.NVar $ translateVar v + NIdt idt -> + Stripped.NIdt $ translateIdent idt + NCst Constant {..} -> + Stripped.mkConstant _constantValue + NApp App {} -> + let (tgt, args) = unfoldApps' node + args' = map translateNode args + in case tgt of + NVar v -> Stripped.mkApps (Stripped.FunVar $ translateVar v) args' + NIdt idt -> Stripped.mkApps (Stripped.FunIdent $ translateIdent idt) args' + _ -> unsupported + NBlt BuiltinApp {..} -> + Stripped.mkBuiltinApp _builtinAppOp (map translateNode _builtinAppArgs) + NCtr Constr {..} -> + Stripped.mkConstr + ( Stripped.ConstrInfo + { _constrInfoName = getInfoName _constrInfo, + _constrInfoLocation = getInfoLocation _constrInfo, + _constrInfoType = Stripped.TyDynamic + } + ) + _constrTag + (map translateNode _constrArgs) + NLet Let {..} -> + Stripped.mkLet + ( Stripped.Binder + { _binderName = _letItem ^. letItemBinder . binderName, + _binderLocation = _letItem ^. letItemBinder . binderLocation, + _binderType = translateType (_letItem ^. letItemBinder . binderType) + } + ) + (translateNode (_letItem ^. letItemValue)) + (translateNode _letBody) + NCase Case {..} -> + Stripped.mkCase + _caseInductive + (translateNode _caseValue) + (map translateCaseBranch _caseBranches) + (fmap translateNode _caseDefault) + _ + | isType node -> + Stripped.mkConstr (Stripped.ConstrInfo "()" Nothing Stripped.TyDynamic) (BuiltinTag TagTrue) [] + _ -> + unsupported + where + unsupported :: a + unsupported = error "Core to Core.Stripped: unsupported node" + + translateCaseBranch :: CaseBranch -> Stripped.CaseBranch + translateCaseBranch CaseBranch {..} = + Stripped.CaseBranch + { _caseBranchInfo = + Stripped.CaseBranchInfo + { _caseBranchInfoConstrName = getInfoName _caseBranchInfo, + _caseBranchInfoConstrType = Stripped.TyDynamic + }, + _caseBranchTag = _caseBranchTag, + _caseBranchBinders = map (over binderType translateType) _caseBranchBinders, + _caseBranchBindersNum = _caseBranchBindersNum, + _caseBranchBody = translateNode _caseBranchBody + } + + translateVar :: Var -> Stripped.Var + translateVar Var {..} = + Stripped.Var + ( Stripped.VarInfo + { _varInfoName = getInfoName _varInfo, + _varInfoLocation = getInfoLocation _varInfo, + _varInfoType = Stripped.TyDynamic + } + ) + _varIndex + + translateIdent :: Ident -> Stripped.Ident + translateIdent Ident {..} = + Stripped.Ident + ( Stripped.IdentInfo + { _identInfoName = getInfoName _identInfo, + _identInfoLocation = getInfoLocation _identInfo, + _identInfoType = Stripped.TyDynamic + } + ) + _identSymbol translateType :: Node -> Stripped.Type -translateType _ = error "not yet implemented" +translateType node = case node of + NVar {} -> + Stripped.TyDynamic + NPi Pi {} -> + let (args, tgt) = unfoldPi node + tyargs = map (^. piLhsBinder . binderType) args + in Stripped.mkFunType (map translateType tyargs) (translateType tgt) + NUniv Univ {} -> + Stripped.TyDynamic + NTyp TypeConstr {..} -> + Stripped.TyApp $ + Stripped.TypeApp + { _typeAppName = getInfoName _typeConstrInfo, + _typeAppLocation = getInfoLocation _typeConstrInfo, + _typeAppSymbol = _typeConstrSymbol, + _typeAppArgs = map translateType _typeConstrArgs + } + NPrim TypePrim {..} -> + Stripped.TyPrim _typePrimPrimitive + NDyn Dynamic {} -> + Stripped.TyDynamic + _ -> error "Core to Core.Stripped: unsupported type" diff --git a/src/Juvix/Compiler/Pipeline.hs b/src/Juvix/Compiler/Pipeline.hs index a5b9e0394e..db83ea1e8b 100644 --- a/src/Juvix/Compiler/Pipeline.hs +++ b/src/Juvix/Compiler/Pipeline.hs @@ -8,6 +8,7 @@ where import Juvix.Compiler.Abstract.Translation qualified as Abstract import Juvix.Compiler.Asm.Pipeline qualified as Asm +import Juvix.Compiler.Asm.Translation.FromCore qualified as Asm import Juvix.Compiler.Backend qualified as Backend import Juvix.Compiler.Backend.C qualified as C import Juvix.Compiler.Builtins @@ -16,7 +17,9 @@ import Juvix.Compiler.Concrete.Translation.FromParsed qualified as Scoper import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver import Juvix.Compiler.Concrete.Translation.FromSource qualified as Parser import Juvix.Compiler.Core.Language qualified as Core +import Juvix.Compiler.Core.Pipeline qualified as Core import Juvix.Compiler.Core.Translation qualified as Core +import Juvix.Compiler.Core.Translation.Stripped.FromCore qualified as Stripped import Juvix.Compiler.Internal qualified as Internal import Juvix.Compiler.Pipeline.Artifacts import Juvix.Compiler.Pipeline.EntryPoint @@ -161,6 +164,9 @@ upToMiniC = upToInternalReachability >>= C.fromInternal -- Internal workflows -------------------------------------------------------------------------------- +coreToMiniC :: Member (Error JuvixError) r => Asm.Options -> Core.InfoTable -> Sem r C.MiniCResult +coreToMiniC opts = asmToMiniC opts . Asm.fromCore . Stripped.fromCore . Core.toStripped + asmToMiniC :: Member (Error JuvixError) r => Asm.Options -> Asm.InfoTable -> Sem r C.MiniCResult asmToMiniC opts = Asm.toReg opts >=> regToMiniC (opts ^. Asm.optLimits) . Reg.fromAsm diff --git a/src/Juvix/Compiler/Reg/Extra.hs b/src/Juvix/Compiler/Reg/Extra.hs index 7c821f1c14..d949d5c7fd 100644 --- a/src/Juvix/Compiler/Reg/Extra.hs +++ b/src/Juvix/Compiler/Reg/Extra.hs @@ -58,7 +58,7 @@ computeMaxStackHeight lims = maximum . map go (maybe 0 (computeMaxStackHeight lims) _instrCaseDefault) computeStringMap :: HashMap Text Int -> Code -> HashMap Text Int -computeStringMap strs = snd . run . execState (0 :: Int, strs) . mapM go +computeStringMap strs = snd . run . execState (HashMap.size strs, strs) . mapM go where go :: Member (State (Int, HashMap Text Int)) r => Instruction -> Sem r () go = \case diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs index f4b1cc3fa4..5486a754e3 100644 --- a/src/Juvix/Extra/Strings.hs +++ b/src/Juvix/Extra/Strings.hs @@ -495,7 +495,7 @@ instrTccall :: IsString s => s instrTccall = "tccall" instrReturn :: IsString s => s -instrReturn = "return" +instrReturn = "ret" instrBr :: IsString s => s instrBr = "br" diff --git a/test/Asm/Compile/Base.hs b/test/Asm/Compile/Base.hs index 758f726865..e63fcb575b 100644 --- a/test/Asm/Compile/Base.hs +++ b/test/Asm/Compile/Base.hs @@ -2,6 +2,7 @@ module Asm.Compile.Base where import Base import Data.Text.IO qualified as TIO +import Juvix.Compiler.Asm.Data.InfoTable import Juvix.Compiler.Asm.Options import Juvix.Compiler.Asm.Translation.FromSource import Juvix.Compiler.Backend qualified as Backend @@ -9,23 +10,26 @@ import Juvix.Compiler.Backend.C qualified as C import Juvix.Compiler.Pipeline qualified as Pipeline import Runtime.Base qualified as Runtime +asmCompileAssertion' :: InfoTable -> Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion +asmCompileAssertion' tab mainFile expectedFile step = do + step "Generate C code" + case run $ runError @JuvixError $ Pipeline.asmToMiniC asmOpts tab of + Left {} -> assertFailure "code generation failed" + Right C.MiniCResult {..} -> + withTempDir' + ( \dirPath -> do + let cFile = dirPath replaceExtension' ".c" (filename mainFile) + TIO.writeFile (toFilePath cFile) _resultCCode + Runtime.clangAssertion cFile expectedFile "" step + ) + where + asmOpts :: Options + asmOpts = makeOptions Backend.TargetCNative64 True + asmCompileAssertion :: Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion asmCompileAssertion mainFile expectedFile step = do step "Parse" s <- readFile (toFilePath mainFile) case runParser (toFilePath mainFile) s of Left err -> assertFailure (show err) - Right tab -> do - step "Generate C code" - case run $ runError @JuvixError $ Pipeline.asmToMiniC asmOpts tab of - Left {} -> assertFailure "code generation failed" - Right C.MiniCResult {..} -> - withTempDir' - ( \dirPath -> do - let cFile = dirPath replaceExtension' ".c" (filename mainFile) - TIO.writeFile (toFilePath cFile) _resultCCode - Runtime.clangAssertion cFile expectedFile "" step - ) - where - asmOpts :: Options - asmOpts = makeOptions Backend.TargetCNative64 True + Right tab -> asmCompileAssertion' tab mainFile expectedFile step diff --git a/test/Asm/Run/Base.hs b/test/Asm/Run/Base.hs index e25af5ae16..53c4f0a169 100644 --- a/test/Asm/Run/Base.hs +++ b/test/Asm/Run/Base.hs @@ -11,6 +11,36 @@ import Juvix.Compiler.Asm.Transformation.Validate import Juvix.Compiler.Asm.Translation.FromSource import Juvix.Data.PPOutput +asmRunAssertion' :: InfoTable -> Path Abs File -> (String -> IO ()) -> Assertion +asmRunAssertion' tab expectedFile step = do + step "Validate" + case validate' tab of + Just err -> assertFailure (show (pretty err)) + Nothing -> + case tab ^. infoMainFunction of + Just sym -> do + withTempDir' + ( \dirPath -> do + let outputFile = dirPath $(mkRelFile "out.out") + hout <- openFile (toFilePath outputFile) WriteMode + step "Interpret" + r' <- doRun hout tab (getFunInfo tab sym) + case r' of + Left err -> do + hClose hout + assertFailure (show (pretty err)) + Right value' -> do + case value' of + ValVoid -> return () + _ -> hPutStrLn hout (ppPrint tab value') + hClose hout + actualOutput <- TIO.readFile (toFilePath outputFile) + step "Compare expected and actual program output" + expected <- TIO.readFile (toFilePath expectedFile) + assertEqDiff ("Check: RUN output = " <> toFilePath expectedFile) actualOutput expected + ) + Nothing -> assertFailure "no 'main' function" + asmRunAssertion :: Path Abs File -> Path Abs File -> (InfoTable -> Either AsmError InfoTable) -> (InfoTable -> Assertion) -> (String -> IO ()) -> Assertion asmRunAssertion mainFile expectedFile trans testTrans step = do step "Parse" @@ -22,33 +52,7 @@ asmRunAssertion mainFile expectedFile trans testTrans step = do Left err -> assertFailure (show (pretty err)) Right tab -> do testTrans tab - step "Validate" - case validate' tab of - Just err -> assertFailure (show (pretty err)) - Nothing -> - case tab ^. infoMainFunction of - Just sym -> do - withTempDir' - ( \dirPath -> do - let outputFile = dirPath $(mkRelFile "out.out") - hout <- openFile (toFilePath outputFile) WriteMode - step "Interpret" - r' <- doRun hout tab (getFunInfo tab sym) - case r' of - Left err -> do - hClose hout - assertFailure (show (pretty err)) - Right value' -> do - case value' of - ValVoid -> return () - _ -> hPutStrLn hout (ppPrint tab value') - hClose hout - actualOutput <- TIO.readFile (toFilePath outputFile) - step "Compare expected and actual program output" - expected <- TIO.readFile (toFilePath expectedFile) - assertEqDiff ("Check: RUN output = " <> toFilePath expectedFile) actualOutput expected - ) - Nothing -> assertFailure "no 'main' function" + asmRunAssertion' tab expectedFile step asmRunErrorAssertion :: Path Abs File -> (String -> IO ()) -> Assertion asmRunErrorAssertion mainFile step = do diff --git a/test/Core.hs b/test/Core.hs index 6d6c26ea04..a42e321480 100644 --- a/test/Core.hs +++ b/test/Core.hs @@ -1,8 +1,10 @@ module Core where import Base +import Core.Asm qualified as Asm +import Core.Compile qualified as Compile import Core.Eval qualified as Eval import Core.Transformation qualified as Transformation allTests :: TestTree -allTests = testGroup "JuvixCore tests" [Eval.allTests, Transformation.allTests] +allTests = testGroup "JuvixCore tests" [Eval.allTests, Transformation.allTests, Asm.allTests, Compile.allTests] diff --git a/test/Core/Asm.hs b/test/Core/Asm.hs new file mode 100644 index 0000000000..123a0fd2ae --- /dev/null +++ b/test/Core/Asm.hs @@ -0,0 +1,7 @@ +module Core.Asm where + +import Base +import Core.Asm.Positive qualified as P + +allTests :: TestTree +allTests = testGroup "JuvixCore to JuvixAsm translation" [P.allTests] diff --git a/test/Core/Asm/Base.hs b/test/Core/Asm/Base.hs new file mode 100644 index 0000000000..13e9cb012e --- /dev/null +++ b/test/Core/Asm/Base.hs @@ -0,0 +1,53 @@ +module Core.Asm.Base where + +import Asm.Run.Base qualified as Asm +import Base +import Core.Eval.Base +import Core.Eval.Positive qualified as Eval +import Data.Text.IO qualified as TIO +import Juvix.Compiler.Asm.Translation.FromCore qualified as Asm +import Juvix.Compiler.Core.Pipeline +import Juvix.Compiler.Core.Translation.FromSource +import Juvix.Compiler.Core.Translation.Stripped.FromCore qualified as Stripped +import Juvix.Data.PPOutput + +newtype Test = Test + { _testEval :: Eval.PosTest + } + +fromTest :: Test -> TestTree +fromTest = mkTest . toTestDescr + +root :: Path Abs Dir +root = relToProject $(mkRelDir "tests/Core/positive/") + +toTestDescr :: Test -> TestDescr +toTestDescr Test {..} = + let Eval.PosTest {..} = _testEval + tRoot = root _relDir + file' = tRoot _file + expected' = tRoot _expectedFile + in TestDescr + { _testName = _name, + _testRoot = tRoot, + _testAssertion = Steps $ coreAsmAssertion file' expected' + } + +coreAsmAssertion :: + Path Abs File -> + Path Abs File -> + (String -> IO ()) -> + Assertion +coreAsmAssertion mainFile expectedFile step = do + step "Parse" + r <- parseFile mainFile + case r of + Left err -> assertFailure (show (pretty err)) + Right (_, Nothing) -> do + step "Empty program: compare expected and actual program output" + expected <- TIO.readFile (toFilePath expectedFile) + assertEqDiff ("Check: EVAL output = " <> toFilePath expectedFile) "" expected + Right (tabIni, Just node) -> do + step "Translate" + let tab = Asm.fromCore $ Stripped.fromCore $ toStripped $ setupMainFunction tabIni node + Asm.asmRunAssertion' tab expectedFile step diff --git a/test/Core/Asm/Positive.hs b/test/Core/Asm/Positive.hs new file mode 100644 index 0000000000..d05ce688e4 --- /dev/null +++ b/test/Core/Asm/Positive.hs @@ -0,0 +1,20 @@ +module Core.Asm.Positive where + +import Base +import Core.Asm.Base +import Core.Eval.Positive qualified as Eval + +allTests :: TestTree +allTests = testGroup "JuvixCore to JuvixAsm positive tests" (map liftTest (Eval.filterOutTests ignoredTests Eval.tests)) + +ignoredTests :: [String] +ignoredTests = + [ "Match with complex patterns" + ] + +liftTest :: Eval.PosTest -> TestTree +liftTest _testEval = + fromTest + Test + { _testEval + } diff --git a/test/Core/Compile.hs b/test/Core/Compile.hs new file mode 100644 index 0000000000..ab9592f7e2 --- /dev/null +++ b/test/Core/Compile.hs @@ -0,0 +1,7 @@ +module Core.Compile where + +import Base +import Core.Compile.Positive qualified as P + +allTests :: TestTree +allTests = testGroup "JuvixCore compile" [P.allTests] diff --git a/test/Core/Compile/Base.hs b/test/Core/Compile/Base.hs new file mode 100644 index 0000000000..1e137280d1 --- /dev/null +++ b/test/Core/Compile/Base.hs @@ -0,0 +1,53 @@ +module Core.Compile.Base where + +import Asm.Compile.Base qualified as Asm +import Base +import Core.Eval.Base +import Core.Eval.Positive qualified as Eval +import Data.Text.IO qualified as TIO +import Juvix.Compiler.Asm.Translation.FromCore qualified as Asm +import Juvix.Compiler.Core.Pipeline +import Juvix.Compiler.Core.Translation.FromSource +import Juvix.Compiler.Core.Translation.Stripped.FromCore qualified as Stripped +import Juvix.Data.PPOutput + +newtype Test = Test + { _testEval :: Eval.PosTest + } + +fromTest :: Test -> TestTree +fromTest = mkTest . toTestDescr + +root :: Path Abs Dir +root = relToProject $(mkRelDir "tests/Core/positive/") + +toTestDescr :: Test -> TestDescr +toTestDescr Test {..} = + let Eval.PosTest {..} = _testEval + tRoot = root _relDir + file' = tRoot _file + expected' = tRoot _expectedFile + in TestDescr + { _testName = _name, + _testRoot = tRoot, + _testAssertion = Steps $ coreCompileAssertion file' expected' + } + +coreCompileAssertion :: + Path Abs File -> + Path Abs File -> + (String -> IO ()) -> + Assertion +coreCompileAssertion mainFile expectedFile step = do + step "Parse" + r <- parseFile mainFile + case r of + Left err -> assertFailure (show (pretty err)) + Right (_, Nothing) -> do + step "Empty program: compare expected and actual program output" + expected <- TIO.readFile (toFilePath expectedFile) + assertEqDiff ("Check: EVAL output = " <> toFilePath expectedFile) "" expected + Right (tabIni, Just node) -> do + step "Translate to JuvixAsm" + let tab = Asm.fromCore $ Stripped.fromCore $ toStripped $ setupMainFunction tabIni node + Asm.asmCompileAssertion' tab mainFile expectedFile step diff --git a/test/Core/Compile/Positive.hs b/test/Core/Compile/Positive.hs new file mode 100644 index 0000000000..4b1804f936 --- /dev/null +++ b/test/Core/Compile/Positive.hs @@ -0,0 +1,27 @@ +module Core.Compile.Positive where + +import Base +import Core.Compile.Base +import Core.Eval.Positive qualified as Eval + +allTests :: TestTree +allTests = testGroup "JuvixCore compilation tests" (map liftTest (Eval.filterOutTests ignoredTests Eval.tests)) + +-- Arbitrary precision integers and general pattern matching not yet supported +ignoredTests :: [String] +ignoredTests = + [ "Tail recursion: Fibonacci numbers in linear time", + "Fast exponentiation", + "Nested 'case', 'let' and 'if' with variable capture", + "Mutual recursion", + "LetRec", + "Big numbers", + "Match with complex patterns" + ] + +liftTest :: Eval.PosTest -> TestTree +liftTest _testEval = + fromTest + Test + { _testEval + } diff --git a/test/Core/Eval/Base.hs b/test/Core/Eval/Base.hs index fc485e2d6d..6b18d18f30 100644 --- a/test/Core/Eval/Base.hs +++ b/test/Core/Eval/Base.hs @@ -31,14 +31,15 @@ coreEvalAssertion mainFile expectedFile trans testTrans step = do expected <- TIO.readFile (toFilePath expectedFile) assertEqDiff ("Check: EVAL output = " <> toFilePath expectedFile) "" expected Right (tabIni, Just node) -> do - let tab = applyTransformations trans tabIni + let tab = applyTransformations trans (setupMainFunction tabIni node) testTrans tab + let node' = fromJust $ tab ^. identContext . at (fromJust $ tab ^. infoMain) withTempDir' ( \dirPath -> do let outputFile = dirPath $(mkRelFile "out.out") hout <- openFile (toFilePath outputFile) WriteMode step "Evaluate" - r' <- doEval mainFile hout tab node + r' <- doEval mainFile hout tab node' case r' of Left err -> do hClose hout diff --git a/test/Core/Eval/Positive.hs b/test/Core/Eval/Positive.hs index 2090606c9b..544db7781f 100644 --- a/test/Core/Eval/Positive.hs +++ b/test/Core/Eval/Positive.hs @@ -24,6 +24,9 @@ testDescr PosTest {..} = _testAssertion = Steps $ coreEvalAssertion file' expected' [] (const (return ())) } +filterOutTests :: [String] -> [PosTest] -> [PosTest] +filterOutTests out = filter (\PosTest {..} -> _name `notElem` out) + allTests :: TestTree allTests = testGroup diff --git a/test/Core/Transformation/Pipeline.hs b/test/Core/Transformation/Pipeline.hs index 9238a95dea..04069acfb5 100644 --- a/test/Core/Transformation/Pipeline.hs +++ b/test/Core/Transformation/Pipeline.hs @@ -3,13 +3,14 @@ module Core.Transformation.Pipeline (allTests) where import Base import Core.Eval.Positive qualified as Eval import Core.Transformation.Base +import Juvix.Compiler.Core.Pipeline import Juvix.Compiler.Core.Transformation allTests :: TestTree allTests = testGroup "Transformation pipeline" (map liftTest Eval.tests) pipe :: [TransformationId] -pipe = [NatToInt, LambdaLifting, MoveApps, RemoveTypeArgs, TopEtaExpand] +pipe = toStrippedTransformations liftTest :: Eval.PosTest -> TestTree liftTest _testEval = diff --git a/tests/Core/positive/out/test009.out b/tests/Core/positive/out/test009.out index 0aeb73169b..dbaf7f94b8 100644 --- a/tests/Core/positive/out/test009.out +++ b/tests/Core/positive/out/test009.out @@ -1,5 +1,4 @@ 50005000 -5000050000 120 3628800 -93326215443944152681699238856266700490715968264381621468592963895217599993229915608941463976156518286253697920827223758251185210916864000000000000000000000000 +479001600 diff --git a/tests/Core/positive/out/test017.out b/tests/Core/positive/out/test017.out index b7a2459a37..b9d569380c 100644 --- a/tests/Core/positive/out/test017.out +++ b/tests/Core/positive/out/test017.out @@ -1,2 +1 @@ 50005000 -5000050000 diff --git a/tests/Core/positive/out/test023.out b/tests/Core/positive/out/test023.out index f3a9cf67e2..62660ff383 100644 --- a/tests/Core/positive/out/test023.out +++ b/tests/Core/positive/out/test023.out @@ -2,9 +2,6 @@ cons 10 (cons 9 (cons 8 (cons 7 (cons 6 (cons 5 (cons 4 (cons 3 (cons 2 (cons 1 cons 1 (cons 2 (cons 3 (cons 4 (cons 5 (cons 6 (cons 7 (cons 8 (cons 9 (cons 10 nil))))))))) cons 10 (cons 9 (cons 8 (cons 7 (cons 6 nil)))) cons 0 (cons 1 (cons 2 (cons 3 (cons 4 (cons 5 (cons 6 (cons 7 (cons 8 (cons 9 nil))))))))) -50005000 -5000050000 -50005000 -5000050000 -50005000 -5000050000 +500500 +500500 +500500 diff --git a/tests/Core/positive/out/test026.out b/tests/Core/positive/out/test026.out index a5e1d4be0b..da66482945 100644 --- a/tests/Core/positive/out/test026.out +++ b/tests/Core/positive/out/test026.out @@ -2,5 +2,3 @@ -1448007509520 5510602057585725 -85667472308246220 -527851146861989286336 --441596546382859135501706333021475 diff --git a/tests/Core/positive/out/test030.out b/tests/Core/positive/out/test030.out index 1c266518b8..105e25d6f2 100644 --- a/tests/Core/positive/out/test030.out +++ b/tests/Core/positive/out/test030.out @@ -1,3 +1,2 @@ cons 2 (cons 3 (cons 5 (cons 7 (cons 11 (cons 13 (cons 17 (cons 19 (cons 23 (cons 29 nil))))))))) 547 -1229 diff --git a/tests/Core/positive/out/test031.out b/tests/Core/positive/out/test031.out index 215125f069..e0fa7441a8 100644 --- a/tests/Core/positive/out/test031.out +++ b/tests/Core/positive/out/test031.out @@ -3,4 +3,4 @@ 15 17 29 -1021 +125 diff --git a/tests/Core/positive/out/test032.out b/tests/Core/positive/out/test032.out index 6e557e13de..3a6afd1c7d 100644 --- a/tests/Core/positive/out/test032.out +++ b/tests/Core/positive/out/test032.out @@ -1,4 +1,4 @@ 10 21 2187 -1021 +125 diff --git a/tests/Core/positive/test009.jvc b/tests/Core/positive/test009.jvc index 78adb63f22..c5a723e4e3 100644 --- a/tests/Core/positive/test009.jvc +++ b/tests/Core/positive/test009.jvc @@ -9,7 +9,6 @@ def fact := \x fact' x 1; def writeLn := \x write x >> write "\n"; writeLn (sum 10000) >> -writeLn (sum 100000) >> writeLn (fact 5) >> writeLn (fact 10) >> -writeLn (fact 100) +writeLn (fact 12) diff --git a/tests/Core/positive/test012.jvc b/tests/Core/positive/test012.jvc index 00105ab6d7..d701c8335a 100644 --- a/tests/Core/positive/test012.jvc +++ b/tests/Core/positive/test012.jvc @@ -17,7 +17,7 @@ def gen : int -> tree := \n else node3 (gen (n - 1)) (gen (n - 1)) (gen (n - 1)); -def preorder : tree -> tree := \t case t of { +def preorder : tree -> IO := \t case t of { node1 c := write 1 >> preorder c; node2 l r := write 2 >> preorder l >> preorder r; node3 l m r := write 3 >> preorder l >> preorder m >> preorder r; diff --git a/tests/Core/positive/test017.jvc b/tests/Core/positive/test017.jvc index 3f27647695..301f1bf69c 100644 --- a/tests/Core/positive/test017.jvc +++ b/tests/Core/positive/test017.jvc @@ -6,5 +6,4 @@ def sum := \x sum' x 0; def writeLn := \x write x >> write "\n"; -writeLn (sum 10000) >> -writeLn (sum 100000) +writeLn (sum 10000) diff --git a/tests/Core/positive/test023.jvc b/tests/Core/positive/test023.jvc index ee5f2f0fd7..32a81c62d7 100644 --- a/tests/Core/positive/test023.jvc +++ b/tests/Core/positive/test023.jvc @@ -36,9 +36,6 @@ writeLn (gen 10) >> writeLn (rev (gen 10)) >> writeLn (filter (\x x > 5) (gen 10)) >> writeLn (rev (map (\x x - 1) (gen 10))) >> -writeLn (sum 10000) >> -writeLn (sum 100000) >> -writeLn (sum' 10000) >> -writeLn (sum' 100000) >> -writeLn (sum'' 10000) >> -writeLn (sum'' 100000) +writeLn (sum 1000) >> +writeLn (sum' 1000) >> +writeLn (sum'' 1000) diff --git a/tests/Core/positive/test026.jvc b/tests/Core/positive/test026.jvc index 9fb6a62ebd..aaa57a278b 100644 --- a/tests/Core/positive/test026.jvc +++ b/tests/Core/positive/test026.jvc @@ -37,6 +37,4 @@ def writeLn := \x write x >> write "\n"; writeLn (f (gen 10)) >> writeLn (f (gen 15)) >> writeLn (f (gen 16)) >> -writeLn (f (gen 17)) >> -writeLn (f (gen 18)) >> -writeLn (f (gen 20)) +writeLn (f (gen 17)) diff --git a/tests/Core/positive/test030.jvc b/tests/Core/positive/test030.jvc index 342d3a0b2f..247e646421 100644 --- a/tests/Core/positive/test030.jvc +++ b/tests/Core/positive/test030.jvc @@ -9,42 +9,45 @@ type list { cons : any -> list -> list; }; -def force := \f f unit; +type Stream { + scons : any -> (Unit -> Stream) -> Stream; +}; + +def force : (Unit -> Stream) -> Stream := \f f unit; -def filter := \p \s \_ +def filter : (any -> bool) -> (Unit -> Stream) -> Unit -> Stream := \p \s \_ case force s of { - cons h t := + scons h t := if p h then - cons h (filter p t) + scons h (filter p t) else force (filter p t) }; -def take := \n \s +def take : int -> (Unit -> Stream) -> list := \n \s if n = 0 then nil else case force s of { - cons h t := cons h (take (n - 1) t) + scons h t := cons h (take (n - 1) t) }; -def nth := \n \s +def nth : int -> (Unit -> Stream) -> any := \n \s case force s of { - cons h t := if n = 0 then h else nth (n - 1) t + scons h t := if n = 0 then h else nth (n - 1) t }; -def numbers := \n \_ cons n (numbers (n + 1)); +def numbers : int -> Unit -> Stream := \n \_ scons n (numbers (n + 1)); -def indivisible := \n \x if x % n = 0 then false else true; -def eratostenes := \s \_ +def indivisible : int -> int -> bool := \n \x if x % n = 0 then false else true; +def eratostenes : (Unit -> Stream) -> Unit -> Stream := \s \_ case force s of { - cons n t := - cons n (eratostenes (filter (indivisible n) t)) + scons n t := + scons n (eratostenes (filter (indivisible n) t)) }; -def primes := eratostenes (numbers 2); +def primes : Unit -> Stream := eratostenes (numbers 2); def writeLn := \x write x >> write "\n"; writeLn (take 10 primes) >> -writeLn (nth 100 primes) >> -writeLn (nth 200 primes) +writeLn (nth 100 primes) diff --git a/tests/Core/positive/test031.jvc b/tests/Core/positive/test031.jvc index 75bc70519b..840b0b971a 100644 --- a/tests/Core/positive/test031.jvc +++ b/tests/Core/positive/test031.jvc @@ -15,4 +15,4 @@ writeLn (ack 1 7) >> writeLn (ack 1 13) >> writeLn (ack 2 7) >> writeLn (ack 2 13) >> -writeLn (ack 3 7) +writeLn (ack 3 4) diff --git a/tests/Core/positive/test032.jvc b/tests/Core/positive/test032.jvc index 1bb72ee68f..f5ffa912be 100644 --- a/tests/Core/positive/test032.jvc +++ b/tests/Core/positive/test032.jvc @@ -22,4 +22,4 @@ def writeLn := \x write x >> write "\n"; writeLn (plus 3 7) >> writeLn (mult 3 7) >> writeLn (exp 3 7) >> -writeLn (ackermann 3 7) +writeLn (ackermann 3 4) diff --git a/tests/Core/positive/test040.jvc b/tests/Core/positive/test040.jvc index 006f1f89f6..423e78b96f 100644 --- a/tests/Core/positive/test040.jvc +++ b/tests/Core/positive/test040.jvc @@ -13,24 +13,26 @@ def fib := def writeLn := \x write x >> write "\n"; def mutrec := + let two := 2 in + let one := 1 in letrec[f g h] f := \x { - if x < 1 then - 1 + if x < one then + one else - g (x - 1) + 2 * x + g (x - one) + two * x }; g := \x { - if x < 1 then - 1 + if x < one then + one else - x + h (x - 1) + x + h (x - one) }; h := \x letrec z := { - if x < 1 then - 1 + if x < one then + one else - x * f (x - 1) + x * f (x - one) } in z; in writeLn (f 5) >> writeLn (f 10) >> writeLn (f 100) >> writeLn (g 5) >> writeLn (h 5); diff --git a/tests/Core/positive/test042.jvc b/tests/Core/positive/test042.jvc index bbde6ef523..d5ba48eda2 100644 --- a/tests/Core/positive/test042.jvc +++ b/tests/Core/positive/test042.jvc @@ -11,6 +11,4 @@ def hd : Π A : Type, list A → A := λ(A : Type) λl case l of { cons _ x _ := def tl : Π A : Type, list A → list A := λ(A : Type) λl case l of { cons _ _ y := y }; -def main := hd int (tl int (id (list int) (cons int 1 (cons int 2 (nil int))))); - -main +hd int (tl int (id (list int) (cons int 1 (cons int 2 (nil int))))) diff --git a/tests/Core/positive/test043.jvc b/tests/Core/positive/test043.jvc index 13e8cff9d3..b46150e86a 100644 --- a/tests/Core/positive/test043.jvc +++ b/tests/Core/positive/test043.jvc @@ -7,6 +7,4 @@ def fun' := λ(T : Type → Type) λ(A : Type) λ(B : T A) λ(x : B) let h := λ(b : B) λ(a : A) a * b - b in f (λ(y : B) h y x); -def main := fun int 2 + fun' (λA A) int int 3; - -main +fun int 2 + fun' (λ(A : Type) A) int int 3 diff --git a/tests/Core/positive/test044.jvc b/tests/Core/positive/test044.jvc index e909eddaf8..db7d4bb05c 100644 --- a/tests/Core/positive/test044.jvc +++ b/tests/Core/positive/test044.jvc @@ -12,6 +12,6 @@ def h : int -> int := compose f (g 3); def j : int -> int -> int := g; -def k : int -> int -> int -> int := expand j; +def k : int -> int -> any -> int := expand j; h 13 + j 2 3 + k 9 4 7