-
Notifications
You must be signed in to change notification settings - Fork 0
/
cps.ml
216 lines (189 loc) · 6.91 KB
/
cps.ml
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
open Syntax
open Support.Error
exception NoRuleApplies
(* for the ease of typing *)
type cps_term =
| Var of string
| Fix of string * string * ty option * cps_term
| Abs of string * ty option * cps_term
| App of cps_term * cps_term
| Let of string * cps_term * cps_term
| Shift of string * cps_term
| Reset of cps_term
| If of cps_term * cps_term * cps_term
| Succ of cps_term
| Pred of cps_term
| IsZero of cps_term
| Nat of int
| Bool of bool
(***** support for list *******)
| Cons of cps_term * cps_term
| Nil
(* lmatch t1 { case nil => t2 case hd :: tl => t3 } *)
| LMatch of cps_term * cps_term * string * string * cps_term
let rec cps_term_to_term (t: cps_term) : term = (match t with
| Var(s) -> dummyinfo, AnNone,
TmVar(s)
| Fix(f, x, ty, t') -> dummyinfo, AnNone,
TmFix(AnNone, f, x, ty, cps_term_to_term t')
| Abs(x, ty, t') -> dummyinfo, AnNone,
TmAbs(AnNone, x, ty, cps_term_to_term t')
| App(t1, t2) -> dummyinfo, AnNone,
TmApp(AnNone, cps_term_to_term t1, cps_term_to_term t2)
| Let(x, v, t') -> dummyinfo, AnNone,
TmLet(x, cps_term_to_term v, cps_term_to_term t')
| Shift(x, t') -> dummyinfo, AnNone,
TmShift(AnNone, x, cps_term_to_term t')
| Reset(t') -> dummyinfo, AnNone,
TmReset(cps_term_to_term t')
| If(c, v1, v2) -> dummyinfo, AnNone,
TmIf(cps_term_to_term c, cps_term_to_term v1, cps_term_to_term v2)
| Succ(t') -> dummyinfo, AnNone,
TmSucc(cps_term_to_term t')
| Pred(t') -> dummyinfo, AnNone,
TmPred(cps_term_to_term t')
| IsZero(t') -> dummyinfo, AnNone,
TmIsZero(cps_term_to_term t')
| Nat(v) -> dummyinfo, AnNone, TmNat(v)
| Bool(v) -> dummyinfo, AnNone, TmBool(v)
(***** support for list *******)
| Cons(t1, t2) -> dummyinfo, AnNone,
TmCons(cps_term_to_term t1, cps_term_to_term t2)
| Nil -> dummyinfo, AnNone, TmNil
| LMatch(a, b, c, d, e) -> dummyinfo, AnNone,
TmLMatch(cps_term_to_term a, cps_term_to_term b, c, d, cps_term_to_term e)
) (* end of match *)
let new_k () : string = freshname "?k"
let new_v () : string = freshname "?v"
let is_pure (t: term) : bool = (match t with
| (_, AnPure, _) -> true
| _ -> false)
(* see Figure 8. *)
let rec cps_pure (t: term) : cps_term = (match t with
| (_, AnImpure, _) -> raise NoRuleApplies
| (_, AnId(_), _) -> raise NoRuleApplies
| (_, AnNone, _) -> raise NoRuleApplies
(* constant *)
| (_, _, TmNat v) -> Nat v
| (_, _, TmBool v) -> Bool v
(* variable *)
| (_, _, TmVar v) -> Var v
(* abstraction #1 *)
| (_, _, TmAbs(AnPure, _1, _2, e1)) when is_pure e1
-> Abs(_1, _2, cps_pure e1)
(* abstraction #2 *)
| (_, _, TmAbs(AnImpure, _1, _2, e1)) when is_pure e1
-> let k : string = new_k () in
Abs(_1, _2,
Abs(k, None,
App(Var(k), cps_pure e1)))
(* abstraction #3 *)
| (_, _, TmAbs(AnImpure, _1, _2, e1)) when not @@ is_pure e1
-> let k : string = new_k () in
Abs(_1, _2,
Abs(k, None,
cps_with_k e1 (fun v -> App(Var(k), v))))
(* Fix #1 *)
| (_, _, TmFix(AnPure, f, x, ty, e1))
-> Fix(f, x, ty, cps_pure e1)
(* Fix #2 *)
| (_, _, TmFix(AnImpure, f, x, ty, e1)) when is_pure e1
-> let k : string = new_k () in
Abs(x, ty, Abs(k, None, App(Var(k),
App(Fix(f, x, ty, cps_pure e1), Var(x)))))
(* Fix #3 *)
| (_, _, TmFix(AnImpure, f, x, ty, e1)) when not @@ is_pure e1
-> let k : string = new_k () in
Fix(f, x, ty,
Abs(k, None,
cps_with_k e1 (fun v -> App(Var(k), v))))
(* Application *)
| (_, _, TmApp(AnPure, e1, e2))
-> App(cps_pure e1, cps_pure e2)
(* Reset #1 *)
| (_, _, TmReset(e1)) when is_pure e1
-> cps_pure e1
(* Reset #2 *)
| (_, _, TmReset(e1)) when not @@ is_pure e1
-> cps_with_k e1 @@ fun v -> v
(* let *)
| (_, _, TmLet(x, e1, e2)) when is_pure e1 && is_pure e2
-> Let(x, cps_pure e1, cps_pure e2)
(* if *)
| (_, _, TmIf(e1, e2, e3)) when is_pure e1 && is_pure e2 && is_pure e3
-> If(cps_pure e1, cps_pure e2, cps_pure e3)
(* Primitive functions *)
| (_, _, TmSucc(e1)) -> Succ(cps_pure e1)
| (_, _, TmPred(e1)) -> Pred(cps_pure e1)
| (_, _, TmIsZero(e1)) -> IsZero(cps_pure e1)
(* List Manipulation *)
| (_, _, TmCons(e1, e2))
-> Cons(cps_pure e1, cps_pure e2)
| (_, _, TmNil)
-> Nil
| (_, _, TmLMatch (e1, e2, hd, tl, e3))
-> LMatch(cps_pure e1, cps_pure e2, hd, tl, cps_pure e3)
| _ -> raise NoRuleApplies)
and cps_with_k (t: term) (k: cps_term -> cps_term) : cps_term = (match t with
| (_, AnPure, _) -> k @@ cps_pure t
(* Application *)
| (_, _, TmApp(AnPure, e1, e2))
-> cps_with_k e1 @@ fun v1 ->
cps_with_k e2 @@ fun v2 ->
k @@ App(v1, v2)
| (_, _, TmApp(AnImpure, e1, e2))
-> cps_with_k e1 @@ fun v1 ->
cps_with_k e2 @@ fun v2 ->
let v : string = new_v () in
App(App(v1, v2), Abs(v, None, k @@ Var v))
(* Shift *)
| (_, _, TmShift(AnPure, x, e1))
-> let v : string = new_v () in
Let(x, Abs(v, None, k @@ Var v),
cps_with_k e1 @@ fun v1 -> v1)
| (_, _, TmShift(AnImpure, x, e1))
-> let v : string = new_v () and k' : string = new_k () in
Let(x,
Abs(v, None,
Abs(k', None, k @@ Var v)),
cps_with_k e1 @@ fun v1 -> v1)
(* let *)
| (_, _, TmLet(x, v1, e2)) when is_pure v1
-> Let(x, cps_pure v1, cps_with_k e2 k)
| (fi, _, TmLet(x, v1, e2)) when not @@ is_pure v1
-> cps_with_k
(fi, AnImpure, TmApp(AnImpure,
(fi, AnPure, TmAbs(AnImpure, x, None, e2)),
v1)) k
(* if *)
| (_, _, TmIf(e1, e2, e3))
-> cps_with_k e1 @@ fun v1 ->
let v' : string = new_v () and k' : string = new_k () in
Let(k', Abs(v', None, k @@ Var v'),
If(v1,
cps_with_k e2 (fun v -> App(Var k', v)),
cps_with_k e3 (fun v -> App(Var k', v))))
(* List Manipulation *)
| (_, _, TmCons(e1, e2))
-> cps_with_k e1 @@ fun v1 ->
cps_with_k e2 @@ fun v2 ->
k (Cons(v1, v2))
| (_, _, TmLMatch (e1, e2, hd, tl, e3))
-> cps_with_k e1 @@ fun v1 ->
let v' : string = new_v () and k' : string = new_k () in
Let(k', Abs(v', None, k @@ Var v'),
LMatch(v1, cps_with_k e2 (fun v -> App(Var k', v)),
hd, tl, cps_with_k e3 (fun v -> App(Var k', v)) ))
(* Primitive functions *)
| (_, _, TmSucc(e1))
-> cps_with_k e1 @@ fun v -> k @@ Succ v
| (_, _, TmPred(e1))
-> cps_with_k e1 @@ fun v -> k @@ Pred v
| (_, _, TmIsZero(e1))
-> cps_with_k e1 @@ fun v -> k @@ IsZero v
| _ -> raise NoRuleApplies)
let cps (t: term) : term =
let (t': cps_term) =
if is_pure t then cps_pure(t)
else cps_with_k t (fun x -> x)
in cps_term_to_term t'