X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=ocaml%2Flambda4.ml;h=311537a151c3409ace586ee7ef0982a2a2ed8ceb;hb=5a57b32e5e068d05c1feb7455861bc8d5e4bd05a;hp=c6cecec5c0c064f972071344d4c6381559a4b120;hpb=417e6bbe7973c9413216a87dff01f920d39e4657;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index c6cecec..311537a 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -3,7 +3,7 @@ open Util.Vars
 open Pure
 open Num
 
-let bomb = ref(`Var(-1,-666));;
+let divergent = ref(`Var(-1, -666));;
 
 (*
  The number of arguments which can applied to numbers
@@ -436,21 +436,8 @@ prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ strin
   | Some div ->
    if List.mem (hd_of_i_var div) inedible
    then p
-   else
-    let n = match div with `I(_,args) -> Listx.length args | `Var _ -> 0 in
-    let p, bomb' = make_fresh_var p (-666) in
-    (if !bomb <> `Var (-1,-666) then
-     failwithProblem p
-      ("Bomb was duplicated! It was " ^ string_of_nf !bomb ^
-       ", tried to change it to " ^ string_of_nf bomb'));
-    bomb := bomb';
-    prerr_endline ("Just created bomb var: " ^ string_of_nf !bomb);
-    let x = hd_of_i_var div in
-    let inst = make_lams !bomb n in
-    let p = {p with div=None} in
-    (* subst_in_problem (hd_of_i_var div) inst p in *)
-     {p with sigma=p.sigma@[x,inst]} in
-     let dangerous_conv = showstoppers_conv in
+   else (divergent := `Var(hd_of_i_var div, -666); {p with div=None}) in
+ let dangerous_conv = showstoppers_conv in
 prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
 List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv;
  let conv =
@@ -486,8 +473,6 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.
   `Continue p
 
 let instantiate p x n =
- (if hd_of_i_var (cast_to_i_var !bomb) = x
-   then failwithProblem p ("BOMB (" ^ string_of_nf !bomb ^ ") cannot be instantiated!"));
  let arity_of_x = max_arity_tms x (all_terms p) in
  (if arity_of_x = None then failwithProblem p "step on var non occurring in problem");
  (if Util.option_get(arity_of_x) = min_int then failwithProblem p "step on fake variable");
@@ -656,10 +641,7 @@ let env_of_sigma freshno sigma should_explode =
    (try
     e,Pure.lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[]
    with
-    Not_found ->
-    if n = hd_of_i_var (cast_to_i_var !bomb)
-     then ([], Pure.omega should_explode, [])
-     else ([], Pure.V n, []) ) :: e
+    Not_found -> ([], Pure.V n, []) ) :: e
  in aux 0
 ;;
 (* ************************************************************************** *)
@@ -692,7 +674,6 @@ let solve p =
  match check p with
  | Some s -> `Unseparable s
  | None ->
- bomb := `Var(-1,-666);
  Console.print_hline();
  let p_finale = auto p p.initialSpecialK in
  let freshno,sigma = p_finale.freshno, p_finale.sigma in
@@ -706,6 +687,7 @@ let solve p =
   (string_of_var p_finale.var_names x ^ " := " ^ string_of_term p_finale inst)) sigma;
 
  prerr_endline "---------<PURE>---------";
+ ToScott.bomb := !divergent;
  let scott_of_nf t = ToScott.t_of_nf (t :> nf) in
  let div = option_map scott_of_nf p.div in
  let conv = List.map scott_of_nf p.conv in