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