clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
authorwenzelm
Fri Aug 27 16:29:12 2010 +0200 (2010-08-27)
changeset 38802a925c0ee42f7
parent 38801 319a28dd3564
child 38803 38b68972721b
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;
src/HOL/Tools/meson.ML
src/Pure/search.ML
     1.1 --- a/src/HOL/Tools/meson.ML	Fri Aug 27 15:46:08 2010 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Fri Aug 27 16:29:12 2010 +0200
     1.3 @@ -50,6 +50,9 @@
     1.4  val max_clauses_default = 60;
     1.5  val (max_clauses, setup) = Attrib.config_int "max_clauses" (K max_clauses_default);
     1.6  
     1.7 +(*No known example (on 1-5-2007) needs even thirty*)
     1.8 +val iter_deepen_limit = 50;
     1.9 +
    1.10  val disj_forward = @{thm disj_forward};
    1.11  val disj_forward2 = @{thm disj_forward2};
    1.12  val make_pos_rule = @{thm make_pos_rule};
    1.13 @@ -640,7 +643,7 @@
    1.14      end;
    1.15  
    1.16  fun iter_deepen_prolog_tac horns =
    1.17 -    ITER_DEEPEN (has_fewer_prems 1) (prolog_step_tac' horns);
    1.18 +    ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
    1.19  
    1.20  fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON make_clauses
    1.21    (fn cls =>
    1.22 @@ -653,7 +656,10 @@
    1.23              cat_lines ("meson method called:" ::
    1.24                map (Display.string_of_thm ctxt) (cls @ ths) @
    1.25                ["clauses:"] @ map (Display.string_of_thm ctxt) horns))
    1.26 -        in THEN_ITER_DEEPEN (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns) end));
    1.27 +        in
    1.28 +          THEN_ITER_DEEPEN iter_deepen_limit
    1.29 +            (resolve_tac goes 1) (has_fewer_prems 1) (prolog_step_tac' horns)
    1.30 +        end));
    1.31  
    1.32  fun meson_tac ctxt ths =
    1.33    SELECT_GOAL (TRY (safe_tac (claset_of ctxt)) THEN TRYALL (iter_deepen_meson_tac ctxt ths));
     2.1 --- a/src/Pure/search.ML	Fri Aug 27 15:46:08 2010 +0200
     2.2 +++ b/src/Pure/search.ML	Fri Aug 27 16:29:12 2010 +0200
     2.3 @@ -18,9 +18,8 @@
     2.4    val THEN_MAYBE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
     2.5    val DEPTH_SOLVE: tactic -> tactic
     2.6    val DEPTH_SOLVE_1: tactic -> tactic
     2.7 -  val iter_deepen_limit: int Unsynchronized.ref
     2.8 -  val THEN_ITER_DEEPEN: tactic -> (thm -> bool) -> (int -> tactic) -> tactic
     2.9 -  val ITER_DEEPEN: (thm -> bool) -> (int -> tactic) -> tactic
    2.10 +  val THEN_ITER_DEEPEN: int -> tactic -> (thm -> bool) -> (int -> tactic) -> tactic
    2.11 +  val ITER_DEEPEN: int -> (thm -> bool) -> (int -> tactic) -> tactic
    2.12    val trace_DEEPEN: bool Unsynchronized.ref
    2.13    val DEEPEN: int * int -> (int -> int -> tactic) -> int -> int -> tactic
    2.14    val trace_BEST_FIRST: bool Unsynchronized.ref
    2.15 @@ -117,21 +116,18 @@
    2.16      in  prune_aux (take (qs, []))  end;
    2.17  
    2.18  
    2.19 -(*No known example (on 1-5-2007) needs even thirty*)
    2.20 -val iter_deepen_limit = Unsynchronized.ref 50;
    2.21 -
    2.22  (*Depth-first iterative deepening search for a state that satisfies satp
    2.23    tactic tac0 sets up the initial goal queue, while tac1 searches it.
    2.24    The solution sequence is redundant: the cutoff heuristic makes it impossible
    2.25    to suppress solutions arising from earlier searches, as the accumulated cost
    2.26    (k) can be wrong.*)
    2.27 -fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st =>
    2.28 +fun THEN_ITER_DEEPEN lim tac0 satp tac1 = traced_tac (fn st =>
    2.29   let val countr = Unsynchronized.ref 0
    2.30       and tf = tracify trace_DEPTH_FIRST (tac1 1)
    2.31       and qs0 = tac0 st
    2.32       (*bnd = depth bound; inc = estimate of increment required next*)
    2.33       fun depth (bnd,inc) [] =
    2.34 -          if bnd > !iter_deepen_limit then
    2.35 +          if bnd > lim then
    2.36               (tracing (string_of_int (!countr) ^
    2.37                         " inferences so far.  Giving up at " ^ string_of_int bnd);
    2.38                NONE)
    2.39 @@ -170,19 +166,19 @@
    2.40                 end
    2.41    in depth (0,5) [] end);
    2.42  
    2.43 -val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac;
    2.44 +fun ITER_DEEPEN lim = THEN_ITER_DEEPEN lim all_tac;
    2.45  
    2.46  
    2.47  (*Simple iterative deepening tactical.  It merely "deepens" any search tactic
    2.48    using increment "inc" up to limit "lim". *)
    2.49  val trace_DEEPEN = Unsynchronized.ref false;
    2.50  
    2.51 -fun DEEPEN (inc,lim) tacf m i =
    2.52 +fun DEEPEN (inc, lim) tacf m i =
    2.53    let
    2.54      fun dpn m st =
    2.55        st |>
    2.56         (if has_fewer_prems i st then no_tac
    2.57 -        else if m>lim then
    2.58 +        else if m > lim then
    2.59            (if !trace_DEEPEN then tracing "Search depth limit exceeded: giving up" else ();
    2.60              no_tac)
    2.61          else