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}
```
Core transformations apply to the whole InfoTable, the REPL needs to
apply Core transformations to the single node that it compiles from the
user input string.
The solution in this commit is to:
1. Compile the input string as before to obtain a Core Node.
2. Add this Node to a copy of the Core InfoTable for the loaded file.
3. Apply the (CLI specified) Core transformations to this InfoTable.
4. Extract the (now transformed) Node from the InfoTable.
We can think of a way to improve this, maybe when we tackle allowing the
user to make new definitions in the REPL.
As soon as compilation of pattern matching is complete we should enable
some (all?) Core transformations by default.
Example:
At the moment we get the following result in the REPL:
```
juvix repl
...
Stdlib.Prelude> 1 + 1
suc (suc zero)
```
After this commit we can turn on `nat-to-int` transformation:
```
juvix repl -t nat-to-int
Stdlib.Prelude> 1 + 1
2
```
* Part of https://github.com/anoma/juvix/issues/1531
This PR:
- Closes#1647
It gives compilation errors for language features that require more
substantial support (recursion, polymorphism). The additional features
are to be implemented in future separate PRs.
* Adds a new target `geb` to the CLI command `juvix dev core compile`,
which produces a `*.geb` output file in the `.juvix-build` directory.
* Adds a few tests. These are not yet checked automatically because
there is no GEB evaluator; checking the `*.geb` output would be too
brittle.
This PR addresses a caching issue in our CI by streamlining each
operating system's build and test processes, reducing CI time. 🤞 Also,
our caching strategy has been updated with the new restore/save actions.
For example, we aim to cache the .stack folder, and if the stack build
is successful, the .stack-build. The building documentation job
continues depending on the Linux build. Upon merging this PR, we get
back to the point where the CI maintain a cache for each OS to be shared
among all PRs, significantly reducing CI testing time. The expected
scenario is as follows. The CI can take, on average, 35' in Linux to
build and test everything. Using caching, that time is reduced to less
than 10'. macOS is a different story. It can easily take one hour, and
even more, the first time to build and test the project. After that, it
might take an average of 20'.
- Caching strategies
[descriptions](https://github.com/actions/cache/blob/main/caching-strategies.md#saving-cache-even-if-the-build-fails)
- Closes#1776
Before this change, nested as-patterns (i.e as-patterns binding
arguments to constructors) were not translated to Core pattern binders.
This meant that the following function would crash the compiler:
```
f : List Nat -> List Nat;
f (x :: a@(x' :: xs)) := a;
f _ := nil;
```
i.e the nested as-pattern `a` was ignored in the internal to core
translation.
This commit translates each as-pattern to a Core `PatternBinder`.
* Fixes https://github.com/anoma/juvix/issues/1788
* Fixes https://github.com/anoma/juvix/issues/1738
- Closes#1637.
A function type signature is now allowed to have a body. This is valid
for both top level and let definitions.
```
not : Bool -> Bool := λ {
| true := false
| false := true
};
```
This PR adds a new field `infoBuiltins : HashMap BuiltinPrim IdentKind`
to the Core InfoTable. This is used to register builtin inductive,
constructors and functions against their corresponding Core
symbols/tags.
The point of doing this is to make it easier to lookup the Infos for
builtins during the internal to core translation:
d91241a685/src/Juvix/Compiler/Core/Translation/FromInternal.hs (L65)
This is one proposed approach, I think Jan mentioned using the Builtins
effect for this but it doesn't seem appropriate to expose the
registration function from the Builtins effect at this part of the code.
Perhaps I misunderstood, if so I'm happy to revisit this refactor.
The integer to Nat translation in the Internal to Core translation
depends on both Nat and Bool builtin types being in the InfoTable.
544bddba43/src/Juvix/Compiler/Core/Translation/FromInternal.hs (L67)
If the root module does not contain an explicit reference to the builtin
Bool (for example) then builtin Bool type is filtered out by the
reachability analysis and therefore is not available at transltaion
time.
In this commit we add both builtin Nat and builtin Bool as start nodes
in the reachability analysis to guarantee that they will not be filtered
out.
- Fixes https://github.com/anoma/juvix/issues/1774
- Fixes#1723
- It refactors parsing/scoping so that the scoper does not need to read
files or parse any module. Instead, the parser takes care of parsing all
the imported modules transitively.
Filepaths within a Loc must now be absolute or an error is thrown when
mkLoc is called. This Loc is used when displaying errors.
This commit uses imaginary absolute file paths in the Core repl and Asm
commands in the cases (parsing a single expression for example).
Before this fix, the `core {repl, read, eval}` and `asm` commands would
crash if it encountered an error when invoked with a relative path, or
in the case of a repl when parsing a single expression.
Filepaths within a `Loc` must now be absolute or an error is thrown when
`mkLoc` is called. This `Loc` is used when displaying errors.
This commit converts the Core evaluator filepath to an absolute path
before calling `mkLoc`.
Before this fix, the Core evaluator would crash if it encountered an
error instead of displaying the error if called on a relative path.
The current Github action responsible for installing Wasmer fails from
time to time, and it also is outdated, not following the new NodeJS 16
requirement by Github.
We could use https://github.com/jaxxstorm/action-install-gh-release
instead, but unfortunately, it does not have the proper support to
expose the binaries contained in an inner folder, as in the case with
the Wasmer release. In the meantime, let's use my
[fork](https://github.com/jonaprieto/action-install-gh-release) while I
open PR to the main repository.
