-
Notifications
You must be signed in to change notification settings - Fork 4
/
Copy pathenv_cexpScript.sml
103 lines (91 loc) · 3.03 KB
/
env_cexpScript.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
(*
Compiler expressions for stateLang
*)
open HolKernel Parse boolLib bossLib BasicProvers dep_rewrite;
open stringTheory optionTheory sumTheory pairTheory listTheory alistTheory
pure_expTheory pure_semanticsTheory arithmeticTheory mlstringTheory
pred_setTheory;
val _ = new_theory "env_cexp";
val _ = set_grammar_ancestry ["pure_exp","mlstring"];
val _ = numLib.prefer_num();
Type vname = “:mlstring”
Datatype:
cop = Cons mlstring
| AtomOp atom_op
End
Datatype:
cexp = Var vname
| Prim cop (cexp list)
| App cexp cexp
| Lam vname cexp
| Letrec ((vname # cexp) list) cexp
| Let (vname option) cexp cexp
| If cexp cexp cexp
| Delay cexp
| Box cexp
| Force cexp
| Case vname ((vname # (vname list) # cexp) list)
(((vname # num) list # cexp) option)
(* monads *)
| Ret cexp
| Raise cexp
| Bind cexp cexp
| Handle cexp cexp
| Act cexp
| Length cexp
| Alloc cexp cexp
| Deref cexp cexp
| Update cexp cexp cexp
End
Definition cns_arities_def:
cns_arities (Var v :cexp) = {} ∧
cns_arities (Prim op es) = (
(case op of
| Cons cn => {{explode cn, LENGTH es}}
| _ => {}) ∪
BIGUNION (set (MAP cns_arities es))) ∧
cns_arities (App e1 e2) = cns_arities e1 ∪ cns_arities e2 ∧
cns_arities (Lam x e) = cns_arities e ∧
cns_arities (Letrec funs e) =
BIGUNION (set (MAP (λ(v,e). cns_arities e) funs)) ∪ cns_arities e ∧
cns_arities (Let x e1 e2) = cns_arities e1 ∪ cns_arities e2 ∧
cns_arities (If e e1 e2) = cns_arities e ∪ cns_arities e1 ∪ cns_arities e2 ∧
cns_arities (Case v css d) = (
let css_cn_ars = set (MAP (λ(cn,vs,e). explode cn, LENGTH vs) css) in
(case d of
| NONE => {css_cn_ars}
| SOME (a,e) =>
(set (MAP (λ(cn,ar). explode cn, ar) a) ∪ css_cn_ars) INSERT cns_arities e) ∪
BIGUNION (set (MAP (λ(cn,vs,e). cns_arities e) css))) ∧
cns_arities (Box e) = cns_arities e ∧
cns_arities (Delay e) = cns_arities e ∧
cns_arities (Force e) = cns_arities e ∧
cns_arities (Ret e) = cns_arities e ∧
cns_arities (Raise e) = cns_arities e ∧
cns_arities (Act e) = cns_arities e ∧
cns_arities (Length e) = cns_arities e ∧
cns_arities (Bind e1 e2) = cns_arities e1 ∪ cns_arities e2 ∧
cns_arities (Handle e1 e2) = cns_arities e1 ∪ cns_arities e2 ∧
cns_arities (Deref e1 e2) = cns_arities e1 ∪ cns_arities e2 ∧
cns_arities (Alloc e1 e2) = cns_arities e1 ∪ cns_arities e2 ∧
cns_arities (Update e1 e2 e3) = cns_arities e1 ∪ cns_arities e2 ∪ cns_arities e3
Termination
WF_REL_TAC `measure cexp_size`
End
Definition Lams_def:
Lams [] x = x ∧
Lams (y::ys) x = Lam y (Lams ys x)
End
Definition Apps_def:
Apps x [] = x ∧
Apps x (y::ys) = Apps (App x y) ys
End
Definition dest_Delay_def:
dest_Delay (Delay x) = SOME x ∧
dest_Delay _ = NONE
End
Definition dest_Lam_def:
dest_Lam (Lam v x) = SOME (v,x) ∧
dest_Lam _ = NONE
End
val _ = export_theory();