mirror of
https://github.com/anoma/juvix.git
synced 2024-08-17 04:01:05 +03:00
Remove Geb backend (#2886)
* Closes https://github.com/anoma/juvix/issues/2840
This commit is contained in:
parent
ea359adba4
commit
40f5be4d7f
@ -7,7 +7,6 @@ where
|
||||
import Commands.Base
|
||||
import Commands.Compile.Anoma qualified as Anoma
|
||||
import Commands.Compile.Cairo qualified as Cairo
|
||||
import Commands.Compile.Geb qualified as Geb
|
||||
import Commands.Compile.Native qualified as Native
|
||||
import Commands.Compile.Options
|
||||
import Commands.Compile.RiscZeroRust qualified as RiscZeroRust
|
||||
@ -18,7 +17,6 @@ runCommand :: (Members '[EmbedIO, App, TaggedLock] r) => CompileCommand -> Sem r
|
||||
runCommand = \case
|
||||
Native opts -> Native.runCommand opts
|
||||
Wasi opts -> Wasi.runCommand opts
|
||||
Geb opts -> Geb.runCommand opts
|
||||
Anoma opts -> Anoma.runCommand opts
|
||||
Cairo opts -> Cairo.runCommand opts
|
||||
Vampir opts -> Vampir.runCommand opts
|
||||
|
@ -1,37 +0,0 @@
|
||||
module Commands.Compile.Geb where
|
||||
|
||||
import Commands.Base
|
||||
import Commands.Compile.Geb.Options
|
||||
import Commands.Extra.NewCompile
|
||||
import Juvix.Compiler.Backend.Geb qualified as Geb
|
||||
import System.FilePath (takeBaseName)
|
||||
|
||||
runCommand :: (Members '[App, TaggedLock, EmbedIO] r) => GebOptions 'InputMain -> Sem r ()
|
||||
runCommand opts = do
|
||||
let opts' = opts ^. gebCompileCommonOptions
|
||||
inputFile = opts' ^. compileInputFile
|
||||
moutputFile = opts' ^. compileOutputFile
|
||||
coreRes <- fromCompileCommonOptionsMain opts' >>= compileToCore
|
||||
entryPoint <-
|
||||
applyOptions opts
|
||||
<$> getEntryPoint (opts' ^. compileInputFile)
|
||||
let ext :: FileExt
|
||||
ext
|
||||
| opts ^. gebOnlyTerm = FileExtJuvixGeb
|
||||
| otherwise = FileExtLisp
|
||||
gebFile :: Path Abs File <- getOutputFile ext inputFile moutputFile
|
||||
let spec
|
||||
| opts ^. gebOnlyTerm = Geb.OnlyTerm
|
||||
| otherwise =
|
||||
Geb.LispPackage
|
||||
Geb.LispPackageSpec
|
||||
{ _lispPackageName = fromString . takeBaseName $ toFilePath gebFile,
|
||||
_lispPackageEntry = "*entry*"
|
||||
}
|
||||
Geb.Result {..} <-
|
||||
getRight
|
||||
. run
|
||||
. runReader entryPoint
|
||||
. runError @JuvixError
|
||||
$ coreToGeb spec (coreRes ^. coreResultModule)
|
||||
writeFileEnsureLn gebFile _resultCode
|
@ -1,35 +0,0 @@
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
module Commands.Compile.Geb.Options
|
||||
( module Commands.Compile.Geb.Options,
|
||||
module Commands.Compile.CommonOptions,
|
||||
)
|
||||
where
|
||||
|
||||
import Commands.Compile.CommonOptions
|
||||
import CommonOptions
|
||||
|
||||
data GebOptions (k :: InputKind) = GebOptions
|
||||
{ _gebCompileCommonOptions :: CompileCommonOptions k,
|
||||
_gebOnlyTerm :: Bool
|
||||
}
|
||||
|
||||
deriving stock instance (Typeable k, Data (InputFileType k)) => Data (GebOptions k)
|
||||
|
||||
makeLenses ''GebOptions
|
||||
|
||||
parseGeb :: (SingI k) => Parser (GebOptions k)
|
||||
parseGeb = do
|
||||
_gebCompileCommonOptions <- parseCompileCommonOptions
|
||||
_gebOnlyTerm <-
|
||||
switch
|
||||
( short 'G' -- TODO I would like to deprecate the short flag
|
||||
<> long "only-term"
|
||||
<> help "Produce term output only"
|
||||
)
|
||||
pure GebOptions {..}
|
||||
|
||||
instance EntryPointOptions (GebOptions k) where
|
||||
applyOptions opts =
|
||||
set entryPointTarget (Just TargetGeb)
|
||||
. applyOptions (opts ^. gebCompileCommonOptions)
|
@ -5,7 +5,6 @@ where
|
||||
|
||||
import Commands.Compile.Anoma.Options
|
||||
import Commands.Compile.Cairo.Options
|
||||
import Commands.Compile.Geb.Options
|
||||
import Commands.Compile.Native.Options
|
||||
import Commands.Compile.RiscZeroRust.Options
|
||||
import Commands.Compile.Vampir.Options
|
||||
@ -16,7 +15,6 @@ import CommonOptions
|
||||
data CompileCommand
|
||||
= Native (NativeOptions 'InputMain)
|
||||
| Wasi (WasiOptions 'InputMain)
|
||||
| Geb (GebOptions 'InputMain)
|
||||
| Vampir (VampirOptions 'InputMain)
|
||||
| Anoma (AnomaOptions 'InputMain)
|
||||
| Cairo (CairoOptions 'InputMain)
|
||||
@ -31,7 +29,6 @@ supportedTargets =
|
||||
[ (AppTargetVampIR, Vampir <$> parseVampir),
|
||||
(AppTargetAnoma, Anoma <$> parseAnoma),
|
||||
(AppTargetCairo, Cairo <$> parseCairo),
|
||||
(AppTargetGeb, Geb <$> parseGeb),
|
||||
(AppTargetWasm32Wasi, Wasi <$> parseWasi),
|
||||
(AppTargetNative64, Native <$> parseNative),
|
||||
(AppTargetRiscZeroRust, RiscZeroRust <$> parseRiscZeroRust)
|
||||
|
@ -10,7 +10,6 @@ import Commands.Dev.Casm qualified as Casm
|
||||
import Commands.Dev.Core qualified as Core
|
||||
import Commands.Dev.DevCompile qualified as DevCompile
|
||||
import Commands.Dev.DisplayRoot qualified as DisplayRoot
|
||||
import Commands.Dev.Geb qualified as Geb
|
||||
import Commands.Dev.Highlight qualified as Highlight
|
||||
import Commands.Dev.ImportTree qualified as ImportTree
|
||||
import Commands.Dev.Internal qualified as Internal
|
||||
@ -35,7 +34,6 @@ runCommand = \case
|
||||
Internal opts -> Internal.runCommand opts
|
||||
Termination opts -> Termination.runCommand opts
|
||||
Core opts -> Core.runCommand opts
|
||||
Geb opts -> Geb.runCommand opts
|
||||
Asm opts -> Asm.runCommand opts
|
||||
Reg opts -> Reg.runCommand opts
|
||||
Tree opts -> Tree.runCommand opts
|
||||
|
@ -82,7 +82,6 @@ runCommand opts = do
|
||||
AppTargetRiscZeroRust -> err "RISC0 Rust"
|
||||
AppTargetAnoma -> err "Anoma"
|
||||
AppTargetTree -> err "JuvixTree"
|
||||
AppTargetGeb -> err "GEB"
|
||||
AppTargetVampIR -> err "VampIR"
|
||||
AppTargetCore -> err "JuvixCore"
|
||||
AppTargetAsm -> err "JuvixAsm"
|
||||
|
@ -49,7 +49,6 @@ runCommand opts = do
|
||||
AppTargetReg -> err "JuvixReg"
|
||||
AppTargetAnoma -> err "Anoma"
|
||||
AppTargetTree -> err "JuvixTree"
|
||||
AppTargetGeb -> err "GEB"
|
||||
AppTargetVampIR -> err "VampIR"
|
||||
AppTargetCore -> err "JuvixCore"
|
||||
AppTargetAsm -> err "JuvixAsm"
|
||||
|
@ -19,7 +19,6 @@ runCommand opts = do
|
||||
case opts ^. compileTarget of
|
||||
AppTargetWasm32Wasi -> runCPipeline arg
|
||||
AppTargetNative64 -> runCPipeline arg
|
||||
AppTargetGeb -> runGebPipeline arg
|
||||
AppTargetVampIR -> runVampIRPipeline arg
|
||||
AppTargetCore -> return ()
|
||||
AppTargetAsm -> runAsmPipeline arg
|
||||
|
@ -8,7 +8,6 @@ import Data.Aeson qualified as JSON
|
||||
import Juvix.Compiler.Asm.Pretty qualified as Asm
|
||||
import Juvix.Compiler.Backend qualified as Backend
|
||||
import Juvix.Compiler.Backend.C qualified as C
|
||||
import Juvix.Compiler.Backend.Geb qualified as Geb
|
||||
import Juvix.Compiler.Backend.Rust.Data.Result qualified as Rust
|
||||
import Juvix.Compiler.Backend.VampIR.Translation qualified as VampIR
|
||||
import Juvix.Compiler.Casm.Data.Result qualified as Casm
|
||||
@ -18,7 +17,6 @@ import Juvix.Compiler.Core.Data.TransformationId qualified as Core
|
||||
import Juvix.Compiler.Reg.Pretty qualified as Reg
|
||||
import Juvix.Compiler.Tree.Pretty qualified as Tree
|
||||
import Juvix.Prelude.Pretty
|
||||
import System.FilePath (takeBaseName)
|
||||
|
||||
data PipelineArg = PipelineArg
|
||||
{ _pipelineArgOptions :: CompileOptions,
|
||||
@ -41,7 +39,6 @@ getEntry PipelineArg {..} = do
|
||||
getTarget = \case
|
||||
AppTargetWasm32Wasi -> Backend.TargetCWasm32Wasi
|
||||
AppTargetNative64 -> Backend.TargetCNative64
|
||||
AppTargetGeb -> Backend.TargetGeb
|
||||
AppTargetVampIR -> Backend.TargetVampIR
|
||||
AppTargetCore -> Backend.TargetCore
|
||||
AppTargetAsm -> Backend.TargetAsm
|
||||
@ -86,30 +83,6 @@ runCPipeline pa@PipelineArg {..} = do
|
||||
ensureDir buildDir
|
||||
return (buildDir <//> replaceExtension' ".c" (filename inputFileCompile))
|
||||
|
||||
runGebPipeline ::
|
||||
forall r.
|
||||
(Members '[EmbedIO, App, TaggedLock] r) =>
|
||||
PipelineArg ->
|
||||
Sem r ()
|
||||
runGebPipeline pa@PipelineArg {..} = do
|
||||
entryPoint <- getEntry pa
|
||||
gebFile <- Compile.outputFile _pipelineArgOptions
|
||||
let spec
|
||||
| _pipelineArgOptions ^. compileTerm = Geb.OnlyTerm
|
||||
| otherwise =
|
||||
Geb.LispPackage
|
||||
Geb.LispPackageSpec
|
||||
{ _lispPackageName = fromString . takeBaseName $ toFilePath gebFile,
|
||||
_lispPackageEntry = "*entry*"
|
||||
}
|
||||
Geb.Result {..} <-
|
||||
getRight
|
||||
. run
|
||||
. runReader entryPoint
|
||||
. runError @JuvixError
|
||||
$ coreToGeb spec _pipelineArgModule
|
||||
writeFileEnsureLn gebFile _resultCode
|
||||
|
||||
runVampIRPipeline ::
|
||||
forall r.
|
||||
(Members '[EmbedIO, App, TaggedLock] r) =>
|
||||
|
@ -15,7 +15,6 @@ coreSupportedTargets =
|
||||
NonEmpty.fromList
|
||||
[ AppTargetNative64,
|
||||
AppTargetWasm32Wasi,
|
||||
AppTargetGeb,
|
||||
AppTargetVampIR,
|
||||
AppTargetTree,
|
||||
AppTargetAsm,
|
||||
|
@ -105,4 +105,4 @@ parseCoreCommand =
|
||||
compileInfo =
|
||||
info
|
||||
(CoreCompile <$> parseCoreCompileOptions)
|
||||
(progDesc "Compile a JuvixCore file to native code, WebAssembly, GEB or VampIR")
|
||||
(progDesc "Compile a JuvixCore file to native code, WebAssembly, or VampIR")
|
||||
|
@ -1,21 +0,0 @@
|
||||
module Commands.Dev.Geb
|
||||
( module Commands.Dev.Geb,
|
||||
module Commands.Dev.Geb.Options,
|
||||
)
|
||||
where
|
||||
|
||||
import Commands.Base
|
||||
import Commands.Dev.Geb.Check as Infer
|
||||
import Commands.Dev.Geb.Eval as Eval
|
||||
import Commands.Dev.Geb.Infer as Check
|
||||
import Commands.Dev.Geb.Options
|
||||
import Commands.Dev.Geb.Read as Read
|
||||
import Commands.Dev.Geb.Repl as Repl
|
||||
|
||||
runCommand :: forall r. (Members '[EmbedIO, App] r) => GebCommand -> Sem r ()
|
||||
runCommand = \case
|
||||
GebCommandRepl opts -> Repl.runCommand opts
|
||||
GebCommandEval opts -> Eval.runCommand opts
|
||||
GebCommandRead opts -> Read.runCommand opts
|
||||
GebCommandInfer opts -> Infer.runCommand opts
|
||||
GebCommandCheck opts -> Check.runCommand opts
|
@ -1,26 +0,0 @@
|
||||
module Commands.Dev.Geb.Check where
|
||||
|
||||
import Commands.Base
|
||||
import Commands.Dev.Geb.Infer.Options
|
||||
import Juvix.Compiler.Backend.Geb qualified as Geb
|
||||
import Juvix.Compiler.Backend.Geb.Pretty
|
||||
|
||||
runCommand ::
|
||||
forall r.
|
||||
(Member App r, Member EmbedIO r) =>
|
||||
GebInferOptions ->
|
||||
Sem r ()
|
||||
runCommand opts = do
|
||||
let b :: AppPath File
|
||||
b = opts ^. gebInferOptionsInputFile
|
||||
f :: Path Abs File <- fromAppPathFile b
|
||||
content :: Text <- readFile f
|
||||
case Geb.runParser f content of
|
||||
Right (Geb.ExpressionMorphism morph) -> do
|
||||
case Geb.inferObject' morph of
|
||||
Left err -> exitJuvixError (JuvixError err)
|
||||
Right ty -> do
|
||||
renderStdOut (ppOutDefault ty)
|
||||
putStrLn ""
|
||||
Right _ -> exitJuvixError (error @JuvixError "Not a morphism")
|
||||
Left err -> exitJuvixError (JuvixError err)
|
@ -1,58 +0,0 @@
|
||||
module Commands.Dev.Geb.Eval where
|
||||
|
||||
import Commands.Base
|
||||
import Commands.Dev.Geb.Eval.Options
|
||||
import Juvix.Compiler.Backend.Geb.Evaluator qualified as Geb
|
||||
import Juvix.Compiler.Backend.Geb.Language qualified as Geb
|
||||
import Juvix.Compiler.Backend.Geb.Pretty qualified as Geb
|
||||
import Juvix.Compiler.Backend.Geb.Translation.FromSource qualified as Geb
|
||||
|
||||
runCommand ::
|
||||
forall r a.
|
||||
( Members '[App, EmbedIO] r,
|
||||
CanonicalProjection a Geb.EvaluatorOptions,
|
||||
CanonicalProjection a GebEvalOptions
|
||||
) =>
|
||||
a ->
|
||||
Sem r ()
|
||||
runCommand opts = do
|
||||
let b :: AppPath File
|
||||
b = project opts ^. gebEvalOptionsInputFile
|
||||
f :: Path Abs File <- fromAppPathFile b
|
||||
content :: Text <- readFile f
|
||||
case Geb.runParser f content of
|
||||
Left err -> exitJuvixError (JuvixError err)
|
||||
Right gebTerm -> do
|
||||
evalAndPrint opts gebTerm
|
||||
putStrLn ""
|
||||
|
||||
evalAndPrint ::
|
||||
forall r a.
|
||||
( Members '[App, EmbedIO] r,
|
||||
CanonicalProjection a Geb.EvaluatorOptions
|
||||
) =>
|
||||
a ->
|
||||
Geb.Expression ->
|
||||
Sem r ()
|
||||
evalAndPrint opts = \case
|
||||
Geb.ExpressionObject _ -> error Geb.objNoEvalMsg
|
||||
Geb.ExpressionMorphism morphism -> do
|
||||
let opts' :: Geb.EvaluatorOptions = project opts
|
||||
let env :: Geb.Env =
|
||||
Geb.Env
|
||||
{ _envEvaluatorOptions = opts',
|
||||
_envContext = mempty
|
||||
}
|
||||
if
|
||||
| opts' ^. Geb.evaluatorOptionsOutputMorphism ->
|
||||
case Geb.evalAndOutputMorphism' env morphism of
|
||||
Left err -> exitJuvixError err
|
||||
Right m -> renderStdOut (Geb.ppOut opts' m)
|
||||
| otherwise ->
|
||||
case Geb.eval' env morphism of
|
||||
Left err -> exitJuvixError err
|
||||
Right m -> renderStdOut (Geb.ppOut opts' m)
|
||||
Geb.ExpressionTypedMorphism tyMorph ->
|
||||
evalAndPrint
|
||||
opts
|
||||
(Geb.ExpressionMorphism (tyMorph ^. Geb.typedMorphism))
|
@ -1,38 +0,0 @@
|
||||
module Commands.Dev.Geb.Eval.Options where
|
||||
|
||||
import CommonOptions
|
||||
import Data.List.NonEmpty qualified as NonEmpty
|
||||
import Juvix.Compiler.Backend.Geb.Evaluator qualified as Geb
|
||||
import Juvix.Compiler.Backend.Geb.Pretty qualified as Geb
|
||||
|
||||
data GebEvalOptions = GebEvalOptions
|
||||
{ _gebEvalOptionsInputFile :: AppPath File,
|
||||
_gebEvalOptionsOutputMorphism :: Bool
|
||||
}
|
||||
deriving stock (Data)
|
||||
|
||||
makeLenses ''GebEvalOptions
|
||||
|
||||
instance CanonicalProjection GebEvalOptions Geb.EvaluatorOptions where
|
||||
project x =
|
||||
Geb.EvaluatorOptions
|
||||
{ _evaluatorOptionsOutputMorphism = (x ^. gebEvalOptionsOutputMorphism)
|
||||
}
|
||||
|
||||
instance CanonicalProjection GebEvalOptions Geb.Options where
|
||||
project _ = Geb.defaultOptions
|
||||
|
||||
parseGebEvalOptions :: Parser GebEvalOptions
|
||||
parseGebEvalOptions = do
|
||||
_gebEvalOptionsInputFile <- parseInputFiles (NonEmpty.fromList [FileExtJuvixGeb, FileExtLisp])
|
||||
_gebEvalOptionsOutputMorphism <- optOutputMorphism
|
||||
pure GebEvalOptions {..}
|
||||
|
||||
optOutputMorphism :: Parser Bool
|
||||
optOutputMorphism =
|
||||
switch
|
||||
( long "output-morphism"
|
||||
<> short 'm'
|
||||
<> showDefault
|
||||
<> help "Output a Geb morphism back from a Geb value"
|
||||
)
|
@ -1,33 +0,0 @@
|
||||
module Commands.Dev.Geb.Infer where
|
||||
|
||||
import Commands.Base
|
||||
import Commands.Dev.Geb.Infer.Options
|
||||
import Juvix.Compiler.Backend.Geb qualified as Geb
|
||||
|
||||
runCommand ::
|
||||
forall r.
|
||||
(Member App r, Member EmbedIO r) =>
|
||||
GebInferOptions ->
|
||||
Sem r ()
|
||||
runCommand opts = do
|
||||
let b :: AppPath File
|
||||
b = opts ^. gebInferOptionsInputFile
|
||||
f :: Path Abs File <- fromAppPathFile b
|
||||
content :: Text <- readFile f
|
||||
case Geb.runParser f content of
|
||||
Right (Geb.ExpressionMorphism gebTerm) ->
|
||||
case Geb.inferObject' gebTerm of
|
||||
Left err -> exitJuvixError (JuvixError err)
|
||||
Right obj -> renderStdOut (Geb.ppOut opts obj)
|
||||
Right (Geb.ExpressionTypedMorphism tyMorph) -> do
|
||||
case run . runError @Geb.CheckingError $ Geb.check' tyMorph of
|
||||
Left err -> exitJuvixError (JuvixError err)
|
||||
Right _ -> do
|
||||
renderStdOut $
|
||||
Geb.ppOut
|
||||
opts
|
||||
(tyMorph ^. Geb.typedMorphismObject)
|
||||
putStrLn ""
|
||||
Right (Geb.ExpressionObject _) ->
|
||||
exitJuvixError (error @JuvixError "No inference for objects")
|
||||
Left err -> exitJuvixError (JuvixError err)
|
@ -1,20 +0,0 @@
|
||||
module Commands.Dev.Geb.Infer.Options where
|
||||
|
||||
import CommonOptions
|
||||
import Data.List.NonEmpty qualified as NonEmpty
|
||||
import Juvix.Compiler.Backend.Geb.Pretty qualified as Geb
|
||||
|
||||
newtype GebInferOptions = GebInferOptions
|
||||
{ _gebInferOptionsInputFile :: AppPath File
|
||||
}
|
||||
deriving stock (Data)
|
||||
|
||||
makeLenses ''GebInferOptions
|
||||
|
||||
instance CanonicalProjection GebInferOptions Geb.Options where
|
||||
project _ = Geb.defaultOptions
|
||||
|
||||
parseGebInferOptions :: Parser GebInferOptions
|
||||
parseGebInferOptions = do
|
||||
_gebInferOptionsInputFile <- parseInputFiles (NonEmpty.fromList [FileExtJuvixGeb, FileExtLisp])
|
||||
pure GebInferOptions {..}
|
@ -1,76 +0,0 @@
|
||||
module Commands.Dev.Geb.Options
|
||||
( module Commands.Dev.Geb.Options,
|
||||
module Commands.Dev.Geb.Eval.Options,
|
||||
module Commands.Dev.Geb.Repl.Options,
|
||||
)
|
||||
where
|
||||
|
||||
import Commands.Dev.Geb.Eval.Options
|
||||
import Commands.Dev.Geb.Infer.Options
|
||||
import Commands.Dev.Geb.Read.Options
|
||||
import Commands.Dev.Geb.Repl.Options
|
||||
import CommonOptions
|
||||
|
||||
data GebCommand
|
||||
= GebCommandRepl GebReplOptions
|
||||
| GebCommandEval GebEvalOptions
|
||||
| GebCommandRead GebReadOptions
|
||||
| GebCommandInfer GebInferOptions
|
||||
| GebCommandCheck GebInferOptions
|
||||
deriving stock (Data)
|
||||
|
||||
parseGebCommand :: Parser GebCommand
|
||||
parseGebCommand =
|
||||
hsubparser $
|
||||
mconcat
|
||||
[ commandRepl,
|
||||
commandEval,
|
||||
commandRead,
|
||||
commandInfer,
|
||||
commandCheck
|
||||
]
|
||||
where
|
||||
commandRepl :: Mod CommandFields GebCommand
|
||||
commandRepl = command "repl" replInfo
|
||||
|
||||
commandEval :: Mod CommandFields GebCommand
|
||||
commandEval = command "eval" evalInfo
|
||||
|
||||
commandRead :: Mod CommandFields GebCommand
|
||||
commandRead = command "read" readInfo
|
||||
|
||||
commandInfer :: Mod CommandFields GebCommand
|
||||
commandInfer = command "infer" inferInfo
|
||||
|
||||
commandCheck :: Mod CommandFields GebCommand
|
||||
commandCheck = command "check" checkInfo
|
||||
|
||||
replInfo :: ParserInfo GebCommand
|
||||
replInfo =
|
||||
info
|
||||
(GebCommandRepl <$> parseGebReplOptions)
|
||||
(progDesc "Start an interactive session of the JuvixGeb evaluator")
|
||||
|
||||
evalInfo :: ParserInfo GebCommand
|
||||
evalInfo =
|
||||
info
|
||||
(GebCommandEval <$> parseGebEvalOptions)
|
||||
(progDesc "Evaluate a JuvixGeb file and pretty print the result")
|
||||
|
||||
readInfo :: ParserInfo GebCommand
|
||||
readInfo =
|
||||
info
|
||||
(GebCommandRead <$> parseGebReadOptions)
|
||||
(progDesc "Read a JuvixGeb file and pretty print it")
|
||||
|
||||
inferInfo :: ParserInfo GebCommand
|
||||
inferInfo =
|
||||
info
|
||||
(GebCommandInfer <$> parseGebInferOptions)
|
||||
(progDesc "Infer the Geb object for a Geb morphism found in the given file. ")
|
||||
|
||||
checkInfo :: ParserInfo GebCommand
|
||||
checkInfo =
|
||||
info
|
||||
(GebCommandInfer <$> parseGebInferOptions)
|
||||
(progDesc "Check the given Geb object matches the given Geb morphism")
|
@ -1,22 +0,0 @@
|
||||
module Commands.Dev.Geb.Read where
|
||||
|
||||
import Commands.Base
|
||||
import Commands.Dev.Geb.Read.Options
|
||||
import Juvix.Compiler.Backend.Geb.Pretty qualified as Geb
|
||||
import Juvix.Compiler.Backend.Geb.Translation.FromSource qualified as Geb
|
||||
|
||||
runCommand ::
|
||||
forall r.
|
||||
(Member App r, Member EmbedIO r) =>
|
||||
GebReadOptions ->
|
||||
Sem r ()
|
||||
runCommand opts = do
|
||||
let b :: AppPath File
|
||||
b = opts ^. gebReadOptionsInputFile
|
||||
f :: Path Abs File <- fromAppPathFile b
|
||||
content :: Text <- readFile f
|
||||
case Geb.runParser f content of
|
||||
Left err -> exitJuvixError (JuvixError err)
|
||||
Right gebTerm -> do
|
||||
renderStdOut (Geb.ppOut opts gebTerm)
|
||||
putStrLn ""
|
@ -1,21 +0,0 @@
|
||||
module Commands.Dev.Geb.Read.Options where
|
||||
|
||||
import CommonOptions
|
||||
import Data.List.NonEmpty qualified as NonEmpty
|
||||
import Juvix.Compiler.Backend.Geb.Pretty qualified as Geb
|
||||
|
||||
newtype GebReadOptions = GebReadOptions
|
||||
{ _gebReadOptionsInputFile :: AppPath File
|
||||
}
|
||||
deriving stock (Data)
|
||||
|
||||
makeLenses ''GebReadOptions
|
||||
|
||||
instance CanonicalProjection GebReadOptions Geb.Options where
|
||||
project _ = Geb.defaultOptions
|
||||
|
||||
parseGebReadOptions :: Parser GebReadOptions
|
||||
parseGebReadOptions = do
|
||||
_gebReadOptionsInputFile <-
|
||||
parseInputFiles (NonEmpty.fromList [FileExtJuvixGeb, FileExtLisp])
|
||||
pure GebReadOptions {..}
|
@ -1,305 +0,0 @@
|
||||
module Commands.Dev.Geb.Repl where
|
||||
|
||||
import Commands.Base hiding
|
||||
( command,
|
||||
)
|
||||
import Commands.Dev.Geb.Repl.Format
|
||||
import Commands.Dev.Geb.Repl.Options
|
||||
import Control.Exception (throwIO)
|
||||
import Control.Monad.State.Strict qualified as State
|
||||
import Data.String.Interpolate (i, __i)
|
||||
import Juvix.Compiler.Backend qualified as Backend
|
||||
import Juvix.Compiler.Backend.Geb qualified as Geb
|
||||
import Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Error
|
||||
import Juvix.Data.Error.GenericError qualified as Error
|
||||
import Juvix.Extra.Paths
|
||||
import Juvix.Extra.Version
|
||||
import Juvix.Prelude.Pretty qualified as P
|
||||
import System.Console.ANSI qualified as Ansi
|
||||
import System.Console.Haskeline
|
||||
import System.Console.Repline qualified as Repline
|
||||
|
||||
type ReplS = State.StateT ReplState IO
|
||||
|
||||
type Repl a = Repline.HaskelineT ReplS a
|
||||
|
||||
data ReplState = ReplState
|
||||
{ _replContextEntryPoint :: Maybe EntryPoint,
|
||||
_replStateInvokeDir :: Path Abs Dir,
|
||||
_replStateGlobalOptions :: GlobalOptions
|
||||
}
|
||||
|
||||
makeLenses ''ReplState
|
||||
|
||||
runCommand :: (Members '[EmbedIO, App] r) => GebReplOptions -> Sem r ()
|
||||
runCommand replOpts = do
|
||||
invokeDir <- askInvokeDir
|
||||
root <- askRoot
|
||||
globalOptions <- askGlobalOptions
|
||||
let getReplEntryPoint :: SomeBase File -> Repl EntryPoint
|
||||
getReplEntryPoint inputFile = do
|
||||
gopts <- State.gets (^. replStateGlobalOptions)
|
||||
absInputFile :: Path Abs File <- replMakeAbsolute inputFile
|
||||
set entryPointTarget (Just Backend.TargetGeb)
|
||||
<$> runM (runTaggedLockPermissive (entryPointFromGlobalOptions root (Just absInputFile) gopts))
|
||||
liftIO
|
||||
. State.evalStateT
|
||||
(replAction replOpts getReplEntryPoint)
|
||||
$ ReplState
|
||||
{ _replContextEntryPoint = Nothing,
|
||||
_replStateGlobalOptions = globalOptions,
|
||||
_replStateInvokeDir = invokeDir
|
||||
}
|
||||
|
||||
loadEntryPoint :: EntryPoint -> Repl ()
|
||||
loadEntryPoint ep = do
|
||||
State.modify
|
||||
( set
|
||||
replContextEntryPoint
|
||||
(Just ep)
|
||||
)
|
||||
let epPath :: Maybe (Path Abs File) = ep ^. entryPointModulePath
|
||||
whenJust epPath $ \path -> do
|
||||
liftIO (putStrLn . pack $ "OK loaded " <> toFilePath path)
|
||||
content <- liftIO (readFile path)
|
||||
let evalRes =
|
||||
Geb.runEval $
|
||||
Geb.RunEvalArgs
|
||||
{ _runEvalArgsContent = content,
|
||||
_runEvalArgsInputFile = path,
|
||||
_runEvalArgsEvaluatorOptions = Geb.defaultEvaluatorOptions
|
||||
}
|
||||
printEvalResult evalRes
|
||||
|
||||
reloadFile :: String -> Repl ()
|
||||
reloadFile _ = do
|
||||
mentryPoint <- State.gets ((^. replContextEntryPoint))
|
||||
maybe noFileLoadedMsg loadEntryPoint mentryPoint
|
||||
|
||||
pSomeFile :: String -> SomeBase File
|
||||
pSomeFile = someFile . unpack . strip . pack
|
||||
|
||||
type ReplEntryPoint = SomeBase File -> Repl EntryPoint
|
||||
|
||||
loadFile :: ReplEntryPoint -> SomeBase File -> Repl ()
|
||||
loadFile getReplEntryPoint f = do
|
||||
entryPoint <- getReplEntryPoint f
|
||||
loadEntryPoint entryPoint
|
||||
|
||||
inferObject :: String -> Repl ()
|
||||
inferObject gebMorphism = Repline.dontCrash $ do
|
||||
case Geb.runParser gebReplPath (pack gebMorphism) of
|
||||
Left err -> printError (JuvixError err)
|
||||
Right (Geb.ExpressionMorphism morphism) -> do
|
||||
case Geb.inferObject' morphism of
|
||||
Right obj -> renderOut (Geb.ppOut Geb.defaultEvaluatorOptions obj)
|
||||
Left err -> printError (JuvixError err)
|
||||
Right (Geb.ExpressionTypedMorphism _) ->
|
||||
checkTypedMorphism gebMorphism
|
||||
Right _ -> printError (error "Inference only works on Geb morphisms.")
|
||||
|
||||
checkTypedMorphism :: String -> Repl ()
|
||||
checkTypedMorphism gebMorphism = Repline.dontCrash $ do
|
||||
case Geb.runParser gebReplPath (pack gebMorphism) of
|
||||
Left err -> printError (JuvixError err)
|
||||
Right (Geb.ExpressionTypedMorphism tyMorphism) -> do
|
||||
case run . runError @CheckingError $ Geb.check' tyMorphism of
|
||||
Right obj -> renderOut (Geb.ppOut Geb.defaultEvaluatorOptions obj)
|
||||
Left err -> printError (JuvixError err)
|
||||
Right _ -> printError (error "Checking only works on typed Geb morphisms.")
|
||||
|
||||
runReplCommand :: String -> Repl ()
|
||||
runReplCommand input_ =
|
||||
Repline.dontCrash $
|
||||
do
|
||||
let evalRes =
|
||||
Geb.runEval $
|
||||
Geb.RunEvalArgs
|
||||
{ _runEvalArgsContent = pack input_,
|
||||
_runEvalArgsInputFile = gebReplPath,
|
||||
_runEvalArgsEvaluatorOptions = Geb.defaultEvaluatorOptions
|
||||
}
|
||||
printEvalResult evalRes
|
||||
|
||||
evalAndOutputMorphism :: String -> Repl ()
|
||||
evalAndOutputMorphism input_ =
|
||||
Repline.dontCrash $ do
|
||||
let evalRes =
|
||||
Geb.runEval $
|
||||
Geb.RunEvalArgs
|
||||
{ _runEvalArgsContent = pack input_,
|
||||
_runEvalArgsInputFile = gebReplPath,
|
||||
_runEvalArgsEvaluatorOptions =
|
||||
Geb.defaultEvaluatorOptions
|
||||
{ Geb._evaluatorOptionsOutputMorphism = True
|
||||
}
|
||||
}
|
||||
printEvalResult evalRes
|
||||
|
||||
options :: ReplEntryPoint -> [(String, String -> Repl ())]
|
||||
options replEntryPoint =
|
||||
[ ("help", Repline.dontCrash . helpText),
|
||||
-- `multiline` is included here for auto-completion purposes only.
|
||||
-- `repline`'s `multilineCommand` logic overrides this no-op.
|
||||
(multilineCmd, Repline.dontCrash . \_ -> return ()),
|
||||
("check", checkTypedMorphism),
|
||||
("load", Repline.dontCrash . loadFile replEntryPoint . pSomeFile),
|
||||
("morphism", evalAndOutputMorphism),
|
||||
("quit", quit),
|
||||
("reload", Repline.dontCrash . reloadFile),
|
||||
("root", printRoot),
|
||||
("type", inferObject),
|
||||
("version", displayVersion)
|
||||
]
|
||||
|
||||
optsCompleter :: ReplEntryPoint -> Repline.WordCompleter ReplS
|
||||
optsCompleter replEntryPoint n = do
|
||||
let names = (":" <>) . fst <$> options replEntryPoint
|
||||
return (filter (isPrefixOf n) names)
|
||||
|
||||
prefix :: Maybe Char
|
||||
prefix = Just ':'
|
||||
|
||||
multilineCommand :: Maybe String
|
||||
multilineCommand = Just multilineCmd
|
||||
|
||||
tabComplete :: ReplEntryPoint -> Repline.CompleterStyle ReplS
|
||||
tabComplete replEntryPoint =
|
||||
Repline.Prefix
|
||||
(Repline.wordCompleter (optsCompleter replEntryPoint))
|
||||
defaultMatcher
|
||||
|
||||
replAction :: GebReplOptions -> ReplEntryPoint -> ReplS ()
|
||||
replAction replOpts replEntryPoint =
|
||||
Repline.evalReplOpts
|
||||
Repline.ReplOpts
|
||||
{ prefix,
|
||||
multilineCommand,
|
||||
initialiser = initSession replOpts,
|
||||
finaliser = endSession,
|
||||
command = runReplCommand,
|
||||
options = options replEntryPoint,
|
||||
tabComplete = tabComplete replEntryPoint,
|
||||
banner
|
||||
}
|
||||
|
||||
defaultMatcher :: [(String, CompletionFunc ReplS)]
|
||||
defaultMatcher = [(":load", Repline.fileCompleter)]
|
||||
|
||||
banner :: Repline.MultiLine -> Repl String
|
||||
banner = \case
|
||||
Repline.MultiLine -> return "... "
|
||||
Repline.SingleLine -> replPromptText
|
||||
|
||||
noFileLoadedMsg :: Repl ()
|
||||
noFileLoadedMsg =
|
||||
renderOut
|
||||
. ReplMessageDoc
|
||||
$ P.annotate
|
||||
ReplError
|
||||
"No file loaded. Load a file using the `:load FILE` command."
|
||||
<> P.line
|
||||
|
||||
initSession :: GebReplOptions -> Repl ()
|
||||
initSession replOpts
|
||||
| replOpts ^. gebReplOptionsSilent = return ()
|
||||
| otherwise = renderOut welcomeMsg
|
||||
|
||||
welcomeMsg :: ReplMessageDoc
|
||||
welcomeMsg =
|
||||
ReplMessageDoc $
|
||||
P.annotate ReplIntro "Welcome to the Juvix Geb REPL!"
|
||||
<> P.line
|
||||
<> normal [i|Juvix v#{versionTag}: https://juvix.org.|]
|
||||
<> P.line
|
||||
<> normal "Type :help for help."
|
||||
<> P.line
|
||||
|
||||
replPromptText :: Repl String
|
||||
replPromptText = do
|
||||
r <- replText . ReplMessageDoc $ P.annotate ReplPrompt "geb> "
|
||||
return (unpack r)
|
||||
|
||||
helpText :: String -> Repl ()
|
||||
helpText _ =
|
||||
renderOutNormal
|
||||
[__i|
|
||||
EXPRESSION Evaluate a Geb morphism
|
||||
:help Print this help
|
||||
:load FILE Load a file into the REPL
|
||||
:reload Reload the currently loaded file
|
||||
:check EXPRESSION Check the type of a Geb morphism
|
||||
:type EXPRESSION Infer the type of a Geb morphism
|
||||
:morphism EXPRESSION Read back after evaluate a Geb morphism
|
||||
:version Display the Juvix version
|
||||
:multiline Enter multiline mode
|
||||
:root Print the root directory of the REPL
|
||||
:version Display the Juvix version
|
||||
:quit Exit the REPL
|
||||
|]
|
||||
|
||||
multilineCmd :: String
|
||||
multilineCmd = "multiline"
|
||||
|
||||
quit :: String -> Repl ()
|
||||
quit _ = liftIO (throwIO Interrupt)
|
||||
|
||||
endSession :: Repl Repline.ExitDecision
|
||||
endSession = return Repline.Exit
|
||||
|
||||
printRoot :: String -> Repl ()
|
||||
printRoot _ = do
|
||||
r <- State.gets (^. replStateInvokeDir)
|
||||
renderOutNormal $ pack (toFilePath r)
|
||||
|
||||
displayVersion :: String -> Repl ()
|
||||
displayVersion _ = renderOutNormal versionTag
|
||||
|
||||
replMakeAbsolute :: SomeBase b -> Repl (Path Abs b)
|
||||
replMakeAbsolute = \case
|
||||
Abs p -> return p
|
||||
Rel r -> do
|
||||
invokeDir <- State.gets (^. replStateInvokeDir)
|
||||
return (invokeDir <//> r)
|
||||
|
||||
replText :: (P.HasAnsiBackend a, P.HasTextBackend a) => a -> Repl Text
|
||||
replText t = do
|
||||
opts <- State.gets (^. replStateGlobalOptions)
|
||||
hasAnsi <- liftIO (Ansi.hSupportsANSIColor stdout)
|
||||
return $ P.toAnsiText (not (opts ^. globalNoColors) && hasAnsi) t
|
||||
|
||||
render' :: (P.HasAnsiBackend a, P.HasTextBackend a) => a -> Repl ()
|
||||
render' t = do
|
||||
opts <- State.gets (^. replStateGlobalOptions)
|
||||
hasAnsi <- liftIO (Ansi.hSupportsANSIColor stdout)
|
||||
liftIO (P.renderIO (not (opts ^. globalNoColors) && hasAnsi) t)
|
||||
|
||||
renderOut :: (P.HasAnsiBackend a, P.HasTextBackend a) => a -> Repl ()
|
||||
renderOut t = render' t >> liftIO (putStrLn "")
|
||||
|
||||
renderOutNormal :: Text -> Repl ()
|
||||
renderOutNormal = renderOut . ReplMessageDoc . normal
|
||||
|
||||
printError :: JuvixError -> Repl ()
|
||||
printError e = do
|
||||
opts <- State.gets (^. replStateGlobalOptions)
|
||||
hasAnsi <- liftIO (Ansi.hSupportsANSIColor stderr)
|
||||
let useAnsi = (not (opts ^. globalNoColors) && hasAnsi)
|
||||
errorText <-
|
||||
replText . ReplMessageDoc
|
||||
$ P.annotate
|
||||
ReplError
|
||||
$ pretty
|
||||
( run
|
||||
. runReader (project' @GenericOptions opts)
|
||||
$ Error.render useAnsi False e
|
||||
)
|
||||
hPutStrLn stderr errorText
|
||||
|
||||
printEvalResult :: Either JuvixError Geb.RunEvalResult -> Repl ()
|
||||
printEvalResult = \case
|
||||
Left err -> printError err
|
||||
Right (Geb.RunEvalResultGebValue v) ->
|
||||
renderOut (Geb.ppOut Geb.defaultEvaluatorOptions v)
|
||||
Right (Geb.RunEvalResultMorphism morphism) ->
|
||||
renderOut (Geb.ppOut Geb.defaultEvaluatorOptions morphism)
|
@ -1,40 +0,0 @@
|
||||
module Commands.Dev.Geb.Repl.Format
|
||||
( module Commands.Dev.Geb.Repl.Format,
|
||||
pretty,
|
||||
)
|
||||
where
|
||||
|
||||
import Juvix.Prelude
|
||||
import Juvix.Prelude.Pretty
|
||||
import Prettyprinter.Render.Terminal
|
||||
|
||||
data ReplStyle
|
||||
= ReplPrompt
|
||||
| ReplName
|
||||
| ReplError
|
||||
| ReplIntro
|
||||
| ReplNormal
|
||||
|
||||
newtype ReplMessageDoc = ReplMessageDoc (Doc ReplStyle)
|
||||
|
||||
instance HasAnsiBackend ReplMessageDoc where
|
||||
toAnsiStream (ReplMessageDoc o) = reAnnotateS stylize (layoutPretty defaultLayoutOptions o)
|
||||
toAnsiDoc (ReplMessageDoc o) = reAnnotate stylize o
|
||||
|
||||
instance HasTextBackend ReplMessageDoc where
|
||||
toTextDoc (ReplMessageDoc o) = unAnnotate o
|
||||
toTextStream (ReplMessageDoc o) = layoutPretty defaultLayoutOptions (unAnnotate o)
|
||||
|
||||
stylize :: ReplStyle -> AnsiStyle
|
||||
stylize = \case
|
||||
ReplPrompt -> color Blue
|
||||
ReplName -> color Green
|
||||
ReplError -> color Red
|
||||
ReplNormal -> color Blue
|
||||
ReplIntro -> bold
|
||||
|
||||
normal :: Text -> Doc ReplStyle
|
||||
normal = annotate ReplNormal . pretty
|
||||
|
||||
ppOutput :: Doc ReplStyle -> AnsiText
|
||||
ppOutput = mkAnsiText . ReplMessageDoc
|
@ -1,25 +0,0 @@
|
||||
module Commands.Dev.Geb.Repl.Options where
|
||||
|
||||
import CommonOptions
|
||||
|
||||
newtype GebReplOptions = GebReplOptions
|
||||
{ _gebReplOptionsSilent :: Bool
|
||||
}
|
||||
deriving stock (Data)
|
||||
|
||||
makeLenses ''GebReplOptions
|
||||
|
||||
defaultGebReplOptions :: GebReplOptions
|
||||
defaultGebReplOptions =
|
||||
GebReplOptions
|
||||
{ _gebReplOptionsSilent = False
|
||||
}
|
||||
|
||||
parseGebReplOptions :: Parser GebReplOptions
|
||||
parseGebReplOptions = do
|
||||
_gebReplOptionsSilent <-
|
||||
switch
|
||||
( long "--silent"
|
||||
<> help "Don't show the Juvix information in the REPL"
|
||||
)
|
||||
pure GebReplOptions {..}
|
@ -2,7 +2,6 @@ module Commands.Dev.Options
|
||||
( module Commands.Dev.Options,
|
||||
module Commands.Dev.Asm.Options,
|
||||
module Commands.Dev.Core.Options,
|
||||
module Commands.Dev.Geb.Options,
|
||||
module Commands.Dev.Internal.Options,
|
||||
module Commands.Dev.Parse.Options,
|
||||
module Commands.Dev.Highlight.Options,
|
||||
@ -17,7 +16,6 @@ import Commands.Dev.Casm.Options
|
||||
import Commands.Dev.Core.Options
|
||||
import Commands.Dev.DevCompile.Options (DevCompileCommand, parseDevCompileCommand)
|
||||
import Commands.Dev.DisplayRoot.Options
|
||||
import Commands.Dev.Geb.Options
|
||||
import Commands.Dev.Highlight.Options
|
||||
import Commands.Dev.ImportTree.Options
|
||||
import Commands.Dev.Internal.Options
|
||||
@ -40,7 +38,6 @@ data DevCommand
|
||||
| Internal InternalCommand
|
||||
| DevCompile DevCompileCommand
|
||||
| Core CoreCommand
|
||||
| Geb GebCommand
|
||||
| Asm AsmCommand
|
||||
| Reg RegCommand
|
||||
| Tree TreeCommand
|
||||
@ -63,7 +60,6 @@ parseDevCommand =
|
||||
commandDevCompile,
|
||||
commandInternal,
|
||||
commandCore,
|
||||
commandGeb,
|
||||
commandAsm,
|
||||
commandReg,
|
||||
commandTree,
|
||||
@ -107,13 +103,6 @@ commandInternal =
|
||||
(Internal <$> parseInternalCommand)
|
||||
(progDesc "Subcommands related to Internal")
|
||||
|
||||
commandGeb :: Mod CommandFields DevCommand
|
||||
commandGeb =
|
||||
command "geb" $
|
||||
info
|
||||
(Geb <$> parseGebCommand)
|
||||
(progDesc "Subcommands related to JuvixGeb")
|
||||
|
||||
commandCore :: Mod CommandFields DevCommand
|
||||
commandCore =
|
||||
command "core" $
|
||||
|
@ -71,7 +71,6 @@ runCommand opts = do
|
||||
AppTargetReg -> err "JuvixReg"
|
||||
AppTargetAnoma -> err "Anoma"
|
||||
AppTargetTree -> err "JuvixTree"
|
||||
AppTargetGeb -> err "GEB"
|
||||
AppTargetVampIR -> err "VampIR"
|
||||
AppTargetCore -> err "JuvixCore"
|
||||
AppTargetAsm -> err "JuvixAsm"
|
||||
|
@ -37,7 +37,6 @@ getEntry PipelineArg {..} = do
|
||||
getTarget = \case
|
||||
AppTargetWasm32Wasi -> Backend.TargetCWasm32Wasi
|
||||
AppTargetNative64 -> Backend.TargetCNative64
|
||||
AppTargetGeb -> Backend.TargetGeb
|
||||
AppTargetVampIR -> Backend.TargetVampIR
|
||||
AppTargetCore -> Backend.TargetCore
|
||||
AppTargetAsm -> Backend.TargetAsm
|
||||
|
@ -27,7 +27,6 @@ runCompile opts = do
|
||||
case opts ^. compileTarget of
|
||||
AppTargetWasm32Wasi -> clangWasmWasiCompile opts
|
||||
AppTargetNative64 -> clangNativeCompile opts
|
||||
AppTargetGeb -> return (())
|
||||
AppTargetVampIR -> return ()
|
||||
AppTargetCore -> return ()
|
||||
AppTargetAsm -> return ()
|
||||
@ -48,7 +47,6 @@ prepareRuntime buildDir o = do
|
||||
AppTargetNative64
|
||||
| o ^. compileDebug -> writeRuntime nativeDebugRuntime
|
||||
AppTargetNative64 -> writeRuntime nativeReleaseRuntime
|
||||
AppTargetGeb -> return ()
|
||||
AppTargetVampIR -> return ()
|
||||
AppTargetCore -> return ()
|
||||
AppTargetAsm -> return ()
|
||||
@ -107,9 +105,6 @@ outputFile opts = do
|
||||
| opts ^. compilePreprocess -> addExtension' cFileExt (addExtension' ".out" (removeExtension' inputFile))
|
||||
| opts ^. compileAssembly -> replaceExtension' ".wat" inputFile
|
||||
| otherwise -> replaceExtension' ".wasm" baseOutputFile
|
||||
AppTargetGeb
|
||||
| opts ^. compileTerm -> replaceExtension' juvixGebFileExt inputFile
|
||||
| otherwise -> replaceExtension' lispFileExt baseOutputFile
|
||||
AppTargetVampIR ->
|
||||
replaceExtension' vampIRFileExt baseOutputFile
|
||||
AppTargetCore ->
|
||||
|
@ -12,7 +12,6 @@ import Prelude (Show (show))
|
||||
data CompileTarget
|
||||
= AppTargetNative64
|
||||
| AppTargetWasm32Wasi
|
||||
| AppTargetGeb
|
||||
| AppTargetVampIR
|
||||
| AppTargetCore
|
||||
| AppTargetAsm
|
||||
@ -28,7 +27,6 @@ instance Show CompileTarget where
|
||||
show = \case
|
||||
AppTargetWasm32Wasi -> "wasi"
|
||||
AppTargetNative64 -> "native"
|
||||
AppTargetGeb -> "geb"
|
||||
AppTargetVampIR -> "vampir"
|
||||
AppTargetCore -> "core"
|
||||
AppTargetAsm -> "asm"
|
||||
@ -50,7 +48,6 @@ data CompileOptions' inputFile = CompileOptions
|
||||
_compileCOutput :: Bool,
|
||||
_compilePreprocess :: Bool,
|
||||
_compileAssembly :: Bool,
|
||||
_compileTerm :: Bool,
|
||||
_compileUnsafe :: Bool,
|
||||
_compileOutputFile :: Maybe (AppPath File),
|
||||
_compileTarget :: CompileTarget,
|
||||
@ -72,7 +69,6 @@ compileTargetDescription = \case
|
||||
AppTargetWasm32Wasi -> "Compile to WASI (WebAssembly System Interface)"
|
||||
AppTargetAnoma -> "Compile to Anoma"
|
||||
AppTargetCairo -> "Compile to Cairo"
|
||||
AppTargetGeb -> "Compile to Geb"
|
||||
AppTargetVampIR -> "Compile to VampIR"
|
||||
AppTargetCasm -> "Compile to JuvixCasm"
|
||||
AppTargetCore -> "Compile to VampIR"
|
||||
@ -129,16 +125,6 @@ parseCompileOptions' supportedTargets parserFile = do
|
||||
<> long "only-assemble"
|
||||
<> help "Produce assembly output only (for targets: wasi, native)"
|
||||
)
|
||||
_compileTerm <-
|
||||
if
|
||||
| elem AppTargetGeb supportedTargets ->
|
||||
switch
|
||||
( short 'G'
|
||||
<> long "only-term"
|
||||
<> help "Produce term output only (for targets: geb)"
|
||||
)
|
||||
| otherwise ->
|
||||
pure False
|
||||
_compileNockmaUsePrettySymbols <-
|
||||
switch
|
||||
( long "nockma-pretty"
|
||||
|
@ -19,7 +19,6 @@ RUNTIME=$((RUNTIME_C+RUNTIME_RUST+RUNTIME_VAMPIR+RUNTIME_JVT+RUNTIME_CASM))
|
||||
BACKENDC=$(count src/Juvix/Compiler/Backend/C/)
|
||||
BACKENDRUST=$(count src/Juvix/Compiler/Backend/Rust/)
|
||||
CAIRO=$(count src/Juvix/Compiler/Backend/Cairo/)
|
||||
GEB=$(count src/Juvix/Compiler/Backend/Geb/)
|
||||
VAMPIR=$(count src/Juvix/Compiler/Backend/VampIR/)
|
||||
CASM=$(count src/Juvix/Compiler/Casm/)
|
||||
NOCK=$(count src/Juvix/Compiler/Nockma)
|
||||
@ -43,7 +42,7 @@ PRELUDE=$(count src/Juvix/Prelude/)
|
||||
STORE=$(count src/Juvix/Compiler/Store/)
|
||||
|
||||
FRONT=$((CONCRETE + INTERNAL + BUILTINS + PIPELINE))
|
||||
BACK=$((BACKENDC + BACKENDRUST + GEB + VAMPIR + NOCK + REG + ASM + TREE + CORE + CASM + CAIRO))
|
||||
BACK=$((BACKENDC + BACKENDRUST + VAMPIR + NOCK + REG + ASM + TREE + CORE + CASM + CAIRO))
|
||||
OTHER=$((APP + STORE + HTML + MARKDOWN + ISABELLE + EXTRA + DATA + PRELUDE))
|
||||
TESTS=$(count test/)
|
||||
|
||||
@ -56,7 +55,6 @@ echo " Builtins: $BUILTINS LOC"
|
||||
echo " Pipeline: $PIPELINE LOC"
|
||||
echo "Middle and back end: $BACK LOC"
|
||||
echo " VampIR backend: $VAMPIR LOC"
|
||||
echo " GEB backend: $GEB LOC"
|
||||
echo " C backend: $BACKENDC LOC"
|
||||
echo " Rust backend: $BACKENDRUST LOC"
|
||||
echo " Cairo backend: $((CASM + CAIRO)) LOC"
|
||||
|
@ -6,7 +6,6 @@ import Juvix.Prelude
|
||||
data Target
|
||||
= TargetCWasm32Wasi
|
||||
| TargetCNative64
|
||||
| TargetGeb
|
||||
| TargetVampIR
|
||||
| TargetCore
|
||||
| TargetAsm
|
||||
@ -69,8 +68,6 @@ getLimits tgt debug = case tgt of
|
||||
_limitsBuiltinUIDsNum = 8,
|
||||
_limitsSpecialisedApply = 3
|
||||
}
|
||||
TargetGeb ->
|
||||
defaultLimits
|
||||
TargetVampIR ->
|
||||
defaultLimits
|
||||
TargetCore ->
|
||||
|
@ -1,14 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb
|
||||
( module Juvix.Compiler.Backend.Geb.Language,
|
||||
module Juvix.Compiler.Backend.Geb.Translation,
|
||||
module Juvix.Compiler.Backend.Geb.Evaluator,
|
||||
module Juvix.Compiler.Backend.Geb.Pretty,
|
||||
module Juvix.Compiler.Backend.Geb.Analysis.TypeChecking,
|
||||
)
|
||||
where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Analysis.TypeChecking
|
||||
import Juvix.Compiler.Backend.Geb.Evaluator
|
||||
import Juvix.Compiler.Backend.Geb.Language
|
||||
import Juvix.Compiler.Backend.Geb.Pretty
|
||||
import Juvix.Compiler.Backend.Geb.Translation
|
@ -1,8 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Analysis.TypeChecking
|
||||
( module Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Checker,
|
||||
module Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Error,
|
||||
)
|
||||
where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Checker
|
||||
import Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Error
|
@ -1,220 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Checker
|
||||
( module Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Checker,
|
||||
)
|
||||
where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Error
|
||||
import Juvix.Compiler.Backend.Geb.Data.Context as Context
|
||||
import Juvix.Compiler.Backend.Geb.Extra
|
||||
import Juvix.Compiler.Backend.Geb.Language
|
||||
|
||||
type CheckingEnv = Context Object
|
||||
|
||||
check' :: (Member (Error CheckingError) r) => TypedMorphism -> Sem r TypedMorphism
|
||||
check' tyMorph = do
|
||||
runReader (mempty @CheckingEnv) $ check (tyMorph ^. typedMorphism) (tyMorph ^. typedMorphismObject)
|
||||
return tyMorph
|
||||
|
||||
check :: (Members '[Reader CheckingEnv, Error CheckingError] r) => Morphism -> Object -> Sem r ()
|
||||
check morph obj' = do
|
||||
ctx <- ask @CheckingEnv
|
||||
obj <- runReader ctx (inferObject morph)
|
||||
checkTypesEqual obj obj'
|
||||
|
||||
checkTypesEqual :: (Members '[Reader CheckingEnv, Error CheckingError] r) => Object -> Object -> Sem r ()
|
||||
checkTypesEqual obj obj' =
|
||||
unless
|
||||
(obj == obj')
|
||||
( throw $
|
||||
CheckingErrorTypeMismatch
|
||||
TypeMismatch
|
||||
{ _typeMismatchExpected = obj,
|
||||
_typeMismatchActual = obj'
|
||||
}
|
||||
)
|
||||
|
||||
checkSameType :: (InferEffects r) => [Morphism] -> Sem r ()
|
||||
checkSameType = \case
|
||||
[] -> return ()
|
||||
(x : xs) -> do
|
||||
obj <- inferObject x
|
||||
checkListSameType xs obj
|
||||
|
||||
checkListSameType :: (InferEffects r) => [Morphism] -> Object -> Sem r ()
|
||||
checkListSameType morphs obj = mapM_ (`check` obj) morphs
|
||||
|
||||
inferObject' :: Morphism -> Either CheckingError Object
|
||||
inferObject' = run . runError . runReader mempty . inferObject @'[Reader CheckingEnv, Error CheckingError]
|
||||
|
||||
type InferEffects r = Members '[Reader CheckingEnv, Error CheckingError] r
|
||||
|
||||
inferObject :: (InferEffects r) => Morphism -> Sem r Object
|
||||
inferObject = \case
|
||||
MorphismUnit -> return ObjectTerminal
|
||||
MorphismInteger {} -> return ObjectInteger
|
||||
MorphismAbsurd x -> inferObjectAbsurd x
|
||||
MorphismApplication app -> inferObjectApplication app
|
||||
MorphismPair pair -> inferObjectPair pair
|
||||
MorphismCase c -> inferObjectCase c
|
||||
MorphismFirst p -> inferObjectFirst p
|
||||
MorphismSecond p -> inferObjectSecond p
|
||||
MorphismLambda l -> inferObjectLambda l
|
||||
MorphismBinop op -> inferObjectBinop op
|
||||
MorphismVar v -> inferObjectVar v
|
||||
MorphismLeft a -> inferObjectLeft a
|
||||
MorphismRight b -> inferObjectRight b
|
||||
MorphismFail x -> return $ x ^. failureType
|
||||
|
||||
inferObjectAbsurd :: (InferEffects r) => Absurd -> Sem r Object
|
||||
inferObjectAbsurd x = do
|
||||
check (x ^. absurdValue) (x ^. absurdType)
|
||||
return ObjectInitial
|
||||
|
||||
inferObjectApplication :: (InferEffects r) => Application -> Sem r Object
|
||||
inferObjectApplication app = do
|
||||
homTy <- inferObject (app ^. applicationLeft)
|
||||
lType <- inferObject (app ^. applicationRight)
|
||||
case homTy of
|
||||
ObjectHom Hom {..} -> do
|
||||
checkTypesEqual _homDomain lType
|
||||
return _homCodomain
|
||||
_ ->
|
||||
throw $
|
||||
CheckingErrorExpectedType
|
||||
ExpectedType
|
||||
{ _expectedTypeObject = homTy,
|
||||
_expectedTypeKind = "hom object"
|
||||
}
|
||||
|
||||
inferObjectLambda :: (InferEffects r) => Lambda -> Sem r Object
|
||||
inferObjectLambda l = do
|
||||
let aType = l ^. lambdaVarType
|
||||
ctx <- ask @CheckingEnv
|
||||
bType <-
|
||||
local
|
||||
(const (Context.cons aType ctx))
|
||||
(inferObject (l ^. lambdaBody))
|
||||
return $
|
||||
ObjectHom $
|
||||
Hom
|
||||
{ _homDomain = aType,
|
||||
_homCodomain = bType
|
||||
}
|
||||
|
||||
inferObjectPair :: (InferEffects r) => Pair -> Sem r Object
|
||||
inferObjectPair pair = do
|
||||
lType <- inferObject (pair ^. pairLeft)
|
||||
rType <- inferObject (pair ^. pairRight)
|
||||
return $
|
||||
ObjectProduct
|
||||
Product
|
||||
{ _productLeft = lType,
|
||||
_productRight = rType
|
||||
}
|
||||
|
||||
inferObjectCase :: (InferEffects r) => Case -> Sem r Object
|
||||
inferObjectCase c = do
|
||||
vType <- inferObject (c ^. caseOn)
|
||||
case vType of
|
||||
ObjectCoproduct Coproduct {..} -> do
|
||||
ctx <- ask @CheckingEnv
|
||||
leftType <-
|
||||
local
|
||||
(const (Context.cons _coproductLeft ctx))
|
||||
(inferObject (c ^. caseLeft))
|
||||
rightType <-
|
||||
local
|
||||
(const (Context.cons _coproductRight ctx))
|
||||
(inferObject (c ^. caseRight))
|
||||
checkTypesEqual leftType rightType
|
||||
return leftType
|
||||
_ ->
|
||||
throw $
|
||||
CheckingErrorExpectedType
|
||||
ExpectedType
|
||||
{ _expectedTypeObject = vType,
|
||||
_expectedTypeKind = "coproduct"
|
||||
}
|
||||
|
||||
inferObjectFirst :: (InferEffects r) => First -> Sem r Object
|
||||
inferObjectFirst p = do
|
||||
pairType <- inferObject (p ^. firstValue)
|
||||
case pairType of
|
||||
ObjectProduct Product {..} ->
|
||||
return _productLeft
|
||||
_ ->
|
||||
throw $
|
||||
CheckingErrorExpectedType
|
||||
ExpectedType
|
||||
{ _expectedTypeObject = pairType,
|
||||
_expectedTypeKind = "product"
|
||||
}
|
||||
|
||||
inferObjectSecond :: (InferEffects r) => Second -> Sem r Object
|
||||
inferObjectSecond p = do
|
||||
pairType <- inferObject (p ^. secondValue)
|
||||
case pairType of
|
||||
ObjectProduct Product {..} ->
|
||||
return _productRight
|
||||
_ ->
|
||||
throw $
|
||||
CheckingErrorExpectedType
|
||||
ExpectedType
|
||||
{ _expectedTypeObject = pairType,
|
||||
_expectedTypeKind = "product"
|
||||
}
|
||||
|
||||
inferObjectVar :: (InferEffects r) => Var -> Sem r Object
|
||||
inferObjectVar v = do
|
||||
ctx <- ask @CheckingEnv
|
||||
return $ Context.lookup (v ^. varIndex) ctx
|
||||
|
||||
inferObjectBinop :: (InferEffects r) => Binop -> Sem r Object
|
||||
inferObjectBinop opApp = do
|
||||
let outTy = objectBinop opApp
|
||||
leftArg = opApp ^. binopLeft
|
||||
rightArg = opApp ^. binopRight
|
||||
args = [leftArg, rightArg]
|
||||
|
||||
case opApp ^. binopOpcode of
|
||||
OpAdd -> do
|
||||
checkListSameType args ObjectInteger
|
||||
return outTy
|
||||
OpSub -> do
|
||||
checkListSameType args ObjectInteger
|
||||
return outTy
|
||||
OpMul -> do
|
||||
checkListSameType args ObjectInteger
|
||||
return outTy
|
||||
OpDiv -> do
|
||||
checkListSameType args ObjectInteger
|
||||
return outTy
|
||||
OpMod -> do
|
||||
checkListSameType args ObjectInteger
|
||||
return outTy
|
||||
OpLt -> do
|
||||
checkListSameType args ObjectInteger
|
||||
return outTy
|
||||
OpEq -> do
|
||||
checkSameType args
|
||||
return outTy
|
||||
|
||||
inferObjectLeft :: (InferEffects r) => LeftInj -> Sem r Object
|
||||
inferObjectLeft LeftInj {..} = do
|
||||
lType <- inferObject _leftInjValue
|
||||
return $
|
||||
ObjectCoproduct $
|
||||
Coproduct
|
||||
{ _coproductLeft = lType,
|
||||
_coproductRight = _leftInjRightType
|
||||
}
|
||||
|
||||
inferObjectRight :: (InferEffects r) => RightInj -> Sem r Object
|
||||
inferObjectRight RightInj {..} = do
|
||||
rType <- inferObject _rightInjValue
|
||||
return $
|
||||
ObjectCoproduct $
|
||||
Coproduct
|
||||
{ _coproductLeft = _rightInjLeftType,
|
||||
_coproductRight = rType
|
||||
}
|
@ -1,166 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Analysis.TypeChecking.Error where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Language
|
||||
import Juvix.Compiler.Backend.Geb.Pretty
|
||||
|
||||
-- | Errors that can occur during type checking / inference
|
||||
data CheckingError
|
||||
= CheckingErrorTypeMismatch TypeMismatch
|
||||
| CheckingErrorExpectedType ExpectedType
|
||||
| CheckingErrorLackOfInformation LackOfInformation
|
||||
| CheckingErrorWrongObject WrongObject
|
||||
deriving stock (Show, Eq)
|
||||
|
||||
data TypeMismatch = TypeMismatch
|
||||
{ _typeMismatchExpected :: Object,
|
||||
_typeMismatchActual :: Object
|
||||
}
|
||||
deriving stock (Show, Eq)
|
||||
|
||||
data ExpectedType = ExpectedType
|
||||
{ _expectedTypeObject :: Object,
|
||||
_expectedTypeKind :: Text
|
||||
}
|
||||
deriving stock (Show, Eq)
|
||||
|
||||
data LackOfInformation = LackOfInformation
|
||||
{ _lackOfInformationMorphism :: Maybe Morphism,
|
||||
_lacOfInformationHelperObject :: Maybe Object,
|
||||
_lackOfInformationMessage :: String
|
||||
}
|
||||
deriving stock (Show, Eq)
|
||||
|
||||
data WrongObject = WrongObject
|
||||
{ _wrongObjectExpected :: Maybe Object,
|
||||
_wrongObjectActual :: Maybe Object,
|
||||
_wrongObjectMorphism :: Morphism,
|
||||
_wrongObjectMessage :: String
|
||||
}
|
||||
deriving stock (Show, Eq)
|
||||
|
||||
makeLenses ''TypeMismatch
|
||||
makeLenses ''ExpectedType
|
||||
makeLenses ''LackOfInformation
|
||||
makeLenses ''WrongObject
|
||||
|
||||
instance ToGenericError TypeMismatch where
|
||||
genericError e = ask >>= generr
|
||||
where
|
||||
generr opts =
|
||||
return
|
||||
GenericError
|
||||
{ _genericErrorLoc = defaultLoc,
|
||||
_genericErrorMessage = ppOutput msg,
|
||||
_genericErrorIntervals = [defaultLoc]
|
||||
}
|
||||
where
|
||||
opts' = fromGenericOptions opts
|
||||
expected = e ^. typeMismatchExpected
|
||||
actual = e ^. typeMismatchActual
|
||||
msg =
|
||||
"Object:"
|
||||
<> line
|
||||
<> ppCode' opts' actual
|
||||
<> line
|
||||
<> "is expected to be equal to:"
|
||||
<> line
|
||||
<> ppCode' opts' expected
|
||||
|
||||
instance ToGenericError ExpectedType where
|
||||
genericError e = ask >>= generr
|
||||
where
|
||||
generr opts =
|
||||
return
|
||||
GenericError
|
||||
{ _genericErrorLoc = defaultLoc,
|
||||
_genericErrorMessage = ppOutput msg,
|
||||
_genericErrorIntervals = [defaultLoc]
|
||||
}
|
||||
where
|
||||
opts' = fromGenericOptions opts
|
||||
expected = e ^. expectedTypeObject
|
||||
msg =
|
||||
"Expected "
|
||||
<> pretty (e ^. expectedTypeKind)
|
||||
<> ", got:"
|
||||
<> line
|
||||
<> ppCode' opts' expected
|
||||
|
||||
instance ToGenericError LackOfInformation where
|
||||
genericError e = ask >>= generr
|
||||
where
|
||||
generr opts =
|
||||
return
|
||||
GenericError
|
||||
{ _genericErrorLoc = defaultLoc,
|
||||
_genericErrorMessage = ppOutput msg,
|
||||
_genericErrorIntervals = [defaultLoc]
|
||||
}
|
||||
where
|
||||
opts' = fromGenericOptions opts
|
||||
morph = e ^. lackOfInformationMorphism
|
||||
obj = e ^. lacOfInformationHelperObject
|
||||
msg =
|
||||
"Lack of information:"
|
||||
<> line
|
||||
<> indent' (pretty (e ^. lackOfInformationMessage))
|
||||
<> case morph of
|
||||
Nothing -> mempty
|
||||
Just m ->
|
||||
line
|
||||
<> "The morphism:"
|
||||
<> line
|
||||
<> indent' (ppCode' opts' m)
|
||||
<> case obj of
|
||||
Nothing -> mempty
|
||||
Just o ->
|
||||
line
|
||||
<> "The object:"
|
||||
<> line
|
||||
<> indent' (ppCode' opts' o)
|
||||
|
||||
instance ToGenericError WrongObject where
|
||||
genericError e = ask >>= generr
|
||||
where
|
||||
generr opts =
|
||||
return
|
||||
GenericError
|
||||
{ _genericErrorLoc = defaultLoc,
|
||||
_genericErrorMessage = ppOutput msg,
|
||||
_genericErrorIntervals = [defaultLoc]
|
||||
}
|
||||
where
|
||||
opts' = fromGenericOptions opts
|
||||
msg =
|
||||
pretty (e ^. wrongObjectMessage)
|
||||
<> line
|
||||
<> "The morphism:"
|
||||
<> line
|
||||
<> indent' (ppCode' opts' (e ^. wrongObjectMorphism))
|
||||
<> case e ^. wrongObjectExpected of
|
||||
Nothing -> mempty
|
||||
Just o ->
|
||||
line
|
||||
<> "The expected object:"
|
||||
<> line
|
||||
<> indent' (ppCode' opts' o)
|
||||
<> case e ^. wrongObjectActual of
|
||||
Nothing -> mempty
|
||||
Just o ->
|
||||
line
|
||||
<> "The actual object:"
|
||||
<> line
|
||||
<> indent' (ppCode' opts' o)
|
||||
|
||||
instance ToGenericError CheckingError where
|
||||
genericError = \case
|
||||
CheckingErrorTypeMismatch e -> genericError e
|
||||
CheckingErrorExpectedType e -> genericError e
|
||||
CheckingErrorLackOfInformation e -> genericError e
|
||||
CheckingErrorWrongObject e -> genericError e
|
||||
|
||||
mockFile :: Path Abs File
|
||||
mockFile = $(mkAbsFile "/geb-checking-error")
|
||||
|
||||
defaultLoc :: Interval
|
||||
defaultLoc = singletonInterval (mkInitialLoc mockFile)
|
@ -1,9 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Data.Context
|
||||
( module Juvix.Compiler.Backend.Geb.Data.Context,
|
||||
module Juvix.Compiler.Core.Data.BinderList,
|
||||
)
|
||||
where
|
||||
|
||||
import Juvix.Compiler.Core.Data.BinderList
|
||||
|
||||
type Context a = BinderList a
|
@ -1,350 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Evaluator
|
||||
( module Juvix.Compiler.Backend.Geb.Evaluator,
|
||||
module Juvix.Compiler.Backend.Geb.Evaluator.Options,
|
||||
module Juvix.Compiler.Backend.Geb.Evaluator.Data,
|
||||
)
|
||||
where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Data.Context as Context
|
||||
import Juvix.Compiler.Backend.Geb.Evaluator.Data
|
||||
import Juvix.Compiler.Backend.Geb.Evaluator.Error
|
||||
import Juvix.Compiler.Backend.Geb.Evaluator.Options
|
||||
import Juvix.Compiler.Backend.Geb.Extra
|
||||
import Juvix.Compiler.Backend.Geb.Language
|
||||
import Juvix.Compiler.Backend.Geb.Translation.FromSource as Geb
|
||||
|
||||
data RunEvalArgs = RunEvalArgs
|
||||
{ _runEvalArgsInputFile :: Path Abs File,
|
||||
_runEvalArgsContent :: Text,
|
||||
_runEvalArgsEvaluatorOptions :: EvaluatorOptions
|
||||
}
|
||||
|
||||
makeLenses ''RunEvalArgs
|
||||
|
||||
runEval :: RunEvalArgs -> Either JuvixError RunEvalResult
|
||||
runEval RunEvalArgs {..} = do
|
||||
case Geb.runParser _runEvalArgsInputFile _runEvalArgsContent of
|
||||
Left err -> Left (JuvixError err)
|
||||
Right m' -> do
|
||||
let env :: Env =
|
||||
Env
|
||||
{ _envEvaluatorOptions = _runEvalArgsEvaluatorOptions,
|
||||
_envContext = mempty
|
||||
}
|
||||
let outputFormat morph
|
||||
| _runEvalArgsEvaluatorOptions ^. evaluatorOptionsOutputMorphism =
|
||||
RunEvalResultMorphism <$> evalAndOutputMorphism' env morph
|
||||
| otherwise = RunEvalResultGebValue <$> eval' env morph
|
||||
|
||||
case m' of
|
||||
ExpressionObject _ -> Left (error @JuvixError objNoEvalMsg)
|
||||
ExpressionTypedMorphism tyMorph ->
|
||||
outputFormat (tyMorph ^. typedMorphism)
|
||||
ExpressionMorphism m -> outputFormat m
|
||||
|
||||
objNoEvalMsg :: Text
|
||||
objNoEvalMsg = "Geb objects cannot be evaluated, only morphisms."
|
||||
|
||||
eval' :: Env -> Morphism -> Either JuvixError GebValue
|
||||
eval' env m =
|
||||
run . runError $
|
||||
mapError (JuvixError @EvalError) $
|
||||
runReader env $
|
||||
eval m
|
||||
|
||||
evalAndOutputMorphism' :: Env -> Morphism -> Either JuvixError Morphism
|
||||
evalAndOutputMorphism' env m = run . runError $ runReader env (evalAndOutputMorphism m)
|
||||
|
||||
evalAndOutputMorphism ::
|
||||
(Members '[Reader Env, Error JuvixError] r) =>
|
||||
Morphism ->
|
||||
Sem r Morphism
|
||||
evalAndOutputMorphism m = do
|
||||
val :: GebValue <- mapError (JuvixError @EvalError) $ eval m
|
||||
return $ quote val
|
||||
|
||||
type EvalEffects r = Members '[Reader Env, Error EvalError] r
|
||||
|
||||
eval :: (EvalEffects r) => Morphism -> Sem r GebValue
|
||||
eval morph =
|
||||
case morph of
|
||||
MorphismAbsurd x -> evalAbsurd x
|
||||
MorphismApplication app -> evalApp app
|
||||
MorphismBinop op -> evalBinop op
|
||||
MorphismCase c -> evalCase c
|
||||
MorphismFirst f -> evalFirst f
|
||||
MorphismInteger i -> evalBitChoice i
|
||||
MorphismLambda l -> evalLambda l
|
||||
MorphismLeft m -> evalLeftInj m
|
||||
MorphismPair p -> evalPair p
|
||||
MorphismRight m -> evalRightInj m
|
||||
MorphismSecond s -> evalSecond s
|
||||
MorphismUnit -> return GebValueMorphismUnit
|
||||
MorphismVar x -> evalVar x
|
||||
MorphismFail x -> evalFail x
|
||||
|
||||
evalBitChoice :: BitChoice -> Sem r GebValue
|
||||
evalBitChoice n = do
|
||||
return (GebValueMorphismInteger (n ^. bitChoice))
|
||||
|
||||
evalVar :: (EvalEffects r) => Var -> Sem r GebValue
|
||||
evalVar var = do
|
||||
ctx <- asks (^. envContext)
|
||||
let val = Context.lookup (var ^. varIndex) ctx
|
||||
return val
|
||||
|
||||
evalAbsurd :: (EvalEffects r) => Absurd -> Sem r GebValue
|
||||
evalAbsurd morph =
|
||||
throw
|
||||
EvalError
|
||||
{ _evalErrorMsg = "Absurd can not be evaluated.",
|
||||
_evalErrorGebValue = Nothing,
|
||||
_evalErrorGebExpression = Just $ MorphismAbsurd morph
|
||||
}
|
||||
|
||||
evalPair :: (EvalEffects r) => Pair -> Sem r GebValue
|
||||
evalPair pair = do
|
||||
left <- eval $ pair ^. pairLeft
|
||||
right <- eval $ pair ^. pairRight
|
||||
return $
|
||||
GebValueMorphismPair $
|
||||
Pair
|
||||
{ _pairLeft = left,
|
||||
_pairRight = right
|
||||
}
|
||||
|
||||
evalFirst :: (EvalEffects r) => First -> Sem r GebValue
|
||||
evalFirst f = do
|
||||
res <- eval $ f ^. firstValue
|
||||
case res of
|
||||
GebValueMorphismPair pair -> return $ pair ^. pairLeft
|
||||
_ ->
|
||||
throw
|
||||
EvalError
|
||||
{ _evalErrorMsg = "First can only be applied to pairs.",
|
||||
_evalErrorGebValue = Nothing,
|
||||
_evalErrorGebExpression = Just (MorphismFirst f)
|
||||
}
|
||||
|
||||
evalSecond :: (EvalEffects r) => Second -> Sem r GebValue
|
||||
evalSecond s = do
|
||||
res <- eval $ s ^. secondValue
|
||||
case res of
|
||||
GebValueMorphismPair pair -> return $ pair ^. pairRight
|
||||
_ ->
|
||||
throw
|
||||
EvalError
|
||||
{ _evalErrorMsg = "Second can only be applied to pairs.",
|
||||
_evalErrorGebValue = Just res,
|
||||
_evalErrorGebExpression = Just (MorphismSecond s)
|
||||
}
|
||||
|
||||
evalLeftInj :: (EvalEffects r) => LeftInj -> Sem r GebValue
|
||||
evalLeftInj s = do
|
||||
res <- eval $ s ^. leftInjValue
|
||||
return $
|
||||
GebValueMorphismLeft $
|
||||
LeftInj
|
||||
{ _leftInjValue = res,
|
||||
_leftInjRightType = s ^. leftInjRightType
|
||||
}
|
||||
|
||||
evalRightInj :: (EvalEffects r) => RightInj -> Sem r GebValue
|
||||
evalRightInj s = do
|
||||
res <- eval $ s ^. rightInjValue
|
||||
return $
|
||||
GebValueMorphismRight $
|
||||
RightInj
|
||||
{ _rightInjValue = res,
|
||||
_rightInjLeftType = s ^. rightInjLeftType
|
||||
}
|
||||
|
||||
evalApp :: (EvalEffects r) => Application -> Sem r GebValue
|
||||
evalApp app = do
|
||||
arg <- eval (app ^. applicationRight)
|
||||
apply (app ^. applicationLeft) arg
|
||||
|
||||
apply ::
|
||||
(EvalEffects r) =>
|
||||
Morphism ->
|
||||
GebValue ->
|
||||
Sem r GebValue
|
||||
apply fun' arg = do
|
||||
fun <- eval fun'
|
||||
case fun of
|
||||
GebValueClosure cls ->
|
||||
do
|
||||
let clsEnv = cls ^. valueClosureEnv
|
||||
bodyEnv = Context.cons arg clsEnv
|
||||
local (set envContext bodyEnv) $
|
||||
eval (cls ^. valueClosureLambda . lambdaBody)
|
||||
_ ->
|
||||
throw $
|
||||
EvalError
|
||||
{ _evalErrorMsg = "Can only apply functions.",
|
||||
_evalErrorGebValue = (Just fun),
|
||||
_evalErrorGebExpression = Nothing
|
||||
}
|
||||
|
||||
evalExtendContext :: (EvalEffects r) => GebValue -> Morphism -> Sem r GebValue
|
||||
evalExtendContext v m = do
|
||||
ctx <- asks (^. envContext)
|
||||
local (set envContext (Context.cons v ctx)) $
|
||||
eval m
|
||||
|
||||
evalLambda :: (EvalEffects r) => Lambda -> Sem r GebValue
|
||||
evalLambda lambda = do
|
||||
ctx <- asks (^. envContext)
|
||||
return $
|
||||
GebValueClosure $
|
||||
ValueClosure
|
||||
{ _valueClosureLambda = lambda,
|
||||
_valueClosureEnv = ctx
|
||||
}
|
||||
|
||||
evalCase :: (EvalEffects r) => Case -> Sem r GebValue
|
||||
evalCase c = do
|
||||
vCaseOn <- eval $ c ^. caseOn
|
||||
case vCaseOn of
|
||||
GebValueMorphismLeft leftArg -> evalExtendContext (leftArg ^. leftInjValue) (c ^. caseLeft)
|
||||
GebValueMorphismRight rightArg -> evalExtendContext (rightArg ^. rightInjValue) (c ^. caseRight)
|
||||
_ ->
|
||||
throw
|
||||
EvalError
|
||||
{ _evalErrorMsg = "Case can only be applied to terms of the coproduct object.",
|
||||
_evalErrorGebValue = Just vCaseOn,
|
||||
_evalErrorGebExpression = Just (MorphismCase c)
|
||||
}
|
||||
|
||||
evalBinop ::
|
||||
(EvalEffects r) =>
|
||||
Binop ->
|
||||
Sem r GebValue
|
||||
evalBinop binop = do
|
||||
left <- eval $ binop ^. binopLeft
|
||||
right <- eval $ binop ^. binopRight
|
||||
let lfPair m1 m2 =
|
||||
( GebValueMorphismPair
|
||||
( Pair
|
||||
{ _pairLeft = m1,
|
||||
_pairRight = m2
|
||||
}
|
||||
)
|
||||
)
|
||||
case (left, right) of
|
||||
(GebValueMorphismInteger l, GebValueMorphismInteger r) ->
|
||||
case binop ^. binopOpcode of
|
||||
OpAdd -> return $ GebValueMorphismInteger $ l + r
|
||||
OpSub -> return $ GebValueMorphismInteger $ l - r
|
||||
OpMul -> return $ GebValueMorphismInteger $ l * r
|
||||
OpDiv -> return $ GebValueMorphismInteger $ l `div` r
|
||||
OpMod -> return $ GebValueMorphismInteger $ l `mod` r
|
||||
OpLt ->
|
||||
if
|
||||
| l < r -> return valueTrue
|
||||
| otherwise -> return valueFalse
|
||||
OpEq ->
|
||||
if
|
||||
| l == r -> return valueTrue
|
||||
| otherwise -> return valueFalse
|
||||
(m1, m2) -> case binop ^. binopOpcode of
|
||||
OpEq ->
|
||||
if
|
||||
| sameKind m1 m2 ->
|
||||
if
|
||||
| m1 == m2 -> return valueTrue
|
||||
| otherwise -> return valueFalse
|
||||
| otherwise ->
|
||||
throw
|
||||
EvalError
|
||||
{ _evalErrorMsg = "Equality can only be applied to values of the same kind.",
|
||||
_evalErrorGebValue = Just (lfPair m1 m2),
|
||||
_evalErrorGebExpression = (Just (MorphismBinop binop))
|
||||
}
|
||||
_ ->
|
||||
throw
|
||||
EvalError
|
||||
{ _evalErrorMsg = "Cannot apply operation",
|
||||
_evalErrorGebValue = Just (lfPair m1 m2),
|
||||
_evalErrorGebExpression = Just (MorphismBinop binop)
|
||||
}
|
||||
|
||||
evalFail :: (EvalEffects r) => Failure -> Sem r GebValue
|
||||
evalFail Failure {..} =
|
||||
throw
|
||||
EvalError
|
||||
{ _evalErrorMsg = "failure: " <> _failureMessage,
|
||||
_evalErrorGebValue = Nothing,
|
||||
_evalErrorGebExpression = Nothing
|
||||
}
|
||||
|
||||
sameKind :: GebValue -> GebValue -> Bool
|
||||
sameKind l r = case (l, r) of
|
||||
(GebValueMorphismInteger _, GebValueMorphismInteger _) -> True
|
||||
(GebValueMorphismUnit, GebValueMorphismUnit) -> True
|
||||
(GebValueMorphismLeft _, GebValueMorphismLeft _) -> True
|
||||
(GebValueMorphismRight _, GebValueMorphismRight _) -> True
|
||||
(GebValueMorphismPair _, GebValueMorphismPair _) -> True
|
||||
(GebValueClosure _, GebValueClosure _) -> True
|
||||
_ -> False
|
||||
|
||||
valueTrue :: GebValue
|
||||
valueTrue =
|
||||
GebValueMorphismLeft $
|
||||
LeftInj
|
||||
{ _leftInjValue = GebValueMorphismUnit,
|
||||
_leftInjRightType = ObjectTerminal
|
||||
}
|
||||
|
||||
valueFalse :: GebValue
|
||||
valueFalse =
|
||||
GebValueMorphismRight $
|
||||
RightInj
|
||||
{ _rightInjValue = GebValueMorphismUnit,
|
||||
_rightInjLeftType = ObjectTerminal
|
||||
}
|
||||
|
||||
quote :: GebValue -> Morphism
|
||||
quote = \case
|
||||
GebValueClosure cls -> quoteClosure cls
|
||||
GebValueMorphismInteger i -> quoteBitChoice i
|
||||
GebValueMorphismLeft m -> quoteValueMorphismLeft m
|
||||
GebValueMorphismPair m -> quoteValueMorphismPair m
|
||||
GebValueMorphismRight m -> quoteValueMorphismRight m
|
||||
GebValueMorphismUnit -> MorphismUnit
|
||||
|
||||
quoteBitChoice :: Integer -> Morphism
|
||||
quoteBitChoice n = MorphismInteger (BitChoice {_bitChoice = n})
|
||||
|
||||
quoteClosure :: ValueClosure -> Morphism
|
||||
quoteClosure cls =
|
||||
let env = map quote (toList (cls ^. valueClosureEnv))
|
||||
in substs env (MorphismLambda (cls ^. valueClosureLambda))
|
||||
|
||||
quoteValueMorphismPair :: ValuePair -> Morphism
|
||||
quoteValueMorphismPair vpair =
|
||||
let pLeft = quote (vpair ^. pairLeft)
|
||||
pRight = quote (vpair ^. pairRight)
|
||||
in MorphismPair
|
||||
Pair
|
||||
{ _pairLeft = pLeft,
|
||||
_pairRight = pRight
|
||||
}
|
||||
|
||||
quoteValueMorphismLeft :: ValueLeftInj -> Morphism
|
||||
quoteValueMorphismLeft m =
|
||||
let leftMorphism = quote (m ^. leftInjValue)
|
||||
in MorphismLeft
|
||||
LeftInj
|
||||
{ _leftInjValue = leftMorphism,
|
||||
_leftInjRightType = m ^. leftInjRightType
|
||||
}
|
||||
|
||||
quoteValueMorphismRight :: ValueRightInj -> Morphism
|
||||
quoteValueMorphismRight m =
|
||||
let rightMorphism = quote (m ^. rightInjValue)
|
||||
in MorphismRight
|
||||
RightInj
|
||||
{ _rightInjValue = rightMorphism,
|
||||
_rightInjLeftType = m ^. rightInjLeftType
|
||||
}
|
@ -1,10 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Evaluator.Data
|
||||
( module Juvix.Compiler.Backend.Geb.Evaluator.Data.Env,
|
||||
module Juvix.Compiler.Backend.Geb.Evaluator.Data.Values,
|
||||
module Juvix.Compiler.Backend.Geb.Evaluator.Data.RunEvalResult,
|
||||
)
|
||||
where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Evaluator.Data.Env
|
||||
import Juvix.Compiler.Backend.Geb.Evaluator.Data.RunEvalResult
|
||||
import Juvix.Compiler.Backend.Geb.Evaluator.Data.Values
|
@ -1,20 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Evaluator.Data.Env where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Data.Context as Context
|
||||
import Juvix.Compiler.Backend.Geb.Evaluator.Data.Values
|
||||
import Juvix.Compiler.Backend.Geb.Evaluator.Options
|
||||
import Juvix.Compiler.Backend.Geb.Language
|
||||
|
||||
data Env = Env
|
||||
{ _envEvaluatorOptions :: EvaluatorOptions,
|
||||
_envContext :: Context GebValue
|
||||
}
|
||||
|
||||
makeLenses ''Env
|
||||
|
||||
defaultEvalEnv :: Env
|
||||
defaultEvalEnv =
|
||||
Env
|
||||
{ _envEvaluatorOptions = defaultEvaluatorOptions,
|
||||
_envContext = mempty
|
||||
}
|
@ -1,13 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Evaluator.Data.RunEvalResult (module Juvix.Compiler.Backend.Geb.Evaluator.Data.RunEvalResult) where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Evaluator.Data.Values
|
||||
import Juvix.Compiler.Backend.Geb.Language
|
||||
|
||||
data RunEvalResult
|
||||
= RunEvalResultGebValue GebValue
|
||||
| RunEvalResultMorphism Morphism
|
||||
deriving stock (Show, Eq)
|
||||
|
||||
instance HasAtomicity RunEvalResult where
|
||||
atomicity (RunEvalResultGebValue v) = atomicity v
|
||||
atomicity (RunEvalResultMorphism m) = atomicity m
|
@ -1,36 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Evaluator.Data.Values where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Data.Context as Context
|
||||
import Juvix.Compiler.Backend.Geb.Language hiding (show)
|
||||
|
||||
type ValueLeftInj = LeftInj' GebValue
|
||||
|
||||
type ValueRightInj = RightInj' GebValue
|
||||
|
||||
type ValuePair = Pair' GebValue
|
||||
|
||||
data GebValue
|
||||
= GebValueMorphismUnit
|
||||
| GebValueMorphismInteger Integer
|
||||
| GebValueMorphismLeft ValueLeftInj
|
||||
| GebValueMorphismRight ValueRightInj
|
||||
| GebValueMorphismPair ValuePair
|
||||
| GebValueClosure ValueClosure
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
data ValueClosure = ValueClosure
|
||||
{ _valueClosureEnv :: Context GebValue,
|
||||
_valueClosureLambda :: Lambda
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
instance HasAtomicity GebValue where
|
||||
atomicity = \case
|
||||
GebValueMorphismInteger {} -> Atom
|
||||
GebValueMorphismLeft {} -> Aggregate appFixity
|
||||
GebValueMorphismPair {} -> Aggregate appFixity
|
||||
GebValueMorphismRight {} -> Aggregate appFixity
|
||||
GebValueMorphismUnit -> Atom
|
||||
GebValueClosure {} -> Aggregate appFixity
|
||||
|
||||
makeLenses ''ValueClosure
|
@ -1,86 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Evaluator.Error where
|
||||
|
||||
import GHC.Exception qualified as Exception
|
||||
import GHC.Show qualified as S
|
||||
import Juvix.Compiler.Backend.Geb.Evaluator.Data.Values
|
||||
import Juvix.Compiler.Backend.Geb.Language
|
||||
import Juvix.Compiler.Backend.Geb.Pretty
|
||||
|
||||
data EvalError = EvalError
|
||||
{ _evalErrorMsg :: !Text,
|
||||
_evalErrorGebValue :: !(Maybe GebValue),
|
||||
_evalErrorGebExpression :: !(Maybe Morphism)
|
||||
}
|
||||
|
||||
data QuoteError = QuoteError
|
||||
{ _quoteErrorMsg :: Text,
|
||||
_quoteErrorGebValue :: Maybe GebValue,
|
||||
_quoteErrorGebExpression :: Maybe Object
|
||||
}
|
||||
|
||||
makeLenses ''EvalError
|
||||
makeLenses ''QuoteError
|
||||
|
||||
-- TODO: Make this a proper error with a location
|
||||
instance ToGenericError EvalError where
|
||||
genericError e =
|
||||
return
|
||||
GenericError
|
||||
{ _genericErrorLoc = defaultLoc,
|
||||
_genericErrorMessage = mkAnsiText (pack (S.show e)),
|
||||
_genericErrorIntervals = []
|
||||
}
|
||||
|
||||
mockFile :: Path Abs File
|
||||
mockFile = $(mkAbsFile "/geb-eval-error")
|
||||
|
||||
defaultLoc :: Interval
|
||||
defaultLoc = singletonInterval (mkInitialLoc mockFile)
|
||||
|
||||
instance Show EvalError where
|
||||
show :: EvalError -> String
|
||||
show (EvalError {..}) =
|
||||
"evaluation error: "
|
||||
<> fromText _evalErrorMsg
|
||||
<> "\n"
|
||||
<> case _evalErrorGebValue of
|
||||
Nothing -> ""
|
||||
Just val -> "Value:\n" <> fromText (ppTrace val)
|
||||
<> "\n"
|
||||
<> case _evalErrorGebExpression of
|
||||
Nothing -> ""
|
||||
Just expr ->
|
||||
"Morphism:\n"
|
||||
<> fromText (ppTrace expr)
|
||||
<> "\n"
|
||||
|
||||
evalError ::
|
||||
(Member (Error JuvixError) r) =>
|
||||
Text ->
|
||||
Maybe GebValue ->
|
||||
Maybe Morphism ->
|
||||
Sem r a
|
||||
evalError msg val m =
|
||||
throw . JuvixError $
|
||||
( EvalError
|
||||
{ _evalErrorMsg = msg,
|
||||
_evalErrorGebValue = val,
|
||||
_evalErrorGebExpression = m
|
||||
}
|
||||
)
|
||||
|
||||
instance Exception.Exception QuoteError
|
||||
|
||||
instance Show QuoteError where
|
||||
show :: QuoteError -> String
|
||||
show QuoteError {..} =
|
||||
"Quote error: "
|
||||
<> fromText _quoteErrorMsg
|
||||
<> case _quoteErrorGebValue of
|
||||
Nothing -> ""
|
||||
Just val -> ": " <> fromText (ppTrace val)
|
||||
<> case _quoteErrorGebExpression of
|
||||
Nothing -> ""
|
||||
Just expr ->
|
||||
"GebObject associated:\n"
|
||||
<> fromText (ppTrace expr)
|
@ -1,19 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Evaluator.Options where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Pretty qualified as Geb
|
||||
import Juvix.Prelude
|
||||
|
||||
newtype EvaluatorOptions = EvaluatorOptions
|
||||
{ _evaluatorOptionsOutputMorphism :: Bool
|
||||
}
|
||||
|
||||
makeLenses ''EvaluatorOptions
|
||||
|
||||
instance CanonicalProjection EvaluatorOptions Geb.Options where
|
||||
project _ = Geb.defaultOptions
|
||||
|
||||
defaultEvaluatorOptions :: EvaluatorOptions
|
||||
defaultEvaluatorOptions =
|
||||
EvaluatorOptions
|
||||
{ _evaluatorOptionsOutputMorphism = False
|
||||
}
|
@ -1,97 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Extra where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Language
|
||||
|
||||
-- | Destructs a product in a right-associative way, e.g., (a, (b, c)) is
|
||||
-- destructed to [a, b, c]
|
||||
destructProduct :: Object -> [Object]
|
||||
destructProduct = \case
|
||||
ObjectProduct Product {..} -> _productLeft : destructProduct _productRight
|
||||
x -> [x]
|
||||
|
||||
objectBool :: Object
|
||||
objectBool = ObjectCoproduct (Coproduct ObjectTerminal ObjectTerminal)
|
||||
|
||||
morphismTrue :: Morphism
|
||||
morphismTrue =
|
||||
MorphismLeft
|
||||
LeftInj
|
||||
{ _leftInjRightType = ObjectTerminal,
|
||||
_leftInjValue = MorphismUnit
|
||||
}
|
||||
|
||||
morphismFalse :: Morphism
|
||||
morphismFalse =
|
||||
MorphismRight
|
||||
RightInj
|
||||
{ _rightInjLeftType = ObjectTerminal,
|
||||
_rightInjValue = MorphismUnit
|
||||
}
|
||||
|
||||
-- | NOTE: `arg2` needs to be shifted by 1!
|
||||
mkOr :: Morphism -> Morphism -> Morphism
|
||||
mkOr arg1 arg2 =
|
||||
MorphismCase
|
||||
Case
|
||||
{ _caseOn = arg1,
|
||||
_caseLeft = morphismTrue,
|
||||
_caseRight = arg2
|
||||
}
|
||||
|
||||
mkHoms :: [Object] -> Object -> Object
|
||||
mkHoms argtys codty = case argtys of
|
||||
[] -> codty
|
||||
ty : tys ->
|
||||
ObjectHom $
|
||||
Hom
|
||||
{ _homDomain = ty,
|
||||
_homCodomain = (mkHoms tys codty)
|
||||
}
|
||||
|
||||
objectBinop :: Binop -> Object
|
||||
objectBinop op = case op ^. binopOpcode of
|
||||
OpAdd -> ObjectInteger
|
||||
OpSub -> ObjectInteger
|
||||
OpMul -> ObjectInteger
|
||||
OpDiv -> ObjectInteger
|
||||
OpMod -> ObjectInteger
|
||||
OpEq -> objectBool
|
||||
OpLt -> objectBool
|
||||
|
||||
mapVars :: (Int -> Var -> Morphism) -> Morphism -> Morphism
|
||||
mapVars f m = go 0 m
|
||||
where
|
||||
go :: Int -> Morphism -> Morphism
|
||||
go k = \case
|
||||
MorphismAbsurd x -> MorphismAbsurd (over absurdValue (go k) x)
|
||||
MorphismUnit -> MorphismUnit
|
||||
MorphismLeft x -> MorphismLeft (over leftInjValue (go k) x)
|
||||
MorphismRight x -> MorphismRight (over rightInjValue (go k) x)
|
||||
MorphismCase x -> MorphismCase (over caseOn (go k) (over caseLeft (go k) (over caseRight (go k) x)))
|
||||
MorphismPair x -> MorphismPair (over pairLeft (go k) (over pairRight (go k) x))
|
||||
MorphismFirst x -> MorphismFirst (over firstValue (go k) x)
|
||||
MorphismSecond x -> MorphismSecond (over secondValue (go k) x)
|
||||
MorphismLambda x -> MorphismLambda (over lambdaBody (go (k + 1)) x)
|
||||
MorphismApplication x -> MorphismApplication (over applicationLeft (go k) (over applicationRight (go k) x))
|
||||
MorphismVar x -> f k x
|
||||
MorphismInteger i -> MorphismInteger i
|
||||
MorphismBinop x -> MorphismBinop (over binopLeft (go k) (over binopRight (go k) x))
|
||||
MorphismFail x -> MorphismFail x
|
||||
|
||||
shift :: Int -> Morphism -> Morphism
|
||||
shift 0 m = m
|
||||
shift n m = mapVars go m
|
||||
where
|
||||
go :: Int -> Var -> Morphism
|
||||
go k v@Var {..} | _varIndex >= k = MorphismVar v {_varIndex = _varIndex + n}
|
||||
go _ v = MorphismVar v
|
||||
|
||||
substs :: [Morphism] -> Morphism -> Morphism
|
||||
substs env = mapVars go
|
||||
where
|
||||
n :: Int
|
||||
n = length env
|
||||
|
||||
go :: Int -> Var -> Morphism
|
||||
go k Var {..} | _varIndex >= k && _varIndex < k + n = shift k (env !! (_varIndex - k))
|
||||
go _ v = MorphismVar v
|
@ -1,121 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Keywords
|
||||
( module Juvix.Compiler.Backend.Geb.Keywords,
|
||||
module Juvix.Data.Keyword,
|
||||
module Juvix.Data.Keyword.All,
|
||||
)
|
||||
where
|
||||
|
||||
import Juvix.Data.Keyword
|
||||
import Juvix.Data.Keyword.All
|
||||
import Juvix.Extra.Strings qualified as Str
|
||||
import Juvix.Prelude
|
||||
|
||||
allKeywordStrings :: HashSet Text
|
||||
allKeywordStrings = keywordsStrings allKeywords
|
||||
|
||||
allKeywords :: [Keyword]
|
||||
allKeywords =
|
||||
[ kwGebMorphismAbsurd,
|
||||
kwGebMorphismUnit,
|
||||
kwGebMorphismLeft,
|
||||
kwGebMorphismRight,
|
||||
kwGebMorphismCase,
|
||||
kwGebMorphismPair,
|
||||
kwGebMorphismFirst,
|
||||
kwGebMorphismSecond,
|
||||
kwGebMorphismLambda,
|
||||
kwGebMorphismApplication,
|
||||
kwGebObjectInteger,
|
||||
kwGebBinopAdd,
|
||||
kwGebBinopSub,
|
||||
kwGebBinopMul,
|
||||
kwGebBinopDiv,
|
||||
kwGebBinopMod,
|
||||
kwGebBinopEq,
|
||||
kwGebBinopLt,
|
||||
kwGebBitChoice,
|
||||
kwGebObjectInitial,
|
||||
kwGebObjectTerminal,
|
||||
kwGebObjectProduct,
|
||||
kwGebObjectCoproduct,
|
||||
kwGebObjectHom,
|
||||
kwGebVar
|
||||
]
|
||||
|
||||
kwGebMorphismAbsurd :: Keyword
|
||||
kwGebMorphismAbsurd = asciiKw Str.gebAbsurd
|
||||
|
||||
kwGebMorphismUnit :: Keyword
|
||||
kwGebMorphismUnit = asciiKw Str.gebUnit
|
||||
|
||||
kwGebMorphismLeft :: Keyword
|
||||
kwGebMorphismLeft = asciiKw Str.gebLeft
|
||||
|
||||
kwGebMorphismRight :: Keyword
|
||||
kwGebMorphismRight = asciiKw Str.gebRight
|
||||
|
||||
kwGebMorphismCase :: Keyword
|
||||
kwGebMorphismCase = asciiKw Str.gebCase
|
||||
|
||||
kwGebMorphismPair :: Keyword
|
||||
kwGebMorphismPair = asciiKw Str.gebPair
|
||||
|
||||
kwGebMorphismFirst :: Keyword
|
||||
kwGebMorphismFirst = asciiKw Str.gebFst
|
||||
|
||||
kwGebMorphismSecond :: Keyword
|
||||
kwGebMorphismSecond = asciiKw Str.gebSnd
|
||||
|
||||
kwGebMorphismLambda :: Keyword
|
||||
kwGebMorphismLambda = asciiKw Str.gebLamb
|
||||
|
||||
kwGebMorphismApplication :: Keyword
|
||||
kwGebMorphismApplication = asciiKw Str.gebApp
|
||||
|
||||
kwGebBinopAdd :: Keyword
|
||||
kwGebBinopAdd = asciiKw Str.gebAdd
|
||||
|
||||
kwGebBinopSub :: Keyword
|
||||
kwGebBinopSub = asciiKw Str.gebSub
|
||||
|
||||
kwGebBinopMul :: Keyword
|
||||
kwGebBinopMul = asciiKw Str.gebMul
|
||||
|
||||
kwGebBinopDiv :: Keyword
|
||||
kwGebBinopDiv = asciiKw Str.gebDiv
|
||||
|
||||
kwGebBinopMod :: Keyword
|
||||
kwGebBinopMod = asciiKw Str.gebMod
|
||||
|
||||
kwGebBinopEq :: Keyword
|
||||
kwGebBinopEq = asciiKw Str.gebEq
|
||||
|
||||
kwGebBinopLt :: Keyword
|
||||
kwGebBinopLt = asciiKw Str.gebLt
|
||||
|
||||
kwGebObjectInteger :: Keyword
|
||||
kwGebObjectInteger = asciiKw Str.gebInteger
|
||||
|
||||
kwGebVar :: Keyword
|
||||
kwGebVar = asciiKw Str.gebVar
|
||||
|
||||
kwGebBitChoice :: Keyword
|
||||
kwGebBitChoice = asciiKw Str.gebBitChoice
|
||||
|
||||
kwGebObjectInitial :: Keyword
|
||||
kwGebObjectInitial = asciiKw Str.gebInitial
|
||||
|
||||
kwGebObjectTerminal :: Keyword
|
||||
kwGebObjectTerminal = asciiKw Str.gebTerminal
|
||||
|
||||
kwGebObjectProduct :: Keyword
|
||||
kwGebObjectProduct = asciiKw Str.gebProd
|
||||
|
||||
kwGebObjectCoproduct :: Keyword
|
||||
kwGebObjectCoproduct = asciiKw Str.gebCoprod
|
||||
|
||||
kwGebObjectHom :: Keyword
|
||||
kwGebObjectHom = asciiKw Str.gebHom
|
||||
|
||||
kwTyped :: Keyword
|
||||
kwTyped = asciiKw Str.gebTyped
|
@ -1,239 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Language
|
||||
( module Juvix.Compiler.Backend.Geb.Language,
|
||||
module Juvix.Prelude,
|
||||
)
|
||||
where
|
||||
|
||||
import Juvix.Prelude hiding (First, Product)
|
||||
|
||||
{-
|
||||
The following datatypes correspond to GEB types for terms
|
||||
(https://github.com/anoma/geb/blob/main/src/specs/lambda.lisp) and types
|
||||
(https://github.com/anoma/geb/blob/main/src/specs/geb.lisp).
|
||||
-}
|
||||
|
||||
-- | Represents GEB's `case-on`. `_caseOn` is the value matched on of type
|
||||
-- `_caseLeftType + _caseRightType`, `_caseLeft` has type `_caseLeftType ->
|
||||
-- _caseCodomainType` and `_caseRight` has type `_caseRightType ->
|
||||
-- _caseCodomainType`.
|
||||
data Case = Case
|
||||
{ _caseOn :: Morphism,
|
||||
_caseLeft :: Morphism,
|
||||
_caseRight :: Morphism
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
data Absurd = Absurd
|
||||
{ _absurdType :: Object,
|
||||
_absurdValue :: Morphism
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
data LeftInj' a = LeftInj
|
||||
{ _leftInjRightType :: Object,
|
||||
_leftInjValue :: a
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
type LeftInj = LeftInj' Morphism
|
||||
|
||||
data RightInj' a = RightInj
|
||||
{ _rightInjLeftType :: Object,
|
||||
_rightInjValue :: a
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
type RightInj = RightInj' Morphism
|
||||
|
||||
data Pair' a = Pair
|
||||
{ _pairLeft :: a,
|
||||
_pairRight :: a
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
type Pair = Pair' Morphism
|
||||
|
||||
newtype First = First
|
||||
{ _firstValue :: Morphism
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
newtype Second = Second
|
||||
{ _secondValue :: Morphism
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
data Lambda = Lambda
|
||||
{ _lambdaVarType :: Object,
|
||||
_lambdaBody :: Morphism
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
data Application = Application
|
||||
{ _applicationLeft :: Morphism,
|
||||
_applicationRight :: Morphism
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
newtype Var = Var
|
||||
{ _varIndex :: Int
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
data Opcode
|
||||
= OpAdd
|
||||
| OpSub
|
||||
| OpMul
|
||||
| OpDiv
|
||||
| OpMod
|
||||
| OpEq
|
||||
| OpLt
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
data Binop = Binop
|
||||
{ _binopOpcode :: Opcode,
|
||||
_binopLeft :: Morphism,
|
||||
_binopRight :: Morphism
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
data Failure = Failure
|
||||
{ _failureMessage :: Text,
|
||||
_failureType :: Object
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
newtype BitChoice = BitChoice
|
||||
{ _bitChoice :: Integer
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
-- | Corresponds to the GEB type for terms (morphisms of the category): `stlc`
|
||||
-- (https://github.com/anoma/geb/blob/main/src/specs/lambda.lisp).
|
||||
data Morphism
|
||||
= MorphismAbsurd Absurd
|
||||
| MorphismUnit
|
||||
| MorphismLeft LeftInj
|
||||
| MorphismRight RightInj
|
||||
| MorphismCase Case
|
||||
| MorphismPair Pair
|
||||
| MorphismFirst First
|
||||
| MorphismSecond Second
|
||||
| MorphismLambda Lambda
|
||||
| MorphismApplication Application
|
||||
| MorphismVar Var
|
||||
| MorphismInteger BitChoice
|
||||
| MorphismBinop Binop
|
||||
| MorphismFail Failure
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
data Product = Product
|
||||
{ _productLeft :: Object,
|
||||
_productRight :: Object
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
data Coproduct = Coproduct
|
||||
{ _coproductLeft :: Object,
|
||||
_coproductRight :: Object
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
-- | Function type
|
||||
data Hom = Hom
|
||||
{ _homDomain :: Object,
|
||||
_homCodomain :: Object
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
-- | Corresponds to the GEB type for types (objects of the category): `substobj`
|
||||
-- (https://github.com/anoma/geb/blob/main/src/specs/geb.lisp).
|
||||
data Object
|
||||
= -- | empty type
|
||||
ObjectInitial
|
||||
| -- | unit type
|
||||
ObjectTerminal
|
||||
| ObjectProduct Product
|
||||
| ObjectCoproduct Coproduct
|
||||
| -- | function type
|
||||
ObjectHom Hom
|
||||
| ObjectInteger
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
data Expression
|
||||
= ExpressionMorphism Morphism
|
||||
| ExpressionObject Object
|
||||
| ExpressionTypedMorphism TypedMorphism
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
data TypedMorphism = TypedMorphism
|
||||
{ _typedMorphism :: Morphism,
|
||||
_typedMorphismObject :: Object
|
||||
}
|
||||
deriving stock (Show, Eq, Generic)
|
||||
|
||||
instance HasAtomicity Opcode where
|
||||
atomicity OpAdd = Atom
|
||||
atomicity OpSub = Atom
|
||||
atomicity OpMul = Atom
|
||||
atomicity OpDiv = Atom
|
||||
atomicity OpMod = Atom
|
||||
atomicity OpEq = Atom
|
||||
atomicity OpLt = Atom
|
||||
|
||||
instance HasAtomicity Morphism where
|
||||
atomicity = \case
|
||||
MorphismAbsurd {} -> Aggregate appFixity
|
||||
MorphismUnit -> Atom
|
||||
MorphismLeft {} -> Aggregate appFixity
|
||||
MorphismRight {} -> Aggregate appFixity
|
||||
MorphismCase {} -> Aggregate appFixity
|
||||
MorphismPair {} -> Aggregate appFixity
|
||||
MorphismFirst {} -> Aggregate appFixity
|
||||
MorphismSecond {} -> Aggregate appFixity
|
||||
MorphismLambda {} -> Aggregate appFixity
|
||||
MorphismApplication {} -> Aggregate appFixity
|
||||
MorphismVar {} -> Aggregate appFixity
|
||||
MorphismInteger {} -> Aggregate appFixity
|
||||
MorphismBinop {} -> Aggregate appFixity
|
||||
MorphismFail {} -> Aggregate appFixity
|
||||
|
||||
instance HasAtomicity Object where
|
||||
atomicity = \case
|
||||
ObjectInitial -> Atom
|
||||
ObjectTerminal -> Atom
|
||||
ObjectProduct {} -> Aggregate appFixity
|
||||
ObjectCoproduct {} -> Aggregate appFixity
|
||||
ObjectHom {} -> Aggregate appFixity
|
||||
ObjectInteger -> Atom
|
||||
|
||||
instance HasAtomicity Expression where
|
||||
atomicity = \case
|
||||
ExpressionMorphism m -> atomicity m
|
||||
ExpressionObject o -> atomicity o
|
||||
ExpressionTypedMorphism tm -> atomicity tm
|
||||
|
||||
instance HasAtomicity TypedMorphism where
|
||||
atomicity _ = Aggregate appFixity
|
||||
|
||||
-- TODO: hasLoc
|
||||
|
||||
makeLenses ''Absurd
|
||||
makeLenses ''Application
|
||||
makeLenses ''Binop
|
||||
makeLenses ''Case
|
||||
makeLenses ''Coproduct
|
||||
makeLenses ''First
|
||||
makeLenses ''Failure
|
||||
makeLenses ''Hom
|
||||
makeLenses ''Lambda
|
||||
makeLenses ''LeftInj'
|
||||
makeLenses ''Morphism
|
||||
makeLenses ''Object
|
||||
makeLenses ''Pair'
|
||||
makeLenses ''Product
|
||||
makeLenses ''RightInj'
|
||||
makeLenses ''Second
|
||||
makeLenses ''TypedMorphism
|
||||
makeLenses ''Var
|
||||
makeLenses ''BitChoice
|
@ -1,32 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Pretty
|
||||
( module Juvix.Compiler.Backend.Geb.Pretty,
|
||||
module Juvix.Compiler.Backend.Geb.Pretty.Base,
|
||||
module Juvix.Compiler.Backend.Geb.Pretty.Options,
|
||||
module Juvix.Data.PPOutput,
|
||||
)
|
||||
where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Language
|
||||
import Juvix.Compiler.Backend.Geb.Pretty.Base
|
||||
import Juvix.Compiler.Backend.Geb.Pretty.Options
|
||||
import Juvix.Data.PPOutput
|
||||
import Prettyprinter.Render.Terminal qualified as Ansi
|
||||
|
||||
ppOutDefault :: (HasAtomicity c, PrettyCode c) => c -> AnsiText
|
||||
ppOutDefault = mkAnsiText . PPOutput . doc defaultOptions
|
||||
|
||||
ppOut :: (CanonicalProjection a Options, HasAtomicity c, PrettyCode c) => a -> c -> AnsiText
|
||||
ppOut o = mkAnsiText . PPOutput . doc (project o)
|
||||
|
||||
ppTrace' :: (CanonicalProjection a Options, HasAtomicity c, PrettyCode c) => a -> c -> Text
|
||||
ppTrace' opts = Ansi.renderStrict . reAnnotateS stylize . layoutPretty defaultLayoutOptions . doc (project opts)
|
||||
|
||||
ppTrace :: (HasAtomicity c, PrettyCode c) => c -> Text
|
||||
ppTrace = ppTrace' traceOptions
|
||||
|
||||
ppPrint :: (HasAtomicity c, PrettyCode c) => c -> Text
|
||||
ppPrint = show . ppOutDefault
|
||||
|
||||
ppPrintLisp :: Text -> Text -> Morphism -> Object -> Text
|
||||
ppPrintLisp packageName entryName morph =
|
||||
show . mkAnsiText . PPOutput . docLisp defaultOptions packageName entryName morph
|
@ -1,270 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Pretty.Base
|
||||
( module Juvix.Compiler.Backend.Geb.Pretty.Base,
|
||||
module Juvix.Data.CodeAnn,
|
||||
module Juvix.Compiler.Backend.Geb.Pretty.Options,
|
||||
)
|
||||
where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Evaluator.Data.RunEvalResult
|
||||
import Juvix.Compiler.Backend.Geb.Evaluator.Data.Values
|
||||
import Juvix.Compiler.Backend.Geb.Language
|
||||
import Juvix.Compiler.Backend.Geb.Pretty.Keywords
|
||||
import Juvix.Compiler.Backend.Geb.Pretty.Options
|
||||
import Juvix.Data.CodeAnn
|
||||
|
||||
doc :: (HasAtomicity c, PrettyCode c) => Options -> c -> Doc Ann
|
||||
doc opts x =
|
||||
run $
|
||||
runReader opts $
|
||||
case atomicity x of
|
||||
Atom -> ppCode x
|
||||
Aggregate _ -> parens <$> ppCode x
|
||||
|
||||
docLisp :: Options -> Text -> Text -> Morphism -> Object -> Doc Ann
|
||||
docLisp opts packageName entryName morph _ =
|
||||
"(defpackage #:"
|
||||
<> pretty packageName
|
||||
<> line
|
||||
<> indent' "(:shadowing-import-from :geb.lambda.spec #:pair #:right #:left)"
|
||||
<> line
|
||||
<> indent' "(:shadowing-import-from :geb.spec #:case)"
|
||||
<> line
|
||||
<> indent' "(:shadowing-import-from :geb.lambda.trans #:int)"
|
||||
<> line
|
||||
<> indent' "(:use #:common-lisp #:geb.lambda.spec #:geb)"
|
||||
<> line
|
||||
<> indent' "(:export :*entry*))"
|
||||
<> line
|
||||
<> line
|
||||
<> "(in-package :"
|
||||
<> pretty packageName
|
||||
<> ")"
|
||||
<> line
|
||||
<> line
|
||||
<> parens
|
||||
( "defparameter"
|
||||
<+> pretty entryName
|
||||
<> line
|
||||
<> indent'
|
||||
(doc opts morph)
|
||||
)
|
||||
|
||||
class PrettyCode c where
|
||||
ppCode :: (Member (Reader Options) r) => c -> Sem r (Doc Ann)
|
||||
|
||||
ppCode' :: (PrettyCode c) => Options -> c -> Doc Ann
|
||||
ppCode' opts = run . runReader opts . ppCode
|
||||
|
||||
instance PrettyCode Case where
|
||||
ppCode Case {..} = do
|
||||
val <- ppArg _caseOn
|
||||
left <- ppArg _caseLeft
|
||||
right <- ppArg _caseRight
|
||||
return $
|
||||
kwCaseOn <> line <> indent 2 (vsep [val, left, right])
|
||||
|
||||
instance (HasAtomicity a, PrettyCode a) => PrettyCode (Pair' a) where
|
||||
ppCode Pair {..} = do
|
||||
left <- ppArg _pairLeft
|
||||
right <- ppArg _pairRight
|
||||
return $ kwPair <> line <> indent' (vsep [left, right])
|
||||
|
||||
instance PrettyCode First where
|
||||
ppCode First {..} = do
|
||||
val <- ppArg _firstValue
|
||||
return $ kwFst <> line <> indent' val
|
||||
|
||||
instance PrettyCode Second where
|
||||
ppCode Second {..} = do
|
||||
val <- ppArg _secondValue
|
||||
return $ kwSnd <> line <> indent' val
|
||||
|
||||
instance (HasAtomicity a, PrettyCode a) => PrettyCode (LeftInj' a) where
|
||||
ppCode LeftInj {..} = do
|
||||
rty <- ppArg _leftInjRightType
|
||||
val <- ppArg _leftInjValue
|
||||
return $ kwLeft <> line <> indent' (vsep [rty, val])
|
||||
|
||||
instance (HasAtomicity a, PrettyCode a) => PrettyCode (RightInj' a) where
|
||||
ppCode RightInj {..} = do
|
||||
lty <- ppArg _rightInjLeftType
|
||||
val <- ppArg _rightInjValue
|
||||
return $ kwRight <> line <> indent' (vsep [lty, val])
|
||||
|
||||
instance PrettyCode Absurd where
|
||||
ppCode Absurd {..} = do
|
||||
ty <- ppArg _absurdType
|
||||
val <- ppArg _absurdValue
|
||||
return $ kwAbsurd <> line <> indent' (vsep [ty, val])
|
||||
|
||||
instance PrettyCode Lambda where
|
||||
ppCode Lambda {..} = do
|
||||
vty <- ppArg _lambdaVarType
|
||||
body <- ppArg _lambdaBody
|
||||
return $ kwLamb <> line <> indent' (vsep [parens (kwList <> line <> indent' vty), body])
|
||||
|
||||
instance PrettyCode Application where
|
||||
ppCode Application {..} = do
|
||||
left <- ppArg _applicationLeft
|
||||
right <- ppArg _applicationRight
|
||||
return $ kwApp <> line <> indent' (vsep [left, parens (kwList <> line <> indent' right)])
|
||||
|
||||
instance PrettyCode Opcode where
|
||||
ppCode = \case
|
||||
OpAdd -> return kwAdd
|
||||
OpSub -> return kwSub
|
||||
OpMul -> return kwMul
|
||||
OpDiv -> return kwDiv
|
||||
OpMod -> return kwMod
|
||||
OpEq -> return kwEq
|
||||
OpLt -> return kwLt
|
||||
|
||||
instance PrettyCode Binop where
|
||||
ppCode Binop {..} = do
|
||||
op <- ppCode _binopOpcode
|
||||
left <- ppArg _binopLeft
|
||||
right <- ppArg _binopRight
|
||||
return $ op <> line <> indent' (vsep [left, right])
|
||||
|
||||
instance PrettyCode Failure where
|
||||
ppCode Failure {..} = do
|
||||
ty <- ppArg _failureType
|
||||
return $ kwFail <+> ty
|
||||
|
||||
instance PrettyCode Var where
|
||||
ppCode Var {..} = do
|
||||
return $
|
||||
kwVar
|
||||
<+> annotate AnnLiteralInteger (pretty _varIndex)
|
||||
|
||||
instance PrettyCode Morphism where
|
||||
ppCode = \case
|
||||
MorphismAbsurd val -> ppCode val
|
||||
MorphismUnit -> return $ parens kwUnit
|
||||
MorphismLeft val -> ppCode val
|
||||
MorphismRight val -> ppCode val
|
||||
MorphismCase x -> ppCode x
|
||||
MorphismPair x -> ppCode x
|
||||
MorphismFirst x -> ppCode x
|
||||
MorphismSecond x -> ppCode x
|
||||
MorphismLambda x -> ppCode x
|
||||
MorphismApplication x -> ppCode x
|
||||
MorphismVar idx -> ppCode idx
|
||||
MorphismInteger n -> ppCode n
|
||||
MorphismBinop x -> ppCode x
|
||||
MorphismFail x -> ppCode x
|
||||
|
||||
instance PrettyCode BitChoice where
|
||||
ppCode BitChoice {..} = do
|
||||
let pnumb = (annotate AnnLiteralInteger (pretty _bitChoice))
|
||||
return $ kwBitChoice <+> pnumb
|
||||
|
||||
instance PrettyCode Product where
|
||||
ppCode Product {..} = do
|
||||
left <- ppArg _productLeft
|
||||
right <- ppArg _productRight
|
||||
return $ kwProd <> line <> indent' (vsep [left, right])
|
||||
|
||||
instance PrettyCode Coproduct where
|
||||
ppCode Coproduct {..} = do
|
||||
left <- ppArg _coproductLeft
|
||||
right <- ppArg _coproductRight
|
||||
return $ kwCoprod <> line <> indent' (vsep [left, right])
|
||||
|
||||
instance PrettyCode Hom where
|
||||
ppCode Hom {..} = do
|
||||
dom <- ppArg _homDomain
|
||||
cod <- ppArg _homCodomain
|
||||
return $ kwHom <> line <> indent' (vsep [dom, cod])
|
||||
|
||||
instance PrettyCode Object where
|
||||
ppCode =
|
||||
\case
|
||||
ObjectInitial -> return kwInitial
|
||||
ObjectTerminal -> return kwTerminal
|
||||
ObjectProduct x -> ppCode x
|
||||
ObjectCoproduct x -> ppCode x
|
||||
ObjectHom x -> ppCode x
|
||||
ObjectInteger -> return kwInteger
|
||||
|
||||
instance PrettyCode Expression where
|
||||
ppCode = \case
|
||||
ExpressionMorphism x -> ppCode x
|
||||
ExpressionObject x -> ppCode x
|
||||
ExpressionTypedMorphism x -> ppCode x
|
||||
|
||||
instance PrettyCode TypedMorphism where
|
||||
ppCode TypedMorphism {..} = do
|
||||
m <- ppArg _typedMorphism
|
||||
o <- ppArg _typedMorphismObject
|
||||
return $ kwTyped <> line <> indent' (vsep [m, o])
|
||||
|
||||
instance PrettyCode ValueClosure where
|
||||
ppCode cls = do
|
||||
lamb <- ppArg (MorphismLambda (cls ^. valueClosureLambda))
|
||||
env <- mapM ppArg (toList (cls ^. valueClosureEnv))
|
||||
return $
|
||||
kwClosure
|
||||
<> line
|
||||
<> indent'
|
||||
( vsep
|
||||
[ parens
|
||||
( kwClosureEnv
|
||||
<> line
|
||||
<> indent'
|
||||
( if null env
|
||||
then kwNil
|
||||
else (vsep env)
|
||||
)
|
||||
),
|
||||
lamb
|
||||
]
|
||||
)
|
||||
|
||||
instance PrettyCode GebValue where
|
||||
ppCode = \case
|
||||
GebValueMorphismUnit -> return kwUnit
|
||||
GebValueMorphismInteger n -> return $ annotate AnnLiteralInteger (pretty n)
|
||||
GebValueMorphismLeft x -> ppCode x
|
||||
GebValueMorphismRight x -> ppCode x
|
||||
GebValueMorphismPair x -> ppCode x
|
||||
GebValueClosure x -> ppCode x
|
||||
|
||||
instance PrettyCode RunEvalResult where
|
||||
ppCode = \case
|
||||
RunEvalResultMorphism m -> ppCode m
|
||||
RunEvalResultGebValue v -> ppCode v
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- helper functions
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
ppArg ::
|
||||
(PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
|
||||
a ->
|
||||
Sem r (Doc Ann)
|
||||
ppArg = ppRightExpression appFixity
|
||||
|
||||
ppRightExpression ::
|
||||
(PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
|
||||
Fixity ->
|
||||
a ->
|
||||
Sem r (Doc Ann)
|
||||
ppRightExpression = ppLRExpression isRightAssoc
|
||||
|
||||
ppLeftExpression ::
|
||||
(PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
|
||||
Fixity ->
|
||||
a ->
|
||||
Sem r (Doc Ann)
|
||||
ppLeftExpression = ppLRExpression isLeftAssoc
|
||||
|
||||
ppLRExpression ::
|
||||
(HasAtomicity a, PrettyCode a, Member (Reader Options) r) =>
|
||||
(Fixity -> Bool) ->
|
||||
Fixity ->
|
||||
a ->
|
||||
Sem r (Doc Ann)
|
||||
ppLRExpression associates fixlr e =
|
||||
parensIf (atomParens associates (atomicity e) fixlr)
|
||||
<$> ppCode e
|
@ -1,95 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Pretty.Keywords where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Language
|
||||
import Juvix.Data.CodeAnn
|
||||
import Juvix.Extra.Strings qualified as Str
|
||||
|
||||
kwAbsurd :: Doc Ann
|
||||
kwAbsurd = keyword Str.gebAbsurd
|
||||
|
||||
kwUnit :: Doc Ann
|
||||
kwUnit = keyword Str.gebUnit
|
||||
|
||||
kwLeft :: Doc Ann
|
||||
kwLeft = keyword Str.gebLeft
|
||||
|
||||
kwRight :: Doc Ann
|
||||
kwRight = keyword Str.gebRight
|
||||
|
||||
kwFst :: Doc Ann
|
||||
kwFst = keyword Str.gebFst
|
||||
|
||||
kwSnd :: Doc Ann
|
||||
kwSnd = keyword Str.gebSnd
|
||||
|
||||
kwPair :: Doc Ann
|
||||
kwPair = keyword Str.gebPair
|
||||
|
||||
kwLamb :: Doc Ann
|
||||
kwLamb = keyword Str.gebLamb
|
||||
|
||||
kwList :: Doc Ann
|
||||
kwList = keyword Str.gebList
|
||||
|
||||
kwClosure :: Doc Ann
|
||||
kwClosure = keyword Str.gebValueClosure
|
||||
|
||||
kwClosureEnv :: Doc Ann
|
||||
kwClosureEnv = keyword Str.gebValueClosureEnv
|
||||
|
||||
kwNil :: Doc Ann
|
||||
kwNil = keyword Str.lispNil
|
||||
|
||||
kwApp :: Doc Ann
|
||||
kwApp = keyword Str.gebApp
|
||||
|
||||
kwVar :: Doc Ann
|
||||
kwVar = keyword Str.gebVar
|
||||
|
||||
kwAdd :: Doc Ann
|
||||
kwAdd = keyword Str.gebAdd
|
||||
|
||||
kwSub :: Doc Ann
|
||||
kwSub = keyword Str.gebSub
|
||||
|
||||
kwMul :: Doc Ann
|
||||
kwMul = keyword Str.gebMul
|
||||
|
||||
kwDiv :: Doc Ann
|
||||
kwDiv = keyword Str.gebDiv
|
||||
|
||||
kwMod :: Doc Ann
|
||||
kwMod = keyword Str.gebMod
|
||||
|
||||
kwEq :: Doc Ann
|
||||
kwEq = keyword Str.gebEq
|
||||
|
||||
kwLt :: Doc Ann
|
||||
kwLt = keyword Str.gebLt
|
||||
|
||||
kwBitChoice :: Doc Ann
|
||||
kwBitChoice = keyword Str.gebBitChoice
|
||||
|
||||
kwInitial :: Doc Ann
|
||||
kwInitial = keyword Str.gebInitial
|
||||
|
||||
kwTerminal :: Doc Ann
|
||||
kwTerminal = keyword Str.gebTerminal
|
||||
|
||||
kwProd :: Doc Ann
|
||||
kwProd = keyword Str.gebProd
|
||||
|
||||
kwCoprod :: Doc Ann
|
||||
kwCoprod = keyword Str.gebCoprod
|
||||
|
||||
kwHom :: Doc Ann
|
||||
kwHom = keyword Str.gebHom
|
||||
|
||||
kwInteger :: Doc Ann
|
||||
kwInteger = keyword Str.gebInteger
|
||||
|
||||
kwTyped :: Doc Ann
|
||||
kwTyped = keyword Str.gebTyped
|
||||
|
||||
kwFail :: Doc Ann
|
||||
kwFail = keyword Str.gebFail
|
@ -1,21 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Pretty.Options where
|
||||
|
||||
import Juvix.Prelude
|
||||
|
||||
-- no fields for now, but make it easier to add options in the future I don't
|
||||
-- remove this datatype entirely
|
||||
data Options = Options
|
||||
|
||||
makeLenses ''Options
|
||||
|
||||
defaultOptions :: Options
|
||||
defaultOptions = Options
|
||||
|
||||
traceOptions :: Options
|
||||
traceOptions = defaultOptions
|
||||
|
||||
fromGenericOptions :: GenericOptions -> Options
|
||||
fromGenericOptions _ = defaultOptions
|
||||
|
||||
instance CanonicalProjection GenericOptions Options where
|
||||
project = fromGenericOptions
|
@ -1,34 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Translation
|
||||
( module Juvix.Compiler.Backend.Geb.Translation,
|
||||
module Juvix.Compiler.Backend.Geb.Translation.FromCore,
|
||||
module Juvix.Compiler.Backend.Geb.Translation.FromSource,
|
||||
)
|
||||
where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Language
|
||||
import Juvix.Compiler.Backend.Geb.Pretty
|
||||
import Juvix.Compiler.Backend.Geb.Translation.FromCore hiding (Env)
|
||||
import Juvix.Compiler.Backend.Geb.Translation.FromSource
|
||||
|
||||
newtype Result = Result
|
||||
{ _resultCode :: Text
|
||||
}
|
||||
|
||||
data LispPackageSpec = LispPackageSpec
|
||||
{ _lispPackageName :: Text,
|
||||
_lispPackageEntry :: Text
|
||||
}
|
||||
|
||||
data ResultSpec
|
||||
= OnlyTerm
|
||||
| LispPackage LispPackageSpec
|
||||
|
||||
toResult :: ResultSpec -> Morphism -> Object -> Result
|
||||
toResult spec morph obj = case spec of
|
||||
OnlyTerm ->
|
||||
Result (ppPrint morph <> "\n")
|
||||
LispPackage LispPackageSpec {..} ->
|
||||
Result (ppPrintLisp _lispPackageName _lispPackageEntry morph obj <> "\n")
|
||||
|
||||
makeLenses ''Result
|
||||
makeLenses ''LispPackageSpec
|
@ -1,585 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Translation.FromCore where
|
||||
|
||||
import Data.HashMap.Strict qualified as HashMap
|
||||
import Juvix.Compiler.Backend.Geb.Extra
|
||||
import Juvix.Compiler.Backend.Geb.Language
|
||||
import Juvix.Compiler.Core.Data.IdentDependencyInfo qualified as Core
|
||||
import Juvix.Compiler.Core.Data.InfoTable qualified as Core
|
||||
import Juvix.Compiler.Core.Extra qualified as Core
|
||||
import Juvix.Compiler.Core.Info.TypeInfo qualified as Info
|
||||
import Juvix.Compiler.Core.Language (Index, Level, Symbol)
|
||||
|
||||
data Env = Env
|
||||
{ _envIdentMap :: HashMap Symbol Level,
|
||||
_envLevel :: Level,
|
||||
-- | `envShiftLevels` contains the de Bruijn levels immediately before which a
|
||||
-- | binder was inserted
|
||||
_envShiftLevels :: [Level]
|
||||
}
|
||||
|
||||
emptyEnv :: Env
|
||||
emptyEnv =
|
||||
Env
|
||||
{ _envIdentMap = mempty,
|
||||
_envLevel = 0,
|
||||
_envShiftLevels = []
|
||||
}
|
||||
|
||||
type Trans = Sem '[Reader Env]
|
||||
|
||||
makeLenses ''Env
|
||||
|
||||
zeroLevel :: Trans a -> Trans a
|
||||
zeroLevel = local (set envLevel 0)
|
||||
|
||||
underBinders :: Int -> Trans a -> Trans a
|
||||
underBinders n = local (over envLevel (+ n))
|
||||
|
||||
underBinder :: Trans a -> Trans a
|
||||
underBinder = underBinders 1
|
||||
|
||||
shifting :: Trans a -> Trans a
|
||||
shifting m = do
|
||||
varsNum <- asks (^. envLevel)
|
||||
local (over envShiftLevels (varsNum :)) m
|
||||
|
||||
withSymbol :: Symbol -> Trans a -> Trans a
|
||||
withSymbol sym a = do
|
||||
level <- asks (^. envLevel)
|
||||
let modif :: Env -> Env =
|
||||
over envIdentMap (HashMap.insert sym level)
|
||||
. over envLevel (+ 1)
|
||||
. over envShiftLevels (0 :)
|
||||
local modif a
|
||||
|
||||
fromCore :: Core.InfoTable -> (Morphism, Object)
|
||||
fromCore tab = case tab ^. Core.infoMain of
|
||||
Just sym ->
|
||||
let node = Core.lookupTabIdentifierNode tab sym
|
||||
syms = reverse $ filter (/= sym) $ Core.createCallGraph tab ^. Core.depInfoTopSort
|
||||
idents = map (Core.lookupTabIdentifierInfo tab) syms
|
||||
morph = run . runReader emptyEnv $ goIdents node idents
|
||||
obj = convertType $ Info.getNodeType node
|
||||
in (morph, obj)
|
||||
Nothing ->
|
||||
error "no main function"
|
||||
where
|
||||
unsupported :: forall a. a
|
||||
unsupported = error "unsupported"
|
||||
|
||||
{-
|
||||
The translation of each identifier is saved separately to avoid exponential
|
||||
blow-up. For example, the program:
|
||||
```
|
||||
a : A
|
||||
|
||||
f : A -> A
|
||||
f x = F
|
||||
|
||||
g : A -> A
|
||||
g x = f (f x)
|
||||
|
||||
main : A
|
||||
main = g (g a)
|
||||
```
|
||||
is translated as if it were a single node:
|
||||
```
|
||||
(\a -> (\f -> (\g -> g (g a)) (\x -> f (f x))) (\x -> F)) a
|
||||
```
|
||||
-}
|
||||
goIdents :: Core.Node -> [Core.IdentifierInfo] -> Trans Morphism
|
||||
goIdents node = \case
|
||||
[] ->
|
||||
zeroLevel (convertNode node)
|
||||
ii : idents -> do
|
||||
lamb <- mkLambda
|
||||
arg <- zeroLevel (convertNode fundef)
|
||||
return $
|
||||
MorphismApplication
|
||||
Application
|
||||
{ _applicationLeft = lamb,
|
||||
_applicationRight = arg
|
||||
}
|
||||
where
|
||||
sym = ii ^. Core.identifierSymbol
|
||||
fundef = Core.lookupTabIdentifierNode tab sym
|
||||
argty = convertType (Info.getNodeType fundef)
|
||||
mkLambda = do
|
||||
body <- withSymbol sym (goIdents node idents)
|
||||
return $
|
||||
MorphismLambda
|
||||
Lambda
|
||||
{ _lambdaVarType = argty,
|
||||
_lambdaBody = body
|
||||
}
|
||||
|
||||
convertNode :: Core.Node -> Trans Morphism
|
||||
convertNode = \case
|
||||
Core.NVar x -> convertVar x
|
||||
Core.NIdt x -> convertIdent x
|
||||
Core.NCst x -> convertConstant x
|
||||
Core.NApp x -> convertApp x
|
||||
Core.NBlt x -> convertBuiltinApp x
|
||||
Core.NCtr x -> convertConstr x
|
||||
Core.NLam x -> convertLambda x
|
||||
Core.NLet x -> convertLet x
|
||||
Core.NCase x -> convertCase x
|
||||
Core.NRec {} -> unsupported -- LetRecs should be lifted out beforehand
|
||||
Core.NMatch {} -> unsupported -- Pattern matching should be compiled beforehand
|
||||
Core.NPi {} -> unsupported
|
||||
Core.NUniv {} -> unsupported
|
||||
Core.NTyp {} -> unsupported
|
||||
Core.NPrim {} -> unsupported
|
||||
Core.NDyn {} -> unsupported
|
||||
Core.NBot {} -> unsupported
|
||||
Core.Closure {} -> unsupported
|
||||
|
||||
insertedBinders :: Level -> [Level] -> Index -> Int
|
||||
insertedBinders varsNum shiftLevels idx =
|
||||
length (filter ((varsNum - idx) <=) shiftLevels)
|
||||
|
||||
convertVar :: Core.Var -> Trans Morphism
|
||||
convertVar Core.Var {..} = do
|
||||
varsNum <- asks (^. envLevel)
|
||||
shiftLevels <- asks (^. envShiftLevels)
|
||||
let newIdx = _varIndex + insertedBinders varsNum shiftLevels _varIndex
|
||||
return $ MorphismVar Var {_varIndex = newIdx}
|
||||
|
||||
convertIdent :: Core.Ident -> Trans Morphism
|
||||
convertIdent Core.Ident {..} = do
|
||||
varsNum <- asks (^. envLevel)
|
||||
shiftLevels <- asks (^. envShiftLevels)
|
||||
identMap <- asks (^. envIdentMap)
|
||||
let newIdx = varsNum + length shiftLevels - fromJust (HashMap.lookup _identSymbol identMap) - 1
|
||||
return $ MorphismVar Var {_varIndex = newIdx}
|
||||
|
||||
convertConstant :: Core.Constant -> Trans Morphism
|
||||
convertConstant Core.Constant {..} = case _constantValue of
|
||||
Core.ConstInteger n -> return $ MorphismInteger (BitChoice {_bitChoice = n})
|
||||
Core.ConstField {} -> unsupported
|
||||
Core.ConstString {} -> unsupported
|
||||
|
||||
convertApp :: Core.App -> Trans Morphism
|
||||
convertApp Core.App {..} = do
|
||||
_applicationLeft <- convertNode _appLeft
|
||||
_applicationRight <- convertNode _appRight
|
||||
return $
|
||||
MorphismApplication
|
||||
Application
|
||||
{ _applicationLeft,
|
||||
_applicationRight
|
||||
}
|
||||
|
||||
convertBuiltinApp :: Core.BuiltinApp -> Trans Morphism
|
||||
convertBuiltinApp Core.BuiltinApp {..} = case _builtinAppOp of
|
||||
Core.OpIntAdd -> convertBinop OpAdd _builtinAppArgs
|
||||
Core.OpIntSub -> convertBinop OpSub _builtinAppArgs
|
||||
Core.OpIntMul -> convertBinop OpMul _builtinAppArgs
|
||||
Core.OpIntDiv -> convertBinop OpDiv _builtinAppArgs
|
||||
Core.OpIntMod -> convertBinop OpMod _builtinAppArgs
|
||||
Core.OpIntLt -> convertBinop OpLt _builtinAppArgs
|
||||
Core.OpIntLe -> convertOpIntLe _builtinAppArgs
|
||||
Core.OpEq -> convertOpEq _builtinAppArgs
|
||||
Core.OpFail -> convertOpFail (Info.getInfoType _builtinAppInfo) _builtinAppArgs
|
||||
_ ->
|
||||
unsupported
|
||||
|
||||
convertBinop :: Opcode -> [Core.Node] -> Trans Morphism
|
||||
convertBinop op = \case
|
||||
[arg1, arg2] -> do
|
||||
arg1' <- convertNode arg1
|
||||
arg2' <- convertNode arg2
|
||||
return $
|
||||
MorphismBinop
|
||||
Binop
|
||||
{ _binopOpcode = op,
|
||||
_binopLeft = arg1',
|
||||
_binopRight = arg2'
|
||||
}
|
||||
_ ->
|
||||
error "wrong builtin application argument number"
|
||||
|
||||
convertOpIntLe :: [Core.Node] -> Trans Morphism
|
||||
convertOpIntLe = \case
|
||||
[arg1, arg2] -> do
|
||||
arg1' <- convertNode arg1
|
||||
arg2' <- convertNode arg2
|
||||
let le =
|
||||
MorphismLambda
|
||||
Lambda
|
||||
{ _lambdaVarType = ObjectInteger,
|
||||
_lambdaBody =
|
||||
MorphismLambda
|
||||
Lambda
|
||||
{ _lambdaVarType = ObjectInteger,
|
||||
_lambdaBody =
|
||||
mkOr
|
||||
( MorphismBinop
|
||||
Binop
|
||||
{ _binopOpcode = OpLt,
|
||||
_binopLeft = MorphismVar Var {_varIndex = 1},
|
||||
_binopRight = MorphismVar Var {_varIndex = 0}
|
||||
}
|
||||
)
|
||||
( MorphismBinop
|
||||
Binop
|
||||
{ _binopOpcode = OpEq,
|
||||
_binopLeft = MorphismVar Var {_varIndex = 2},
|
||||
_binopRight = MorphismVar Var {_varIndex = 1}
|
||||
}
|
||||
)
|
||||
}
|
||||
}
|
||||
in return $
|
||||
MorphismApplication
|
||||
Application
|
||||
{ _applicationLeft =
|
||||
MorphismApplication
|
||||
Application
|
||||
{ _applicationLeft = le,
|
||||
_applicationRight = arg1'
|
||||
},
|
||||
_applicationRight = arg2'
|
||||
}
|
||||
_ ->
|
||||
error "wrong builtin application argument number"
|
||||
|
||||
convertOpEq :: [Core.Node] -> Trans Morphism
|
||||
convertOpEq args = case args of
|
||||
arg1 : arg2 : _
|
||||
| Info.getNodeType arg1 == Core.mkTypeInteger'
|
||||
&& Info.getNodeType arg2 == Core.mkTypeInteger' ->
|
||||
convertBinop OpEq args
|
||||
_ ->
|
||||
error "unsupported equality argument types"
|
||||
|
||||
convertOpFail :: Core.Type -> [Core.Node] -> Trans Morphism
|
||||
convertOpFail ty args = case args of
|
||||
[Core.NCst (Core.Constant _ (Core.ConstString msg))] -> do
|
||||
return $ MorphismFail (Failure msg (convertType ty))
|
||||
_ ->
|
||||
error "unsupported fail arguments"
|
||||
|
||||
convertConstr :: Core.Constr -> Trans Morphism
|
||||
convertConstr Core.Constr {..} = do
|
||||
args <- convertProduct _constrArgs
|
||||
unless (tagNum < length constructors) $
|
||||
error "constructor tag out of range"
|
||||
return $ (constructors !! tagNum) args
|
||||
where
|
||||
ci = Core.lookupTabConstructorInfo tab _constrTag
|
||||
sym = ci ^. Core.constructorInductive
|
||||
ctrs = Core.lookupTabInductiveInfo tab sym ^. Core.inductiveConstructors
|
||||
tagNum =
|
||||
fromJust
|
||||
$ elemIndex
|
||||
_constrTag
|
||||
. sort
|
||||
$ ctrs
|
||||
constructors = mkConstructors $ convertInductive sym
|
||||
|
||||
mkConstructors :: Object -> [Morphism -> Morphism]
|
||||
mkConstructors = \case
|
||||
ObjectCoproduct a -> do
|
||||
let lType = a ^. coproductLeft
|
||||
rType = a ^. coproductRight
|
||||
lInj :: Morphism -> Morphism
|
||||
lInj x =
|
||||
MorphismLeft
|
||||
LeftInj
|
||||
{ _leftInjRightType = rType,
|
||||
_leftInjValue = x
|
||||
}
|
||||
rInj :: Morphism -> Morphism
|
||||
rInj x =
|
||||
MorphismRight
|
||||
RightInj
|
||||
{ _rightInjLeftType = lType,
|
||||
_rightInjValue = x
|
||||
}
|
||||
lInj : map (rInj .) (mkConstructors rType)
|
||||
_ -> [id]
|
||||
|
||||
convertProduct :: [Core.Node] -> Trans Morphism
|
||||
convertProduct args = do
|
||||
case reverse args of
|
||||
h : t -> do
|
||||
env <- ask
|
||||
let convertNode' = run . runReader env . convertNode
|
||||
return $
|
||||
fst $
|
||||
foldr
|
||||
(\x -> mkPair (convertNode' x, convertType (Info.getNodeType x)))
|
||||
(convertNode' h, convertType (Info.getNodeType h))
|
||||
(reverse t)
|
||||
[] -> return MorphismUnit
|
||||
where
|
||||
mkPair :: (Morphism, Object) -> (Morphism, Object) -> (Morphism, Object)
|
||||
mkPair (x, xty) (y, yty) = (z, zty)
|
||||
where
|
||||
z =
|
||||
MorphismPair
|
||||
Pair
|
||||
{ _pairLeft = x,
|
||||
_pairRight = y
|
||||
}
|
||||
zty =
|
||||
ObjectProduct
|
||||
Product
|
||||
{ _productLeft = xty,
|
||||
_productRight = yty
|
||||
}
|
||||
|
||||
convertLet :: Core.Let -> Trans Morphism
|
||||
convertLet Core.Let {..} = do
|
||||
_lambdaBody <- underBinder (convertNode _letBody)
|
||||
let domty = convertType (_letItem ^. Core.letItemBinder . Core.binderType)
|
||||
arg <- convertNode (_letItem ^. Core.letItemValue)
|
||||
return $
|
||||
MorphismApplication
|
||||
Application
|
||||
{ _applicationLeft =
|
||||
MorphismLambda
|
||||
Lambda
|
||||
{ _lambdaVarType = domty,
|
||||
_lambdaBody
|
||||
},
|
||||
_applicationRight = arg
|
||||
}
|
||||
|
||||
convertLambda :: Core.Lambda -> Trans Morphism
|
||||
convertLambda Core.Lambda {..} = do
|
||||
body <- underBinder (convertNode _lambdaBody)
|
||||
return $
|
||||
MorphismLambda
|
||||
Lambda
|
||||
{ _lambdaVarType = convertType (_lambdaBinder ^. Core.binderType),
|
||||
_lambdaBody = body
|
||||
}
|
||||
|
||||
convertCase :: Core.Case -> Trans Morphism
|
||||
convertCase Core.Case {..} = do
|
||||
if
|
||||
| null branches -> do
|
||||
x <- convertNode _caseValue
|
||||
let ty = convertType (Info.getInfoType _caseInfo)
|
||||
return $
|
||||
MorphismAbsurd
|
||||
Absurd
|
||||
{ _absurdType = ty,
|
||||
_absurdValue = x
|
||||
}
|
||||
| missingCtrsNum > 1 -> do
|
||||
arg <- convertNode defaultNode
|
||||
val <- shifting (convertNode _caseValue)
|
||||
body <- shifting (go indty val branches)
|
||||
let ty = convertType (Info.getNodeType defaultNode)
|
||||
return $
|
||||
MorphismApplication
|
||||
Application
|
||||
{ _applicationLeft =
|
||||
MorphismLambda
|
||||
Lambda
|
||||
{ _lambdaVarType = ty,
|
||||
_lambdaBody = body
|
||||
},
|
||||
_applicationRight = arg
|
||||
}
|
||||
| otherwise -> do
|
||||
val <- convertNode _caseValue
|
||||
go indty val branches
|
||||
where
|
||||
indty = convertInductive _caseInductive
|
||||
ii = Core.lookupTabInductiveInfo tab _caseInductive
|
||||
missingCtrs =
|
||||
filter
|
||||
( \x ->
|
||||
isNothing
|
||||
( find
|
||||
(\y -> x ^. Core.constructorTag == y ^. Core.caseBranchTag)
|
||||
_caseBranches
|
||||
)
|
||||
)
|
||||
(map (Core.lookupTabConstructorInfo tab) (ii ^. Core.inductiveConstructors))
|
||||
missingCtrsNum = length missingCtrs
|
||||
ctrBrs = map mkCtrBranch missingCtrs
|
||||
defaultNode = fromMaybe (error "not all cases covered") _caseDefault
|
||||
-- `branches` contains one branch for each constructor of the inductive type.
|
||||
-- `_caseDefault` is the body of those branches which were not present in
|
||||
-- `_caseBranches`.
|
||||
branches = sortOn (^. Core.caseBranchTag) (_caseBranches ++ ctrBrs)
|
||||
codomainType = convertType (Info.getNodeType (head' branches ^. Core.caseBranchBody))
|
||||
|
||||
mkCtrBranch :: Core.ConstructorInfo -> Core.CaseBranch
|
||||
mkCtrBranch ci =
|
||||
Core.CaseBranch
|
||||
{ _caseBranchInfo = mempty,
|
||||
_caseBranchTag = ci ^. Core.constructorTag,
|
||||
_caseBranchBinders = map (Core.Binder "?" Nothing) tyargs,
|
||||
_caseBranchBindersNum = n,
|
||||
_caseBranchBody = defaultBody n
|
||||
}
|
||||
where
|
||||
tyargs = Core.typeArgs (ci ^. Core.constructorType)
|
||||
n = length tyargs
|
||||
defaultBody =
|
||||
if
|
||||
| missingCtrsNum > 1 -> Core.mkVar'
|
||||
| otherwise -> (`Core.shift` defaultNode)
|
||||
|
||||
go :: Object -> Morphism -> [Core.CaseBranch] -> Trans Morphism
|
||||
go ty val = \case
|
||||
[br] -> do
|
||||
-- there is only one constructor, so `ty` is a product of its argument types
|
||||
mkBranch ty val br
|
||||
br : brs -> do
|
||||
bodyLeft <- shifting (mkBranch lty (MorphismVar (Var 0)) br)
|
||||
bodyRight <- shifting (go rty (MorphismVar (Var 0)) brs)
|
||||
return $
|
||||
MorphismCase
|
||||
Case
|
||||
{ _caseOn = val,
|
||||
_caseLeft = bodyLeft,
|
||||
_caseRight = bodyRight
|
||||
}
|
||||
where
|
||||
(lty, rty) = case ty of
|
||||
ObjectCoproduct Coproduct {..} -> (_coproductLeft, _coproductRight)
|
||||
_ -> impossible
|
||||
[] -> impossible
|
||||
|
||||
mkBranch :: Object -> Morphism -> Core.CaseBranch -> Trans Morphism
|
||||
mkBranch valType val Core.CaseBranch {..} = do
|
||||
branch <- underBinders _caseBranchBindersNum (convertNode _caseBranchBody)
|
||||
if
|
||||
| _caseBranchBindersNum == 0 -> return branch
|
||||
| _caseBranchBindersNum == 1 ->
|
||||
return $
|
||||
MorphismApplication
|
||||
Application
|
||||
{ _applicationLeft =
|
||||
MorphismLambda
|
||||
Lambda
|
||||
{ _lambdaVarType = valType,
|
||||
_lambdaBody = branch
|
||||
},
|
||||
_applicationRight = val
|
||||
}
|
||||
| otherwise ->
|
||||
return $ mkApps (mkLambs branch argtys) val argtys
|
||||
where
|
||||
argtys = destructProduct valType
|
||||
|
||||
-- `mkApps` creates applications of `acc` to extracted components of
|
||||
-- `v` which is a product (right-nested)
|
||||
mkApps :: Morphism -> Morphism -> [Object] -> Morphism
|
||||
mkApps acc v = \case
|
||||
_ : tys ->
|
||||
mkApps acc' v' tys
|
||||
where
|
||||
v' =
|
||||
MorphismSecond
|
||||
Second
|
||||
{ _secondValue = v
|
||||
}
|
||||
acc' =
|
||||
MorphismApplication
|
||||
Application
|
||||
{ _applicationLeft = acc,
|
||||
_applicationRight =
|
||||
if
|
||||
| null tys ->
|
||||
v
|
||||
| otherwise ->
|
||||
MorphismFirst
|
||||
First
|
||||
{ _firstValue = v
|
||||
}
|
||||
}
|
||||
[] ->
|
||||
acc
|
||||
|
||||
mkLambs :: Morphism -> [Object] -> Morphism
|
||||
mkLambs br =
|
||||
fst
|
||||
. foldr
|
||||
( \ty (acc, accty) ->
|
||||
( MorphismLambda
|
||||
Lambda
|
||||
{ _lambdaVarType = ty,
|
||||
_lambdaBody = acc
|
||||
},
|
||||
ObjectHom
|
||||
Hom
|
||||
{ _homDomain = ty,
|
||||
_homCodomain = accty
|
||||
}
|
||||
)
|
||||
)
|
||||
(br, codomainType)
|
||||
|
||||
convertType :: Core.Type -> Object
|
||||
convertType = \case
|
||||
Core.NPi x -> convertPi x
|
||||
Core.NUniv {} -> unsupported -- no polymorphism yet
|
||||
Core.NTyp x -> convertTypeConstr x
|
||||
Core.NPrim x -> convertTypePrim x
|
||||
Core.NDyn {} -> error "incomplete type information (dynamic type encountered)"
|
||||
Core.NLam Core.Lambda {..} -> convertType _lambdaBody
|
||||
_ -> unsupported
|
||||
|
||||
convertPi :: Core.Pi -> Object
|
||||
convertPi Core.Pi {..} =
|
||||
ObjectHom
|
||||
Hom
|
||||
{ _homDomain = convertType (_piBinder ^. Core.binderType),
|
||||
_homCodomain = convertType _piBody
|
||||
}
|
||||
|
||||
convertTypeConstr :: Core.TypeConstr -> Object
|
||||
convertTypeConstr Core.TypeConstr {..} = convertInductive _typeConstrSymbol
|
||||
|
||||
convertTypePrim :: Core.TypePrim -> Object
|
||||
convertTypePrim Core.TypePrim {..} =
|
||||
case _typePrimPrimitive of
|
||||
Core.PrimInteger {} -> ObjectInteger
|
||||
Core.PrimBool {} -> objectBool
|
||||
Core.PrimField {} -> unsupported
|
||||
Core.PrimString -> unsupported
|
||||
|
||||
convertInductive :: Symbol -> Object
|
||||
convertInductive sym = do
|
||||
let ctrs =
|
||||
map (Core.lookupTabConstructorInfo tab) $
|
||||
sort $
|
||||
Core.lookupTabInductiveInfo tab sym ^. Core.inductiveConstructors
|
||||
case reverse ctrs of
|
||||
ci : ctrs' -> do
|
||||
foldr
|
||||
( \x acc ->
|
||||
ObjectCoproduct
|
||||
Coproduct
|
||||
{ _coproductLeft =
|
||||
convertConstructorType $ x ^. Core.constructorType,
|
||||
_coproductRight = acc
|
||||
}
|
||||
)
|
||||
(convertConstructorType (ci ^. Core.constructorType))
|
||||
(reverse ctrs')
|
||||
[] -> ObjectInitial
|
||||
|
||||
convertConstructorType :: Core.Node -> Object
|
||||
convertConstructorType ty =
|
||||
case reverse (Core.typeArgs ty) of
|
||||
hty : tys ->
|
||||
foldr
|
||||
( \x acc ->
|
||||
ObjectProduct
|
||||
Product
|
||||
{ _productLeft = convertType x,
|
||||
_productRight = acc
|
||||
}
|
||||
)
|
||||
(convertType hty)
|
||||
(reverse tys)
|
||||
[] -> ObjectTerminal
|
@ -1,328 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Translation.FromSource
|
||||
( module Juvix.Compiler.Backend.Geb.Translation.FromSource,
|
||||
module Juvix.Parser.Error,
|
||||
)
|
||||
where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Keywords
|
||||
import Juvix.Compiler.Backend.Geb.Language qualified as Geb
|
||||
import Juvix.Compiler.Backend.Geb.Translation.FromSource.Lexer
|
||||
import Juvix.Data.FileExt
|
||||
import Juvix.Parser.Error
|
||||
import Juvix.Prelude
|
||||
import Text.Megaparsec qualified as P
|
||||
import Text.Megaparsec.Char.Lexer qualified as P
|
||||
|
||||
data LispDefParameter = LispDefParameter
|
||||
{ _lispDefParameterName :: Text,
|
||||
_lispDefParameterMorphism :: Geb.Morphism
|
||||
}
|
||||
|
||||
makeLenses ''LispDefParameter
|
||||
|
||||
fromSource ::
|
||||
(Member (Error JuvixError) r) =>
|
||||
Path Abs File ->
|
||||
Text ->
|
||||
Sem r Geb.Expression
|
||||
fromSource fileName input_ =
|
||||
case runParser fileName input_ of
|
||||
Left err -> throw (JuvixError err)
|
||||
Right gebTerm -> pure gebTerm
|
||||
|
||||
runParser ::
|
||||
Path Abs File ->
|
||||
Text ->
|
||||
Either MegaparsecError Geb.Expression
|
||||
runParser fileName input_ = do
|
||||
let parser :: ParsecS r Geb.Expression
|
||||
parser
|
||||
| isJuvixGebFile fileName = parseGeb
|
||||
| isLispFile fileName = parseGebLisp
|
||||
| otherwise = error "unknown file extension"
|
||||
case run $
|
||||
P.runParserT parser (fromAbsFile fileName) input_ of
|
||||
Left err -> Left (MegaparsecError err)
|
||||
Right gebTerm -> Right gebTerm
|
||||
|
||||
parseLispSymbol :: ParsecS r Text
|
||||
parseLispSymbol =
|
||||
P.label "<lisp symbol>" $ do
|
||||
lexeme $
|
||||
P.takeWhile1P Nothing validChars
|
||||
where
|
||||
validChars :: Char -> Bool
|
||||
validChars = (`notElem` ("() " :: String))
|
||||
|
||||
parseLispList :: ParsecS r ()
|
||||
parseLispList =
|
||||
P.label "<lisp list>" $
|
||||
lexeme . parens $
|
||||
P.skipSome parseLispExpr
|
||||
|
||||
parseLispExpr :: ParsecS r ()
|
||||
parseLispExpr =
|
||||
void parseLispSymbol
|
||||
<|> parseLispList
|
||||
|
||||
parseTypedMorphism :: ParsecS r Geb.TypedMorphism
|
||||
parseTypedMorphism =
|
||||
parens $ do
|
||||
symbol "typed"
|
||||
m <- morphism
|
||||
o <- object
|
||||
return $
|
||||
Geb.TypedMorphism
|
||||
{ _typedMorphism = m,
|
||||
_typedMorphismObject = o
|
||||
}
|
||||
|
||||
parseDefParameter :: ParsecS r LispDefParameter
|
||||
parseDefParameter =
|
||||
P.label "<defparameter>" $ do
|
||||
parens $ do
|
||||
symbol "defparameter"
|
||||
n <- parseLispSymbol
|
||||
m <- morphism
|
||||
return
|
||||
LispDefParameter
|
||||
{ _lispDefParameterName = n,
|
||||
_lispDefParameterMorphism = m
|
||||
}
|
||||
|
||||
parseGebLisp :: ParsecS r Geb.Expression
|
||||
parseGebLisp = do
|
||||
space
|
||||
P.label "<defpackage>" parseLispExpr
|
||||
P.label "<in-package>" parseLispExpr
|
||||
entry <- parseDefParameter
|
||||
P.eof
|
||||
return $
|
||||
Geb.ExpressionMorphism $
|
||||
entry
|
||||
^. lispDefParameterMorphism
|
||||
|
||||
parseGeb :: ParsecS r Geb.Expression
|
||||
parseGeb =
|
||||
P.label "<geb program>" $ do
|
||||
space
|
||||
( P.try (Geb.ExpressionObject <$> object)
|
||||
<|> P.try (Geb.ExpressionMorphism <$> morphism)
|
||||
<|> Geb.ExpressionTypedMorphism <$> parseTypedMorphism
|
||||
)
|
||||
<* P.eof
|
||||
|
||||
morphism :: ParsecS r Geb.Morphism
|
||||
morphism =
|
||||
P.label "<geb morphism>" $ do
|
||||
morphismUnit
|
||||
<|> parens
|
||||
( morphismUnit
|
||||
<|> Geb.MorphismAbsurd <$> morphismAbsurd
|
||||
<|> Geb.MorphismLeft <$> morphismLeftInj
|
||||
<|> Geb.MorphismRight <$> morphismRightInj
|
||||
<|> Geb.MorphismCase <$> morphismCase
|
||||
<|> Geb.MorphismPair <$> morphismPair
|
||||
<|> Geb.MorphismFirst <$> morphismFirst
|
||||
<|> Geb.MorphismSecond <$> morphismSecond
|
||||
<|> Geb.MorphismLambda <$> morphismLambda
|
||||
<|> Geb.MorphismApplication <$> morphismApplication
|
||||
<|> Geb.MorphismVar <$> morphismVar
|
||||
<|> Geb.MorphismBinop <$> morphismBinop
|
||||
<|> Geb.MorphismFail <$> morphismFail
|
||||
<|> Geb.MorphismInteger <$> morphismBitChoice
|
||||
)
|
||||
|
||||
morphismList :: ParsecS r Geb.Morphism
|
||||
morphismList = parens $ do
|
||||
kw kwList
|
||||
morphism
|
||||
|
||||
parseNatural :: ParsecS r Integer
|
||||
parseNatural = lexeme P.decimal
|
||||
|
||||
morphismBitChoice :: ParsecS r Geb.BitChoice
|
||||
morphismBitChoice = do
|
||||
P.label "<geb MorphismBitChoice>" $ do
|
||||
kw kwGebBitChoice <* space
|
||||
_bitChoice <- parseNatural
|
||||
return Geb.BitChoice {..}
|
||||
|
||||
opcode :: ParsecS r Geb.Opcode
|
||||
opcode =
|
||||
P.label "<geb Opcode>" $
|
||||
Geb.OpAdd <$ kw kwGebBinopAdd
|
||||
<|> Geb.OpSub <$ kw kwGebBinopSub
|
||||
<|> Geb.OpMul <$ kw kwGebBinopMul
|
||||
<|> Geb.OpDiv <$ kw kwGebBinopDiv
|
||||
<|> Geb.OpMod <$ kw kwGebBinopMod
|
||||
<|> Geb.OpEq <$ kw kwGebBinopEq
|
||||
<|> Geb.OpLt <$ kw kwGebBinopLt
|
||||
|
||||
morphismBinop :: ParsecS r Geb.Binop
|
||||
morphismBinop = do
|
||||
P.label "<geb MorphismBinop>" $ do
|
||||
op <- opcode
|
||||
m1 <- morphism
|
||||
m2 <- morphism
|
||||
return
|
||||
Geb.Binop
|
||||
{ _binopOpcode = op,
|
||||
_binopLeft = m1,
|
||||
_binopRight = m2
|
||||
}
|
||||
|
||||
morphismFail :: ParsecS r Geb.Failure
|
||||
morphismFail = do
|
||||
P.label "<geb MorphismFail>" $ do
|
||||
kw kwErr
|
||||
Geb.Failure "" <$> object
|
||||
|
||||
object :: ParsecS r Geb.Object
|
||||
object =
|
||||
P.label "<geb Object>" $ do
|
||||
objectInitial
|
||||
<|> objectTerminal
|
||||
<|> Geb.ObjectInteger <$ (kw kwGebObjectInteger)
|
||||
<|> parens
|
||||
( Geb.ObjectProduct <$> objectProduct
|
||||
<|> Geb.ObjectCoproduct <$> objectCoproduct
|
||||
<|> Geb.ObjectHom <$> objectHom
|
||||
)
|
||||
|
||||
objectList :: ParsecS r Geb.Object
|
||||
objectList = parens $ do
|
||||
kw kwList
|
||||
object
|
||||
|
||||
morphismUnit :: ParsecS r Geb.Morphism
|
||||
morphismUnit = do
|
||||
P.label "<geb MorphismUnit>" $ do
|
||||
kw kwGebMorphismUnit
|
||||
return Geb.MorphismUnit
|
||||
|
||||
morphismAbsurd :: ParsecS r Geb.Absurd
|
||||
morphismAbsurd =
|
||||
P.label "<geb MorphismAbsurd>" $ do
|
||||
kw kwGebMorphismAbsurd
|
||||
obj <- object
|
||||
morph <- morphism
|
||||
return $
|
||||
Geb.Absurd
|
||||
{ _absurdType = obj,
|
||||
_absurdValue = morph
|
||||
}
|
||||
|
||||
morphismLeftInj :: ParsecS r Geb.LeftInj
|
||||
morphismLeftInj = do
|
||||
P.label "<geb MorphismLeft>" $ do
|
||||
kw kwGebMorphismLeft
|
||||
rType <- object
|
||||
lValue <- morphism
|
||||
return $
|
||||
Geb.LeftInj
|
||||
{ _leftInjRightType = rType,
|
||||
_leftInjValue = lValue
|
||||
}
|
||||
|
||||
morphismRightInj :: ParsecS r Geb.RightInj
|
||||
morphismRightInj = do
|
||||
P.label "<geb MorphismRight>" $ do
|
||||
kw kwGebMorphismRight
|
||||
lType <- object
|
||||
rValue <- morphism
|
||||
return $
|
||||
Geb.RightInj
|
||||
{ _rightInjLeftType = lType,
|
||||
_rightInjValue = rValue
|
||||
}
|
||||
|
||||
morphismCase :: ParsecS r Geb.Case
|
||||
morphismCase = do
|
||||
P.label "<geb MorphismCase>" $ do
|
||||
kw kwGebMorphismCase
|
||||
_caseOn <- morphism
|
||||
_caseLeft <- morphism
|
||||
_caseRight <- morphism
|
||||
return Geb.Case {..}
|
||||
|
||||
morphismPair :: ParsecS r Geb.Pair
|
||||
morphismPair = do
|
||||
P.label "<geb MorphismPair>" $ do
|
||||
kw kwGebMorphismPair
|
||||
_pairLeft <- morphism
|
||||
_pairRight <- morphism
|
||||
return Geb.Pair {..}
|
||||
|
||||
morphismFirst :: ParsecS r Geb.First
|
||||
morphismFirst = do
|
||||
P.label "<geb MorphismFirst>" $ do
|
||||
kw kwGebMorphismFirst
|
||||
_firstValue <- morphism
|
||||
return Geb.First {..}
|
||||
|
||||
morphismSecond :: ParsecS r Geb.Second
|
||||
morphismSecond = do
|
||||
P.label "<geb MorphismSecond>" $ do
|
||||
kw kwGebMorphismSecond
|
||||
_secondValue <- morphism
|
||||
return Geb.Second {..}
|
||||
|
||||
morphismLambda :: ParsecS r Geb.Lambda
|
||||
morphismLambda = do
|
||||
P.label "<geb MorphismLambda>" $ do
|
||||
kw kwGebMorphismLambda
|
||||
_lambdaVarType <- objectList
|
||||
_lambdaBody <- morphism
|
||||
return Geb.Lambda {..}
|
||||
|
||||
morphismApplication :: ParsecS r Geb.Application
|
||||
morphismApplication = do
|
||||
P.label "<geb MorphismApplication>" $ do
|
||||
kw kwGebMorphismApplication
|
||||
_applicationLeft <- morphism
|
||||
_applicationRight <- morphismList
|
||||
return Geb.Application {..}
|
||||
|
||||
morphismVar :: ParsecS r Geb.Var
|
||||
morphismVar = do
|
||||
P.label "<geb MorphismVar>" $ do
|
||||
kw kwGebVar <* space
|
||||
_varIndex <- fromIntegral <$> parseNatural
|
||||
return Geb.Var {..}
|
||||
|
||||
objectInitial :: ParsecS r Geb.Object
|
||||
objectInitial = do
|
||||
P.label "objectInitial>" $ do
|
||||
kw kwGebObjectInitial
|
||||
return Geb.ObjectInitial
|
||||
|
||||
objectTerminal :: ParsecS r Geb.Object
|
||||
objectTerminal = do
|
||||
P.label "objectTermina>" $ do
|
||||
kw kwGebObjectTerminal
|
||||
return Geb.ObjectTerminal
|
||||
|
||||
objectProduct :: ParsecS r Geb.Product
|
||||
objectProduct = do
|
||||
P.label "objectProduct>" $ do
|
||||
kw kwGebObjectProduct
|
||||
_productLeft <- object
|
||||
_productRight <- object
|
||||
return Geb.Product {..}
|
||||
|
||||
objectCoproduct :: ParsecS r Geb.Coproduct
|
||||
objectCoproduct = do
|
||||
P.label "objectCoproduct>" $ do
|
||||
kw kwGebObjectCoproduct
|
||||
_coproductLeft <- object
|
||||
_coproductRight <- object
|
||||
return Geb.Coproduct {..}
|
||||
|
||||
objectHom :: ParsecS r Geb.Hom
|
||||
objectHom = do
|
||||
P.label "objectHom >" $ do
|
||||
kw kwGebObjectHom
|
||||
_homDomain <- object
|
||||
_homCodomain <- object
|
||||
return Geb.Hom {..}
|
@ -1,71 +0,0 @@
|
||||
module Juvix.Compiler.Backend.Geb.Translation.FromSource.Lexer
|
||||
( module Juvix.Compiler.Backend.Geb.Translation.FromSource.Lexer,
|
||||
module Juvix.Parser.Lexer,
|
||||
module Juvix.Compiler.Backend.Geb.Keywords,
|
||||
)
|
||||
where
|
||||
|
||||
import Juvix.Compiler.Backend.Geb.Keywords
|
||||
import Juvix.Extra.Strings qualified as Str
|
||||
import Juvix.Parser.Lexer
|
||||
import Juvix.Prelude
|
||||
import Text.Megaparsec as P hiding (sepBy1, sepEndBy1, some)
|
||||
import Text.Megaparsec.Char.Lexer qualified as L
|
||||
|
||||
space :: forall r. ParsecS r ()
|
||||
space = L.space whiteSpace1 lineCmnt blockCmnt
|
||||
where
|
||||
lineCmnt :: ParsecS r () = L.skipLineComment ";"
|
||||
blockCmnt :: ParsecS r () = L.skipBlockComment "#|" "|#"
|
||||
|
||||
lexeme :: ParsecS r a -> ParsecS r a
|
||||
lexeme = L.lexeme space
|
||||
|
||||
lexemeInterval :: ParsecS r a -> ParsecS r (a, Interval)
|
||||
lexemeInterval = lexeme . interval
|
||||
|
||||
symbol :: Text -> ParsecS r ()
|
||||
symbol = void . L.symbol space
|
||||
|
||||
kw :: Keyword -> ParsecS r ()
|
||||
kw = void . lexeme . kw'
|
||||
|
||||
integer :: ParsecS r (WithLoc Integer)
|
||||
integer = lexeme integer'
|
||||
|
||||
number :: Int -> Int -> ParsecS r (WithLoc Int)
|
||||
number = number' integer
|
||||
|
||||
string :: ParsecS r (Text, Interval)
|
||||
string = lexemeInterval string'
|
||||
|
||||
identifier :: ParsecS r Text
|
||||
identifier = lexeme bareIdentifier
|
||||
|
||||
identifierL :: ParsecS r (Text, Interval)
|
||||
identifierL = lexemeInterval bareIdentifier
|
||||
|
||||
-- | Same as @identifier@ but does not consume space after it.
|
||||
bareIdentifier :: ParsecS r Text
|
||||
bareIdentifier = rawIdentifier allKeywordStrings
|
||||
|
||||
symbolAt :: ParsecS r ()
|
||||
symbolAt = symbol Str.at_
|
||||
|
||||
lbrace :: ParsecS r ()
|
||||
lbrace = symbol "{"
|
||||
|
||||
rbrace :: ParsecS r ()
|
||||
rbrace = symbol "}"
|
||||
|
||||
lparen :: ParsecS r ()
|
||||
lparen = symbol "("
|
||||
|
||||
rparen :: ParsecS r ()
|
||||
rparen = symbol ")"
|
||||
|
||||
parens :: ParsecS r a -> ParsecS r a
|
||||
parens = between lparen rparen
|
||||
|
||||
braces :: ParsecS r a -> ParsecS r a
|
||||
braces = between (symbol "{") (symbol "}")
|
@ -21,7 +21,6 @@ data TransformationId
|
||||
| EtaExpandApps
|
||||
| DisambiguateNames
|
||||
| CombineInfoTables
|
||||
| CheckGeb
|
||||
| CheckExec
|
||||
| CheckRust
|
||||
| CheckVampIR
|
||||
@ -43,7 +42,6 @@ data TransformationId
|
||||
| FilterUnreachable
|
||||
| OptPhaseEval
|
||||
| OptPhaseExec
|
||||
| OptPhaseGeb
|
||||
| OptPhaseVampIR
|
||||
| OptPhaseMain
|
||||
deriving stock (Data, Bounded, Enum, Show)
|
||||
@ -51,7 +49,6 @@ data TransformationId
|
||||
data PipelineId
|
||||
= PipelineStored
|
||||
| PipelineNormalize
|
||||
| PipelineGeb
|
||||
| PipelineVampIR
|
||||
| PipelineStripped
|
||||
| PipelineExec
|
||||
@ -79,10 +76,6 @@ toStrippedTransformations :: TransformationId -> [TransformationId]
|
||||
toStrippedTransformations checkId =
|
||||
combineInfoTablesTransformations ++ [checkId, LambdaLetRecLifting, TopEtaExpand, OptPhaseExec, MoveApps, RemoveTypeArgs]
|
||||
|
||||
toGebTransformations :: [TransformationId]
|
||||
toGebTransformations =
|
||||
combineInfoTablesTransformations ++ [CheckGeb, LetRecLifting, OptPhaseGeb, UnrollRecursion, FoldTypeSynonyms, ComputeTypeInfo]
|
||||
|
||||
instance TransformationId' TransformationId where
|
||||
transformationText :: TransformationId -> Text
|
||||
transformationText = \case
|
||||
@ -102,7 +95,6 @@ instance TransformationId' TransformationId where
|
||||
UnrollRecursion -> strUnrollRecursion
|
||||
DisambiguateNames -> strDisambiguateNames
|
||||
CombineInfoTables -> strCombineInfoTables
|
||||
CheckGeb -> strCheckGeb
|
||||
CheckExec -> strCheckExec
|
||||
CheckRust -> strCheckRust
|
||||
CheckVampIR -> strCheckVampIR
|
||||
@ -124,7 +116,6 @@ instance TransformationId' TransformationId where
|
||||
FilterUnreachable -> strFilterUnreachable
|
||||
OptPhaseEval -> strOptPhaseEval
|
||||
OptPhaseExec -> strOptPhaseExec
|
||||
OptPhaseGeb -> strOptPhaseGeb
|
||||
OptPhaseVampIR -> strOptPhaseVampIR
|
||||
OptPhaseMain -> strOptPhaseMain
|
||||
|
||||
@ -133,7 +124,6 @@ instance PipelineId' TransformationId PipelineId where
|
||||
pipelineText = \case
|
||||
PipelineStored -> strStoredPipeline
|
||||
PipelineNormalize -> strNormalizePipeline
|
||||
PipelineGeb -> strGebPipeline
|
||||
PipelineVampIR -> strVampIRPipeline
|
||||
PipelineStripped -> strStrippedPipeline
|
||||
PipelineExec -> strExecPipeline
|
||||
@ -142,7 +132,6 @@ instance PipelineId' TransformationId PipelineId where
|
||||
pipeline = \case
|
||||
PipelineStored -> toStoredTransformations
|
||||
PipelineNormalize -> toNormalizeTransformations
|
||||
PipelineGeb -> toGebTransformations
|
||||
PipelineVampIR -> toVampIRTransformations
|
||||
PipelineStripped -> toStrippedTransformations IdentityTrans
|
||||
PipelineExec -> toStrippedTransformations CheckExec
|
||||
|
@ -11,9 +11,6 @@ strStoredPipeline = "pipeline-stored"
|
||||
strNormalizePipeline :: Text
|
||||
strNormalizePipeline = "pipeline-normalize"
|
||||
|
||||
strGebPipeline :: Text
|
||||
strGebPipeline = "pipeline-geb"
|
||||
|
||||
strVampIRPipeline :: Text
|
||||
strVampIRPipeline = "pipeline-vampir"
|
||||
|
||||
@ -71,9 +68,6 @@ strDisambiguateNames = "disambiguate-names"
|
||||
strCombineInfoTables :: Text
|
||||
strCombineInfoTables = "combine-info-tables"
|
||||
|
||||
strCheckGeb :: Text
|
||||
strCheckGeb = "check-geb"
|
||||
|
||||
strCheckExec :: Text
|
||||
strCheckExec = "check-exec"
|
||||
|
||||
@ -134,9 +128,6 @@ strOptPhaseEval = "opt-phase-eval"
|
||||
strOptPhaseExec :: Text
|
||||
strOptPhaseExec = "opt-phase-exec"
|
||||
|
||||
strOptPhaseGeb :: Text
|
||||
strOptPhaseGeb = "opt-phase-geb"
|
||||
|
||||
strOptPhaseVampIR :: Text
|
||||
strOptPhaseVampIR = "opt-phase-vampir"
|
||||
|
||||
|
@ -21,10 +21,6 @@ toStored = mapReader fromEntryPoint . applyTransformations toStoredTransformatio
|
||||
toStripped :: (Members '[Error JuvixError, Reader EntryPoint] r) => TransformationId -> Module -> Sem r Module
|
||||
toStripped checkId = mapReader fromEntryPoint . applyTransformations (toStrippedTransformations checkId)
|
||||
|
||||
-- | Perform transformations on stored Core necessary before the translation to GEB
|
||||
toGeb :: (Members '[Error JuvixError, Reader EntryPoint] r) => Module -> Sem r Module
|
||||
toGeb = mapReader fromEntryPoint . applyTransformations toGebTransformations
|
||||
|
||||
-- | Perform transformations on stored Core necessary before the translation to VampIR
|
||||
toVampIR :: (Members '[Error JuvixError, Reader EntryPoint] r) => Module -> Sem r Module
|
||||
toVampIR = mapReader fromEntryPoint . applyTransformations toVampIRTransformations
|
||||
|
@ -16,7 +16,6 @@ import Juvix.Compiler.Core.Transformation.Base
|
||||
import Juvix.Compiler.Core.Transformation.Check.Anoma
|
||||
import Juvix.Compiler.Core.Transformation.Check.Cairo
|
||||
import Juvix.Compiler.Core.Transformation.Check.Exec
|
||||
import Juvix.Compiler.Core.Transformation.Check.Geb
|
||||
import Juvix.Compiler.Core.Transformation.Check.Rust
|
||||
import Juvix.Compiler.Core.Transformation.Check.VampIR
|
||||
import Juvix.Compiler.Core.Transformation.CombineInfoTables (combineInfoTables)
|
||||
@ -44,7 +43,6 @@ import Juvix.Compiler.Core.Transformation.Optimize.LetFolding
|
||||
import Juvix.Compiler.Core.Transformation.Optimize.MandatoryInlining
|
||||
import Juvix.Compiler.Core.Transformation.Optimize.Phase.Eval qualified as Phase.Eval
|
||||
import Juvix.Compiler.Core.Transformation.Optimize.Phase.Exec qualified as Phase.Exec
|
||||
import Juvix.Compiler.Core.Transformation.Optimize.Phase.Geb qualified as Phase.Geb
|
||||
import Juvix.Compiler.Core.Transformation.Optimize.Phase.Main qualified as Phase.Main
|
||||
import Juvix.Compiler.Core.Transformation.Optimize.Phase.VampIR qualified as Phase.VampIR
|
||||
import Juvix.Compiler.Core.Transformation.Optimize.SimplifyComparisons (simplifyComparisons)
|
||||
@ -80,7 +78,6 @@ applyTransformations ts tbl = foldM (flip appTrans) tbl ts
|
||||
EtaExpandApps -> return . etaExpansionApps
|
||||
DisambiguateNames -> return . disambiguateNames
|
||||
CombineInfoTables -> return . combineInfoTables
|
||||
CheckGeb -> mapError (JuvixError @CoreError) . checkGeb
|
||||
CheckExec -> mapError (JuvixError @CoreError) . checkExec
|
||||
CheckRust -> mapError (JuvixError @CoreError) . checkRust
|
||||
CheckVampIR -> mapError (JuvixError @CoreError) . checkVampIR
|
||||
@ -102,6 +99,5 @@ applyTransformations ts tbl = foldM (flip appTrans) tbl ts
|
||||
FilterUnreachable -> return . filterUnreachable
|
||||
OptPhaseEval -> Phase.Eval.optimize
|
||||
OptPhaseExec -> Phase.Exec.optimize
|
||||
OptPhaseGeb -> Phase.Geb.optimize
|
||||
OptPhaseVampIR -> Phase.VampIR.optimize
|
||||
OptPhaseMain -> Phase.Main.optimize
|
||||
|
@ -1,14 +0,0 @@
|
||||
module Juvix.Compiler.Core.Transformation.Check.Geb where
|
||||
|
||||
import Juvix.Compiler.Core.Error
|
||||
import Juvix.Compiler.Core.Transformation.Base
|
||||
import Juvix.Compiler.Core.Transformation.Check.Base
|
||||
|
||||
checkGeb :: forall r. (Member (Error CoreError) r) => Module -> Sem r Module
|
||||
checkGeb md =
|
||||
checkMainExists md
|
||||
>> checkNoRecursiveTypes md
|
||||
>> checkNoAxioms md
|
||||
>> mapAllNodesM checkNoIO md
|
||||
>> mapAllNodesM (checkBuiltins False) md
|
||||
>> mapAllNodesM (checkTypes False md) md
|
@ -1,8 +0,0 @@
|
||||
module Juvix.Compiler.Core.Transformation.Optimize.Phase.Geb where
|
||||
|
||||
import Juvix.Compiler.Core.Options
|
||||
import Juvix.Compiler.Core.Transformation.Base
|
||||
import Juvix.Compiler.Core.Transformation.Optimize.Phase.Main qualified as Main
|
||||
|
||||
optimize :: (Member (Reader CoreOptions) r) => Module -> Sem r Module
|
||||
optimize = withOptimizationLevel 1 Main.optimize
|
@ -14,7 +14,6 @@ import Juvix.Compiler.Asm.Translation.FromTree qualified as Asm
|
||||
import Juvix.Compiler.Backend qualified as Backend
|
||||
import Juvix.Compiler.Backend.C qualified as C
|
||||
import Juvix.Compiler.Backend.Cairo qualified as Cairo
|
||||
import Juvix.Compiler.Backend.Geb qualified as Geb
|
||||
import Juvix.Compiler.Backend.Isabelle.Data.Result qualified as Isabelle
|
||||
import Juvix.Compiler.Backend.Isabelle.Translation.FromTyped qualified as Isabelle
|
||||
import Juvix.Compiler.Backend.Rust.Translation.FromReg qualified as Rust
|
||||
@ -198,13 +197,6 @@ upToVampIR ::
|
||||
upToVampIR =
|
||||
upToStoredCore >>= \Core.CoreResult {..} -> storedCoreToVampIR _coreResultModule
|
||||
|
||||
upToGeb ::
|
||||
(Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError] r) =>
|
||||
Geb.ResultSpec ->
|
||||
Sem r Geb.Result
|
||||
upToGeb spec =
|
||||
upToStoredCore >>= \Core.CoreResult {..} -> storedCoreToGeb spec _coreResultModule
|
||||
|
||||
upToAnoma ::
|
||||
(Members '[HighlightBuilder, Reader Parser.ParserResult, Reader EntryPoint, Reader Store.ModuleTable, Files, NameIdGen, Error JuvixError] r) =>
|
||||
Sem r NockmaTree.AnomaResult
|
||||
@ -265,9 +257,6 @@ storedCoreToCasm = local (set entryPointFieldSize cairoFieldSize) . storedCoreTo
|
||||
storedCoreToCairo :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r Cairo.Result
|
||||
storedCoreToCairo = storedCoreToCasm >=> casmToCairo
|
||||
|
||||
storedCoreToGeb :: (Members '[Error JuvixError, Reader EntryPoint] r) => Geb.ResultSpec -> Core.Module -> Sem r Geb.Result
|
||||
storedCoreToGeb spec = Core.toGeb >=> return . uncurry (Geb.toResult spec) . Geb.fromCore . Core.computeCombinedInfoTable
|
||||
|
||||
storedCoreToVampIR :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r VampIR.Result
|
||||
storedCoreToVampIR = Core.toVampIR >=> VampIR.fromCore . Core.computeCombinedInfoTable
|
||||
|
||||
@ -302,9 +291,6 @@ coreToRiscZeroRust = Core.toStored >=> storedCoreToRiscZeroRust
|
||||
coreToMiniC :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r C.MiniCResult
|
||||
coreToMiniC = coreToAsm >=> asmToMiniC
|
||||
|
||||
coreToGeb :: (Members '[Error JuvixError, Reader EntryPoint] r) => Geb.ResultSpec -> Core.Module -> Sem r Geb.Result
|
||||
coreToGeb spec = Core.toStored >=> storedCoreToGeb spec
|
||||
|
||||
coreToVampIR :: (Members '[Error JuvixError, Reader EntryPoint] r) => Core.Module -> Sem r VampIR.Result
|
||||
coreToVampIR = Core.toStored >=> storedCoreToVampIR
|
||||
|
||||
|
@ -10,7 +10,6 @@ import Prelude (show)
|
||||
data FileExt
|
||||
= FileExtJuvix
|
||||
| FileExtJuvixMarkdown
|
||||
| FileExtJuvixGeb
|
||||
| FileExtJuvixCore
|
||||
| FileExtJuvixAsm
|
||||
| FileExtJuvixReg
|
||||
@ -42,9 +41,6 @@ juvixMarkdownFileExt = ".juvix.md"
|
||||
juvixMarkdownFileExts :: (IsString a) => NonEmpty a
|
||||
juvixMarkdownFileExts = ".juvix" :| [".md"]
|
||||
|
||||
juvixGebFileExt :: (IsString a) => a
|
||||
juvixGebFileExt = ".geb"
|
||||
|
||||
juvixCoreFileExt :: (IsString a) => a
|
||||
juvixCoreFileExt = ".jvc"
|
||||
|
||||
@ -109,7 +105,6 @@ fileExtToIsString :: (IsString a) => FileExt -> a
|
||||
fileExtToIsString = \case
|
||||
FileExtJuvix -> juvixFileExt
|
||||
FileExtJuvixMarkdown -> juvixMarkdownFileExt
|
||||
FileExtJuvixGeb -> juvixGebFileExt
|
||||
FileExtJuvixCore -> juvixCoreFileExt
|
||||
FileExtJuvixAsm -> juvixAsmFileExt
|
||||
FileExtJuvixReg -> juvixRegFileExt
|
||||
@ -136,7 +131,6 @@ toMetavar :: FileExt -> String
|
||||
toMetavar = \case
|
||||
FileExtJuvix -> "JUVIX_FILE"
|
||||
FileExtJuvixMarkdown -> "JUVIX_MARKDOWN_FILE"
|
||||
FileExtJuvixGeb -> "JUVIX_GEB_FILE"
|
||||
FileExtJuvixCore -> "JUVIX_CORE_FILE"
|
||||
FileExtJuvixAsm -> "JUVIX_ASM_FILE"
|
||||
FileExtJuvixReg -> "JUVIX_REG_FILE"
|
||||
@ -173,9 +167,6 @@ isJuvixMarkdownFile p = case splitExtension p of
|
||||
Just (f, ext) -> ext == markdownFileExt && isJuvixFile f
|
||||
_ -> False
|
||||
|
||||
isJuvixGebFile :: Path b File -> Bool
|
||||
isJuvixGebFile = (== Just juvixGebFileExt) . fileExtension
|
||||
|
||||
isJuvixCoreFile :: Path b File -> Bool
|
||||
isJuvixCoreFile = (== Just juvixCoreFileExt) . fileExtension
|
||||
|
||||
@ -228,7 +219,6 @@ toFileExt :: Path b File -> Maybe FileExt
|
||||
toFileExt p
|
||||
| isJuvixFile p = Just FileExtJuvix
|
||||
| isJuvixMarkdownFile p = Just FileExtJuvixMarkdown
|
||||
| isJuvixGebFile p = Just FileExtJuvixGeb
|
||||
| isJuvixCoreFile p = Just FileExtJuvixCore
|
||||
| isJuvixAsmFile p = Just FileExtJuvixAsm
|
||||
| isJuvixRegFile p = Just FileExtJuvixReg
|
||||
|
@ -4,7 +4,6 @@ module Juvix.Extra.Paths
|
||||
)
|
||||
where
|
||||
|
||||
import Juvix.Data.FileExt
|
||||
import Juvix.Extra.Paths.Base
|
||||
import Juvix.Prelude.Base
|
||||
import Juvix.Prelude.Path
|
||||
@ -40,8 +39,5 @@ replPath = $(mkAbsFile "/repl")
|
||||
formatStdinPath :: Path Abs File
|
||||
formatStdinPath = $(mkAbsFile "/format-stdin")
|
||||
|
||||
gebReplPath :: Path Abs File
|
||||
gebReplPath = $(mkAbsFile ("/repl" <> juvixGebFileExt))
|
||||
|
||||
noFile :: Path Abs File
|
||||
noFile = $(mkAbsFile "/<text>")
|
||||
|
@ -833,99 +833,6 @@ instrReturn = "ret"
|
||||
instrBr :: (IsString s) => s
|
||||
instrBr = "br"
|
||||
|
||||
gebAbsurd :: (IsString s) => s
|
||||
gebAbsurd = "absurd"
|
||||
|
||||
gebUnit :: (IsString s) => s
|
||||
gebUnit = "unit"
|
||||
|
||||
gebLeft :: (IsString s) => s
|
||||
gebLeft = "left"
|
||||
|
||||
gebRight :: (IsString s) => s
|
||||
gebRight = "right"
|
||||
|
||||
gebCase :: (IsString s) => s
|
||||
gebCase = "case-on"
|
||||
|
||||
gebPair :: (IsString s) => s
|
||||
gebPair = "pair"
|
||||
|
||||
gebFst :: (IsString s) => s
|
||||
gebFst = "fst"
|
||||
|
||||
gebSnd :: (IsString s) => s
|
||||
gebSnd = "snd"
|
||||
|
||||
gebLamb :: (IsString s) => s
|
||||
gebLamb = "lamb"
|
||||
|
||||
gebList :: (IsString s) => s
|
||||
gebList = "list"
|
||||
|
||||
gebValueClosure :: (IsString s) => s
|
||||
gebValueClosure = "cls"
|
||||
|
||||
gebValueClosureEnv :: (IsString s) => s
|
||||
gebValueClosureEnv = "env"
|
||||
|
||||
lispNil :: (IsString s) => s
|
||||
lispNil = "nil"
|
||||
|
||||
gebApp :: (IsString s) => s
|
||||
gebApp = "app"
|
||||
|
||||
gebVar :: (IsString s) => s
|
||||
gebVar = "index"
|
||||
|
||||
gebBitChoice :: (IsString s) => s
|
||||
gebBitChoice = "bit-choice"
|
||||
|
||||
gebAdd :: (IsString s) => s
|
||||
gebAdd = "plus"
|
||||
|
||||
gebSub :: (IsString s) => s
|
||||
gebSub = "minus"
|
||||
|
||||
gebMul :: (IsString s) => s
|
||||
gebMul = "times"
|
||||
|
||||
gebDiv :: (IsString s) => s
|
||||
gebDiv = "divide"
|
||||
|
||||
gebMod :: (IsString s) => s
|
||||
gebMod = "modulo"
|
||||
|
||||
gebFail :: (IsString s) => s
|
||||
gebFail = "err"
|
||||
|
||||
gebEq :: (IsString s) => s
|
||||
gebEq = "lamb-eq"
|
||||
|
||||
gebLt :: (IsString s) => s
|
||||
gebLt = "lamb-lt"
|
||||
|
||||
gebInitial :: (IsString s) => s
|
||||
gebInitial = "so0"
|
||||
|
||||
gebTerminal :: (IsString s) => s
|
||||
gebTerminal = "so1"
|
||||
|
||||
gebProd :: (IsString s) => s
|
||||
gebProd = "prod"
|
||||
|
||||
gebCoprod :: (IsString s) => s
|
||||
gebCoprod = "coprod"
|
||||
|
||||
gebHom :: (IsString s) => s
|
||||
gebHom = "fun-type"
|
||||
|
||||
gebInteger :: (IsString s) => s
|
||||
gebInteger = "int"
|
||||
|
||||
gebTyped :: (IsString s) => s
|
||||
gebTyped = "typed"
|
||||
|
||||
juvixDotOrg :: (IsString s) => s
|
||||
juvixDotOrg = "https://juvix.org"
|
||||
|
||||
|
@ -1,15 +0,0 @@
|
||||
module BackendGeb where
|
||||
|
||||
import BackendGeb.Compilation qualified as Compilation
|
||||
import BackendGeb.Eval qualified as Eval
|
||||
import BackendGeb.FromCore qualified as FromCore
|
||||
import Base
|
||||
|
||||
allTests :: TestTree
|
||||
allTests =
|
||||
testGroup
|
||||
"BackendGeb tests"
|
||||
[ Eval.allTests,
|
||||
FromCore.allTests,
|
||||
Compilation.allTests
|
||||
]
|
@ -1,10 +0,0 @@
|
||||
module BackendGeb.Compilation where
|
||||
|
||||
import BackendGeb.Compilation.Positive qualified as P
|
||||
import Base
|
||||
|
||||
allTests :: TestTree
|
||||
allTests =
|
||||
testGroup
|
||||
"Compilation to Geb"
|
||||
[P.allTests]
|
@ -1,18 +0,0 @@
|
||||
module BackendGeb.Compilation.Base where
|
||||
|
||||
import BackendGeb.FromCore.Base
|
||||
import Base
|
||||
import Juvix.Compiler.Backend (Target (TargetGeb))
|
||||
import Juvix.Compiler.Core qualified as Core
|
||||
|
||||
gebCompilationAssertion ::
|
||||
Path Abs Dir ->
|
||||
Path Abs File ->
|
||||
Path Abs File ->
|
||||
(String -> IO ()) ->
|
||||
Assertion
|
||||
gebCompilationAssertion root mainFile expectedFile step = do
|
||||
step "Translate to JuvixCore"
|
||||
entryPoint <- set entryPointTarget (Just TargetGeb) <$> testDefaultEntryPointIO root mainFile
|
||||
m <- (^. pipelineResult . Core.coreResultModule) . snd <$> testRunIO entryPoint upToStoredCore
|
||||
coreToGebTranslationAssertion' (Core.computeCombinedInfoTable m) entryPoint expectedFile step
|
@ -1,187 +0,0 @@
|
||||
module BackendGeb.Compilation.Positive where
|
||||
|
||||
import BackendGeb.Compilation.Base
|
||||
import Base
|
||||
|
||||
data PosTest = PosTest
|
||||
{ _name :: String,
|
||||
_relDir :: Path Rel Dir,
|
||||
_file :: Path Rel File,
|
||||
_expectedFile :: Path Rel File
|
||||
}
|
||||
|
||||
root :: Path Abs Dir
|
||||
root = relToProject $(mkRelDir "tests/Geb/positive/Compilation")
|
||||
|
||||
testDescr :: PosTest -> TestDescr
|
||||
testDescr PosTest {..} =
|
||||
let tRoot = root <//> _relDir
|
||||
file' = tRoot <//> _file
|
||||
expected' = tRoot <//> _expectedFile
|
||||
in TestDescr
|
||||
{ _testName = _name,
|
||||
_testRoot = tRoot,
|
||||
_testAssertion =
|
||||
Steps $
|
||||
gebCompilationAssertion tRoot file' expected'
|
||||
}
|
||||
|
||||
allTests :: TestTree
|
||||
allTests =
|
||||
testGroup
|
||||
"JuvixGeb positive compilation tests"
|
||||
(map (mkTest . testDescr) tests)
|
||||
|
||||
tests :: [PosTest]
|
||||
tests =
|
||||
[ PosTest
|
||||
"Test001: not function"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test001.juvix")
|
||||
$(mkRelFile "out/test001.geb"),
|
||||
PosTest
|
||||
"Test002: pattern matching"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test002.juvix")
|
||||
$(mkRelFile "out/test002.geb"),
|
||||
PosTest
|
||||
"Test003: inductive types"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test003.juvix")
|
||||
$(mkRelFile "out/test003.geb"),
|
||||
PosTest
|
||||
"Test004: definitions"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test004.juvix")
|
||||
$(mkRelFile "out/test004.geb"),
|
||||
PosTest
|
||||
"Test005: basic arithmetic"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test005.juvix")
|
||||
$(mkRelFile "out/test005.geb"),
|
||||
PosTest
|
||||
"Test006: arithmetic"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test006.juvix")
|
||||
$(mkRelFile "out/test006.geb"),
|
||||
PosTest
|
||||
"Test007: single-constructor inductive types"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test007.juvix")
|
||||
$(mkRelFile "out/test007.geb"),
|
||||
PosTest
|
||||
"Test008: higher-order inductive types"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test008.juvix")
|
||||
$(mkRelFile "out/test008.geb"),
|
||||
PosTest
|
||||
"Test009: let"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test009.juvix")
|
||||
$(mkRelFile "out/test009.geb"),
|
||||
PosTest
|
||||
"Test010: functions returning functions with variable capture"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test010.juvix")
|
||||
$(mkRelFile "out/test010.geb"),
|
||||
PosTest
|
||||
"Test011: applications with lets and cases in function position"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test011.juvix")
|
||||
$(mkRelFile "out/test011.geb"),
|
||||
PosTest
|
||||
"Test012: mid-square hashing (unrolled)"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test012.juvix")
|
||||
$(mkRelFile "out/test012.geb"),
|
||||
PosTest
|
||||
"Test013: recursion"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test013.juvix")
|
||||
$(mkRelFile "out/test013.geb"),
|
||||
PosTest
|
||||
"Test014: tail recursion"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test014.juvix")
|
||||
$(mkRelFile "out/test014.geb"),
|
||||
PosTest
|
||||
"Test015: tail recursion: Fibonacci numbers in linear time"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test015.juvix")
|
||||
$(mkRelFile "out/test015.geb"),
|
||||
PosTest
|
||||
"Test016: local functions with free variables"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test016.juvix")
|
||||
$(mkRelFile "out/test016.geb"),
|
||||
PosTest
|
||||
"Test017: recursion through higher-order functions"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test017.juvix")
|
||||
$(mkRelFile "out/test017.geb"),
|
||||
PosTest
|
||||
"Test018: tail recursion through higher-order functions"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test018.juvix")
|
||||
$(mkRelFile "out/test018.geb"),
|
||||
PosTest
|
||||
"Test019: higher-order functions"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test019.juvix")
|
||||
$(mkRelFile "out/test019.geb"),
|
||||
PosTest
|
||||
"Test020: McCarthy's 91 function"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test020.juvix")
|
||||
$(mkRelFile "out/test020.geb"),
|
||||
PosTest
|
||||
"Test021: fast exponentiation"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test021.juvix")
|
||||
$(mkRelFile "out/test021.geb"),
|
||||
PosTest
|
||||
"Test022: mutual recursion"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test022.juvix")
|
||||
$(mkRelFile "out/test022.geb"),
|
||||
PosTest
|
||||
"Test023: Euclid's algorithm"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test023.juvix")
|
||||
$(mkRelFile "out/test023.geb"),
|
||||
PosTest
|
||||
"Test024: Ackermann function"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test024.juvix")
|
||||
$(mkRelFile "out/test024.geb"),
|
||||
PosTest
|
||||
"Test025: mid-square hashing"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test025.juvix")
|
||||
$(mkRelFile "out/test025.geb"),
|
||||
PosTest
|
||||
"Test026: recursive let"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test026.juvix")
|
||||
$(mkRelFile "out/test026.geb"),
|
||||
PosTest
|
||||
"Test027: simple case expression"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test027.juvix")
|
||||
$(mkRelFile "out/test027.geb"),
|
||||
PosTest
|
||||
"Test028: mutually recursive let expressions"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test028.juvix")
|
||||
$(mkRelFile "out/test028.geb"),
|
||||
PosTest
|
||||
"Test029: pattern matching on natural numbers"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test029.juvix")
|
||||
$(mkRelFile "out/test029.geb"),
|
||||
PosTest
|
||||
"Test030: recursion with unroll pragma"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "test030.juvix")
|
||||
$(mkRelFile "out/test030.geb")
|
||||
]
|
@ -1,10 +0,0 @@
|
||||
module BackendGeb.Eval where
|
||||
|
||||
import BackendGeb.Eval.Positive qualified as EvalP
|
||||
import Base
|
||||
|
||||
allTests :: TestTree
|
||||
allTests =
|
||||
testGroup
|
||||
"JuvixGeb eval tests"
|
||||
[EvalP.allTests]
|
@ -1,77 +0,0 @@
|
||||
module BackendGeb.Eval.Base where
|
||||
|
||||
import Base
|
||||
import Juvix.Compiler.Backend.Geb qualified as Geb
|
||||
import Juvix.Prelude.Pretty
|
||||
|
||||
gebEvalAssertion ::
|
||||
Path Abs File ->
|
||||
Path Abs File ->
|
||||
(String -> IO ()) ->
|
||||
Assertion
|
||||
gebEvalAssertion mainFile expectedFile step = do
|
||||
step "Parse"
|
||||
input_ <- readFile mainFile
|
||||
case Geb.runParser mainFile input_ of
|
||||
Left err -> assertFailure (prettyString err)
|
||||
Right (Geb.ExpressionObject _) -> do
|
||||
step "No evaluation for objects"
|
||||
assertFailure (unpack Geb.objNoEvalMsg)
|
||||
Right (Geb.ExpressionMorphism gebMorphism) ->
|
||||
gebEvalAssertion' mainFile expectedFile step gebMorphism
|
||||
Right (Geb.ExpressionTypedMorphism typedMorphism) ->
|
||||
gebEvalAssertion'
|
||||
mainFile
|
||||
expectedFile
|
||||
step
|
||||
(typedMorphism ^. Geb.typedMorphism)
|
||||
|
||||
gebEvalAssertion' ::
|
||||
Path Abs File ->
|
||||
Path Abs File ->
|
||||
(String -> IO ()) ->
|
||||
Geb.Morphism ->
|
||||
Assertion
|
||||
gebEvalAssertion' _mainFile expectedFile step gebMorphism = do
|
||||
let env :: Geb.Env =
|
||||
Geb.Env
|
||||
{ _envEvaluatorOptions = Geb.defaultEvaluatorOptions,
|
||||
_envContext = mempty
|
||||
}
|
||||
withTempDir' $
|
||||
\dirPath -> do
|
||||
let outputFile = dirPath <//> $(mkRelFile "out.out")
|
||||
step "Evaluate"
|
||||
hout <- openFile (toFilePath outputFile) WriteMode
|
||||
let result = Geb.eval' env gebMorphism
|
||||
case result of
|
||||
Left err -> do
|
||||
hClose hout
|
||||
assertFailure (prettyString (fromJuvixError @GenericError err))
|
||||
Right value -> do
|
||||
hPutStrLn hout (Geb.ppPrint value)
|
||||
hClose hout
|
||||
actualOutput <- readFile outputFile
|
||||
expected <- readFile expectedFile
|
||||
step "Compare expected and actual program output"
|
||||
assertEqDiffText
|
||||
("Check: EVAL output = " <> toFilePath expectedFile)
|
||||
actualOutput
|
||||
expected
|
||||
|
||||
gebEvalErrorAssertion :: Path Abs File -> (String -> IO ()) -> Assertion
|
||||
gebEvalErrorAssertion mainFile step = do
|
||||
step "Parse"
|
||||
input_ <- readFile mainFile
|
||||
case Geb.runParser mainFile input_ of
|
||||
Left _ -> assertBool "" True
|
||||
Right (Geb.ExpressionObject _) -> assertFailure "no error"
|
||||
Right morph' -> do
|
||||
step "Evaluate"
|
||||
let gebMorphism = case morph' of
|
||||
Geb.ExpressionMorphism morph -> morph
|
||||
Geb.ExpressionTypedMorphism typedMorphism ->
|
||||
typedMorphism ^. Geb.typedMorphism
|
||||
case Geb.eval' Geb.defaultEvalEnv gebMorphism of
|
||||
Left _ -> assertBool "" True
|
||||
Right _ -> assertFailure "no error"
|
@ -1,80 +0,0 @@
|
||||
module BackendGeb.Eval.Positive where
|
||||
|
||||
import BackendGeb.Eval.Base
|
||||
import Base
|
||||
|
||||
data PosTest = PosTest
|
||||
{ _name :: String,
|
||||
_relDir :: Path Rel Dir,
|
||||
_file :: Path Rel File,
|
||||
_expectedFile :: Path Rel File
|
||||
}
|
||||
|
||||
root :: Path Abs Dir
|
||||
root = relToProject $(mkRelDir "tests/Geb/positive")
|
||||
|
||||
testDescr :: PosTest -> TestDescr
|
||||
testDescr PosTest {..} =
|
||||
let tRoot = root <//> _relDir
|
||||
file' = tRoot <//> _file
|
||||
expected' = tRoot <//> _expectedFile
|
||||
in TestDescr
|
||||
{ _testName = _name,
|
||||
_testRoot = tRoot,
|
||||
_testAssertion =
|
||||
Steps $
|
||||
gebEvalAssertion file' expected'
|
||||
}
|
||||
|
||||
filterOutTests :: [String] -> [PosTest] -> [PosTest]
|
||||
filterOutTests out = filter (\PosTest {..} -> _name `notElem` out)
|
||||
|
||||
allTests :: TestTree
|
||||
allTests =
|
||||
testGroup
|
||||
"JuvixGeb positive evaluation tests"
|
||||
(map (mkTest . testDescr) tests)
|
||||
|
||||
tests :: [PosTest]
|
||||
tests =
|
||||
[ PosTest
|
||||
"App case on"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "app-case-on.geb")
|
||||
$(mkRelFile "Eval/out/app-case-on.out"),
|
||||
PosTest
|
||||
"App fst pair"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "app-fst-pair.geb")
|
||||
$(mkRelFile "Eval/out/app-fst-pair.out"),
|
||||
PosTest
|
||||
"lambda"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "lamb.geb")
|
||||
$(mkRelFile "Eval/out/lamb.out"),
|
||||
PosTest
|
||||
"App lambda"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "app-lambda.geb")
|
||||
$(mkRelFile "Eval/out/app-lambda.out"),
|
||||
PosTest
|
||||
"Double application"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "app-app-lambda.geb")
|
||||
$(mkRelFile "Eval/out/app-app-lambda.out"),
|
||||
PosTest
|
||||
"Basic app"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "basic-app.geb")
|
||||
$(mkRelFile "Eval/out/basic-app.out"),
|
||||
PosTest
|
||||
"case on"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "case-on.geb")
|
||||
$(mkRelFile "Eval/out/case-on.out"),
|
||||
PosTest
|
||||
"left unit"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "left-unit.geb")
|
||||
$(mkRelFile "Eval/out/left-unit.out")
|
||||
]
|
@ -1,10 +0,0 @@
|
||||
module BackendGeb.FromCore where
|
||||
|
||||
import BackendGeb.FromCore.Positive qualified as FromCoreP
|
||||
import Base
|
||||
|
||||
allTests :: TestTree
|
||||
allTests =
|
||||
testGroup
|
||||
"Translation from Juvix Core to Geb"
|
||||
[FromCoreP.allTests]
|
@ -1,89 +0,0 @@
|
||||
module BackendGeb.FromCore.Base where
|
||||
|
||||
import Base
|
||||
import GHC.Base (seq)
|
||||
import Juvix.Compiler.Backend (Target (TargetGeb))
|
||||
import Juvix.Compiler.Backend.Geb qualified as Geb
|
||||
import Juvix.Compiler.Core qualified as Core
|
||||
import Juvix.Compiler.Core.Pretty qualified as Core
|
||||
import Juvix.Prelude.Pretty
|
||||
|
||||
coreToGebTranslationAssertion ::
|
||||
Path Abs Dir ->
|
||||
Path Abs File ->
|
||||
Path Abs File ->
|
||||
(String -> IO ()) ->
|
||||
Assertion
|
||||
coreToGebTranslationAssertion root mainFile expectedFile step = do
|
||||
step "Parse Juvix Core file"
|
||||
input_ <- readFile mainFile
|
||||
entryPoint <- set entryPointTarget (Just TargetGeb) <$> testDefaultEntryPointIO root mainFile
|
||||
case Core.runParserMain mainFile defaultModuleId mempty input_ of
|
||||
Left err -> assertFailure . prettyString $ err
|
||||
Right coreInfoTable -> coreToGebTranslationAssertion' coreInfoTable entryPoint expectedFile step
|
||||
|
||||
coreToGebTranslationAssertion' ::
|
||||
Core.InfoTable ->
|
||||
EntryPoint ->
|
||||
Path Abs File ->
|
||||
(String -> IO ()) ->
|
||||
Assertion
|
||||
coreToGebTranslationAssertion' coreInfoTable entryPoint expectedFile step = do
|
||||
step "Prepare the Juvix Core node for translation to Geb"
|
||||
case run . runReader entryPoint . runError @Geb.JuvixError $ Core.toGeb (Core.moduleFromInfoTable coreInfoTable) of
|
||||
Left err ->
|
||||
assertFailure . prettyString $
|
||||
fromJuvixError @GenericError err
|
||||
Right readyCoreModule ->
|
||||
let readyCoreInfoTable = Core.computeCombinedInfoTable readyCoreModule
|
||||
in length (fromText (Core.ppTrace readyCoreInfoTable) :: String) `seq` do
|
||||
step "Translate the Juvix Core node to Geb"
|
||||
let (translatedMorphism, translatedObj) = Geb.fromCore readyCoreInfoTable
|
||||
step "Typecheck the translated Geb node"
|
||||
let typeMorph =
|
||||
Geb.TypedMorphism
|
||||
{ _typedMorphism = translatedMorphism,
|
||||
_typedMorphismObject = translatedObj
|
||||
}
|
||||
case run . runError @Geb.CheckingError $ Geb.check' typeMorph of
|
||||
Left err ->
|
||||
assertFailure . prettyString $
|
||||
fromJuvixError @GenericError (JuvixError err)
|
||||
Right _ -> do
|
||||
step "Try evaluating the JuvixCore node"
|
||||
let resultCoreEval :: Core.Node = Core.evalInfoTable stderr readyCoreInfoTable
|
||||
step "Translate the result of the evaluated JuvixCore node to Geb"
|
||||
let (gebCoreEvalResult, _) = Geb.fromCore $ Core.setupMainFunction defaultModuleId readyCoreInfoTable resultCoreEval
|
||||
case ( Geb.eval' Geb.defaultEvalEnv translatedMorphism,
|
||||
Geb.eval' Geb.defaultEvalEnv gebCoreEvalResult
|
||||
) of
|
||||
(Left err, _) -> do
|
||||
step "The evaluation of the translated Geb node failed"
|
||||
assertFailure . prettyString $
|
||||
fromJuvixError @GenericError (JuvixError err)
|
||||
(_, Left err) -> do
|
||||
step "The evaluation of gebCoreEvalResult failed"
|
||||
assertFailure . prettyString $ fromJuvixError @GenericError (JuvixError err)
|
||||
( Right resEvalTranslatedMorph,
|
||||
Right resEvalGebCoreEvalResult
|
||||
) -> do
|
||||
step "Compare the geb value of the Core eval output and the Geb eval output"
|
||||
if
|
||||
| resEvalTranslatedMorph /= resEvalGebCoreEvalResult ->
|
||||
assertFailure "The evaluation for the Core node and the Geb node are not equal"
|
||||
| otherwise -> do
|
||||
expectedInput <- readFile expectedFile
|
||||
step "Compare expected and actual program output"
|
||||
let compareEvalOutput morph =
|
||||
if
|
||||
| Geb.quote resEvalTranslatedMorph /= morph ->
|
||||
assertFailure $
|
||||
"The result of evaluating the translated Geb"
|
||||
<> "node is not equal to the expected output"
|
||||
| otherwise -> assertBool "" True
|
||||
case Geb.runParser expectedFile expectedInput of
|
||||
Left parseErr -> assertFailure . prettyString $ parseErr
|
||||
Right (Geb.ExpressionMorphism m) -> compareEvalOutput m
|
||||
Right (Geb.ExpressionTypedMorphism m) -> compareEvalOutput (m ^. Geb.typedMorphism)
|
||||
Right (Geb.ExpressionObject _) ->
|
||||
assertFailure "Expected a morphism, but got an object for the expected output"
|
@ -1,175 +0,0 @@
|
||||
module BackendGeb.FromCore.Positive where
|
||||
|
||||
import BackendGeb.FromCore.Base
|
||||
import Base
|
||||
|
||||
data PosTest = PosTest
|
||||
{ _name :: String,
|
||||
_relDir :: Path Rel Dir,
|
||||
_file :: Path Rel File,
|
||||
_expectedFile :: Path Rel File
|
||||
}
|
||||
|
||||
root :: Path Abs Dir
|
||||
root = relToProject $(mkRelDir "tests/Geb/positive")
|
||||
|
||||
testDescr :: PosTest -> TestDescr
|
||||
testDescr PosTest {..} =
|
||||
let tRoot = root <//> _relDir
|
||||
file' = tRoot <//> _file
|
||||
expected' = tRoot <//> _expectedFile
|
||||
in TestDescr
|
||||
{ _testName = _name,
|
||||
_testRoot = tRoot,
|
||||
_testAssertion =
|
||||
Steps $
|
||||
coreToGebTranslationAssertion tRoot file' expected'
|
||||
}
|
||||
|
||||
filterOutTests :: [String] -> [PosTest] -> [PosTest]
|
||||
filterOutTests out = filter (\PosTest {..} -> _name `notElem` out)
|
||||
|
||||
allTests :: TestTree
|
||||
allTests =
|
||||
testGroup
|
||||
"JuvixGeb positive translation tests"
|
||||
(map (mkTest . testDescr) tests)
|
||||
|
||||
tests :: [PosTest]
|
||||
tests =
|
||||
[ PosTest
|
||||
"Test001: not function"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test001.jvc")
|
||||
$(mkRelFile "Eval/out/test001.geb"),
|
||||
PosTest
|
||||
"Test002: pattern matching"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test002.jvc")
|
||||
$(mkRelFile "Eval/out/test002.geb"),
|
||||
PosTest
|
||||
"Test003: inductive types"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test003.jvc")
|
||||
$(mkRelFile "Eval/out/test003.geb"),
|
||||
PosTest
|
||||
"Test004: definitions"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test004.jvc")
|
||||
$(mkRelFile "Eval/out/test004.geb"),
|
||||
PosTest
|
||||
"Test005: basic arithmetic"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test005.jvc")
|
||||
$(mkRelFile "Eval/out/test005.geb"),
|
||||
PosTest
|
||||
"Test006: arithmetic"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test006.jvc")
|
||||
$(mkRelFile "Eval/out/test006.geb"),
|
||||
PosTest
|
||||
"Test007: single-constructor inductive types"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test007.jvc")
|
||||
$(mkRelFile "Eval/out/test007.geb"),
|
||||
PosTest
|
||||
"Test008: higher-order inductive types"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test008.jvc")
|
||||
$(mkRelFile "Eval/out/test008.geb"),
|
||||
PosTest
|
||||
"Test009: comparisons"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test009.jvc")
|
||||
$(mkRelFile "Eval/out/test009.geb"),
|
||||
PosTest
|
||||
"Test010: let"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test010.jvc")
|
||||
$(mkRelFile "Eval/out/test010.geb"),
|
||||
PosTest
|
||||
"Test011: functions returning functions with variable capture"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test011.jvc")
|
||||
$(mkRelFile "Eval/out/test011.geb"),
|
||||
PosTest
|
||||
"Test012: partial application"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test012.jvc")
|
||||
$(mkRelFile "Eval/out/test012.geb"),
|
||||
PosTest
|
||||
"Test013: mid-square hashing (unrolled)"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test013.jvc")
|
||||
$(mkRelFile "Eval/out/test013.geb"),
|
||||
PosTest
|
||||
"Test014: recursion"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test014.jvc")
|
||||
$(mkRelFile "Eval/out/test014.geb"),
|
||||
PosTest
|
||||
"Test015: tail recursion"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test015.jvc")
|
||||
$(mkRelFile "Eval/out/test015.geb"),
|
||||
PosTest
|
||||
"Test016: tail recursion: Fibonacci numbers in linear time"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test016.jvc")
|
||||
$(mkRelFile "Eval/out/test016.geb"),
|
||||
PosTest
|
||||
"Test017: recursion through higher-order functions"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test017.jvc")
|
||||
$(mkRelFile "Eval/out/test017.geb"),
|
||||
PosTest
|
||||
"Test018: tail recursion through higher-order functions"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test018.jvc")
|
||||
$(mkRelFile "Eval/out/test018.geb"),
|
||||
PosTest
|
||||
"Test019: higher-order functions and recursion"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test019.jvc")
|
||||
$(mkRelFile "Eval/out/test019.geb"),
|
||||
PosTest
|
||||
"Test020: McCarthy's 91 function"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test020.jvc")
|
||||
$(mkRelFile "Eval/out/test020.geb"),
|
||||
PosTest
|
||||
"Test021: fast exponentiation"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test021.jvc")
|
||||
$(mkRelFile "Eval/out/test021.geb"),
|
||||
PosTest
|
||||
"Test022: mutual recursion"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test022.jvc")
|
||||
$(mkRelFile "Eval/out/test022.geb"),
|
||||
PosTest
|
||||
"Test023: Euclid's algorithm"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test023.jvc")
|
||||
$(mkRelFile "Eval/out/test023.geb"),
|
||||
PosTest
|
||||
"Test024: Ackermann function"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test024.jvc")
|
||||
$(mkRelFile "Eval/out/test024.geb"),
|
||||
PosTest
|
||||
"Test025: mid-square hashing"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test025.jvc")
|
||||
$(mkRelFile "Eval/out/test025.geb"),
|
||||
PosTest
|
||||
"Test026: letrec"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test026.jvc")
|
||||
$(mkRelFile "Eval/out/test026.geb"),
|
||||
PosTest
|
||||
"Test027: type synonyms"
|
||||
$(mkRelDir ".")
|
||||
$(mkRelFile "Core/test027.jvc")
|
||||
$(mkRelFile "Eval/out/test027.geb")
|
||||
]
|
@ -2,7 +2,6 @@ module Main (main) where
|
||||
|
||||
import Anoma qualified
|
||||
import Asm qualified
|
||||
import BackendGeb qualified
|
||||
import BackendMarkdown qualified
|
||||
import Base
|
||||
import Casm qualified
|
||||
@ -31,8 +30,7 @@ slowTests =
|
||||
sequentialTestGroup
|
||||
"Juvix slow tests"
|
||||
AllFinish
|
||||
[ BackendGeb.allTests,
|
||||
Runtime.allTests,
|
||||
[ Runtime.allTests,
|
||||
Reg.allTests,
|
||||
Asm.allTests,
|
||||
Tree.allTests,
|
||||
|
5
tests/Geb/positive/Compilation/.gitignore
vendored
5
tests/Geb/positive/Compilation/.gitignore
vendored
@ -1,5 +0,0 @@
|
||||
*.lisp
|
||||
*.pir
|
||||
*.pp
|
||||
*.plonk
|
||||
*.proof
|
@ -1,5 +0,0 @@
|
||||
module Package;
|
||||
|
||||
import PackageDescription.Basic open;
|
||||
|
||||
package : Package := basicPackage;
|
@ -1,3 +0,0 @@
|
||||
(right
|
||||
so1
|
||||
(unit))
|
@ -1,3 +0,0 @@
|
||||
(left
|
||||
so1
|
||||
(unit))
|
@ -1,3 +0,0 @@
|
||||
(left
|
||||
so1
|
||||
(unit))
|
@ -1,3 +0,0 @@
|
||||
(left
|
||||
so1
|
||||
(unit))
|
@ -1 +0,0 @@
|
||||
(bit-choice 11)
|
@ -1,2 +0,0 @@
|
||||
(bit-choice 32)
|
||||
|
@ -1 +0,0 @@
|
||||
(bit-choice 8)
|
@ -1,3 +0,0 @@
|
||||
(left
|
||||
so1
|
||||
(unit))
|
@ -1 +0,0 @@
|
||||
(bit-choice 32)
|
@ -1 +0,0 @@
|
||||
(bit-choice 8)
|
@ -1 +0,0 @@
|
||||
(bit-choice 9)
|
@ -1 +0,0 @@
|
||||
(bit-choice 3)
|
@ -1 +0,0 @@
|
||||
(bit-choice 5050)
|
@ -1 +0,0 @@
|
||||
(bit-choice 5050)
|
@ -1 +0,0 @@
|
||||
(bit-choice 55)
|
@ -1 +0,0 @@
|
||||
(bit-choice 771)
|
@ -1 +0,0 @@
|
||||
(bit-choice 55)
|
@ -1 +0,0 @@
|
||||
(bit-choice 5050)
|
@ -1 +0,0 @@
|
||||
(bit-choice 11)
|
@ -1 +0,0 @@
|
||||
(bit-choice 364)
|
@ -1 +0,0 @@
|
||||
(bit-choice 48830320)
|
@ -1 +0,0 @@
|
||||
(bit-choice 6386010)
|
@ -1 +0,0 @@
|
||||
(bit-choice 87)
|
@ -1 +0,0 @@
|
||||
(bit-choice 203)
|
Some files were not shown because too many files have changed in this diff Show More
Loading…
Reference in New Issue
Block a user