better logging and immediate pruning of new goals when

- length(goals) > maxwidth
- depth = maxdepth and goals <> []

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 61e9ff015e3c954e6c7deb1abcdf5bc85bb48493..525e1bfb695627144133ddb80d73f32cfc26f0a4 100644 (file)
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -14,7 +14,8 @@
 open Printf
 
 let debug = ref false
-let debug_print s = if !debug then prerr_endline (Lazy.force s) else ()
+let debug_print ?(depth=0) s = 
+  if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else ()
 let debug_do f = if !debug then f () else ()
 
 open Continuationals.Stack
@@ -1070,17 +1071,21 @@ let sort_new_elems l =
   List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2) l
 ;;
 
-let try_candidate status t g =
+let try_candidate flags depth status t g =
  try
-   debug_print (lazy (" try " ^ CicNotationPp.pp_term t));
+   debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
    let status = NTactics.focus_tac [g] status in
    let status = NTactics.apply_tac ("",0,t) status in
    let open_goals = head_goals status#stack in
-   debug_print 
-     (lazy (" success: "^String.concat " "(List.map string_of_int open_goals)));
-   incr candidate_no;
-   Some ((!candidate_no,t),status,open_goals)
- with Error (msg,exn) -> debug_print (lazy " failed"); None
+   debug_print ~depth
+     (lazy ("success: "^String.concat " "(List.map string_of_int open_goals)));
+   if List.length open_goals > flags.maxwidth || 
+      (depth = flags.maxdepth && open_goals <> []) then
+      (debug_print ~depth (lazy "pruned immediately"); None)
+   else
+     (incr candidate_no;
+      Some ((!candidate_no,t),status,open_goals))
+ with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
 ;;
 
 let rec mk_irl n = function
@@ -1106,13 +1111,14 @@ let get_candidates status cache_th signature gty =
   List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
 ;;
 
-let applicative_case signature status flags g gty cache = 
+let applicative_case depth signature status flags g gty cache = 
   let candidates = get_candidates status cache signature gty in
-  debug_print (lazy ("candidates: " ^ string_of_int (List.length candidates)));
+  debug_print ~depth
+    (lazy ("candidates: " ^ string_of_int (List.length candidates)));
   let elems = 
     List.fold_left 
       (fun elems cand ->
-        match try_candidate status cand g with
+        match try_candidate flags depth status cand g with
         | None -> elems
         | Some x -> x::elems)
       [] candidates
@@ -1130,7 +1136,7 @@ let equational_and_applicative_case
         signature status flags g gty cache 
     in
     let more_elems =
-        applicative_case 
+        applicative_case depth
           signature status flags g gty cache 
     in
       elems@more_elems
@@ -1141,7 +1147,7 @@ let equational_and_applicative_case
          smart_applicative_case dbd tables depth s fake_proof goalno 
            gty m context signature universe cache flags
       | None -> *)
-         applicative_case 
+         applicative_case depth
           signature status flags g gty cache 
     in
       elems
@@ -1188,7 +1194,6 @@ let intro_case status gno gty depth cache name =
    let status, keys = keys_of_term status t in
    let cache = List.fold_left (add_to_th t) cache keys in
    debug_print (lazy (" intro: "^ string_of_int open_goal));
