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