author  wenzelm 
Sat, 09 Apr 2016 11:34:23 +0200  
changeset 62919  9eb0359d6a77 
parent 62916  621afc4607ec 
permissions  rwrr 
23178  1 
(* Title: Pure/search.ML 
60940  2 
Author: Lawrence C Paulson 
3 
Author: Norbert Voelker, FernUniversitaet Hagen 

1588  4 

16179  5 
Search tacticals. 
1588  6 
*) 
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  10 
signature SEARCH = 
32940  11 
sig 
12 
val DEPTH_FIRST: (thm > bool) > tactic > tactic 

13 
val has_fewer_prems: int > thm > bool 

14 
val IF_UNSOLVED: tactic > tactic 

15 
val SOLVE: tactic > tactic 

16 
val THEN_MAYBE: tactic * tactic > tactic 

17 
val THEN_MAYBE': ('a > tactic) * ('a > tactic) > 'a > tactic 

18 
val DEPTH_SOLVE: tactic > tactic 

19 
val DEPTH_SOLVE_1: tactic > tactic 

38802
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8)  eliminated global ref;
wenzelm
parents:
35408
diff
changeset

20 
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

21 
val ITER_DEEPEN: int > (thm > bool) > (int > tactic) > tactic 
32940  22 
val DEEPEN: int * int > (int > int > tactic) > int > int > tactic 
23 
val THEN_BEST_FIRST: tactic > (thm > bool) * (thm > int) > tactic > tactic 

24 
val BEST_FIRST: (thm > bool) * (thm > int) > tactic > tactic 

25 
val BREADTH_FIRST: (thm > bool) > tactic > tactic 

26 
val QUIET_BREADTH_FIRST: (thm > bool) > tactic > tactic 

27 
val THEN_ASTAR: tactic > (thm > bool) * (int > thm > int) > tactic > tactic 

28 
val ASTAR: (thm > bool) * (int > thm > int) > tactic > tactic 

29 
end; 

1588  30 

32940  31 
structure Search: SEARCH = 
1588  32 
struct 
33 

34 
(**** Depthfirst search ****) 

35 

36 
(*Searches until "satp" reports proof tree as satisfied. 

37 
Suppresses duplicate solutions to minimize search space.*) 

23178  38 
fun DEPTH_FIRST satp tac = 
60940  39 
let 
40 
fun depth used [] = NONE 

41 
 depth used (q :: qs) = 

42 
(case Seq.pull q of 

43 
NONE => depth used qs 

44 
 SOME (st, stq) => 

45 
if satp st andalso not (member Thm.eq_thm used st) then 

46 
SOME (st, Seq.make (fn() => depth (st :: used) (stq :: qs))) 

47 
else depth used (tac st :: stq :: qs)); 

62916
621afc4607ec
eliminated ancient TTYbased Tactical.tracify and related global references;
wenzelm
parents:
60940
diff
changeset

48 
in fn st => Seq.make (fn () => depth [] [Seq.single st]) end; 
1588  49 

50 

51 
(*Predicate: Does the rule have fewer than n premises?*) 

59582  52 
fun has_fewer_prems n rule = Thm.nprems_of rule < n; 
1588  53 

54 
(*Apply a tactic if subgoals remain, else do nothing.*) 

55 
val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac; 

56 

5754  57 
(*Force a tactic to solve its goal completely, otherwise fail *) 
58 
fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac; 

59 

2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2143
diff
changeset

60 
(*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

61 
as before. This ensures that tac2 is only applied to an outcome of tac1.*) 
23178  62 
fun (tac1 THEN_MAYBE tac2) st = 
59582  63 
(tac1 THEN COND (has_fewer_prems (Thm.nprems_of st)) all_tac tac2) st; 
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2143
diff
changeset

64 

85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2143
diff
changeset

65 
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

66 

1588  67 
(*Tactical to reduce the number of premises by 1. 
68 
If no subgoals then it must fail! *) 

3538  69 
fun DEPTH_SOLVE_1 tac st = st > 
59582  70 
(case Thm.nprems_of st of 
71 
0 => no_tac 

72 
 n => DEPTH_FIRST (has_fewer_prems n) tac); 

