Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add Geb Backend Evaluator with some extra subcommands #1808

Merged
merged 60 commits into from Feb 22, 2023
Merged

Conversation

jonaprieto
Copy link
Collaborator

@jonaprieto jonaprieto commented Feb 3, 2023

This PR introduces an evaluator for the Geb STLC interface/fragment and other related commands, including a REPL to interact with his backend.

We have included a REPL and support for commands such as read and eval here. Check out:

juvix dev geb --help
  • Add Geb evaluator with the two basic eval strategies.
  • Add quasi quoter: return morphisms from typed geb values.
  • Add type/object inference for morphisms.
  • All combined: morphisms-eval-to-morphisms
  • Parse and pretty printer Geb values (without quoting them)
  • Parse files containing Geb terms:
    • Saved in a .lisp file according to anoma/geb example (typed object).
    • Store in a .geb file simple as simple lisp expression.
  • Add related commands to the CLI for dev geb:
    • Subcommand: eval
    • Subcommand: read
    • Subcommand: infer
    • Subcommand: repl
    • Subcommand: check
  • Minor changes hom by !-> in the Geb prettyprinter
  • Add tests for:
    • New subcommand (smoke tests)
    • 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).
  • Update the vs code-plugin to load Geb repl and eval. (anoma/vscode-juvix@31994c8)

@jonaprieto jonaprieto added enhancement New feature or request backend:geb labels Feb 3, 2023
@jonaprieto jonaprieto added this to the 0.3 - Valencia milestone Feb 3, 2023
@jonaprieto jonaprieto self-assigned this Feb 3, 2023
@jonaprieto jonaprieto linked an issue Feb 3, 2023 that may be closed by this pull request
@jonaprieto jonaprieto added the CLI label Feb 10, 2023
@jonaprieto jonaprieto changed the title Add Geb evaluator Add Geb Backend Evaluator Feb 10, 2023
@jonaprieto jonaprieto force-pushed the 1751-geb-evaluator branch 2 times, most recently from 331bdd6 to f758a79 Compare February 15, 2023 10:52
@jonaprieto jonaprieto force-pushed the 1751-geb-evaluator branch 2 times, most recently from 5b887f5 to 7d43158 Compare February 21, 2023 14:06
@jonaprieto jonaprieto marked this pull request as ready for review February 21, 2023 14:08
foo.lisp Outdated Show resolved Hide resolved
@jonaprieto jonaprieto changed the title Add Geb Backend Evaluator Add Geb Backend Evaluator with some extra subcommands Feb 21, 2023
examples/demo/Demo.juvix Outdated Show resolved Hide resolved
@lukaszcz lukaszcz merged commit 9a4da4c into main Feb 22, 2023
@lukaszcz lukaszcz deleted the 1751-geb-evaluator branch February 22, 2023 14:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
backend:geb CLI enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

GEB evaluator
3 participants