- Closes#2006
During lambda lifting, we now substitute the calls to the lifted
functions before recursively applying lambda lifting. This will slightly
increase the amount of captured variables. However, I think this is the
only way since we need all identifiers to have a type when recursing.
This PR adds a builtin integer type to the surface language that is
compiled to the backend integer type.
## Inductive definition
The `Int` type is defined in the standard library as:
```
builtin int
type Int :=
| --- ofNat n represents the integer n
ofNat : Nat -> Int
| --- negSuc n represents the integer -(n + 1)
negSuc : Nat -> Int;
```
## New builtin functions defined in the standard library
```
intToString : Int -> String;
+ : Int -> Int -> Int;
neg : Int -> Int;
* : Int -> Int -> Int;
- : Int -> Int -> Int;
div : Int -> Int -> Int;
mod : Int -> Int -> Int;
== : Int -> Int -> Bool;
<= : Int -> Int -> Bool;
< : Int -> Int -> Bool;
```
Additional builtins required in the definition of the other builtins:
```
negNat : Nat -> Int;
intSubNat : Nat -> Nat -> Int;
nonNeg : Int -> Bool;
```
## REPL types of literals
In the REPL, non-negative integer literals have the inferred type `Nat`,
negative integer literals have the inferred type `Int`.
```
Stdlib.Prelude> :t 1
Nat
Stdlib.Prelude> :t -1
Int
:t let x : Int := 1 in x
Int
```
## The standard library Prelude
The definitions of `*`, `+`, `div` and `mod` are not exported from the
standard library prelude as these would conflict with the definitions
from `Stdlib.Data.Nat`.
Stdlib.Prelude
```
open import Stdlib.Data.Int hiding {+;*;div;mod} public;
```
* Closes https://github.com/anoma/juvix/issues/1679
* Closes https://github.com/anoma/juvix/issues/1984
---------
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
Previously we were:
* discarding the types table
* discarding the name ids state
after processing an expression in the REPL.
For example evaluating:
```
let even : _; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10
```
would loop in the REPL.
We noticed that the `n` in `suc n` was being given type `Type` instead
of `Nat`. This was because the name id given to n was incorrect, the
REPL started using name ids from 0 again.
We fixed this issue by storing information, including the types table
and name ids state in the Artifacts data structure that is returned when
we run the pipeline for the first time. This information is then used
when we call functions to compile / type check REPL expressions.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
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
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
* 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>
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>
Adds Juvix tests for the compilation pipeline - these are converted from
the JuvixCore tests (those that make sense). Currently, only the
translation from Juvix to JuvixCore is checked for the tests that can be
type-checked. Ultimately, the entire compilation pipeline down to native
code / WebAssembly should be checked on these tests.
Closes#1689
