Tentative commit: tactics dropped and clean-up

[fireball-separation.git] / ocaml / pure.ml

diff --git a/ocaml/pure.ml b/ocaml/pure.ml
index 78c6c4cbcbdbb5ae05e179eb85fe8b1145f500a7..95dae1513d166833d6ba2fd69868b86e7c1a2ee7 100644 (file)
--- a/ocaml/pure.ml
+++ b/ocaml/pure.ml
@@ -7,6 +7,7 @@ type t =
   | V of int
   | A of t * t
   | L of t
+  | B
 
 let rec print ?(l=[]) =
  function
@@ -15,6 +16,7 @@ let rec print ?(l=[]) =
   | L t ->
      let name = string_of_var (List.length l) in
      "λ" ^ name ^ "." ^ print ~l:(name::l) t
+  | B -> "B"
 
 let lift m =
  let rec aux l =
@@ -22,6 +24,7 @@ let lift m =
    | V n -> V (if n < l then n else n+m)
    | A (t1,t2) -> A (aux l t1, aux l t2)
    | L t -> L (aux (l+1) t)
+   | B -> B
  in
   aux 0
 
@@ -72,7 +75,8 @@ let unwind ?(tbl = Hashtbl.create 317) m =
        (try
          lift l (cache_unwind (List.nth e (n - l)))
         with Failure _ -> V (n - l))
-    | L t -> L (aux (l+1) t) in
+    | L t -> L (aux (l+1) t)
+    | B -> B in
   let t = aux 0 t in
   List.fold_left (fun f a -> A(f,a)) t s
 in
@@ -81,15 +85,19 @@ in
 let mwhd m =
  let rec aux =
   function
-     (e,A(t1,t2),s) ->
+   | (e,A(t1,t2),s) ->
        let t2' = aux (e,t2,[]) in
-       aux (e,t1,t2'::s)
+       let (_,t,_) = t2' in
+       if t = B
+        then t2'
+        else aux (e,t1,t2'::s)
    | (e,L t,x::s) -> aux (x::e,t,s)
    | (e,V n,s) as m ->
       (try
         let e,t,s' = List.nth e n in
         aux (e,t,s'@s)
        with Failure _ -> m)
+   | (e, B, _) -> (e, B, [])
    | (_,L _,[]) as m -> m
  in
   unwind (aux m)