1(* Full fledge version, using objects to structure code *)
2
3open StdLabels
4open MoreLabels
5
6(* Use maps for substitutions and sets for free variables *)
7
8module Subst = Map.Make(struct type t = string let compare = compare end)
9module Names = Set.Make(struct type t = string let compare = compare end)
10
11(* To build recursive objects *)
12
13let lazy_fix make =
14  let rec obj () = make (lazy (obj ()) : _ Lazy.t) in
15  obj ()
16
17let (!!) = Lazy.force
18
19(* The basic operations *)
20
21class type ['a, 'b] ops =
22  object
23    method free : 'b -> Names.t
24    method subst : sub:'a Subst.t -> 'b -> 'a
25    method eval : 'b -> 'a
26  end
27
28(* Variables are common to lambda and expr *)
29
30type var = [`Var of string]
31
32let var = object (self : ([>var], var) #ops)
33  method subst ~sub (`Var s as x) =
34    try Subst.find s sub with Not_found -> x
35  method free (`Var s) =
36    Names.singleton s
37  method eval (#var as v) = v
38end
39
40(* The lambda language: free variables, substitutions, and evaluation *)
41
42type 'a lambda = [`Var of string | `Abs of string * 'a | `App of 'a * 'a]
43
44let next_id =
45  let current = ref 3 in
46  fun () -> incr current; !current
47
48let lambda_ops (ops : ('a,'a) #ops Lazy.t) =
49  let free = lazy !!ops#free
50  and subst = lazy !!ops#subst
51  and eval = lazy !!ops#eval in
52  object (self : ([> 'a lambda], 'a lambda) #ops)
53    method free = function
54        #var as x -> var#free x
55      | `Abs (s, t) -> Names.remove s (!!free t)
56      | `App (t1, t2) -> Names.union (!!free t1) (!!free t2)
57
58    method private map ~f = function
59        #var as x -> x
60      | `Abs (s, t) as l ->
61          let t' = f t in
62          if t == t' then l else `Abs(s, t')
63      | `App (t1, t2) as l ->
64          let t'1 = f t1 and t'2 = f t2 in
65          if t'1 == t1 && t'2 == t2 then l else `App (t'1, t'2)
66
67    method subst ~sub = function
68        #var as x -> var#subst ~sub x
69      | `Abs(s, t) as l ->
70          let used = !!free t in
71          let used_expr =
72            Subst.fold sub ~init:[]
73              ~f:(fun ~key ~data acc ->
74                if Names.mem s used then data::acc else acc) in
75          if List.exists used_expr ~f:(fun t -> Names.mem s (!!free t)) then
76            let name = s ^ string_of_int (next_id ()) in
77            `Abs(name,
78                 !!subst ~sub:(Subst.add ~key:s ~data:(`Var name) sub) t)
79          else
80            self#map ~f:(!!subst ~sub:(Subst.remove s sub)) l
81      | `App _ as l ->
82          self#map ~f:(!!subst ~sub) l
83
84    method eval l =
85      match self#map ~f:!!eval l with
86        `App(`Abs(s,t1), t2) ->
87          !!eval (!!subst ~sub:(Subst.add ~key:s ~data:t2 Subst.empty) t1)
88      | t -> t
89end
90
91(* Operations specialized to lambda *)
92
93let lambda = lazy_fix lambda_ops
94
95(* The expr language of arithmetic expressions *)
96
97type 'a expr =
98    [ `Var of string | `Num of int | `Add of 'a * 'a
99    | `Neg of 'a | `Mult of 'a * 'a]
100
101let expr_ops (ops : ('a,'a) #ops Lazy.t) =
102  let free = lazy !!ops#free
103  and subst = lazy !!ops#subst
104  and eval = lazy !!ops#eval in
105  object (self : ([> 'a expr], 'a expr) #ops)
106    method free = function
107        #var as x -> var#free x
108      | `Num _ -> Names.empty
109      | `Add(x, y) -> Names.union (!!free x) (!!free y)
110      | `Neg x -> !!free x
111      | `Mult(x, y) -> Names.union (!!free x) (!!free y)
112
113    method private map ~f = function
114        #var as x -> x
115      | `Num _ as x -> x
116      | `Add(x, y) as e ->
117          let x' = f x and y' = f y in
118          if x == x' && y == y' then e
119          else `Add(x', y')
120      | `Neg x as e ->
121          let x' = f x in
122          if x == x' then e else `Neg x'
123      | `Mult(x, y) as e ->
124          let x' = f x and y' = f y in
125          if x == x' && y == y' then e
126          else `Mult(x', y')
127
128    method subst ~sub = function
129        #var as x -> var#subst ~sub x
130      | #expr as e -> self#map ~f:(!!subst ~sub) e
131
132    method eval (#expr as e) =
133      match self#map ~f:!!eval e with
134        `Add(`Num m, `Num n) -> `Num (m+n)
135      | `Neg(`Num n) -> `Num (-n)
136      | `Mult(`Num m, `Num n) -> `Num (m*n)
137      | e -> e
138  end
139
140(* Specialized versions *)
141
142let expr = lazy_fix expr_ops
143
144(* The lexpr language, reunion of lambda and expr *)
145
146type 'a lexpr = [ 'a lambda | 'a expr ]
147
148let lexpr_ops (ops : ('a,'a) #ops Lazy.t) =
149  let lambda = lambda_ops ops in
150  let expr = expr_ops ops in
151  object (self : ([> 'a lexpr], 'a lexpr) #ops)
152    method free = function
153        #lambda as x -> lambda#free x
154      | #expr as x -> expr#free x
155
156    method subst ~sub = function
157        #lambda as x -> lambda#subst ~sub x
158      | #expr as x -> expr#subst ~sub x
159
160    method eval = function
161        #lambda as x -> lambda#eval x
162      | #expr as x -> expr#eval x
163end
164
165let lexpr = lazy_fix lexpr_ops
166
167let rec print = function
168  | `Var id -> print_string id
169  | `Abs (id, l) -> print_string ("\ " ^ id ^ " . "); print l
170  | `App (l1, l2) -> print l1; print_string " "; print l2
171  | `Num x -> print_int x
172  | `Add (e1, e2) -> print e1; print_string " + "; print e2
173  | `Neg e -> print_string "-"; print e
174  | `Mult (e1, e2) -> print e1; print_string " * "; print e2
175
176let () =
177  let e1 = lambda#eval (`App(`Abs("x",`Var"x"), `Var"y")) in
178  let e2 = expr#eval (`Add(`Mult(`Num 3,`Neg(`Num 2)), `Var"x")) in
179  let e3 =
180    lexpr#eval (`Add(`App(`Abs("x",`Mult(`Var"x",`Var"x")),`Num 2), `Num 5))
181  in
182  print e1; print_newline ();
183  print e2; print_newline ();
184  print e3; print_newline ()
185