--- 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;