src/Pure/search.ML
changeset 23178 07ba6b58b3d2
parent 22360 26ead7ed4f4b
child 23841 598839baafed
     1.1 --- a/src/Pure/search.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Pure/search.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	Pure/search.ML
     1.5 +(*  Title:      Pure/search.ML
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson and Norbert Voelker
     1.8 +    Author:     Lawrence C Paulson and Norbert Voelker
     1.9  
    1.10  Search tacticals.
    1.11  *)
    1.12 @@ -9,33 +9,33 @@
    1.13  
    1.14  signature SEARCH =
    1.15    sig
    1.16 -  val DEEPEN  	        : int*int -> (int->int->tactic) -> int -> int -> tactic
    1.17 +  val DEEPEN            : int*int -> (int->int->tactic) -> int -> int -> tactic
    1.18  
    1.19 -  val THEN_MAYBE	: tactic * tactic -> tactic
    1.20 -  val THEN_MAYBE'	: ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
    1.21 +  val THEN_MAYBE        : tactic * tactic -> tactic
    1.22 +  val THEN_MAYBE'       : ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
    1.23  
    1.24 -  val trace_DEPTH_FIRST	: bool ref
    1.25 -  val DEPTH_FIRST	: (thm -> bool) -> tactic -> tactic
    1.26 -  val DEPTH_SOLVE	: tactic -> tactic
    1.27 -  val DEPTH_SOLVE_1	: tactic -> tactic
    1.28 -  val ITER_DEEPEN	: (thm->bool) -> (int->tactic) -> tactic
    1.29 -  val THEN_ITER_DEEPEN	: tactic -> (thm->bool) -> (int->tactic) -> tactic
    1.30 +  val trace_DEPTH_FIRST : bool ref
    1.31 +  val DEPTH_FIRST       : (thm -> bool) -> tactic -> tactic
    1.32 +  val DEPTH_SOLVE       : tactic -> tactic
    1.33 +  val DEPTH_SOLVE_1     : tactic -> tactic
    1.34 +  val ITER_DEEPEN       : (thm->bool) -> (int->tactic) -> tactic
    1.35 +  val THEN_ITER_DEEPEN  : tactic -> (thm->bool) -> (int->tactic) -> tactic
    1.36    val iter_deepen_limit : int ref
    1.37  
    1.38 -  val has_fewer_prems	: int -> thm -> bool   
    1.39 -  val IF_UNSOLVED	: tactic -> tactic
    1.40 -  val SOLVE		: tactic -> tactic
    1.41 +  val has_fewer_prems   : int -> thm -> bool
    1.42 +  val IF_UNSOLVED       : tactic -> tactic
    1.43 +  val SOLVE             : tactic -> tactic
    1.44    val DETERM_UNTIL_SOLVED: tactic -> tactic
    1.45 -  val trace_BEST_FIRST	: bool ref
    1.46 -  val BEST_FIRST	: (thm -> bool) * (thm -> int) -> tactic -> tactic
    1.47 -  val THEN_BEST_FIRST	: tactic -> (thm->bool) * (thm->int) -> tactic
    1.48 -			  -> tactic
    1.49 -  val trace_ASTAR	: bool ref
    1.50 -  val ASTAR	        : (thm -> bool) * (int->thm->int) -> tactic -> tactic
    1.51 -  val THEN_ASTAR	: tactic -> (thm->bool) * (int->thm->int) -> tactic
    1.52 -			  -> tactic
    1.53 -  val BREADTH_FIRST	: (thm -> bool) -> tactic -> tactic
    1.54 -  val QUIET_BREADTH_FIRST	: (thm -> bool) -> tactic -> tactic
    1.55 +  val trace_BEST_FIRST  : bool ref
    1.56 +  val BEST_FIRST        : (thm -> bool) * (thm -> int) -> tactic -> tactic
    1.57 +  val THEN_BEST_FIRST   : tactic -> (thm->bool) * (thm->int) -> tactic
    1.58 +                          -> tactic
    1.59 +  val trace_ASTAR       : bool ref
    1.60 +  val ASTAR             : (thm -> bool) * (int->thm->int) -> tactic -> tactic
    1.61 +  val THEN_ASTAR        : tactic -> (thm->bool) * (int->thm->int) -> tactic
    1.62 +                          -> tactic
    1.63 +  val BREADTH_FIRST     : (thm -> bool) -> tactic -> tactic
    1.64 +  val QUIET_BREADTH_FIRST       : (thm -> bool) -> tactic -> tactic
    1.65    end;
    1.66  
    1.67  
    1.68 @@ -48,7 +48,7 @@
    1.69        (Term.term_ord o Library.pairself (#prop o Thm.rep_thm)));
    1.70  
    1.71  
    1.72 -structure Search : SEARCH = 
    1.73 +structure Search : SEARCH =
    1.74  struct
    1.75  
    1.76  (**** Depth-first search ****)
    1.77 @@ -57,17 +57,17 @@
    1.78  
    1.79  (*Searches until "satp" reports proof tree as satisfied.
    1.80    Suppresses duplicate solutions to minimize search space.*)
    1.81 -fun DEPTH_FIRST satp tac = 
    1.82 +fun DEPTH_FIRST satp tac =
    1.83   let val tac = tracify trace_DEPTH_FIRST tac
    1.84       fun depth used [] = NONE
    1.85         | depth used (q::qs) =
    1.86 -	  case Seq.pull q of
    1.87 -	      NONE         => depth used qs
    1.88 -	    | SOME(st,stq) => 
    1.89 -		if satp st andalso not (member Thm.eq_thm used st)
    1.90 -		then SOME(st, Seq.make
    1.91 -			         (fn()=> depth (st::used) (stq::qs)))
    1.92 -		else depth used (tac st :: stq :: qs)
    1.93 +          case Seq.pull q of
    1.94 +              NONE         => depth used qs
    1.95 +            | SOME(st,stq) =>
    1.96 +                if satp st andalso not (member Thm.eq_thm used st)
    1.97 +                then SOME(st, Seq.make
    1.98 +                                 (fn()=> depth (st::used) (stq::qs)))
    1.99 +                else depth used (tac st :: stq :: qs)
   1.100    in  traced_tac (fn st => depth [] [Seq.single st])  end;
   1.101  
   1.102  
   1.103 @@ -86,7 +86,7 @@
   1.104  
   1.105  (*Execute tac1, but only execute tac2 if there are at least as many subgoals
   1.106    as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
   1.107 -fun (tac1 THEN_MAYBE tac2) st = 
   1.108 +fun (tac1 THEN_MAYBE tac2) st =
   1.109      (tac1  THEN  COND (has_fewer_prems (nprems_of st)) all_tac tac2)  st;
   1.110  
   1.111  fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
   1.112 @@ -95,7 +95,7 @@
   1.113    If no subgoals then it must fail! *)
   1.114  fun DEPTH_SOLVE_1 tac st = st |>
   1.115      (case nprems_of st of
   1.116 -	0 => no_tac
   1.117 +        0 => no_tac
   1.118        | n => DEPTH_FIRST (has_fewer_prems n) tac);
   1.119  
   1.120  (*Uses depth-first search to solve ALL subgoals*)
   1.121 @@ -114,21 +114,21 @@
   1.122    may perform >1 inference*)
   1.123  
   1.124  (*Pruning of rigid ancestor to prevent backtracking*)
   1.125 -fun prune (new as (k', np':int, rgd', stq), qs) = 
   1.126 +fun prune (new as (k', np':int, rgd', stq), qs) =
   1.127      let fun prune_aux (qs, []) = new::qs
   1.128            | prune_aux (qs, (k,np,rgd,q)::rqs) =
   1.129 -	      if np'+1 = np andalso rgd then
   1.130 -		  (if !trace_DEPTH_FIRST then
   1.131 -		       tracing ("Pruning " ^ 
   1.132 -				string_of_int (1+length rqs) ^ " levels")
   1.133 -		   else ();
   1.134 -		   (*Use OLD k: zero-cost solution; see Stickel, p 365*)
   1.135 -		   (k, np', rgd', stq) :: qs)
   1.136 -	      else prune_aux ((k,np,rgd,q)::qs, rqs)
   1.137 +              if np'+1 = np andalso rgd then
   1.138 +                  (if !trace_DEPTH_FIRST then
   1.139 +                       tracing ("Pruning " ^
   1.140 +                                string_of_int (1+length rqs) ^ " levels")
   1.141 +                   else ();
   1.142 +                   (*Use OLD k: zero-cost solution; see Stickel, p 365*)
   1.143 +                   (k, np', rgd', stq) :: qs)
   1.144 +              else prune_aux ((k,np,rgd,q)::qs, rqs)
   1.145          fun take ([], rqs) = ([], rqs)
   1.146 -	  | take (arg as ((k,np,rgd,stq)::qs, rqs)) = 
   1.147 -	        if np' < np then take (qs, (k,np,rgd,stq)::rqs)
   1.148 -		            else arg
   1.149 +          | take (arg as ((k,np,rgd,stq)::qs, rqs)) =
   1.150 +                if np' < np then take (qs, (k,np,rgd,stq)::rqs)
   1.151 +                            else arg
   1.152      in  prune_aux (take (qs, []))  end;
   1.153  
   1.154  
   1.155 @@ -140,49 +140,49 @@
   1.156    The solution sequence is redundant: the cutoff heuristic makes it impossible
   1.157    to suppress solutions arising from earlier searches, as the accumulated cost
   1.158    (k) can be wrong.*)
   1.159 -fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st => 
   1.160 +fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st =>
   1.161   let val countr = ref 0
   1.162       and tf = tracify trace_DEPTH_FIRST (tac1 1)
   1.163       and qs0 = tac0 st
   1.164       (*bnd = depth bound; inc = estimate of increment required next*)
   1.165 -     fun depth (bnd,inc) [] = 
   1.166 +     fun depth (bnd,inc) [] =
   1.167            if bnd > !iter_deepen_limit then
   1.168 -	     (tracing (string_of_int (!countr) ^ 
   1.169 -		       " inferences so far.  Giving up at " ^ string_of_int bnd);
   1.170 -	      NONE)
   1.171 +             (tracing (string_of_int (!countr) ^
   1.172 +                       " inferences so far.  Giving up at " ^ string_of_int bnd);
   1.173 +              NONE)
   1.174            else
   1.175 -	     (tracing (string_of_int (!countr) ^ 
   1.176 -		       " inferences so far.  Searching to depth " ^ 
   1.177 -		       string_of_int bnd);
   1.178 -	      (*larger increments make it run slower for the hard problems*)
   1.179 -	      depth (bnd+inc, 10)) [(0, 1, false, qs0)]
   1.180 +             (tracing (string_of_int (!countr) ^
   1.181 +                       " inferences so far.  Searching to depth " ^
   1.182 +                       string_of_int bnd);
   1.183 +              (*larger increments make it run slower for the hard problems*)
   1.184 +              depth (bnd+inc, 10)) [(0, 1, false, qs0)]
   1.185         | depth (bnd,inc) ((k,np,rgd,q)::qs) =
   1.186 -	  if k>=bnd then depth (bnd,inc) qs
   1.187 +          if k>=bnd then depth (bnd,inc) qs
   1.188            else
   1.189 -	  case (countr := !countr+1;
   1.190 -		if !trace_DEPTH_FIRST then
   1.191 -		    tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
   1.192 -		else ();
   1.193 -		Seq.pull q) of
   1.194 -	     NONE         => depth (bnd,inc) qs
   1.195 -	   | SOME(st,stq) => 
   1.196 -	       if satp st	(*solution!*)
   1.197 -	       then SOME(st, Seq.make
   1.198 -			 (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs)))
   1.199 +          case (countr := !countr+1;
   1.200 +                if !trace_DEPTH_FIRST then
   1.201 +                    tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
   1.202 +                else ();
   1.203 +                Seq.pull q) of
   1.204 +             NONE         => depth (bnd,inc) qs
   1.205 +           | SOME(st,stq) =>
   1.206 +               if satp st       (*solution!*)
   1.207 +               then SOME(st, Seq.make
   1.208 +                         (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs)))
   1.209  
   1.210 -	       else 
   1.211 +               else
   1.212                 let val np' = nprems_of st
   1.213 -		     (*rgd' calculation assumes tactic operates on subgoal 1*)
   1.214 +                     (*rgd' calculation assumes tactic operates on subgoal 1*)
   1.215                     val rgd' = not (has_vars (hd (prems_of st)))
   1.216                     val k' = k+np'-np+1  (*difference in # of subgoals, +1*)
   1.217 -               in  if k'+np' >= bnd 
   1.218 -		   then depth (bnd, Int.min(inc, k'+np'+1-bnd)) qs
   1.219 -		   else if np' < np (*solved a subgoal; prune rigid ancestors*)
   1.220 -                   then depth (bnd,inc) 
   1.221 -		         (prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs))
   1.222 -	           else depth (bnd,inc) ((k', np', rgd', tf st) :: 
   1.223 -					 (k,np,rgd,stq) :: qs)
   1.224 -	       end
   1.225 +               in  if k'+np' >= bnd
   1.226 +                   then depth (bnd, Int.min(inc, k'+np'+1-bnd)) qs
   1.227 +                   else if np' < np (*solved a subgoal; prune rigid ancestors*)
   1.228 +                   then depth (bnd,inc)
   1.229 +                         (prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs))
   1.230 +                   else depth (bnd,inc) ((k', np', rgd', tf st) ::
   1.231 +                                         (k,np,rgd,stq) :: qs)
   1.232 +               end
   1.233    in depth (0,5) [] end);
   1.234  
   1.235  val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac;
   1.236 @@ -190,16 +190,16 @@
   1.237  
   1.238  (*Simple iterative deepening tactical.  It merely "deepens" any search tactic
   1.239    using increment "inc" up to limit "lim". *)
   1.240 -fun DEEPEN (inc,lim) tacf m i = 
   1.241 -  let fun dpn m st = 
   1.242 +fun DEEPEN (inc,lim) tacf m i =
   1.243 +  let fun dpn m st =
   1.244         st |> (if has_fewer_prems i st then no_tac
   1.245 -	      else if m>lim then 
   1.246 -		       (warning "Search depth limit exceeded: giving up"; 
   1.247 -			no_tac)
   1.248 -	      else (warning ("Search depth = " ^ string_of_int m);
   1.249 -			     tacf m i  ORELSE  dpn (m+inc)))
   1.250 +              else if m>lim then
   1.251 +                       (warning "Search depth limit exceeded: giving up";
   1.252 +                        no_tac)
   1.253 +              else (warning ("Search depth = " ^ string_of_int m);
   1.254 +                             tacf m i  ORELSE  dpn (m+inc)))
   1.255    in  dpn m  end;
   1.256 - 
   1.257 +
   1.258  (*** Best-first search ***)
   1.259  
   1.260  val trace_BEST_FIRST = ref false;
   1.261 @@ -209,7 +209,7 @@
   1.262    | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
   1.263  
   1.264  (*Check for and delete duplicate proof states*)
   1.265 -fun deleteAllMin prf heap = 
   1.266 +fun deleteAllMin prf heap =
   1.267        if ThmHeap.is_empty heap then heap
   1.268        else if Thm.eq_thm (prf, #2 (ThmHeap.min heap))
   1.269        then deleteAllMin prf (ThmHeap.delete_min heap)
   1.270 @@ -218,23 +218,22 @@
   1.271  (*Best-first search for a state that satisfies satp (incl initial state)
   1.272    Function sizef estimates size of problem remaining (smaller means better).
   1.273    tactic tac0 sets up the initial priority queue, while tac1 searches it. *)
   1.274 -fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 = 
   1.275 +fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 =
   1.276    let val tac = tracify trace_BEST_FIRST tac1
   1.277        fun pairsize th = (sizef th, th);
   1.278        fun bfs (news,nprf_heap) =
   1.279 -	   (case  List.partition satp news  of
   1.280 -		([],nonsats) => next(foldr ThmHeap.insert
   1.281 -					nprf_heap (map pairsize nonsats))
   1.282 -	      | (sats,_)  => some_of_list sats)
   1.283 +           (case  List.partition satp news  of
   1.284 +                ([],nonsats) => next(fold_rev ThmHeap.insert (map pairsize nonsats) nprf_heap)
   1.285 +              | (sats,_)  => some_of_list sats)
   1.286        and next nprf_heap =
   1.287              if ThmHeap.is_empty nprf_heap then NONE
   1.288 -	    else 
   1.289 -	    let val (n,prf) = ThmHeap.min nprf_heap
   1.290 -	    in if !trace_BEST_FIRST 
   1.291 -	       then tracing("state size = " ^ string_of_int n)  
   1.292 +            else
   1.293 +            let val (n,prf) = ThmHeap.min nprf_heap
   1.294 +            in if !trace_BEST_FIRST
   1.295 +               then tracing("state size = " ^ string_of_int n)
   1.296                 else ();
   1.297 -	       bfs (Seq.list_of (tac prf), 
   1.298 -		    deleteAllMin prf (ThmHeap.delete_min nprf_heap))
   1.299 +               bfs (Seq.list_of (tac prf),
   1.300 +                    deleteAllMin prf (ThmHeap.delete_min nprf_heap))
   1.301              end
   1.302        fun btac st = bfs (Seq.list_of (tac0 st), ThmHeap.empty)
   1.303    in traced_tac btac end;
   1.304 @@ -242,32 +241,32 @@
   1.305  (*Ordinary best-first search, with no initial tactic*)
   1.306  val BEST_FIRST = THEN_BEST_FIRST all_tac;
   1.307  
   1.308 -(*Breadth-first search to satisfy satpred (including initial state) 
   1.309 +(*Breadth-first search to satisfy satpred (including initial state)
   1.310    SLOW -- SHOULD NOT USE APPEND!*)
   1.311 -fun gen_BREADTH_FIRST message satpred (tac:tactic) = 
   1.312 +fun gen_BREADTH_FIRST message satpred (tac:tactic) =
   1.313    let val tacf = Seq.list_of o tac;
   1.314        fun bfs prfs =
   1.315 -	 (case  List.partition satpred prfs  of
   1.316 -	      ([],[]) => []
   1.317 -	    | ([],nonsats) => 
   1.318 -		  (message("breadth=" ^ string_of_int(length nonsats));
   1.319 -		   bfs (maps tacf nonsats))
   1.320 -	    | (sats,_)  => sats)
   1.321 +         (case  List.partition satpred prfs  of
   1.322 +              ([],[]) => []
   1.323 +            | ([],nonsats) =>
   1.324 +                  (message("breadth=" ^ string_of_int(length nonsats));
   1.325 +                   bfs (maps tacf nonsats))
   1.326 +            | (sats,_)  => sats)
   1.327    in (fn st => Seq.of_list (bfs [st])) end;
   1.328  
   1.329  val BREADTH_FIRST = gen_BREADTH_FIRST tracing;
   1.330  val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ());
   1.331  
   1.332  
   1.333 -(*  Author: 	Norbert Voelker, FernUniversitaet Hagen
   1.334 +(*  Author:     Norbert Voelker, FernUniversitaet Hagen
   1.335      Remarks:    Implementation of A*-like proof procedure by modification
   1.336 -		of the existing code for BEST_FIRST and best_tac so that the 
   1.337 -		current level of search is taken into account.
   1.338 -*)		
   1.339 +                of the existing code for BEST_FIRST and best_tac so that the
   1.340 +                current level of search is taken into account.
   1.341 +*)
   1.342  
   1.343  (*Insertion into priority queue of states, marked with level *)
   1.344  fun insert_with_level (lnth: int*int*thm, []) = [lnth]
   1.345 -  | insert_with_level ((l,m,th), (l',n,th')::nths) = 
   1.346 +  | insert_with_level ((l,m,th), (l',n,th')::nths) =
   1.347        if  n<m then (l',n,th') :: insert_with_level ((l,m,th), nths)
   1.348        else if  n=m andalso Thm.eq_thm(th,th')
   1.349                then (l',n,th')::nths
   1.350 @@ -277,23 +276,23 @@
   1.351  fun some_of_list []     = NONE
   1.352    | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
   1.353  
   1.354 -val trace_ASTAR = ref false; 
   1.355 +val trace_ASTAR = ref false;
   1.356  
   1.357 -fun THEN_ASTAR tac0 (satp, costf) tac1 = 
   1.358 -  let val tf = tracify trace_ASTAR tac1;   
   1.359 +fun THEN_ASTAR tac0 (satp, costf) tac1 =
   1.360 +  let val tf = tracify trace_ASTAR tac1;
   1.361        fun bfs (news,nprfs,level) =
   1.362        let fun cost thm = (level, costf level thm, thm)
   1.363        in (case  List.partition satp news  of
   1.364 -            ([],nonsats) 
   1.365 -		 => next (foldr insert_with_level nprfs (map cost nonsats))
   1.366 +            ([],nonsats)
   1.367 +                 => next (List.foldr insert_with_level nprfs (map cost nonsats))
   1.368            | (sats,_)  => some_of_list sats)
   1.369 -      end and    
   1.370 +      end and
   1.371        next []  = NONE
   1.372          | next ((level,n,prf)::nprfs)  =
   1.373 -            (if !trace_ASTAR 
   1.374 +            (if !trace_ASTAR
   1.375                 then tracing("level = " ^ string_of_int level ^
   1.376 -			 "  cost = " ^ string_of_int n ^ 
   1.377 -                         "  queue length =" ^ string_of_int (length nprfs))  
   1.378 +                         "  cost = " ^ string_of_int n ^
   1.379 +                         "  queue length =" ^ string_of_int (length nprfs))
   1.380                 else ();
   1.381               bfs (Seq.list_of (tf prf), nprfs,level+1))
   1.382        fun tf st = bfs (Seq.list_of (tac0 st), [], 0)