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