Commits

Sébastien Ferré committed 6f6bd36

Initial revision

Comments (0)

Files changed (1)

+
+class virtual ['a,'b] 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 virtual to_string : string
+  end
+
+class ['a,'b] var =
+  object (self)
+    inherit ['a,'b] 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)
+*)
+    method to_string = "x" ^ string_of_int (Oo.id self)
+  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) =
+  object (self)
+(*    constraint 'd = 'b -> 'c *)
+    inherit ['a, 'd] 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 to_string = x#to_string ^ "\\" ^ t#to_string
+  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)
+
+class ['a, 'c] app (t : ('a, 'b -> 'c) term) (u : ('a, 'b) term) =
+  object (self)
+    inherit ['a, 'c] 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 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)
+    method to_string = "(" ^ t#to_string ^ " " ^ u#to_string ^ ")"
+  end
+let app t u = new app t u
+
+(*
+let t0 () = abs (fun (x : ('a,unit) term) -> app x x)
+*)
+
+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
+
+(*
+class virtual ['a] term =
+  object
+    method virtual witness : 'a
+  end
+
+class ['a] var =
+  object
+    method witness : 'a = raise Not_found
+  end
+
+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)
+
+class ['a] app (t : ('b -> 'a) term) (u : 'b term) =
+  object
+    inherit ['a] term
+    method witness = t#witness u#witness
+  end
+
+let t = abs (fun (x : unit term) -> new app x x);;
+let t1 = new app t (new var);;
+*)