Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Pattern matching compilation #1874

Merged
merged 36 commits into from
Mar 27, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
36 commits
Select commit Hold shift + click to select a range
8405217
Rename match-to-case to naive-match-to-case and add match-to-case stub
lukaszcz Feb 28, 2023
3913d85
efficient pattern matching compilation (wip)
lukaszcz Mar 2, 2023
3e213d9
simplify pattern representation
lukaszcz Mar 8, 2023
a00cfbb
fix pattern binders in Internal-to-Core
lukaszcz Mar 8, 2023
f96fee0
fix Internal-to-Core pattern translation
lukaszcz Mar 9, 2023
dd73ed0
fix Internal-to-Core
lukaszcz Mar 9, 2023
f88bc1f
adapt pattern matching compilation to new pattern representation
lukaszcz Mar 10, 2023
ff4f7f0
error message
lukaszcz Mar 10, 2023
093309b
fix pattern matching compilation (wip)
lukaszcz Mar 10, 2023
1f99b66
fix compilation after rebase
lukaszcz Mar 16, 2023
b3f81a7
use rmap
lukaszcz Mar 17, 2023
3338478
fix error message
lukaszcz Mar 17, 2023
e085f87
fix error message
lukaszcz Mar 17, 2023
e7842cb
ignore type parameters
lukaszcz Mar 17, 2023
367397d
generate failure nodes
lukaszcz Mar 17, 2023
7b5231f
fix spacing
lukaszcz Mar 17, 2023
05a2c04
preserve binder names
lukaszcz Mar 17, 2023
5397e67
fix binders in types
lukaszcz Mar 20, 2023
88248b1
move-apps for 'trace' and 'fail'
lukaszcz Mar 20, 2023
1af7312
add coverage checking
lukaszcz Mar 21, 2023
1aa2215
fix Core.toStripped
lukaszcz Mar 21, 2023
f2627b1
naming changes
lukaszcz Mar 21, 2023
4019d1c
naming changes
lukaszcz Mar 21, 2023
ba75b85
fix coverage checking
lukaszcz Mar 21, 2023
124bf4c
add 'total' keyword
lukaszcz Mar 21, 2023
8c79c9d
add negative test
lukaszcz Mar 21, 2023
9691898
preserve function location in Internal-to-Core
lukaszcz Mar 21, 2023
93b5c8b
Revert "add 'total' keyword"
lukaszcz Mar 23, 2023
a13508b
fix coverage
lukaszcz Mar 23, 2023
efa9673
fix tests
lukaszcz Mar 23, 2023
51dccfd
changes for review
lukaszcz Mar 23, 2023
8d267dd
fix compilation
lukaszcz Mar 24, 2023
8e52734
Merge branch 'main' into pattern-matching-compilation
lukaszcz Mar 24, 2023
d5effb8
Merge branch 'main' into pattern-matching-compilation
lukaszcz Mar 24, 2023
1520356
fix examples
lukaszcz Mar 24, 2023
7ad0a7a
minor naming change
lukaszcz Mar 24, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion app/App.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ module App where
import CommonOptions
import Data.ByteString qualified as ByteString
import GlobalOptions
import Juvix.Compiler.Backend qualified as Backend
import Juvix.Compiler.Builtins.Effect
import Juvix.Compiler.Pipeline
import Juvix.Data.Error qualified as Error
Expand Down Expand Up @@ -85,11 +86,14 @@ getEntryPoint' RunAppIOArgs {..} inputFile = do
_entryPointBuildDir = _runAppIOArgsBuildDir,
_entryPointNoTermination = opts ^. globalNoTermination,
_entryPointNoPositivity = opts ^. globalNoPositivity,
_entryPointNoCoverage = opts ^. globalNoCoverage,
_entryPointNoStdlib = opts ^. globalNoStdlib,
_entryPointPackage = _runAppIOArgsPkg,
_entryPointModulePaths = pure (someBaseToAbs _runAppIOArgsInvokeDir (inputFile ^. pathPath)),
_entryPointGenericOptions = project opts,
_entryPointStdin = estdin
_entryPointStdin = estdin,
_entryPointDebug = False,
_entryPointTarget = Backend.TargetCore
}

someBaseToAbs' :: (Members '[App] r) => SomeBase a -> Sem r (Path Abs a)
Expand Down
5 changes: 3 additions & 2 deletions app/Commands/Compile.hs
Original file line number Diff line number Diff line change
Expand Up @@ -28,9 +28,10 @@ runCommand opts@CompileOptions {..} = do
TargetAsm -> Compile.runAsmPipeline arg

