src/Pure/search.ML

 
 infix 1 THEN_MAYBE THEN_MAYBE';
 
 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
   val SOLVE: tactic -> tactic
   val THEN_MAYBE: tactic * tactic -> tactic
   val THEN_MAYBE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
   val DEPTH_SOLVE: tactic -> tactic
   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;
 
 structure Search: SEARCH =
 struct
 
 (**** 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
             NONE => depth used qs
           | SOME (st, stq) =>
               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?*)
 fun has_fewer_prems n rule = Thm.nprems_of rule < n;
 

 fun prune (new as (k', np':int, rgd', stq), qs) =
   let
     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)) =
             if np' < np then take (qs, (k, np, rgd, stq) :: rqs) else arg;
   in prune_aux (take (qs, [])) end;

 (*Depth-first iterative deepening search for a state that satisfies satp
   tactic tac0 sets up the initial goal queue, while tac1 searches it.
   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!*)
                 SOME(st, Seq.make (fn() => depth (bnd, inc) ((k, np, rgd, stq) :: qs)))
               else

                   if k' + np' >= bnd then depth (bnd, Int.min (inc, k' + np' + 1 - bnd)) qs
                   else if np' < np (*solved a subgoal; prune rigid ancestors*)
                   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;
 
 
 (*** Best-first search ***)
 

 (
   type elem = int * thm;
   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));
 
 (*Check for and delete duplicate proof states*)

   else heap;
 
 (*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 =
-  let
-    val tac = tracify trace_BEST_FIRST tac1;
+fun THEN_BEST_FIRST tac0 (satp, sizef) tac =
+  let
     fun pairsize th = (sizef th, th);
     fun bfs (news, nprf_heap) =
       (case List.partition satp news of
         ([], nonsats) => next (fold_rev Thm_Heap.insert (map pairsize nonsats) nprf_heap)
       | (sats, _)  => some_of_list sats)
     and next nprf_heap =
       if Thm_Heap.is_empty nprf_heap then NONE
       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;
 
 (*Breadth-first search to satisfy satpred (including initial state)

 
 (*For creating output sequence*)
 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 =
-  let
-    val tf = tracify trace_ASTAR tac1;
+fun THEN_ASTAR tac0 (satp, costf) tac =
+  let
     fun bfs (news, nprfs, level) =
       let fun cost thm = (level, costf level thm, thm) in
         (case List.partition satp news of
           ([], nonsats) => next (fold_rev (insert_with_level o cost) nonsats nprfs)
         | (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;
 
 end;