-
Notifications
You must be signed in to change notification settings - Fork 4
/
Tail.ml
271 lines (223 loc) · 8.78 KB
/
Tail.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
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
(* This intermediate language describes the result of the CPS transformation.
It is a lambda-calculus where the ordering of computations is explicit and
where every function call is a tail call.
The following syntactic categories are distinguished:
1. "Values" include variables, integer literals, and applications of the
primitive integer operations to values. Instead of "values", they could
also be referred to as "pure expressions". They are expressions whose
evaluation terminates and has no side effect, not even memory
allocation.
2. "Blocks" include lambda-abstractions. Even though lambda-abstractions
are traditionally considered values, here, they are viewed as
expressions whose evaluation has a side effect, namely, the allocation
of a memory block.
3. "Terms" are expressions with side effects. Terms always appear in tail
position: an examination of the syntax of terms shows that a term can be
viewed as a sequence of [LetVal], [LetBlo] and [Print] instructions,
terminated with either [Exit] or [TailCall]. This implies, in
particular, that every call is a tail call.
In contrast with the surface language, where every lambda-abstraction has
arity 1, in this calculus, lambda-abstractions of arbitrary arity are
supported. A lambda-abstraction [Lam] carries a list of formal arguments
and a function call [TailCall] carries a list of actual arguments. Partial
applications or over-applications are not supported: it is the programmer's
responsibility to ensure that every function call provides exactly as many
arguments as expected by the called function. *)
type variable =
Atom.atom
and self = Lambda.self =
| Self of variable
| NoSelf
and binop = Lambda.binop =
| OpAdd
| OpSub
| OpMul
| OpDiv
and value =
| VVar of variable
| VLit of int
| VBinOp of value * binop * value
and tag =
int
and block =
| Lam of self * variable list * term
| Tuple of value list
| Constructor of tag * value list
(* Terms include the following constructs:
- The primitive operation [Exit] stops the program.
- The tail call [TailCall (v, vs)] transfers control to the function [v]
with actual arguments [vs]. (The value [v] should be a function, and its
arity should be the length of [vs].)
- The continuation call [ContCall (v, ks, vs)] transfers control to the
function [v], with actual arguments [vs], and continuations to apply [ks].
(The value [v] should be a function, and [ks] a list of functions
having arity 2 or 3.)
- The term [Print (v, t)] prints the value [v], then executes the term [t].
(The value [v] should be a primitive integer value.)
- The term [LetVal (x, v, t)] binds the variable [x] to the value [v], then
executes the term [t].
- The term [LetBlo (x, b, t)] allocates the memory block [b] and binds the
variable [x] to its address, then executes the term [t].
The semantics of [ContCall (f, ks, [x1; ...; xn])] are defined as follows:
- [ContCall (f, ks, [x1; ...; xn]) -> TailCall (f, [x1; ...; xn; ks])] if
f has arity n + 1.
- [ContCall (f, k :: ks, [x1; ...; xn]) ->
TailCall (k, [(fun x_{n+1} ... xm ks2 -> ContCall (f, ks2, [x1; ...; xm])); ks])]
if f has arity m + 1 > n + 1.
- [ContCall (f, k :: ks, [x1; ...; xn]) ->
TailCall (f, [x1; ...; xm; (fun g ks2 -> ContCall (g, k :: ks2, [x_{m+1}; ...; xn])) :: ks])]
if f has arity m + 1 < n + 1.
*)
and term =
| Exit
| TailCall of value * value list
| ContCall of value * value * value list
| Print of value * term
| LetVal of variable * value * term
| LetBlo of variable * block * term
| IfZero of value * term * term
| DestructTuple of value * variable list * term
| Switch of value * (tag * variable list * term) list * term option
[@@deriving show { with_path = false }]
(* -------------------------------------------------------------------------- *)
(* Constructor functions. *)
let vvar x =
VVar x
let vvars xs =
List.map vvar xs
(* -------------------------------------------------------------------------- *)
(* Computing the free variables of a value, block, or term. *)
open Atom.Set
let rec fv_value (v : value) =
match v with
| VVar x ->
singleton x
| VLit _ ->
empty
| VBinOp (v1, _, v2) ->
union (fv_value v1) (fv_value v2)
and fv_values (vs : value list) =
union_many fv_value vs
and fv_lambda (xs : variable list) (t : term) =
diff (fv_term t) (of_list xs)
and fv_block (b : block) =
match b with
| Lam (NoSelf, xs, t) ->
fv_lambda xs t
| Lam (Self f, xs, t) ->
remove f (fv_lambda xs t)
| Tuple l | Constructor (_, l) -> fv_values l
and fv_term (t : term) =
match t with
| Exit ->
empty
| TailCall (v, vs) ->
fv_values (v :: vs)
| ContCall (v, ks, vs) ->
fv_values (v :: ks :: vs)
| Print (v1, t2) ->
union (fv_value v1) (fv_term t2)
| LetVal (x, v1, t2) ->
union
(fv_value v1)
(remove x (fv_term t2))
| LetBlo (x, b1, t2) ->
union
(fv_block b1)
(remove x (fv_term t2))
| IfZero (v1, t2, t3) ->
union (fv_value v1) (union (fv_term t2) (fv_term t3))
| DestructTuple (v, xs, t) ->
union (fv_value v) (diff (fv_term t) (of_list xs))
| Switch (v, l, r) ->
let fv = fv_value v in
let fv = match r with Some r -> union fv (fv_term r) | None -> fv in
union fv
(union_many (fun (_, xs, t) -> diff (fv_term t) (of_list xs)) l)
let rec rename_value (r : Atom.atom Atom.Map.t) (v : value) =
match v with
| VVar x ->
VVar (try Atom.Map.find x r
with Not_found -> x)
| VLit _ -> v
| VBinOp (v1, op, v2) -> VBinOp (rename_value r v1, op, rename_value r v2)
and rename_values (r : Atom.atom Atom.Map.t) (vs : value list) =
List.map (rename_value r) vs
and rename_lambda (r : Atom.atom Atom.Map.t) (xs : variable list) (t : term) =
assert (not (List.exists (fun v -> Atom.Map.mem v r) xs));
rename_term r t
and rename_block (r : Atom.atom Atom.Map.t) (b : block) =
match b with
| Lam (NoSelf, xs, t) ->
Lam (NoSelf, xs, rename_lambda r xs t)
| Lam (Self f, xs, t) ->
Lam (Self f, xs, rename_lambda r (f :: xs) t)
| Tuple l -> Tuple (rename_values r l)
| Constructor (tag, l) -> Constructor (tag, rename_values r l)
and rename_term (r : Atom.atom Atom.Map.t) (t : term) =
match t with
| Exit -> Exit
| TailCall (v, vs) ->
TailCall (rename_value r v, rename_values r vs)
| ContCall (v, ks, vs) ->
ContCall (rename_value r v, rename_value r ks, rename_values r vs)
| Print (v1, t2) ->
Print (rename_value r v1, rename_term r t2)
| LetVal (x, v1, t2) ->
assert (not (Atom.Map.mem x r));
LetVal (x, rename_value r v1, rename_term r t2)
| LetBlo (x, b1, t2) ->
assert (not (Atom.Map.mem x r));
LetBlo (x, rename_block r b1, rename_term r t2)
| IfZero (v1, t2, t3) ->
IfZero (rename_value r v1, rename_term r t2, rename_term r t3)
| DestructTuple (v, xs, t) ->
assert (not (List.exists (fun x -> Atom.Map.mem x r) xs));
DestructTuple (rename_value r v, xs, rename_term r t)
| Switch (v, l, t) ->
let t = match t with None -> None | Some t -> Some (rename_term r t) in
let v = rename_value r v in
let l = List.map (fun (tag, xs, t) ->
assert (not (List.exists (fun x -> Atom.Map.mem x r) xs));
(tag, xs, rename_term r t)
) l in
Switch (v, l, t)
(* [let x_1 = v_1 in ... let x_n = v_n in t] *)
let rec sequential_let (xs : variable list) (vs : value list) (t : term) =
match xs, vs with
| [], [] ->
t
| x :: xs, VVar v :: vs ->
rename_term (Atom.Map.singleton x v) (sequential_let xs vs t)
| x :: xs, v :: vs ->
LetVal (x, v, sequential_let xs vs t)
| _ ->
assert false
(* [let x_1 = v_1 and ... x_n = v_n in t] *)
let parallel_let (xs : variable list) (vs : value list) (t : term) =
assert (List.length xs = List.length vs);
assert (Atom.Set.disjoint (Atom.Set.of_list xs) (fv_values vs));
sequential_let xs vs t
let rec simpl (t : term) : term =
match t with
| Exit | TailCall _ | ContCall _ | Print _ -> t
| LetVal (x, VVar v, t) ->
rename_term (Atom.Map.singleton x v) (simpl t)
| LetVal (x, v, t) -> LetVal (x, v, simpl t)
| LetBlo (f, Lam (self, args, body), t) ->
let t = simpl t in
let body = simpl body in
begin match t with
| TailCall (VVar f1, vals) when Atom.equal f f1 && self = NoSelf ->
parallel_let args vals body
| _ -> LetBlo (f, Lam (self, args, body), t)
end
| LetBlo (x, b, t) ->
LetBlo (x, b, simpl t)
| IfZero (v, t1, t2) -> IfZero (v, simpl t1, simpl t2)
| DestructTuple (v, xs, t) -> DestructTuple (v, xs, simpl t)
| Switch (v, l, t) ->
let t = match t with None -> None | Some t -> Some (simpl t) in
let l = List.map (fun (tag, xs, t) -> (tag, xs, simpl t)) l in
Switch (v, l, t)
let optimize = simpl