X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=f26607bbf730f31a6b364e628880869f240182e9;hb=0c2f070e30e80810236099f3a9dcfb6edca0f783;hp=2f6a0a0fed506d5c82b4974aa87176268f91a298;hpb=b277f630cb63b40ae983282ea81ffefe288d3e8f;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 2f6a0a0..f26607b 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -6,6 +6,7 @@ open Num
 (* exceptions *)
 exception Pacman
 exception Bottom
+exception Lambda
 exception Backtrack of string
 
 (*
@@ -208,7 +209,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
       let freshno,new_t,acc_new_ps =
        try
         expand_match (freshno,ps,acc_new_ps) t
-       with Pacman -> freshno,convergent_dummy,acc_new_ps
+       with Pacman | Lambda -> freshno,convergent_dummy,acc_new_ps
           | Bottom -> raise (Backtrack "Bottom in conv") in
       aux_conv ps (freshno,acc_conv@[new_t],acc_new_ps) todo_conv
 
@@ -257,7 +258,7 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif
          let t = mk_match (`N i) orig bs_lift bs (args :> nf list) in
 (*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 *)
+   | `Lam _ -> raise Lambda (* assert false (* algorithm invariant/loose typing *) *)
    | `Bottom -> raise Bottom
    | `Pacman -> raise Pacman
    | #i_n_var as x ->
@@ -368,22 +369,22 @@ let rec edible ({div; conv; ps} as p) arities showstoppers =
            aux showstoppers xs
           with
            Dangerous ->
-            aux (sort_uniq (h::showstoppers)) ps in
-
- let showstoppers = sort_uniq (aux showstoppers ps) in
- let dangerous_conv =
-  List.map (dangerous_conv p arities showstoppers) (conv :> nf_nob list) in
+            aux (sort_uniq (h::showstoppers)) ps
+  in
+    let showstoppers = sort_uniq (aux showstoppers ps) in
+    let dangerous_conv =
+     List.map (dangerous_conv p arities showstoppers) (conv :> nf_nob list) 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 showstoppers' = showstoppers @ List.concat dangerous_conv in
- let showstoppers' = sort_uniq (match div with
-  | None -> showstoppers'
-  | Some div ->
-    if List.exists ((=) (hd_of_i_var div)) showstoppers'
-    then showstoppers' @ free_vars (div :> nf) else showstoppers') in
- if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers', dangerous_conv
+    let showstoppers' = showstoppers @ List.concat dangerous_conv in
+    let showstoppers' = sort_uniq (match div with
+     | None -> showstoppers'
+     | Some div ->
+       if List.exists ((=) (hd_of_i_var div)) showstoppers'
+       then showstoppers' @ free_vars (div :> nf) else showstoppers') in
+    if showstoppers <> showstoppers' then edible p arities showstoppers' else showstoppers', dangerous_conv
 ;;
 
 let precompute_edible_data {ps; div} xs =
@@ -431,8 +432,8 @@ let critical_showstoppers p =
   let showstoppers_eat = List.filter
     (fun x -> not (List.mem x showstoppers_step))
     showstoppers_eat in
-List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ (string_of_var p.var_names) v)) showstoppers_step;
-List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ (string_of_var p.var_names) v)) showstoppers_eat;
+  List.iter (fun v -> prerr_endline ("DANGEROUS STEP: " ^ (string_of_var p.var_names) v)) showstoppers_step;
+  List.iter (fun v -> prerr_endline ("DANGEROUS EAT: " ^ (string_of_var p.var_names) v)) showstoppers_eat;
   p, showstoppers_step, showstoppers_eat
   ;;
 
@@ -556,7 +557,7 @@ let compute_special_k tms =
  | `Bottom
  | `Pacman
  | `Var _ -> 0 in
- Listx.max (Listx.map (fun t -> max (aux 0 t) (aux' true t)) tms)
+ Listx.max (Listx.map (aux 0) tms) + Listx.max (Listx.map (aux' true) tms)
 ;;
 
 let choose_step p =
@@ -582,36 +583,6 @@ let choose_step p =
       | x::_ ->
          prerr_endline ("INSTANTIATING TO EAT " ^ string_of_var p.var_names x);
          x) in
-(* Strategy that  decreases the special_k to 0 first (round robin)
-1:11m42 2:14m5 3:11m16s 4:14m46s 5:12m7s 6:6m31s *)
- let x =
-  try
-   match
-    hd_of (List.find (fun t ->
-     compute_special_k (Listx.Nil (t :> nf)) > 0 && arity_of_hd t > 0
-     ) (all_terms p))
-   with
-    | None -> assert false
-    | Some x ->
-       prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var p.var_names x);
-       x
-  with
-   Not_found ->
-    let arity_of_x = max_arity_tms x (all_terms p) in
-    assert (Util.option_get arity_of_x > 0);
-    x in
-(* Instantiate in decreasing order of compute_special_k
-1:15m14s 2:13m14s 3:4m55s 4:4m43s 5:4m34s 6:6m28s 7:3m31s
-let x =
- try
-  (match hd_of (snd (List.hd (List.sort (fun c1 c2 -> - compare (fst c1) (fst c2)) (filter_map (function `I _ as t -> Some (compute_special_k (Listx.Nil (t :> nf)),t) | _ -> None) (all_terms p))))) with
-      None -> assert false
-    | Some x ->
-       prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x);
-       x)
- with
-  Not_found -> x
-in*)
  let arity_of_x = Util.option_get (max_arity_tms x (all_terms p)) in
  let safe_arity_of_x = safe_arity_of_var p x in
  x, min arity_of_x safe_arity_of_x