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