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