/
abt.ml
359 lines (274 loc) · 10.1 KB
/
abt.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
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
module Var : sig
(** Variables, named by strings, which can be bound to a {!module:Binding} or
left free. *)
type t
(** A varibale of type [t] is either free or bound. *)
module Binding : sig
(** A binding is an immutable reference to which a variable can be bound. *)
include Map.OrderedType
val equal : t -> t -> bool
val v : string -> t
(** [binding s] is a new binding for variables named [s] *)
val name : t -> string
end
val compare : t -> t -> int
(** Bound variables are equal if they are have the same binding, free
variables are greater than bound variables, and variables are otherwise
compared lexigraphically by name.
Specifically,
[compare a b] is [0] iff
- [is_free a && is_free b] and [name a = name b]
- [is_bound a && is_bound b] and both [a] and [b] are bound to the same
{!type:binding} by way of {!val:bind}.
[compare a b] is [String.compare (name a) (name b)] if
[is_free a && is_free b] or [is_bound a && is_bound b].
[compare a b] is -1 if [is_bound a] and [is_free b] or 1 if [is_free a]
and [is_bound b] *)
val equal : t -> t -> bool
(** [equal a b] is [true] iff
- [is_free a && is_free b] and [name a = name b]
- [is_bound a && is_bound b] and both [a] and [b] are bound to the same
{!type:binding} by way of {!val:bind}. *)
val is_free : t -> bool
val is_bound : t -> bool
val v : string -> t
val to_string : t -> string
val name : t -> string
(** [name v] is [to_string v] *)
val bind : t -> Binding.t -> t option
(** [bind v bnd] is [Some var] when [is_free v] and [name v = Binding.name bnd],
where [var] is a new variable with the same name but bound to [bnd].
Otherwise, it is [None].
See {!val:equal}. *)
val is_bound_to : t -> Binding.t -> bool
(** [is_bound_to v bnd] is [true] if [v] is bound to [bnd], via {!val:bind} *)
val of_binding : Binding.t -> t
(** [of_binding bnd] is a variable bound to [bnd] *)
val to_binding : t -> Binding.t option
(** [to_binding v] is [Some bnd] iff [v] is bound to [bnd] via {!val:bind}.
Otherwise it is [None]. *)
end = struct
module Binding = struct
type t = string ref
let v s = ref s
let name bnd = !bnd
let compare a b =
if a == b then
0
else
String.compare !a !b
let equal a b = Int.equal (compare a b) 0
end
type t =
| Free of string
| Bound of Binding.t
let compare a b =
match (a, b) with
| Bound a, Bound b -> Binding.compare a b
| Free a, Free b -> String.compare a b
| Free _, Bound _ -> 1 (* Free vars are greater than bound vars *)
| Bound _, Free _ -> -1
let equal a b = Int.equal (compare a b) 0
let is_free = function
| Free _ -> true
| _ -> false
let is_bound t = not (is_free t)
let name = function
| Free s -> s
| Bound b -> !b
let to_string = name
let v s = Free s
let bind v b =
match v with
| Bound _ -> None
| Free name ->
if name = !b then
Some (Bound b)
else
None
let of_binding b = Bound b
let to_binding = function
| Bound b -> Some b
| Free _ -> None
let is_bound_to v bnd =
match v with
| Free _ -> false
| Bound b -> b == bnd
end
module type Operator = sig
(** An operator *)
type 'a t
val map : ('a -> 'b) -> 'a t -> 'b t
val to_string : string t -> string
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
end
module Make (O : Operator) : sig
(** [Make (O)] is a module for constructing and manipulating ABTs for the
operators defined in [O]. *)
type t
(** The type of ABT's constructed from the operators defind in {module:!O} *)
val v : string -> t
(** [v x] is a leaf in the ABT consisting of a variable named [x] *)
val op : t O.t -> t
(** [op o] is a branch in the ABT consisting of the operator [o] *)
val ( #. ) : string -> t -> t
(** [x #. t] is a new abt obtained by binding all {i free} variables named
[x] in [t]
Note that this does {b not} bind the variables to a {i value}, (for which,
see {!subst}). This only binds the free variables within the scope of an
abstraction that ranges over the given (sub) abt [t]. *)
val subst : string -> value:t -> t -> t
(** [subst name ~value t] is a new abt obtained by substituting [value] for
the outermost scope of variables bound to [name] in [t] *)
val to_string : t -> string
(** [to_string t] is the representation of [t] as a string *)
val equal : t -> t -> bool
(** [equal t t'] is [true] when [t] and [t'] are alpha equivalent and [false] otherwise *)
end = struct
type 'a abt =
| Var of Var.t
| Bnd of Var.Binding.t * 'a
| Opr of 'a O.t
type t = T of t abt
(* Get the ABT inside of t *)
let un_t : t -> t abt = fun (T abt) -> abt
(* Put the ABT inside of t *)
let in_t : t abt -> t = fun abt -> T abt
(* Apply f to the ABT inside of t *)
let app_t : (t abt -> t abt) -> t -> t = fun f t -> un_t t |> f |> in_t
(* Alpha-equivalence is derived by checking that the structure of the
two abts is the same.
- For operators, this just amounts to checking the equality supplied by the
given {!modtype:Operator}, [O].
- For variable, we check that the pointer {i structure} is equivalent, and
do take no account of names, since alpha equivalence is fundamentally
concerned with the (anonymous) binding structure of ABTs. *)
let equal : t -> t -> bool =
let module Bindmap = Map.Make (Var.Binding) in
let vars_equal bimap x x' =
match Var.(to_binding x, to_binding x') with
| Some _, None -> false
| None, Some _ -> false
| None, None -> Var.equal x x'
| Some b, Some b' ->
(* Two bound variables are equal when their bindings correspond *)
match Bindmap.find_opt b bimap with
| Some b'' -> Var.Binding.equal b' b''
| None -> false
in
let rec equal : Var.Binding.t Bindmap.t -> t -> t -> bool =
fun bimap t t' ->
match (un_t t, un_t t') with
| Opr o, Opr o' -> O.equal (equal bimap) o o'
| Bnd (b, t), Bnd (b', t') ->
(* Associate corresponding bindings in a bimap *)
equal (Bindmap.add b b' bimap) t t'
| Var x, Var x' -> vars_equal bimap x x'
| _ -> false
in
fun a b -> equal Bindmap.empty a b
let rec to_string t =
un_t t |> function
| Var v -> Var.to_string v
| Bnd (b, abt) -> Var.(name @@ of_binding b) ^ "." ^ to_string abt
| Opr op -> O.map to_string op |> O.to_string
let rec bind : Var.Binding.t -> t -> t =
fun bnd ->
app_t @@ function
| Opr op -> Opr (O.map (bind bnd) op)
| Bnd (b, t) -> Bnd (b, bind bnd t)
| Var v ->
match Var.bind v bnd with
| None -> Var v
| Some v' -> Var v'
let ( #. ) : string -> t -> t =
fun name abt ->
let binding : Var.Binding.t = Var.Binding.v name in
let scope = bind binding abt in
T (Bnd (binding, scope))
let rec subst_val : Var.Binding.t -> value:t -> t -> t =
fun bnd ~value ->
app_t @@ function
| Opr op -> Opr (O.map (subst_val bnd ~value) op)
| Bnd (b, t) ->
(* As an optimization, we don't go any deeper if the variable is shadowed.
* We could, safely, but there's no point. *)
if String.equal (Var.Binding.name b) (Var.Binding.name bnd) then
Bnd (b, t)
else
Bnd (b, subst_val bnd ~value t)
| Var v ->
if Var.is_bound_to v bnd then
un_t value
else
Var v
let rec subst : string -> value:t -> t -> t =
fun name ~value ->
app_t @@ function
| Var v -> Var v
| Opr op -> Opr (O.map (subst name ~value) op)
| Bnd (b, t) ->
if Var.Binding.name b = name then
un_t (subst_val b ~value t)
else
Bnd (b, subst name ~value t)
let op a = T (Opr a)
let v : string -> t = fun s -> T (Var (Var.v s))
end
let%expect_test "Example usage" =
let module Ex = struct
module Operator = struct
type 'a t =
| Num of int
| Plus of 'a * 'a
let equal eq a b =
match (a, b) with
| Num n, Num n' -> Int.equal n n'
| Plus (a, b), Plus (a', b') -> eq a a' && eq b b'
| _ -> false
let map f t =
match t with
| Num n -> Num n
| Plus (a, b) -> Plus (f a, f b)
let to_string : string t -> string = function
| Num n -> Int.to_string n
| Plus (a, b) -> Printf.sprintf "(%s + %s)" a b
end
include Make (Operator)
let num n = op (Num n)
let plus a b = op (Plus (a, b))
let show t = to_string t |> print_endline
end in
let one : Ex.t = Ex.(num 1) in
Ex.show one;
[%expect {| 1 |}];
let two : Ex.t = Ex.(num 2) in
Ex.show two;
[%expect {| 2 |}];
let one_plus_x = Ex.(plus one (v "x")) in
Ex.show one_plus_x;
[%expect {| (1 + x) |}];
let one_plus_y = Ex.(plus one (v "y")) in
Ex.show one_plus_y;
[%expect {| (1 + y) |}];
(* Free variables are not alpha equivalent *)
assert (Ex.(not @@ equal one_plus_x one_plus_y));
let shadow_x_in_bound_x = Ex.("x" #. (plus "x"#.one_plus_x (v "x"))) in
Ex.show shadow_x_in_bound_x;
[%expect {| x.(x.(1 + x) + x) |}];
let bind_x_in_bound_y = Ex.("y" #. (plus "x"#.one_plus_x (v "y"))) in
Ex.show bind_x_in_bound_y;
[%expect {| y.(x.(1 + x) + y) |}];
(* Bound variables allow alpha equivalence *)
assert (Ex.(equal shadow_x_in_bound_x bind_x_in_bound_y));
(* Substitution respects shadowed scope *)
let subst1 = Ex.(shadow_x_in_bound_x |> subst "x" ~value:(num 3)) in
Ex.show subst1;
[%expect {| (x.(1 + x) + 3) |}];
(* Subsequent substitution works as expected *)
Ex.(subst1 |> subst "x" ~value:(num 4) |> show);
[%expect {| ((1 + 4) + 3) |}];
(* Substitution does not mutate abts, so we can give alternate assignments to
previously defined trees. *)
Ex.(subst1 |> subst "x" ~value:(num 99) |> show);
[%expect {| ((1 + 99) + 3) |}]