Source

ocaml-lib / lambda.ml

Diff from to

lambda.ml

+(* objectives:
+   - lambda terms as data structures, rather than code
+   - introspection of abstractions
+   - safety w.r.t. variable names (avoiding variable renaming)
+   - internal beta-reduction + customization
+   - typed lambda-terms, verified by Caml
+*)
 
-class virtual ['a,'b] term =
+class virtual ['a] term =
   object (self)
     method virtual case : 'a
-    method virtual witness : 'b
-(*    method subst : (int * ('a,'b) term) list -> ('a,'b) term = fun env -> (self :> ('a,'b) term) *)
-    method subst : ('a,'b) term = (self :> ('a,'b) term)
-    method reduce : ('a,'b) term = (self :> ('a,'b) term)
+    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
+*)
   end
 
-class ['a,'b] var =
+type ('a, 'b) expr = Expr of 'a term
+
+class ['a] var =
   object (self)
-    inherit ['a,'b] term
+    inherit ['a] term
     method case = `Var (Oo.id self)
-    method witness = failwith "witness"
-    val mutable def : ('a,'b) term option = None
-    method set_def t = def <- Some t
-    method reset_def = def <- None
-    method subst = match def with None -> (self :> ('a,'b) term) | Some s -> s
-(*
     method subst env =
       try List.assoc (Oo.id self) env
-      with Not_found -> (self :> ('a,'b) term)
-*)
+      with Not_found -> (self :> 'a term)
     method to_string = "x" ^ string_of_int (Oo.id self)
+    method map f = (self :> 'a term)
+(*    method fold_left f init = f init self#case *)
   end
-let var () = new var
 
-let for_assoc x u f = x#set_def u; let res = f () in x#reset_def; res
-
-class ['a, 'd] abs (x : ('a,'b) var) (t : ('a,'c) term) =
+class ['a] abs (x : 'a var) (t : 'a term) =
   object (self)
-(*    constraint 'd = 'b -> 'c *)
-    inherit ['a, 'd] term
+    inherit ['a] term
     val x = x
     val t = t
     method case = `Abs (x,t)
-    method witness = fun (x : 'b) -> t#witness
-    method subst = ({<x = x; t = t#subst>} :> ('a,'d) term)
-(*    method subst env = ({<x = x; t = t#subst env>} :> ('a, 'd) term) *)
-    method reduce = ({<x = x; t = t#reduce>} :> ('a, 'd) term)
+    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 map f = f (`Abs (x, t#map f))
   end
-let abs (f : ('a, 'b) term -> ('a, 'c) term) =
-  let x = (new var : ('a,'b) var) in
-  (new abs x (f (x :> ('a,'b) term)) : ('a, 'b -> 'c) term)
+let abs (f : 'a term -> 'a term) =
+  let x = new var in
+  (new abs x (f (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))
 
-class ['a, 'c] app (t : ('a, 'b -> 'c) term) (u : ('a, 'b) term) =
+class ['a] app (t : 'a term) (u : 'a term) =
   object (self)
-    inherit ['a, 'c] term
+    inherit ['a] term
     val t = t
     val u = u
     method case = `App (t,u)
-    method witness = t#witness u#witness
-    method subst = ({<t = t#subst; u = u#subst>} :> ('a,'c) term)
-(*    method subst env = ({<t = t#subst env; u = u#subst env>} :> ('a,'c) term) *)
+    method subst env = ({<t = t#subst env; u = u#subst env>} :> 'a term)
     method reduce =
       match t#case with
-      | `Abs (x,v) -> for_assoc x u (fun () -> v#subst#reduce)
-      | _ -> ({<t = t#reduce; u = u#reduce>} :> ('a,'c) term)
+      | `Abs (x,v) -> (v#subst [(Oo.id x, u)])#reduce
+      | _ -> ({<t = t#reduce; 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
-let app t u = new app t u
+let app t u = (new app t u :> 'a term)
+let eapp (Expr t : ('a,'b -> 'c) expr) (Expr u : ('a,'b) expr) : ('a,'c) expr =
+  Expr (app t u)
 
-(*
-let t0 () = abs (fun (x : ('a,unit) term) -> app x x)
-*)
+(* Optional *)
+type 'a case =
+    [ `Var of int
+    | `Abs of 'a * 'a
+    | `App of 'a * 'a ]
+type closed_term = 'a case term as 'a
+type 'b closed_expr = (closed_term case,'b) expr
 
-let test () =
-  let t = abs (fun (p2 : ('a, int -> int -> bool) term) -> abs (fun (np : ('a, (int -> bool) -> bool) term)  -> abs (fun (x : ('a, int) term) -> app np (abs (fun (y : ('a, int) term) -> app (app p2 x) y))))) in
-  let t1 = t#reduce in
-  print_endline t1#to_string
+let t0 () : closed_term = abs (fun x -> app x x)
+(* let et0 = eabs (fun x -> eapp x x) *) (* should not typecheck *)
 
-(*
-class virtual ['a] term =
-  object
-    method virtual witness : 'a
-  end
-
-class ['a] var =
-  object
-    method witness : 'a = raise Not_found
-  end
+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)
 
-class ['a] abs (x : 'b var) (t : 'c term) =
-  object
-    constraint 'a = 'b -> 'c
-    inherit ['a] term
-    method witness = fun (x : 'b) -> t#witness
-  end
-let abs (f : 'a var -> 'b term) = let x = new var in (new abs x (f x) : ('a -> 'b) abs)
+(* Tests *)
 
-class ['a] app (t : ('b -> 'a) term) (u : 'b term) =
-  object
-    inherit ['a] term
-    method witness = t#witness u#witness
-  end
+let test () =
+  let t = abs (fun p2 -> abs (fun np -> abs (fun x -> app np (abs (fun y -> app (app p2 x) y))))) in
+  let t1 = t#reduce in
+  print_endline t1#to_string
 
-let t = abs (fun (x : unit term) -> new app x x);;
-let t1 = new app t (new var);;
-*)
+let etest () =
+  let Expr t =
+    eabs (fun (p2 : ('a,'e -> 'e -> 's) expr) ->
+      eabs (fun (np : ('a,('e -> 's) -> 's) expr) ->
+	eabs (fun x ->
+	  eapp np 
+	    (eabs (fun y ->
+	      eapp (eapp p2 x) y))))) in
+  let t1 = t#reduce in
+  print_endline t1#to_string