1. we compare the expected branching with the actual one and

   prune the candidate when the latter is larger. The optimization
   is meant to rule out stange applications of flexible terms,
   such as the application of eq_f that always succeeds.
2. At top level, we index local equalitites for paramodulation for
   each cluster (i.e. we assume metas in a same cluster shares the
   same context *)

diff --git a/matitaB/components/ng_tactics/nnAuto.ml b/matitaB/components/ng_tactics/nnAuto.ml
index af30fcf9373166de3a267ad7b22ecb788ab526a6..fc8c83938689a9be03f9452275eae10a18d49474 100644 (file)
--- a/matitaB/components/ng_tactics/nnAuto.ml
+++ b/matitaB/components/ng_tactics/nnAuto.ml
@@ -942,8 +942,24 @@ let sort_candidates status ctx candidates =
 let sort_new_elems l =
   List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
 
+let rec stack_goals level gs = 
+  if level = 0 then []
+  else match gs with 
+    | [] -> assert false
+    | (g,_,_,_)::s -> 
+        let is_open = function
+          | (_,Continuationals.Stack.Open i) -> Some i
+          | (_,Continuationals.Stack.Closed _) -> None
+        in
+         HExtlib.filter_map is_open g @ stack_goals (level-1) s
+;;
+
+let open_goals level status = stack_goals level status#stack
+;;
+
 let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
  try
+  let old_og_no = List.length (open_goals (depth+1) status) in
   debug_print ~depth (lazy ("try " ^ (NotationPp.pp_term status) t));
   let status = 
     if smart= 0 then NTactics.apply_tac ("",0,t) status 
@@ -953,25 +969,27 @@ let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
       with Error _ -> 
         smart_apply_auto ("",0,t) eq_cache status 
   in
-(*
-  let og_no = openg_no status in 
-    if (* og_no > flags.maxwidth || *)
-      ((depth + 1) = flags.maxdepth && og_no <> 0) then
-        (debug_print ~depth (lazy "pruned immediately"); None)
-    else *)
-      (* useless 
-      let status, cict = disambiguate status ctx ("",0,t) None in
-      let status,ct = term_of_cic_term status cict ctx in
-      let _,_,metasenv,subst,_ = status#obj in
-      let ty = NCicTypeChecker.typeof subst metasenv ctx ct in
-      let res = branch status (mk_cic_term ctx ty) in
-      if smart=1 && og_no > res then 
-       (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = " 
+    (* we compare the expected branching with the actual one and
+       prune the candidate when the latter is larger. The optimization
+       is meant to rule out stange applications of flexible terms,
+       such as the application of eq_f that always succeeds.  
+       There is some gain but less than expected *)
+  let og_no = List.length (open_goals (depth+1) status) in
+  let status, cict = disambiguate status ctx ("",0,t) None in
+  let status,ct = term_of_cic_term status cict ctx in
+  let _,_,metasenv,subst,_ = status#obj in
+  let ty = NCicTypeChecker.typeof status subst metasenv ctx ct in
+  let res = branch status (mk_cic_term ctx ty) in
+  let diff = og_no - old_og_no in
+  debug_print (lazy ("expected branching: " ^ (string_of_int res)));
+  debug_print (lazy ("actual: branching" ^ (string_of_int diff))); 
+  (* one goal is closed by the application *)
+  if og_no - old_og_no >= res then 
+    (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = " 
                    ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
-        debug_print ~depth (lazy "strange application"); None)
-      else *)
-       (incr candidate_no;
-        Some ((!candidate_no,t),status))
+     debug_print ~depth (lazy "strange application"); None)
+  else 
+    (incr candidate_no; Some ((!candidate_no,t),status))
  with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
 ;;
 
@@ -1498,21 +1516,6 @@ let deep_focus_tac level focus status =
    status#set_stack gstatus
 ;;
 
-let rec stack_goals level gs = 
-  if level = 0 then []
-  else match gs with 
-    | [] -> assert false
-    | (g,_,_,_)::s -> 
-        let is_open = function
-          | (_,Continuationals.Stack.Open i) -> Some i
-          | (_,Continuationals.Stack.Closed _) -> None
-        in
-         HExtlib.filter_map is_open g @ stack_goals (level-1) s
-;;
-
-let open_goals level status = stack_goals level status#stack
-;;
-
 let move_to_side level status =
 match status#stack with
   | [] -> assert false
@@ -1525,6 +1528,12 @@ match status#stack with
       List.for_all (fun i -> IntSet.mem i others) 
        (HExtlib.filter_map is_open g)
 
+let top_cache ~depth top status cache =
+  if top then
+    let unit_eq = index_local_equations status#eq_cache status in 
+    {cache with unit_eq = unit_eq}
+  else cache
+
 let rec auto_clusters ?(top=false)  
     flags signature cache depth status : unit =
   debug_print ~depth (lazy ("entering auto clusters at depth " ^
@@ -1546,6 +1555,7 @@ let rec auto_clusters ?(top=false)
         in 
          auto_clusters flags signature cache (depth-1) status
   else if List.length goals < 2 then
+    let cache = top_cache ~depth top status cache in
     auto_main flags signature cache depth status
   else
     let all_goals = open_goals (depth+1) status in
@@ -1566,6 +1576,7 @@ let rec auto_clusters ?(top=false)
       let flags = 
         {flags with last = (List.length all_goals = 1)} in 
        (* no need to cluster *)
+      let cache = top_cache ~depth top status cache in
         auto_main flags signature cache depth status 
     else
       let classes = if top then List.rev classes else classes in
@@ -1586,6 +1597,7 @@ let rec auto_clusters ?(top=false)
              debug_print ~depth (lazy ("stack length = " ^ 
                        (string_of_int lold)));
              let fstatus = deep_focus_tac (depth+1) gl status in
+             let cache = top_cache ~depth top fstatus cache in
              try 
                debug_print ~depth (lazy ("focusing on" ^ 
                               String.concat "," (List.map string_of_int gl)));
@@ -1756,8 +1768,8 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
   let status = (status:> NTacStatus.tac_status) in
   let goals = head_goals status#stack in
   let status, facts = mk_th_cache status goals in
-  let unit_eq = index_local_equations status#eq_cache status in 
-  let cache = init_cache ~facts ~unit_eq () in 
+(* let unit_eq = index_local_equations status#eq_cache status in *) 
+  let cache = init_cache ~facts () in 
 (*   pp_th status facts; *)
 (*
   NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->