mirror of
https://github.com/anoma/juvix.git
synced 2024-12-30 19:14:46 +03:00
9a4da4cab8
This PR introduces an evaluator for the Geb STLC interface/fragment and
other related commands, including a REPL to interact with his backend.
-
https://github.com/anoma/geb/blob/mariari/binaries/src/specs/lambda.lisp
We have included a REPL and support for commands such as read and eval
here. Check out:
```
juvix dev geb --help
```
- [x] Add Geb evaluator with the two basic eval strategies.
- [x] Add quasi quoter: return morphisms from typed geb values.
- [x] Add type/object inference for morphisms.
- [x] All combined: morphisms-eval-to-morphisms
- [x] Parse and pretty printer Geb values (without quoting them)
- [x] Parse files containing Geb terms:
- [x] Saved in a .lisp file according to anoma/geb example (typed
object).
- [x] Store in a .geb file simple as simple lisp expression.
- [x] Add related commands to the CLI for `dev geb`:
- [x] Subcommand: eval
- [x] Subcommand: read
- [x] Subcommand: infer
- [x] Subcommand: repl
- [x] Subcommand: check
- [x] Minor changes `hom` by `!->` in the Geb prettyprinter
- [x] Add tests for:
- [x] New subcommand (smoke tests)
- [x] Eval
Issues to solve after merging this PR:
- Add location to Geb ast for proper error location.
- Add tests for all related subcommands, e.g. check, and infer.
- Check compilation from Core to Geb: (run inferObject with the type
provided by the core node).
- [x] Update the vs code-plugin to load Geb repl and eval.
(31994c8684
)
77 lines
2.1 KiB
Haskell
77 lines
2.1 KiB
Haskell
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")
|