# HG changeset patch # User wenzelm # Date 1460148438 -7200 # Node ID 621afc4607ec9f19b4df53f06a3e11c7f256053d # Parent 0f794993485a911283ec25e23395065ceacf48ee eliminated ancient TTY-based Tactical.tracify and related global references; diff -r 0f794993485a -r 621afc4607ec src/Pure/search.ML --- 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; diff -r 0f794993485a -r 621afc4607ec src/Pure/tactical.ML --- 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;