forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
cfNormaliseScript.sml
491 lines (447 loc) · 16.3 KB
/
cfNormaliseScript.sml
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
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
(*
Defines the normalise_prog function which puts an arbitrary program
in A-normal form.
*)
open preamble
open set_sepTheory helperLib ml_translatorTheory ConseqConv
open semanticPrimitivesTheory cfHeapsTheory
open cfHeapsBaseLib cfStoreTheory
open cfTacticsBaseLib;
open evaluateTheory
open ASCIInumbersTheory
val _ = new_theory "cfNormalise"
(*------------------------------------------------------------------*)
(** The [cf] function assumes that programs are in "normal form"
(which is close to ANF). These lemmas exploit the fact that some
program is in normal form.
The [cfNormaliseLib.normalise_prog] function puts an arbitrary
program in normal form.
*)
val exp2v_def = Define `
exp2v _ (Lit l) = SOME (Litv l) /\
exp2v env (Var name) = nsLookup env.v name /\
exp2v _ _ = NONE`
Theorem exp2v_evaluate:
!e env st v. exp2v env e = SOME v ==>
evaluate st env [e] = (st, Rval [v])
Proof
Induct \\ fs [exp2v_def, evaluate_def]
QED
val exp2v_list_def = Define `
exp2v_list env [] = SOME [] /\
exp2v_list env (x :: xs) =
(case exp2v env x of
| NONE => NONE
| SOME v =>
(case exp2v_list env xs of
| NONE => NONE
| SOME vs => SOME (v :: vs)))`;
Theorem exp2v_list_evaluate:
!l lv env st. exp2v_list env l = SOME lv ==>
evaluate st env l = (st, Rval lv)
Proof
Induct
THEN1 (fs [exp2v_list_def, evaluate_def])
THEN1 (
rpt strip_tac \\ fs [exp2v_list_def] \\
every_case_tac \\ fs [] \\ rw [] \\
first_assum progress \\ progress exp2v_evaluate \\
Cases_on `l` \\ fs [evaluate_def]
)
QED
Theorem evaluate_rcons:
!env st st' st'' l x lv v.
evaluate st env l = (st', Rval lv) /\
evaluate st' env [x] = (st'', Rval [v]) ==>
evaluate st env (l ++ [x]) = (st'', Rval (lv ++ [v]))
Proof
Induct_on `l`
THEN1 (
rpt strip_tac \\ fs [evaluate_def]
)
THEN1 (
rpt strip_tac \\ fs [evaluate_def] \\
Cases_on `l` \\ fs []
THEN1 (
fs [evaluate_def] \\
last_assum (fn t =>
progress_with t
(CONJ_PAIR evaluatePropsTheory.evaluate_length |> fst)) \\
fs [LENGTH_EQ_NUM_compute]
)
THEN1 (
qpat_x_assum `evaluate _ _ (_::_::_) = _`
(assume_tac o REWRITE_RULE [evaluate_def]) \\
every_case_tac \\ fs [] \\ rw [] \\ first_assum progress \\
simp [evaluate_def]
)
)
QED
Theorem exp2v_list_REVERSE:
!l (st: 'ffi semanticPrimitives$state) lv env. exp2v_list env l = SOME lv ==>
evaluate st env (REVERSE l) = (st, Rval (REVERSE lv))
Proof
Induct \\ rpt gen_tac \\ disch_then (assume_tac o GSYM) \\
fs [exp2v_list_def, evaluate_def] \\
every_case_tac \\ fs [] \\ rw [] \\ irule evaluate_rcons \\
metis_tac [exp2v_evaluate]
QED
Theorem exp2v_list_rcons:
!xs x l env.
exp2v_list env (xs ++ [x]) = SOME l ==>
?xvs xv.
l = xvs ++ [xv] /\
exp2v_list env xs = SOME xvs /\
exp2v env x = SOME xv
Proof
Induct_on `xs` \\ fs [exp2v_list_def] \\ rpt strip_tac \\
every_case_tac \\ fs [] \\
first_assum progress \\ fs [] \\ rw []
QED
Theorem exp2v_list_LENGTH:
!l lv env. exp2v_list env l = SOME lv ==> LENGTH l = LENGTH lv
Proof
Induct_on `l` \\ fs [exp2v_list_def] \\ rpt strip_tac \\
every_case_tac \\ res_tac \\ fs [] \\ rw []
QED
(* [dest_opapp]: destruct an n-ary application. *)
val dest_opapp_def = Define `
dest_opapp (App Opapp l) =
(case l of
| [f; x] =>
(case dest_opapp f of
| SOME (f', args) => SOME (f', args ++ [x])
| NONE => SOME (f, [x]))
| _ => NONE) /\
dest_opapp _ = NONE`
(*------------------------------------------------------------------*)
(*
(* Old implementation of the normalisation pass, as a HOL function.
It has been replaced by the ML implementation in
[cfNormaliseLib.sml], see this file for more details.
*)
(* [mk_opapp]: construct an n-ary application. *)
val mk_opapp_def = tDefine "mk_opapp" `
mk_opapp xs =
if LENGTH xs < 2 then HD xs else
App Opapp [mk_opapp (FRONT xs); LAST xs]`
(WF_REL_TAC `measure LENGTH`
\\ fs [LENGTH_FRONT] \\ Cases \\ fs []);
val MEM_exp_size = Q.prove(
`!args a. MEM a args ==> exp_size a <= exp6_size args`,
Induct \\ fs [astTheory.exp_size_def] \\ rw [] \\ res_tac \\ fs []);
val MEM_exp1_size = Q.prove(
`!rs. MEM (v,a,e') rs ==> exp_size e' < exp1_size rs`,
Induct \\ fs [astTheory.exp_size_def] \\ rw [] \\ res_tac \\ fs []
\\ fs [astTheory.exp_size_def]);
val exp6_size_lemma = Q.prove(
`!xs ys. exp6_size (xs ++ ys) = exp6_size xs + exp6_size ys`,
Induct \\ fs [astTheory.exp_size_def]);
val dest_opapp_size = Q.prove(
`!xs p_1 p_2.
dest_opapp xs = SOME (p_1,p_2) ==>
exp_size p_1 + exp6_size p_2 < exp_size xs`,
recInduct (theorem "dest_opapp_ind") \\ fs [dest_opapp_def]
\\ rw [] \\ every_case_tac \\ fs [] \\ rw []
\\ fs [astTheory.exp_size_def]
\\ res_tac \\ fs [exp6_size_lemma,astTheory.exp_size_def]);
val get_name_aux_def = tDefine "get_name_aux" `
get_name_aux n vs =
let v = "t" ++ num_toString n in
if MEM v vs then get_name_aux (n+1) (FILTER (\x. v <> x) vs) else v`
(WF_REL_TAC `measure (\(n,vs). LENGTH vs)`
\\ rw [] \\ fs [MEM_SPLIT,FILTER_APPEND]
\\ match_mp_tac (DECIDE ``m <= m1 /\ n <= n1 ==> m + n < m1 + (n1 + 1n)``)
\\ fs [LENGTH_FILTER_LEQ]);
val alpha = EVAL ``GENLIST (\n. CHR (n + ORD #"a")) 26`` |> concl |> rand
val alpha_def = Define `alpha = ^alpha`;
(* [get_name vs] returns a fresh name given a list [vs] of already
used names. *)
val get_name_def = Define `
get_name vs =
let ws = FILTER (\s. ~(MEM [s] vs)) alpha in
if NULL ws then get_name_aux 0 vs else [HD ws]`;
(* [Lets [(n1, x1); ...; (nm, xm)] e] is the sequence of Lets:
let n1 = x1 in
let n2 = x2 in
...
let nm = xm in
e
*)
val Lets_def = Define `
Lets [] e = e /\
Lets ((n,x)::xs) e = Let (SOME n) x (Lets xs e)`
val wrap_if_needed_def = Define `
wrap_if_needed needs_wrapping ns e b =
if needs_wrapping then (
let x = get_name ns in
(Var (Short x), x::ns, SNOC (x,e) b)
) else (
(e, ns, b)
)`;
val strip_annot_pat_def = Define `
strip_annot_pat (Pvar v) = Pvar v /\
strip_annot_pat (Plit l) = Plit l /\
strip_annot_pat (Pcon c xs) = Pcon c (strip_annot_pat_list xs) /\
strip_annot_pat (Pref a) = Pref (strip_annot_pat a) /\
strip_annot_pat (Ptannot p _) = strip_annot_pat p /\
strip_annot_pat Pany = Pany /\
strip_annot_pat_list [] = [] /\
strip_annot_pat_list (x::xs) =
strip_annot_pat x :: strip_annot_pat_list xs`;
val strip_annot_exp_def = tDefine"strip_annot_exp"`
(strip_annot_exp (Raise e) =
ast$Raise (strip_annot_exp e))
∧
(strip_annot_exp (Handle e pes) =
Handle (strip_annot_exp e) (strip_annot_pes pes))
∧
(strip_annot_exp (ast$Lit l) = Lit l)
∧
(strip_annot_exp (Con cn es) = Con cn (strip_annot_exps es))
∧
(strip_annot_exp (Var x) = Var x)
∧
(strip_annot_exp (Fun x e) =
Fun x (strip_annot_exp e))
∧
(strip_annot_exp (App op es) =
App op (strip_annot_exps es))
∧
(strip_annot_exp (Log lop e1 e2) =
Log lop (strip_annot_exp e1) (strip_annot_exp e2))
∧
(strip_annot_exp (If e1 e2 e3) =
If (strip_annot_exp e1)
(strip_annot_exp e2)
(strip_annot_exp e3))
∧
(strip_annot_exp (Mat e pes) =
Mat (strip_annot_exp e) (strip_annot_pes pes))
∧
(strip_annot_exp (Let (SOME x) e1 e2) =
Let (SOME x) (strip_annot_exp e1) (strip_annot_exp e2))
∧
(strip_annot_exp (Let NONE e1 e2) =
Let NONE (strip_annot_exp e1) (strip_annot_exp e2))
∧
(strip_annot_exp (Letrec funs e) =
Letrec (strip_annot_funs funs) (strip_annot_exp e))
∧
(strip_annot_exp (Tannot e t) = strip_annot_exp e)
∧
(strip_annot_exp (Lannot e l) = strip_annot_exp e)
∧
(strip_annot_exps [] = [])
∧
(strip_annot_exps (e::es) =
strip_annot_exp e :: strip_annot_exps es)
∧
(strip_annot_pes [] = [])
∧
(strip_annot_pes ((p,e)::pes) =
(strip_annot_pat p, strip_annot_exp e)
:: strip_annot_pes pes)
∧
(strip_annot_funs [] = [])
∧
(strip_annot_funs ((f,x,e)::funs) =
(f,x,strip_annot_exp e) :: strip_annot_funs funs)`
(WF_REL_TAC `inv_image $< (\x. case x of INL e => exp_size e
| INR (INL es) => exps_size es
| INR (INR (INL pes)) => pes_size pes
| INR (INR (INR funs)) => funs_size funs)` >>
srw_tac [ARITH_ss] [size_abbrevs, astTheory.exp_size_def]);
(*
val norm_def = tDefine "norm" `
norm (is_named: bool) (as_value: bool) (ns: string list) (Lit l) = (Lit l, ns, ([]: (string # exp) list)) /\
norm is_named as_value ns (Var (Short name)) = (Var (Short name), name::ns, []) /\
norm is_named as_value ns (Var long) = (Var long, ns, []) /\
norm is_named as_value ns (Let opt e1 e2) =
(case opt of
SOME x =>
(let (e1',ns,b1) = norm T F ns e1 in
let (e2',ns) = protect F (x::ns) e2 in
let e' = Lets b1 (Lets [(x, e1')] e2') in
wrap_if_needed as_value ns e' [])
| NONE =>
(let (e1', ns, b1) = norm F F ns e1 in
let (e2', ns) = protect F ns e2 in
wrap_if_needed as_value ns (Let NONE e1' e2') b1)) /\
norm is_named as_value ns (App Opapp args) =
(case dest_opapp (App Opapp args) of
SOME (f, args) =>
(let (f', ns, b0) = norm F T ns f in
let (args', ns, bi) = norm_list F T ns args in
let e' = mk_opapp (f' :: args') in
let b' = FLAT (REVERSE (b0 :: bi)) (* right-to-left evaluation *) in
wrap_if_needed as_value ns e' b')
| NONE => ARB) /\
norm is_named as_value ns (App op args) =
(let (args', ns, bi) = norm_list F T ns args in
let b' = FLAT (REVERSE bi) in (* right-to-left evaluation *)
wrap_if_needed as_value ns (App op args') b') /\
norm is_named as_value ns (Con x args) =
(let (args', ns, bi) = norm_list F T ns args in
let b = FLAT (REVERSE bi) in (* right-to-left evaluation *)
wrap_if_needed as_value ns (Con x args') b) /\
norm is_named as_value ns (Raise e) =
(let (e',ns,b) = norm F T ns e in
wrap_if_needed as_value ns (Raise e') b) /\
norm is_named as_value ns (Log l e1 e2) =
(let (e1', n1, b1) = norm F T ns e1 in
let (e2', n2, b2) = norm F T n1 e2 in
if b2 = [] then (
if b1 = [] then (
(* produce: <e1> op <e2> *)
(Log l e1' e2', n2, [])
) else (
(* produce: let <b1> in <e1> op <e2> *)
wrap_if_needed as_value n2 (Log l e1' e2') b1
)
) else (
let (e2', n2, b2) = norm F F n1 e2 in
case l of
And =>
(* produce: let <b1> in <e1'> andalso (lets <b2> in <e2'>) *)
wrap_if_needed as_value n2 (Log And e1' (Lets b2 e2')) b1
| Or =>
(* produce: let <b1> in <e1'> orelse (let <b2> in <e2'>) *)
wrap_if_needed as_value n2 (Log Or e1' (Lets b2 e2')) b1
)) /\
norm is_named as_value ns (Fun v e) =
(let (e', ns) = protect is_named (v::ns) e in
wrap_if_needed (as_value \/ ~is_named) ns (Fun v e') []) /\
norm is_named as_value ns (Mat e1 e2) =
(let (e1',n1,b1) = norm F T ns e1 in
let (rows', ni) = norm_rows n1 e2 in
let e' = Mat e1' rows' in
wrap_if_needed as_value ni e' b1) /\
norm is_named as_value ns (Handle e1 e2) =
(let (e1',n1) = protect F ns e1 in
let (rows', ni) = norm_rows n1 e2 in
let e' = Handle e1' rows' in
wrap_if_needed as_value ni e' []) /\
norm is_named as_value ns (If e1 e2 e3) =
(let (e1', ns, b) = norm F T ns e1 in
let (e2', ns) = protect F ns e2 in
let (e3', ns) = protect F ns e3 in
wrap_if_needed as_value ns (If e1' e2' e3') b) /\
norm is_named as_value ns (Letrec rs e) =
(let (rs', ns) = norm_letrec_branches ns rs in
let (e', ns) = protect F ns e in
wrap_if_needed as_value ns (Letrec rs' e') []) /\
norm is_named as_value ns (Tannot e _) =
norm is_named as_value ns e /\
norm is_named as_value ns (Lannot e _) =
norm is_named as_value ns e /\
norm_list is_named as_value ns ([]: exp list) = ([], ns, []) /\
norm_list is_named as_value ns (e::es) =
(let (e', ns, b) = norm is_named as_value ns e in
let (es', ns, bs) = norm_list is_named as_value ns es in
(e' :: es', ns, b::bs)) /\
norm_rows ns ([]: (pat, exp) alist) = ([], ns) /\
norm_rows ns (row :: rows) =
(let (row', ns) = protect_row F ns row in
let (rows', ns) = norm_rows ns rows in
(row' :: rows', ns)) /\
norm_letrec_branches ns ([]: (string, string # exp) alist) = ([], ns) /\
norm_letrec_branches ns (branch :: branches) =
(let (branch', ns) = protect_letrec_branch T ns branch in
let (branches', ns) = norm_letrec_branches ns branches in
(branch' :: branches', ns)) /\
protect is_named ns e =
(let (e',ns,b) = norm is_named F ns e in
(Lets b e', ns)) /\
protect_row is_named ns row =
(let (row_e', ns) = protect is_named ns (SND row) in
((FST row, row_e'), ns)) /\
protect_letrec_branch is_named ns branch =
(let (branch_e', ns) = protect is_named ns (SND (SND branch)) in
((FST branch, FST (SND branch), branch_e'), ns))`
(...);
(* TODO: prove the termination of [norm]. This is probably a bit tricky and
requires refactoring the way [norm] is defined. *)
*)
val full_normalise_def = Define `
full_normalise ns e = FST (protect T ns (strip_annot_exp e))`;
val MEM_v_size = Q.prove(
`!xs. MEM a xs ==> v_size a < v7_size xs`,
Induct \\ fs [v_size_def] \\ rw [] \\ res_tac \\ fs []);
val norm_exp_rel_def = Define `
norm_exp_rel ns e1 e2 <=> (e1 = e2) \/
(full_normalise ns e1 = e2)`
val free_in_def = Define ` (* TODO: complete *)
free_in (Lit l) v = T /\
free_in (Var w) v = (w = v) /\
free_in (Let NONE e1 e2) v = (free_in e1 v \/ free_in e2 v) /\
free_in (Let (SOME x) e1 e2) v = (free_in e1 v \/ (free_in e2 v /\ v <> Short x))`
Inductive norm_rel:
(!i.
norm_rel (Litv i) (Litv i)) /\
(!i.
norm_rel (Loc i) (Loc i)) /\
(!xs ys.
EVERY2 norm_rel xs ys ==>
norm_rel (Vectorv xs) (Vectorv ys)) /\
(!xs ys t.
EVERY2 norm_rel xs ys ==>
norm_rel (Conv t xs) (Conv t ys)) /\
(!v env1 env2 ns e1 e2.
norm_exp_rel ns e1 e2 /\ (free_in e1 = free_in e2) /\
env_rel (free_in e1 DELETE Short v1) env1 env2 ==>
norm_rel (Closure env1 v e1) (Closure env2 v e2)) /\
(!v env1 env2 ns es1 es2.
EVERY2 (\(n1,v1,e1) (n2,v2,e2).
n1 = n2 /\ v1 = v2 /\ norm_exp_rel ns e1 e2 /\ (free_in e1 = free_in e2) /\
env_rel (free_in e1 DELETE Short v1) env1 env2) es1 es2 ==>
norm_rel (Recclosure env1 es1 v) (Recclosure env2 es2 v)) /\
(!env1 env2 s.
(!v x y. v IN s /\
nsLookup env1.v v = SOME x /\
nsLookup env2.v v = SOME y ==>
norm_rel x y) ==>
env_rel s env1 env2)
End
Inductive norm_ref_rel:
(!v1 v2. norm_rel v1 v2 ==> norm_ref_rel (Refv v1) (Refv v2)) /\
(!v1 v2. EVERY2 norm_rel v1 v2 ==> norm_ref_rel (Varray v1) (Varray v2)) /\
(!b. norm_ref_rel (W8array b) (W8array b))
End
Inductive norm_res_rel:
(!v1 v2. norm_rel v1 v2 ==> norm_res_rel (Rval v1) (Rval v2)) /\
(!v1 v2. norm_rel v1 v2 ==> norm_res_rel (Rerr (Rraise v1)) (Rerr (Rraise v2))) /\
(!a. norm_rel v1 v2 ==> norm_res_rel (Rerr (Rabort a)) (Rerr (Rabort a)))
End
val norm_state_rel_def = Define `
norm_state_rel s1 s2 <=>
s1.clock = s2.clock ∧
EVERY2 norm_ref_rel s1.refs s2.refs ∧
s1.ffi = s2.ffi ∧
s1.defined_types = s2.defined_types ∧
s1.defined_mods = s2.defined_mods`
(*
Theorem full_normalise_correct:
env_rel (free_in e) env1 env2 /\ norm_state_rel s1 s2 /\
evaluate ck env1 s1 e1 (rs1,res1) /\ norm_exp_rel e1 e2 ==>
?rs2 res2. evaluate ck env2 s2 e2 (rs2,res2) /\
norm_state_rel rs1 rs2 /\ norm_res_rel res1 res2
Proof
...
QED TODO
*)
val full_normalise_exp_def = Define `
full_normalise_exp exp = full_normalise [] exp`
val full_normalise_decl_def = Define `
full_normalise_decl (Dlet locs pat exp) =
Dlet locs pat (full_normalise [] exp) /\
full_normalise_decl (Dletrec locs l) =
Dletrec locs (MAP (\ (f, n, e). (f, n, full_normalise [f; n] e)) l) /\
full_normalise_decl decl = decl`;
val full_normalise_top_def = Define `
full_normalise_top (Tdec decl) = Tdec (full_normalise_decl decl) /\
full_normalise_top top = top`;
val full_normalise_prog_def = Define `
full_normalise_prog prog = MAP full_normalise_top prog`;
*)
val _ = export_theory ()