-(*    pp_th status cache; *)
    incr candidate_no;
     (* XXX calculate the sort *)
    [(!candidate_no,Ast.Implicit `JustOne),0,status,[open_goal,P]],
@@ -1217,7 +1222,7 @@ let show pos =
     Format.fprintf fmt "@?";
     close_out oc;
     ignore(Sys.command ("dot -Tpng /tmp/a.dot > /tmp/a.png")); 
-    ignore(Sys.command ("gnome-open /tmp/a.png")))
+    ignore(Sys.command ("eog /tmp/a.png")))
 ;;
 
 let rightmost_bro pred =
@@ -1279,7 +1284,7 @@ let auto_main flags signature (pos : 'a and_pos) cache =
 
   and nextO ~unfocus (pos : 'a or_pos) cache =
     match Z.getO pos with
-    | S _ -> assert false (* XXX set to Nil when backtracking *)
+    | S _ -> assert false (* XXX set to Nil when backtrack *)
     | D g -> 
         match Z.downO pos with
         | Z.Solution (s,_,_) -> move_solution_up ~unfocus s pos cache 
@@ -1315,51 +1320,52 @@ let auto_main flags signature (pos : 'a and_pos) cache =
             | Some pos -> move_solution_up ~unfocus:true status pos cache 
 
   and attack pos cache and_item =
-     show pos;
+     (* show pos; *)
      match and_item with
        | _, S _ -> assert false (* next would close the proof or give a D *) 
-       | _ when Unix.gettimeofday () > flags.timeout ->
-           debug_print (lazy ("fail timeout"));
+       | (_, depth, _),_ when Unix.gettimeofday () > flags.timeout ->
+           debug_print ~depth (lazy ("fail timeout"));
            Gaveup 
        | (s, depth, width), D (_, T as g) when not flags.do_types -> 
-           debug_print (lazy "skip goal in Type");
+           debug_print ~depth (lazy "skip goal in Type");
            next ~unfocus:true (solved g depth width s pos) cache
        | (_,depth,_), D _ when depth > flags.maxdepth -> 
-           debug_print (lazy "fail depth");
+           debug_print ~depth (lazy "fail depth");
            next_choice (failed pos) cache
-       | (_,_,size), D _ when size > flags.maxsize -> 
-           debug_print (lazy "fail size");
+       | (_,depth,size), D _ when size > flags.maxsize -> 
+           debug_print ~depth (lazy "fail size");
            next_choice (failed pos) cache
        | (s,depth,size), D (gno,_ as g) -> 
            (* assert unexplored *)
            assert (Z.eject pos = ZipTree.Nil);
            match calculate_goal_ty g s with
            | None -> 
-              debug_print (lazy ("success side effect: " ^ string_of_int gno));
+              debug_print 
+                ~depth (lazy ("success side effect: " ^ string_of_int gno));
               next ~unfocus:false (solved g depth size s pos) cache
            | Some gty ->
               let s, gty = apply_subst s (ctx_of gty) gty in
-              debug_print (lazy ("EXAMINE: "^ ppterm s gty));
+              debug_print ~depth (lazy ("EXAMINE: "^ ppterm s gty));
               match cache_examine cache gty with
               | `Failed_in d when d <= depth -> 
-                  debug_print (lazy ("fail depth (c): "^string_of_int gno));
+                 debug_print ~depth(lazy("fail depth (c): "^string_of_int gno));
                   next_choice (failed pos) cache
               | `UnderInspection -> 
-                  debug_print (lazy ("fail loop: " ^ string_of_int gno));
+                  debug_print ~depth (lazy("fail loop: "^string_of_int gno));
                   next_choice (failed pos) cache
               | `Succeded t -> 
-                  debug_print (lazy ("success (c): " ^ string_of_int gno));
+                  debug_print ~depth (lazy("success (c): "^string_of_int gno));
                   let s = put_in_subst s g t gty in
                   next ~unfocus:true (solved g depth size s pos) cache
               | `Notfound 
               | `Failed_in _ -> 
                  (* more depth or is the first time we see the goal *)
                   if prunable s gty () then
-                    (debug_print (lazy( "fail one father is equal"));
+                    (debug_print ~depth (lazy( "fail one father is equal"));
                     next_choice (failed pos) cache)
                   else
                   let cache = cache_add_underinspection cache gty depth in
-                  debug_print (lazy ("INSPECTING: " ^ 
+                  debug_print ~depth (lazy ("INSPECTING: " ^ 
                     string_of_int gno ^ "("^ string_of_int size ^ ") "));
                   (* pos are possible computations for proving gty *)
                   let subgoals, cache =