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