mirror of
https://github.com/anoma/juvix.git
synced 2025-01-07 16:22:14 +03:00
c93013229a
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>
54 lines
1.5 KiB
Plaintext
54 lines
1.5 KiB
Plaintext
-- merge sort
|
||
module test032;
|
||
|
||
open import Stdlib.Prelude;
|
||
open import Stdlib.Data.Nat.Ord;
|
||
|
||
split : {A : Type} → Nat → List A → List A × List A;
|
||
split zero xs := (nil, xs);
|
||
split (suc n) nil := (nil, nil);
|
||
split (suc n) (x :: xs) := case split n xs
|
||
| l1, l2 := (x :: l1, l2);
|
||
|
||
terminating
|
||
merge' : List Nat → List Nat → List Nat;
|
||
merge' nil ys := ys;
|
||
merge' xs nil := xs;
|
||
merge' xs@(x :: xs') ys@(y :: ys') := if (x <= y) (x :: merge' xs' ys) (y :: merge' xs ys');
|
||
|
||
terminating
|
||
sort : List Nat → List Nat;
|
||
sort xs :=
|
||
let n : Nat; n := length xs in
|
||
if (n <= 1)
|
||
xs
|
||
(case split (div n 2) xs
|
||
| l1, l2 := merge' (sort l1) (sort l2)
|
||
);
|
||
|
||
terminating
|
||
uniq : List Nat → List Nat;
|
||
uniq nil := nil;
|
||
uniq (x :: nil) := x :: nil;
|
||
uniq (x :: xs@(x' :: _)) := if (x == x') (uniq xs) (x :: uniq xs);
|
||
|
||
gen : List Nat → Nat → (Nat → Nat) → List Nat;
|
||
gen acc zero f := acc;
|
||
gen acc (suc n) f := gen (f (suc n) :: acc) n f;
|
||
|
||
gen2 : List (List Nat) → Nat → Nat → List (List Nat);
|
||
gen2 acc m zero := acc;
|
||
gen2 acc m (suc n) := gen2 (gen nil m ((+) (suc n)) :: acc) m n;
|
||
|
||
printListNatLn : List Nat → IO;
|
||
printListNatLn nil := printStringLn "nil";
|
||
printListNatLn (x :: xs) := printNat x >> printString " :: " >> printListNatLn xs;
|
||
|
||
main : IO;
|
||
main :=
|
||
printListNatLn (take 10 (uniq (sort (flatten (gen2 nil 6 40))))) >>
|
||
printListNatLn (take 10 (uniq (sort (flatten (gen2 nil 9 80))))) >>
|
||
printListNatLn (take 10 (uniq (sort (flatten (gen2 nil 6 80)))));
|
||
|
||
end;
|