# HG changeset patch
# User paulson
# Date 859987482 -7200
# Node ID acee08856cc9a105809790372fdc512a752586b7
# Parent  17a23a62f82ab53314541beaf94cfdbf9f949e67
DEEPEN now takes an upper bound for terminating searches

diff -r 17a23a62f82a -r acee08856cc9 src/Pure/search.ML
--- a/src/Pure/search.ML	Wed Apr 02 15:23:33 1997 +0200
+++ b/src/Pure/search.ML	Wed Apr 02 15:24:42 1997 +0200
@@ -9,6 +9,8 @@
 
 signature SEARCH =
   sig
+  val DEEPEN  	        : int*int -> (int->int->tactic) -> int -> int -> tactic
+
   val THEN_MAYBE	: tactic * tactic -> tactic
   val THEN_MAYBE'	: ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
 
@@ -83,7 +85,7 @@
 
 
 
-(**** Iterative deepening ****)
+(**** Iterative deepening with pruning ****)
 
 fun has_vars (Var _) = true
   | has_vars (Abs (_,_,t)) = has_vars t
@@ -161,6 +163,17 @@
 val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac;
 
 
+(*Simple iterative deepening tactical.  It merely "deepens" any search tactic
+  using increment "inc" up to limit "lim". *)
+fun DEEPEN (inc,lim) tacf m i = 
+  let fun dpn m = STATE(fn state => 
+			if has_fewer_prems i state then no_tac
+			else if m>lim then 
+			     (writeln "Giving up..."; no_tac)
+			else (writeln ("Depth = " ^ string_of_int m);
+			      tacf m i  ORELSE  dpn (m+inc)))
+  in  dpn m  end;
+
 (*** Best-first search ***)
 
 val trace_BEST_FIRST = ref false;