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
This PR adds the `match-to-case` Core transformation. This transforms
pattern matching nodes to a sequence of case and let nodes.
## High level description
Each branch of the match is compiled to a lambda. In the combined match
Each branch of the match is compiled to a lambda. These lambdas are
combined in nested lets and each lambda is called in turn as each branch
gets checked. The lambda corresponding to the first branch gets called
first, if the pattern match in the branch fails, the lambda
corresponding to the next branch is called and so on. If no branches
match then a lambda is called which returns a fail node.
Conceptually:
<table>
<tr>
<td>
Core
</td>
<td>
Transformed
</td>
</tr>
<tr>
<td>
```
match v1 .. vn {
b1
b2
...
bk
}
```
</td>
<td>
```
λ
let c0 := λ FAIL in
let ck := λ {...} in
...
let c1 := λ {...} in
c1 v1 ... vn
```
</td>
</tr>
</table>
The patterns on each branch are compiled to either let bindings (pattern
binders) or case expressions (constructor patterns).
Auxillary bindings are added in the case of nested constructor patterns.
The default branch in each case expression has a call to the lambda
corresponding to the next branch of the match. This is because the
default
branch is reached if the pattern match fails.
<table>
<tr>
<td>
Pattern match
</td>
<td>
Transformed
</td>
</tr>
<tr>
<td>
```
suc (suc n) ↦ n
```
</td>
<td>
```
case ?$0 of {
suc arg_8 := case ?$0 of {
suc n := let n := ?$0 in n$0;
_ := ?$2 ?$1
};
_ := ?$1 ?$0
}
```
</td>
</tr>
</table>
The body of each branch is wrapped in let bindings so that the indicies
of bound
variables in the body point to the correct variables in the compiled
expression.
This is necessary because the auxiliary bindings added for nested
constructor
patterns will cause the original indicies to be offset.
Finally, the free variables in the match branch body need to be shifted
by all the bindings we've added as part of the compilation.
## Examples
### Single wildcard
<table>
<tr>
<td> Juvix </td> <td> Core </td> <td> Transformed Core </td>
</tr>
<tr>
<td>
```
f : Nat -> Nat;
f _ := 1;
```
</td>
<td>
```
λ? match ?$0 with {
_ω309 ↦ ? 1
}
```
</td>
<td>
```
λ? let ? := λ? fail "Non-exhaustive patterns" in
let ? := λ? let _ω309 := ?$0 in
let _ω309 := ?$0 in 1 in
?$0 ?$2
```
</td>
</tr>
</table>
### Single binder
<table>
<tr>
<td> Juvix </td> <td> Core </td> <td> Transformed Core </td>
</tr>
<tr>
<td>
```
f : Nat -> Nat;
f n := n;
```
</td>
<td>
```
λ? match ?$0 with {
n ↦ n$0
}
```
</td>
<td>
```
λ? let ? := λ? fail "Non-exhaustive patterns" in
let ? := λ? let n := ?$0 in
let n := ?$0 in n$0 in
?$0 ?$2
```
</td>
</tr>
</table>
### Single Constructor
<table>
<tr>
<td> Juvix </td> <td> Core </td> <td> Transformed Core </td>
</tr>
<tr>
<td>
```
f : Nat -> Nat;
f (suc n) := n;
```
</td>
<td>
```
λ? match ?$0 with {
suc n ↦ n$0
}
```
</td>
<td>
```
λ? let ? := λ? fail "Non-exhaustive patterns" in let ? := λ? case ?$0 of {
suc n := let n := ?$0 in let n := ?$0 in n$0;
_ := ?$1 ?$0
} in ?$0 ?$2
```
</td>
</tr>
</table>
### Nested Constructor
<table>
<tr>
<td> Juvix </td> <td> Core </td> <td> Transformed Core </td>
</tr>
<tr>
<td>
```
f : Nat -> Nat;
f (suc (suc n)) := n;
```
</td>
<td>
```
λ? match ?$0 with {
suc (suc n) ↦ n$0
}
```
</td>
<td>
```
λ? let ? := λ? fail "Non-exhaustive patterns" in let ? := λ? case ?$0 of {
suc arg_8 := case ?$0 of {
suc n := let n := ?$0 in let n := ?$0 in n$0;
_ := ?$2 ?$1
};
_ := ?$1 ?$0
} in ?$0 ?$2
```
</td>
</tr>
</table>
### Multiple Branches
<table>
<tr>
<td> Juvix </td> <td> Core </td> <td> Transformed Core </td>
</tr>
<tr>
<td>
```
f : Nat -> Nat;
f (suc n) := n;
f zero := 0;
```
</td>
<td>
```
λ? match ?$0 with {
suc n ↦ n$0;
zero ↦ ? 0
}
```
</td>
<td>
```
λ? let ? := λ? fail "Non-exhaustive patterns" in let ? := λ? case ?$0 of {
zero := ? 0;
_ := ?$1 ?$0
} in let ? := λ? case ?$0 of {
suc n := let n := ?$0 in let n := ?$0 in n$0;
_ := ?$1 ?$0
} in ?$0 ?$3
```
</td>
</tr>
</table>
### Nested case with captured variable
<table>
<tr>
<td> Juvix </td> <td> Core </td> <td> Transformed Core </td>
</tr>
<tr>
<td>
```
f : Nat -> Nat -> Nat;
f n m := case m
| suc k := n + k;
```
</td>
<td>
```
f = λ? λ? match ?$1, ?$0 with {
n, m ↦ match m$0 with {
suc k ↦ + n$2 k$0
}
}
```
</td>
<td>
```
λ? λ?
let ? := λ? λ? fail "Non-exhaustive patterns" in
let ? := λ? λ? let n := ?$1 in let m := ?$1 in let n := ?$1 in let m := ?$1 in
let ? := λ? fail "Non-exhaustive patterns" in let ? := λ? case ?$0 of {
suc k := let k := ?$0 in let k := ?$0 in + n$6 k$0;
_ := ?$1 ?$0
} in ?$0 m$2 in ?$0 ?$3 ?$2
```
</td>
</tr>
</table>
## Testing
The `tests/Compilation/positive` tests are run up to the Core evaluator
with `match-to-case` and `nat-to-int` transformations on Core turned on.
---------
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
- Closes#1793.
Now, if the body of a function clause does not fit in a line, the body
will start indented in the next line.
The example presented in the linked issue is now formatted thus:
```
go n s :=
if
(s < n)
(go (sub n 1) s)
(go n (sub s n) + go (sub n 1) s);
```
This pr adds the `_lambdaType :: Maybe Expression` to `Internal.Lambda`.
This field will be `Nothing` before typechecking and `Just _` after it.
The type is printed if present. For example if the input of `juvix dev
internal typecheck M.juvix --print-result` is the following:
```
id : {A : Type} → A → A
id := λ { a := a}
```
Then the output is as follows:
```
id : {A : Type} → A → A
id {_ω209} := λ : _ω209 → _ω209 {| a := a}
```