1588  73 

74 
(*Uses depthfirst search to solve ALL subgoals*) 

75 
val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1); 

76 

77 

78 

2869
acee08856cc9
DEEPEN now takes an upper bound for terminating searches
paulson
parents:
2672
diff
changeset

79 
(**** Iterative deepening with pruning ****) 
1588  80 

81 
fun has_vars (Var _) = true 

60940  82 
 has_vars (Abs (_, _, t)) = has_vars t 
83 
 has_vars (f $ t) = has_vars f orelse has_vars t 

1588  84 
 has_vars _ = false; 
85 

86 
(*Counting of primitive inferences is APPROXIMATE, as the step tactic 

87 
may perform >1 inference*) 

88 

89 
(*Pruning of rigid ancestor to prevent backtracking*) 

23178  90 
fun prune (new as (k', np':int, rgd', stq), qs) = 
60940  91 
let 
92 
fun prune_aux (qs, []) = new :: qs 

93 
 prune_aux (qs, (k, np, rgd, q) :: rqs) = 

94 
if np' + 1 = np andalso rgd then 

95 
(*Use OLD k: zerocost solution; see Stickel, p 365*) 

62916
621afc4607ec
eliminated ancient TTYbased Tactical.tracify and related global references;
wenzelm
parents:
60940
diff
changeset

96 
(k, np', rgd', stq) :: qs 
60940  97 
else prune_aux ((k, np, rgd, q) :: qs, rqs) 
98 
fun take ([], rqs) = ([], rqs) 

99 
 take (arg as ((k, np, rgd, stq) :: qs, rqs)) = 

100 
if np' < np then take (qs, (k, np, rgd, stq) :: rqs) else arg; 

101 
in prune_aux (take (qs, [])) end; 

1588  102 

103 

104 
(*Depthfirst iterative deepening search for a state that satisfies satp 

105 
tactic tac0 sets up the initial goal queue, while tac1 searches it. 

106 
The solution sequence is redundant: the cutoff heuristic makes it impossible 

107 
to suppress solutions arising from earlier searches, as the accumulated cost 

108 
(k) can be wrong.*) 

62916
621afc4607ec
eliminated ancient TTYbased Tactical.tracify and related global references;
wenzelm
parents:
60940
diff
changeset

109 
fun THEN_ITER_DEEPEN lim tac0 satp tac1 st = 
60940  110 
let 
62919  111 
val counter = Unsynchronized.ref 0 
62916
621afc4607ec
eliminated ancient TTYbased Tactical.tracify and related global references;
wenzelm
parents:
60940
diff
changeset

112 
and tf = tac1 1 
60940  113 
and qs0 = tac0 st 
1588  114 
(*bnd = depth bound; inc = estimate of increment required next*) 
60940  115 
fun depth (bnd, inc) [] = 
62916
621afc4607ec
eliminated ancient TTYbased Tactical.tracify and related global references;
wenzelm
parents:
60940
diff
changeset

116 
if bnd > lim then NONE 
22025
7c5896919eb8
Introduction of a bound on DEPTH_ITER, to prevent the meson method from running forever
paulson
parents:
20852
diff
changeset

117 
else 
60940  118 
(*larger increments make it run slower for the hard problems*) 
62916
621afc4607ec
eliminated ancient TTYbased Tactical.tracify and related global references;
wenzelm
parents:
60940
diff
changeset

119 
depth (bnd + inc, 10) [(0, 1, false, qs0)] 
60940  120 
 depth (bnd, inc) ((k, np, rgd, q) :: qs) = 
121 
if k >= bnd then depth (bnd, inc) qs 

1588  122 
else 
62919  123 
(case (Unsynchronized.inc counter; Seq.pull q) of 
60940  124 
NONE => depth (bnd, inc) qs 
125 
 SOME (st, stq) => 

126 
if satp st then (*solution!*) 

127 
SOME(st, Seq.make (fn() => depth (bnd, inc) ((k, np, rgd, stq) :: qs))) 

128 
else 

129 
let 

130 
val np' = Thm.nprems_of st; 

131 
(*rgd' calculation assumes tactic operates on subgoal 1*) 

132 
val rgd' = not (has_vars (hd (Thm.prems_of st))); 

133 
val k' = k + np'  np + 1; (*difference in # of subgoals, +1*) 

134 
in 

135 
if k' + np' >= bnd then depth (bnd, Int.min (inc, k' + np' + 1  bnd)) qs 

136 
else if np' < np (*solved a subgoal; prune rigid ancestors*) 

137 
then depth (bnd, inc) (prune ((k', np', rgd', tf st), (k, np, rgd, stq) :: qs)) 

138 
else depth (bnd, inc) ((k', np', rgd', tf st) :: (k, np, rgd, stq) :: qs) 

139 
end) 

62916
621afc4607ec
eliminated ancient TTYbased Tactical.tracify and related global references;
wenzelm
parents:
60940
diff
changeset

140 
in Seq.make (fn () => depth (0, 5) []) end; 
1588  141 

38802
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8)  eliminated global ref;
wenzelm
parents:
35408
diff
changeset

142 
fun ITER_DEEPEN lim = THEN_ITER_DEEPEN lim all_tac; 
1588  143 

144 

2869
acee08856cc9
DEEPEN now takes an upper bound for terminating searches
paulson
parents:
2672
diff
changeset

145 
(*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

146 
using increment "inc" up to limit "lim". *) 
38802
a925c0ee42f7
clarified iter_deepen_limit vs meson (cf. 7c5896919eb8)  eliminated global ref;
wenzelm
parents:
35408
diff
changeset

147 
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

148 
let 
cd6023a9a922
DEEPEN: all tracing is subject to trace_DEEPEN (NB: Proof General tends to "popup" tracing output);
wenzelm
parents:
33335
diff
changeset

149 
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

150 
st > 
cd6023a9a922
DEEPEN: all tracing is subject to trace_DEEPEN (NB: Proof General tends to "popup" tracing output);
wenzelm
parents:
33335
diff
changeset

151 
(if has_fewer_prems i st then no_tac 
62916
621afc4607ec
eliminated ancient TTYbased Tactical.tracify and related global references;
wenzelm
parents:
60940
diff
changeset

152 
else if m > lim then no_tac 
621afc4607ec
eliminated ancient TTYbased Tactical.tracify and related global references;
wenzelm
parents:
60940
diff
changeset

153 
else tacf m i ORELSE dpn (m+inc)) 
2869
acee08856cc9
DEEPEN now takes an upper bound for terminating searches
paulson
parents:
2672
diff
changeset

154 
in dpn m end; 
23178  155 

32940  156 

1588  157 
(*** Bestfirst search ***) 
158 

32940  159 
(*total ordering on theorems, allowing duplicates to be found*) 
160 
structure Thm_Heap = Heap 

161 
( 

162 
type elem = int * thm; 

59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
55171
diff
changeset

163 
val ord = prod_ord int_ord (Term_Ord.term_ord o apply2 Thm.prop_of); 
32940  164 
); 
165 

1588  166 
(*For creating output sequence*) 
60940  167 
fun some_of_list [] = NONE 
168 
 some_of_list (x :: l) = SOME (x, Seq.make (fn () => some_of_list l)); 

1588  169 

9094  170 
(*Check for and delete duplicate proof states*) 
32940  171 
fun delete_all_min prf heap = 
172 
if Thm_Heap.is_empty heap then heap 

173 
else if Thm.eq_thm (prf, #2 (Thm_Heap.min heap)) 

174 
then delete_all_min prf (Thm_Heap.delete_min heap) 

175 
else heap; 

1588  176 

177 
(*Bestfirst search for a state that satisfies satp (incl initial state) 

178 
Function sizef estimates size of problem remaining (smaller means better). 

179 
tactic tac0 sets up the initial priority queue, while tac1 searches it. *) 

62916
621afc4607ec
eliminated ancient TTYbased Tactical.tracify and related global references;
wenzelm
parents:
60940
diff
changeset

180 
fun THEN_BEST_FIRST tac0 (satp, sizef) tac = 
60940  181 
let 
182 
fun pairsize th = (sizef th, th); 

183 
fun bfs (news, nprf_heap) = 

184 
(case List.partition satp news of 

185 
([], nonsats) => next (fold_rev Thm_Heap.insert (map pairsize nonsats) nprf_heap) 

186 
 (sats, _) => some_of_list sats) 

187 
and next nprf_heap = 

188 
if Thm_Heap.is_empty nprf_heap then NONE 

189 
else 

190 
let 

191 
val (n, prf) = Thm_Heap.min nprf_heap; 

192 
in 

193 
bfs (Seq.list_of (tac prf), delete_all_min prf (Thm_Heap.delete_min nprf_heap)) 

194 
end; 

195 
fun btac st = bfs (Seq.list_of (tac0 st), Thm_Heap.empty) 

62916
621afc4607ec
eliminated ancient TTYbased Tactical.tracify and related global references;
wenzelm
parents:
60940
diff
changeset

196 
in fn st => Seq.make (fn () => btac st) end; 
1588  197 

198 
(*Ordinary bestfirst search, with no initial tactic*) 

199 
val BEST_FIRST = THEN_BEST_FIRST all_tac; 

200 

23178  201 
(*Breadthfirst search to satisfy satpred (including initial state) 
1588  202 
SLOW  SHOULD NOT USE APPEND!*) 
60940  203 
fun gen_BREADTH_FIRST message satpred (tac: tactic) = 
204 
let 

205 
val tacf = Seq.list_of o tac; 

206 
fun bfs prfs = 

207 
(case List.partition satpred prfs of 

208 
([], []) => [] 

209 
 ([], nonsats) => 

210 
(message ("breadth=" ^ string_of_int (length nonsats)); 

211 
bfs (maps tacf nonsats)) 

212 
 (sats, _) => sats); 

213 
in fn st => Seq.of_list (bfs [st]) end; 

1588  214 

12262  215 
val BREADTH_FIRST = gen_BREADTH_FIRST tracing; 
5693  216 
val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ()); 
217 

1588  218 

60940  219 
(* 
220 
Implementation of A*like proof procedure by modification 

221 
of the existing code for BEST_FIRST and best_tac so that the 

222 
current level of search is taken into account. 

23178  223 
*) 
1588  224 

60940  225 
(*Insertion into priority queue of states, marked with level*) 
226 
fun insert_with_level (lnth: int * int * thm) [] = [lnth] 

227 
 insert_with_level (l, m, th) ((l', n, th') :: nths) = 

228 
if n < m then (l', n, th') :: insert_with_level (l, m, th) nths 

229 
else if n = m andalso Thm.eq_thm (th, th') then (l', n, th') :: nths 

230 
else (l, m, th) :: (l', n, th') :: nths; 

1588  231 

232 
(*For creating output sequence*) 

60940  233 
fun some_of_list [] = NONE 
234 
 some_of_list (x :: xs) = SOME (x, Seq.make (fn () => some_of_list xs)); 

1588  235 

62916
621afc4607ec
eliminated ancient TTYbased Tactical.tracify and related global references;
wenzelm
parents:
60940
diff
changeset

236 
fun THEN_ASTAR tac0 (satp, costf) tac = 
60940  237 
let 
238 
fun bfs (news, nprfs, level) = 

239 
let fun cost thm = (level, costf level thm, thm) in 

240 
(case List.partition satp news of 

241 
([], nonsats) => next (fold_rev (insert_with_level o cost) nonsats nprfs) 

242 
 (sats, _) => some_of_list sats) 

243 
end 

244 
and next [] = NONE 

62916
621afc4607ec
eliminated ancient TTYbased Tactical.tracify and related global references;
wenzelm
parents:
60940
diff
changeset

245 
 next ((level, n, prf) :: nprfs) = bfs (Seq.list_of (tac prf), nprfs, level + 1) 
621afc4607ec
eliminated ancient TTYbased Tactical.tracify and related global references;
wenzelm
parents:
60940
diff
changeset

246 
in fn st => Seq.make (fn () => bfs (Seq.list_of (tac0 st), [], 0)) end; 
1588  247 

248 
(*Ordinary ASTAR, with no initial tactic*) 

249 
val ASTAR = THEN_ASTAR all_tac; 

250 

251 
end; 

252 

253 
open Search; 