--- a/src/Pure/search.ML Fri Apr 08 21:49:43 2016 +0200
+++ b/src/Pure/search.ML Fri Apr 08 22:47:18 2016 +0200
@@ -9,7 +9,6 @@
signature SEARCH =
sig
- val trace_DEPTH_FIRST: bool Unsynchronized.ref
val DEPTH_FIRST: (thm -> bool) -> tactic -> tactic
val has_fewer_prems: int -> thm -> bool
val IF_UNSOLVED: tactic -> tactic
@@ -20,14 +19,11 @@
val DEPTH_SOLVE_1: tactic -> tactic
val THEN_ITER_DEEPEN: int -> tactic -> (thm -> bool) -> (int -> tactic) -> tactic
val ITER_DEEPEN: int -> (thm -> bool) -> (int -> tactic) -> tactic
- val trace_DEEPEN: bool Unsynchronized.ref
val DEEPEN: int * int -> (int -> int -> tactic) -> int -> int -> tactic
- val trace_BEST_FIRST: bool Unsynchronized.ref
val THEN_BEST_FIRST: tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic
val BEST_FIRST: (thm -> bool) * (thm -> int) -> tactic -> tactic
val BREADTH_FIRST: (thm -> bool) -> tactic -> tactic
val QUIET_BREADTH_FIRST: (thm -> bool) -> tactic -> tactic
- val trace_ASTAR: bool Unsynchronized.ref
val THEN_ASTAR: tactic -> (thm -> bool) * (int -> thm -> int) -> tactic -> tactic
val ASTAR: (thm -> bool) * (int -> thm -> int) -> tactic -> tactic
end;
@@ -37,13 +33,10 @@
(**** Depth-first search ****)
-val trace_DEPTH_FIRST = Unsynchronized.ref false;
-
(*Searches until "satp" reports proof tree as satisfied.
Suppresses duplicate solutions to minimize search space.*)
fun DEPTH_FIRST satp tac =
let
- val tac = tracify trace_DEPTH_FIRST tac
fun depth used [] = NONE
| depth used (q :: qs) =
(case Seq.pull q of
@@ -52,7 +45,7 @@
if satp st andalso not (member Thm.eq_thm used st) then
SOME (st, Seq.make (fn() => depth (st :: used) (stq :: qs)))
else depth used (tac st :: stq :: qs));
- in traced_tac (fn st => depth [] [Seq.single st]) end;
+ in fn st => Seq.make (fn () => depth [] [Seq.single st]) end;
(*Predicate: Does the rule have fewer than n premises?*)
@@ -99,12 +92,8 @@
fun prune_aux (qs, []) = new :: qs
| prune_aux (qs, (k, np, rgd, q) :: rqs) =
if np' + 1 = np andalso rgd then
- (if !trace_DEPTH_FIRST then
- tracing ("Pruning " ^
- string_of_int (1+length rqs) ^ " levels")
- else ();
(*Use OLD k: zero-cost solution; see Stickel, p 365*)
- (k, np', rgd', stq) :: qs)
+ (k, np', rgd', stq) :: qs
else prune_aux ((k, np, rgd, q) :: qs, rqs)
fun take ([], rqs) = ([], rqs)
| take (arg as ((k, np, rgd, stq) :: qs, rqs)) =
@@ -117,35 +106,21 @@
The solution sequence is redundant: the cutoff heuristic makes it impossible
to suppress solutions arising from earlier searches, as the accumulated cost
(k) can be wrong.*)
-fun THEN_ITER_DEEPEN lim tac0 satp tac1 = traced_tac (fn st =>
+fun THEN_ITER_DEEPEN lim tac0 satp tac1 st =
let
val countr = Unsynchronized.ref 0
- and tf = tracify trace_DEPTH_FIRST (tac1 1)
+ and tf = tac1 1
and qs0 = tac0 st
(*bnd = depth bound; inc = estimate of increment required next*)
fun depth (bnd, inc) [] =
- if bnd > lim then
- (if !trace_DEPTH_FIRST then
- tracing (string_of_int (! countr) ^
- " inferences so far. Giving up at " ^ string_of_int bnd)
- else ();
- NONE)
+ if bnd > lim then NONE
else
- (if !trace_DEPTH_FIRST then
- tracing (string_of_int (!countr) ^
- " inferences so far. Searching to depth " ^ string_of_int bnd)
- else ();
(*larger increments make it run slower for the hard problems*)
- depth (bnd + inc, 10)) [(0, 1, false, qs0)]
+ depth (bnd + inc, 10) [(0, 1, false, qs0)]
| depth (bnd, inc) ((k, np, rgd, q) :: qs) =
if k >= bnd then depth (bnd, inc) qs
else
- (case
- (Unsynchronized.inc countr;
- if !trace_DEPTH_FIRST then
- tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
- else ();
- Seq.pull q) of
+ (case (Unsynchronized.inc countr; Seq.pull q) of
NONE => depth (bnd, inc) qs
| SOME (st, stq) =>
if satp st then (*solution!*)
@@ -162,26 +137,20 @@
then depth (bnd, inc) (prune ((k', np', rgd', tf st), (k, np, rgd, stq) :: qs))
else depth (bnd, inc) ((k', np', rgd', tf st) :: (k, np, rgd, stq) :: qs)
end)
- in depth (0, 5) [] end);
+ in Seq.make (fn () => depth (0, 5) []) end;
fun ITER_DEEPEN lim = THEN_ITER_DEEPEN lim all_tac;
(*Simple iterative deepening tactical. It merely "deepens" any search tactic
using increment "inc" up to limit "lim". *)
-val trace_DEEPEN = Unsynchronized.ref false;
-
fun DEEPEN (inc, lim) tacf m i =
let
fun dpn m st =
st |>
(if has_fewer_prems i st then no_tac
- else if m > lim then
- (if !trace_DEEPEN then tracing "Search depth limit exceeded: giving up" else ();
- no_tac)
- else
- (if !trace_DEEPEN then tracing ("Search depth = " ^ string_of_int m) else ();
- tacf m i ORELSE dpn (m+inc)))
+ else if m > lim then no_tac
+ else tacf m i ORELSE dpn (m+inc))
in dpn m end;
@@ -194,8 +163,6 @@
val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 Thm.prop_of);
);
-val trace_BEST_FIRST = Unsynchronized.ref false;
-
(*For creating output sequence*)
fun some_of_list [] = NONE
| some_of_list (x :: l) = SOME (x, Seq.make (fn () => some_of_list l));
@@ -210,9 +177,8 @@
(*Best-first search for a state that satisfies satp (incl initial state)
Function sizef estimates size of problem remaining (smaller means better).
tactic tac0 sets up the initial priority queue, while tac1 searches it. *)
-fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 =
+fun THEN_BEST_FIRST tac0 (satp, sizef) tac =
let
- val tac = tracify trace_BEST_FIRST tac1;
fun pairsize th = (sizef th, th);
fun bfs (news, nprf_heap) =
(case List.partition satp news of
@@ -223,15 +189,11 @@
else
let
val (n, prf) = Thm_Heap.min nprf_heap;
- val _ =
- if !trace_BEST_FIRST
- then tracing("state size = " ^ string_of_int n)
- else ();
in
bfs (Seq.list_of (tac prf), delete_all_min prf (Thm_Heap.delete_min nprf_heap))
end;
fun btac st = bfs (Seq.list_of (tac0 st), Thm_Heap.empty)
- in traced_tac btac end;
+ in fn st => Seq.make (fn () => btac st) end;
(*Ordinary best-first search, with no initial tactic*)
val BEST_FIRST = THEN_BEST_FIRST all_tac;
@@ -271,11 +233,8 @@
fun some_of_list [] = NONE
| some_of_list (x :: xs) = SOME (x, Seq.make (fn () => some_of_list xs));
-val trace_ASTAR = Unsynchronized.ref false;
-
-fun THEN_ASTAR tac0 (satp, costf) tac1 =
+fun THEN_ASTAR tac0 (satp, costf) tac =
let
- val tf = tracify trace_ASTAR tac1;
fun bfs (news, nprfs, level) =
let fun cost thm = (level, costf level thm, thm) in
(case List.partition satp news of
@@ -283,15 +242,8 @@
| (sats, _) => some_of_list sats)
end
and next [] = NONE
- | next ((level, n, prf) :: nprfs) =
- (if !trace_ASTAR then
- tracing ("level = " ^ string_of_int level ^
- " cost = " ^ string_of_int n ^
- " queue length =" ^ string_of_int (length nprfs))
- else ();
- bfs (Seq.list_of (tf prf), nprfs, level + 1))
- fun tf st = bfs (Seq.list_of (tac0 st), [], 0);
- in traced_tac tf end;
+ | next ((level, n, prf) :: nprfs) = bfs (Seq.list_of (tac prf), nprfs, level + 1)
+ in fn st => Seq.make (fn () => bfs (Seq.list_of (tac0 st), [], 0)) end;
(*Ordinary ASTAR, with no initial tactic*)
val ASTAR = THEN_ASTAR all_tac;
--- a/src/Pure/tactical.ML Fri Apr 08 21:49:43 2016 +0200
+++ b/src/Pure/tactical.ML Fri Apr 08 22:47:18 2016 +0200
@@ -31,11 +31,6 @@
val FIRST1: (int -> tactic) list -> tactic
val RANGE: (int -> tactic) list -> int -> tactic
val print_tac: Proof.context -> string -> tactic
- val pause_tac: tactic
- val trace_REPEAT: bool Unsynchronized.ref
- val suppress_tracing: bool Unsynchronized.ref
- val tracify: bool Unsynchronized.ref -> tactic -> tactic
- val traced_tac: (thm -> (thm * thm Seq.seq) option) -> tactic
val REPEAT_DETERM_N: int -> tactic -> tactic
val REPEAT_DETERM: tactic -> tactic
val REPEAT: tactic -> tactic
@@ -179,73 +174,23 @@
| RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
-(*** Tracing tactics ***)
-
(*Print the current proof state and pass it on.*)
fun print_tac ctxt msg st =
(tracing (msg ^ "\n" ^ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals ctxt st)));
Seq.single st);
-(*Pause until a line is typed -- if non-empty then fail. *)
-fun pause_tac st =
- (tracing "** Press RETURN to continue:";
- if TextIO.inputLine TextIO.stdIn = SOME "\n" then Seq.single st
- else (tracing "Goodbye"; Seq.empty));
-
-exception TRACE_EXIT of thm
-and TRACE_QUIT;
-
-(*Tracing flags*)
-val trace_REPEAT= Unsynchronized.ref false
-and suppress_tracing = Unsynchronized.ref false;
-
-(*Handle all tracing commands for current state and tactic *)
-fun exec_trace_command flag (tac, st) =
- (case TextIO.inputLine TextIO.stdIn of
- SOME "\n" => tac st
- | SOME "f\n" => Seq.empty
- | SOME "o\n" => (flag := false; tac st)
- | SOME "s\n" => (suppress_tracing := true; tac st)
- | SOME "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st))
- | SOME "quit\n" => raise TRACE_QUIT
- | _ =>
- (tracing
- "Type RETURN to continue or...\n\
- \ f - to fail here\n\
- \ o - to switch tracing off\n\
- \ s - to suppress tracing until next entry to a tactical\n\
- \ x - to exit at this point\n\
- \ quit - to abort this tracing run\n\
- \** Well? "; exec_trace_command flag (tac, st)));
-
-
-(*Extract from a tactic, a thm->thm seq function that handles tracing*)
-fun tracify flag tac st =
- if !flag andalso not (!suppress_tracing) then
- (tracing (Pretty.string_of (Pretty.chunks
- (Goal_Display.pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm st)) st @
- [Pretty.str "** Press RETURN to continue:"])));
- exec_trace_command flag (tac, st))
- else tac st;
-
-(*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*)
-fun traced_tac seqf st =
- (suppress_tracing := false;
- Seq.make (fn () => seqf st handle TRACE_EXIT st' => SOME (st', Seq.empty)));
-
(*Deterministic REPEAT: only retains the first outcome;
uses less space than REPEAT; tail recursive.
If non-negative, n bounds the number of repetitions.*)
fun REPEAT_DETERM_N n tac =
let
- val tac = tracify trace_REPEAT tac;
fun drep 0 st = SOME (st, Seq.empty)
| drep n st =
(case Seq.pull (tac st) of
NONE => SOME(st, Seq.empty)
| SOME (st', _) => drep (n - 1) st');
- in traced_tac (drep n) end;
+ in fn st => Seq.make (fn () => drep n st) end;
(*Allows any number of repetitions*)
val REPEAT_DETERM = REPEAT_DETERM_N ~1;
@@ -253,7 +198,6 @@
(*General REPEAT: maintains a stack of alternatives; tail recursive*)
fun REPEAT tac =
let
- val tac = tracify trace_REPEAT tac;
fun rep qs st =
(case Seq.pull (tac st) of
NONE => SOME (st, Seq.make (fn () => repq qs))
@@ -263,7 +207,7 @@
(case Seq.pull q of
NONE => repq qs
| SOME (st, q) => rep (q :: qs) st);
- in traced_tac (rep []) end;
+ in fn st => Seq.make (fn () => rep [] st) end;
(*Repeat 1 or more times*)
fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac;