Introduction of a bound on DEPTH_ITER, to prevent the meson method from running forever

--- a/src/Pure/search.ML	Fri Jan 05 15:33:05 2007 +0100
+++ b/src/Pure/search.ML	Fri Jan 05 17:38:05 2007 +0100
@@ -20,6 +20,7 @@
   val DEPTH_SOLVE_1	: tactic -> tactic
   val ITER_DEEPEN	: (thm->bool) -> (int->tactic) -> tactic
   val THEN_ITER_DEEPEN	: tactic -> (thm->bool) -> (int->tactic) -> tactic
+  val iter_deepen_limit : int ref
 
   val has_fewer_prems	: int -> thm -> bool   
   val IF_UNSOLVED	: tactic -> tactic
@@ -131,6 +132,9 @@
     in  prune_aux (take (qs, []))  end;
 
 
+(*No known example (on 1-5-2007) needs even thirty*)
+val iter_deepen_limit = ref 50;
+
 (*Depth-first iterative deepening search for a state that satisfies satp
   tactic tac0 sets up the initial goal queue, while tac1 searches it.
   The solution sequence is redundant: the cutoff heuristic makes it impossible
@@ -142,6 +146,11 @@
      and qs0 = tac0 st
      (*bnd = depth bound; inc = estimate of increment required next*)
      fun depth (bnd,inc) [] = 
+          if bnd > !iter_deepen_limit then
+	     (tracing (string_of_int (!countr) ^ 
+		       " inferences so far.  Giving up at " ^ string_of_int bnd);
+	      NONE)
+          else
 	     (tracing (string_of_int (!countr) ^ 
 		       " inferences so far.  Searching to depth " ^ 
 		       string_of_int bnd);
@@ -152,8 +161,7 @@
           else
 	  case (countr := !countr+1;
 		if !trace_DEPTH_FIRST then
-		    tracing (string_of_int np ^ 
-			     implode (map (fn _ => "*") qs))
+		    tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
 		else ();
 		Seq.pull q) of
 	     NONE         => depth (bnd,inc) qs