anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2024-09-11 16:26:33 +03:00
Code Issues Projects Releases Wiki Activity

New compilation pipeline (#1832)

Browse Source 
* Depends on PR #1824 
* Closes #1556 
* Closes #1825 
* Closes #1843
* Closes #1729 
* Closes #1596 
* Closes #1343 
* Closes #1382 
* Closes #1867 
* Closes #1876 
* Changes the `juvix compile` command to use the new pipeline.
* Removes the `juvix dev minic` command and the `BackendC` tests.
* Adds the `juvix eval` command.
* Fixes bugs in the Nat-to-integer conversion.
* Fixes bugs in the Internal-to-Core and Core-to-Core.Stripped
translations.
* Fixes bugs in the RemoveTypeArgs transformation.
* Fixes bugs in lambda-lifting (incorrect de Bruijn indices in the types
of added binders).
* Fixes several other bugs in the compilation pipeline.
* Adds a separate EtaExpandApps transformation to avoid quadratic
runtime in the Internal-to-Core translation due to repeated calls to
etaExpandApps.
* Changes Internal-to-Core to avoid generating matches on values which
don't have an inductive type.

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>
Co-authored-by: janmasrovira <janmasrovira@gmail.com>
This commit is contained in:
Łukasz Czajka 2023-03-14 16:24:07 +01:00 committed by GitHub
parent 0f29b3ee93
commit 2d798ec31c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
121 changed files with 2079 additions and 1610 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Makefile
View File

@ -264,7 +264,7 @@ SMOKE := $(shell command -v smoke 2> /dev/null)
.PHONY : smoke-only
smoke-only:
@$(if $(SMOKE),, $(error "Smoke not found, please install it from https://github.com/SamirTalwar/smoke"))
@$(if $(SMOKE),, $(error "Smoke not found, please install it from https://github.com/jonaprieto/smoke"))
@smoke $(shell find tests -name '*.smoke.yaml')
.PHONY : smoke

203
app/Commands/Compile.hs
View File

@ -2,191 +2,30 @@ module Commands.Compile where
import Commands.Base
import Commands.Compile.Options
import Data.ByteString qualified as BS
import Data.FileEmbed qualified as FE
import Commands.Dev.Core.Compile.Base qualified as Compile
import Commands.Extra.Compile qualified as Compile
import Data.Text.IO qualified as TIO
import Juvix.Compiler.Backend.C.Translation.FromInternal qualified as MiniC
import System.Environment
import System.Process qualified as P
import Juvix.Compiler.Core qualified as Core
import Juvix.Compiler.Core.Pretty qualified as Core
runCommand :: (Members '[Embed IO, App] r) => CompileOptions -> Sem r ()
runCommand opts@CompileOptions {..} = do
miniC <- (^. MiniC.resultCCode) <$> runPipeline _compileInputFile upToMiniC
inputFile <- someBaseToAbs' (_compileInputFile ^. pathPath)
result <- runCompile inputFile opts miniC
case result of
Left err -> printFailureExit err
_ -> return ()
Core.CoreResult {..} <- runPipeline _compileInputFile upToCore
let arg =
Compile.PipelineArg
{ _pipelineArgFile = inputFile,
_pipelineArgOptions = opts,
_pipelineArgInfoTable = _coreResultTable
}
case _compileTarget of
TargetNative64 -> Compile.runCPipeline arg
TargetWasm32Wasi -> Compile.runCPipeline arg
TargetGeb -> Compile.runGebPipeline arg
TargetCore -> writeCoreFile arg
TargetAsm -> Compile.runAsmPipeline arg
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)
runCompile :: (Members '[Embed IO, App] r) => Path Abs File -> CompileOptions -> Text -> Sem r (Either Text ())
runCompile inputFileCompile o minic = do
buildDir <- askBuildDir
ensureDir buildDir
f <- inputCFile inputFileCompile
embed (TIO.writeFile (toFilePath f) minic)
prepareRuntime o
case o ^. compileTarget of
TargetWasm -> runError (clangCompile inputFileCompile o)
TargetC -> return (Right ())
TargetNative -> runError (clangNativeCompile inputFileCompile o)
prepareRuntime :: forall r. (Members '[Embed IO, App] r) => CompileOptions -> Sem r ()
prepareRuntime o = mapM_ writeRuntime runtimeProjectDir
where
runtimeProjectDir :: [(Path Rel File, BS.ByteString)]
runtimeProjectDir = case o ^. compileTarget of
TargetNative -> libcRuntime
_ -> case o ^. compileRuntime of
RuntimeWasiStandalone -> wasiStandaloneRuntimeDir <> builtinCRuntimeDir <> wallocDir
RuntimeWasiLibC -> libcRuntime
RuntimeStandalone -> standaloneRuntimeDir <> builtinCRuntimeDir <> wallocDir
writeRuntime :: (Path Rel File, BS.ByteString) -> Sem r ()
writeRuntime (filePath, contents) = do
buildDir <- askBuildDir
embed (BS.writeFile (toFilePath (buildDir <//> filePath)) contents)
wasiStandaloneRuntimeDir :: [(Path Rel File, BS.ByteString)]
wasiStandaloneRuntimeDir = map (first relFile) $(FE.makeRelativeToProject "c-runtime/wasi-standalone" >>= FE.embedDir)
standaloneRuntimeDir :: [(Path Rel File, BS.ByteString)]
standaloneRuntimeDir = map (first relFile) $(FE.makeRelativeToProject "c-runtime/standalone" >>= FE.embedDir)
wasiLibCRuntimeDir :: [(Path Rel File, BS.ByteString)]
wasiLibCRuntimeDir = map (first relFile) $(FE.makeRelativeToProject "c-runtime/wasi-libc" >>= FE.embedDir)
builtinCRuntimeDir :: [(Path Rel File, BS.ByteString)]
builtinCRuntimeDir = map (first relFile) $(FE.makeRelativeToProject "c-runtime/builtins" >>= FE.embedDir)
wallocDir :: [(Path Rel File, BS.ByteString)]
wallocDir = map (first relFile) $(FE.makeRelativeToProject "c-runtime/walloc" >>= FE.embedDir)
libcRuntime :: [(Path Rel File, BS.ByteString)]
libcRuntime = wasiLibCRuntimeDir <> builtinCRuntimeDir
clangNativeCompile ::
forall r.
(Members '[Embed IO, App, Error Text] r) =>
Path Abs File ->
CompileOptions ->
Sem r ()
clangNativeCompile inputFileCompile o = do
inputFile <- getInputFile
outputFile <- getOutputFile
buildDir <- askBuildDir
runClang (nativeArgs buildDir outputFile inputFile)
where
getOutputFile :: Sem r (Path Abs File)
getOutputFile = case o ^. compileOutputFile of
Nothing -> return (removeExtension' inputFileCompile)
Just f -> someBaseToAbs' (f ^. pathPath)
getInputFile :: Sem r (Path Abs File)
getInputFile = inputCFile inputFileCompile
clangCompile ::
forall r.
(Members '[Embed IO, App, Error Text] r) =>
Path Abs File ->
CompileOptions ->
Sem r ()
clangCompile inputFileCompile o = do
outputFile <- getOutputFile
inputFile <- getInputFile
let clangArgs :: Sem r [String]
clangArgs = case o ^. compileRuntime of
RuntimeStandalone -> do
standaloneLibArgs outputFile inputFile
RuntimeWasiStandalone -> wasiStandaloneArgs outputFile inputFile
RuntimeWasiLibC -> wasiLibcArgs outputFile inputFile
clangArgs >>= runClang
where
getOutputFile :: Sem r (Path Abs File)
getOutputFile = maybe (return defaultOutputFile) someBaseToAbs' (o ^? compileOutputFile . _Just . pathPath)
defaultOutputFile :: Path Abs File
defaultOutputFile = replaceExtension' ".wasm" inputFileCompile
getInputFile :: Sem r (Path Abs File)
getInputFile = inputCFile inputFileCompile
sysrootEnvVar :: (Members '[Error Text, Embed IO] r) => Sem r (Path Abs Dir)
sysrootEnvVar =
absDir
<$> fromMaybeM (throw msg) (embed (lookupEnv "WASI_SYSROOT_PATH"))
where
msg :: Text
msg = "Missing environment variable WASI_SYSROOT_PATH"
commonArgs :: Path Abs Dir -> Path Abs File -> [String]
commonArgs buildDir wasmOutputFile =
[ "-std=c99",
"-Oz",
"-I",
toFilePath buildDir,
"-o",
toFilePath wasmOutputFile
]
standaloneLibArgs :: (Members '[App, Embed IO] r) => Path Abs File -> Path Abs File -> Sem r [String]
standaloneLibArgs wasmOutputFile inputFile = do
buildDir <- askBuildDir
return $
commonArgs buildDir wasmOutputFile
<> [ "--target=wasm32",
"-nodefaultlibs",
"-nostartfiles",
"-Wl,--no-entry",
toFilePath (buildDir <//> $(mkRelFile "walloc.c")),
toFilePath inputFile
]
wasiStandaloneArgs :: (Members '[App, Error Text, Embed IO] r) => Path Abs File -> Path Abs File -> Sem r [String]
wasiStandaloneArgs wasmOutputFile inputFile = do
buildDir <- askBuildDir
com <- wasiCommonArgs wasmOutputFile
return $
com
<> [ toFilePath (buildDir <//> $(mkRelFile "walloc.c")),
toFilePath inputFile
]
wasiLibcArgs :: (Members '[App, Error Text, Embed IO] r) => Path Abs File -> Path Abs File -> Sem r [String]
wasiLibcArgs wasmOutputFile inputFile = do
com <- wasiCommonArgs wasmOutputFile
return $ com <> ["-lc", toFilePath inputFile]
nativeArgs :: Path Abs Dir -> Path Abs File -> Path Abs File -> [String]
nativeArgs buildDir outputFile inputFile =
commonArgs buildDir outputFile <> [toFilePath inputFile]
wasiCommonArgs :: (Members '[App, Error Text, Embed IO] r) => Path Abs File -> Sem r [String]
wasiCommonArgs wasmOutputFile = do
sysrootPath <- sysrootEnvVar
buildDir <- askBuildDir
return $
commonArgs buildDir wasmOutputFile
<> [ "-nodefaultlibs",
"--target=wasm32-wasi",
"--sysroot",
toFilePath sysrootPath
]
runClang ::
(Members '[Embed IO, Error Text] r) =>
[String] ->
Sem r ()
runClang args = do
(exitCode, _, err) <- embed (P.readProcessWithExitCode "clang" args "")
case exitCode of
ExitSuccess -> return ()
_ -> throw (pack err)
writeCoreFile :: (Members '[Embed IO, App] r) => Compile.PipelineArg -> Sem r ()
writeCoreFile Compile.PipelineArg {..} = do
coreFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
embed $ TIO.writeFile (toFilePath coreFile) (show $ Core.ppOut Core.defaultOptions {Core._optShowDeBruijnIndices = True} _pipelineArgInfoTable)

81
app/Commands/Compile/Options.hs
View File

@ -1,77 +1,6 @@
module Commands.Compile.Options where
module Commands.Compile.Options
( module Commands.Extra.Compile.Options,
)
where
import CommonOptions
data CompileTarget
= TargetC
| TargetWasm
| TargetNative
deriving stock (Show, Data)
data CompileRuntime
= RuntimeWasiStandalone
| RuntimeWasiLibC
| RuntimeStandalone
deriving stock (Show, Data)
data CompileOptions = CompileOptions
{ _compileTarget :: CompileTarget,
_compileRuntime :: CompileRuntime,
_compileOutputFile :: Maybe (AppPath File),
_compileInputFile :: AppPath File
}
deriving stock (Data)
makeLenses ''CompileOptions
parseCompile :: Parser CompileOptions
parseCompile = do
_compileTarget <-
option
(eitherReader parseTarget)
( long "target"
<> short 't'
<> metavar "TARGET"
<> value TargetNative
<> showDefaultWith targetShow
<> help "select a target: wasm, c, native"
)
_compileRuntime <-
option
(eitherReader parseRuntime)
( long "runtime"
<> short 'r'
<> metavar "RUNTIME"
<> value RuntimeWasiStandalone
<> showDefaultWith runtimeShow
<> help "select a runtime: wasi-standalone, wasi-libc, standalone"
)
_compileOutputFile <- optional parseGenericOutputFile
_compileInputFile <- parseInputJuvixFile
pure CompileOptions {..}
where
parseTarget :: String -> Either String CompileTarget
parseTarget = \case
"wasm" -> Right TargetWasm
"c" -> Right TargetC
"native" -> Right TargetNative
s -> Left $ "unrecognised target: " <> s
targetShow :: CompileTarget -> String
targetShow = \case
TargetC -> "c"
TargetWasm -> "wasm"
TargetNative -> "native"
parseRuntime :: String -> Either String CompileRuntime
parseRuntime = \case
"wasi-standalone" -> Right RuntimeWasiStandalone
"wasi-libc" -> Right RuntimeWasiLibC
"standalone" -> Right RuntimeStandalone
s -> Left $ "unrecognised runtime: " <> s
runtimeShow :: CompileRuntime -> String
runtimeShow = \case
RuntimeWasiStandalone -> "wasi-standalone"
RuntimeWasiLibC -> "wasi-libc"
RuntimeStandalone -> "standalone"
import Commands.Extra.Compile.Options

2
app/Commands/Dev.hs
View File

@ -11,7 +11,6 @@ import Commands.Dev.DisplayRoot qualified as DisplayRoot
import Commands.Dev.Geb qualified as Geb
import Commands.Dev.Highlight qualified as Highlight
import Commands.Dev.Internal qualified as Internal
import Commands.Dev.MiniC qualified as MiniC
import Commands.Dev.Options
import Commands.Dev.Parse qualified as Parse
import Commands.Dev.Runtime qualified as Runtime
@ -24,7 +23,6 @@ runCommand = \case
Parse opts -> Parse.runCommand opts
Scope opts -> Scope.runCommand opts
Internal opts -> Internal.runCommand opts
MiniC opts -> MiniC.runCommand opts
Termination opts -> Termination.runCommand opts
Core opts -> Core.runCommand opts
Geb opts -> Geb.runCommand opts

32
app/Commands/Dev/Asm/Compile.hs
View File

@ -15,26 +15,30 @@ runCommand opts = do
s <- embed (readFile (toFilePath file))
case Asm.runParser (toFilePath file) s of
Left err -> exitJuvixError (JuvixError err)
Right tab -> case run $ runError $ asmToMiniC asmOpts tab of
Left err -> exitJuvixError err
Right C.MiniCResult {..} -> do
buildDir <- askBuildDir
ensureDir buildDir
cFile <- inputCFile file
embed $ TIO.writeFile (toFilePath cFile) _resultCCode
Compile.runCommand opts {_compileInputFile = AppPath (Abs cFile) False}
Right tab -> do
tgt <- asmTarget (opts ^. compileTarget)
case run $ runError $ asmToMiniC (asmOpts tgt) tab of
Left err -> exitJuvixError err
Right C.MiniCResult {..} -> do
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)
asmOpts :: Backend.Target -> Asm.Options
asmOpts tgt = Asm.makeOptions tgt (opts ^. compileDebug)
asmTarget :: CompileTarget -> Backend.Target
asmTarget :: CompileTarget -> Sem r Backend.Target
asmTarget = \case
TargetWasm32Wasi -> Backend.TargetCWasm32Wasi
TargetNative64 -> Backend.TargetCNative64
TargetGeb -> error "GEB target not supported for JuvixAsm"
TargetWasm32Wasi -> return Backend.TargetCWasm32Wasi
TargetNative64 -> return Backend.TargetCNative64
TargetGeb -> exitMsg (ExitFailure 1) "error: GEB target not supported for JuvixAsm"
TargetCore -> exitMsg (ExitFailure 1) "error: JuvixCore target not supported for JuvixAsm"
TargetAsm -> exitMsg (ExitFailure 1) "error: JuvixAsm target not supported for JuvixAsm"
inputCFile :: (Members '[App] r) => Path Abs File -> Sem r (Path Abs File)
inputCFile inputFileCompile = do

2
app/Commands/Dev/Asm/Compile/Options.hs
View File

@ -10,4 +10,4 @@ import CommonOptions
type AsmCompileOptions = CompileOptions
parseAsmCompileOptions :: Parser AsmCompileOptions
parseAsmCompileOptions = parseCompileOptions
parseAsmCompileOptions = parseCompileOptions parseInputJuvixAsmFile

72
app/Commands/Dev/Core/Compile.hs
View File

@ -1,77 +1,23 @@
module Commands.Dev.Core.Compile (runCommand) where
module Commands.Dev.Core.Compile where
import Commands.Base
import Commands.Dev.Core.Compile.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.Backend.Geb qualified as Geb
import Juvix.Compiler.Core.Data.InfoTable qualified as Core
import Juvix.Compiler.Core.Translation.FromSource qualified as Core
import System.FilePath (takeBaseName)
runCommand :: forall r. (Members '[Embed IO, App] r) => CoreCompileOptions -> Sem r ()
runCommand :: forall r. (Members '[Embed IO, App] r) => CompileOptions -> Sem r ()
runCommand opts = do
file <- getFile
s <- embed (readFile (toFilePath file))
tab <- getRight (mapLeft JuvixError (Core.runParserMain file Core.emptyInfoTable s))
let arg = PipelineArg opts file tab
case opts ^. compileTarget of
TargetGeb -> runGebPipeline (PipelineArg opts file tab)
TargetWasm32Wasi -> runCPipeline (PipelineArg opts file tab)
TargetNative64 -> runCPipeline (PipelineArg opts file tab)
TargetWasm32Wasi -> runCPipeline arg
TargetNative64 -> runCPipeline arg
TargetGeb -> runGebPipeline arg
TargetCore -> return ()
TargetAsm -> runAsmPipeline arg
where
getFile :: Sem r (Path Abs File)
getFile = someBaseToAbs' (opts ^. compileInputFile . pathPath)
data PipelineArg = PipelineArg
{ _pipelineArgOptions :: CoreCompileOptions,
_pipelineArgFile :: Path Abs File,
_pipelineArgInfoTable :: Core.InfoTable
}
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)))
cFile <- inputCFile _pipelineArgFile
embed $ TIO.writeFile (toFilePath cFile) _resultCCode
Compile.runCommand _pipelineArgOptions {_compileInputFile = AppPath (Abs cFile) 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
inputCFile :: Path Abs File -> Sem r (Path Abs File)
inputCFile inputFileCompile = do
buildDir <- askBuildDir
ensureDir buildDir
return (buildDir <//> replaceExtension' ".c" (filename inputFileCompile))
runGebPipeline ::
forall r.
(Members '[Embed IO, App] r) =>
PipelineArg ->
Sem r ()
runGebPipeline PipelineArg {..} = do
gebFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
let spec =
if
| _pipelineArgOptions ^. compileTerm -> Geb.OnlyTerm
| otherwise ->
Geb.LispPackage
Geb.LispPackageSpec
{ _lispPackageName = fromString $ takeBaseName $ toFilePath gebFile,
_lispPackageEntry = "*entry*"
}
Geb.Result {..} <- getRight (run (runError (coreToGeb spec _pipelineArgInfoTable :: Sem '[Error JuvixError] Geb.Result)))
embed $ TIO.writeFile (toFilePath gebFile) _resultCode

78
app/Commands/Dev/Core/Compile/Base.hs Normal file
View File

@ -0,0 +1,78 @@
module Commands.Dev.Core.Compile.Base 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.Asm.Pretty qualified as Pretty
import Juvix.Compiler.Backend qualified as Backend
import Juvix.Compiler.Backend.C qualified as C
import Juvix.Compiler.Backend.Geb qualified as Geb
import Juvix.Compiler.Core.Data.InfoTable qualified as Core
import System.FilePath (takeBaseName)
data PipelineArg = PipelineArg
{ _pipelineArgOptions :: CompileOptions,
_pipelineArgFile :: Path Abs File,
_pipelineArgInfoTable :: Core.InfoTable
}
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)))
cFile <- inputCFile _pipelineArgFile
embed $ TIO.writeFile (toFilePath cFile) _resultCCode
outfile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
Compile.runCommand
_pipelineArgOptions
{ _compileInputFile = AppPath (Abs cFile) False,
_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
ensureDir buildDir
return (buildDir <//> replaceExtension' ".c" (filename inputFileCompile))
runGebPipeline ::
forall r.
(Members '[Embed IO, App] r) =>
PipelineArg ->
Sem r ()
runGebPipeline PipelineArg {..} = do
gebFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
let spec =
if
| _pipelineArgOptions ^. compileTerm -> Geb.OnlyTerm
| otherwise ->
Geb.LispPackage
Geb.LispPackageSpec
{ _lispPackageName = fromString $ takeBaseName $ toFilePath gebFile,
_lispPackageEntry = "*entry*"
}
Geb.Result {..} <- getRight (run (runError (coreToGeb spec _pipelineArgInfoTable :: Sem '[Error JuvixError] Geb.Result)))
embed $ TIO.writeFile (toFilePath gebFile) _resultCode
runAsmPipeline :: (Members '[Embed IO, App] r) => PipelineArg -> Sem r ()
runAsmPipeline PipelineArg {..} = do
asmFile <- Compile.outputFile _pipelineArgOptions _pipelineArgFile
let tab' = coreToAsm _pipelineArgInfoTable
code = Pretty.ppPrint tab' tab'
embed $ TIO.writeFile (toFilePath asmFile) code

9
app/Commands/Dev/Core/Compile/Options.hs
View File

@ -1,13 +1,6 @@
module Commands.Dev.Core.Compile.Options
( module Commands.Dev.Core.Compile.Options,
module Commands.Extra.Compile.Options,
( module Commands.Extra.Compile.Options,
)
where
import Commands.Extra.Compile.Options
import CommonOptions
type CoreCompileOptions = CompileOptions
parseCoreCompileOptions :: Parser CoreCompileOptions
parseCoreCompileOptions = parseCompileOptions

3
app/Commands/Dev/Core/FromConcrete.hs
View File

@ -15,7 +15,8 @@ runCommand localOpts = do
let tab' :: InfoTable = Core.applyTransformations (project localOpts ^. coreFromConcreteTransformations) tab
inInputModule :: IdentifierInfo -> Bool
inInputModule = (== Just path) . (^? identifierLocation . _Just . intervalFile)
inInputModule _ | not (localOpts ^. coreFromConcreteFilter) = True
inInputModule x = (== Just path) . (^? identifierLocation . _Just . intervalFile) $ x
mainIdens :: [IdentifierInfo] =
sortOn

6
app/Commands/Dev/Core/FromConcrete/Options.hs
View File

@ -8,6 +8,7 @@ import Juvix.Compiler.Core.Pretty.Options qualified as Core
data CoreFromConcreteOptions = CoreFromConcreteOptions
{ _coreFromConcreteTransformations :: [TransformationId],
_coreFromConcreteShowDeBruijn :: Bool,
_coreFromConcreteFilter :: Bool,
_coreFromConcreteNoIO :: Bool,
_coreFromConcreteEval :: Bool,
_coreFromConcreteInputFile :: AppPath File,
@ -38,6 +39,11 @@ parseCoreFromConcreteOptions = do
( long "show-de-bruijn"
<> help "Show variable de Bruijn indices"
)
_coreFromConcreteFilter <-
switch
( long "filter"
<> help "Filter out the functions not from the input module"
)
_coreFromConcreteEval <-
switch
( long "eval"

6
app/Commands/Dev/Core/Options.hs
View File

@ -16,7 +16,7 @@ data CoreCommand
| FromConcrete CoreFromConcreteOptions
| Strip CoreStripOptions
| CoreAsm CoreAsmOptions
| CoreCompile CoreCompileOptions
| CoreCompile CompileOptions
deriving stock (Data)
parseCoreCommand :: Parser CoreCommand
@ -92,5 +92,5 @@ parseCoreCommand =
compileInfo :: ParserInfo CoreCommand
compileInfo =
info
(CoreCompile <$> parseCoreCompileOptions)
(progDesc "Compile a JuvixCore file to native code or WebAssembly")
(CoreCompile <$> parseCompileOptions parseInputJuvixCoreFile)
(progDesc "Compile a JuvixCore file to native code, WebAssembly or GEB")

2
app/Commands/Dev/Core/Strip.hs
View File

@ -11,7 +11,7 @@ runCommand :: forall r a. (Members '[Embed IO, App] r, CanonicalProjection a Cor
runCommand opts = do
inputFile :: Path Abs File <- someBaseToAbs' sinputFile
s' <- embed (readFile $ toFilePath inputFile)
(tab, _) <- getRight (mapLeft JuvixError (Core.runParser inputFile Core.emptyInfoTable s'))
tab <- getRight (mapLeft JuvixError (Core.runParserMain inputFile Core.emptyInfoTable s'))
let tab' = Stripped.fromCore (Core.toStripped tab)
unless (project opts ^. coreStripNoPrint) $ do
renderStdOut (Core.ppOut opts tab')

10
app/Commands/Dev/MiniC.hs
View File

@ -1,10 +0,0 @@
module Commands.Dev.MiniC where
import Commands.Base
import Commands.Dev.MiniC.Options
import Juvix.Compiler.Backend.C.Translation.FromInternal qualified as MiniC
runCommand :: (Members '[Embed IO, App] r) => MiniCOptions -> Sem r ()
runCommand opts = do
miniC <- (^. MiniC.resultCCode) <$> runPipeline (opts ^. miniCInputFile) upToMiniC
say miniC

10
app/Commands/Dev/Options.hs
View File

@ -18,7 +18,6 @@ import Commands.Dev.DisplayRoot.Options
import Commands.Dev.Geb.Options
import Commands.Dev.Highlight.Options
import Commands.Dev.Internal.Options
import Commands.Dev.MiniC.Options
import Commands.Dev.Parse.Options
import Commands.Dev.Runtime.Options
import Commands.Dev.Scope.Options
@ -33,7 +32,6 @@ data DevCommand
| Geb GebCommand
| Asm AsmCommand
| Runtime RuntimeCommand
| MiniC MiniCOptions
| Parse ParseOptions
| Scope ScopeOptions
| Termination TerminationCommand
@ -49,7 +47,6 @@ parseDevCommand =
commandGeb,
commandAsm,
commandRuntime,
commandMiniC,
commandParse,
commandScope,
commandShowRoot,
@ -64,13 +61,6 @@ commandHighlight =
(Highlight <$> parseHighlight)
(progDesc "Highlight a Juvix file")
commandMiniC :: Mod CommandFields DevCommand
commandMiniC =
command "minic" $
info
(MiniC <$> parseMiniC)
(progDesc "Translate a Juvix file to MiniC")
commandInternal :: Mod CommandFields DevCommand
commandInternal =
command "internal" $

2
app/Commands/Dev/Runtime/Options.hs
View File

@ -20,5 +20,5 @@ parseRuntimeCommand =
compileInfo :: ParserInfo RuntimeCommand
compileInfo =
info
(Compile <$> parseCompileOptions)
(Compile <$> parseCompileOptions parseInputCFile)
(progDesc "Compile a C file with Juvix runtime included")

38
app/Commands/Eval.hs Normal file
View File

@ -0,0 +1,38 @@
module Commands.Eval where
import Commands.Base
import Commands.Eval.Options
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.Pipeline qualified as Core
runCommand :: (Members '[Embed IO, App] r) => EvalOptions -> Sem r ()
runCommand opts@EvalOptions {..} = do
Core.CoreResult {..} <- runPipeline _evalInputFile upToCore
let tab = Core.toEval _coreResultTable
evalNode =
if
| isJust (_evalSymbolName) -> getNode' tab (selInfo tab)
| otherwise -> getNode' tab (mainInfo tab)
Eval.evalAndPrint opts tab evalNode
where
mainInfo :: Core.InfoTable -> Maybe Core.IdentifierInfo
mainInfo tab = do
s <- tab ^. Core.infoMain
tab ^. Core.infoIdentifiers . at s
selInfo :: Core.InfoTable -> Maybe Core.IdentifierInfo
selInfo tab = do
s <- _evalSymbolName
find (^. Core.identifierName . to (== s)) (tab ^. Core.infoIdentifiers)
getNode' :: Core.InfoTable -> Maybe Core.IdentifierInfo -> Core.Node
getNode' tab m = fromMaybe err (getNode tab m)
getNode :: Core.InfoTable -> Maybe Core.IdentifierInfo -> Maybe Core.Node
getNode tab m = m >>= \i -> tab ^. Core.identContext . at (i ^. Core.identifierSymbol)
err :: a
err = error "function not found"

51
app/Commands/Eval/Options.hs Normal file
View File

@ -0,0 +1,51 @@
module Commands.Eval.Options where
import CommonOptions
import Evaluator qualified as Eval
import Juvix.Compiler.Core.Pretty.Options qualified as Core
data EvalOptions = EvalOptions
{ _evalShowDeBruijn :: Bool,
_evalNoIO :: Bool,
_evalInputFile :: AppPath File,
_evalSymbolName :: Maybe Text
}
deriving stock (Data)
makeLenses ''EvalOptions
instance CanonicalProjection EvalOptions Core.Options where
project c =
Core.defaultOptions
{ Core._optShowDeBruijnIndices = c ^. evalShowDeBruijn
}
instance CanonicalProjection EvalOptions Eval.EvalOptions where
project c =
Eval.EvalOptions
{ _evalInputFile = c ^. evalInputFile,
_evalNoIO = c ^. evalNoIO
}
parseEvalOptions :: Parser EvalOptions
parseEvalOptions = do
_evalShowDeBruijn <-
switch
( long "show-de-bruijn"
<> help "Show variable de Bruijn indices"
)
_evalNoIO <-
switch
( long "no-io"
<> help "Don't interpret the IO effects"
)
_evalInputFile <- parseInputJuvixFile
_evalSymbolName <-
optional $
strOption
( long "symbol-name"
<> short 's'
<> help "Evaluate a specific function identifier (default: main)"
<> metavar "NAME"
)
pure EvalOptions {..}

16
app/Commands/Extra/Compile.hs
View File

@ -30,6 +30,8 @@ runCompile inputFile o = do
TargetWasm32Wasi -> runError (clangWasmWasiCompile inputFile o)
TargetNative64 -> runError (clangNativeCompile inputFile o)
TargetGeb -> return $ Right ()
TargetCore -> return $ Right ()
TargetAsm -> return $ Right ()
prepareRuntime :: forall r. (Members '[App, Embed IO] r) => Path Abs Dir -> CompileOptions -> Sem r ()
prepareRuntime buildDir o = do
@ -40,6 +42,8 @@ prepareRuntime buildDir o = do
TargetNative64 | o ^. compileDebug -> writeRuntime nativeDebugRuntime
TargetNative64 -> writeRuntime nativeReleaseRuntime
TargetGeb -> return ()
TargetCore -> return ()
TargetAsm -> return ()
where
wasiReleaseRuntime :: BS.ByteString
wasiReleaseRuntime = $(FE.makeRelativeToProject "runtime/_build.wasm32-wasi/libjuvix.a" >>= FE.embedFile)
@ -75,10 +79,6 @@ outputFile opts inputFile =
where
defaultOutputFile :: Path Abs File
defaultOutputFile = case opts ^. compileTarget of
TargetGeb ->
if
| opts ^. compileTerm -> replaceExtension' ".geb" inputFile
| otherwise -> replaceExtension' ".lisp" inputFile
TargetNative64 ->
if
| opts ^. compileCOutput -> replaceExtension' ".c" inputFile
@ -91,6 +91,14 @@ outputFile opts inputFile =
| opts ^. compilePreprocess -> addExtension' ".c" (addExtension' ".out" (removeExtension' inputFile))
| opts ^. compileAssembly -> replaceExtension' ".wat" inputFile
| otherwise -> replaceExtension' ".wasm" inputFile
TargetGeb ->
if
| opts ^. compileTerm -> replaceExtension' ".geb" inputFile
| otherwise -> replaceExtension' ".lisp" inputFile
TargetCore ->
replaceExtension' ".jvc" inputFile
TargetAsm ->
replaceExtension' ".jva" inputFile
clangNativeCompile ::
forall r.

10
app/Commands/Extra/Compile/Options.hs
View File

@ -7,6 +7,8 @@ data CompileTarget
= TargetWasm32Wasi
| TargetNative64
| TargetGeb
| TargetCore
| TargetAsm
deriving stock (Data, Bounded, Enum)
instance Show CompileTarget where
@ -14,6 +16,8 @@ instance Show CompileTarget where
TargetWasm32Wasi -> "wasm32-wasi"
TargetNative64 -> "native"
TargetGeb -> "geb"
TargetCore -> "core"
TargetAsm -> "asm"
data CompileOptions = CompileOptions
{ _compileDebug :: Bool,
@ -29,8 +33,8 @@ data CompileOptions = CompileOptions
makeLenses ''CompileOptions
parseCompileOptions :: Parser CompileOptions
parseCompileOptions = do
parseCompileOptions :: Parser (AppPath File) -> Parser CompileOptions
parseCompileOptions parseInputFile = do
_compileDebug <-
switch
( short 'g'
@ -63,7 +67,7 @@ parseCompileOptions = do
)
_compileTarget <- optCompileTarget
_compileOutputFile <- optional parseGenericOutputFile
_compileInputFile <- parseGenericInputFile
_compileInputFile <- parseInputFile
pure CompileOptions {..}
optCompileTarget :: Parser CompileTarget

14
app/Commands/Repl.hs
View File

@ -171,21 +171,19 @@ runCommand opts = do
defaultLoc = singletonInterval (mkInitialLoc replPath)
compileThenEval :: ReplContext -> String -> Repl (Either JuvixError Core.Node)
compileThenEval ctx s = bindEither (fmap transformNode' <$> compileString) eval
compileThenEval ctx s = bindEither compileString eval
where
eval :: Core.Node -> Repl (Either JuvixError Core.Node)
eval n =
liftIO $
mapLeft
(JuvixError @Core.CoreError)
<$> doEvalIO False defaultLoc infoTable n
let (tab', n') = runTransformations (Core.toEvalTransformations ++ opts ^. replTransformations) infoTable n
in liftIO $
mapLeft
(JuvixError @Core.CoreError)
<$> doEvalIO False defaultLoc tab' n'
infoTable :: Core.InfoTable
infoTable = ctx ^. replContextExpContext . contextCoreResult . Core.coreResultTable
transformNode' :: Core.Node -> Core.Node
transformNode' = transformNode infoTable (opts ^. replTransformations)
compileString :: Repl (Either JuvixError Core.Node)
compileString = liftIO $ compileExpressionIO' ctx (strip (pack s))

2
app/CommonOptions.hs
View File

@ -240,7 +240,7 @@ optTransformationIds =
(eitherReader parseTransf)
( long "transforms"
<> short 't'
<> value mempty
<> value []
<> metavar "[Transform]"
<> completer (mkCompleter (return . completionsString))
<> help "hint: use autocomplete"

2
app/TopCommand.hs
View File

@ -4,6 +4,7 @@ import Commands.Base
import Commands.Compile qualified as Compile
import Commands.Dev qualified as Dev
import Commands.Doctor qualified as Doctor
import Commands.Eval qualified as Eval
import Commands.Html qualified as Html
import Commands.Init qualified as Init
import Commands.Repl qualified as Repl
@ -29,5 +30,6 @@ runTopCommand = \case
Dev opts -> Dev.runCommand opts
Typecheck opts -> Typecheck.runCommand opts
Compile opts -> Compile.runCommand opts
Eval opts -> Eval.runCommand opts
Html opts -> Html.runCommand opts
JuvixRepl opts -> Repl.runCommand opts

18
app/TopCommand/Options.hs
View File

@ -1,8 +1,9 @@
module TopCommand.Options where
import Commands.Compile.Options
import Commands.Dev.Options
import Commands.Dev.Options qualified as Dev
import Commands.Doctor.Options
import Commands.Eval.Options
import Commands.Html.Options
import Commands.Repl.Options
import Commands.Typecheck.Options
@ -16,8 +17,9 @@ data TopCommand
| DisplayHelp
| Typecheck TypecheckOptions
| Compile CompileOptions
| Eval EvalOptions
| Html HtmlOptions
| Dev DevCommand
| Dev Dev.DevCommand
| Doctor DoctorOptions
| Init
| JuvixRepl ReplOptions
@ -98,9 +100,16 @@ commandCompile :: Mod CommandFields TopCommand
commandCompile =
command "compile" $
info
(Compile <$> parseCompile)
(Compile <$> parseCompileOptions parseInputJuvixFile)
(progDesc "Compile a Juvix file")
commandEval :: Mod CommandFields TopCommand
commandEval =
command "eval" $
info
(Eval <$> parseEvalOptions)
(progDesc "Evaluate a Juvix file")
commandHtml :: Mod CommandFields TopCommand
commandHtml =
command "html" $
@ -112,7 +121,7 @@ commandDev :: Mod CommandFields TopCommand
commandDev =
command "dev" $
info
(Dev <$> parseDevCommand)
(Dev <$> Dev.parseDevCommand)
(progDesc "Commands for the developers")
parseCompilerCommand :: Parser TopCommand
@ -123,6 +132,7 @@ parseCompilerCommand =
metavar "COMPILER_CMD",
commandCheck,
commandCompile,
commandEval,
commandHtml
]
)

2
juvix-stdlib

@ -1 +1 @@
Subproject commit 3a7d37febd078380032d409531123c9436256b86
Subproject commit 402ffe1f232c77ee8fe49ad645dfbfc8451f046a

1
package.yaml
View File

@ -66,6 +66,7 @@ dependencies:
- uniplate == 1.6.*
- unix-compat == 0.5.*
- unordered-containers == 0.2.*
- utf8-string == 1.0.*
- versions == 5.0.*
- yaml == 0.11.*

2
src/Juvix/Compiler/Asm/Extra/Base.hs
View File

@ -30,7 +30,7 @@ isFinalInstr = \case
Return -> True
TailCall {} -> True
TailCallClosures {} -> True
Failure -> True
Failure {} -> False
_ -> False
getConstrSize :: MemRep -> Int -> Int

2
src/Juvix/Compiler/Asm/Extra/Memory.hs
View File

@ -146,7 +146,7 @@ checkValueStack' loc tab tys mem = do
mapM_
( \(ty, idx) -> do
let ty' = fromJust $ topValueStack idx mem
unless (isSubtype ty' ty) $
unless (isSubtype' ty' ty) $
throw $
AsmError loc $
"type mismatch on value stack cell "

3
src/Juvix/Compiler/Asm/Extra/Recursors.hs
View File

@ -187,7 +187,8 @@ recurse' sig = go True
let argsNum = case _callType of
CallClosure -> length (typeArgs ty)
CallFun sym -> getFunInfo (sig ^. recursorInfoTable) sym ^. functionArgsNum
checkFunType ty
when (argsNum /= 0) $
checkFunType ty
when (ty /= TyDynamic && argsNum /= _callArgsNum) $
throw $
AsmError loc "invalid call: the number of supplied arguments doesn't match the number of expected arguments"

20
src/Juvix/Compiler/Asm/Extra/Type.hs
View File

@ -112,12 +112,8 @@ unifyTypes' loc tab ty1 ty2 =
-- 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 ->
| 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
@ -166,3 +162,17 @@ isSubtype ty1 ty2 = case (ty1, ty2) of
(TyFun {}, _) -> False
(_, TyFun {}) -> False
(_, TyConstr {}) -> False
isSubtype' :: Type -> Type -> Bool
isSubtype' ty1 ty2
-- The guard is to ensure correct behaviour with dynamic type targets. E.g.
-- `A -> B -> C -> D` should be a subtype of `(A, B) -> *`.
| tgt1 == TyDynamic || tgt2 == TyDynamic =
isSubtype
(curryType ty1)
(curryType ty2)
where
tgt1 = typeTarget (uncurryType ty1)
tgt2 = typeTarget (uncurryType ty2)
isSubtype' ty1 ty2 =
isSubtype ty1 ty2

34
src/Juvix/Compiler/Asm/Pretty/Base.hs
View File

@ -7,6 +7,7 @@ where
import Data.Foldable
import Data.HashMap.Strict qualified as HashMap
import Data.List.NonEmpty qualified as NonEmpty
import Data.Text qualified as Text
import Juvix.Compiler.Abstract.Data.Name
import Juvix.Compiler.Asm.Data.InfoTable
import Juvix.Compiler.Asm.Extra.Base
@ -36,20 +37,29 @@ wrapCore f c = do
opts <- ask
return $ run $ runReader (toCoreOptions opts) $ f c
quoteAsmName :: Text -> Text
quoteAsmName txt =
foldr
(uncurry Text.replace)
txt
[ ("$", "__dollar__"),
(":", "__colon__")
]
ppConstrName :: (Member (Reader Options) r) => Tag -> Sem r (Doc Ann)
ppConstrName tag = do
opts <- ask
let tab = opts ^. optInfoTable
maybe
(wrapCore Core.ppCode tag)
(\ci -> return $ annotate (AnnKind KNameConstructor) (pretty (ci ^. constructorName)))
(\ci -> return $ annotate (AnnKind KNameConstructor) (pretty (quoteAsmName (ci ^. constructorName))))
(HashMap.lookup tag (tab ^. infoConstrs))
ppIndName :: (Member (Reader Options) r) => Symbol -> Sem r (Doc Ann)
ppIndName sym = do
opts <- ask
let ci = fromMaybe impossible $ HashMap.lookup sym (opts ^. optInfoTable . infoInductives)
return $ annotate (AnnKind KNameInductive) (pretty (ci ^. inductiveName))
return $ annotate (AnnKind KNameInductive) (pretty (quoteAsmName (ci ^. inductiveName)))
ppFunName :: (Member (Reader Options) r) => Symbol -> Sem r (Doc Ann)
ppFunName sym = do
@ -60,7 +70,7 @@ ppFunName sym = do
annotate (AnnKind KNameFunction) $
pretty ("unnamed_function_" ++ show sym :: String)
)
(\fi -> return $ annotate (AnnKind KNameFunction) (pretty (fi ^. functionName)))
(\fi -> return $ annotate (AnnKind KNameFunction) (pretty (quoteAsmName (fi ^. functionName))))
(HashMap.lookup sym (tab ^. infoFunctions))
instance PrettyCode BuiltinDataTag where
@ -344,7 +354,7 @@ ppFunSig FunctionInfo {..} = do
targetty <- ppCode (typeTarget _functionType)
return $
keyword Str.function
<+> annotate (AnnKind KNameFunction) (pretty _functionName)
<+> annotate (AnnKind KNameFunction) (pretty (quoteAsmName _functionName))
<> encloseSep lparen rparen ", " argtys
<+> colon
<+> targetty
@ -353,19 +363,29 @@ ppFunSig FunctionInfo {..} = do
instance PrettyCode ConstructorInfo where
ppCode ConstructorInfo {..} = do
ty <- ppCode _constructorType
return $ annotate (AnnKind KNameConstructor) (pretty _constructorName) <+> colon <+> ty
return $ annotate (AnnKind KNameConstructor) (pretty (quoteAsmName _constructorName)) <+> colon <+> ty
instance PrettyCode InductiveInfo where
ppCode InductiveInfo {..} = do
ctrs <- mapM ppCode _inductiveConstructors
return $ kwInductive <+> annotate (AnnKind KNameInductive) (pretty _inductiveName) <+> braces' (vcat (map (<> semi) ctrs))
return $ kwInductive <+> annotate (AnnKind KNameInductive) (pretty (quoteAsmName _inductiveName)) <+> braces' (vcat (map (<> semi) ctrs))
instance PrettyCode InfoTable where
ppCode InfoTable {..} = do
inds <- mapM ppCode (HashMap.elems _infoInductives)
inds <- mapM ppCode (HashMap.elems (filterOutBuiltins _infoInductives))
funsigs <- mapM ppFunSig (HashMap.elems _infoFunctions)
funs <- mapM ppCode (HashMap.elems _infoFunctions)
return $ vcat (map (<> line) inds) <> line <> vcat funsigs <> line <> line <> vcat (map (<> line) funs)
where
filterOutBuiltins :: HashMap Symbol InductiveInfo -> HashMap Symbol InductiveInfo
filterOutBuiltins =
HashMap.filter
( \ii -> case ii ^. inductiveConstructors of
ci : _ -> case ci ^. constructorTag of
BuiltinTag _ -> False
UserTag _ -> True
[] -> True
)
{--------------------------------------------------------------------------------}
{- helper functions -}

68
src/Juvix/Compiler/Asm/Translation/FromCore.hs
View File

@ -8,7 +8,6 @@ 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
@ -60,6 +59,7 @@ genCode infoTable fi =
Core.NCtr ctr -> goConstr isTail tempSize refs ctr
Core.NLet lt -> goLet isTail tempSize refs lt
Core.NCase c -> goCase isTail tempSize refs c
Core.NIf x -> goIf isTail tempSize refs x
goVar :: Bool -> BinderList Value -> Core.Var -> Code'
goVar isTail refs Core.Var {..} =
@ -132,6 +132,7 @@ genCode infoTable fi =
(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 $
@ -165,50 +166,17 @@ genCode infoTable fi =
goCase :: Bool -> Int -> BinderList Value -> Core.Case -> Code'
goCase isTail tempSize refs (Core.Case {..}) =
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
}
)
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
@ -256,6 +224,18 @@ genCode infoTable fi =
. DL.cons (mkInstr Pop)
. go isTail tempSize refs
goIf :: Bool -> Int -> BinderList Value -> Core.If -> Code'
goIf isTail tempSize refs (Core.If {..}) =
DL.snoc
(go False tempSize refs _ifValue)
( Branch $
CmdBranch
{ _cmdBranchInfo = emptyInfo,
_cmdBranchTrue = DL.toList $ go isTail tempSize refs _ifTrue,
_cmdBranchFalse = DL.toList $ go isTail tempSize refs _ifFalse
}
)
genOp :: Core.BuiltinOp -> Command
genOp = \case
Core.OpIntAdd -> mkBinop IntAdd

3
src/Juvix/Compiler/Backend/C/Extra/Serialization.hs
View File

@ -1,5 +1,6 @@
module Juvix.Compiler.Backend.C.Extra.Serialization where
import Codec.Binary.UTF8.String qualified as UTF8
import Juvix.Compiler.Backend.C.Language
import Juvix.Extra.Strings qualified as Str
import Juvix.Prelude hiding (Binary, Unary)
@ -157,7 +158,7 @@ mkCExpr = \case
ExpressionLiteral l -> case l of
LiteralInt i -> CConst (CIntConst (cInteger i) C.undefNode)
LiteralChar c -> CConst (CCharConst (cChar c) C.undefNode)
LiteralString s -> CConst (CStrConst (cString (unpack s)) C.undefNode)
LiteralString s -> CConst (CStrConst (cString (UTF8.encodeString (unpack s))) C.undefNode)
ExpressionVar n -> CVar (mkIdent n) C.undefNode
ExpressionBinary Binary {..} ->
CBinary (mkBinaryOp _binaryOp) (mkCExpr _binaryLeft) (mkCExpr _binaryRight) C.undefNode

17
src/Juvix/Compiler/Concrete/Data/Builtins.hs
View File

@ -126,3 +126,20 @@ instance Pretty BuiltinAxiom where
BuiltinIOReadline -> Str.ioReadline
BuiltinTrace -> Str.trace_
BuiltinFail -> Str.fail_
data BuiltinType
= BuiltinTypeInductive BuiltinInductive
| BuiltinTypeAxiom BuiltinAxiom
deriving stock (Show, Eq, Ord, Generic, Data)
instance Hashable BuiltinType
instance Pretty BuiltinType where
pretty = \case
BuiltinTypeInductive ty -> pretty ty
BuiltinTypeAxiom ax -> pretty ax
builtinTypeToPrim :: BuiltinType -> BuiltinPrim
builtinTypeToPrim = \case
BuiltinTypeInductive b -> BuiltinsInductive b
BuiltinTypeAxiom b -> BuiltinsAxiom b

2
src/Juvix/Compiler/Core/Data/InfoTable.hs
View File

@ -72,7 +72,7 @@ data InductiveInfo = InductiveInfo
_inductiveConstructors :: [ConstructorInfo],
_inductiveParams :: [ParameterInfo],
_inductivePositive :: Bool,
_inductiveBuiltin :: Maybe BuiltinInductive
_inductiveBuiltin :: Maybe BuiltinType
}
data ConstructorInfo = ConstructorInfo

67
src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
View File

@ -39,6 +39,16 @@ getBoolSymbol = do
ci <- getConstructorInfo (BuiltinTag TagTrue)
return $ ci ^. constructorInductive
getIOSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
getIOSymbol = do
ci <- getConstructorInfo (BuiltinTag TagWrite)
return $ ci ^. constructorInductive
getNatSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
getNatSymbol = do
tab <- getInfoTable
return $ fromJust (lookupBuiltinInductive tab BuiltinNat) ^. inductiveSymbol
checkSymbolDefined :: (Member InfoTableBuilder r) => Symbol -> Sem r Bool
checkSymbolDefined sym = do
tab <- getInfoTable
@ -83,7 +93,7 @@ runInfoTableBuilder tab =
let identKind = IdentInd sym
whenJust
(ii ^. inductiveBuiltin)
(\b -> modify' (over infoBuiltins (HashMap.insert (BuiltinsInductive b) identKind)))
(\b -> modify' (over infoBuiltins (HashMap.insert (builtinTypeToPrim b) identKind)))
modify' (over infoInductives (HashMap.insert sym ii))
modify' (over identMap (HashMap.insert idt identKind))
RegisterIdentNode sym node ->
@ -111,29 +121,36 @@ createBuiltinConstr ::
Text ->
Type ->
Maybe BuiltinConstructor ->
Sem r ConstructorInfo
createBuiltinConstr sym tag nameTxt ty cblt = do
return $
ConstructorInfo
{ _constructorName = nameTxt,
_constructorLocation = Nothing,
_constructorTag = tag,
_constructorType = ty,
_constructorArgsNum = length (typeArgs ty),
_constructorInductive = sym,
_constructorBuiltin = cblt
}
ConstructorInfo
createBuiltinConstr sym tag nameTxt ty cblt =
ConstructorInfo
{ _constructorName = nameTxt,
_constructorLocation = Nothing,
_constructorTag = tag,
_constructorType = ty,
_constructorArgsNum = length (typeArgs ty),
_constructorInductive = sym,
_constructorBuiltin = cblt
}
builtinConstrs ::
Symbol ->
Type ->
[(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] ->
[ConstructorInfo]
builtinConstrs sym ty ctrs =
map (\(tag, name, fty, cblt) -> createBuiltinConstr sym tag name (fty ty) cblt) ctrs
declareInductiveBuiltins ::
(Member InfoTableBuilder r) =>
Text ->
Maybe BuiltinInductive ->
Maybe BuiltinType ->
[(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] ->
Sem r ()
declareInductiveBuiltins indName blt ctrs = do
sym <- freshSymbol
let ty = mkTypeConstr' sym []
constrs <- mapM (\(tag, name, fty, cblt) -> createBuiltinConstr sym tag name (fty ty) cblt) ctrs
constrs = builtinConstrs sym ty ctrs
registerInductive
indName
( InductiveInfo
@ -149,22 +166,26 @@ declareInductiveBuiltins indName blt ctrs = do
)
mapM_ (\ci -> registerConstructor (ci ^. constructorName) ci) constrs
builtinIOConstrs :: [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)]
builtinIOConstrs =
[ (BuiltinTag TagReturn, "return", mkPi' mkDynamic', Nothing),
(BuiltinTag TagBind, "bind", \ty -> mkPi' ty (mkPi' (mkPi' mkDynamic' ty) ty), Nothing),
(BuiltinTag TagWrite, "write", mkPi' mkDynamic', Nothing),
(BuiltinTag TagReadLn, "readLn", id, Nothing)
]
declareIOBuiltins :: (Member InfoTableBuilder r) => Sem r ()
declareIOBuiltins =
declareInductiveBuiltins
"IO"
Nothing
[ (BuiltinTag TagReturn, "return", mkPi' mkDynamic', Nothing),
(BuiltinTag TagBind, "bind", \ty -> mkPi' ty (mkPi' (mkPi' mkDynamic' ty) ty), Nothing),
(BuiltinTag TagWrite, "write", mkPi' mkDynamic', Nothing),
(BuiltinTag TagReadLn, "readLn", id, Nothing)
]
(Just (BuiltinTypeAxiom BuiltinIO))
builtinIOConstrs
declareBoolBuiltins :: (Member InfoTableBuilder r) => Sem r ()
declareBoolBuiltins =
declareInductiveBuiltins
"bool"
(Just BuiltinBool)
(Just (BuiltinTypeInductive BuiltinBool))
[ (BuiltinTag TagTrue, "true", const mkTypeBool', Just BuiltinBoolTrue),
(BuiltinTag TagFalse, "false", const mkTypeBool', Just BuiltinBoolFalse)
]
@ -175,7 +196,7 @@ declareNatBuiltins = do
tagSuc <- freshTag
declareInductiveBuiltins
"nat"
(Just BuiltinNat)
(Just (BuiltinTypeInductive BuiltinNat))
[ (tagZero, "zero", id, Just BuiltinNatZero),
(tagSuc, "suc", \x -> mkPi' x x, Just BuiltinNatSuc)
]

41
src/Juvix/Compiler/Core/Data/TransformationId.hs
View File

@ -14,4 +14,45 @@ data TransformationId
| UnrollRecursion
| ComputeTypeInfo
| MatchToCase
| EtaExpandApps
deriving stock (Data, Bounded, Enum)
data PipelineId
= PipelineEval
| PipelineGeb
| PipelineStripped
deriving stock (Data, Bounded, Enum)
data TransformationLikeId
= TransformationId TransformationId
| PipelineId PipelineId
deriving stock (Data)
allTransformationLikeIds :: [TransformationLikeId]
allTransformationLikeIds =
map TransformationId allElements
++ map PipelineId allElements
fromTransformationLike :: TransformationLikeId -> [TransformationId]
fromTransformationLike = \case
TransformationId i -> [i]
PipelineId p -> pipeline p
fromTransformationLikes :: [TransformationLikeId] -> [TransformationId]
fromTransformationLikes = concatMap fromTransformationLike
toStrippedTransformations :: [TransformationId]
toStrippedTransformations =
toEvalTransformations ++ [LambdaLetRecLifting, TopEtaExpand, MoveApps, RemoveTypeArgs]
toGebTransformations :: [TransformationId]
toGebTransformations = toEvalTransformations ++ [UnrollRecursion, ComputeTypeInfo]
toEvalTransformations :: [TransformationId]
toEvalTransformations = [EtaExpandApps, MatchToCase, NatToInt, ConvertBuiltinTypes]
pipeline :: PipelineId -> [TransformationId]
pipeline = \case
PipelineEval -> toEvalTransformations
PipelineGeb -> toGebTransformations
PipelineStripped -> toStrippedTransformations

99
src/Juvix/Compiler/Core/Data/TransformationId/Parser.hs
View File

@ -14,7 +14,7 @@ parseHelper p t = case runParser p "<input>" t of
Right r -> return r
parseTransformations :: Text -> Either Text [TransformationId]
parseTransformations = parseHelper transformations
parseTransformations = fmap fromTransformationLikes . parseHelper transformations
completionsString :: String -> [String]
completionsString = map unpack . completions . pack
@ -22,36 +22,23 @@ completionsString = map unpack . completions . pack
completions :: Text -> [Text]
completions = fromRight [] . parseHelper pcompletions
transformations :: (MonadParsec e Text m) => m [TransformationId]
transformations :: (MonadParsec e Text m) => m [TransformationLikeId]
transformations = do
L.hspace
sepEndBy transformation comma <* eof
sepEndBy transformationLike comma <* eof
-- | returns a possible list of completions
pcompletions :: (MonadParsec e Text m) => m [Text]
pcompletions = do
L.hspace
l <- sepEndBy transformation comma
l <- sepEndBy transformationLike comma
rest <- Text.strip <$> takeRest
return [ppTransL (notNull l) l <> str | str <- allStrings, Text.isPrefixOf rest str]
where
ppTransL :: Bool -> [TransformationId] -> Text
ppTransL :: Bool -> [TransformationLikeId] -> Text
ppTransL c =
let f :: Text -> Text = if c then (<> ",") else id
in f . Text.intercalate "," . map ppTrans
ppTrans :: TransformationId -> Text
ppTrans = \case
LambdaLetRecLifting -> strLifting
LetRecLifting -> strLetRecLifting
TopEtaExpand -> strTopEtaExpand
MatchToCase -> strMatchToCase
Identity -> strIdentity
RemoveTypeArgs -> strRemoveTypeArgs
MoveApps -> strMoveApps
NatToInt -> strNatToInt
ConvertBuiltinTypes -> strConvertBuiltinTypes
ComputeTypeInfo -> strComputeTypeInfo
UnrollRecursion -> strUnrollRecursion
in f . Text.intercalate "," . map transformationLikeText
lexeme :: (MonadParsec e Text m) => m a -> m a
lexeme = L.lexeme L.hspace
@ -62,33 +49,54 @@ comma = symbol ","
symbol :: (MonadParsec e Text m) => Text -> m ()
symbol = void . lexeme . chunk
transformation :: (MonadParsec e Text m) => m TransformationId
transformation =
symbol strLifting $> LambdaLetRecLifting
<|> symbol strLetRecLifting $> LetRecLifting
<|> symbol strIdentity $> Identity
<|> symbol strTopEtaExpand $> TopEtaExpand
<|> symbol strRemoveTypeArgs $> RemoveTypeArgs
<|> symbol strMoveApps $> MoveApps
<|> symbol strNatToInt $> NatToInt
<|> symbol strConvertBuiltinTypes $> ConvertBuiltinTypes
<|> symbol strUnrollRecursion $> UnrollRecursion
<|> symbol strComputeTypeInfo $> ComputeTypeInfo
<|> symbol strMatchToCase $> MatchToCase
transformationLike :: MonadParsec e Text m => m TransformationLikeId
transformationLike =
TransformationId <$> transformation
<|> PipelineId <$> parsePipeline
pipelineText :: PipelineId -> Text
pipelineText = \case
PipelineEval -> strEvalPipeline
PipelineGeb -> strGebPipeline
PipelineStripped -> strStrippedPipeline
transformationLikeText :: TransformationLikeId -> Text
transformationLikeText = \case
TransformationId t -> transformationText t
PipelineId p -> pipelineText p
transformationText :: TransformationId -> Text
transformationText = \case
LambdaLetRecLifting -> strLifting
LetRecLifting -> strLetRecLifting
TopEtaExpand -> strTopEtaExpand
MatchToCase -> strMatchToCase
EtaExpandApps -> strEtaExpandApps
Identity -> strIdentity
RemoveTypeArgs -> strRemoveTypeArgs
MoveApps -> strMoveApps
NatToInt -> strNatToInt
ConvertBuiltinTypes -> strConvertBuiltinTypes
ComputeTypeInfo -> strComputeTypeInfo
UnrollRecursion -> strUnrollRecursion
parsePipeline :: MonadParsec e Text m => m PipelineId
parsePipeline = choice [symbol (pipelineText t) $> t | t <- allElements]
transformation :: MonadParsec e Text m => m TransformationId
transformation = choice [symbol (transformationText t) $> t | t <- allElements]
allStrings :: [Text]
allStrings =
[ strLifting,
strTopEtaExpand,
strIdentity,
strRemoveTypeArgs,
strMoveApps,
strNatToInt,
strConvertBuiltinTypes,
strUnrollRecursion,
strComputeTypeInfo,
strMatchToCase
]
allStrings = map transformationLikeText allTransformationLikeIds
strEvalPipeline :: Text
strEvalPipeline = "pipeline-eval"
strGebPipeline :: Text
strGebPipeline = "pipeline-geb"
strStrippedPipeline :: Text
strStrippedPipeline = "pipeline-stripped"
strLifting :: Text
strLifting = "lifting"
@ -102,6 +110,9 @@ strTopEtaExpand = "top-eta-expand"
strMatchToCase :: Text
strMatchToCase = "match-to-case"
strEtaExpandApps :: Text
strEtaExpandApps = "eta-expand-apps"
strIdentity :: Text
strIdentity = "identity"

2
src/Juvix/Compiler/Core/Evaluator.hs
View File

@ -75,7 +75,7 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
case eval' env v of
NCtr (Constr _ tag args) -> branch n env args tag def bs
v' -> evalError "matching on non-data" (substEnv env (mkCase i sym v' bs def))
NMatch (Match _ vs bs) ->
NMatch (Match _ _ _ vs bs) ->
let !vs' = map' (eval' env) (toList vs)
in match n env vs' bs
NPi {} -> substEnv env n

235
src/Juvix/Compiler/Core/Extra/Base.hs
View File

@ -5,6 +5,7 @@ module Juvix.Compiler.Core.Extra.Base
where
import Data.Functor.Identity
import Data.List.NonEmpty qualified as NonEmpty
import Juvix.Compiler.Core.Data.BinderList (BinderList)
import Juvix.Compiler.Core.Info qualified as Info
import Juvix.Compiler.Core.Language
@ -52,32 +53,26 @@ mkConstr' = mkConstr Info.empty
mkLambda :: Info -> Binder -> Node -> Node
mkLambda i bi b = NLam (Lambda i bi b)
mkLambda' :: Node -> Node
mkLambda' = mkLambda Info.empty emptyBinder
mkLambda' :: Type -> Node -> Node
mkLambda' ty = mkLambda Info.empty (mkBinder' ty)
mkLambdaTy :: Node -> Node -> Node
mkLambdaTy ty = mkLambda Info.empty (Binder "?" Nothing ty)
mkLambdas' :: [Type] -> Node -> Node
mkLambdas' tys n = foldl' (flip mkLambda') n (reverse tys)
mkLambdasTy :: [Type] -> Node -> Node
mkLambdasTy tys n = foldl' (flip mkLambdaTy) n (reverse tys)
mkLetItem' :: Node -> LetItem
mkLetItem' = LetItem emptyBinder
mkLetItem' :: Type -> Node -> LetItem
mkLetItem' ty = LetItem (mkBinder' ty)
mkLet :: Info -> Binder -> Node -> Node -> Node
mkLet i bi v b = NLet (Let i (LetItem bi v) b)
mkLetTy :: Info -> Type -> Node -> Node -> Node
mkLetTy i ty = mkLet i (Binder "?" Nothing ty)
mkLet' :: Node -> Node -> Node
mkLet' = mkLet Info.empty emptyBinder
mkLet' :: Type -> Node -> Node -> Node
mkLet' ty = mkLet Info.empty (mkBinder' ty)
mkLetRec :: Info -> NonEmpty LetItem -> Node -> Node
mkLetRec i vs b = NRec (LetRec i vs b)
mkLetRec' :: NonEmpty Node -> Node -> Node
mkLetRec' = mkLetRec Info.empty . fmap mkLetItem'
mkLetRec' :: NonEmpty (Type, Node) -> Node -> Node
mkLetRec' = mkLetRec Info.empty . fmap (uncurry mkLetItem')
mkCase :: Info -> Symbol -> Node -> [CaseBranch] -> Maybe Node -> Node
mkCase i sym v bs def = NCase (Case i sym v bs def)
@ -85,10 +80,10 @@ mkCase i sym v bs def = NCase (Case i sym v bs def)
mkCase' :: Symbol -> Node -> [CaseBranch] -> Maybe Node -> Node
mkCase' = mkCase Info.empty
mkMatch :: Info -> NonEmpty Node -> [MatchBranch] -> Node
mkMatch i vs bs = NMatch (Match i vs bs)
mkMatch :: Info -> NonEmpty Type -> Type -> NonEmpty Node -> [MatchBranch] -> Node
mkMatch i vtys rty vs bs = NMatch (Match i vtys rty vs bs)
mkMatch' :: NonEmpty Node -> [MatchBranch] -> Node
mkMatch' :: NonEmpty Type -> Type -> NonEmpty Node -> [MatchBranch] -> Node
mkMatch' = mkMatch Info.empty
mkMatchBranch :: Info -> NonEmpty Pattern -> Node -> MatchBranch
@ -112,6 +107,12 @@ mkIf i sym v b1 b2 = mkCase i sym v [br] (Just b2)
mkIf' :: Symbol -> Node -> Node -> Node -> Node
mkIf' = mkIf Info.empty
mkBinder :: Text -> Type -> Binder
mkBinder name ty = Binder name Nothing ty
mkBinder' :: Type -> Binder
mkBinder' ty = Binder "?" Nothing ty
{------------------------------------------------------------------------}
{- Type constructors -}
@ -139,6 +140,9 @@ mkUniv i l = NUniv (Univ i l)
mkUniv' :: Int -> Type
mkUniv' = mkUniv Info.empty
mkSmallUniv :: Type
mkSmallUniv = mkUniv' (fromIntegral smallLevel)
mkTypeConstr :: Info -> Symbol -> [Type] -> Type
mkTypeConstr i sym args = NTyp (TypeConstr i sym args)
@ -197,10 +201,9 @@ isDynamic = \case
NDyn {} -> True
_ -> False
isTypeConstr :: Type -> Bool
isTypeConstr ty = case typeTarget ty of
NUniv {} -> True
_ -> False
isInductive :: Type -> Bool
isInductive NTyp {} = True
isInductive _ = False
-- | `expandType argtys ty` expands the dynamic target of `ty` to match the
-- number of arguments with types specified by `argstys`. For example,
@ -252,11 +255,6 @@ mkLambdaB = mkLambda mempty
mkLambdasB :: [Binder] -> Node -> Node
mkLambdasB is n = foldl' (flip mkLambdaB) n (reverse is)
mkLambdas' :: Int -> Node -> Node
mkLambdas' k
| k < 0 = impossible
| otherwise = mkLambdasB (replicate k emptyBinder)
-- | \x\y b gives ([y, x], b)
unfoldLambdasRev :: Node -> ([LambdaLhs], Node)
unfoldLambdasRev = go []
@ -272,6 +270,9 @@ unfoldLambdas = first reverse . unfoldLambdasRev
unfoldLambdas' :: Node -> (Int, Node)
unfoldLambdas' = first length . unfoldLambdas
lambdaTypes :: Node -> [Type]
lambdaTypes = map (\LambdaLhs {..} -> _lambdaLhsBinder ^. binderType) . fst . unfoldLambdas
isType :: Node -> Bool
isType = \case
NPi {} -> True
@ -295,15 +296,18 @@ isType = \case
{------------------------------------------------------------------------}
{- functions on Pattern -}
getPatternBinders :: Pattern -> [Binder]
getPatternBinders = reverse . go []
getPatternParts :: Pattern -> [Either Binder Node]
getPatternParts = reverse . go []
where
go :: [Binder] -> Pattern -> [Binder]
go :: [Either Binder Node] -> Pattern -> [Either Binder Node]
go acc = \case
PatConstr PatternConstr {..} -> foldl' go acc _patternConstrArgs
PatBinder p -> go (p ^. patternBinder : acc) (p ^. patternBinderPattern)
PatConstr PatternConstr {..} -> Right _patternConstrType : foldl' go acc _patternConstrArgs
PatBinder p -> go (Left (p ^. patternBinder) : acc) (p ^. patternBinderPattern)
PatWildcard {} -> acc
getPatternBinders :: Pattern -> [Binder]
getPatternBinders = lefts . getPatternParts
getPatternInfos :: Pattern -> [Info]
getPatternInfos = reverse . go []
where
@ -313,6 +317,32 @@ getPatternInfos = reverse . go []
PatBinder PatternBinder {..} -> go acc _patternBinderPattern
PatWildcard PatternWildcard {..} -> _patternWildcardInfo : acc
mapPatternBinders :: (Int -> Binder -> Binder) -> Pattern -> Pattern
mapPatternBinders f = snd . go 0
where
go :: Int -> Pattern -> (Int, Pattern)
go k = \case
PatConstr p ->
let (k', rargs') =
foldl'
( \(m, acc) pat ->
let (m', pat') = go m pat
in (m', pat' : acc)
)
(k, [])
(p ^. patternConstrArgs)
in (k', PatConstr p {_patternConstrArgs = reverse rargs'})
PatBinder p ->
let (k', pat') = go (k + 1) (p ^. patternBinderPattern)
in ( k',
PatBinder
p
{ _patternBinder = f k (p ^. patternBinder),
_patternBinderPattern = pat'
}
)
PatWildcard p -> (k, PatWildcard p)
{------------------------------------------------------------------------}
{- generic Node destruction -}
@ -342,7 +372,7 @@ data NodeDetails = NodeDetails
-- | 'nodeReassemble' reassembles the node from the info, the subinfos and
-- the children (which should be in the same fixed order as in the
-- 'nodeSubinfos' and 'nodeChildren' components).
_nodeReassemble :: Info -> [Info] -> [NodeChild] -> Node
_nodeReassemble :: Info -> [Info] -> [Node] -> Node
}
makeLenses ''NodeDetails
@ -374,44 +404,44 @@ manyBinders bis n =
_childBindersNum = length bis
}
type Reassemble = Info -> [Info] -> [NodeChild] -> Node
type Reassemble = Info -> [Info] -> [Node] -> Node
{-# INLINE noChildren #-}
noChildren :: (Info -> Node) -> Reassemble
noChildren f i _ _ = f i
{-# INLINE oneChild #-}
oneChild :: (Info -> NodeChild -> Node) -> Reassemble
oneChild :: (Info -> Node -> Node) -> Reassemble
oneChild f i _ ch = case ch of
[c] -> f i c
_ -> impossible
{-# INLINE twoChildren #-}
twoChildren :: (Info -> NodeChild -> NodeChild -> Node) -> Reassemble
twoChildren :: (Info -> Node -> Node -> Node) -> Reassemble
twoChildren f i _ ch = case ch of
[l, r] -> f i l r
_ -> impossible
{-# INLINE threeChildren #-}
threeChildren :: (Info -> NodeChild -> NodeChild -> NodeChild -> Node) -> Reassemble
threeChildren :: (Info -> Node -> Node -> Node -> Node) -> Reassemble
threeChildren f i _ ch = case ch of
[a, b, c] -> f i a b c
_ -> impossible
{-# INLINE manyChildren #-}
manyChildren :: (Info -> [NodeChild] -> Node) -> Reassemble
manyChildren :: (Info -> [Node] -> Node) -> Reassemble
manyChildren f i _ = f i
{-# INLINE someChildren #-}
someChildren :: (Info -> NonEmpty NodeChild -> Node) -> Reassemble
someChildren :: (Info -> NonEmpty Node -> Node) -> Reassemble
someChildren f i _ = f i . nonEmpty'
{-# INLINE someChildrenI #-}
someChildrenI :: (Info -> [Info] -> NonEmpty NodeChild -> Node) -> Reassemble
someChildrenI :: (Info -> [Info] -> NonEmpty Node -> Node) -> Reassemble
someChildrenI f i is = f i is . nonEmpty'
{-# INLINE twoManyChildrenI #-}
twoManyChildrenI :: (Info -> [Info] -> NodeChild -> NodeChild -> [NodeChild] -> Node) -> Reassemble
twoManyChildrenI :: (Info -> [Info] -> Node -> Node -> [Node] -> Node) -> Reassemble
twoManyChildrenI f i is = \case
(x : y : xs) -> f i is x y xs
_ -> impossible
@ -450,21 +480,21 @@ destruct = \case
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = map noBinders [l, r],
_nodeReassemble = twoChildren $ \i' l' r' -> mkApp i' (l' ^. childNode) (r' ^. childNode)
_nodeReassemble = twoChildren $ \i' l' r' -> mkApp i' l' r'
}
NBlt (BuiltinApp i op args) ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = map noBinders args,
_nodeReassemble = manyChildren $ \i' args' -> mkBuiltinApp i' op (map (^. childNode) args')
_nodeReassemble = manyChildren $ \i' args' -> mkBuiltinApp i' op args'
}
NCtr (Constr i tag args) ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = map noBinders args,
_nodeReassemble = manyChildren $ \i' -> mkConstr i' tag . map (^. childNode)
_nodeReassemble = manyChildren $ \i' -> mkConstr i' tag
}
NLam (Lambda i bi b) ->
NodeDetails
@ -473,8 +503,8 @@ destruct = \case
_nodeChildren = [noBinders (bi ^. binderType), oneBinder bi b],
_nodeReassemble = twoChildren $ \i' ty' b' ->
let binder' :: Binder
binder' = set binderType (ty' ^. childNode) bi
in mkLambda i' binder' (b' ^. childNode)
binder' = set binderType ty' bi
in mkLambda i' binder' b'
}
NLet (Let i (LetItem bi v) b) ->
NodeDetails
@ -483,8 +513,8 @@ destruct = \case
_nodeChildren = [noBinders (bi ^. binderType), noBinders v, oneBinder bi b],
_nodeReassemble = threeChildren $ \i' ty' v' b' ->
let binder' :: Binder
binder' = set binderType (ty' ^. childNode) bi
in mkLet i' binder' (v' ^. childNode) (b' ^. childNode)
binder' = set binderType ty' bi
in mkLet i' binder' v' b'
}
NRec (LetRec i vs b) ->
NodeDetails
@ -501,11 +531,11 @@ destruct = \case
let numItems :: Int
numItems = length vs
tys' :: [Type]
values' :: [NodeChild]
(values', tys') = second (map (^. childNode)) (splitAtExact numItems valuesTys')
values' :: [Node]
(values', tys') = splitAtExact numItems valuesTys'
items' =
nonEmpty'
[ LetItem (Binder name loc ty') (v' ^. childNode)
[ LetItem (Binder name loc ty') v'
| (v', ty', name, loc) <-
zip4Exact
values'
@ -513,7 +543,7 @@ destruct = \case
(map (^. letItemBinder . binderName) (toList vs))
(map (^. letItemBinder . binderLocation) (toList vs))
]
in mkLetRec i' items' (b' ^. childNode)
in mkLetRec i' items' b'
}
NCase (Case i sym v brs mdef) ->
let branchChildren :: [([Binder], NodeChild)]
@ -526,21 +556,21 @@ destruct = \case
allNodes :: [NodeChild]
allNodes =
concat
[ b : map (noBinders . (^. binderType)) bi
| (bi, b) <- branchChildren
[ br : reverse (foldl' (\r b -> manyBinders (take (length r) bi) (b ^. binderType) : r) [] bi)
| (bi, br) <- branchChildren
]
mkBranch :: Info -> CaseBranch -> Sem '[Input (Maybe NodeChild)] CaseBranch
mkBranch :: Info -> CaseBranch -> Sem '[Input (Maybe Node)] CaseBranch
mkBranch nfo' br = do
b' <- input'
let nBinders = br ^. caseBranchBindersNum
tys' <- map (^. childNode) <$> replicateM nBinders input'
tys' <- replicateM nBinders input'
return
br
{ _caseBranchInfo = nfo',
_caseBranchBinders = zipWithExact (set binderType) tys' (b' ^. childBinders),
_caseBranchBody = b' ^. childNode
_caseBranchBinders = zipWithExact (set binderType) tys' (br ^. caseBranchBinders),
_caseBranchBody = b'
}
mkBranches :: [Info] -> [NodeChild] -> [CaseBranch]
mkBranches :: [Info] -> [Node] -> [CaseBranch]
mkBranches is' allNodes' =
run $
runInputList allNodes' $
@ -555,7 +585,7 @@ destruct = \case
_nodeSubinfos = map (^. caseBranchInfo) brs,
_nodeChildren = noBinders v : allNodes,
_nodeReassemble = someChildrenI $ \i' is' (v' :| allNodes') ->
mkCase i' sym (v' ^. childNode) (mkBranches is' allNodes') Nothing
mkCase i' sym v' (mkBranches is' allNodes') Nothing
}
Just def ->
NodeDetails
@ -563,23 +593,32 @@ destruct = \case
_nodeSubinfos = map (^. caseBranchInfo) brs,
_nodeChildren = noBinders v : noBinders def : allNodes,
_nodeReassemble = twoManyChildrenI $ \i' is' v' def' allNodes' ->
mkCase i' sym (v' ^. childNode) (mkBranches is' allNodes') (Just (def' ^. childNode))
mkCase i' sym v' (mkBranches is' allNodes') (Just def')
}
NMatch (Match i vs branches) ->
NMatch (Match i vtys rty vs branches) ->
let allNodes :: [NodeChild]
allNodes =
concat
[ b
: map (noBinders . (^. binderType)) bis
| (bis, b) <- branchChildren
]
where
branchChildren :: [([Binder], NodeChild)]
branchChildren =
[ (binders, manyBinders binders (br ^. matchBranchBody))
| br <- branches,
let binders = concatMap getPatternBinders (toList (br ^. matchBranchPatterns))
noBinders rty
: map noBinders (toList vtys)
++ map noBinders (toList vs)
++ concat
[ br
: reverse (foldl' (\acc b -> manyBinders (take (length acc) (lefts bis)) (getNode b) : acc) [] bis)
| (bis, br) <- branchChildren
]
where
branchChildren :: [([Either Binder Node], NodeChild)]
branchChildren =
[ (parts, manyBinders (lefts parts) (br ^. matchBranchBody))
| br <- branches,
let parts = concatMap getPatternParts (toList (br ^. matchBranchPatterns))
]
getNode :: Either Binder Node -> Node
getNode = \case
Left b -> b ^. binderType
Right n -> n
branchInfos :: [Info]
branchInfos =
concat
@ -588,7 +627,8 @@ destruct = \case
: concatMap getPatternInfos (br ^. matchBranchPatterns)
| br <- branches
]
setPatternsInfos :: forall r. (Members '[Input (Maybe Info), Input (Maybe NodeChild)] r) => NonEmpty Pattern -> Sem r (NonEmpty Pattern)
-- sets the infos and the binder types in the patterns
setPatternsInfos :: forall r. (Members '[Input (Maybe Info), Input (Maybe Node)] r) => NonEmpty Pattern -> Sem r (NonEmpty Pattern)
setPatternsInfos = mapM goPattern
where
goPattern :: Pattern -> Sem r Pattern
@ -597,20 +637,21 @@ destruct = \case
i' <- input'
return (PatWildcard (set patternWildcardInfo i' x))
PatBinder x -> do
ty <- (^. childNode) <$> input'
ty <- input'
let _patternBinder = set binderType ty (x ^. patternBinder)
_patternBinderPattern <- goPattern (x ^. patternBinderPattern)
return (PatBinder PatternBinder {..})
PatConstr x -> do
i' <- input'
args' <- mapM goPattern (x ^. patternConstrArgs)
return (PatConstr (set patternConstrInfo i' (set patternConstrArgs args' x)))
ty <- input'
return (PatConstr (set patternConstrType ty (set patternConstrInfo i' (set patternConstrArgs args' x))))
in NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = branchInfos,
_nodeChildren = map noBinders (toList vs) ++ allNodes,
_nodeChildren = allNodes,
_nodeReassemble = someChildrenI $ \i' is' chs' ->
let mkBranch :: MatchBranch -> Sem '[Input (Maybe NodeChild), Input (Maybe Info)] MatchBranch
let mkBranch :: MatchBranch -> Sem '[Input (Maybe Node), Input (Maybe Info)] MatchBranch
mkBranch br = do
bi' <- input'
b' <- input'
@ -619,19 +660,28 @@ destruct = \case
br
{ _matchBranchInfo = bi',
_matchBranchPatterns = pats',
_matchBranchBody = b' ^. childNode
_matchBranchBody = b'
}
numVals = length vs
values' :: NonEmpty NodeChild
branchesChilds' :: [NodeChild]
(values', branchesChilds') = first nonEmpty' (splitAtExact numVals (toList chs'))
values' :: NonEmpty Node
valueTypes' :: NonEmpty Node
returnType' :: Node
branchesChildren' :: [Node]
returnType' = head chs'
(valueTypes', chs'') = first nonEmpty' (splitAtExact numVals (NonEmpty.tail chs'))
(values', branchesChildren') = first nonEmpty' (splitAtExact numVals chs'')
branches' :: [MatchBranch]
branches' =
run $
runInputList is' $
runInputList branchesChilds' $
runInputList branchesChildren' $
mapM mkBranch branches
in mkMatch i' (fmap (^. childNode) values') branches'
in mkMatch
i'
valueTypes'
returnType'
values'
branches'
}
NPi (Pi i bi b) ->
NodeDetails
@ -640,8 +690,8 @@ destruct = \case
_nodeChildren = [noBinders (bi ^. binderType), oneBinder bi b],
_nodeReassemble = twoChildren $ \i' bi' b' ->
let binder' :: Binder
binder' = set binderType (bi' ^. childNode) bi
in mkPi i' binder' (b' ^. childNode)
binder' = set binderType bi' bi
in mkPi i' binder' b'
}
NUniv (Univ i l) ->
NodeDetails
@ -655,7 +705,7 @@ destruct = \case
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = map noBinders args,
_nodeReassemble = manyChildren $ \i' -> mkTypeConstr i' sym . map (^. childNode)
_nodeReassemble = manyChildren $ \i' -> mkTypeConstr i' sym
}
NPrim (TypePrim i prim) ->
NodeDetails
@ -677,14 +727,11 @@ destruct = \case
_nodeSubinfos = [],
_nodeChildren = oneBinder bi b : map noBinders env,
_nodeReassemble = someChildren $ \i' (b' :| env') ->
Closure (map (^. childNode) env') (Lambda i' bi (b' ^. childNode))
Closure env' (Lambda i' bi b')
}
reassembleDetails :: NodeDetails -> [Node] -> Node
reassembleDetails d ns = (d ^. nodeReassemble) (d ^. nodeInfo) (d ^. nodeSubinfos) children'
where
children' :: [NodeChild]
children' = zipWithExact (set childNode) ns (d ^. nodeChildren)
reassembleDetails d ns = (d ^. nodeReassemble) (d ^. nodeInfo) (d ^. nodeSubinfos) ns
reassemble :: Node -> [Node] -> Node
reassemble = reassembleDetails . destruct
@ -708,7 +755,7 @@ modifyInfoM f n =
in do
i' <- f (ni ^. nodeInfo)
is' <- mapM f (ni ^. nodeSubinfos)
return ((ni ^. nodeReassemble) i' is' (ni ^. nodeChildren))
return ((ni ^. nodeReassemble) i' is' (map (^. childNode) (ni ^. nodeChildren)))
modifyInfo :: (Info -> Info) -> Node -> Node
modifyInfo f n = runIdentity $ modifyInfoM (pure . f) n

3
src/Juvix/Compiler/Core/Extra/Stripped/Base.hs
View File

@ -41,3 +41,6 @@ mkLet binder value body = NLet (Let () item body)
mkCase :: Symbol -> Node -> [CaseBranch] -> Maybe Node -> Node
mkCase sym v bs def = NCase (Case () sym v bs def)
mkIf :: Node -> Node -> Node -> Node
mkIf v br1 br2 = NIf (If () v br1 br2)

104
src/Juvix/Compiler/Core/Extra/Utils.hs
View File

@ -22,7 +22,6 @@ import Juvix.Compiler.Core.Extra.Recursors
import Juvix.Compiler.Core.Extra.Recursors.Fold.Named
import Juvix.Compiler.Core.Extra.Recursors.Map.Named
import Juvix.Compiler.Core.Extra.SubstEnv
import Juvix.Compiler.Core.Info.TypeInfo
import Juvix.Compiler.Core.Language
isClosed :: Node -> Bool
@ -92,24 +91,39 @@ cosmos f = ufoldA reassemble f
-- if fv = x1, x2, .., xn
-- the result is of the form λx1 λx2 .. λ xn b
captureFreeVars :: [(Index, Binder)] -> Node -> Node
captureFreeVars fv
| n == 0 = id
| otherwise = mkLambdasB infos . mapFreeVars
captureFreeVars freevars = goBinders freevars . mapFreeVars
where
(indices, infos) = unzip fv
n = length fv
s :: HashMap Index Index
s = HashMap.fromList (zip (reverse indices) [0 ..])
mapFreeVars :: Node -> Node
mapFreeVars = dmapN go
where
s :: HashMap Index Index
s = HashMap.fromList (zip (reverse (map fst freevars)) [0 ..])
go :: Index -> Node -> Node
go k = \case
NVar (Var i u)
| Just v <- s ^. at (u - k) -> NVar (Var i (v + k))
m -> m
-- captures all free variables of a node. It also returns the list of captured
goBinders :: [(Index, Binder)] -> Node -> Node
goBinders fv = case unsnoc fv of
Nothing -> id
Just (fvs, (idx, bin)) -> goBinders fvs . mkLambdaB (mapBinder idx bin)
where
indices = map fst fv
mapBinder :: Index -> Binder -> Binder
mapBinder binderIndex = over binderType (dmapN go)
where
go :: Index -> Node -> Node
go k = \case
NVar u
| u ^. varIndex >= k ->
let uCtx = u ^. varIndex - k + binderIndex + 1
err = error ("impossible: could not find " <> show uCtx <> " in " <> show indices)
u' = length indices - 2 - fromMaybe err (elemIndex uCtx indices) + k
in NVar (set varIndex u' u)
m -> m
-- | Captures all free variables of a node. It also returns the list of captured
-- variables in left-to-right order: if snd is of the form λxλy... then fst is
-- [x, y]
captureFreeVarsCtx :: BinderList Binder -> Node -> ([(Var, Binder)], Node)
@ -120,11 +134,11 @@ captureFreeVarsCtx bl n =
freeVarsCtx' :: BinderList Binder -> Node -> [Var]
freeVarsCtx' bl = map fst . freeVarsCtx bl
-- | the output list does not contain repeated elements and is sorted by *decreasing* variable index.
-- | The output list does not contain repeated elements and is sorted by *decreasing* variable index.
-- The indices are relative to the given binder list
freeVarsCtx :: BinderList Binder -> Node -> [(Var, Binder)]
freeVarsCtx ctx n =
BL.lookupsSortedRev ctx . run . fmap fst . runOutputList $ go (freeVarsSorted n)
freeVarsCtx ctx =
BL.lookupsSortedRev ctx . run . fmap fst . runOutputList . go . freeVarsSorted
where
go ::
-- set of free variables relative to the original ctx
@ -135,9 +149,10 @@ freeVarsCtx ctx n =
Just (v, vs) -> do
output v
let idx = v ^. varIndex
bi = BL.lookup idx ctx
bi :: Binder = BL.lookup idx ctx
fbi = freeVarsSorted (bi ^. binderType)
freevarsbi' :: Set Var
freevarsbi' = Set.mapMonotonic (over varIndex (+ (idx + 1))) (freeVarsSorted (bi ^. binderType))
freevarsbi' = Set.mapMonotonic (over varIndex (+ (idx + 1))) fbi
go (freevarsbi' <> vs)
-- | subst for multiple bindings
@ -157,6 +172,18 @@ substs t = umapN go
subst :: Node -> Node -> Node
subst t = substs [t]
-- | `substDrop args argtys` drops `length args` from `argtys` and substitutes
-- the corresponding variables with `args`. For example:
-- ```
-- substDrop [Nat, Var 3] [Type, Type, Var 1, Var 1] =
-- [Nat, Var 4]
-- ``
substDrop :: [Node] -> [Node] -> [Node]
substDrop args argtys =
reverse $ snd $ foldl' (\(args', acc) ty -> (mkVar' 0 : map (shift 1) args', substs args' ty : acc)) (reverse args, []) (drop k argtys)
where
k = length args
-- | reduce all beta redexes present in a term and the ones created immediately
-- downwards (i.e., a "beta-development")
developBeta :: Node -> Node
@ -167,9 +194,12 @@ developBeta = umap go
NApp (App _ (NLam (Lambda {..})) arg) -> subst arg _lambdaBody
_ -> n
etaExpand :: Int -> Node -> Node
etaExpand 0 n = n
etaExpand k n = mkLambdas' k (mkApps' (shift k n) (map mkVar' (reverse [0 .. k - 1])))
etaExpand :: [Type] -> Node -> Node
etaExpand [] n = n
etaExpand argtys n =
mkLambdas' argtys (mkApps' (shift k n) (map mkVar' (reverse [0 .. k - 1])))
where
k = length argtys
convertClosures :: Node -> Node
convertClosures = umap go
@ -182,6 +212,26 @@ convertClosures = umap go
convertRuntimeNodes :: Node -> Node
convertRuntimeNodes = convertClosures
squashApps :: Node -> Node
squashApps = dmap go
where
go :: Node -> Node
go n =
let (l, args) = unfoldApps' n
in case l of
NCtr (Constr i tag args') -> mkConstr i tag (args' ++ args)
NBlt (BuiltinApp i op args') -> mkBuiltinApp i op (args' ++ args)
NTyp (TypeConstr i sym args') -> mkTypeConstr i sym (args' ++ args)
_ -> n
binderFromArgumentInfo :: ArgumentInfo -> Binder
binderFromArgumentInfo a =
Binder
{ _binderName = a ^. argumentName,
_binderLocation = a ^. argumentLocation,
_binderType = a ^. argumentType
}
argumentInfoFromBinder :: Binder -> ArgumentInfo
argumentInfoFromBinder i =
ArgumentInfo
@ -202,6 +252,22 @@ patternBindersNum = length . (^.. patternBinders)
patternType :: Pattern -> Node
patternType = \case
PatWildcard w -> getInfoType (w ^. patternWildcardInfo)
PatWildcard w -> w ^. patternWildcardType
PatBinder b -> b ^. patternBinder . binderType
PatConstr c -> getInfoType (c ^. patternConstrInfo)
PatConstr c -> c ^. patternConstrType
builtinOpArgTypes :: BuiltinOp -> [Type]
builtinOpArgTypes = \case
OpIntAdd -> [mkTypeInteger', mkTypeInteger']
OpIntSub -> [mkTypeInteger', mkTypeInteger']
OpIntMul -> [mkTypeInteger', mkTypeInteger']
OpIntDiv -> [mkTypeInteger', mkTypeInteger']
OpIntMod -> [mkTypeInteger', mkTypeInteger']
OpIntLt -> [mkTypeInteger', mkTypeInteger']
OpIntLe -> [mkTypeInteger', mkTypeInteger']
OpEq -> [mkDynamic', mkDynamic']
OpShow -> [mkDynamic']
OpStrConcat -> [mkTypeString', mkTypeString']
OpStrToInt -> [mkTypeString']
OpTrace -> [mkDynamic', mkDynamic']
OpFail -> [mkTypeString']

2
src/Juvix/Compiler/Core/Language.hs
View File

@ -43,7 +43,7 @@ type Match = Match' Info Node
type MatchBranch = MatchBranch' Info Node
type PatternWildcard = PatternWildcard' Info
type PatternWildcard = PatternWildcard' Info Node
type PatternBinder = PatternBinder' Info Node

36
src/Juvix/Compiler/Core/Language/Nodes.hs
View File

@ -104,6 +104,8 @@ data LetItem' a ty = LetItem
-- body and in the values `length _letRecValues` implicit binders are introduced
-- which hold the functions/values being defined.
-- the last item in _letRecValues will have have index $0 in the body.
-- The values are *not* in scope of the binders. I.e.
-- the binders of the values cannot refer to the values
data LetRec' i a ty = LetRec
{ _letRecInfo :: i,
_letRecValues :: !(NonEmpty (LetItem' a ty)),
@ -131,9 +133,19 @@ data CaseBranch' i a ty = CaseBranch
_caseBranchBody :: !a
}
-- | A special form of `Case` for the booleans. Used only in Core.Stripped.
data If' i a = If
{ _ifInfo :: i,
_ifValue :: !a,
_ifTrue :: !a,
_ifFalse :: !a
}
-- | Complex pattern match. `Match` is lazy: only the selected branch is evaluated.
data Match' i a = Match
{ _matchInfo :: i,
_matchValueTypes :: !(NonEmpty a),
_matchReturnType :: !a,
_matchValues :: !(NonEmpty a),
_matchBranches :: ![MatchBranch' i a]
}
@ -151,12 +163,13 @@ data MatchBranch' i a = MatchBranch
}
data Pattern' i a
= PatWildcard (PatternWildcard' i)
= PatWildcard (PatternWildcard' i a)
| PatBinder (PatternBinder' i a)
| PatConstr (PatternConstr' i a)
newtype PatternWildcard' i = PatternWildcard
{ _patternWildcardInfo :: i
data PatternWildcard' i a = PatternWildcard
{ _patternWildcardInfo :: i,
_patternWildcardType :: a
}
data PatternBinder' i a = PatternBinder
@ -167,7 +180,8 @@ data PatternBinder' i a = PatternBinder
data PatternConstr' i a = PatternConstr
{ _patternConstrInfo :: i,
_patternConstrTag :: !Tag,
_patternConstrArgs :: ![Pattern' i a]
_patternConstrArgs :: ![Pattern' i a],
_patternConstrType :: a
}
-- | Useful for unfolding Pi
@ -251,10 +265,13 @@ instance HasAtomicity (LetRec' i a ty) where
instance HasAtomicity (Case' i bi a ty) where
atomicity _ = Aggregate lambdaFixity
instance HasAtomicity (If' i a) where
atomicity _ = Aggregate lambdaFixity
instance HasAtomicity (Match' i a) where
atomicity _ = Aggregate lambdaFixity
instance HasAtomicity (PatternWildcard' i) where
instance HasAtomicity (PatternWildcard' i a) where
atomicity _ = Atom
instance HasAtomicity (PatternBinder' i a) where
@ -341,15 +358,18 @@ instance (Eq a) => Eq (Constr' i 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 (If' i a) where
(If _ v1 b1 c1) == (If _ v2 b2 c2) = v1 == v2 && b1 == b2 && c1 == c2
instance (Eq a) => Eq (CaseBranch' i a ty) where
(==) =
eqOn (^. caseBranchTag)
..&&.. eqOn (^. caseBranchBody)
instance (Eq a) => Eq (Match' i a) where
(Match _ vs1 bs1) == (Match _ vs2 bs2) = vs1 == vs2 && bs1 == bs2
(Match _ _ _ vs1 bs1) == (Match _ _ _ vs2 bs2) = vs1 == vs2 && bs1 == bs2
instance Eq (PatternWildcard' i) where
instance Eq (PatternWildcard' i a) where
_ == _ = True
instance Eq (Univ' i) where
@ -397,7 +417,7 @@ instance (Eq a) => Eq (MatchBranch' i a) where
(MatchBranch _ pats1 b1) == (MatchBranch _ pats2 b2) = pats1 == pats2 && b1 == b2
instance (Eq a) => Eq (PatternConstr' i a) where
(PatternConstr _ tag1 ps1) == (PatternConstr _ tag2 ps2) = tag1 == tag2 && ps1 == ps2
(PatternConstr _ tag1 ps1 _) == (PatternConstr _ tag2 ps2 _) = tag1 == tag2 && ps1 == ps2
instance Hashable (Ident' i) where
hashWithSalt s = hashWithSalt s . (^. identSymbol)

4
src/Juvix/Compiler/Core/Language/Stripped.hs
View File

@ -64,6 +64,8 @@ type Let = Let' () Node Type
type Case = Case' () CaseBranchInfo Node Type
type If = If' () Node
type CaseBranch = CaseBranch' CaseBranchInfo Node Type
{---------------------------------------------------------------------------------}
@ -77,6 +79,7 @@ data Node
| NCtr Constr
| NLet Let
| NCase Case
| NIf If
deriving stock (Eq)
instance HasAtomicity Node where
@ -89,6 +92,7 @@ instance HasAtomicity Node where
NCtr x -> atomicity x
NLet x -> atomicity x
NCase x -> atomicity x
NIf x -> atomicity x
makeLenses ''VarInfo
makeLenses ''IdentInfo

9
src/Juvix/Compiler/Core/Pipeline.hs
View File

@ -7,24 +7,15 @@ where
import Juvix.Compiler.Core.Data.InfoTable
import Juvix.Compiler.Core.Transformation
toEvalTransformations :: [TransformationId]
toEvalTransformations = [MatchToCase, NatToInt, ConvertBuiltinTypes]
-- | Perform transformations on Core necessary for efficient evaluation
toEval :: InfoTable -> InfoTable
toEval = applyTransformations toEvalTransformations
toStrippedTransformations :: [TransformationId]
toStrippedTransformations = toEvalTransformations ++ [LambdaLetRecLifting, MoveApps, TopEtaExpand, RemoveTypeArgs]
-- | Perform transformations on Core necessary before the translation to
-- Core.Stripped
toStripped :: InfoTable -> InfoTable
toStripped = applyTransformations toStrippedTransformations
toGebTransformations :: [TransformationId]
toGebTransformations = toEvalTransformations ++ [UnrollRecursion, ComputeTypeInfo]
-- | Perform transformations on Core necessary before the translation to GEB
toGeb :: InfoTable -> InfoTable
toGeb = applyTransformations toGebTransformations

105
src/Juvix/Compiler/Core/Pretty/Base.hs
View File

@ -146,6 +146,22 @@ instance (PrettyCode a) => PrettyCode (Binder' a) where
ty' <- ppCode ty
return (parens (pretty name' <+> kwColon <+> ty'))
ppWithType :: Member (Reader Options) r => Doc Ann -> Type -> Sem r (Doc Ann)
ppWithType d = \case
NDyn {} ->
return d
ty -> do
ty' <- ppCode ty
return $ parens (d <+> kwColon <+> ty')
ppTypeAnnot :: Member (Reader Options) r => Type -> Sem r (Doc Ann)
ppTypeAnnot = \case
NDyn {} ->
return mempty
ty -> do
ty' <- ppCode ty
return $ mempty <+> kwColon <+> parens ty'
ppCodeLet' :: (PrettyCode a, Member (Reader Options) r) => Text -> Maybe (Doc Ann) -> Let' i a ty -> Sem r (Doc Ann)
ppCodeLet' name mty lt = do
n' <- ppName KNameConstructor name
@ -186,6 +202,13 @@ ppCodeCase' branchBinderNames branchTagNames Case {..} =
let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs''
return $ kwCase <+> v <+> kwOf <+> bss
instance PrettyCode a => PrettyCode (If' i a) where
ppCode If {..} = do
v <- ppCode _ifValue
l <- ppCode _ifTrue
r <- ppCode _ifFalse
return $ kwIf <+> v <+> kwThen <+> l <+> kwElse <+> r
instance PrettyCode PatternWildcard where
ppCode _ = return kwWildcard
@ -193,10 +216,11 @@ instance PrettyCode PatternBinder where
ppCode PatternBinder {..} = do
n <- ppName KNameLocal (_patternBinder ^. binderName)
case _patternBinderPattern of
PatWildcard {} -> return n
PatWildcard {} -> do
ppWithType n (_patternBinder ^. binderType)
_ -> do
pat <- ppRightExpression appFixity _patternBinderPattern
return $ n <> kwAt <> pat
ppWithType (n <> kwAt <> pat) (_patternBinder ^. binderType)
instance PrettyCode PatternConstr where
ppCode PatternConstr {..} = do
@ -230,17 +254,25 @@ instance PrettyCode Let where
instance PrettyCode LetRec where
ppCode :: forall r. (Member (Reader Options) r) => LetRec -> Sem r (Doc Ann)
ppCode LetRec {..} = do
let tys = fmap (^. letItemBinder . binderType) _letRecValues
names <- mapM (getName . (^. letItemBinder)) _letRecValues
types <- mapM ppCode tys
vs <- mapM (ppCode . (^. letItemValue)) _letRecValues
b' <- ppCode _letRecBody
return $ case names of
hns :| [] -> kwLetRec <+> hns <+> kwAssign <+> head vs <+> kwIn <+> b'
let bs =
zipWith3Exact
(\n ty ty' -> if isDynamic ty' then n else n <+> colon <+> ty)
(toList names)
(toList types)
(toList tys)
return $ case bs of
[hbs] -> kwLetRec <+> hbs <+> kwAssign <+> head vs <+> kwIn <+> b'
_ ->
let bss =
indent' $
align $
concatWith (\a b -> a <> kwSemicolon <> line <> b) $
zipWithExact (\name val -> name <+> kwAssign <+> val) (toList names) (toList vs)
zipWithExact (\b val -> b <+> kwAssign <+> val) (toList bs) (toList vs)
nss = enclose kwSquareL kwSquareR (concatWith (<+>) names)
in kwLetRec <> nss <> line <> bss <> line <> kwIn <> line <> b'
where
@ -283,23 +315,13 @@ instance PrettyCode Node where
branchBodies = map (^. matchBranchBody) _matchBranches
pats <- mapM ppPatterns branchPatterns
vs <- mapM ppCode _matchValues
vs' <- zipWithM ppWithType (toList vs) (toList _matchValueTypes)
bs <- sequence $ zipWithExact (\ps br -> ppCode br >>= \br' -> return $ ps <+> kwMapsto <+> br') pats branchBodies
let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs
return $ kwMatch <+> hsep (punctuate comma (toList vs)) <+> kwWith <+> bss
NPi Pi {..} ->
let piType = _piBinder ^. binderType
in case _piBinder ^. binderName of
"?" -> do
ty <- ppLeftExpression funFixity piType
b <- ppRightExpression funFixity _piBody
return $ ty <+> kwArrow <+> b
name -> do
n <- ppName KNameLocal name
ty <- ppCode piType
b <- ppCode _piBody
return $ kwPi <+> n <+> kwColon <+> ty <> comma <+> b
NUniv Univ {..} ->
return $ kwType <+> pretty _univLevel
rty <- ppTypeAnnot _matchReturnType
return $ kwMatch <+> hsep (punctuate comma vs') <+> kwWith <> rty <+> bss
NPi p -> ppCode p
NUniv u -> ppCode u
NPrim TypePrim {..} -> ppCode _typePrimPrimitive
NTyp TypeConstr {..} -> do
args' <- mapM (ppRightExpression appFixity) _typeConstrArgs
@ -309,6 +331,27 @@ instance PrettyCode Node where
Closure env l@Lambda {} ->
ppCode (substEnv env (NLam l))
instance PrettyCode Pi where
ppCode Pi {..} =
let piType = _piBinder ^. binderType
in case _piBinder ^. binderName of
"?" -> do
ty <- ppLeftExpression funFixity piType
b <- ppRightExpression funFixity _piBody
return $ ty <+> kwArrow <+> b
name -> do
n <- ppName KNameLocal name
ty <- ppCode piType
b <- ppCode _piBody
return $ kwPi <+> n <+> kwColon <+> ty <> comma <+> b
instance PrettyCode (Univ' i) where
ppCode Univ {..} =
return $
if
| _univLevel == 0 -> kwType
| otherwise -> kwType <+> pretty _univLevel
instance PrettyCode Stripped.TypeApp where
ppCode Stripped.TypeApp {..} = do
args' <- mapM (ppRightExpression appFixity) _typeAppArgs
@ -350,6 +393,7 @@ instance PrettyCode Stripped.Node where
let branchBinderNames = map (map (^. binderName) . (^. caseBranchBinders)) _caseBranches
branchTagNames = map (^. (caseBranchInfo . Stripped.caseBranchInfoConstrName)) _caseBranches
in ppCodeCase' branchBinderNames branchTagNames x
Stripped.NIf x -> ppCode x
instance PrettyCode ConstructorInfo where
ppCode :: (Member (Reader Options) r) => ConstructorInfo -> Sem r (Doc Ann)
@ -400,11 +444,19 @@ instance PrettyCode Stripped.ArgumentInfo where
ty <- ppCode _argumentType
return $ name <+> colon <+> ty
instance PrettyCode Stripped.ConstructorInfo where
ppCode :: (Member (Reader Options) r) => Stripped.ConstructorInfo -> Sem r (Doc Ann)
ppCode ci = do
name <- ppName KNameConstructor (ci ^. Stripped.constructorName)
ty <- ppCode (ci ^. Stripped.constructorType)
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
inds' <- ppInductives (HashMap.elems (tbl ^. Stripped.infoInductives))
ctx' <- ppFunctions (tbl ^. Stripped.infoFunctions)
return ("-- Functions" <> line <> ctx' <> line)
return ("-- Types" <> line <> inds' <> line <> "-- Functions" <> line <> ctx' <> line)
where
ppFunctions :: HashMap Symbol Stripped.FunctionInfo -> Sem r (Doc Ann)
ppFunctions ctx = do
@ -418,6 +470,17 @@ instance PrettyCode Stripped.InfoTable where
body' <- ppCode (fi ^. Stripped.functionBody)
return (kwDef <+> sym' <> encloseSep lparen rparen ", " args <+> kwAssign <+> body')
ppInductives :: [Stripped.InductiveInfo] -> Sem r (Doc Ann)
ppInductives inds = do
inds' <- mapM ppInductive inds
return (vsep inds')
where
ppInductive :: Stripped.InductiveInfo -> Sem r (Doc Ann)
ppInductive ii = do
name <- ppName KNameInductive (ii ^. Stripped.inductiveName)
ctrs <- mapM (fmap (<> semi) . ppCode) (ii ^. Stripped.inductiveConstructors)
return (kwInductive <+> name <+> braces (line <> indent' (vsep ctrs) <> line))
instance (PrettyCode a) => PrettyCode (NonEmpty a) where
ppCode x = ppCode (toList x)

1
src/Juvix/Compiler/Core/Transformation.hs
View File

@ -38,3 +38,4 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
ComputeTypeInfo -> computeTypeInfo
UnrollRecursion -> unrollRecursion
MatchToCase -> matchToCase
EtaExpandApps -> etaExpansionApps

29
src/Juvix/Compiler/Core/Transformation/Base.hs
View File

@ -35,3 +35,32 @@ mapT' f tab =
walkT :: (Applicative f) => (Symbol -> Node -> f ()) -> InfoTable -> f ()
walkT f tab = for_ (HashMap.toList (tab ^. identContext)) (uncurry f)
mapAllNodes :: (Node -> Node) -> InfoTable -> InfoTable
mapAllNodes f tab =
mapAxioms convertAxiom $
mapInductives convertInductive $
mapConstructors convertConstructor $
mapIdents convertIdent $
mapT (const f) tab
where
convertIdent :: IdentifierInfo -> IdentifierInfo
convertIdent ii =
ii
{ _identifierType = f (ii ^. identifierType),
_identifierArgsInfo = map (over argumentType f) (ii ^. identifierArgsInfo)
}
convertConstructor :: ConstructorInfo -> ConstructorInfo
convertConstructor = over constructorType f
convertInductive :: InductiveInfo -> InductiveInfo
convertInductive ii =
ii
{ _inductiveKind = f (ii ^. inductiveKind),
_inductiveParams = map (over paramKind f) (ii ^. inductiveParams),
_inductiveConstructors = map convertConstructor (ii ^. inductiveConstructors)
}
convertAxiom :: AxiomInfo -> AxiomInfo
convertAxiom = over axiomType f

2
src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
View File

@ -61,7 +61,7 @@ computeNodeTypeInfo tab = umapL go
let ci = fromJust $ HashMap.lookup _constrTag (tab ^. infoConstructors)
ii = fromJust $ HashMap.lookup (ci ^. constructorInductive) (tab ^. infoInductives)
in case ii ^. inductiveBuiltin of
Just BuiltinBool ->
Just (BuiltinTypeInductive BuiltinBool) ->
mkTypeBool'
_ ->
mkTypeConstr' (ci ^. constructorInductive) (take (length (ii ^. inductiveParams)) _constrArgs)

31
src/Juvix/Compiler/Core/Transformation/ConvertBuiltinTypes.hs
View File

@ -14,37 +14,14 @@ convertNode tab = umap go
go node = case node of
NTyp TypeConstr {..} ->
case ii ^. inductiveBuiltin of
Just BuiltinBool -> mkTypeBool'
Just (BuiltinTypeInductive BuiltinBool) -> mkTypeBool'
Just (BuiltinTypeInductive BuiltinNat) -> mkTypeInteger'
Just (BuiltinTypeAxiom BuiltinString) -> mkTypeString'
_ -> 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
mapAllNodes (convertNode tab) tab

56
src/Juvix/Compiler/Core/Transformation/Eta.hs
View File

@ -15,64 +15,52 @@ etaExpandBuiltins = umap go
go n = case n of
NBlt BuiltinApp {..}
| builtinOpArgsNum _builtinAppOp > length _builtinAppArgs ->
etaExpand (builtinOpArgsNum _builtinAppOp - length _builtinAppArgs) n
etaExpand (substDrop _builtinAppArgs (builtinOpArgTypes _builtinAppOp)) n
_ -> n
etaExpandConstrs :: (Tag -> Int) -> Node -> Node
etaExpandConstrs argsNum = umap go
etaExpandConstrs :: (Tag -> [Type]) -> Node -> Node
etaExpandConstrs getArgtys = umap go
where
go :: Node -> Node
go n = case n of
NCtr Constr {..}
| k > length _constrArgs ->
etaExpand (k - length _constrArgs) n
| length argtys > length _constrArgs ->
etaExpand (substDrop _constrArgs argtys) n
where
k = argsNum _constrTag
argtys = getArgtys _constrTag
_ -> n
etaExpandTypeConstrs :: (Symbol -> Int) -> Node -> Node
etaExpandTypeConstrs argsNum = umap go
etaExpandTypeConstrs :: (Symbol -> [Type]) -> Node -> Node
etaExpandTypeConstrs getArgtys = umap go
where
go :: Node -> Node
go n = case n of
NTyp TypeConstr {..}
| k > length _typeConstrArgs ->
etaExpand (k - length _typeConstrArgs) n
| length argtys > length _typeConstrArgs ->
etaExpand (substDrop _typeConstrArgs argtys) n
where
k = argsNum _typeConstrSymbol
argtys = getArgtys _typeConstrSymbol
_ -> n
squashApps :: Node -> Node
squashApps = dmap go
where
go :: Node -> Node
go n =
let (l, args) = unfoldApps' n
in case l of
NCtr (Constr i tag args') -> mkConstr i tag (args' ++ args)
NBlt (BuiltinApp i op args') -> mkBuiltinApp i op (args' ++ args)
NTyp (TypeConstr i sym args') -> mkTypeConstr i sym (args' ++ args)
_ -> n
etaExpandApps :: InfoTable -> Node -> Node
etaExpandApps tab =
squashApps
. etaExpandTypeConstrs typeConstrArgsNum
. etaExpandConstrs constrArgsNum
. etaExpandTypeConstrs typeConstrArgtys
. etaExpandConstrs constrArgtys
. etaExpandBuiltins
. squashApps
where
constrArgsNum :: Tag -> Int
constrArgsNum tag =
constrArgtys :: Tag -> [Type]
constrArgtys tag =
case HashMap.lookup tag (tab ^. infoConstructors) of
Just ci -> ci ^. constructorArgsNum
Nothing -> 0
Just ci -> typeArgs (ci ^. constructorType)
Nothing -> []
typeConstrArgsNum :: Symbol -> Int
typeConstrArgsNum sym =
typeConstrArgtys :: Symbol -> [Type]
typeConstrArgtys sym =
case HashMap.lookup sym (tab ^. infoInductives) of
Just ci -> length (ci ^. inductiveParams)
Nothing -> 0
Just ci -> map (^. paramKind) (ci ^. inductiveParams)
Nothing -> []
etaExpansionApps :: InfoTable -> InfoTable
etaExpansionApps tab = mapT (const (etaExpandApps tab)) tab
etaExpansionApps tab = mapAllNodes (etaExpandApps tab) tab

20
src/Juvix/Compiler/Core/Transformation/LambdaLetRecLifting.hs
View File

@ -25,7 +25,7 @@ lambdaLiftNode aboveBl top =
typeFromArgs :: [ArgumentInfo] -> Type
typeFromArgs = \case
[] -> mkDynamic' -- change this when we have type info about the body
(a : as) -> mkPi' (a ^. argumentType) (typeFromArgs as)
(a : as) -> mkPi mempty (binderFromArgumentInfo a) (typeFromArgs as)
goTop :: BinderList Binder -> Node -> [LambdaLhs] -> Sem r Node
goTop bl body = \case
@ -77,20 +77,21 @@ lambdaLiftNode aboveBl top =
goLetRec :: LetRec -> Sem r Recur
goLetRec letr = do
let defs :: [Node]
defs = toList (letr ^.. letRecValues . each . letItemValue)
defs = letr ^.. letRecValues . each . letItemValue
ndefs :: Int
ndefs = length defs
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 letRecBinders' bl
binders :: [Binder]
binders = letr ^.. letRecValues . each . letItemBinder
letRecBinders' :: [Binder] <- mapM (lambdaLiftBinder bl) binders
topSyms :: [Symbol] <- forM defs (const freshSymbol)
let bl' :: BinderList Binder
bl' = BL.prependRev letRecBinders' bl
let topNames :: [Text]
topNames :: [Text]
topNames = zipWithExact uniqueName (map (^. binderName) letRecBinders') topSyms
topSymsWithName = zipExact topSyms topNames
let recItemsFreeVars :: [(Var, Binder)]
recItemsFreeVars :: [(Var, Binder)]
recItemsFreeVars = mapMaybe helper (concatMap (freeVarsCtx' bl') defs)
where
helper :: Var -> Maybe (Var, Binder)
@ -151,8 +152,7 @@ lambdaLiftNode aboveBl top =
| otherwise -> impossible
(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
bnd' = over binderType (shift k . subsCalls) bnd
let res :: Node
res = shiftHelper body' (nonEmpty' (zipExact letItems letRecBinders'))
return (Recur res)

124
src/Juvix/Compiler/Core/Transformation/MatchToCase.hs
View File

@ -4,7 +4,6 @@ import Juvix.Compiler.Core.Data.InfoTableBuilder
import Juvix.Compiler.Core.Extra
import Juvix.Compiler.Core.Info.LocationInfo
import Juvix.Compiler.Core.Info.NameInfo (setInfoName)
import Juvix.Compiler.Core.Info.TypeInfo
import Juvix.Compiler.Core.Language
import Juvix.Compiler.Core.Transformation.Base
import Juvix.Compiler.Core.Transformation.MatchToCase.Data
@ -12,14 +11,20 @@ import Juvix.Compiler.Core.Transformation.MatchToCase.Data
matchToCase :: InfoTable -> InfoTable
matchToCase = run . mapT' (const (umapM matchToCaseNode))
mkShiftedPis' :: [Type] -> Type -> Type
mkShiftedPis' lhs rhs = foldl' go (shift (length lhs) rhs) (reverse (indexFrom 0 lhs))
where
go :: Type -> Indexed Type -> Type
go t (Indexed i a) = mkPi' (shift i a) t
matchToCaseNode :: forall r. Member InfoTableBuilder r => Node -> Sem r Node
matchToCaseNode n = case n of
NMatch m -> do
let branches = m ^. matchBranches
values = toList (m ^. matchValues)
matchType = getInfoType (m ^. matchInfo)
valueTypes = (getInfoType . getInfo <$> values)
branchType = mkPis' valueTypes matchType
matchType = m ^. matchReturnType
valueTypes = toList (m ^. matchValueTypes)
branchType = mkShiftedPis' valueTypes matchType
-- Index from 1 because we prepend the fail branch.
branchNodes <-
@ -28,10 +33,12 @@ matchToCaseNode n = case n of
-- The appNode calls the first branch with the values of the match
let appNode = mkApps' (mkVar' 0) (shift (length branchNodes) <$> values)
return (foldr (mkLetTy mempty branchType) appNode branchNodes)
let branchBinder = typeToBinder branchType
let branchBinders = map (branchBinder,) branchNodes
return (mkShiftedBinderLets 0 branchBinders appNode)
_ -> return n
-- | increase all free variable indices by a given value.
-- | Increase all free variable indices by a given value.
-- In this function we consider indices to be embedded at a specified level
shiftEmbedded :: Level -> Index -> Node -> Node
shiftEmbedded _ 0 = id
@ -110,35 +117,71 @@ shiftEmbedded wrappingLevel m = umapN go
-- branch.
compileMatchBranch :: forall r. Members '[InfoTableBuilder] r => Indexed MatchBranch -> Sem r Node
compileMatchBranch (Indexed branchNum br) = do
compiledBranch <- runReader initState' (combineCompiledPatterns (map (compilePattern patternsNum) patterns))
return (mkLambdasTy (patternType <$> patterns) ((compiledBranch ^. compiledPatMkNode) (wrapBody (compiledBranch ^. compiledPatBinders))))
compiledBranch <- runReader initState (combineCompiledPatterns (map (compilePattern 0 branchNum patternsNum) patterns))
return (mkShiftedLambdas branchNum shiftedPatternTypes ((compiledBranch ^. compiledPatMkNode) (wrapBody (compiledBranch ^. compiledPatBinders))))
where
patterns :: [Pattern]
patterns = toList (br ^. matchBranchPatterns)
patternsNum :: Int
patternsNum = length patterns
patternBindersNumList :: [Int]
patternBindersNumList = map (length . getPatternBinders) patterns
accumPatternBindersNum :: [Int]
accumPatternBindersNum = init (scanl (+) 0 patternBindersNumList)
shiftedPatternTypes :: [Type]
shiftedPatternTypes = [shift (-n) b | (n, b) <- zipExact accumPatternBindersNum (map patternType patterns)]
wrapBody :: [CompiledBinder] -> Node
wrapBody binders = foldr (uncurry (mkLet mempty)) shiftedBody vars
where
vars :: [(Binder, Node)]
vars = second mkVar' . swap . toTuple <$> extractOriginalBinders binders
vars = (bimap (shiftBinder patternBindersNum') mkVar' . swap . toTuple) <$> extractOriginalBinders binders
auxiliaryBindersNum :: Int
auxiliaryBindersNum = length (filter isAuxiliaryBinder binders)
patternBindersNum' :: Int
patternBindersNum' = sum patternBindersNumList
shiftedBody :: Node
shiftedBody =
let patternBindersNum' = length (concatMap getPatternBinders patterns)
auxiliaryBindersNum = length (filter isAuxiliaryBinder binders)
in shiftEmbedded
patternBindersNum'
(auxiliaryBindersNum + patternBindersNum' + patternsNum + branchNum)
(br ^. matchBranchBody)
shiftEmbedded
patternBindersNum'
(auxiliaryBindersNum + patternBindersNum' + patternsNum + branchNum)
(br ^. matchBranchBody)
initState' :: CompileState
initState' =
CompileState
{ _compileStateBindersAbove = 0,
_compileStateCompiledPattern = mempty
}
-- | Increase the indices of free variables in the binderTyped by a given value
shiftBinder :: Index -> Binder -> Binder
shiftBinder idx = over binderType (shift idx)
-- | Make a sequence of nested lets from a list of binders / value pairs. The
-- indices of free variables in binder types are shifted by the sum of
-- `baseShift` and the number of lets that have already been added in the
-- sequence.
mkShiftedBinderLets :: Index -> [(Binder, Node)] -> Node -> Node
mkShiftedBinderLets baseShift vars body = foldr f body (indexFrom 0 vars)
where
f :: Indexed (Binder, Node) -> Node -> Node
f (Indexed idx (b, v)) = mkLet mempty (shiftBinder (baseShift + idx) b) v
mkShiftedLambdas :: Index -> [Type] -> Node -> Node
mkShiftedLambdas baseShift tys body = foldr f body (indexFrom 0 tys)
where
f :: Indexed Type -> Node -> Node
f (Indexed idx ty) = mkLambda' (shift (baseShift + idx) ty)
-- | Wrap a type node in an unnamed binder.
typeToBinder :: Type -> Binder
typeToBinder ty =
Binder
{ _binderName = "?",
_binderLocation = Nothing,
_binderType = ty
}
-- | Extract original binders (i.e binders which are referenced in the match
-- branch body) from a list of `CompiledBinder`s indexed by the total number
@ -187,13 +230,14 @@ combineCompiledPatterns ps = go indexedPatterns
-- (wildcard, binder or constructor) introduces an auxiliary binder.
-- The arguments are then compiled recursively using a new CompileState context.
-- The default case points to the next branch pattern.
compilePattern :: forall r. Members [Reader CompileState, Reader CompileStateNode, InfoTableBuilder] r => Int -> Pattern -> Sem r CompiledPattern
compilePattern numPatterns = \case
compilePattern :: forall r. Members [Reader CompileState, Reader CompileStateNode, InfoTableBuilder] r => Int -> Int -> Int -> Pattern -> Sem r CompiledPattern
compilePattern baseShift branchNum numPatterns = \case
PatWildcard {} -> return (CompiledPattern [] id)
PatBinder b -> do
subPats <- resetCurrentNode (incBindersAbove (compilePattern numPatterns (b ^. patternBinderPattern)))
subPats <- resetCurrentNode (incBindersAbove (compilePattern baseShift branchNum numPatterns (b ^. patternBinderPattern)))
auxPatternsNum <- length . filter isAuxiliaryBinder <$> asks (^. compileStateCompiledPattern . compiledPatBinders)
currentNode <- asks (^. compileStateNodeCurrent)
let newBinder = b ^. patternBinder
let newBinder = shiftBinder (baseShift + branchNum + numPatterns + auxPatternsNum) (b ^. patternBinder)
let compiledBinder =
CompiledPattern
{ _compiledPatBinders = [OriginalBinder newBinder],
@ -208,41 +252,31 @@ compilePattern numPatterns = \case
where
compileCase :: [Pattern] -> Sem r CompiledPattern
compileCase args = do
binders <- mapM mkBinder args
binders <- mapM mkBinder'' args
CompiledPattern <$> mapM mkCompiledBinder args <*> mkCaseFromBinders binders
compileArgs :: [Pattern] -> Sem r CompiledPattern
compileArgs args = do
bindersAbove <- asks (^. compileStateBindersAbove)
let ctorArgsPatterns = compilePattern numPatterns <$> args
state = mkState bindersAbove
runReader state (combineCompiledPatterns ctorArgsPatterns)
where
mkState :: Int -> CompileState
mkState bindersAbove =
( CompileState
{ _compileStateBindersAbove = bindersAbove + length args,
_compileStateCompiledPattern = mempty
}
)
let ctorArgsPatterns = compilePattern (length args) branchNum numPatterns <$> args
addBindersAbove (length args) (resetCompiledPattern (combineCompiledPatterns ctorArgsPatterns))
mkCompiledBinder :: Pattern -> Sem r CompiledBinder
mkCompiledBinder p = AuxiliaryBinder <$> mkBinder p
mkCompiledBinder p = AuxiliaryBinder <$> mkBinder'' p
mkBinder :: Pattern -> Sem r Binder
mkBinder = \case
mkBinder'' :: Pattern -> Sem r Binder
mkBinder'' = \case
PatBinder b -> return (b ^. patternBinder)
PatWildcard w -> do
let info = w ^. patternWildcardInfo
return
Binder
{ _binderName = "_",
{ _binderName = "?",
_binderLocation = getInfoLocation info,
_binderType = getInfoType info
_binderType = mkDynamic'
}
PatConstr c' -> do
let info = c' ^. patternConstrInfo
mkUniqueBinder "arg" (getInfoLocation info) (getInfoType info)
mkUniqueBinder "arg" (getInfoLocation info) mkDynamic'
mkCaseFromBinders :: [Binder] -> Sem r (Node -> Node)
mkCaseFromBinders binders = do
@ -277,7 +311,7 @@ compilePattern numPatterns = \case
)
failNode :: [Type] -> Node
failNode tys = mkLambdasTy tys (mkBuiltinApp' OpFail [mkConstant' (ConstString "Non-exhaustive patterns")])
failNode tys = mkShiftedLambdas 0 tys (mkBuiltinApp' OpFail [mkConstant' (ConstString "Non-exhaustive patterns")])
mkUniqueBinder' :: Member InfoTableBuilder r => Text -> Node -> Sem r Binder
mkUniqueBinder' name ty = mkUniqueBinder name Nothing ty

32
src/Juvix/Compiler/Core/Transformation/MatchToCase/Data.hs
View File

@ -46,26 +46,18 @@ data CompileState = CompileState
newtype CompileStateNode = CompileStateNode
{_compileStateNodeCurrent :: Node}
initState :: CompileState
initState =
CompileState
{ _compileStateBindersAbove = 0,
_compileStateCompiledPattern =
CompiledPattern
{ _compiledPatBinders = [],
_compiledPatMkNode = id
}
}
stateWithBindersAbove :: Int -> CompileState
stateWithBindersAbove n = initState {_compileStateBindersAbove = n}
makeLenses ''CompiledPattern
makeLenses ''CompileState
makeLenses ''CompileStateNode
addBindersAbove :: Member (Reader CompileState) r => Int -> Sem r CompiledPattern -> Sem r CompiledPattern
addBindersAbove bindersNum = local (over compileStateBindersAbove (+ bindersNum))
incBindersAbove :: Member (Reader CompileState) r => Sem r CompiledPattern -> Sem r CompiledPattern
incBindersAbove = local (over compileStateBindersAbove (+ 1))
incBindersAbove = addBindersAbove 1
resetCompiledPattern :: Member (Reader CompileState) r => Sem r CompiledPattern -> Sem r CompiledPattern
resetCompiledPattern = local (set compileStateCompiledPattern mempty)
resetCurrentNode :: Member (Reader CompileStateNode) r => Sem r CompiledPattern -> Sem r CompiledPattern
resetCurrentNode = local (set compileStateNodeCurrent (mkVar' 0))
@ -83,3 +75,13 @@ instance Monoid CompiledPattern where
{ _compiledPatBinders = [],
_compiledPatMkNode = id
}
initState :: CompileState
initState =
CompileState
{ _compileStateBindersAbove = 0,
_compileStateCompiledPattern = mempty
}
stateWithBindersAbove :: Int -> CompileState
stateWithBindersAbove n = initState {_compileStateBindersAbove = n}

25
src/Juvix/Compiler/Core/Transformation/NatToInt.hs
View File

@ -24,15 +24,28 @@ convertNode tab = convert [] 0
NApp (App _ (NApp (App _ (NIdt (Ident {..})) l)) r) ->
Recur' (levels, convertIdentApp node (\g -> g _identInfo l r) _identSymbol)
NApp (App _ (NIdt (Ident {..})) l) ->
Recur' (levels, convertIdentApp node (\g -> mkLet' l $ mkLambdaTy mkTypeInteger' $ g _identInfo (mkVar' 1) (mkVar' 0)) _identSymbol)
Recur'
( levels,
convertIdentApp
node
( \g ->
mkLet' mkTypeInteger' l $
mkLambda' mkTypeInteger' $
g _identInfo (mkVar' 1) (mkVar' 0)
)
_identSymbol
)
NIdt (Ident {..})
| Just _identSymbol == tab ^. infoIntToNat ->
End' (mkLambda' mkTypeInteger' (mkVar' 0))
NIdt (Ident {..}) ->
Recur'
( levels,
convertIdentApp
node
( \g ->
mkLambdaTy mkTypeInteger' $
mkLambdaTy mkTypeInteger' $
mkLambda' mkTypeInteger' $
mkLambda' mkTypeInteger' $
g _identInfo (mkVar' 1) (mkVar' 0)
)
_identSymbol
@ -48,7 +61,7 @@ convertNode tab = convert [] 0
NCase (Case {..}) ->
let ii = fromJust $ HashMap.lookup _caseInductive (tab ^. infoInductives)
in case ii ^. inductiveBuiltin of
Just BuiltinNat ->
Just (BuiltinTypeInductive BuiltinNat) ->
case _caseBranches of
[br] -> makeIf br (maybeBranch _caseDefault)
[br1, br2] ->
@ -94,7 +107,7 @@ convertNode tab = convert [] 0
Just BuiltinNatSub ->
f
( \info x y ->
mkLet' (mkBuiltinApp info OpIntSub [x, y]) $
mkLet' mkTypeInteger' (mkBuiltinApp info OpIntSub [x, y]) $
mkIf'
boolSymbol
(mkBuiltinApp' OpIntLe [mkConstant' (ConstInteger 0), mkVar' 0])
@ -123,6 +136,6 @@ natToInt tab = mapT (const (convertNode tab')) tab'
tab' =
case tab ^. infoIntToNat of
Just sym ->
tab {_identContext = HashMap.insert sym (mkLambda' (mkVar' 0)) (tab ^. identContext)}
tab {_identContext = HashMap.insert sym (mkLambda' mkTypeInteger' (mkVar' 0)) (tab ^. identContext)}
Nothing ->
tab

58
src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs
View File

@ -7,13 +7,22 @@ where
import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Core.Data.BinderList qualified as BL
import Juvix.Compiler.Core.Extra
import Juvix.Compiler.Core.Pretty
import Juvix.Compiler.Core.Transformation.Base
isTypeConstr :: InfoTable -> Type -> Bool
isTypeConstr tab ty = case typeTarget ty of
NUniv {} ->
True
NIdt Ident {..} ->
isTypeConstr tab (fromJust $ HashMap.lookup _identSymbol (tab ^. identContext))
_ -> False
convertNode :: InfoTable -> Node -> Node
convertNode tab = convert mempty
where
unsupported :: forall a. a
unsupported = error "remove type arguments: unsupported node"
unsupported :: forall a. Node -> a
unsupported node = error ("remove type arguments: unsupported node\n\t" <> ppTrace node)
convert :: BinderList Binder -> Node -> Node
convert vars = dmapLR' (vars, go)
@ -23,11 +32,18 @@ convertNode tab = convert mempty
NVar v@(Var {..}) ->
let ty = BL.lookup _varIndex vars ^. binderType
in if
| isTypeConstr ty -> End (mkDynamic _varInfo)
| isTypeConstr tab ty -> End (mkDynamic _varInfo)
| otherwise -> End (NVar (shiftVar (-k) v))
where
k = length (filter (isTypeConstr . (^. binderType)) (take _varIndex (toList vars)))
NApp (App {}) ->
k = length (filter (isTypeConstr tab . (^. binderType)) (take _varIndex (toList vars)))
NIdt Ident {..} ->
let fi = fromJust $ HashMap.lookup _identSymbol (tab ^. infoIdentifiers)
in if
| isTypeConstr tab (fi ^. identifierType) ->
Recur (fromJust $ HashMap.lookup _identSymbol (tab ^. identContext))
| otherwise ->
Recur node
NApp App {..} ->
let (h, args) = unfoldApps node
ty =
case h of
@ -36,9 +52,11 @@ convertNode tab = convert mempty
NIdt (Ident {..}) ->
let fi = fromJust $ HashMap.lookup _identSymbol (tab ^. infoIdentifiers)
in fi ^. identifierType
_ -> unsupported
_ -> unsupported node
args' = filterArgs ty args
in if
| isTypeConstr tab ty ->
End (mkDynamic _appInfo)
| null args' ->
End (convert vars h)
| otherwise ->
@ -51,12 +69,21 @@ convertNode tab = convert mempty
NCase (Case {..}) ->
End (mkCase _caseInfo _caseInductive (convert vars _caseValue) (map convertBranch _caseBranches) (fmap (convert vars) _caseDefault))
where
nParams :: Int
nParams = maybe 0 (length . (^. inductiveParams)) (tab ^. infoInductives . at _caseInductive)
convertBranch :: CaseBranch -> CaseBranch
convertBranch br@CaseBranch {..} =
let binders' = filterBinders vars _caseBranchBinders
let paramBinders = map (set binderType mkSmallUniv) (take nParams _caseBranchBinders)
argBinders = drop nParams _caseBranchBinders
tyargs = drop nParams (typeArgs (fromJust (tab ^. infoConstructors . at _caseBranchTag) ^. constructorType))
argBinders' = zipWith (\b ty -> if isDynamic (b ^. binderType) && isTypeConstr tab ty then set binderType ty b else b) argBinders (tyargs ++ repeat mkDynamic')
binders' =
filterBinders
(BL.prependRev paramBinders vars)
argBinders'
body' =
convert
(BL.prependRev _caseBranchBinders vars)
(BL.prependRev argBinders' (BL.prependRev paramBinders vars))
_caseBranchBody
in br
{ _caseBranchBinders = binders',
@ -66,22 +93,25 @@ convertNode tab = convert mempty
filterBinders :: BinderList Binder -> [Binder] -> [Binder]
filterBinders _ [] = []
filterBinders vars' (b : bs)
| isTypeConstr (b ^. binderType) =
| isTypeConstr tab (b ^. binderType) =
filterBinders (BL.cons b vars') bs
filterBinders vars' (b : bs) =
over binderType (convert vars') b : filterBinders (BL.cons b vars') bs
NLam (Lambda {..})
| isTypeConstr (_lambdaBinder ^. binderType) ->
| isTypeConstr tab (_lambdaBinder ^. binderType) ->
End (convert (BL.cons _lambdaBinder vars) _lambdaBody)
NLet (Let {..})
| isTypeConstr tab (_letItem ^. letItemBinder . binderType) ->
End (convert (BL.cons (_letItem ^. letItemBinder) vars) _letBody)
NPi (Pi {..})
| isTypeConstr (_piBinder ^. binderType) && not (isTypeConstr _piBody) ->
| isTypeConstr tab (_piBinder ^. binderType) && not (isTypeConstr tab _piBody) ->
End (convert (BL.cons _piBinder vars) _piBody)
_ -> Recur node
where
filterArgs :: Type -> [a] -> [a]
filterArgs ty args =
map fst $
filter (not . isTypeConstr . snd) (zip args (typeArgs ty ++ repeat mkDynamic'))
filter (not . isTypeConstr tab . snd) (zip args (typeArgs ty ++ repeat mkDynamic'))
convertIdent :: InfoTable -> IdentifierInfo -> IdentifierInfo
convertIdent tab ii =
@ -91,7 +121,7 @@ convertIdent tab ii =
map (uncurry (set argumentType)) $
zipExact tyargs' $
map fst $
filter (not . isTypeConstr . snd) (zipExact (ii ^. identifierArgsInfo) tyargs),
filter (not . isTypeConstr tab . snd) (zipExact (ii ^. identifierArgsInfo) tyargs),
_identifierArgsNum = length (typeArgs ty')
}
where
@ -112,7 +142,7 @@ convertInductive :: InfoTable -> InductiveInfo -> InductiveInfo
convertInductive tab ii =
ii
{ _inductiveKind = ty',
_inductiveParams = map (over paramKind (convertNode tab) . fst) $ filter (not . isTypeConstr . snd) (zipExact (ii ^. inductiveParams) tyargs),
_inductiveParams = map (over paramKind (convertNode tab) . fst) $ filter (not . isTypeConstr tab . snd) (zipExact (ii ^. inductiveParams) tyargs),
_inductiveConstructors = map (convertConstructor tab) (ii ^. inductiveConstructors)
}
where

557
src/Juvix/Compiler/Core/Translation/FromInternal.hs
View File

@ -2,6 +2,7 @@ module Juvix.Compiler.Core.Translation.FromInternal where
import Data.HashMap.Strict qualified as HashMap
import Data.List.NonEmpty (fromList)
import Data.List.NonEmpty qualified as NonEmpty
import Juvix.Compiler.Abstract.Data.Name
import Juvix.Compiler.Concrete.Data.Literal (LiteralLoc)
import Juvix.Compiler.Core.Data
@ -10,7 +11,6 @@ import Juvix.Compiler.Core.Info qualified as Info
import Juvix.Compiler.Core.Info.LocationInfo
import Juvix.Compiler.Core.Info.NameInfo
import Juvix.Compiler.Core.Language
import Juvix.Compiler.Core.Transformation.Eta (etaExpandApps)
import Juvix.Compiler.Core.Translation.FromInternal.Data
import Juvix.Compiler.Internal.Extra qualified as Internal
import Juvix.Compiler.Internal.Translation.Extra qualified as Internal
@ -18,9 +18,6 @@ import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking qu
import Juvix.Data.Loc qualified as Loc
import Juvix.Extra.Strings qualified as Str
unsupported :: Text -> a
unsupported thing = error ("Internal to Core: Not yet supported: " <> thing)
-- Translation of a Name into the identifier index used in the Core InfoTable
mkIdentIndex :: Name -> Text
mkIdentIndex = show . (^. Internal.nameId . Internal.unNameId)
@ -47,28 +44,28 @@ setupIntToNat sym tab =
_argumentIsImplicit = Explicit
}
],
_identifierType = mkDynamic',
_identifierType = mkPi' mkTypeInteger' mkTypeInteger',
_identifierIsExported = False,
_identifierBuiltin = Nothing
}
node =
case (tagZeroM, tagSucM, boolSymM) of
(Just tagZero, Just tagSuc, Just boolSym) ->
mkLambda' $
mkLambda' mkTypeInteger' $
mkIf'
boolSym
(mkBuiltinApp' OpEq [mkVar' 0, mkConstant' (ConstInteger 0)])
(mkConstr (setInfoName "zero" mempty) tagZero [])
(mkConstr (setInfoName "suc" mempty) tagSuc [mkApp' (mkIdent' sym) (mkBuiltinApp' OpIntSub [mkVar' 0, mkConstant' (ConstInteger 1)])])
_ ->
mkLambda' $ mkVar' 0
mkLambda' mkTypeInteger' $ mkVar' 0
tagZeroM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatZero
tagSucM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatSuc
boolSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinBool
fromInternal :: Internal.InternalTypedResult -> Sem k CoreResult
fromInternal i = do
(res, _) <- runInfoTableBuilder tab0 (runReader (i ^. InternalTyped.resultIdenTypes) f)
(res, _) <- runInfoTableBuilder tab0 (evalState (i ^. InternalTyped.resultFunctions) (runReader (i ^. InternalTyped.resultIdenTypes) f))
return $
CoreResult
{ _coreResultTable = setupIntToNat intToNatSym res,
@ -81,13 +78,12 @@ fromInternal i = do
intToNatSym :: Symbol
intToNatSym = 0
f :: (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable] r) => Sem r ()
f :: (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable] r) => Sem r ()
f = do
declareIOBuiltins
let resultModules = toList (i ^. InternalTyped.resultModules)
runReader (Internal.buildTable resultModules) (mapM_ coreModule resultModules)
where
coreModule :: (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) => Internal.Module -> Sem r ()
coreModule :: (Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) => Internal.Module -> Sem r ()
coreModule m = do
registerInductiveDefs m
registerFunctionDefs m
@ -100,22 +96,25 @@ fromInternalExpression res exp = do
(Internal.buildTable modules)
( runInfoTableBuilder
(res ^. coreResultTable)
( runReader
(res ^. coreResultInternalTypedResult . InternalTyped.resultIdenTypes)
(runReader initIndexTable (goExpression exp))
( evalState
(res ^. coreResultInternalTypedResult . InternalTyped.resultFunctions)
( runReader
(res ^. coreResultInternalTypedResult . InternalTyped.resultIdenTypes)
(runReader initIndexTable (goExpression exp))
)
)
)
registerInductiveDefs ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
Internal.Module ->
Sem r ()
registerInductiveDefs m = registerInductiveDefsBody (m ^. Internal.moduleBody)
registerInductiveDefsBody ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
Internal.ModuleBody ->
Sem r ()
registerInductiveDefsBody body = mapM_ go (body ^. Internal.moduleStatements)
@ -131,14 +130,14 @@ registerInductiveDefsBody body = mapM_ go (body ^. Internal.moduleStatements)
registerFunctionDefs ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
Internal.Module ->
Sem r ()
registerFunctionDefs m = registerFunctionDefsBody (m ^. Internal.moduleBody)
registerFunctionDefsBody ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
Internal.ModuleBody ->
Sem r ()
registerFunctionDefsBody body = mapM_ go (body ^. Internal.moduleStatements)
@ -152,28 +151,43 @@ registerFunctionDefsBody body = mapM_ go (body ^. Internal.moduleStatements)
goInductiveDef ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
Internal.InductiveDef ->
Sem r ()
goInductiveDef i = do
sym <- freshSymbol
ctorInfos <- mapM (goConstructor sym) (i ^. Internal.inductiveConstructors)
let info =
let params =
map
( \p ->
ParameterInfo
{ _paramName = p ^. Internal.inductiveParamName . nameText,
_paramLocation = Just $ p ^. Internal.inductiveParamName . nameLoc,
_paramIsImplicit = False, -- TODO: not currently easily available in Internal
_paramKind = mkSmallUniv
}
)
(i ^. Internal.inductiveParameters)
info =
InductiveInfo
{ _inductiveName = i ^. Internal.inductiveName . nameText,
_inductiveLocation = Just $ i ^. Internal.inductiveName . nameLoc,
_inductiveSymbol = sym,
_inductiveKind = mkDynamic',
_inductiveConstructors = ctorInfos,
_inductiveParams = [],
_inductiveKind = mkSmallUniv,
_inductiveConstructors = [],
_inductiveParams = params,
_inductivePositive = i ^. Internal.inductivePositive,
_inductiveBuiltin = i ^. Internal.inductiveBuiltin
_inductiveBuiltin = fmap BuiltinTypeInductive (i ^. Internal.inductiveBuiltin)
}
registerInductive (mkIdentIndex (i ^. Internal.inductiveName)) info
idx = mkIdentIndex (i ^. Internal.inductiveName)
-- The inductive needs to be registered before translating the constructors,
-- because their types refer to the inductive
registerInductive idx info
ctorInfos <- mapM (goConstructor sym) (i ^. Internal.inductiveConstructors)
registerInductive idx info {_inductiveConstructors = ctorInfos}
goConstructor ::
forall r.
(Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable] r) =>
(Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable] r) =>
Symbol ->
Internal.InductiveConstructorDef ->
Sem r ConstructorInfo
@ -219,7 +233,7 @@ goConstructor sym ctor = do
runReader
initIndexTable
( Internal.constructorType ctorName
>>= goExpression
>>= goType
)
argsNum :: Sem r Int
@ -229,32 +243,43 @@ goConstructor sym ctor = do
goMutualBlock ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
Internal.MutualBlock ->
Sem r ()
goMutualBlock m = do
funcsWithSym <- mapM withSym (m ^. Internal.mutualFunctions)
mapM_ goFunctionDefIden funcsWithSym
mapM_ goFunctionDef funcsWithSym
tys <- mapM goFunctionDefIden funcsWithSym
mapM_ goFunctionDef (zipExact (toList funcsWithSym) (toList tys))
where
withSym :: a -> Sem r (a, Symbol)
withSym x = do
sym <- freshSymbol
return (x, sym)
goType ::
forall r.
(Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader IndexTable] r) =>
Internal.Expression ->
Sem r Type
goType ty = do
normTy <- evalState InternalTyped.iniState (InternalTyped.strongNormalize' ty)
squashApps <$> goExpression normTy
goFunctionDefIden ::
forall r.
(Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable] r) =>
(Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable] r) =>
(Internal.FunctionDef, Symbol) ->
Sem r ()
Sem r Type
goFunctionDefIden (f, sym) = do
funTy <- runReader initIndexTable (goExpression (f ^. Internal.funDefType))
funTy <- runReader initIndexTable (goType (f ^. Internal.funDefType))
let info =
IdentifierInfo
{ _identifierName = f ^. Internal.funDefName . nameText,
_identifierLocation = Just $ f ^. Internal.funDefName . nameLoc,
_identifierSymbol = sym,
_identifierType = funTy,
-- _identiferArgsNum needs to match the number of lambdas in the
-- body. This needs to be filled in later (in goFunctionDef).
_identifierArgsNum = 0,
_identifierArgsInfo = [],
_identifierIsExported = False,
@ -262,97 +287,170 @@ goFunctionDefIden (f, sym) = do
}
registerIdent (mkIdentIndex (f ^. Internal.funDefName)) info
when (f ^. Internal.funDefName . Internal.nameText == Str.main) (registerMain sym)
return funTy
goFunctionDef ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
(Internal.FunctionDef, Symbol) ->
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
((Internal.FunctionDef, Symbol), Type) ->
Sem r ()
goFunctionDef (f, sym) = do
goFunctionDef ((f, sym), ty) = do
mbody <- case f ^. Internal.funDefBuiltin of
Just Internal.BuiltinBoolIf -> return Nothing
Just _ -> Just <$> runReader initIndexTable (mkFunBody f)
Nothing -> Just <$> runReader initIndexTable (mkFunBody f)
Just _ -> Just <$> runReader initIndexTable (mkFunBody ty f)
Nothing -> Just <$> runReader initIndexTable (mkFunBody ty f)
forM_ mbody (registerIdentNode sym)
forM_ mbody setIdentArgsInfo'
where
setIdentArgsInfo' :: Node -> Sem r ()
setIdentArgsInfo' node = do
let (is, _) = unfoldLambdas node
setIdentArgsInfo sym (map (argumentInfoFromBinder . (^. lambdaLhsBinder)) is)
mkFunBody ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Type -> -- converted type of the function
Internal.FunctionDef ->
Sem r Node
mkFunBody f
| nPatterns == 0 = goExpression (f ^. Internal.funDefClauses . _head1 . Internal.clauseBody)
mkFunBody ty f =
mkBody ty (fmap (\c -> (c ^. Internal.clausePatterns, c ^. Internal.clauseBody)) (f ^. Internal.funDefClauses))
mkBody ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Type -> -- type of the function
NonEmpty ([Internal.PatternArg], Internal.Expression) ->
Sem r Node
mkBody ty clauses
| nPatterns == 0 = goExpression (snd (head clauses))
| otherwise = do
let values :: [Node]
values = mkVar Info.empty <$> vs
ms <-
local
(over indexTableVarsNum (+ nPatterns))
(mapM goFunctionClause (f ^. Internal.funDefClauses))
let match = mkMatch' (fromList values) (toList ms)
return $ foldr (\_ n -> mkLambda' n) match vs
let values = mkVar Info.empty <$> vs
argtys = take nPatterns (typeArgs ty)
values' = map fst $ filter (isInductive . snd) (zipExact values argtys)
matchArgtys = shiftMatchTypeArg <$> indexFrom 0 argtys
matchTypeTarget = typeTarget ty
matchIndArgTys = filter isInductive matchArgtys
matchReturnType' = mkPis' (drop nPatterns (typeArgs ty)) matchTypeTarget
case values' of
[] -> do
vars <- asks (^. indexTableVars)
varsNum <- asks (^. indexTableVarsNum)
let (pats, body) = head clauses
(vars', varsNum') =
foldl'
(\(vrs, k) pat -> (addPatternVariableNames pat k vrs, k + 1))
(vars, varsNum)
pats
body' <-
local
(set indexTableVars vars' . set indexTableVarsNum varsNum')
(goExpression body)
return $ foldr mkLambda' body' argtys
_ : _ -> do
varsNum <- asks (^. indexTableVarsNum)
ms <- underBinders nPatterns (mapM (uncurry (goClause varsNum)) clauses)
let match = mkMatch' (fromList matchIndArgTys) matchReturnType' (fromList values') (toList ms)
return $ foldr mkLambda' match argtys
where
-- Assumption: All clauses have the same number of patterns
nPatterns :: Int
nPatterns = length (f ^. Internal.funDefClauses . _head1 . Internal.clausePatterns)
nPatterns = checkPatternsNum (length (fst (head clauses))) (NonEmpty.tail $ fmap fst clauses)
vs :: [Index]
vs = reverse (take nPatterns [0 ..])
-- The types of arguments in the match must be shifted due to the
-- difference in level between when the type argument in bound (in a
-- surrounding lambda) and when it is used in the match constructor.
--
-- For example:
--
-- f : {A : Type} -> A -> List A -> A -> A -> List A;
-- f _ _ _ := \ { _ := nil };
--
-- f has the following type, with indices:
--
-- A -> A$0 -> List A$1 -> A$2 -> A$3 -> A$4 -> List A$5
--
-- Is translated to the following match (omiting the translation of the body):
--
-- λ(? : Type)
-- λ(? : A$0)
-- λ(? : List A$1)
-- λ(? : A$2)
-- λ(? : A$3)
-- match (?$2 : List A$4) with : (A$4 → List A$5)
--
-- The return type (A$4 -> List A$5) already has the correct indices
-- relative to the match node. However the type of the match argument has
-- been shifted by the number of pattern binders below it.
shiftMatchTypeArg :: Indexed Type -> Type
shiftMatchTypeArg (Indexed idx ty') = shift (nPatterns - idx) ty'
checkPatternsNum :: Int -> [[a]] -> Int
checkPatternsNum len = \case
[] -> len
ps : pats | length ps == len -> checkPatternsNum len pats
_ -> error "internal-to-core: all clauses must have the same number of patterns"
goClause :: Level -> [Internal.PatternArg] -> Internal.Expression -> Sem r MatchBranch
goClause lvl pats body = goPatternArgs lvl body pats ptys
where
ptys :: [Type]
ptys = take (length pats) (typeArgs ty)
goCase ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Internal.Case ->
Sem r Node
goCase c = do
expr <- goExpression (c ^. Internal.caseExpression)
branches <- toList <$> mapM goCaseBranch (c ^. Internal.caseBranches)
return (mkMatch' (pure expr) branches)
goCaseBranch ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Internal.CaseBranch ->
Sem r MatchBranch
goCaseBranch b = goPatternArgs (b ^. Internal.caseBranchExpression) [b ^. Internal.caseBranchPattern]
underBinders :: Members '[Reader IndexTable] r => Int -> Sem r a -> Sem r a
underBinders nBinders = local (over indexTableVarsNum (+ nBinders))
ty <- goType (fromJust $ c ^. Internal.caseExpressionType)
case ty of
NTyp {} -> do
branches <- toList <$> mapM (goCaseBranch ty) (c ^. Internal.caseBranches)
rty <- goType (fromJust $ c ^. Internal.caseExpressionWholeType)
return (mkMatch' (NonEmpty.singleton ty) rty (pure expr) branches)
_ ->
case c ^. Internal.caseBranches of
Internal.CaseBranch {..} :| _ ->
case _caseBranchPattern ^. Internal.patternArgPattern of
Internal.PatternVariable {} -> do
vars <- asks (^. indexTableVars)
varsNum <- asks (^. indexTableVarsNum)
let vars' = addPatternVariableNames _caseBranchPattern varsNum vars
body <-
local
(set indexTableVars vars')
(underBinders 1 (goExpression _caseBranchExpression))
return $ mkLet' ty expr body
_ ->
impossible
where
goCaseBranch :: Type -> Internal.CaseBranch -> Sem r MatchBranch
goCaseBranch ty b = goPatternArgs 0 (b ^. Internal.caseBranchExpression) [b ^. Internal.caseBranchPattern] [ty]
goLambda ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Internal.Lambda ->
Sem r Node
goLambda l = do
ms <- underBinders nPatterns (mapM goLambdaClause (l ^. Internal.lambdaClauses))
let values = reverse (take nPatterns (mkVar' <$> [0 ..]))
match = mkMatch' (fromList values) (toList ms)
return $ foldr (\_ n -> mkLambda' n) match values
where
nPatterns :: Int
nPatterns = length (l ^. Internal.lambdaClauses . _head1 . Internal.lambdaPatterns)
goLambdaClause ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Internal.LambdaClause ->
Sem r MatchBranch
goLambdaClause clause = goPatternArgs (clause ^. Internal.lambdaBody) ps
where
ps :: [Internal.PatternArg]
ps = toList (clause ^. Internal.lambdaPatterns)
ty <- goType (fromJust (l ^. Internal.lambdaType))
mkBody ty (fmap (\c -> (toList (c ^. Internal.lambdaPatterns), c ^. Internal.lambdaBody)) (l ^. Internal.lambdaClauses))
goLet ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Internal.Let ->
Sem r Node
goLet l = do
vars <- asks (^. indexTableVars)
varsNum <- asks (^. indexTableVarsNum)
let bs :: [Name]
bs = map (\(Internal.LetFunDef (Internal.FunctionDef {..})) -> _funDefName) (toList $ l ^. Internal.letClauses)
bs = map (\(Internal.LetFunDef Internal.FunctionDef {..}) -> _funDefName) (toList $ l ^. Internal.letClauses)
(vars', varsNum') =
foldl'
( \(vs, k) name ->
@ -360,26 +458,27 @@ goLet l = do
)
(vars, varsNum)
bs
(defs, value) <-
local
(set indexTableVars vars' . set indexTableVarsNum varsNum')
( do
a <- mapM goLetClause (l ^. Internal.letClauses)
b <- goExpression (l ^. Internal.letExpression)
return (a, b)
)
return $ mkLetRec' defs value
(defs, value) <- do
values <-
mapM
( \(Internal.LetFunDef f) -> do
funTy <- goType (f ^. Internal.funDefType)
goLetClause ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Internal.LetClause ->
Sem r Node
goLetClause (Internal.LetFunDef f) = mkFunBody f
funBody <- local (set indexTableVars vars' . set indexTableVarsNum varsNum') (mkFunBody funTy f)
return (funTy, funBody)
)
(l ^. Internal.letClauses)
lbody <-
local
(set indexTableVars vars' . set indexTableVarsNum varsNum')
(goExpression (l ^. Internal.letExpression))
return (values, lbody)
return $ mkLetRec' defs value
goAxiomInductive ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
Internal.AxiomDef ->
Sem r ()
goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
@ -391,8 +490,8 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
Internal.BuiltinBoolPrint -> return ()
Internal.BuiltinIOSequence -> return ()
Internal.BuiltinIOReadline -> return ()
Internal.BuiltinString -> registerInductiveAxiom
Internal.BuiltinIO -> registerInductiveAxiom
Internal.BuiltinString -> registerInductiveAxiom (Just BuiltinString) []
Internal.BuiltinIO -> registerInductiveAxiom Nothing builtinIOConstrs
Internal.BuiltinTrace -> return ()
Internal.BuiltinFail -> return ()
Internal.BuiltinStringConcat -> return ()
@ -400,30 +499,34 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
Internal.BuiltinStringToNat -> return ()
Internal.BuiltinNatToString -> return ()
registerInductiveAxiom :: Sem r ()
registerInductiveAxiom = do
registerInductiveAxiom :: Maybe BuiltinAxiom -> [(Tag, Text, Type -> Type, Maybe BuiltinConstructor)] -> Sem r ()
registerInductiveAxiom ax ctrs = do
sym <- freshSymbol
let info =
let ty = mkTypeConstr' sym []
ctrs' = builtinConstrs sym ty ctrs
info =
InductiveInfo
{ _inductiveName = a ^. Internal.axiomName . nameText,
_inductiveLocation = Just $ a ^. Internal.axiomName . nameLoc,
_inductiveSymbol = sym,
_inductiveKind = mkDynamic',
_inductiveConstructors = [],
_inductiveKind = mkSmallUniv,
_inductiveConstructors = ctrs',
_inductiveParams = [],
_inductivePositive = False,
_inductiveBuiltin = Nothing
_inductiveBuiltin = fmap BuiltinTypeAxiom ax
}
registerInductive (mkIdentIndex (a ^. Internal.axiomName)) info
mapM_ (\ci -> registerConstructor (ci ^. constructorName) ci) ctrs'
goAxiomDef ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
Internal.AxiomDef ->
Sem r ()
goAxiomDef a = do
boolSym <- getBoolSymbol
case a ^. Internal.axiomBuiltin >>= builtinBody boolSym of
natSym <- getNatSymbol
case a ^. Internal.axiomBuiltin >>= builtinBody boolSym natSym of
Just body -> do
sym <- freshSymbol
ty <- axiomType'
@ -440,17 +543,20 @@ goAxiomDef a = do
}
registerIdent (mkIdentIndex (a ^. Internal.axiomName)) info
registerIdentNode sym body
let (is, _) = unfoldLambdas body
setIdentArgsInfo sym (map (argumentInfoFromBinder . (^. lambdaLhsBinder)) is)
Nothing -> return ()
where
builtinBody :: Symbol -> Internal.BuiltinAxiom -> Maybe Node
builtinBody boolSym = \case
Internal.BuiltinNatPrint -> Just writeLambda
Internal.BuiltinStringPrint -> Just writeLambda
Internal.BuiltinBoolPrint -> Just writeLambda
builtinBody :: Symbol -> Symbol -> Internal.BuiltinAxiom -> Maybe Node
builtinBody boolSym natSym = \case
Internal.BuiltinNatPrint -> Just $ writeLambda (mkTypeConstr' natSym [])
Internal.BuiltinStringPrint -> Just $ writeLambda mkTypeString'
Internal.BuiltinBoolPrint -> Just $ writeLambda mkTypeBool'
Internal.BuiltinIOSequence -> Nothing
Internal.BuiltinIOReadline ->
Just
( mkLambda'
mkTypeString'
( mkConstr'
(BuiltinTag TagBind)
[ mkConstr' (BuiltinTag TagReadLn) [],
@ -459,13 +565,15 @@ goAxiomDef a = do
)
)
Internal.BuiltinStringConcat ->
Just (mkLambda' (mkLambda' (mkBuiltinApp' OpStrConcat [mkVar' 1, mkVar' 0])))
Just (mkLambda' mkTypeString' (mkLambda' mkTypeString' (mkBuiltinApp' OpStrConcat [mkVar' 1, mkVar' 0])))
Internal.BuiltinStringEq ->
Just (mkLambda' (mkLambda' (mkBuiltinApp' OpEq [mkVar' 1, mkVar' 0])))
Just (mkLambda' mkTypeString' (mkLambda' mkTypeString' (mkBuiltinApp' OpEq [mkVar' 1, mkVar' 0])))
Internal.BuiltinStringToNat -> do
Just
( mkLambda'
mkTypeString'
( mkLet'
mkTypeInteger'
(mkBuiltinApp' OpStrToInt [mkVar' 0])
( mkIf'
boolSym
@ -476,57 +584,82 @@ goAxiomDef a = do
)
)
Internal.BuiltinNatToString ->
Just (mkLambda' (mkBuiltinApp' OpShow [mkVar' 0]))
Just (mkLambda' (mkTypeConstr' natSym []) (mkBuiltinApp' OpShow [mkVar' 0]))
Internal.BuiltinString -> Nothing
Internal.BuiltinIO -> Nothing
Internal.BuiltinTrace -> Nothing
Internal.BuiltinFail ->
Just (mkLambda' (mkLambda' (mkBuiltinApp' OpFail [mkVar' 0])))
Just (mkLambda' mkSmallUniv (mkLambda' (mkVar' 0) (mkBuiltinApp' OpFail [mkVar' 0])))
axiomType' :: Sem r Type
axiomType' = runReader initIndexTable (goExpression (a ^. Internal.axiomType))
axiomType' = runReader initIndexTable (goType (a ^. Internal.axiomType))
writeLambda :: Node
writeLambda = mkLambda' (mkConstr' (BuiltinTag TagWrite) [mkVar' 0])
writeLambda :: Type -> Node
writeLambda ty = mkLambda' ty (mkConstr' (BuiltinTag TagWrite) [mkVar' 0])
fromPatternArg ::
forall r.
(Members '[InfoTableBuilder, Reader Internal.InfoTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Internal.PatternArg ->
Sem r Pattern
fromPatternArg pa = case pa ^. Internal.patternArgName of
Just pan -> wrapAsPattern pan <$> subPat
Just pan -> do
ty <- getPatternType pan
wrapAsPattern pan ty <$> subPat
Nothing -> subPat
where
subPat :: Sem r Pattern
subPat = fromPattern (pa ^. Internal.patternArgPattern)
wrapAsPattern :: Name -> Pattern -> Pattern
wrapAsPattern pan pat =
wrapAsPattern :: Name -> Type -> Pattern -> Pattern
wrapAsPattern pan ty pat =
( PatBinder
( PatternBinder
{ _patternBinder =
Binder
{ _binderName = pan ^. nameText,
_binderLocation = Just (pan ^. nameLoc),
_binderType = mkDynamic'
_binderType = ty
},
_patternBinderPattern = pat
}
)
)
getPatternType :: Name -> Sem r Type
getPatternType n = asks (fromJust . HashMap.lookup n) >>= goType
-- The types of the pattern must be shifted by the index of the argument
-- within the params
indexedPatternArgs :: [Internal.PatternArg] -> Sem r [Pattern]
indexedPatternArgs ps = mapM go (indexFrom 0 ps)
where
go :: Indexed (Internal.PatternArg) -> Sem r Pattern
go (Indexed i p) = local (over indexTableVarsNum (+ i)) (fromPatternArg p)
fromPattern :: Internal.Pattern -> Sem r Pattern
fromPattern = \case
Internal.PatternVariable n -> return $ PatBinder (PatternBinder (Binder (n ^. nameText) (Just (n ^. nameLoc)) mkDynamic') wildcard)
Internal.PatternVariable n -> do
ty <- getPatternType n
return $ PatBinder (PatternBinder (Binder (n ^. nameText) (Just (n ^. nameLoc)) ty) (wildcard ty))
Internal.PatternConstructorApp c -> do
(indParams, _) <- InternalTyped.lookupConstructorArgTypes n
patternArgs <- mapM fromPatternArg params
let indArgs = replicate (length indParams) wildcard
patternArgs <- indexedPatternArgs params
let indArgs = replicate (length indParams) (wildcard mkSmallUniv)
args = indArgs ++ patternArgs
m <- getIdent identIndex
ctorTy <- goType (fromJust (c ^. Internal.constrAppType))
case m of
Just (IdentConstr tag) -> return $ PatConstr (PatternConstr (setInfoLocation (n ^. nameLoc) (setInfoName (n ^. nameText) Info.empty)) tag args)
Just (IdentConstr tag) ->
return $
PatConstr
( PatternConstr
{ _patternConstrInfo = setInfoLocation (n ^. nameLoc) (setInfoName (n ^. nameText) Info.empty),
_patternConstrTag = tag,
_patternConstrArgs = args,
_patternConstrType = ctorTy
}
)
Just _ -> error ("internal to core: not a constructor " <> txt)
Nothing -> error ("internal to core: undeclared identifier: " <> txt)
where
@ -542,8 +675,8 @@ fromPatternArg pa = case pa ^. Internal.patternArgName of
txt :: Text
txt = c ^. Internal.constrAppConstructor . Internal.nameText
where
wildcard :: Pattern
wildcard = PatWildcard (PatternWildcard Info.empty)
wildcard :: Type -> Pattern
wildcard ty = PatWildcard (PatternWildcard Info.empty ty)
getPatternArgVars :: Internal.PatternArg -> [Name]
getPatternArgVars pa = case pa ^. Internal.patternArgName of
@ -561,59 +694,65 @@ getPatternArgVars pa = case pa ^. Internal.patternArgName of
goPatternArgs ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Level -> -- the level of the first binder for the matched value
Internal.Expression ->
[Internal.PatternArg] ->
[Type] -> -- types of the patterns
Sem r MatchBranch
goPatternArgs body ps = do
vars <- asks (^. indexTableVars)
varsNum <- asks (^. indexTableVarsNum)
pats <- patterns
let bs :: [Name]
bs = concatMap getPatternArgVars ps
(vars', varsNum') =
foldl'
( \(vs, k) name ->
(HashMap.insert (name ^. nameId) k vs, k + 1)
)
(vars, varsNum)
bs
body' :: Sem r Node
body' =
goPatternArgs lvl0 body ps0 ptys0 = go lvl0 [] ps0 ptys0
where
-- `lvl` is the level of the lambda-bound variable corresponding to the current pattern
go :: Level -> [Pattern] -> [Internal.PatternArg] -> [Type] -> Sem r MatchBranch
go lvl pats ps ptys = case (ps, ptys) of
-- The pattern has an inductive type, so can be matched on
(p : ps', NTyp {} : ptys') -> do
pat <- fromPatternArg p
vars <- asks (^. indexTableVars)
varsNum <- asks (^. indexTableVarsNum)
let bs :: [Name]
bs = getPatternArgVars p
(vars', varsNum') =
foldl'
( \(vs, k) name ->
(HashMap.insert (name ^. nameId) k vs, k + 1)
)
(vars, varsNum)
bs
local
(set indexTableVars vars' . set indexTableVarsNum varsNum')
(goExpression body)
MatchBranch Info.empty (fromList pats) <$> body'
where
patterns :: Sem r [Pattern]
patterns = mapM fromPatternArg ps
(go (lvl + 1) (pat : pats) ps' ptys')
(p : ps', _ : ptys') ->
-- The pattern does not have an inductive type, so is excluded from the match
case p ^. Internal.patternArgPattern of
Internal.PatternVariable {} -> do
vars <- asks (^. indexTableVars)
let vars' = addPatternVariableNames p lvl vars
local
(set indexTableVars vars')
(go (lvl + 1) pats ps' ptys')
_ ->
impossible
([], []) -> do
body' <- goExpression body
return $ MatchBranch Info.empty (fromList (reverse pats)) body'
_ ->
impossible
goFunctionClause ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Internal.FunctionClause ->
Sem r MatchBranch
goFunctionClause clause = goPatternArgs (clause ^. Internal.clauseBody) internalPatternArgs
where
internalPatternArgs :: [Internal.PatternArg]
internalPatternArgs = clause ^. Internal.clausePatterns
addPatternVariableNames ::
Internal.PatternArg ->
Level ->
HashMap NameId Level ->
HashMap NameId Level
addPatternVariableNames p lvl vars =
foldl' (\vs name -> HashMap.insert (name ^. nameId) lvl vs) vars (getPatternArgVars p)
goExpression ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Internal.Expression ->
Sem r Node
goExpression e = do
node <- goExpression' e
tab <- getInfoTable
return $ etaExpandApps tab node
goExpression' ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Internal.Expression ->
Sem r Node
goExpression' = \case
goExpression = \case
Internal.ExpressionLet l -> goLet l
Internal.ExpressionLiteral l -> do
tab <- getInfoTable
@ -626,9 +765,9 @@ goExpression' = \case
Internal.IdenFunction n -> do
funInfoBuiltin <- Internal.getFunctionBuiltinInfo n
case funInfoBuiltin of
Just Internal.BuiltinBoolIf -> error "if must be called with 3 arguments"
Just Internal.BuiltinBoolOr -> error "|| must be called with 2 arguments"
Just Internal.BuiltinBoolAnd -> error "&& must be called with 2 arguments"
Just Internal.BuiltinBoolIf -> error "internal to core: if must be called with 3 arguments"
Just Internal.BuiltinBoolOr -> error "internal to core: || must be called with 2 arguments"
Just Internal.BuiltinBoolAnd -> error "internal to core: && must be called with 2 arguments"
_ -> return ()
-- if the function was defined by a let, then in Core it is stored in a variable
vars <- asks (^. indexTableVars)
@ -657,8 +796,8 @@ goExpression' = \case
Internal.IdenAxiom n -> do
axiomInfoBuiltin <- Internal.getAxiomBuiltinInfo n
case axiomInfoBuiltin of
Just Internal.BuiltinIOSequence -> error ">> must be called with 2 arguments"
Just Internal.BuiltinTrace -> error "trace must be called with 2 arguments"
Just Internal.BuiltinIOSequence -> error "internal to core: >> must be called with 2 arguments"
Just Internal.BuiltinTrace -> error "internal to core: trace must be called with 2 arguments"
_ -> return ()
m <- getIdent identIndex
return $ case m of
@ -679,34 +818,45 @@ goExpression' = \case
Internal.ExpressionSimpleLambda l -> goSimpleLambda l
Internal.ExpressionLambda l -> goLambda l
Internal.ExpressionCase l -> goCase l
e@(Internal.ExpressionFunction {}) -> goFunction (Internal.unfoldFunType e)
Internal.ExpressionHole h -> error ("goExpression hole: " <> show (Loc.getLoc h))
Internal.ExpressionUniverse {} -> return (mkUniv' (fromIntegral smallLevel))
e@Internal.ExpressionFunction {} -> goFunction (Internal.unfoldFunType e)
Internal.ExpressionHole h -> error ("internal to core: goExpression hole: " <> show (Loc.getLoc h))
Internal.ExpressionUniverse {} -> return mkSmallUniv
goFunction ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
([Internal.FunctionParameter], Internal.Expression) ->
Sem r Node
goFunction (params, returnTypeExpr) = foldr f (goExpression returnTypeExpr) params
goFunction (params, returnTypeExpr) = go params
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)
case param ^. Internal.paramName of
Nothing -> mkPi mempty paramBinder <$> acc
Just vn -> mkPi mempty paramBinder <$> localAddName vn acc
go :: [Internal.FunctionParameter] -> Sem r Node
go = \case
param : params' -> do
paramTy <- goType (param ^. Internal.paramType)
let paramBinder =
Binder
{ _binderName = maybe "?" (^. nameText) $ param ^. Internal.paramName,
_binderLocation = fmap (^. nameLoc) $ param ^. Internal.paramName,
_binderType = paramTy
}
case param ^. Internal.paramName of
Nothing -> mkPi mempty paramBinder <$> local (over indexTableVarsNum (+ 1)) (go params')
Just vn -> mkPi mempty paramBinder <$> localAddName vn (go params')
[] ->
goType returnTypeExpr
goSimpleLambda ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Internal.SimpleLambda ->
Sem r Node
goSimpleLambda l = localAddName (l ^. Internal.slambdaVar) (mkLambda' <$> goExpression (l ^. Internal.slambdaBody))
goSimpleLambda l = do
ty <- goType (l ^. Internal.slambdaVarType)
localAddName (l ^. Internal.slambdaVar) (mkLambda' ty <$> goExpression (l ^. Internal.slambdaBody))
goApplication ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Internal.Application ->
Sem r Node
goApplication a = do
@ -729,11 +879,18 @@ goApplication a = do
Just Internal.BuiltinString -> app
Just Internal.BuiltinIO -> app
Just Internal.BuiltinIOSequence -> do
ioSym <- getIOSymbol
as <- exprArgs
case as of
(arg1 : arg2 : xs) ->
return (mkApps' (mkConstr' (BuiltinTag TagBind) [arg1, mkLambda' (shift 1 arg2)]) xs)
_ -> error ">> must be called with 2 arguments"
return $
mkApps'
( mkConstr'
(BuiltinTag TagBind)
[arg1, mkLambda' (mkTypeConstr' ioSym []) (shift 1 arg2)]
)
xs
_ -> error "internal to core: >> must be called with 2 arguments"
Just Internal.BuiltinIOReadline -> app
Just Internal.BuiltinStringConcat -> app
Just Internal.BuiltinStringEq -> app
@ -744,7 +901,7 @@ goApplication a = do
case as of
(_ : _ : arg1 : arg2 : xs) ->
return (mkApps' (mkBuiltinApp' OpTrace [arg1, arg2]) xs)
_ -> error "trace must be called with 2 arguments"
_ -> error "internal to core: trace must be called with 2 arguments"
Just Internal.BuiltinFail -> app
Nothing -> app
Internal.ExpressionIden (Internal.IdenFunction n) -> do
@ -755,19 +912,19 @@ goApplication a = do
as <- exprArgs
case as of
(_ : v : b1 : b2 : xs) -> return (mkApps' (mkIf' sym v b1 b2) xs)
_ -> error "if must be called with 3 arguments"
_ -> error "internal to core: if must be called with 3 arguments"
Just Internal.BuiltinBoolOr -> do
sym <- getBoolSymbol
as <- exprArgs
case as of
(x : y : xs) -> return (mkApps' (mkIf' sym x (mkConstr' (BuiltinTag TagTrue) []) y) xs)
_ -> error "|| must be called with 2 arguments"
_ -> error "internal to core: || must be called with 2 arguments"
Just Internal.BuiltinBoolAnd -> do
sym <- getBoolSymbol
as <- exprArgs
case as of
(x : y : xs) -> return (mkApps' (mkIf' sym x y (mkConstr' (BuiltinTag TagFalse) [])) xs)
_ -> error "&& must be called with 2 arguments"
_ -> error "internal to core: && must be called with 2 arguments"
_ -> app
_ -> app

3
src/Juvix/Compiler/Core/Translation/FromInternal/Data/IndexTable.hs
View File

@ -26,3 +26,6 @@ localAddName n s = do
( over indexTableVars (HashMap.insert (n ^. nameId) idx)
. over indexTableVarsNum (+ 1)
)
underBinders :: Members '[Reader IndexTable] r => Int -> Sem r a -> Sem r a
underBinders nBinders = local (over indexTableVarsNum (+ nBinders))

147
src/Juvix/Compiler/Core/Translation/FromSource.hs
View File

@ -156,16 +156,7 @@ parseDefinition sym ty = do
&& not (isDynamic (typeTarget ty))
)
$ parseFailure off "type mismatch: too many lambdas"
lift $ setIdentArgsInfo sym (map (toArgumentInfo . (^. lambdaLhsBinder)) is)
where
toArgumentInfo :: Binder -> ArgumentInfo
toArgumentInfo bi =
ArgumentInfo
{ _argumentName = bi ^. binderName,
_argumentLocation = bi ^. binderLocation,
_argumentType = bi ^. binderType,
_argumentIsImplicit = Explicit
}
lift $ setIdentArgsInfo sym (map (argumentInfoFromBinder . (^. lambdaLhsBinder)) is)
statementInductive ::
(Member InfoTableBuilder r) =>
@ -250,6 +241,15 @@ bracedExpr ::
ParsecS r Node
bracedExpr varsNum vars = braces (expr varsNum vars) <|> expr varsNum vars
typeAnnot ::
(Member InfoTableBuilder r) =>
Index ->
HashMap Text Level ->
ParsecS r Node
typeAnnot varsNum vars = do
kw kwColon
expr varsNum vars
typeExpr ::
(Member InfoTableBuilder r) =>
Index ->
@ -587,8 +587,7 @@ exprPi ::
exprPi varsNum vars = do
kw kwPi
(name, loc) <- parseLocalName
kw kwColon
ty <- expr varsNum vars
ty <- typeAnnot varsNum vars
kw kwComma
let vars' = HashMap.insert name varsNum vars
bi = Binder name (Just loc) ty
@ -612,8 +611,7 @@ exprLambda varsNum vars = do
parens
( do
n <- parseLocalName
kw kwColon
ty <- expr varsNum vars
ty <- typeAnnot varsNum vars
return (n, Just ty)
)
<|> (\n -> (n, Nothing)) <$> parseLocalName
@ -667,12 +665,14 @@ letrecDefs names varsNum vars = forM names letrecItem
letrecItem n = do
off <- P.getOffset
(txt, i) <- identifierL
mty <- optional (typeAnnot varsNum vars)
when (n /= txt) $
parseFailure off "identifier name doesn't match letrec signature"
kw kwAssign
v <- bracedExpr varsNum vars
kw kwSemicolon
return $ LetItem (Binder txt (Just i) mkDynamic') v
let ty = fromMaybe mkDynamic' mty
return $ LetItem (Binder txt (Just i) ty) v
letrecDef ::
(Member InfoTableBuilder r) =>
@ -693,7 +693,7 @@ exprLet ::
exprLet varsNum vars = do
kw kwLet
(name, loc) <- parseLocalName
mty <- optional (kw kwColon >> expr varsNum vars)
mty <- optional (typeAnnot varsNum vars)
kw kwAssign
value <- bracedExpr varsNum vars
kw kwIn
@ -824,20 +824,42 @@ exprMatch ::
ParsecS r Node
exprMatch varsNum vars = do
kw kwMatch
values <- P.sepBy (bracedExpr varsNum vars) (kw kwComma)
vals <- P.sepBy (exprMatchValue varsNum vars) (kw kwComma)
kw kwWith
braces (exprMatch' values varsNum vars)
<|> exprMatch' values varsNum vars
mty <- optional (typeAnnot varsNum vars)
let rty = fromMaybe mkDynamic' mty
braces (exprMatch' vals rty varsNum vars)
<|> exprMatch' vals rty varsNum vars
exprMatchValue ::
(Member InfoTableBuilder r) =>
Index ->
HashMap Text Level ->
ParsecS r (Node, Type)
exprMatchValue varsNum vars = parens (exprMatchValue' varsNum vars) <|> exprMatchValue' varsNum vars
exprMatchValue' ::
(Member InfoTableBuilder r) =>
Index ->
HashMap Text Level ->
ParsecS r (Node, Type)
exprMatchValue' varsNum vars = do
val <- expr varsNum vars
mty <- optional (typeAnnot varsNum vars)
return (val, fromMaybe mkDynamic' mty)
exprMatch' ::
(Member InfoTableBuilder r) =>
[Node] ->
[(Node, Type)] ->
Type ->
Index ->
HashMap Text Level ->
ParsecS r Node
exprMatch' values varsNum vars = do
exprMatch' vals rty varsNum vars = do
let values = map fst vals
types = map snd vals
bs <- P.sepEndBy (matchBranch (length values) varsNum vars) (kw kwSemicolon)
return $ mkMatch' (fromList values) bs
return $ mkMatch' (fromList types) rty (fromList values) bs
matchBranch ::
(Member InfoTableBuilder r) =>
@ -847,7 +869,7 @@ matchBranch ::
ParsecS r MatchBranch
matchBranch patsNum varsNum vars = do
off <- P.getOffset
pats <- P.sepBy branchPattern (kw kwComma)
pats <- branchPatterns varsNum vars
kw kwAssign
unless (length pats == patsNum) $
parseFailure off "wrong number of patterns"
@ -863,50 +885,87 @@ matchBranch patsNum varsNum vars = do
br <- bracedExpr varsNum' vars'
return $ MatchBranch Info.empty (fromList pats) br
branchPatterns ::
(Member InfoTableBuilder r) =>
Index ->
HashMap Text Level ->
ParsecS r [Pattern]
branchPatterns varsNum vars = do
(pat, (varsNum', vars')) <- branchPattern varsNum vars
pats <- (kw kwComma >> branchPatterns varsNum' vars') <|> return []
return (pat : pats)
branchPattern ::
(Member InfoTableBuilder r) =>
ParsecS r Pattern
branchPattern =
wildcardPattern
<|> binderOrConstrPattern True
<|> parens branchPattern
Index ->
HashMap Text Level ->
ParsecS r (Pattern, (Index, HashMap Text Level))
branchPattern varsNum vars =
parens (branchPattern varsNum vars)
<|> wildcardPattern varsNum vars
<|> binderOrConstrPattern True varsNum vars
wildcardPattern :: ParsecS r Pattern
wildcardPattern = do
wildcardPattern ::
Index ->
HashMap Text Level ->
ParsecS r (Pattern, (Index, HashMap Text Level))
wildcardPattern varsNum vars = do
kw kwWildcard
return $ PatWildcard (PatternWildcard Info.empty)
return (PatWildcard (PatternWildcard Info.empty mkDynamic'), (varsNum, vars))
binderOrConstrPattern ::
(Member InfoTableBuilder r) =>
Bool ->
ParsecS r Pattern
binderOrConstrPattern parseArgs = do
Index ->
HashMap Text Level ->
ParsecS r (Pattern, (Index, HashMap Text Level))
binderOrConstrPattern parseArgs varsNum vars = do
off <- P.getOffset
(txt, i) <- identifierL
r <- lift (getIdent txt)
case r of
Just (IdentConstr tag) -> do
ps <- if parseArgs then P.many branchPattern else return []
(ps, (varsNum', vars')) <- if parseArgs then constrArgPatterns varsNum vars else return ([], (varsNum, vars))
ci <- lift $ getConstructorInfo tag
when
(ci ^. constructorArgsNum /= length ps)
(parseFailure off "wrong number of constructor arguments")
let info = setInfoName (ci ^. constructorName) Info.empty
return $ PatConstr (PatternConstr info tag ps)
mty <- optional (typeAnnot varsNum vars)
return (PatConstr (PatternConstr info tag ps (fromMaybe mkDynamic' mty)), (varsNum', vars'))
_ -> do
mp <- optional binderPattern
let pat = fromMaybe (PatWildcard (PatternWildcard Info.empty)) mp
binder = Binder txt (Just i) mkDynamic'
return $ PatBinder (PatternBinder binder pat)
let vars1 = HashMap.insert txt varsNum vars
mp <- optional (binderPattern (varsNum + 1) vars1)
mty <- optional (typeAnnot varsNum vars)
let ty = fromMaybe mkDynamic' mty
(pat, (varsNum', vars')) = fromMaybe (PatWildcard (PatternWildcard Info.empty ty), (varsNum + 1, vars1)) mp
binder = Binder txt (Just i) ty
return (PatBinder (PatternBinder binder pat), (varsNum', vars'))
constrArgPatterns ::
(Member InfoTableBuilder r) =>
Index ->
HashMap Text Level ->
ParsecS r ([Pattern], (Index, HashMap Text Level))
constrArgPatterns varsNum vars = do
mr <- optional (branchPattern varsNum vars)
case mr of
Just (pat, (varsNum', vars')) -> do
(pats, (varsNum'', vars'')) <- constrArgPatterns varsNum' vars'
return (pat : pats, (varsNum'', vars''))
Nothing ->
return ([], (varsNum, vars))
binderPattern ::
(Member InfoTableBuilder r) =>
ParsecS r Pattern
binderPattern = do
Index ->
HashMap Text Level ->
ParsecS r (Pattern, (Index, HashMap Text Level))
binderPattern varsNum vars = do
symbolAt
wildcardPattern
<|> binderOrConstrPattern False
<|> parens branchPattern
parens (branchPattern varsNum vars)
<|> wildcardPattern varsNum vars
<|> binderOrConstrPattern False varsNum vars
exprNamed ::
(Member InfoTableBuilder r) =>

60
src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
View File

@ -14,10 +14,20 @@ 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)
_infoFunctions = fmap (translateFunctionInfo tab) (tab' ^. infoIdentifiers),
_infoInductives = fmap translateInductiveInfo (tab' ^. infoInductives),
_infoConstructors = fmap translateConstructorInfo (tab' ^. infoConstructors)
}
where
tab' =
tab
{ _infoIdentifiers = HashMap.filter (\ii -> isNothing (ii ^. identifierBuiltin)) (tab ^. infoIdentifiers),
_infoInductives = HashMap.filter (\ii -> isNothing (ii ^. inductiveBuiltin) || isIO (ii ^. inductiveBuiltin)) (tab ^. infoInductives),
_infoConstructors = HashMap.filter (\ci -> isNothing (ci ^. constructorBuiltin)) (tab ^. infoConstructors)
}
isIO :: Maybe BuiltinType -> Bool
isIO (Just (BuiltinTypeAxiom BuiltinIO)) = True
isIO _ = False
translateFunctionInfo :: InfoTable -> IdentifierInfo -> Stripped.FunctionInfo
translateFunctionInfo tab IdentifierInfo {..} =
@ -117,12 +127,26 @@ translateNode node = case node of
)
(translateNode (_letItem ^. letItemValue))
(translateNode _letBody)
NCase Case {..} ->
Stripped.mkCase
_caseInductive
(translateNode _caseValue)
(map translateCaseBranch _caseBranches)
(fmap translateNode _caseDefault)
NCase Case {..} -> case _caseBranches of
[br@CaseBranch {..}]
| _caseBranchTag == BuiltinTag TagTrue ->
translateIf _caseValue (br ^. caseBranchBody) (fromMaybe branchFailure _caseDefault)
[br@CaseBranch {..}]
| _caseBranchTag == BuiltinTag TagFalse ->
translateIf _caseValue (fromMaybe branchFailure _caseDefault) (br ^. caseBranchBody)
[br1, br2]
| br1 ^. caseBranchTag == BuiltinTag TagTrue
&& br2 ^. caseBranchTag == BuiltinTag TagFalse ->
translateIf _caseValue (br1 ^. caseBranchBody) (br2 ^. caseBranchBody)
| br1 ^. caseBranchTag == BuiltinTag TagFalse
&& br2 ^. caseBranchTag == BuiltinTag TagTrue ->
translateIf _caseValue (br2 ^. caseBranchBody) (br1 ^. caseBranchBody)
_ ->
Stripped.mkCase
_caseInductive
(translateNode _caseValue)
(map translateCaseBranch _caseBranches)
(fmap translateNode _caseDefault)
_
| isType node ->
Stripped.mkConstr (Stripped.ConstrInfo "()" Nothing Stripped.TyDynamic) (BuiltinTag TagTrue) []
@ -132,7 +156,16 @@ translateNode node = case node of
unsupported :: a
unsupported = error "Core to Core.Stripped: unsupported node"
translateIf :: Node -> Node -> Node -> Stripped.Node
translateIf val br1 br2 = Stripped.mkIf (translateNode val) (translateNode br1) (translateNode br2)
branchFailure :: Node
branchFailure = mkBuiltinApp' OpFail [mkConstant' (ConstString "illegal `if` branch")]
translateCaseBranch :: CaseBranch -> Stripped.CaseBranch
translateCaseBranch CaseBranch {..}
| _caseBranchTag == BuiltinTag TagTrue || _caseBranchTag == BuiltinTag TagFalse =
error "Core to Core.Stripped: invalid case on booleans"
translateCaseBranch CaseBranch {..} =
Stripped.CaseBranch
{ _caseBranchInfo =
@ -190,4 +223,11 @@ translateType node = case node of
Stripped.TyPrim _typePrimPrimitive
NDyn Dynamic {} ->
Stripped.TyDynamic
_ -> error "Core to Core.Stripped: unsupported type"
_ ->
Stripped.TyDynamic
-- TODO: We need to return TyDynamic here to handle type synonyms. This should
-- be handled by RemoveTypeArgs, but currently it cannot be because
-- lambda-letrec-lifting doesn't preserve the type information about the body.
-- _ -> error $ "Core to Core.Stripped: unsupported type: " <> ppTrace node

28
src/Juvix/Compiler/Internal/Extra.hs
View File

@ -222,7 +222,10 @@ class HasExpressions a where
leafExpressions :: Traversal' a Expression
instance HasExpressions LambdaClause where
leafExpressions f (LambdaClause ps b) = LambdaClause ps <$> leafExpressions f b
leafExpressions f l = do
_lambdaPatterns <- traverse (leafExpressions f) (l ^. lambdaPatterns)
_lambdaBody <- leafExpressions f (l ^. lambdaBody)
pure LambdaClause {..}
instance HasExpressions Lambda where
leafExpressions f l = do
@ -243,8 +246,22 @@ instance HasExpressions Expression where
ExpressionUniverse {} -> f e
ExpressionHole {} -> f e
instance HasExpressions ConstructorApp where
leafExpressions f = traverseOf (constrAppType . _Just) (leafExpressions f)
instance HasExpressions PatternArg where
leafExpressions f = traverseOf patternArgPattern (leafExpressions f)
instance HasExpressions Pattern where
leafExpressions f p = case p of
PatternVariable {} -> pure p
PatternConstructorApp a -> PatternConstructorApp <$> leafExpressions f a
instance HasExpressions CaseBranch where
leafExpressions f = traverseOf caseBranchExpression (leafExpressions f)
leafExpressions f b = do
_caseBranchPattern <- leafExpressions f (b ^. caseBranchPattern)
_caseBranchExpression <- leafExpressions f (b ^. caseBranchExpression)
pure CaseBranch {..}
instance HasExpressions Case where
leafExpressions f l = do
@ -315,9 +332,10 @@ subsHoles s = over leafExpressions helper
_ -> e
instance HasExpressions FunctionClause where
leafExpressions f (FunctionClause n ps b) = do
b' <- leafExpressions f b
pure (FunctionClause n ps b')
leafExpressions f c = do
_clauseBody <- leafExpressions f (c ^. clauseBody)
_clausePatterns <- traverse (leafExpressions f) (c ^. clausePatterns)
pure FunctionClause {_clauseName = c ^. clauseName, ..}
instance HasExpressions Example where
leafExpressions f = traverseOf exampleExpression (leafExpressions f)

18
src/Juvix/Compiler/Internal/Language.hs
View File

@ -6,7 +6,6 @@ module Juvix.Compiler.Internal.Language
module Juvix.Compiler.Concrete.Data.Literal,
module Juvix.Data.Universe,
module Juvix.Data.Hole,
module Juvix.Data.Wildcard,
module Juvix.Compiler.Concrete.Data.Builtins,
)
where
@ -17,7 +16,6 @@ import Juvix.Compiler.Concrete.Data.Literal
import Juvix.Data.Hole
import Juvix.Data.IsImplicit
import Juvix.Data.Universe hiding (smallUniverse)
import Juvix.Data.Wildcard
import Juvix.Data.WithLoc
import Juvix.Prelude
@ -204,7 +202,9 @@ instance Hashable Application where
-- | Fully applied constructor in a pattern.
data ConstructorApp = ConstructorApp
{ _constrAppConstructor :: Name,
_constrAppParameters :: [PatternArg]
_constrAppParameters :: [PatternArg],
-- | The type checker fills this field
_constrAppType :: Maybe Expression
}
deriving stock (Eq, Generic, Data)
@ -322,8 +322,8 @@ instance HasAtomicity Function where
atomicity = const (Aggregate funFixity)
instance HasAtomicity ConstructorApp where
atomicity (ConstructorApp _ args)
| null args = Atom
atomicity ConstructorApp {..}
| null _constrAppParameters = Atom
| otherwise = Aggregate appFixity
instance HasAtomicity PatternArg where
@ -411,7 +411,7 @@ instance HasLoc PatternArg where
getLoc a = fmap getLoc (a ^. patternArgName) ?<> getLoc (a ^. patternArgPattern)
instance HasLoc ConstructorApp where
getLoc (ConstructorApp c ps) =
case last <$> nonEmpty ps of
Just p -> getLoc c <> getLoc p
Nothing -> getLoc c
getLoc ConstructorApp {..} =
case last <$> nonEmpty _constrAppParameters of
Just p -> getLoc _constrAppConstructor <> getLoc p
Nothing -> getLoc _constrAppConstructor

3
src/Juvix/Compiler/Internal/Translation/FromAbstract.hs
View File

@ -259,7 +259,8 @@ goConstructorApp c = do
return
ConstructorApp
{ _constrAppConstructor = c ^. Abstract.constrAppConstructor . Abstract.constructorRefName,
_constrAppParameters = _constrAppParameters'
_constrAppParameters = _constrAppParameters',
_constrAppType = Nothing
}
isSmallType :: Abstract.Expression -> Bool

7
src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
View File

@ -322,16 +322,17 @@ checkPattern ari = traverseOf (patternArgName . each) nameAri >=> traverseOf pat
}
)
-- | TODO: insert holes for constructor implicit arguments
checkConstructorApp ::
forall r.
(Members '[Reader InfoTable, Error ArityCheckerError, State LocalVars] r) =>
ConstructorApp ->
Sem r ConstructorApp
checkConstructorApp ca@(ConstructorApp c ps) = do
checkConstructorApp ca = do
let c = ca ^. constrAppConstructor
args <- (^. constructorInfoArgs) <$> lookupConstructor c
let arities = map typeArity args
n = length arities
ps = ca ^. constrAppParameters
lps = length ps
when
(n /= lps)
@ -344,7 +345,7 @@ checkConstructorApp ca@(ConstructorApp c ps) = do
)
)
ps' <- zipWithM checkPattern arities ps
return (ConstructorApp c ps')
return (ConstructorApp c ps' Nothing)
checkCase ::
forall r.

61
src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
View File

@ -269,10 +269,11 @@ checkFunctionClause ::
FunctionClause ->
Sem r FunctionClause
checkFunctionClause clauseType FunctionClause {..} = do
body' <- checkClause clauseType _clausePatterns _clauseBody
(patterns', body') <- checkClause clauseType _clausePatterns _clauseBody
return
FunctionClause
{ _clauseBody = body',
_clausePatterns = patterns',
..
}
@ -286,19 +287,21 @@ checkClause ::
[PatternArg] ->
-- | Body
Expression ->
Sem r Expression -- Checked body
Sem r ([PatternArg], Expression) -- (Checked patterns, Checked body)
checkClause clauseType clausePats body = do
locals0 <- ask
(localsPats, bodyTy) <- helper clausePats clauseType
(localsPats, (checkedPatterns, bodyType)) <- helper clausePats clauseType
let locals' = locals0 <> localsPats
bodyTy' = substitutionE (localsToSubsE locals') bodyTy
local (const locals') (checkExpression bodyTy' body)
bodyTy' = substitutionE (localsToSubsE locals') bodyType
checkedBody <- local (const locals') (checkExpression bodyTy' body)
return (checkedPatterns, checkedBody)
where
helper :: [PatternArg] -> Expression -> Sem r (LocalVars, Expression)
helper :: [PatternArg] -> Expression -> Sem r (LocalVars, ([PatternArg], Expression))
helper pats ty = runState emptyLocalVars (go pats ty)
go :: [PatternArg] -> Expression -> Sem (State LocalVars ': r) Expression
go :: [PatternArg] -> Expression -> Sem (State LocalVars ': r) ([PatternArg], Expression)
go pats bodyTy = case pats of
[] -> return bodyTy
[] -> return ([], bodyTy)
(p : ps) -> do
bodyTy' <- weakNormalize bodyTy
case bodyTy' of
@ -308,8 +311,8 @@ checkClause clauseType clausePats body = do
_ -> case unfoldFunType bodyTy' of
([], _) -> error "too many patterns"
(par : pars, ret) -> do
checkPattern par p
go ps (foldFunType pars ret)
par' <- checkPattern par p
first (par' :) <$> go ps (foldFunType pars ret)
-- | Refines a hole into a function type. I.e. '_@1' is matched with '_@fresh → _@fresh'
holeRefineToFunction :: (Members '[Inference, NameIdGen] r) => Hole -> Sem r Function
@ -347,10 +350,10 @@ checkPattern ::
(Members '[Reader InfoTable, Error TypeCheckerError, State LocalVars, Inference, NameIdGen, State FunctionsTable] r) =>
FunctionParameter ->
PatternArg ->
Sem r ()
Sem r PatternArg
checkPattern = go
where
go :: FunctionParameter -> PatternArg -> Sem r ()
go :: FunctionParameter -> PatternArg -> Sem r PatternArg
go argTy patArg = do
matchIsImplicit (argTy ^. paramImplicit) patArg
tyVarMap <- fmap (ExpressionIden . IdenVar) . (^. localTyMap) <$> get
@ -358,8 +361,8 @@ checkPattern = go
pat = patArg ^. patternArgPattern
name = patArg ^. patternArgName
whenJust name (\n -> addVar n ty argTy)
case pat of
PatternVariable v -> addVar v ty argTy
pat' <- case pat of
PatternVariable v -> addVar v ty argTy $> pat
PatternConstructorApp a -> do
s <- checkSaturatedInductive ty
info <- lookupConstructor (a ^. constrAppConstructor)
@ -388,7 +391,7 @@ checkPattern = go
(matchTypes patternTy (ExpressionHole hole))
err
let tyArgs = zipExact indParams paramHoles
goConstr a tyArgs
PatternConstructorApp <$> goConstr indName a tyArgs
Right (ind, tyArgs) -> do
when
(ind /= constrIndName)
@ -401,21 +404,24 @@ checkPattern = go
}
)
)
goConstr a tyArgs
PatternConstructorApp <$> goConstr (IdenInductive ind) a tyArgs
return (set patternArgPattern pat' patArg)
where
addVar :: VarName -> Expression -> FunctionParameter -> Sem r ()
addVar v ty argType = do
modify (addType v ty)
registerIden v ty
whenJust (argType ^. paramName) (\v' -> modify (addTypeMapping v' v))
goConstr :: ConstructorApp -> [(InductiveParameter, Expression)] -> Sem r ()
goConstr app@(ConstructorApp c ps) ctx = do
goConstr :: Iden -> ConstructorApp -> [(InductiveParameter, Expression)] -> Sem r ConstructorApp
goConstr inductivename app@(ConstructorApp c ps _) ctx = do
(_, psTys) <- constructorArgTypes <$> lookupConstructor c
let psTys' = map (substituteIndParams ctx) psTys
expectedNum = length psTys
let w = map unnamedParameter psTys'
w = map unnamedParameter psTys'
when (expectedNum /= length ps) (throw (appErr app expectedNum))
zipWithM_ go w ps
pis <- zipWithM go w ps
let appTy = foldExplicitApplication (ExpressionIden inductivename) (map snd ctx)
return app {_constrAppType = Just appTy, _constrAppParameters = pis}
appErr :: ConstructorApp -> Int -> TypeCheckerError
appErr app expected =
ErrArity
@ -555,11 +561,12 @@ inferExpression' hint e = case e of
_caseExpressionType = Just (typedCaseExpression ^. typedType)
_caseExpressionWholeType = Just ty
goBranch :: CaseBranch -> Sem r CaseBranch
goBranch b =
traverseOf
caseBranchExpression
(checkClause funty (pure (b ^. caseBranchPattern)))
b
goBranch b = do
(onePat, _caseBranchExpression) <- checkClause funty [b ^. caseBranchPattern] (b ^. caseBranchExpression)
let _caseBranchPattern = case onePat of
[x] -> x
_ -> impossible
return CaseBranch {..}
where
funty :: Expression
funty = ExpressionFunction (mkFunction (typedCaseExpression ^. typedType) ty)
@ -587,8 +594,8 @@ inferExpression' hint e = case e of
where
goClause :: Expression -> LambdaClause -> Sem r LambdaClause
goClause ty (LambdaClause pats body) = do
body' <- checkClause ty (toList pats) body
return (LambdaClause pats body')
(pats', body') <- checkClause ty (toList pats) body
return (LambdaClause (nonEmpty' pats') body')
goUniverse :: SmallUniverse -> Sem r TypedExpression
goUniverse u =

2
src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
View File

@ -384,7 +384,7 @@ matchPatterns (PatternArg impl1 name1 pat1) (PatternArg impl2 name2 pat2) =
(PatternVariable {}, _) -> err
(_, PatternVariable {}) -> err
goConstructor :: ConstructorApp -> ConstructorApp -> Sem r Bool
goConstructor (ConstructorApp c1 args1) (ConstructorApp c2 args2)
goConstructor (ConstructorApp c1 args1 _) (ConstructorApp c2 args2 _)
| c1 /= c2 = err
| otherwise = case zipExactMay args1 args2 of
Nothing -> err

28
src/Juvix/Compiler/Pipeline.hs
View File

@ -156,17 +156,41 @@ upToCore ::
upToCore =
upToInternalReachability >>= Core.fromInternal
upToAsm ::
(Members '[Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, PathResolver] r) =>
Sem r Asm.InfoTable
upToAsm =
upToCore >>= \Core.CoreResult {..} -> return (coreToAsm _coreResultTable)
upToMiniC ::
(Members '[Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, PathResolver] r) =>
Asm.Options ->
Sem r C.MiniCResult
upToMiniC = upToInternalReachability >>= C.fromInternal
upToMiniC opts =
upToAsm >>= asmToMiniC opts
upToGeb ::
(Members '[Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, PathResolver] r) =>
Geb.ResultSpec ->
Sem r Geb.Result
upToGeb spec =
upToCore >>= \Core.CoreResult {..} -> coreToGeb spec _coreResultTable
upToEval ::
(Members '[Reader EntryPoint, Files, NameIdGen, Error JuvixError, Builtins, PathResolver] r) =>
Sem r Core.CoreResult
upToEval =
upToCore >>= \r -> return r {Core._coreResultTable = Core.toEval (r ^. Core.coreResultTable)}
--------------------------------------------------------------------------------
-- Internal workflows
--------------------------------------------------------------------------------
coreToAsm :: Core.InfoTable -> Asm.InfoTable
coreToAsm = Asm.fromCore . Stripped.fromCore . Core.toStripped
coreToMiniC :: (Member (Error JuvixError) r) => Asm.Options -> Core.InfoTable -> Sem r C.MiniCResult
coreToMiniC opts = asmToMiniC opts . Asm.fromCore . Stripped.fromCore . Core.toStripped
coreToMiniC opts = asmToMiniC opts . coreToAsm
asmToMiniC :: (Member (Error JuvixError) r) => Asm.Options -> Asm.InfoTable -> Sem r C.MiniCResult
asmToMiniC opts = Asm.toReg opts >=> regToMiniC (opts ^. Asm.optLimits) . Reg.fromAsm

15
src/Juvix/Compiler/Pipeline/ExpressionContext.hs
View File

@ -57,11 +57,10 @@ mainModuleScope e = fromJust (moduleScope e (mainModuleTopPath e))
mainModuleTopPath :: ExpressionContext -> C.TopModulePath
mainModuleTopPath = (^. contextScoperResult . Scoper.mainModule . C.modulePath . S.nameConcrete)
transformNode :: InfoTable -> [TransformationId] -> Node -> Node
transformNode tab ts n = snd (run (runInfoTableBuilder tab transformNode'))
where
transformNode' :: Member InfoTableBuilder r => Sem r Node
transformNode' = do
sym <- freshSymbol
registerIdentNode sym n
lookupDefault impossible sym . (^. identContext) . applyTransformations ts <$> getInfoTable
runTransformations :: [TransformationId] -> InfoTable -> Node -> (InfoTable, Node)
runTransformations ts tab n = snd $ run $ runInfoTableBuilder tab $ do
sym <- freshSymbol
registerIdentNode sym n
tab' <- applyTransformations ts <$> getInfoTable
let node' = lookupDefault impossible sym (tab' ^. identContext)
return (tab', node')

5
test/Asm/Compile/Base.hs
View File

@ -3,6 +3,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.Error
import Juvix.Compiler.Asm.Options
import Juvix.Compiler.Asm.Translation.FromSource
import Juvix.Compiler.Backend qualified as Backend
@ -14,7 +15,9 @@ asmCompileAssertion' :: InfoTable -> Path Abs File -> Path Abs File -> (String -
asmCompileAssertion' tab mainFile expectedFile step = do
step "Generate C code"
case run $ runError @JuvixError $ Pipeline.asmToMiniC asmOpts tab of
Left {} -> assertFailure "code generation failed"
Left e -> do
let err :: AsmError = fromJust (fromJuvixError e)
assertFailure ("code generation failed:" <> "\n" <> unpack (err ^. asmErrorMsg))
Right C.MiniCResult {..} ->
withTempDir'
( \dirPath -> do

8
test/BackendC.hs
View File

@ -1,8 +0,0 @@
module BackendC where
import BackendC.Examples qualified as E
import BackendC.Positive qualified as P
import Base
allTests :: TestTree
allTests = testGroup "Backend C tests" [P.allTests, E.allTests]

155
test/BackendC/Base.hs
View File

@ -1,155 +0,0 @@
module BackendC.Base where
import Base
import Data.FileEmbed
import Data.Text.IO qualified as TIO
import Juvix.Compiler.Backend.C.Translation.FromInternal as MiniC
import Juvix.Compiler.Builtins (iniState)
import Juvix.Compiler.Pipeline
import System.Process qualified as P
clangCompile ::
(Path Abs File -> Path Abs File -> [String]) ->
MiniC.MiniCResult ->
(Path Abs File -> IO Text) ->
(String -> IO ()) ->
IO Text
clangCompile mkClangArgs cResult execute step =
withTempDir'
( \dirPath -> do
let cOutputFile = dirPath <//> $(mkRelFile "out.c")
wasmOutputFile = dirPath <//> $(mkRelFile "Input.wasm")
TIO.writeFile (toFilePath cOutputFile) (cResult ^. MiniC.resultCCode)
step "WASM generation"
P.callProcess
"clang"
(mkClangArgs wasmOutputFile cOutputFile)
step "WASM execution"
execute wasmOutputFile
)
wasmClangAssertionCGenOnly :: Path Abs File -> ((String -> IO ()) -> Assertion)
wasmClangAssertionCGenOnly mainFile step = do
step "C Generation"
root <- getCurrentDir
let entryPoint = defaultEntryPoint root mainFile
(void . runIO' iniState entryPoint) upToMiniC
wasmClangAssertion :: WASMInfo -> Path Abs File -> Path Abs File -> ((String -> IO ()) -> Assertion)
wasmClangAssertion WASMInfo {..} mainFile expectedFile step = do
step "Check clang and wasmer are on path"
assertCmdExists $(mkRelFile "clang")
assertCmdExists $(mkRelFile "wasmer")
root <- getCurrentDir
step "C Generation"
let entryPoint = defaultEntryPoint root mainFile
p :: MiniC.MiniCResult <- snd <$> runIO' iniState entryPoint upToMiniC
expected <- TIO.readFile (toFilePath expectedFile)
step "Compile C with wasm standalone runtime"
actualStandalone <- clangCompile standaloneArgs p _wasmInfoActual step
step "Compare expected and actual program output"
assertEqDiffText ("Check: WASM output = " <> toFilePath expectedFile) actualStandalone expected
wasiClangAssertion :: StdlibMode -> Path Abs File -> Path Abs File -> Text -> ((String -> IO ()) -> Assertion)
wasiClangAssertion stdlibMode mainFile expectedFile stdinText step = do
step "Check clang and wasmer are on path"
assertCmdExists $(mkRelFile "clang")
assertCmdExists $(mkRelFile "wasmer")
step "Lookup WASI_SYSROOT_PATH"
sysrootPath <- getWasiSysrootPath
root <- getCurrentDir
step "C Generation"
let entryPoint = (defaultEntryPoint root mainFile) {_entryPointNoStdlib = stdlibMode == StdlibExclude}
p :: MiniC.MiniCResult <- snd <$> runIO' iniState entryPoint upToMiniC
expected <- TIO.readFile (toFilePath expectedFile)
let execute :: Path Abs File -> IO Text
execute outputFile = pack <$> P.readProcess "wasmer" [toFilePath outputFile] (unpack stdinText)
step "Compile C with standalone runtime"
actualStandalone <- clangCompile (wasiStandaloneArgs sysrootPath) p execute step
step "Compare expected and actual program output"
assertEqDiffText ("check: WASM output = " <> toFilePath expectedFile) actualStandalone expected
step "Compile C with libc runtime"
actualLibc <- clangCompile (libcArgs sysrootPath) p execute step
step "Compare expected and actual program output"
assertEqDiffText ("check: WASM output = " <> toFilePath expectedFile) actualLibc expected
builtinRuntime :: Path Abs Dir
builtinRuntime = absDir $(makeRelativeToProject "c-runtime/builtins" >>= strToExp)
standaloneArgs :: Path Abs File -> Path Abs File -> [String]
standaloneArgs wasmOutputFile cOutputFile =
[ "-nodefaultlibs",
"-std=c99",
"-Oz",
"-I",
toFilePath (parent minicRuntime),
"-I",
toFilePath builtinRuntime,
"-Werror",
"--target=wasm32",
"-nostartfiles",
"-Wl,--no-entry",
"-o",
toFilePath wasmOutputFile,
toFilePath wallocPath,
toFilePath cOutputFile
]
where
minicRuntime :: Path Abs File
minicRuntime = absFile $(makeRelativeToProject "c-runtime/standalone/c-runtime.h" >>= strToExp)
wallocPath :: Path Abs File
wallocPath = absFile $(makeRelativeToProject "c-runtime/walloc/walloc.c" >>= strToExp)
wasiStandaloneArgs :: Path Abs Dir -> Path Abs File -> Path Abs File -> [String]
wasiStandaloneArgs sysrootPath wasmOutputFile cOutputFile =
[ "-nodefaultlibs",
"-std=c99",
"-Oz",
"-I",
toFilePath (parent minicRuntime),
"-I",
toFilePath builtinRuntime,
"-Werror",
"--target=wasm32-wasi",
"--sysroot",
toFilePath sysrootPath,
"-o",
toFilePath wasmOutputFile,
toFilePath wallocPath,
toFilePath cOutputFile
]
where
minicRuntime :: Path Abs File
minicRuntime = absFile $(makeRelativeToProject "c-runtime/wasi-standalone/c-runtime.h" >>= strToExp)
wallocPath :: Path Abs File
wallocPath = absFile $(makeRelativeToProject "c-runtime/walloc/walloc.c" >>= strToExp)
libcArgs :: Path Abs Dir -> Path Abs File -> Path Abs File -> [String]
libcArgs sysrootPath wasmOutputFile cOutputFile =
[ "-nodefaultlibs",
"-std=c99",
"-Oz",
"-I",
toFilePath (parent minicRuntime),
"-I",
toFilePath builtinRuntime,
"-Werror",
"-lc",
"--target=wasm32-wasi",
"--sysroot",
toFilePath sysrootPath,
"-o",
toFilePath wasmOutputFile,
toFilePath cOutputFile
]
where
minicRuntime :: Path Abs File
minicRuntime = absFile $(makeRelativeToProject "c-runtime/wasi-libc/c-runtime.h" >>= strToExp)

75
test/BackendC/Examples.hs
View File

@ -1,75 +0,0 @@
module BackendC.Examples where
import BackendC.Base
import Base
import Data.FileEmbed
data ExampleTest
= ExampleExecTest ExecTest
| ExampleCGenOnlyTest TestSpec
data TestSpec = TestSpec
{ _name :: String,
_testDir :: Path Rel Dir,
_mainFile :: Path Rel File
}
data ExecTest = ExecTest
{ _spec :: TestSpec,
_expectedDir :: Path Rel Dir,
_stdinText :: Text,
_compileMode :: CompileMode
}
makeLenses ''ExecTest
makeLenses ''TestSpec
execTest :: String -> Path Rel Dir -> Path Rel File -> Path Rel Dir -> Text -> CompileMode -> ExecTest
execTest _name _testDir _mainFile _expectedDir _stdinText _compileMode = ExecTest {_spec = TestSpec {..}, ..}
exampleRoot :: Path Abs Dir
exampleRoot = absDir $(makeRelativeToProject (toFilePath $(mkRelDir "examples/milestone")) >>= strToExp)
testDescr :: ExampleTest -> TestDescr
testDescr = \case
ExampleExecTest ExecTest {..} ->
let mainRoot = exampleRoot <//> _spec ^. testDir
mainFile' = mainRoot <//> (_spec ^. mainFile)
expectedFile = absDir $(makeRelativeToProject "tests/examplesExpected" >>= strToExp) <//> _expectedDir <//> $(mkRelFile "expected.golden")
in TestDescr
{ _testName = _spec ^. name,
_testRoot = mainRoot,
_testAssertion = case _compileMode of
WASI stdlibMode -> Steps $ wasiClangAssertion stdlibMode mainFile' expectedFile _stdinText
WASM i -> Steps $ wasmClangAssertion i mainFile' expectedFile
}
ExampleCGenOnlyTest TestSpec {..} ->
let mainRoot = exampleRoot <//> _testDir
mainFile' = mainRoot <//> _mainFile
in TestDescr
{ _testName = _name,
_testRoot = mainRoot,
_testAssertion = Steps $ wasmClangAssertionCGenOnly mainFile'
}
allTests :: TestTree
allTests =
testGroup
"Backend C milestone example tests"
(map (mkTest . testDescr) tests)
tests :: [ExampleTest]
tests =
map ExampleExecTest execTests <> map ExampleCGenOnlyTest testSpecs
where
execTests :: [ExecTest]
execTests =
[ execTest "Validity Predicate example" $(mkRelDir "ValidityPredicates") $(mkRelFile "Tests.juvix") $(mkRelDir "ValidityPredicates") "" (WASI StdlibInclude),
execTest "TicTacToe CLI example" $(mkRelDir "TicTacToe") $(mkRelFile "CLI/TicTacToe.juvix") $(mkRelDir "TicTacToe") "aaa\n0\n10\n1\n2\n3\n3\n4\n5\n6\n7\n8\n9\n" (WASI StdlibInclude),
execTest "Fibonacci example" $(mkRelDir "Fibonacci") $(mkRelFile "Fibonacci.juvix") $(mkRelDir "Fibonacci") "" (WASI StdlibInclude),
execTest "Collatz sequence generator" $(mkRelDir "Collatz") $(mkRelFile "Collatz.juvix") $(mkRelDir "Collatz") "123\n" (WASI StdlibInclude),
execTest "Towers of Hanoi" $(mkRelDir "Hanoi") $(mkRelFile "Hanoi.juvix") $(mkRelDir "Hanoi") "" (WASI StdlibInclude),
execTest "Pascal's triangle" $(mkRelDir "PascalsTriangle") $(mkRelFile "PascalsTriangle.juvix") $(mkRelDir "PascalsTriangle") "" (WASI StdlibInclude)
]
testSpecs :: [TestSpec]
testSpecs = [TestSpec "TicTacToe Web example (C gen only)" $(mkRelDir "TicTacToe") $(mkRelFile "Web/TicTacToe.juvix")]

89
test/BackendC/Positive.hs
View File

@ -1,89 +0,0 @@
module BackendC.Positive where
import BackendC.Base
import Base
import System.Process qualified as P
data PosTest = PosTest
{ _name :: String,
_relDir :: Path Rel Dir,
_compileMode :: CompileMode
}
makeLenses ''PosTest
root :: Path Abs Dir
root = relToProject $(mkRelDir "tests/positive/MiniC")
mainFile :: Path Rel File
mainFile = $(mkRelFile "Input.juvix")
expectedFile :: Path Rel File
expectedFile = $(mkRelFile "expected.golden")
actualCallExport :: Text -> [Text] -> Path Abs File -> IO Text
actualCallExport funName funArgs outputFile =
pack
<$> P.readProcess
"wasmer"
(["run", toFilePath outputFile, "--invoke", unpack funName] <> (unpack <$> funArgs))
""
actualCallNode :: Path Rel File -> Path Abs File -> IO Text
actualCallNode jsFile outputFile = do
assertCmdExists $(mkRelFile "node")
let outputDir = parent outputFile
outputJsFile = outputDir <//> jsFile
copyFile jsFile outputJsFile
withCurrentDir
outputDir
( pack
<$> P.readProcess
"node"
[toFilePath outputJsFile]
""
)
testDescr :: PosTest -> TestDescr
testDescr PosTest {..} =
let tRoot = root <//> _relDir
mainFile' = tRoot <//> mainFile
expectedFile' = tRoot <//> expectedFile
in TestDescr
{ _testName = _name,
_testRoot = tRoot,
_testAssertion = Steps $ case _compileMode of
WASI stdlibMode -> wasiClangAssertion stdlibMode mainFile' expectedFile' ""
WASM i -> wasmClangAssertion i mainFile' expectedFile'
}
allTests :: TestTree
allTests =
testGroup
"Backend C positive tests"
(map (mkTest . testDescr) tests)
tests :: [PosTest]
tests =
[ PosTest "HelloWorld" $(mkRelDir "HelloWorld") (WASI StdlibExclude),
PosTest "Inductive types and pattern matching" $(mkRelDir "Nat") (WASI StdlibExclude),
PosTest "Polymorphic types" $(mkRelDir "Polymorphism") (WASI StdlibExclude),
PosTest "Polymorphic axioms" $(mkRelDir "PolymorphicAxioms") (WASI StdlibExclude),
PosTest "Polymorphic target" $(mkRelDir "PolymorphicTarget") (WASI StdlibExclude),
PosTest "Multiple modules" $(mkRelDir "MultiModules") (WASI StdlibExclude),
PosTest "Higher Order Functions" $(mkRelDir "HigherOrder") (WASI StdlibExclude),
PosTest "Higher Order Functions and explicit holes" $(mkRelDir "PolymorphismHoles") (WASI StdlibExclude),
PosTest "Closures with no environment" $(mkRelDir "ClosureNoEnv") (WASI StdlibExclude),
PosTest "Closures with environment" $(mkRelDir "ClosureEnv") (WASI StdlibExclude),
PosTest "SimpleFungibleTokenImplicit" $(mkRelDir "SimpleFungibleTokenImplicit") (WASI StdlibExclude),
PosTest "Mutually recursive function" $(mkRelDir "MutuallyRecursive") (WASI StdlibExclude),
PosTest "Nested List type" $(mkRelDir "NestedList") (WASI StdlibExclude),
PosTest "Builtin types and functions" $(mkRelDir "Builtins") (WASI StdlibExclude),
PosTest "Builtin types and functions from stdlib" $(mkRelDir "BuiltinsStdlib") (WASI StdlibInclude),
PosTest "Import from embedded standard library" $(mkRelDir "StdlibImport") (WASI StdlibInclude),
PosTest "Axiom without a compile block" $(mkRelDir "AxiomNoCompile") (WASI StdlibInclude),
PosTest "Invoke a function using exported name" $(mkRelDir "ExportName") (WASM (WASMInfo (actualCallExport "fun" []))),
PosTest "Invoke a function using exported name with args" $(mkRelDir "ExportNameArgs") (WASM (WASMInfo (actualCallExport "fun" ["0"]))),
PosTest "Invoke an imported function in Juvix and exported function in JS" $(mkRelDir "ImportExportName") (WASM (WASMInfo (actualCallNode $(mkRelFile "input.js")))),
PosTest "Invoke an exported function using Anoma _validate_tx signature" $(mkRelDir "AlwaysValidVP") (WASM (WASMInfo (actualCallNode $(mkRelFile "input.js"))))
]

2
test/BackendGeb/Eval/Base.hs
View File

@ -16,7 +16,7 @@ gebEvalAssertion mainFile expectedFile step = do
case Geb.runParser mainFile input of
Left err -> assertFailure (show (pretty err))
Right (Geb.ExpressionObject _) -> do
step "No evalution for objects"
step "No evaluation for objects"
assertFailure (unpack Geb.objNoEvalMsg)
Right (Geb.ExpressionMorphism gebMorphism) ->
gebEvalAssertion' mainFile expectedFile step gebMorphism

40
test/Compilation/Base.hs
View File

@ -1,50 +1,24 @@
module Compilation.Base where
import Base
import Core.Compile.Base
import Core.Eval.Base
import Data.HashMap.Strict qualified as HashMap
import Data.Text.IO qualified as TIO
import Juvix.Compiler.Builtins (iniState)
import Juvix.Compiler.Core.Data.InfoTable qualified as Core
import Juvix.Compiler.Core.Extra
import Juvix.Compiler.Core.Info qualified as Info
import Juvix.Compiler.Core.Info.NoDisplayInfo
import Juvix.Compiler.Core.Pipeline qualified as Core
import Juvix.Compiler.Core.Pretty
import Juvix.Compiler.Core.Translation.FromInternal.Data qualified as Core
import Juvix.Compiler.Pipeline
compileAssertion ::
Bool ->
Path Abs File ->
Path Abs File ->
(String -> IO ()) ->
Assertion
compileAssertion mainFile expectedFile step = do
compileAssertion onlyEval mainFile expectedFile step = do
step "Translate to JuvixCore"
cwd <- getCurrentDir
let entryPoint = defaultEntryPoint cwd mainFile
tab' <- (^. Core.coreResultTable) . snd <$> runIO' iniState entryPoint upToCore
let tab = Core.toEval tab'
case (tab ^. Core.infoMain) >>= ((tab ^. Core.identContext) HashMap.!?) of
Just node -> do
withTempDir'
( \dirPath -> do
let outputFile = dirPath <//> $(mkRelFile "out.out")
hout <- openFile (toFilePath outputFile) WriteMode
step "Evaluate"
r' <- doEval mainFile hout tab node
case r' of
Left err -> do
hClose hout
assertFailure (show (pretty err))
Right value -> do
unless
(Info.member kNoDisplayInfo (getInfo value))
(hPutStrLn hout (ppPrint value))
hClose hout
actualOutput <- TIO.readFile (toFilePath outputFile)
step "Compare expected and actual program output"
expected <- TIO.readFile (toFilePath expectedFile)
assertEqDiffText ("Check: EVAL output = " <> toFilePath expectedFile) actualOutput expected
)
Nothing -> assertFailure ("No main function registered in: " <> toFilePath mainFile)
tab <- (^. Core.coreResultTable) . snd <$> runIO' iniState entryPoint upToCore
coreEvalAssertion' (Core.toEval tab) mainFile expectedFile step
unless onlyEval $
coreCompileAssertion' tab mainFile expectedFile step

28
test/Compilation/Positive.hs
View File

@ -7,6 +7,7 @@ data PosTest = PosTest
{ _name :: String,
_dir :: Path Abs Dir,
_file :: Path Abs File,
_onlyEval :: Bool,
_expectedFile :: Path Abs File
}
@ -26,32 +27,29 @@ toTestDescr PosTest {..} =
in TestDescr
{ _testName = _name,
_testRoot = tRoot,
_testAssertion = Steps $ compileAssertion file' expected'
_testAssertion = Steps $ compileAssertion _onlyEval file' expected'
}
filterOutTests :: [String] -> [PosTest] -> [PosTest]
filterOutTests out = filter (\PosTest {..} -> _name `notElem` out)
allTests :: TestTree
allTests =
testGroup
"Juvix compilation pipeline positive tests"
( map
(mkTest . toTestDescr)
( filterOutTests
[ "Nested binders with variable capture"
]
tests
)
)
(map (mkTest . toTestDescr) tests)
posTest :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest
posTest _name rdir rfile routfile =
posTest' :: Bool -> String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest
posTest' _onlyEval _name rdir rfile routfile =
let _dir = root <//> rdir
_file = _dir <//> rfile
_expectedFile = root <//> routfile
in PosTest {..}
posTest :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest
posTest = posTest' False
-- tests which use large integers are only evaluated but not compiled
posTestEval :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest
posTestEval = posTest' True
tests :: [PosTest]
tests =
[ posTest
@ -104,7 +102,7 @@ tests =
$(mkRelDir ".")
$(mkRelFile "test010.juvix")
$(mkRelFile "out/test010.out"),
posTest
posTestEval
"Tail recursion: Fibonacci numbers in linear time"
$(mkRelDir ".")
$(mkRelFile "test011.juvix")

4
test/Core/Asm/Positive.hs
View File

@ -8,9 +8,7 @@ allTests :: TestTree
allTests = testGroup "JuvixCore to JuvixAsm positive tests" (map liftTest (Eval.filterOutTests ignoredTests Eval.tests))
ignoredTests :: [String]
ignoredTests =
[ "Match with complex patterns"
]
ignoredTests = []
liftTest :: Eval.PosTest -> TestTree
liftTest _testEval =

5
test/Core/Compile/Base.hs
View File

@ -5,6 +5,8 @@ import Base
import Core.Eval.Base
import Core.Eval.Positive qualified as Eval
import Data.Text.IO qualified as TIO
import GHC.Base (seq)
import Juvix.Compiler.Asm.Pretty qualified as Asm
import Juvix.Compiler.Asm.Translation.FromCore qualified as Asm
import Juvix.Compiler.Core.Pipeline
import Juvix.Compiler.Core.Translation.FromSource
@ -42,7 +44,8 @@ coreCompileAssertion' ::
coreCompileAssertion' tab mainFile expectedFile step = do
step "Translate to JuvixAsm"
let tab' = Asm.fromCore $ Stripped.fromCore $ toStripped tab
Asm.asmCompileAssertion' tab' mainFile expectedFile step
length (fromText (Asm.ppPrint tab' tab') :: String) `seq`
Asm.asmCompileAssertion' tab' mainFile expectedFile step
coreCompileAssertion ::
Path Abs File ->

5
test/Core/Compile/Positive.hs
View File

@ -7,7 +7,7 @@ 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
-- Arbitrary precision integers not yet supported
ignoredTests :: [String]
ignoredTests =
[ "Tail recursion: Fibonacci numbers in linear time",
@ -15,8 +15,7 @@ ignoredTests =
"Nested 'case', 'let' and 'if' with variable capture",
"Mutual recursion",
"LetRec",
"Big numbers",
"Match with complex patterns"
"Big numbers"
]
liftTest :: Eval.PosTest -> TestTree

56
test/Core/Eval/Base.hs
View File

@ -1,7 +1,9 @@
module Core.Eval.Base where
import Base
import Data.HashMap.Strict qualified as HashMap
import Data.Text.IO qualified as TIO
import GHC.Base (seq)
import Juvix.Compiler.Core.Data.InfoTable
import Juvix.Compiler.Core.Error
import Juvix.Compiler.Core.Evaluator
@ -13,6 +15,38 @@ import Juvix.Compiler.Core.Pretty
import Juvix.Compiler.Core.Transformation
import Juvix.Compiler.Core.Translation.FromSource
coreEvalAssertion' ::
InfoTable ->
Path Abs File ->
Path Abs File ->
(String -> IO ()) ->
Assertion
coreEvalAssertion' tab mainFile expectedFile step =
length (fromText (ppPrint tab) :: String) `seq`
case (tab ^. infoMain) >>= ((tab ^. identContext) HashMap.!?) of
Just node -> do
withTempDir'
( \dirPath -> do
let outputFile = dirPath <//> $(mkRelFile "out.out")
hout <- openFile (toFilePath outputFile) WriteMode
step "Evaluate"
r' <- doEval mainFile hout tab node
case r' of
Left err -> do
hClose hout
assertFailure (show (pretty err))
Right value -> do
unless
(Info.member kNoDisplayInfo (getInfo value))
(hPutStrLn hout (ppPrint value))
hClose hout
actualOutput <- TIO.readFile (toFilePath outputFile)
step "Compare expected and actual program output"
expected <- TIO.readFile (toFilePath expectedFile)
assertEqDiffText ("Check: EVAL output = " <> toFilePath expectedFile) actualOutput expected
)
Nothing -> assertFailure ("No main function registered in: " <> toFilePath mainFile)
coreEvalAssertion ::
Path Abs File ->
Path Abs File ->
@ -32,27 +66,7 @@ coreEvalAssertion mainFile expectedFile trans testTrans step = do
Right (tabIni, Just node) -> do
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'
case r' of
Left err -> do
hClose hout
assertFailure (show (pretty err))
Right value -> do
unless
(Info.member kNoDisplayInfo (getInfo value))
(hPutStrLn hout (ppPrint value))
hClose hout
actualOutput <- TIO.readFile (toFilePath outputFile)
step "Compare expected and actual program output"
expected <- TIO.readFile (toFilePath expectedFile)
assertEqDiffText ("Check: EVAL output = " <> toFilePath expectedFile) actualOutput expected
)
coreEvalAssertion' tab mainFile expectedFile step
coreEvalErrorAssertion :: Path Abs File -> (String -> IO ()) -> Assertion
coreEvalErrorAssertion mainFile step = do

54
test/Core/Eval/Positive.hs
View File

@ -10,6 +10,8 @@ data PosTest = PosTest
_expectedFile :: Path Rel File
}
makeLenses ''PosTest
root :: Path Abs Dir
root = relToProject $(mkRelDir "tests/Core/positive")
@ -274,5 +276,55 @@ tests =
"String builtins"
$(mkRelDir ".")
$(mkRelFile "test048.jvc")
$(mkRelFile "out/test048.out")
$(mkRelFile "out/test048.out"),
PosTest
"Lifting and polymorphism"
$(mkRelDir ".")
$(mkRelFile "test049.jvc")
$(mkRelFile "out/test049.out"),
PosTest
"Church numerals with pattern matching"
$(mkRelDir ".")
$(mkRelFile "test050.jvc")
$(mkRelFile "out/test050.out"),
PosTest
"Type annotations for patterns"
$(mkRelDir ".")
$(mkRelFile "test051.jvc")
$(mkRelFile "out/test051.out"),
PosTest
"foldl with match"
$(mkRelDir ".")
$(mkRelFile "test052.jvc")
$(mkRelFile "out/test052.out"),
PosTest
"Match with higher-order polymorphic functions"
$(mkRelDir ".")
$(mkRelFile "test053.jvc")
$(mkRelFile "out/test053.out"),
PosTest
"Typed match"
$(mkRelDir ".")
$(mkRelFile "test054.jvc")
$(mkRelFile "out/test054.out"),
PosTest
"Eta-expansion of polymorphic constructors"
$(mkRelDir ".")
$(mkRelFile "test055.jvc")
$(mkRelFile "out/test055.out"),
PosTest
"LetRec with type annotations"
$(mkRelDir ".")
$(mkRelFile "test056.jvc")
$(mkRelFile "out/test056.out"),
PosTest
"Type synonyms"
$(mkRelDir ".")
$(mkRelFile "test057.jvc")
$(mkRelFile "out/test057.out"),
PosTest
"Lifting and partial application"
$(mkRelDir ".")
$(mkRelFile "test058.jvc")
$(mkRelFile "out/test058.out")
]

1
test/Core/Transformation/Pipeline.hs
View File

@ -3,7 +3,6 @@ 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

4
test/Internal/Eval/Base.hs
View File

@ -10,6 +10,7 @@ import Juvix.Compiler.Core.Extra
import Juvix.Compiler.Core.Info qualified as Info
import Juvix.Compiler.Core.Info.NoDisplayInfo
import Juvix.Compiler.Core.Pretty
import Juvix.Compiler.Core.Transformation (etaExpansionApps)
import Juvix.Compiler.Core.Translation.FromInternal.Data as Core
import Juvix.Compiler.Pipeline
@ -18,7 +19,8 @@ internalCoreAssertion mainFile expectedFile step = do
step "Translate to Core"
cwd <- getCurrentDir
let entryPoint = defaultEntryPoint cwd mainFile
tab <- (^. Core.coreResultTable) . snd <$> runIO' iniState entryPoint upToCore
tab0 <- (^. Core.coreResultTable) . snd <$> runIO' iniState entryPoint upToCore
let tab = etaExpansionApps tab0
case (tab ^. infoMain) >>= ((tab ^. identContext) HashMap.!?) of
Just node -> do
withTempDir'

4
test/Main.hs
View File

@ -2,7 +2,6 @@ module Main (main) where
import Arity qualified
import Asm qualified
import BackendC qualified
import BackendGeb qualified
import Base
import Compilation qualified
@ -20,8 +19,7 @@ slowTests :: TestTree
slowTests =
testGroup
"Juvix slow tests"
[ BackendC.allTests,
BackendGeb.allTests,
[ BackendGeb.allTests,
Runtime.allTests,
Asm.allTests,
Core.allTests,

2
tests/Asm/negative/vtest010.jva
View File

@ -1,6 +1,6 @@
-- Value stack type mismatch
function id(*) {
function id(integer) : integer {
push arg[0];
ret;
}

12
tests/Compilation/positive/out/test035.out
View File

@ -1,9 +1,9 @@
9 :: 7 :: 5 :: 3 :: 1 :: nil
20300
1380938444160
328376729742336
635244975397025280
10896523177832686508800
209585186558797617308313141313536
300
4160
2336
5280
8800
13536
1
0

2
tests/Compilation/positive/test005.juvix
View File

@ -13,6 +13,6 @@ I : {A : Type} → A → A;
I := S K (K {_} {Bool});
main : IO;
main := printNatLn $ I 1 + I I 1 + I (I 1) + I I I 1 + I (I I) I (I I I) 1 + I I I (I I I (I I)) I (I I) I I I 1;
main := printNatLn (I 1 + I I 1 + I (I 1) + I I I 1 + I (I I) I (I I I) 1 + I I I (I I I (I I)) I (I I) I I I 1);
end;

4
tests/Compilation/positive/test030.juvix
View File

@ -4,7 +4,9 @@ module test030;
open import Stdlib.Prelude;
iterate : {A : Type} → (A → A) → Nat → A → A;
iterate f zero x := x;
-- clauses with differing number of patterns not yet supported
-- iterate f zero x := x;
iterate f zero := id;
iterate f (suc n) := f ∘ (iterate f n);
plus : Nat → Nat → Nat;

6
tests/Compilation/positive/test035.juvix
View File

@ -28,9 +28,9 @@ f leaf := 1;
f (node l r) :=
case g l, g r
| (leaf, leaf) := 3
| (node l r, leaf) := (f l + f r) * 2
| (node l1 r1, node l2 r2) := (f l1 + f r1) * (f l2 + f r2)
| (_, node l r) := f l + f r;
| (node l r, leaf) := mod ((f l + f r) * 2) 20000
| (node l1 r1, node l2 r2) := mod ((f l1 + f r1) * (f l2 + f r2)) 20000
| (_, node l r) := mod (f l + f r) 20000;
g leaf := leaf;
g (node (node _ _) r) := r;

2
tests/Compilation/positive/test036.juvix
View File

@ -1,7 +1,7 @@
-- eta-expansion
module test036;
open import Stdlib.Prelude public;
open import Stdlib.Prelude;
expand : {A : Type} → A → Nat → A;
expand f x := f;

10
tests/Core/positive/out/test041.out
View File

@ -1,7 +1,7 @@
cons 9 (cons 7 (cons 5 (cons 3 (cons 1 nil))))
-12096
-1448007509520
5510602057585725
-85667472308246220
527851146861989286336
-441596546382859135501706333021475
10480
5725
13780
-13664
18525

1
tests/Core/positive/out/test049.out Normal file
View File

@ -0,0 +1 @@
1

1
tests/Core/positive/out/test050.out Normal file
View File

@ -0,0 +1 @@
3

1
tests/Core/positive/out/test051.out Normal file
View File

@ -0,0 +1 @@
1

1
tests/Core/positive/out/test052.out Normal file
View File

@ -0,0 +1 @@
6

1
tests/Core/positive/out/test053.out Normal file
View File

@ -0,0 +1 @@
35

7
tests/Core/positive/out/test054.out Normal file
View File

@ -0,0 +1,7 @@
25
-12096
10480
5725
13780
-13664
18525

1
tests/Core/positive/out/test055.out Normal file
View File

@ -0,0 +1 @@
1

1
tests/Core/positive/out/test056.out Normal file
View File

@ -0,0 +1 @@
4

Some files were not shown because too many files have changed in this diff Show More