1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-21 05:41:49 +03:00
juvix/app/Commands/Dev/Core/Read.hs

51 lines
2.3 KiB
Haskell
Raw Normal View History

2022-09-14 17:16:15 +03:00
module Commands.Dev.Core.Read where
import Commands.Base
import Commands.Dev.Core.Read.Options
import Evaluator qualified as Eval
import Juvix.Compiler.Core.Options qualified as Core
import Juvix.Compiler.Core.Pretty qualified as Pretty
2022-10-21 20:13:06 +03:00
import Juvix.Compiler.Core.Scoper qualified as Scoper
2022-09-14 17:16:15 +03:00
import Juvix.Compiler.Core.Transformation qualified as Core
import Juvix.Compiler.Core.Transformation.DisambiguateNames qualified as Core
2022-09-14 17:16:15 +03:00
import Juvix.Compiler.Core.Translation.FromSource qualified as Core
Add Geb Backend Evaluator with some extra subcommands (#1808) 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. (https://github.com/anoma/vscode-juvix/commit/31994c8684e9b44a62d58ac13304b9e04503410c)
2023-02-22 17:27:40 +03:00
runCommand ::
forall r a.
( Members '[Embed IO, App] r,
CanonicalProjection a Eval.EvalOptions,
CanonicalProjection a Pretty.Options,
Add Geb Backend Evaluator with some extra subcommands (#1808) 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. (https://github.com/anoma/vscode-juvix/commit/31994c8684e9b44a62d58ac13304b9e04503410c)
2023-02-22 17:27:40 +03:00
CanonicalProjection a CoreReadOptions
) =>
a ->
Sem r ()
2022-09-14 17:16:15 +03:00
runCommand opts = do
gopts <- askGlobalOptions
inputFile :: Path Abs File <- fromAppPathFile sinputFile
2022-12-20 15:05:40 +03:00
s' <- embed . readFile . toFilePath $ inputFile
tab <- getRight (mapLeft JuvixError (Core.runParserMain inputFile Core.emptyInfoTable s'))
let r = run $ runReader (project @GlobalOptions @Core.CoreOptions gopts) $ runError @JuvixError $ Core.applyTransformations (project opts ^. coreReadTransformations) tab
tab0 <- getRight $ mapLeft JuvixError r
let tab' = if project opts ^. coreReadNoDisambiguate then tab0 else Core.disambiguateNames tab0
2022-10-21 20:13:06 +03:00
embed (Scoper.scopeTrace tab')
unless (project opts ^. coreReadNoPrint) $ do
renderStdOut (Pretty.ppOut opts tab')
whenJust (tab' ^. Core.infoMain) $ \sym -> doEval tab' (fromJust $ tab' ^. Core.identContext . at sym)
2022-09-14 17:16:15 +03:00
where
2022-10-21 20:13:06 +03:00
doEval :: Core.InfoTable -> Core.Node -> Sem r ()
doEval tab' node =
if
| project opts ^. coreReadEval -> do
embed (putStrLn "--------------------------------")
embed (putStrLn "| Eval |")
embed (putStrLn "--------------------------------")
Eval.evalAndPrint opts tab' node
| project opts ^. coreReadNormalize -> do
embed (putStrLn "--------------------------------")
embed (putStrLn "| Normalize |")
embed (putStrLn "--------------------------------")
Eval.normalizeAndPrint opts tab' node
| otherwise -> return ()
sinputFile :: AppPath File
sinputFile = project opts ^. coreReadInputFile