1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-21 22:01:41 +03:00
juvix/app/Commands/Dev/Options.hs

139 lines
3.5 KiB
Haskell
Raw Normal View History

2022-09-14 17:16:15 +03:00
module Commands.Dev.Options
( module Commands.Dev.Options,
2022-09-29 18:44:55 +03:00
module Commands.Dev.Asm.Options,
2022-09-14 17:16:15 +03:00
module Commands.Dev.Core.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
module Commands.Dev.Geb.Options,
2022-09-14 17:16:15 +03:00
module Commands.Dev.Internal.Options,
module Commands.Dev.Parse.Options,
module Commands.Dev.Highlight.Options,
module Commands.Dev.Scope.Options,
module Commands.Dev.Termination.Options,
2022-12-20 15:05:40 +03:00
module Commands.Dev.DisplayRoot.Options,
2022-09-14 17:16:15 +03:00
)
where
2022-12-06 13:33:20 +03:00
import Commands.Dev.Asm.Options hiding (Compile)
2022-09-14 17:16:15 +03:00
import Commands.Dev.Core.Options
2022-12-20 15:05:40 +03:00
import Commands.Dev.DisplayRoot.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
import Commands.Dev.Geb.Options
2022-09-14 17:16:15 +03:00
import Commands.Dev.Highlight.Options
import Commands.Dev.Internal.Options
import Commands.Dev.Parse.Options
import Commands.Dev.Repl.Options
2022-11-03 11:38:09 +03:00
import Commands.Dev.Runtime.Options
2022-09-14 17:16:15 +03:00
import Commands.Dev.Scope.Options
import Commands.Dev.Termination.Options
import Commands.Repl.Options
2022-09-14 17:16:15 +03:00
import CommonOptions
data DevCommand
2022-12-20 15:05:40 +03:00
= DisplayRoot RootOptions
2022-09-14 17:16:15 +03:00
| Highlight HighlightOptions
| Internal InternalCommand
| Core CoreCommand
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
| Geb GebCommand
2022-09-29 18:44:55 +03:00
| Asm AsmCommand
2022-11-03 11:38:09 +03:00
| Runtime RuntimeCommand
2022-09-14 17:16:15 +03:00
| Parse ParseOptions
| Scope ScopeOptions
| Termination TerminationCommand
| JuvixDevRepl ReplOptions
2022-09-14 17:16:15 +03:00
deriving stock (Data)
parseDevCommand :: Parser DevCommand
parseDevCommand =
hsubparser
( mconcat
[ commandHighlight,
commandInternal,
commandCore,
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
commandGeb,
2022-09-29 18:44:55 +03:00
commandAsm,
2022-11-03 11:38:09 +03:00
commandRuntime,
2022-09-14 17:16:15 +03:00
commandParse,
commandScope,
commandShowRoot,
commandTermination,
commandJuvixDevRepl
2022-09-14 17:16:15 +03:00
]
)
commandHighlight :: Mod CommandFields DevCommand
commandHighlight =
command "highlight" $
info
(Highlight <$> parseHighlight)
(progDesc "Highlight a Juvix file")
commandInternal :: Mod CommandFields DevCommand
commandInternal =
command "internal" $
info
(Internal <$> parseInternalCommand)
(progDesc "Subcommands related to Internal")
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
commandGeb :: Mod CommandFields DevCommand
commandGeb =
command "geb" $
info
(Geb <$> parseGebCommand)
(progDesc "Subcommands related to JuvixGeb")
2022-09-14 17:16:15 +03:00
commandCore :: Mod CommandFields DevCommand
commandCore =
command "core" $
info
(Core <$> parseCoreCommand)
(progDesc "Subcommands related to JuvixCore")
2022-09-29 18:44:55 +03:00
commandAsm :: Mod CommandFields DevCommand
commandAsm =
command "asm" $
info
(Asm <$> parseAsmCommand)
(progDesc "Subcommands related to JuvixAsm")
2022-11-03 11:38:09 +03:00
commandRuntime :: Mod CommandFields DevCommand
commandRuntime =
command "runtime" $
info
(Runtime <$> parseRuntimeCommand)
(progDesc "Subcommands related to the Juvix runtime")
2022-09-14 17:16:15 +03:00
commandParse :: Mod CommandFields DevCommand
commandParse =
command "parse" $
info
(Parse <$> parseParse)
(progDesc "Parse a Juvix file")
commandScope :: Mod CommandFields DevCommand
commandScope =
command "scope" $
info
(Scope <$> parseScope)
(progDesc "Parse and scope a Juvix file")
commandShowRoot :: Mod CommandFields DevCommand
commandShowRoot =
command "root" $
info
2022-12-20 15:05:40 +03:00
(DisplayRoot <$> parseRoot)
2022-09-14 17:16:15 +03:00
(progDesc "Show the root path for a Juvix project")
commandTermination :: Mod CommandFields DevCommand
commandTermination =
command "termination" $
info
(Termination <$> parseTerminationCommand)
(progDesc "Subcommands related to termination checking")
commandJuvixDevRepl :: Mod CommandFields DevCommand
commandJuvixDevRepl =
command
"repl"
( info
(JuvixDevRepl <$> parseDevRepl)
(progDesc "Run the Juvix dev REPL")
)