src/Pure/search.ML
author wenzelm
Wed Dec 12 23:36:07 2012 +0100 (2012-12-12 ago)
changeset 50499 f496b2b7bafb
parent 48263 94a7dc2276e4
child 55171 dc7a6f6be01b
permissions -rw-r--r--
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
     1 (*  Title:      Pure/search.ML
     2     Author:     Lawrence C Paulson and Norbert Voelker
     3 
     4 Search tacticals.
     5 *)
     6 
     7 infix 1 THEN_MAYBE THEN_MAYBE';
     8 
     9 signature SEARCH =
    10 sig
    11   val trace_DEPTH_FIRST: bool Unsynchronized.ref
    12   val DEPTH_FIRST: (thm -> bool) -> tactic -> tactic
    13   val has_fewer_prems: int -> thm -> bool
    14   val IF_UNSOLVED: tactic -> tactic
    15   val SOLVE: tactic -> tactic
    16   val THEN_MAYBE: tactic * tactic -> tactic
    17   val THEN_MAYBE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
    18   val DEPTH_SOLVE: tactic -> tactic
    19   val DEPTH_SOLVE_1: tactic -> tactic
    20   val THEN_ITER_DEEPEN: int -> tactic -> (thm -> bool) -> (int -> tactic) -> tactic
    21   val ITER_DEEPEN: int -> (thm -> bool) -> (int -> tactic) -> tactic
    22   val trace_DEEPEN: bool Unsynchronized.ref
    23   val DEEPEN: int * int -> (int -> int -> tactic) -> int -> int -> tactic
    24   val trace_BEST_FIRST: bool Unsynchronized.ref
    25   val THEN_BEST_FIRST: tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic
    26   val BEST_FIRST: (thm -> bool) * (thm -> int) -> tactic -> tactic
    27   val BREADTH_FIRST: (thm -> bool) -> tactic -> tactic
    28   val QUIET_BREADTH_FIRST: (thm -> bool) -> tactic -> tactic
    29   val trace_ASTAR: bool Unsynchronized.ref
    30   val THEN_ASTAR: tactic -> (thm -> bool) * (int -> thm -> int) -> tactic -> tactic
    31   val ASTAR: (thm -> bool) * (int -> thm -> int) -> tactic -> tactic
    32 end;
    33 
    34 structure Search: SEARCH =
    35 struct
    36 
    37 (**** Depth-first search ****)
    38 
    39 val trace_DEPTH_FIRST = Unsynchronized.ref false;
    40 
    41 (*Searches until "satp" reports proof tree as satisfied.
    42   Suppresses duplicate solutions to minimize search space.*)
    43 fun DEPTH_FIRST satp tac =
    44  let val tac = tracify trace_DEPTH_FIRST tac
    45      fun depth used [] = NONE
    46        | depth used (q::qs) =
    47           case Seq.pull q of
    48               NONE         => depth used qs
    49             | SOME(st,stq) =>
    50                 if satp st andalso not (member Thm.eq_thm used st)
    51                 then SOME(st, Seq.make
    52                                  (fn()=> depth (st::used) (stq::qs)))
    53                 else depth used (tac st :: stq :: qs)
    54   in  traced_tac (fn st => depth [] [Seq.single st])  end;
    55 
    56 
    57 
    58 (*Predicate: Does the rule have fewer than n premises?*)
    59 fun has_fewer_prems n rule = (nprems_of rule < n);
    60 
    61 (*Apply a tactic if subgoals remain, else do nothing.*)
    62 val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac;
    63 
    64 (*Force a tactic to solve its goal completely, otherwise fail *)
    65 fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac;
    66 
    67 (*Execute tac1, but only execute tac2 if there are at least as many subgoals
    68   as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
    69 fun (tac1 THEN_MAYBE tac2) st =
    70   (tac1  THEN  COND (has_fewer_prems (nprems_of st)) all_tac tac2)  st;
    71 
    72 fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
    73 
    74 (*Tactical to reduce the number of premises by 1.
    75   If no subgoals then it must fail! *)
    76 fun DEPTH_SOLVE_1 tac st = st |>
    77     (case nprems_of st of
    78         0 => no_tac
    79       | n => DEPTH_FIRST (has_fewer_prems n) tac);
    80 
    81 (*Uses depth-first search to solve ALL subgoals*)
    82 val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1);
    83 
    84 
    85 
    86 (**** Iterative deepening with pruning ****)
    87 
    88 fun has_vars (Var _) = true
    89   | has_vars (Abs (_,_,t)) = has_vars t
    90   | has_vars (f$t) = has_vars f orelse has_vars t
    91   | has_vars _ = false;
    92 
    93 (*Counting of primitive inferences is APPROXIMATE, as the step tactic
    94   may perform >1 inference*)
    95 
    96 (*Pruning of rigid ancestor to prevent backtracking*)
    97 fun prune (new as (k', np':int, rgd', stq), qs) =
    98     let fun prune_aux (qs, []) = new::qs
    99           | prune_aux (qs, (k,np,rgd,q)::rqs) =
   100               if np'+1 = np andalso rgd then
   101                   (if !trace_DEPTH_FIRST then
   102                        tracing ("Pruning " ^
   103                                 string_of_int (1+length rqs) ^ " levels")
   104                    else ();
   105                    (*Use OLD k: zero-cost solution; see Stickel, p 365*)
   106                    (k, np', rgd', stq) :: qs)
   107               else prune_aux ((k,np,rgd,q)::qs, rqs)
   108         fun take ([], rqs) = ([], rqs)
   109           | take (arg as ((k,np,rgd,stq)::qs, rqs)) =
   110                 if np' < np then take (qs, (k,np,rgd,stq)::rqs)
   111                             else arg
   112     in  prune_aux (take (qs, []))  end;
   113 
   114 
   115 (*Depth-first iterative deepening search for a state that satisfies satp
   116   tactic tac0 sets up the initial goal queue, while tac1 searches it.
   117   The solution sequence is redundant: the cutoff heuristic makes it impossible
   118   to suppress solutions arising from earlier searches, as the accumulated cost
   119   (k) can be wrong.*)
   120 fun THEN_ITER_DEEPEN lim tac0 satp tac1 = traced_tac (fn st =>
   121  let val countr = Unsynchronized.ref 0
   122      and tf = tracify trace_DEPTH_FIRST (tac1 1)
   123      and qs0 = tac0 st
   124      (*bnd = depth bound; inc = estimate of increment required next*)
   125      fun depth (bnd,inc) [] =
   126           if bnd > lim then
   127              (tracing (string_of_int (!countr) ^
   128                        " inferences so far.  Giving up at " ^ string_of_int bnd);
   129               NONE)
   130           else
   131              (tracing (string_of_int (!countr) ^
   132                        " inferences so far.  Searching to depth " ^
   133                        string_of_int bnd);
   134               (*larger increments make it run slower for the hard problems*)
   135               depth (bnd+inc, 10)) [(0, 1, false, qs0)]
   136        | depth (bnd,inc) ((k,np,rgd,q)::qs) =
   137           if k>=bnd then depth (bnd,inc) qs
   138           else
   139           case (Unsynchronized.inc countr;
   140                 if !trace_DEPTH_FIRST then
   141                     tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
   142                 else ();
   143                 Seq.pull q) of
   144              NONE         => depth (bnd,inc) qs
   145            | SOME(st,stq) =>
   146                if satp st       (*solution!*)
   147                then SOME(st, Seq.make
   148                          (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs)))
   149 
   150                else
   151                let val np' = nprems_of st
   152                      (*rgd' calculation assumes tactic operates on subgoal 1*)
   153                    val rgd' = not (has_vars (hd (prems_of st)))
   154                    val k' = k+np'-np+1  (*difference in # of subgoals, +1*)
   155                in  if k'+np' >= bnd
   156                    then depth (bnd, Int.min(inc, k'+np'+1-bnd)) qs
   157                    else if np' < np (*solved a subgoal; prune rigid ancestors*)
   158                    then depth (bnd,inc)
   159                          (prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs))
   160                    else depth (bnd,inc) ((k', np', rgd', tf st) ::
   161                                          (k,np,rgd,stq) :: qs)
   162                end
   163   in depth (0,5) [] end);
   164 
   165 fun ITER_DEEPEN lim = THEN_ITER_DEEPEN lim all_tac;
   166 
   167 
   168 (*Simple iterative deepening tactical.  It merely "deepens" any search tactic
   169   using increment "inc" up to limit "lim". *)
   170 val trace_DEEPEN = Unsynchronized.ref false;
   171 
   172 fun DEEPEN (inc, lim) tacf m i =
   173   let
   174     fun dpn m st =
   175       st |>
   176        (if has_fewer_prems i st then no_tac
   177         else if m > lim then
   178           (if !trace_DEEPEN then tracing "Search depth limit exceeded: giving up" else ();
   179             no_tac)
   180         else
   181           (if !trace_DEEPEN then tracing ("Search depth = " ^ string_of_int m) else ();
   182             tacf m i  ORELSE  dpn (m+inc)))
   183   in  dpn m  end;
   184 
   185 
   186 (*** Best-first search ***)
   187 
   188 (*total ordering on theorems, allowing duplicates to be found*)
   189 structure Thm_Heap = Heap
   190 (
   191   type elem = int * thm;
   192   val ord = prod_ord int_ord (Term_Ord.term_ord o pairself Thm.prop_of);
   193 );
   194 
   195 val trace_BEST_FIRST = Unsynchronized.ref false;
   196 
   197 (*For creating output sequence*)
   198 fun some_of_list []     = NONE
   199   | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
   200 
   201 (*Check for and delete duplicate proof states*)
   202 fun delete_all_min prf heap =
   203   if Thm_Heap.is_empty heap then heap
   204   else if Thm.eq_thm (prf, #2 (Thm_Heap.min heap))
   205   then delete_all_min prf (Thm_Heap.delete_min heap)
   206   else heap;
   207 
   208 (*Best-first search for a state that satisfies satp (incl initial state)
   209   Function sizef estimates size of problem remaining (smaller means better).
   210   tactic tac0 sets up the initial priority queue, while tac1 searches it. *)
   211 fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 =
   212   let val tac = tracify trace_BEST_FIRST tac1
   213       fun pairsize th = (sizef th, th);
   214       fun bfs (news,nprf_heap) =
   215            (case  List.partition satp news  of
   216                 ([],nonsats) => next(fold_rev Thm_Heap.insert (map pairsize nonsats) nprf_heap)
   217               | (sats,_)  => some_of_list sats)
   218       and next nprf_heap =
   219             if Thm_Heap.is_empty nprf_heap then NONE
   220             else
   221             let val (n,prf) = Thm_Heap.min nprf_heap
   222             in if !trace_BEST_FIRST
   223                then tracing("state size = " ^ string_of_int n)
   224                else ();
   225                bfs (Seq.list_of (tac prf),
   226                     delete_all_min prf (Thm_Heap.delete_min nprf_heap))
   227             end
   228       fun btac st = bfs (Seq.list_of (tac0 st), Thm_Heap.empty)
   229   in traced_tac btac end;
   230 
   231 (*Ordinary best-first search, with no initial tactic*)
   232 val BEST_FIRST = THEN_BEST_FIRST all_tac;
   233 
   234 (*Breadth-first search to satisfy satpred (including initial state)
   235   SLOW -- SHOULD NOT USE APPEND!*)
   236 fun gen_BREADTH_FIRST message satpred (tac:tactic) =
   237   let val tacf = Seq.list_of o tac;
   238       fun bfs prfs =
   239          (case  List.partition satpred prfs  of
   240               ([],[]) => []
   241             | ([],nonsats) =>
   242                   (message("breadth=" ^ string_of_int(length nonsats));
   243                    bfs (maps tacf nonsats))
   244             | (sats,_)  => sats)
   245   in (fn st => Seq.of_list (bfs [st])) end;
   246 
   247 val BREADTH_FIRST = gen_BREADTH_FIRST tracing;
   248 val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ());
   249 
   250 
   251 (*  Author:     Norbert Voelker, FernUniversitaet Hagen
   252     Remarks:    Implementation of A*-like proof procedure by modification
   253                 of the existing code for BEST_FIRST and best_tac so that the
   254                 current level of search is taken into account.
   255 *)
   256 
   257 (*Insertion into priority queue of states, marked with level *)
   258 fun insert_with_level (lnth: int*int*thm) [] = [lnth]
   259   | insert_with_level (l,m,th) ((l',n,th') :: nths) =
   260       if  n<m then (l',n,th') :: insert_with_level (l,m,th) nths
   261       else if  n=m andalso Thm.eq_thm(th,th')
   262               then (l',n,th')::nths
   263               else (l,m,th)::(l',n,th')::nths;
   264 
   265 (*For creating output sequence*)
   266 fun some_of_list []     = NONE
   267   | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
   268 
   269 val trace_ASTAR = Unsynchronized.ref false;
   270 
   271 fun THEN_ASTAR tac0 (satp, costf) tac1 =
   272   let val tf = tracify trace_ASTAR tac1;
   273       fun bfs (news,nprfs,level) =
   274       let fun cost thm = (level, costf level thm, thm)
   275       in (case  List.partition satp news  of
   276             ([],nonsats)
   277                  => next (fold_rev (insert_with_level o cost) nonsats nprfs)
   278           | (sats,_)  => some_of_list sats)
   279       end and
   280       next []  = NONE
   281         | next ((level,n,prf)::nprfs)  =
   282             (if !trace_ASTAR
   283                then tracing("level = " ^ string_of_int level ^
   284                          "  cost = " ^ string_of_int n ^
   285                          "  queue length =" ^ string_of_int (length nprfs))
   286                else ();
   287              bfs (Seq.list_of (tf prf), nprfs,level+1))
   288       fun tf st = bfs (Seq.list_of (tac0 st), [], 0)
   289   in traced_tac tf end;
   290 
   291 (*Ordinary ASTAR, with no initial tactic*)
   292 val ASTAR = THEN_ASTAR all_tac;
   293 
   294 end;
   295 
   296 open Search;