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