On the last goal at maxdepth we stop at the first solution.

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index fdf2d2ea3138130ca23aa7ecabeac40b0fc1fdb0..c9f641cb3ae72ef01a32c204311698dbdfa31208 100644 (file)
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -1371,6 +1371,7 @@ let search_in_th gty th =
 
 type flags = {
         do_types : bool; (* solve goals in Type *)
+        last : bool; (* last goal: take first solution only  *)
         maxwidth : int;
         maxsize  : int;
         maxdepth : int;
@@ -1427,7 +1428,7 @@ let try_candidate ?(smart=0) flags depth status eq_cache t =
        smart_apply_auto ("",0,t) eq_cache status in 
   let og_no = openg_no status in 
     if (* og_no > flags.maxwidth || *)
-      (depth = flags.maxdepth && og_no <> 0) then
+      ((depth + 1) = flags.maxdepth && og_no <> 0) then
        (print ~depth (lazy "pruned immediately"); None)
    else
      (incr candidate_no;
@@ -1496,24 +1497,32 @@ let applicative_case depth signature status flags gty (cache:cache) =
 (*
   let sm = 0 in 
   let smart_candidates = [] in *)
-  let sm = if is_eq then 0 else 2 in 
-  let elems = 
+  let sm = if is_eq then 0 else 2 in
+  let only_one = flags.last && (depth + 1 = flags.maxdepth) in 
+  print (lazy ("only_one: " ^ (string_of_bool only_one)));
+  let elems =  
     List.fold_left 
       (fun elems cand ->
-        match try_candidate (~smart:sm) 
-         flags depth status cache.unit_eq cand with
-        | None -> elems
-        | Some x -> x::elems)
+        if (only_one && (elems <> [])) then elems 
+        else
+          match try_candidate (~smart:sm) 
+            flags depth status cache.unit_eq cand with
+               | None -> elems
+               | Some x -> x::elems)
       [] candidates
   in
   let more_elems = 
-    List.fold_left 
-      (fun elems cand ->
-        match try_candidate (~smart:1) 
-         flags depth status cache.unit_eq cand with
-        | None -> elems
-        | Some x -> x::elems)
-      [] smart_candidates
+    if only_one && elems <> [] then elems 
+    else
+      List.fold_left 
+       (fun elems cand ->
+        if (only_one && (elems <> [])) then elems 
+        else
+           match try_candidate (~smart:1) 
+            flags depth status cache.unit_eq cand with
+               | None -> elems
+               | Some x -> x::elems)
+       [] smart_candidates
   in
   elems@more_elems
 ;;
@@ -1729,6 +1738,7 @@ let focus_tac focus status =
 let rec auto_clusters ?(top=false)  
     flags signature cache depth status : unit =
   debug_print ~depth (lazy "entering auto clusters");
+  print (lazy ("auto cluster: " ^ (string_of_bool flags.last)));
   (* ignore(Unix.select [] [] [] 0.01); *)
   let status = clean_up_tac status in
   let goals = head_goals status#stack in
@@ -1737,7 +1747,7 @@ let rec auto_clusters ?(top=false)
   else if List.length goals < 2 then 
     auto_main flags signature cache depth status 
   else
-    debug_print ~depth (lazy ("goals = " ^ 
+    print ~depth (lazy ("goals = " ^ 
       String.concat "," (List.map string_of_int goals)));
     let classes = HExtlib.clusters (deps status) goals in
     let classes = if top then List.rev classes else classes in
@@ -1769,6 +1779,7 @@ and
    of the initial head goals in the stack *)
 
 auto_main flags signature (cache:cache) depth status: unit =
+  print (lazy ("auto enter: " ^ (string_of_bool flags.last)));
   debug_print ~depth (lazy "entering auto main");
   (* ignore(Unix.select [] [] [] 0.01); *)
   let status = sort_tac (clean_up_tac status) in
@@ -1795,8 +1806,10 @@ auto_main flags signature (cache:cache) depth status: unit =
          (debug_print (lazy "SUBSUMED");
           raise (Gaveup IntSet.add g IntSet.empty))
        else 
+        let do_flags = 
+         {flags with last = flags.last && (not branch)} in 
        let alternatives, cache = 
-          do_something signature flags status g depth gty cache in
+          do_something signature do_flags status g depth gty cache in
        let loop_cache =
          let under_inspection = 
            add_to_th closegty cache.under_inspection closegty in
@@ -1812,7 +1825,11 @@ auto_main flags signature (cache:cache) depth status: unit =
                debug_print (~depth:depth') 
                 (lazy ("Case: " ^ CicNotationPp.pp_term t));
               let flags' = 
-                {flags with maxwidth = flags.maxwidth - ng +1} in 
+                {flags with maxwidth = flags.maxwidth - ng +1} in
+                (* sistemare *)
+              let flags' = 
+                {flags' with last = flags'.last && (not branch)} in 
+               print (lazy ("auto last: " ^ (string_of_bool flags'.last)));
               try auto_clusters flags' signature loop_cache
                 depth' status; unsat
                with 
@@ -1822,6 +1839,8 @@ auto_main flags signature (cache:cache) depth status: unit =
                       let status = NTactics.merge_tac status
                       in
                         (* old cache, here *)
+                      let flags = 
+                        {flags with maxwidth = flags.maxwidth - 1} in 
                         try auto_clusters flags signature cache 
                           depth status; assert false
                         with Gaveup f ->
@@ -1873,6 +1892,7 @@ let auto_tac ~params:(_univ,flags) status =
   let goals = List.map (fun i -> (i,P)) goals in
   let signature = () in
   let flags = { 
+          last = true;
           maxwidth = width;
           maxsize = size;
           maxdepth = depth;