Detection of divergents

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 340b955049e3cc64230cb81bf258663fcdfe941b..c6cecec5c0c064f972071344d4c6381559a4b120 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -657,9 +657,9 @@ let env_of_sigma freshno sigma should_explode =
     e,Pure.lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[]
    with
     Not_found ->
     e,Pure.lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[]
    with
     Not_found ->

-     if should_explode && n = hd_of_i_var (cast_to_i_var !bomb)
-      then ([], (let f t = Pure.A(t,t) in f (Pure.L (f (Pure.V 0)))), [])
-      else ([],Pure.V n,[]))::e
+    if n = hd_of_i_var (cast_to_i_var !bomb)
+     then ([], Pure.omega should_explode, [])
+     else ([], Pure.V n, []) ) :: e

  in aux 0
 ;;
 (* ************************************************************************** *)
  in aux 0
 ;;
 (* ************************************************************************** *)


@@ -712,22 +712,22 @@ let solve p =
  let ps = List.map scott_of_nf p.ps in
 
  let sigma' = List.map (fun (x,inst) -> x, scott_of_nf inst) sigma in
  let ps = List.map scott_of_nf p.ps in
 
  let sigma' = List.map (fun (x,inst) -> x, scott_of_nf inst) sigma in

- let e' = env_of_sigma freshno sigma' false (* FIXME shoudl_explode *) in
+ let e' = env_of_sigma freshno sigma' false in
+ let e'' = env_of_sigma freshno sigma' true in

 
  prerr_endline "--------<REDUCE>---------";
 
  prerr_endline "--------<REDUCE>---------";

- let pure_bomb = ToScott.t_of_nf (!bomb) in (* Pure.B *)

  (function
    | Some div ->
       print_endline (Pure.print div);
       let t = Pure.mwhd (e',div,[]) in
       prerr_endline ("*:: " ^ (Pure.print t));
  (function
    | Some div ->
       print_endline (Pure.print div);
       let t = Pure.mwhd (e',div,[]) in
       prerr_endline ("*:: " ^ (Pure.print t));

-      assert (t = pure_bomb)
+      assert (Pure.diverged t)

    | None -> ()) div;
  List.iter (fun n ->
   verbose ("_::: " ^ (Pure.print n));
    | None -> ()) div;
  List.iter (fun n ->
   verbose ("_::: " ^ (Pure.print n));

-  let t = Pure.mwhd (e',n,[]) in
+  let t = Pure.mwhd (e'',n,[]) in

   verbose ("_:: " ^ (Pure.print t));
   verbose ("_:: " ^ (Pure.print t));

-  assert (t <> pure_bomb)
+  assert (not (Pure.diverged t))

  ) conv ;
  List.iteri (fun i n ->
   verbose ((string_of_int i) ^ "::: " ^ (Pure.print n));
  ) conv ;
  List.iteri (fun i n ->
   verbose ((string_of_int i) ^ "::: " ^ (Pure.print n));

diff --git a/ocaml/pure.ml b/ocaml/pure.ml
index 95dae1513d166833d6ba2fd69868b86e7c1a2ee7..29288aa4b4ac847b06e463c13c99e642294304a8 100644 (file)
--- a/ocaml/pure.ml
+++ b/ocaml/pure.ml
@@ -101,6 +101,13 @@ let mwhd m =
    | (_,L _,[]) as m -> m
  in
   unwind (aux m)
    | (_,L _,[]) as m -> m
  in
   unwind (aux 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;;

 
 end
 
 
 end
 

diff --git a/ocaml/pure.mli b/ocaml/pure.mli
index a6b90acf7e16c6be71967352756223cbefb70f6d..1b60c09d269ca93716450608bcc7c6d4e4a2ff37 100644 (file)
--- a/ocaml/pure.mli
+++ b/ocaml/pure.mli
@@ -3,8 +3,9 @@ module Pure :
     type t = V of int | A of t * t | L of t | B
     val print : ?l:string list -> t -> string
     val lift : int -> t -> t
     type t = V of int | A of t * t | L of t | B
     val print : ?l:string list -> t -> string
     val lift : int -> t -> t

-    val unwind : ?tbl:('a list * t * 'a list as 'a, t) Hashtbl.t -> 'a -> t

     val mwhd : (('a * t * ('b list as 'c) as 'b) list as 'a) * t * 'c -> t
     val mwhd : (('a * t * ('b list as 'c) as 'b) list as 'a) * t * 'c -> t

+    val omega : bool -> t
+    val diverged : t -> bool

   end
 
 module Scott :
   end
 
 module Scott :