Source

ocaml-lib / lambda.ml

Diff from to

File lambda.ml

     method subst : (int * 'a term) list -> 'a term = fun env -> (self :> 'a term)
     method reduce : 'a term = (self :> 'a term)
     method virtual to_string : string
-    method virtual map : ('a -> 'a term) -> 'a term
-(*
-    method virtual fold_left : 'b. ('b -> 'a -> 'b) -> 'b -> 'b
-*)
+    method map : ('a -> 'a term) -> 'a term = fun f -> (self :> 'a term)
   end
 
 type ('a, 'b) expr = Expr of 'a term
 
-class ['a] var =
+class ['a] var (id : int) =
   object (self)
     inherit ['a] term
-    method case = `Var (Oo.id self)
+    val id = id
+    method case = `Var id
     method subst env =
-      try List.assoc (Oo.id self) env
+      try List.assoc id env
       with Not_found -> (self :> 'a term)
-    method to_string = "x" ^ string_of_int (Oo.id self)
-    method map f = (self :> 'a term)
+    method to_string = "x" ^ string_of_int id
+    method map f = (f (`Var id) :> 'a term)
 (*    method fold_left f init = f init self#case *)
   end
 
-class ['a] abs (x : 'a var) (t : 'a term) =
+class ['a] abs (x : int) (t : 'a term) =
   object (self)
     inherit ['a] term
     val x = x
     method case = `Abs (x,t)
     method subst env = ({<x = x; t = t#subst env>} :> 'a term)
     method reduce = ({<x = x; t = t#reduce>} :> 'a term)
-    method to_string = x#to_string ^ "\\" ^ t#to_string
+    method to_string = "x" ^ string_of_int x ^ "\\" ^ t#to_string
     method map f = f (`Abs (x, t#map f))
   end
-let abs (f : 'a term -> 'a term) =
-  let x = new var in
-  (new abs x (f (x :> 'a term)) :> 'a term)
+let cpt = ref 0
+let abs =
+  fun (f : 'a term -> 'a term) ->
+    let x = incr cpt; !cpt in
+    (new abs x (f (new var x :> 'a term)) :> 'a term)
 let eabs (f : ('a,'b) expr -> ('a,'c) expr) : ('a,'b -> 'c) expr =
   Expr (abs (fun x -> let Expr y = f (Expr x) in y))
 
     method case = `App (t,u)
     method subst env = ({<t = t#subst env; u = u#subst env>} :> 'a term)
     method reduce =
-      match t#case with
-      | `Abs (x,v) -> (v#subst [(Oo.id x, u)])#reduce
-      | _ -> ({<t = t#reduce; u = u#reduce>} :> 'a term)
+      let t' = t#reduce in
+      match t'#case with
+      | `Abs (x,v) -> (v#subst [(x, u)])#reduce
+      | _ -> ({<t = t'; u = u#reduce>} :> 'a term)
     method to_string = "(" ^ t#to_string ^ " " ^ u#to_string ^ ")"
     method map f = f (`App (t#map f, u#map f))
   end
 (* Optional *)
 type 'a case =
     [ `Var of int
-    | `Abs of 'a * 'a
+    | `Abs of int * 'a
     | `App of 'a * 'a ]
 type closed_term = 'a case term as 'a
 type 'b closed_expr = (closed_term case,'b) expr
 let t0 () : closed_term = abs (fun x -> app x x)
 (* let et0 = eabs (fun x -> eapp x x) *) (* should not typecheck *)
 
+(* another (orthogonal) implementation of reduce *)
+let reduce_case reduce_rec =
+  function
+    | `Var x -> new var x
+    | `Abs (x,v') -> new abs x v'
+    | `App (u',v') ->
+	match u'#case with
+	| `Abs (x,w) -> reduce_rec (w#subst [(x, v')])
+	| _ -> new app u' v'
+let rec reduce t = t#map (reduce_case reduce)
+
 let rec reduce t =
-  t#map
-    (function
-      | `Var _ -> new var
-      | `Abs (x,v) -> new abs x v
-      | `App (u,v) ->
-	  match u#case with
-	  | `Abs (x,w) -> reduce (w#subst [(Oo.id x, v)])
-	  | _ -> new app u v)
+  match t#case with
+  | `Var x -> new var x
+  | `Abs (x,v) -> new abs x (reduce v)
+  | `App (u,v) ->
+      let u' = reduce u in
+      let v' = reduce v in
+      match u'#case with
+      | `Abs (x,w) -> reduce (w#subst [(x,v')])
+      | _ -> new app u' v'
+
+let rec to_string t =
+  match t#case with
+  | `Var x -> "x" ^ string_of_int x
+  | `Abs (x,v) -> "x" ^ string_of_int x ^ "\\" ^ to_string v
+  | `App (u,v) -> "(" ^ to_string u ^ ", " ^ to_string v ^ ")"
+
+class ['a] to_string = (* allows extendable recursion without need for additional names *)
+  object (self)
+    method apply (t : 'a term case) : string =
+      match t with
+      | `Var x -> "x" ^ string_of_int x
+      | `Abs (x,v) -> "x" ^ string_of_int x ^ "\\" ^ self#apply v#case
+      | `App (u,v) -> "(" ^ self#apply u#case ^ ", " ^ self#apply v#case ^ ")"
+  end
 
 (* Tests *)
 
 	      eapp (eapp p2 x) y))))) in
   let t1 = t#reduce in
   print_endline t1#to_string
+
+(* Extension with constants *)
+
+class ['a,'c] const (c : 'c) =
+  object
+    inherit ['a] term
+    val c = c
+    method case = `Const c
+    method to_string = "const"
+  end
+let const c = new const c
+let econst c : ('a,'b) expr = Expr (const c)
+
+type ('a,'c) case2 = [ 'a case | `Const of 'c]
+
+class ['a,'c] to_string2 =
+  object
+    inherit ['a] to_string as to_string
+    method apply t =
+      match t with
+      | #case as t1 -> to_string#apply t1
+      | `Const (c : 'c) -> "const"
+  end
+
+let etest2 () =
+  let Expr t = eapp (eabs (fun (x : ('a,'b) expr) -> x)) (econst 1 : ('a,'b) expr) in
+  print_endline (to_string2#apply t#case);
+  let t1 = t#reduce in
+  print_endline t1#to_string
+