X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fpure.ml;h=be08bb4ae3086086e704824d2636c9d843c38409;hb=ad332f3befc4922498db7a9ca6dbb7cc67dbf75b;hp=7963f8732132a75bab5620326e1c193278af16ff;hpb=5a57b32e5e068d05c1feb7455861bc8d5e4bd05a;p=fireball-separation.git

diff --git a/ocaml/pure.ml b/ocaml/pure.ml
index 7963f87..be08bb4 100644
--- a/ocaml/pure.ml
+++ b/ocaml/pure.ml
@@ -75,7 +75,7 @@ let unwind ?(tbl = Hashtbl.create 317) m =
     | V n ->
        (try
          lift l (cache_unwind (List.nth e (n - l)))
-        with Failure _ -> V (n - l))
+        with Failure _ -> V n)
     | L t -> L (aux (l+1) t)
     | B -> B in
   let t = aux 0 t in
@@ -90,11 +90,20 @@ in
      String.concat "," (List.map print_machine s) ^ "]"
 ;; *)
 
+  let omega = let delta = L(A(V 0, V 0)) in A(delta,delta)
+
+  let rec is_divergent =
+   function
+      t when t = omega -> true
+    | A(t,_) -> is_divergent t
+    | L(t) -> is_divergent t
+    | _ -> false
+
   let mwhd m =
    let rec aux g =
     function
     (* mmm -> print_endline (print_machine mmm); match mmm with *)
-        m when unwind m = let d = L(A(V 0, V 0)) in A(d,d) -> [], B, []
+        m when is_divergent (unwind m) -> [], B, []
      | (e,A(t1,t2),s) ->
          let t2' = aux g (e,t2,[]) in
          let (_,t,_) = t2' in
@@ -106,7 +115,7 @@ in
         (try
           let e,t,s' = List.nth e n in
           aux g (e,t,s'@s)
-         with Invalid_argument "List.nth" | Failure _ -> m
+         with Invalid_argument _ | Failure _ -> m
          )
      | (e, B, _) -> (e, B, [])
      | (e, L t, []) ->
@@ -132,6 +141,19 @@ let omega should_explode =
 
 let diverged = (=) B;;
 
+(* Note: maps only variables <= freshno *)
+let env_of_sigma freshno sigma =
+ let rec aux n =
+  if n > freshno then
+   []
+  else
+   let e = aux (n+1) in
+   (try
+    e, lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[]
+   with
+    Not_found -> ([], V n, []) ) :: e
+ in aux 0
+
 end
 
 module Scott =