1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
|
val add_int = {ocaml: "add_int", lem: "integerAdd"} : (int, int) -> int
overload operator + = {add_int}
val eq_int = {ocaml: "eq_int", lem: "eq"} : (int, int) -> bool
val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq"} : forall ('a : Type). ('a, 'a) -> bool
overload operator == = {eq_int, eq_anything}
/* Test constant propagation part of monomorphisation involving
functions. We should reduce a function application when the
arguments are suitable values, the function is pure and the result
is a value.
*/
enum AnEnum = One | Two | Three
union EnumlikeUnion = { First, Second }
union ProperUnion = {
Stuff : AnEnum,
Nonsense : EnumLikeUnion
}
val canReduce : AnEnum -> AnEnum
function canReduce (x) = {
match (x) {
One => Two,
x => x
}
}
val cannotReduce : AnEnum -> int
function cannotReduce (x) = {
let y : int = match (x) { One => 1, _ => 5 } in
2 + y
}
register whatever : int
val impure : AnEnum -> AnEnum effect {rreg}
function impure (x) = {
match (x) {
One => Two,
x => let _ = whatever in x
}
}
val canReduceUnion : AnEnum -> EnumlikeUnion
function canReduceUnion (x) = {
match (x) {
One => First,
_ => Second
}
}
val canReduceUnion2 : AnEnum -> ProperUnion
function canReduceUnion2 (x) = {
match (x) {
One => Nonsense(First),
y => Stuff(y)
}
}
val test : AnEnum -> (AnEnum,int,AnEnum,EnumlikeUnion,ProperUnion) effect {rreg}
function test (x) = {
let a = canReduce(x) in
let b = cannotReduce(x) in
let c = impure(x) in
let d = canReduceUnion(x) in
let e = canReduceUnion2(x) in
(a,b,c,d,e)
}
val run : unit -> unit effect {rreg,escape}
function run () = {
assert(test(One) == (Two,3,Two,First,Nonsense(First)));
assert(test(Two) == (Two,7,Two,Second,Stuff(Two)));
assert(test(Three) == (Three,7,Three,Second,Stuff(Three)));
}
|
