-
Notifications
You must be signed in to change notification settings - Fork 54
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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
- Loading branch information
Showing
71 changed files
with
1,108 additions
and
303 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 {..} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 {..} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.