X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fpure.ml;h=3bd7ec491a11059bd91c9a90800f58175fb62cf6;hb=6e5e1945c99404f171f90a93c18c336aaeaab546;hp=f1cac843e2349f15c1e5c4cf9c5dd00e3c05e4af;hpb=5cecab147f53f77dcf70a0f1845772d41cff1597;p=fireball-separation.git

diff --git a/ocaml/pure.ml b/ocaml/pure.ml
index f1cac84..3bd7ec4 100644
--- a/ocaml/pure.ml
+++ b/ocaml/pure.ml
@@ -90,10 +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 is_divergent (unwind m) -> [], B, []
      | (e,A(t1,t2),s) ->
          let t2' = aux g (e,t2,[]) in
          let (_,t,_) = t2' in
@@ -131,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 =