X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fpure.ml;h=be08bb4ae3086086e704824d2636c9d843c38409;hb=refs%2Fheads%2Fstrong_simple_measure;hp=95dae1513d166833d6ba2fd69868b86e7c1a2ee7;hpb=978648853f982a5e5755f084fb22342fdbb3534e;p=fireball-separation.git

diff --git a/ocaml/pure.ml b/ocaml/pure.ml
index 95dae15..be08bb4 100644
--- a/ocaml/pure.ml
+++ b/ocaml/pure.ml
@@ -21,7 +21,7 @@ let rec print ?(l=[]) =
 let lift m =
  let rec aux l =
   function
-   | V n -> V (if n < l then n else n+m)
+   | V n -> V (if n >= l then n+m else n)
    | A (t1,t2) -> A (aux l t1, aux l t2)
    | L t -> L (aux (l+1) t)
    | B -> B
@@ -29,21 +29,22 @@ let lift m =
   aux 0
 
 (* Reference implementation.
-   Reduction machine used below
+   Reduction machine used below *)
 let subst delift_by_one what with_what =
  let rec aux l =
   function
    | A(t1,t2) -> A(aux l t1, aux l t2)
    | V n ->
-       if n = what + l then
+       if (if what < 0 then n = what else n = what + l) then
         lift l with_what
        else
         V (if delift_by_one && n >= l then n-1 else n)
    | L t -> L (aux (l+1) t)
+   | B -> B
  in
   aux 0
 
-let rec whd =
+(* let rec whd =
  function
   | A(t1, t2) ->
      let t2 = whd t2 in
@@ -74,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
@@ -82,25 +83,76 @@ let unwind ?(tbl = Hashtbl.create 317) m =
 in
  unwind m
 
-let mwhd m =
- let rec aux =
-  function
-   | (e,A(t1,t2),s) ->
-       let t2' = aux (e,t2,[]) in
-       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)
+
+(* let rec print_machine (e,t,s) =
+ "[" ^ String.concat "," (List.map print_machine e) ^
+     "|" ^ print t ^ "|" ^
+     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
+         if t = B
+          then t2'
+          else aux g (e,t1,t2'::s)
+     | (e,L t,x::s) -> aux g (x::e,t,s)
+     | (e,V n,s) as m ->
+        (try
+          let e,t,s' = List.nth e n in
+          aux g (e,t,s'@s)
+         with Invalid_argument _ | Failure _ -> m
+         )
+     | (e, B, _) -> (e, B, [])
+     | (e, L t, []) ->
+      let t = subst true 0 (V g) t in
+      (* print_endline ("." ^ string_of_int g ^ " " ^ print_machine ((e,t,[]))); *)
+      let m' = aux (g-1) (e, t, []) in
+      let t' = unwind m' in
+      (* print_endline ("=" ^ print t');
+      print_endline ("==" ^ print (lift 1 t')); *)
+      let t' = subst false g (V 0) (lift 1 t') in
+      (* print_endline ("===" ^ print t'); *)
+      [], (if t' = B then t' else L t'), []
+
+   in
+    unwind (aux ~-2 m)
+;;
+
+let omega should_explode =
+ if should_explode
+  then let f t = A(t,t) in f (L (f (V 0)))
+  else B
+;;
+
+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