X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=48262639dfbda9ea48b1d6dcf5ef384af93d39d8;hb=0a50c398d9eef65620f18f99ef675770b50a920c;hp=dfe0da1b8c927a96c3591d1f1711c4b74db57af6;hpb=4c81587c5f911c4d5f818765106bb5373967d715;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index dfe0da1..4826263 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -58,7 +58,7 @@ let first bound p var f =
    with Backtrack s ->
 prerr_endline (">>>>>> BACKTRACK (reason: " ^ s ^") measure=$ ");
      List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ;
-prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int i);
+prerr_endline("Now trying var="^string_of_var p.var_names var^" i="^string_of_int (i+1));
      aux (i+1)
  in
   aux 1
@@ -368,22 +368,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 =
@@ -397,6 +397,11 @@ let precompute_edible_data {ps; div} xs =
    ) xs)
 ;;
 
+(** Returns (p, showstoppers_step, showstoppers_eat) where:
+    - showstoppers_step are the heads occurring twice
+      in the same discriminating set
+    - showstoppers_eat are the heads in ps having different number
+      of arguments *)
 let critical_showstoppers p =
   let p = super_simplify p in
   let hd_of_div = match p.div with None -> [] | Some t -> [hd_of_i_var t] in
@@ -426,8 +431,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
   ;;
 
@@ -436,11 +441,11 @@ let eat p =
   let showstoppers = showstoppers_step @ showstoppers_eat in
   let heads = List.sort compare (filter_map hd_of ps) in
   let arities = precompute_edible_data p (uniq heads) in
-  let showstoppers, showstoppers_conv = edible p arities showstoppers in
-  let l = List.filter (fun (_,hd,_) -> not (List.mem hd showstoppers)) arities in
+  let inedible, showstoppers_conv = edible p arities showstoppers in
+  let l = List.filter (fun (_,hd,_) -> not (List.mem hd inedible)) arities in
   let p =
   List.fold_left (fun p (pos,hd,nargs) -> if pos = -1 then p else
-   let v = `N(pos) in
+   let v = `N pos in
    let inst = make_lams v nargs in
 prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ string_of_term p inst);
    { p with sigma = p.sigma @ [hd,inst] }
@@ -457,7 +462,7 @@ prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ strin
  let p = match p.div with
   | None -> p
   | Some div ->
-   if List.mem (hd_of_i_var div) showstoppers
+   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
@@ -465,14 +470,14 @@ prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ strin
     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 p.var_names) l))) dangerous_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 =
    List.map (function s,t ->
     try
      if s <> [] then t else (
      (match t with | `Var _ -> raise Not_found | _ -> ());
-     let _ = List.find (fun h -> hd_of t = Some h) showstoppers in
+     let _ = List.find (fun h -> hd_of t = Some h) inedible in
       t)
     with Not_found -> match hd_of t with
      | None -> assert (t = convergent_dummy); t