This PR adds testing for the core-to-geb translation.
It works as follows:
1. Parse the Juvix Core file.
2. Prepare the Juvix Core node for translation to Geb.
3. Translate the Juvix Core node to Geb.
5. Perform type checking on the translated Geb node to ensure that the
types
from the core node make sense in the Geb context and avoid any Geb
runtime
errors.
6. Evaluate the Juvix Core node to see if it produces the expected
result.
7. Translate the result of the evaluated Juvix Core node to Geb for
comparison
with the expected output later.
8. Compare the result of the evaluation of the Geb term produced in step
3
with the result of the evaluation of the Geb term produced in step 6 to
ensure consistency.
9. If step 8 succeeds, then compare the output of step 6 (the evaluation
of the core
node) with the expected output (given in Geb format) to ensure that
the program is functioning as intended.
This PR goes after:
- https://github.com/anoma/juvix/pull/1863
and
https://github.com/anoma/juvix/pull/1832
This implements a basic version of the algorithm from: Luc Maranget,
[Compiling pattern matching to good decision
trees](http://moscova.inria.fr/~maranget/papers/ml05e-maranget.pdf). No
heuristics are used - the first column is always chosen.
* Closes#1798
* Closes#1225
* Closes#1926
* Adds a global `--no-coverage` option which turns off coverage checking
in favour of generating runtime failures
* Changes the representation of Match patterns in JuvixCore to achieve a
more streamlined implementation
* Adds options to the Core pipeline
* Depends on PR #1909
* Closes#1750
* Adds recursion unrolling tests on JuvixCore
* Adds a version of the mid-square hash example without the recursion
manually unrolled
For now, the recursion is always unrolled to a fixed depth (140). In the
future, we want to add a global option to override this depth, as well
as a mechanism to specify it on a per-function basis. In a more distant
future, we might want to try deriving the unrolling depth heuristically
for each function.
In this PR I will add tests for the example programs in
`examples/milestone`.
There's currently an runtime assertion error generated by the Hanoi
example https://github.com/anoma/juvix/issues/1919, so it'd be good to
test these programs in the future.
This PR changes two things:
- Deploy the documentation website using the (official) deploy action:
- https://github.com/actions/deploy-pages
- Check the documentation generation for all the PRs.
- PR on top of:
- #1905
- #1908
After merging this PR, we could delete the github-pages branch.
This pull request introduces a new workflow that automatically deletes
caches created for closed pull requests. This is necessary because these
caches can quickly accumulate and take up valuable server space, which
is especially important now that we have many pull requests being
created regularly.
Currently, only recursion in functions is checked. This PR also adds
some utilities (TypeDependencyInfo) that will be useful for issue #1907.
---------
Co-authored-by: janmasrovira <janmasrovira@gmail.com>
This PR goes after:
- #1797
Included in this PR:
- Add Clang formatting (v.15) as part of the pre-commits.
- Add new pre-commits:
- forbid binary files
- check toml files for mdbook
- detect-private-key
- format-juvix-examples: check all the Juvix programs in the `examples`
folder type-check for local runs.
- Remove .pre-commit-hooks and add ormolu for local pre-commit runs
instead.
In this PR, I have updated the README file to reflect the new goals of
the project and highlight related products to Juvix. The ORG files have
been replaced with Markdown for better readability and maintainability.
Additionally, I have added a couple of files to fine-tune the mdbook
settings. These changes, I believe, will make it easier for users to
understand and contribute to the project.🤞
- Closes#1878
- New pre-commit hook to format md, yaml, js, CSS files.
To check the website generation, I have deployed the result here:
Work in progress.
- https://jonaprieto.github.io/juvix
- https://github.com/jonaprieto/juvix
---------
Co-authored-by: Paul Cadman <pcadman@gmail.com>
Co-authored-by: Christopher Goes <cwgoes@pluranimity.org>
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
builtin inductive axioms must be registered in the same pass as
inductive types becuase inductive types may use builtin inductives in
the types of their constructors.
```
builtin string axiom String : Type;
type BoxedString :=
| boxed : String -> BoxedString;
```
The separate passes for processing functions and inductives was
unnecessary. This commit combines `registerInductiveDefs` and
`registerFunctionDefs` into a single pass over a modules statements
* Depends on #1832
* Closes#1844
* Adds errors to the Core pipeline
* Checks for no recursion in the GEB pipeline
* Checks for no polymorphism in the GEB pipeline
* Checks for no dynamic type in the GEB pipeline
* Checks for no IO in the GEB pipeline
* Checks for no unsupported builtins in the GEB pipeline
The `rmap` recursor allows to specify changes in binders while going
downward through a Core node. This should help in implementing
transformations on Core which need to add/remove/change binders.
* Depends on PR #1875
* Adds unit tests for `rmap`
* Changes the `NatToInt` transformation to use `rmap`
Print JuvixCore InfoTable in such a way that it can be parsed back by
the JuvixCore parser.
* Depends on PR #1832
* Depends on PR #1862
* Closes#1841
* Adds "JuvixCore print" tests which read the files from
Core/positive/*.jvc, print them, read them back and check if the
evaluation results are preserved.
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* Bump version in package.yaml
* Update version smoke test
* Updates installing doc (though link will not work until we've produced
a linux binary after release)
* Updates changelog.org
* Depends on PR #1832
* Closes#1799
* Removes Backend.C.Translation.FromInternal
* Removes `foreign` and `compile` blocks
* Removes unused test files
* Removes the old C runtime
* Removes other dead code
* Depends on PR #1824
* Closes#1556
* Closes#1825
* Closes#1843
* Closes#1729
* Closes#1596
* Closes#1343
* Closes#1382
* Closes#1867
* Closes#1876
* Changes the `juvix compile` command to use the new pipeline.
* Removes the `juvix dev minic` command and the `BackendC` tests.
* Adds the `juvix eval` command.
* Fixes bugs in the Nat-to-integer conversion.
* Fixes bugs in the Internal-to-Core and Core-to-Core.Stripped
translations.
* Fixes bugs in the RemoveTypeArgs transformation.
* Fixes bugs in lambda-lifting (incorrect de Bruijn indices in the types
of added binders).
* Fixes several other bugs in the compilation pipeline.
* Adds a separate EtaExpandApps transformation to avoid quadratic
runtime in the Internal-to-Core translation due to repeated calls to
etaExpandApps.
* Changes Internal-to-Core to avoid generating matches on values which
don't have an inductive type.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Co-authored-by: janmasrovira <janmasrovira@gmail.com>
- Closes#1879
The issue was possibly caused by the use of `readerState`:
```
readerState :: forall a r x. (Member (State a) r) => Sem (Reader a ': r) x -> Sem r x
readerState m = get >>= (`runReader` m)
```
I originally thought it would be a good idea to "freeze" some `State`
effect into a `Reader` effect in the following situation:
- Some function `s` needs to update the state.
- Some function `f` only reads the state.
- Then you would have `g .. = ... readerState @MyState f`
- This way, it would be reflected in the type that `g` cannot update the
state. However, for some reason I have not been able to clearly
identify, this was not working as expected.
* Fixes https://github.com/anoma/juvix/issues/1811
This PR updates:
* The CI workflows to use GHC 9.2.6
* The stack resolver to LTS-20.12
* The cabal.project to point to stackage LTS-20.12
* The linux static build CI to use alpine GHC 9.2.6
NB: You may need to install GHC 9.2.6 and run `cabal update` before
trying the build with `cabal`.
This pr implements pretty printing of patterns using the Ape interface.
This means that we will have pretty chains of infix constructors and `,`
will be printed as expected (in a pattern), i.e. `(a, b)` instead of `(a
, b)`
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
This PR adds support for all recent changes in GEB introduced by:
- https://github.com/anoma/geb/pull/70
- Closes#1814
Summary:
- [x] Add LeftInj, RightIng, and Absurd types in GEB language
- [x] Fix FromCore translation for the new data types and minor code
styling issues.
- [x] Fix GEB-STLC type inference and checking
- [X] Add support for evaluating typed morphism "(typed ...)" in the Geb
repl and .geb files.
- [x] Simplify a bit the Geb parser
- [x] Fix `dev geb check` command
- [x] Type check files in `tests/Geb/positive`
After this PR, we should include interval location for Geb terms to
facility debugging type-checking errors.
The pretty printer for `Core` depends on `substEnv`, so it is convenient
to have it isolated so that it is possible to use ``ppTrace`` when
debugging functions in `Core.Utils` (or anything depending on it).
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)
I paired with @janmasrovira on this work.
Before this change - long type signatures were formatted to contain line
breaks within applications:
```
exampleFunction : {A : Type} -> List A -> List A -> List
A -> List A -> List A -> List A -> List A -> Nat;
```
After this change we treat `->` and an infix operator and format like
other infix applications:
```
exampleFunction :
{A : Type}
-> List A
-> List A
-> List A
-> List A
-> List A
-> List A
-> List A
-> Nat;
```
* Fixes#1850
Co-authored-by: @janmasrovira
