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