X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=583d99eb89ca9f77777cd6a653f0cda135f61d95;hb=4627d2b89b5a96e09b1921e033a5c1d7dd50dbc6;hp=8f080d57ef4dbc9a8140ee3c16b50d166a73e514;hpb=8392da1be43d50073e2d51bae917dcc570431a78;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 8f080d5..583d99e 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -3,8 +3,6 @@ open Util.Vars
 open Pure
 open Num
 
-let bomb = ref(`Var(-1,-666));;
-
 (*
  The number of arguments which can applied to numbers
  safely, depending on the encoding of numbers.
@@ -26,6 +24,9 @@ type problem =
  ; trail: discriminating_set list list
 };;
 
+(* exceptions *)
+exception Pacman
+exception Bottom
 exception Backtrack of string
 
 let first bound p var f =
@@ -34,10 +35,10 @@ let first bound p var f =
   if i > bound then
    raise (Backtrack ("no more alternatives for " ^ string_of_var var))
   else
-   try
-     f p i
-   with
-    Backtrack s ->
+   try(try
+    f p i
+   with Pacman | Bottom -> raise (Backtrack "Pacman/Bottom"))
+   with Backtrack s ->
 prerr_endline ("!!BACKTRACK!! " ^ s);
      List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ;
 prerr_endline("Now trying var="^string_of_var var^" i="^string_of_int i);
@@ -68,21 +69,21 @@ let string_of_measure = string_of_int;;
 
 let string_of_problem label ({freshno; div; conv; ps; deltas} as p) =
  Console.print_hline ();
- prerr_endline ("\n||||| Displaying problem: " ^ label ^ " |||||");
- let nl = "\n " in
- let deltas = String.concat nl (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in
+ prerr_string ("\n(* DISPLAY PROBLEM (" ^ label ^ ") - ");
+ let nl = "\n" in
+ let deltas = String.concat (nl^"   ") (List.map (fun r -> String.concat " <> " (List.map (fun (i,_) -> string_of_int i) !r)) deltas) in
  let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
-    nl ^ "measure="^string_of_measure(problem_measure p)^" freshno = " ^ string_of_int freshno
- ^nl^"\b> DISCRIMINATING SETS (deltas)"
- ^nl^"(*"^deltas^(if deltas = "" then "" else "*)"^nl)
- ^"\b (* DIVERGENT *)" ^ nl
- ^" "^ (match div with None -> "None" | Some div -> "(Some\""^ print ~l (div :> nf) ^"\" ") ^ nl
- ^"\b (* CONVERGENT *) [" ^ nl
- ^ String.concat "\n   " (List.map (fun t -> "(* _: *) " ^ (if t = `N (-1) then "PAC;" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^
+ "measure="^string_of_measure(problem_measure p) (* ^ " freshno = " ^ string_of_int freshno*)
+ ^ nl ^ "   Discriminating sets (deltas):"
+ ^ nl ^ "   " ^ deltas ^ (if deltas = " " then "" else nl) ^ "*)"
+ ^"(* DIVERGENT  *)" ^ nl
+ ^"     "^ (match div with None -> "None" | Some div -> "(Some\""^ print ~l (div :> nf) ^"\")") ^ nl
+ ^"  (* CONVERGENT *) [" ^ nl ^ "  "
+ ^ String.concat "\n  " (List.map (fun t -> "(* _ *) " ^ (if t = `N (-1) then "" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^
  (if conv = [] then "" else nl)
- ^ "\b] (* NUMERIC *) [" ^ nl
+ ^ "] (* NUMERIC    *) [" ^ nl ^ " "
  ^ String.concat "\n " (List.mapi (fun i t -> " (* "^ string_of_int i ^" *) \"" ^ print ~l (t :> nf) ^ "\";") ps)
- ^ nl
+ ^ nl ^ "] [\"*\"];;" ^ nl
 ;;
 
 
@@ -159,7 +160,7 @@ let subst_in_problem x inst ({freshno; div; conv; ps; sigma} as p) =
  let len_ps = List.length ps in
 (*(let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
 prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
- let rec aux ((freshno,acc_ps,acc_new_ps) as acc) =
+ let rec aux_ps ((freshno,acc_ps,acc_new_ps) as acc) =
   function
   | [] -> acc
   | t::todo_ps ->
@@ -169,31 +170,31 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
      let freshno,new_t,acc_new_ps =
       expand_match (freshno,acc_ps@`Var(max_int/3,-666)::todo_ps,acc_new_ps) t
      in
-      aux (freshno,acc_ps@[new_t],acc_new_ps) todo_ps
+      aux_ps (freshno,acc_ps@[new_t],acc_new_ps) todo_ps
 
   (* cut&paste from aux above *)
-  and aux' ps ((freshno,acc_conv,acc_new_ps) as acc) =
+  and aux_conv ps ((freshno,acc_conv,acc_new_ps) as acc) =
    function
    | [] -> acc
    | t::todo_conv ->
-(*prerr_endline ("EXPAND t:" ^ print (t :> nf));*)
-       let t = subst false false x inst (t :> nf) in
+   (*prerr_endline ("EXPAND t:" ^ print (t :> nf));*)
+      let t = try
+       subst false false x inst (t :> nf)
+      with Pacman -> `N(-1) in (* DUMMY CONVERGENT *)
 (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*)
-       let freshno,new_t,acc_new_ps =
-        expand_match (freshno,ps,acc_new_ps) t
-       in
-        aux' ps (freshno,acc_conv@[new_t],acc_new_ps) todo_conv
+      let freshno,new_t,acc_new_ps = expand_match (freshno,ps,acc_new_ps) t in
+      aux_conv ps (freshno,acc_conv@[new_t],acc_new_ps) todo_conv
 
   (* cut&paste from aux' above *)
-  and aux'' ps (freshno,acc_new_ps) =
+  and aux_div ps (freshno,acc_new_ps) =
    function
    | None -> freshno, None, acc_new_ps
    | Some t ->
-      let t = subst false false x inst (t :> nf) in
-      let freshno,new_t,acc_new_ps =
-       expand_match (freshno,ps,acc_new_ps) t
-      in
-       freshno,Some new_t,acc_new_ps
+      try
+       let t = subst false false x inst (t :> nf) in
+       let freshno,new_t,acc_new_ps = expand_match (freshno,ps,acc_new_ps) t in
+        freshno,Some(cast_to_i_var new_t),acc_new_ps
+      with Bottom -> freshno, None, acc_new_ps
 
   and expand_match ((freshno,acc_ps,acc_new_ps) as acc) t =
    match t with
@@ -224,15 +225,16 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif
 (*prerr_endline ("NUOVO t:" ^ print (fst t :> nf) ^ " more_args=" ^ string_of_int (snd t));*)
           expand_match (freshno,acc_ps,acc_new_ps) t
    | `Lam _ -> assert false (* algorithm invariant/loose typing *)
-   | `Bottom | `Pacman -> raise (Backtrack "BOT or PAC in toplevel numeric positioon")
+   | `Bottom -> raise Bottom
+   | `Pacman -> raise Pacman
    | #i_n_var as x ->
       let x = simple_expand_match (acc_ps@acc_new_ps) x in
       freshno,cast_to_i_num_var x,acc_new_ps in
 
- let freshno,old_ps,new_ps = aux (freshno,[],[]) (ps :> i_num_var list) in
- let freshno,conv,new_ps = aux' old_ps (freshno,[],new_ps) (conv :> i_num_var list) in
- let freshno,div,new_ps = aux'' old_ps (freshno,new_ps) (div :> i_num_var option) in
- let div = option_map cast_to_i_var div in
+ let freshno,old_ps,new_ps = aux_ps (freshno,[],[]) (ps :> i_num_var list) in
+ let freshno,conv,new_ps = aux_conv old_ps (freshno,[],new_ps) (conv :> i_num_var list) in
+ let freshno,div,new_ps = aux_div old_ps (freshno,new_ps) (div :> i_num_var option) in
+
  let ps = List.map cast_to_i_n_var (old_ps @ new_ps) in
  let conv = List.map cast_to_i_n_var conv in
 (let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
@@ -428,20 +430,10 @@ prerr_endline ("# INST_IN_EAT: " ^ string_of_var x ^ " := " ^ print ~l inst));
    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
-    prerr_endline ("# INST (div): " ^ string_of_var x ^ " := " ^ string_of_nf inst);
-    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
+    let inst = make_lams `Bottom n in
+    subst_in_problem x inst p in
+ let dangerous_conv = showstoppers_conv in
 let _ = 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 l))) dangerous_conv; in
  let conv =
@@ -477,8 +469,6 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l))
   `Continue p
 
 let instantiate p x perm 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");
  let arity_of_x = Util.option_get(arity_of_x) in
@@ -668,7 +658,7 @@ let optimize_numerals p =
   replace_in_sigma (List.rev perm) p.sigma
 ;;
 
-let env_of_sigma freshno sigma should_explode =
+let env_of_sigma freshno sigma =
  let rec aux n =
   if n > freshno then
    []
@@ -677,10 +667,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 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
+    Not_found -> ([],Pure.V n,[]))::e
  in aux 0
 ;;
 
@@ -718,14 +705,12 @@ let main problems =
   List.iter
    (fun (p,n,cmds) ->
     Console.print_hline();
-    bomb := `Var (-1,-666);
     let p_finale = aux p n cmds in
     let freshno,sigma = p_finale.freshno, p_finale.sigma in
     prerr_endline ("------- <DONE> ------\n ");
     (* prerr_endline (string_of_problem "Original problem" p); *)
     prerr_endline "---------------------";
     let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
-    prerr_endline (" BOMB == " ^ print ~l !bomb);
     prerr_endline "---------------------";
     List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma;
 (*
@@ -744,14 +729,13 @@ let main problems =
     let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
     List.iter (fun (x,inst) -> prerr_endline (string_of_var x ^ " := " ^ print ~l inst)) sigma;
     prerr_endline "---------<PURE>---------";
+
     let div = option_map (fun div -> ToScott.scott_of_nf (div :> nf)) p.div in
     let conv = List.map (fun t -> ToScott.scott_of_nf (t :> nf)) p.conv in
     let ps = List.map (fun t -> ToScott.scott_of_nf (t :> nf)) p.ps in
-    let sigma = List.map (fun (x,inst) -> x, ToScott.scott_of_nf inst) sigma in
-    (*let ps_ok = List.fold_left (fun ps (x,inst) ->
-      List.map (Pure.subst false x inst) ps) ps sigma in*)
-    let e = env_of_sigma freshno sigma true in
-    let e' = env_of_sigma freshno sigma false in
+
+    let sigma' = List.map (fun (x,inst) -> x, ToScott.scott_of_nf inst) sigma in
+    let e' = env_of_sigma freshno sigma' in
 
 (*
      prerr_endline "---------<PPP>---------";
@@ -769,17 +753,16 @@ in
       print_endline (Pure.print div);
       let t = Pure.mwhd (e',div,[]) in
       prerr_endline ("*:: " ^ (Pure.print t));
-      prerr_endline (print !bomb);
-      assert (t = ToScott.scott_of_nf (!bomb:>nf))
+      assert (t = Pure.B)
      | None -> ()) div;
      List.iter (fun n ->
        prerr_endline ("_::: " ^ (Pure.print n));
-       let t = Pure.mwhd (e,n,[]) in
+       let t = Pure.mwhd (e',n,[]) in
        prerr_endline ("_:: " ^ (Pure.print t))
      ) conv ;
      List.iteri (fun i n ->
        prerr_endline ((string_of_int i) ^ "::: " ^ (Pure.print n));
-       let t = Pure.mwhd (e,n,[]) in
+       let t = Pure.mwhd (e',n,[]) in
        prerr_endline ((string_of_int i) ^ ":: " ^ (Pure.print t));
        assert (t = Scott.mk_n i)
      ) ps ;