src/Pure/search.ML
changeset 2869 acee08856cc9
parent 2672 85d7e800d754
child 3538 ed9de44032e0
     1.1 --- a/src/Pure/search.ML	Wed Apr 02 15:23:33 1997 +0200
     1.2 +++ b/src/Pure/search.ML	Wed Apr 02 15:24:42 1997 +0200
     1.3 @@ -9,6 +9,8 @@
     1.4  
     1.5  signature SEARCH =
     1.6    sig
     1.7 +  val DEEPEN  	        : int*int -> (int->int->tactic) -> int -> int -> tactic
     1.8 +
     1.9    val THEN_MAYBE	: tactic * tactic -> tactic
    1.10    val THEN_MAYBE'	: ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
    1.11  
    1.12 @@ -83,7 +85,7 @@
    1.13  
    1.14  
    1.15  
    1.16 -(**** Iterative deepening ****)
    1.17 +(**** Iterative deepening with pruning ****)
    1.18  
    1.19  fun has_vars (Var _) = true
    1.20    | has_vars (Abs (_,_,t)) = has_vars t
    1.21 @@ -161,6 +163,17 @@
    1.22  val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac;
    1.23  
    1.24  
    1.25 +(*Simple iterative deepening tactical.  It merely "deepens" any search tactic
    1.26 +  using increment "inc" up to limit "lim". *)
    1.27 +fun DEEPEN (inc,lim) tacf m i = 
    1.28 +  let fun dpn m = STATE(fn state => 
    1.29 +			if has_fewer_prems i state then no_tac
    1.30 +			else if m>lim then 
    1.31 +			     (writeln "Giving up..."; no_tac)
    1.32 +			else (writeln ("Depth = " ^ string_of_int m);
    1.33 +			      tacf m i  ORELSE  dpn (m+inc)))
    1.34 +  in  dpn m  end;
    1.35 +
    1.36  (*** Best-first search ***)
    1.37  
    1.38  val trace_BEST_FIRST = ref false;