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
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
|
From mininix Require Export nix.interp nix.notations.
From stdpp Require Import options.
Open Scope Z_scope.
(** Compare base vals without comparing the proofs. Since we do not have
definitional proof irrelevance, comparing the proofs would fail (and in practice
make Coq loop). *)
Definition res_eq (rv : res val) (bl2 : base_lit) :=
match rv with
| Res (Some (VLit bl1 _)) => bl1 = bl2
| _ => False
end.
Infix "=?" := res_eq.
Definition float_1 :=
ceil: (Float.of_Z 20 /: 3).
Goal interp 100 ∅ float_1 =? 7.
Proof. by vm_compute. Qed.
Definition float_2 :=
Float.of_Z 100000000000000000000000000000000000000000000000000000000000000000000000000000 *:
Float.of_Z 100000000000000000000000000000000000000000000000000000000000000000000000000000 *:
Float.of_Z 100000000000000000000000000000000000000000000000000000000000000000000000000000 *:
Float.of_Z 100000000000000000000000000000000000000000000000000000000000000000000000000000 *:
Float.of_Z 100000000000000000000000000000000000000000000000000000000000000000000000000000.
Goal interp 100 ∅ float_2 =? NFloat (Binary.B754_infinity false).
Proof. by vm_compute. Qed.
Definition float_3 := float_2 /: float_2.
Goal interp 100 ∅ float_3 =? NFloat (`Float.indef_nan).
Proof. by vm_compute. Qed.
Definition let_let :=
let: "x" := 1 in let: "x" := 2 in "x".
Goal interp 100 ∅ let_let =? 2.
Proof. by vm_compute. Qed.
Definition with_let :=
with: EAttr {[ "x" := AttrN 1 ]} in let: "x" := 2 in "x".
Goal interp 100 ∅ with_let =? 2.
Proof. by vm_compute. Qed.
Definition let_with :=
let: "x" := 1 in with: EAttr {[ "x" := AttrN 2 ]} in "x".
Goal interp 100 ∅ let_with =? 1.
Proof. by vm_compute. Qed.
Definition with_with :=
with: EAttr {[ "x" := AttrN 1 ]} in with: EAttr {[ "x" := AttrN 2 ]} in "x".
Goal interp 100 ∅ with_with =? 2.
Proof. by vm_compute. Qed.
Definition with_with_inherit :=
with: EAttr {[ "x" := AttrN 1 ]} in with: EAttr {[ "x" := AttrN "x" ]} in "x".
Goal interp 100 ∅ with_with_inherit =? 1.
Proof. by vm_compute. Qed.
Definition with_loop :=
with: EAttr {[ "x" := AttrR "x" ]} in "x".
Goal interp 100 ∅ with_loop = NoFuel.
Proof. by vm_compute. Qed.
Definition rec_attr_shadow_1 :=
let: "foo" := EAttr {[ "bar" := AttrN 10 ]} in
EAttr {[
"bar" := AttrR ("foo" .: "bar");
"foo" := AttrR (EAttr {[ "bar" := AttrN 20 ]})
]} .: "bar".
Goal interp 100 ∅ rec_attr_shadow_1 =? 20.
Proof. by vm_compute. Qed.
Definition rec_attr_shadow_2 :=
EAttr {[
"y" := AttrR (EAttr {[ "y" := AttrN "z" ]} .: "y");
"z" := AttrR 20
]} .: "y".
Goal interp 100 ∅ rec_attr_shadow_2 =? 20.
Proof. by vm_compute. Qed.
Definition nested_functor_1 :=
EAttr {[ "__functor" := AttrN $ λ: "self",
EAttr {[ "__functor" := AttrN $ λ: "self" "x", 10 ]} ]} 10.
Goal interp 100 ∅ nested_functor_1 =? 10.
Proof. by vm_compute. Qed.
Definition nested_functor_2 :=
EAttr {[ "__functor" := AttrN $
EAttr {[ "__functor" := AttrN $ λ: "self" "self" "x", 10 ]} ]} 10.
Goal interp 100 ∅ nested_functor_2 =? 10.
Proof. by vm_compute. Qed.
Definition functor_loop_1 :=
EAttr {[ "__functor" := AttrN $
λ: "self", "self" "self"
]} 10.
Goal interp 1000 ∅ functor_loop_1 = NoFuel.
Proof. by vm_compute. Qed.
Definition functor_loop_2 :=
EAttr {[ "__functor" := AttrN $
λ: "self" "f", "f" ("self" "f")
]} (λ: "go" "x", "go" "x") 10.
Goal interp 1000 ∅ functor_loop_2 = NoFuel.
Proof. by vm_compute. Qed.
Fixpoint many_lets (i : nat) (e : expr) : expr :=
match i with
| O => e
| S i => let: "x" +:+ pretty i := 0 in many_lets i e
end.
Fixpoint many_adds (i : nat) : expr :=
match i with
| O => 0
| S i => ("x" +:+ pretty i) +: many_adds i
end.
Definition big_prog (i : nat) : expr := many_lets i $ many_adds i.
Definition big := big_prog 1000.
Goal interp 5000 ∅ big =? 0.
Proof. by vm_compute. Qed.
Definition matching_1 :=
(λattr: {[ "x" := None; "y" := None ]}, "x" +: "y")
(EAttr {[ "x" := AttrN 10; "y" := AttrN 11 ]}).
Goal interp 1000 ∅ matching_1 =? 21.
Proof. by vm_compute. Qed.
Definition matching_2 :=
(λattr: {[ "x" := None; "y" := Some (EId' "x") ]}, "x" +: "y")
(EAttr {[ "x" := AttrN 10 ]}).
Goal interp 1000 ∅ matching_2 =? 20.
Proof. by vm_compute. Qed.
Definition matching_3 :=
(λattr: {[ "x" := None; "y" := None ]}, "x" +: "y")
(EAttr {[ "x" := AttrN 10 ]}).
Goal interp 1000 ∅ matching_3 = mfail.
Proof. by vm_compute. Qed.
Definition matching_4 :=
(λattr: {[ "x" := None; "y" := None ]}, "x" +: "y")
(EAttr {[ "x" := AttrN 10; "y" := AttrN 11; "z" := AttrN 12 ]}).
Goal interp 1000 ∅ matching_4 = mfail.
Proof. by vm_compute. Qed.
Definition matching_5 :=
(λattr: {[ "x" := None; "y" := None ]} .., "x" +: "y")
(EAttr {[ "x" := AttrN 10; "y" := AttrN 11; "z" := AttrN 12 ]}).
Goal interp 1000 ∅ matching_5 =? 21.
Proof. by vm_compute. Qed.
Definition matching_6 :=
(λattr: {[ "y" := Some (EId' "y") ]}, "y")
(EAttr {[ "y" := AttrN 10 ]}).
Goal interp 1000 ∅ matching_6 =? 10.
Proof. by vm_compute. Qed.
Definition matching_7 :=
(λattr: {[ "y" := Some (EId' "y") ]}, "y") (EAttr ∅).
Goal interp 1000 ∅ matching_7 = NoFuel.
Proof. by vm_compute. Qed.
Definition matching_8 :=
(λattr: {[ "y" := Some (EId' "y") ]}.., "y")
(EAttr {[ "x" := AttrN 10 ]}).
Goal interp 1000 ∅ matching_8 = NoFuel.
Proof. by vm_compute. Qed.
Definition list_lt_1 :=
EList [ELit 2; ELit 3] <: EList [ELit 3].
Goal interp 1000 ∅ list_lt_1 =? true.
Proof. by vm_compute. Qed.
Definition list_lt_2 :=
EList [ELit 2; ELit 3] <: EList [ELit 2].
Goal interp 1000 ∅ list_lt_2 =? false.
Proof. by vm_compute. Qed.
Definition list_lt_3 :=
EList [ELit 2] <: EList [ELit 2; ELit 3].
Goal interp 1000 ∅ list_lt_3 =? true.
Proof. by vm_compute. Qed.
|