writeCoreFile :: (Members '[Embed IO, App] r) => Compile.PipelineArg -> Sem r ()
writeCoreFile Compile.PipelineArg {..} = do
writeCoreFile [email protected] {..} = do
entryPoint <- Compile.getEntry pa
coreFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
r <- runError @JuvixError $ Core.toEval _pipelineArgInfoTable
r <- runReader entryPoint $ runError @JuvixError $ Core.toEval _pipelineArgInfoTable
case r of
Left e -> exitJuvixError e
Right tab ->
Expand Down
19 changes: 11 additions & 8 deletions app/Commands/Dev/Asm/Compile.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,20 +4,26 @@ import Commands.Base
import Commands.Dev.Asm.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.Asm.Translation.FromSource qualified as Asm
import Juvix.Compiler.Backend qualified as Backend
import Juvix.Compiler.Backend.C qualified as C

runCommand :: forall r. (Members '[Embed IO, App] r) => AsmCompileOptions -> Sem r ()
runCommand opts = do
file <- getFile
ep <- getEntryPoint (AppPath (Abs file) True)
tgt <- getTarget (opts ^. compileTarget)
let entryPoint :: EntryPoint
entryPoint =
ep
{ _entryPointTarget = tgt,
_entryPointDebug = opts ^. compileDebug
}
s <- embed (readFile (toFilePath file))
case Asm.runParser (toFilePath file) s of
Left err -> exitJuvixError (JuvixError err)
Right tab -> do
tgt <- asmTarget (opts ^. compileTarget)
case run $ runError $ asmToMiniC (asmOpts tgt) tab of
case run $ runReader entryPoint $ runError $ asmToMiniC tab of
Left err -> exitJuvixError err
Right C.MiniCResult {..} -> do
buildDir <- askBuildDir
Expand All @@ -29,11 +35,8 @@ runCommand opts = do
getFile :: Sem r (Path Abs File)
getFile = someBaseToAbs' (opts ^. compileInputFile . pathPath)

asmOpts :: Backend.Target -> Asm.Options
asmOpts tgt = Asm.makeOptions tgt (opts ^. compileDebug)

asmTarget :: CompileTarget -> Sem r Backend.Target
asmTarget = \case
getTarget :: CompileTarget -> Sem r Backend.Target
getTarget = \case
TargetWasm32Wasi -> return Backend.TargetCWasm32Wasi
TargetNative64 -> return Backend.TargetCNative64
TargetGeb -> exitMsg (ExitFailure 1) "error: GEB target not supported for JuvixAsm"
Expand Down
4 changes: 3 additions & 1 deletion app/Commands/Dev/Core/Asm.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,16 +5,18 @@ 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.Options qualified as Core
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
gopts <- askGlobalOptions
inputFile :: Path Abs File <- someBaseToAbs' sinputFile
s' <- embed (readFile $ toFilePath inputFile)
tab <- getRight (mapLeft JuvixError (Core.runParserMain inputFile Core.emptyInfoTable s'))
r <- runError @JuvixError $ Core.toStripped tab
r <- runReader (project @GlobalOptions @Core.CoreOptions gopts) $ runError @JuvixError $ Core.toStripped' tab
tab' <- Asm.fromCore . Stripped.fromCore <$> getRight r
if
| project opts ^. coreAsmPrint ->
Expand Down
48 changes: 28 additions & 20 deletions app/Commands/Dev/Core/Compile/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,7 @@ 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.Asm.Pretty qualified as Pretty
import Juvix.Compiler.Asm.Pretty qualified as Asm
import Juvix.Compiler.Backend qualified as Backend
import Juvix.Compiler.Backend.C qualified as C
import Juvix.Compiler.Backend.Geb qualified as Geb
Expand All @@ -18,13 +17,31 @@ data PipelineArg = PipelineArg
_pipelineArgInfoTable :: Core.InfoTable
}

getEntry :: Members '[Embed IO, App] r => PipelineArg -> Sem r EntryPoint
getEntry PipelineArg {..} = do
ep <- getEntryPoint (AppPath (Abs _pipelineArgFile) True)
return $
ep
{ _entryPointTarget = getTarget (_pipelineArgOptions ^. compileTarget),
_entryPointDebug = _pipelineArgOptions ^. compileDebug
}
where
getTarget :: CompileTarget -> Backend.Target
getTarget = \case
TargetWasm32Wasi -> Backend.TargetCWasm32Wasi
TargetNative64 -> Backend.TargetCNative64
TargetGeb -> Backend.TargetGeb
TargetCore -> Backend.TargetCore
TargetAsm -> Backend.TargetAsm

runCPipeline ::
forall r.
(Members '[Embed IO, App] r) =>
PipelineArg ->
Sem r ()
runCPipeline PipelineArg {..} = do
C.MiniCResult {..} <- getRight (run (runError (coreToMiniC asmOpts _pipelineArgInfoTable :: Sem '[Error JuvixError] C.MiniCResult)))
runCPipeline pa@PipelineArg {..} = do
entryPoint <- getEntry pa
C.MiniCResult {..} <- getRight (run (runReader entryPoint (runError (coreToMiniC _pipelineArgInfoTable :: Sem '[Error JuvixError, Reader EntryPoint] C.MiniCResult))))
cFile <- inputCFile _pipelineArgFile
embed $ TIO.writeFile (toFilePath cFile) _resultCCode
outfile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
Expand All @@ -34,17 +51,6 @@ runCPipeline PipelineArg {..} = do
_compileOutputFile = Just (AppPath (Abs outfile) False)
}
where
asmOpts :: Asm.Options
asmOpts = Asm.makeOptions (asmTarget (_pipelineArgOptions ^. compileTarget)) (_pipelineArgOptions ^. compileDebug)

asmTarget :: CompileTarget -> Backend.Target
asmTarget = \case
TargetWasm32Wasi -> Backend.TargetCWasm32Wasi
TargetNative64 -> Backend.TargetCNative64
TargetGeb -> impossible
TargetCore -> impossible
TargetAsm -> impossible

inputCFile :: Path Abs File -> Sem r (Path Abs File)
inputCFile inputFileCompile = do
buildDir <- askBuildDir
Expand All @@ -56,7 +62,8 @@ runGebPipeline ::
(Members '[Embed IO, App] r) =>
PipelineArg ->
Sem r ()
runGebPipeline PipelineArg {..} = do
runGebPipeline pa@PipelineArg {..} = do
entryPoint <- getEntry pa
gebFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
let spec =
if
Expand All @@ -67,13 +74,14 @@ runGebPipeline PipelineArg {..} = do
{ _lispPackageName = fromString $ takeBaseName $ toFilePath gebFile,
_lispPackageEntry = "*entry*"
}
Geb.Result {..} <- getRight (run (runError (coreToGeb spec _pipelineArgInfoTable :: Sem '[Error JuvixError] Geb.Result)))
Geb.Result {..} <- getRight (run (runReader entryPoint (runError (coreToGeb spec _pipelineArgInfoTable :: Sem '[Error JuvixError, Reader EntryPoint] Geb.Result))))
embed $ TIO.writeFile (toFilePath gebFile) _resultCode

runAsmPipeline :: (Members '[Embed IO, App] r) => PipelineArg -> Sem r ()
runAsmPipeline PipelineArg {..} = do
runAsmPipeline pa@PipelineArg {..} = do
entryPoint <- getEntry pa
asmFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
r <- runError @JuvixError (coreToAsm _pipelineArgInfoTable)
r <- runReader entryPoint $ runError @JuvixError (coreToAsm _pipelineArgInfoTable)
tab' <- getRight r
let code = Pretty.ppPrint tab' tab'
let code = Asm.ppPrint tab' tab'
embed $ TIO.writeFile (toFilePath asmFile) code
4 changes: 3 additions & 1 deletion app/Commands/Dev/Core/FromConcrete.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,16 +4,18 @@ import Commands.Base
import Commands.Dev.Core.FromConcrete.Options
import Evaluator
import Juvix.Compiler.Core.Data.InfoTable
import Juvix.Compiler.Core.Options qualified as Core
import Juvix.Compiler.Core.Pretty qualified as Core
import Juvix.Compiler.Core.Transformation qualified as Core
import Juvix.Compiler.Core.Transformation.DisambiguateNames (disambiguateNames)
import Juvix.Compiler.Core.Translation

runCommand :: forall r. Members '[Embed IO, App] r => CoreFromConcreteOptions -> Sem r ()
runCommand localOpts = do
gopts <- askGlobalOptions
tab <- (^. coreResultTable) <$> runPipeline (localOpts ^. coreFromConcreteInputFile) upToCore
path :: Path Abs File <- someBaseToAbs' (localOpts ^. coreFromConcreteInputFile . pathPath)
r <- runError @JuvixError $ Core.applyTransformations (project localOpts ^. coreFromConcreteTransformations) tab
let r = run $ runReader (project @GlobalOptions @Core.CoreOptions gopts) $ runError @JuvixError $ Core.applyTransformations (project localOpts ^. coreFromConcreteTransformations) tab
tab0 :: InfoTable <- getRight r
let tab' :: InfoTable = if localOpts ^. coreFromConcreteNoDisambiguate then tab0 else disambiguateNames tab0
inInputModule :: IdentifierInfo -> Bool
Expand Down
10 changes: 6 additions & 4 deletions app/Commands/Dev/Core/Read.hs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,8 @@ module Commands.Dev.Core.Read where
import Commands.Base
import Commands.Dev.Core.Read.Options
import Evaluator qualified as Eval
import Juvix.Compiler.Core.Pretty qualified as Core
import Juvix.Compiler.Core.Options qualified as Core
import Juvix.Compiler.Core.Pretty qualified as Pretty
import Juvix.Compiler.Core.Scoper qualified as Scoper
import Juvix.Compiler.Core.Transformation qualified as Core
import Juvix.Compiler.Core.Transformation.DisambiguateNames qualified as Core
Expand All @@ -13,21 +14,22 @@ runCommand ::
forall r a.
( Members '[Embed IO, App] r,
CanonicalProjection a Eval.EvalOptions,
CanonicalProjection a Core.Options,
CanonicalProjection a Pretty.Options,
CanonicalProjection a CoreReadOptions
) =>
a ->
Sem r ()
runCommand opts = do
gopts <- askGlobalOptions
inputFile :: Path Abs File <- someBaseToAbs' sinputFile
s' <- embed . readFile . toFilePath $ inputFile
tab <- getRight (mapLeft JuvixError (Core.runParserMain inputFile Core.emptyInfoTable s'))
r <- runError @JuvixError $ Core.applyTransformations (project opts ^. coreReadTransformations) tab
let r = run $ runReader (project @GlobalOptions @Core.CoreOptions gopts) $ runError @JuvixError $ Core.applyTransformations (project opts ^. coreReadTransformations) tab
tab0 <- getRight $ mapLeft JuvixError r
let tab' = if project opts ^. coreReadNoDisambiguate then tab0 else Core.disambiguateNames tab0
embed (Scoper.scopeTrace tab')
unless (project opts ^. coreReadNoPrint) $ do
renderStdOut (Core.ppOut opts tab')
renderStdOut (Pretty.ppOut opts tab')
whenJust (tab' ^. Core.infoMain) $ \sym -> doEval tab' (fromJust $ tab' ^. Core.identContext . at sym)
where
doEval :: Core.InfoTable -> Core.Node -> Sem r ()
Expand Down
7 changes: 6 additions & 1 deletion app/Commands/Dev/Core/Strip.hs
Original file line number Diff line number Diff line change
Expand Up @@ -2,17 +2,22 @@ module Commands.Dev.Core.Strip where

import Commands.Base
import Commands.Dev.Core.Strip.Options
import Juvix.Compiler.Core.Options qualified as Core
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
gopts <- askGlobalOptions
inputFile :: Path Abs File <- someBaseToAbs' sinputFile
s' <- embed (readFile $ toFilePath inputFile)
(tab, _) <- getRight (mapLeft JuvixError (Core.runParser inputFile Core.emptyInfoTable s'))
r <- runError @JuvixError (Core.toStripped tab)
let r =
run $
runReader (project gopts) $
runError @JuvixError (Core.toStripped' tab :: Sem '[Error JuvixError, Reader Core.CoreOptions] Core.InfoTable)
tab' <- getRight $ mapLeft JuvixError $ mapRight Stripped.fromCore r
unless (project opts ^. coreStripNoPrint) $ do
renderStdOut (Core.ppOut opts tab')
Expand Down
18 changes: 10 additions & 8 deletions app/Commands/Dev/Geb/Repl.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,11 @@ module Commands.Dev.Geb.Repl where
import Commands.Base hiding (command)
import Commands.Dev.Geb.Repl.Format
import Commands.Dev.Geb.Repl.Options
import Commands.Extra.Paths
import Control.Exception (throwIO)
import Control.Monad.State.Strict qualified as State
import Data.String.Interpolate (i, __i)
import Juvix.Compiler.Backend qualified as Backend
import Juvix.Compiler.Backend.Geb qualified as Geb
import Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Error
import Juvix.Data.Error.GenericError qualified as Error
Expand All @@ -29,9 +31,6 @@ data ReplState = ReplState

makeLenses ''ReplState

replPath :: Path Abs File
replPath = $(mkAbsFile "/repl.geb")

runCommand :: (Members '[Embed IO, App] r) => GebReplOptions -> Sem r ()
runCommand replOpts = do
root <- askPkgDir
Expand All @@ -50,11 +49,14 @@ runCommand replOpts = do
_entryPointResolverRoot = root,
_entryPointNoTermination = gopts ^. globalNoTermination,
_entryPointNoPositivity = gopts ^. globalNoPositivity,
_entryPointNoCoverage = gopts ^. globalNoCoverage,
_entryPointNoStdlib = gopts ^. globalNoStdlib,
_entryPointPackage = package,
_entryPointModulePaths = pure absInputFile,
_entryPointGenericOptions = project gopts,
_entryPointStdin = Nothing
_entryPointStdin = Nothing,
_entryPointTarget = Backend.TargetGeb,
_entryPointDebug = False
}
embed
( State.evalStateT
Expand Down Expand Up @@ -103,7 +105,7 @@ loadFile getReplEntryPoint f = do

inferObject :: String -> Repl ()
inferObject gebMorphism = Repline.dontCrash $ do
case Geb.runParser replPath (pack gebMorphism) of
case Geb.runParser gebReplPath (pack gebMorphism) of
Left err -> printError (JuvixError err)
Right (Geb.ExpressionMorphism morphism) -> do
case Geb.inferObject' morphism of
Expand All @@ -115,7 +117,7 @@ inferObject gebMorphism = Repline.dontCrash $ do

checkTypedMorphism :: String -> Repl ()
checkTypedMorphism gebMorphism = Repline.dontCrash $ do
case Geb.runParser replPath (pack gebMorphism) of
case Geb.runParser gebReplPath (pack gebMorphism) of
Left err -> printError (JuvixError err)
Right (Geb.ExpressionTypedMorphism tyMorphism) -> do
case run . runError @CheckingError $ Geb.check' tyMorphism of
Expand All @@ -131,7 +133,7 @@ runReplCommand input =
Geb.runEval $
Geb.RunEvalArgs
{ _runEvalArgsContent = pack input,
_runEvalArgsInputFile = replPath,
_runEvalArgsInputFile = gebReplPath,
_runEvalArgsEvaluatorOptions = Geb.defaultEvaluatorOptions
}
printEvalResult evalRes
Expand All @@ -143,7 +145,7 @@ evalAndOutputMorphism input =
Geb.runEval $
Geb.RunEvalArgs
{ _runEvalArgsContent = pack input,
_runEvalArgsInputFile = replPath,
_runEvalArgsInputFile = gebReplPath,
_runEvalArgsEvaluatorOptions =
Geb.defaultEvaluatorOptions
{ Geb._evaluatorOptionsOutputMorphism = True
Expand Down
8 changes: 7 additions & 1 deletion app/Commands/Eval.hs
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,18 @@ import Evaluator qualified as Eval
import Juvix.Compiler.Core qualified as Core
import Juvix.Compiler.Core.Data.InfoTable qualified as Core
import Juvix.Compiler.Core.Language qualified as Core
import Juvix.Compiler.Core.Options qualified as Core
import Juvix.Compiler.Core.Pipeline qualified as Core

runCommand :: (Members '[Embed IO, App] r) => EvalOptions -> Sem r ()
runCommand opts@EvalOptions {..} = do
gopts <- askGlobalOptions
Core.CoreResult {..} <- runPipeline _evalInputFile upToCore
r <- runError @JuvixError $ Core.toEval _coreResultTable
let r =
run $
runReader (project gopts) $
runError @JuvixError $
(Core.toEval' _coreResultTable :: Sem '[Error JuvixError, Reader Core.CoreOptions] Core.InfoTable)
tab <- getRight r
let evalNode =
if
Expand Down
3 changes: 3 additions & 0 deletions app/Commands/Extra/Paths.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,3 +5,6 @@ import Juvix.Prelude
-- | imaginary file path for error messages in the repl.
replPath :: Path Abs File
replPath = $(mkAbsFile "/<repl>")

gebReplPath :: Path Abs File
janmasrovira marked this conversation as resolved.
Show resolved Hide resolved
gebReplPath = $(mkAbsFile "/repl.geb")
Loading