blanchet@39232
|
1 |
(* Title: HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
|
immler@31037
|
2 |
Author: Philipp Meyer, TU Muenchen
|
blanchet@36370
|
3 |
Author: Jasmin Blanchette, TU Muenchen
|
immler@31037
|
4 |
|
blanchet@41223
|
5 |
Minimization of fact list for Metis using external provers.
|
immler@31037
|
6 |
*)
|
immler@31037
|
7 |
|
blanchet@39232
|
8 |
signature SLEDGEHAMMER_MINIMIZE =
|
boehmes@32525
|
9 |
sig
|
blanchet@47168
|
10 |
type stature = ATP_Problem_Generate.stature
|
blanchet@47148
|
11 |
type play = ATP_Proof_Reconstruct.play
|
blanchet@49265
|
12 |
type mode = Sledgehammer_Provers.mode
|
blanchet@41335
|
13 |
type params = Sledgehammer_Provers.params
|
blanchet@49265
|
14 |
type prover = Sledgehammer_Provers.prover
|
blanchet@35867
|
15 |
|
blanchet@43517
|
16 |
val binary_min_facts : int Config.T
|
blanchet@49265
|
17 |
val auto_minimize_min_facts : int Config.T
|
blanchet@49265
|
18 |
val auto_minimize_max_time : real Config.T
|
blanchet@40242
|
19 |
val minimize_facts :
|
blanchet@49336
|
20 |
(thm list -> unit) -> string -> params -> bool -> int -> int -> Proof.state
|
blanchet@47168
|
21 |
-> ((string * stature) * thm list) list
|
blanchet@47168
|
22 |
-> ((string * stature) * thm list) list option
|
blanchet@44102
|
23 |
* ((unit -> play) * (play -> string) * string)
|
blanchet@49336
|
24 |
val get_minimizing_prover :
|
blanchet@49336
|
25 |
Proof.context -> mode -> (thm list -> unit) -> string -> prover
|
blanchet@39240
|
26 |
val run_minimize :
|
blanchet@49336
|
27 |
params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list
|
blanchet@49336
|
28 |
-> Proof.state -> unit
|
blanchet@35866
|
29 |
end;
|
boehmes@32525
|
30 |
|
blanchet@39232
|
31 |
structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
|
immler@31037
|
32 |
struct
|
immler@31037
|
33 |
|
blanchet@43926
|
34 |
open ATP_Util
|
blanchet@39736
|
35 |
open ATP_Proof
|
blanchet@47148
|
36 |
open ATP_Problem_Generate
|
blanchet@47148
|
37 |
open ATP_Proof_Reconstruct
|
blanchet@36140
|
38 |
open Sledgehammer_Util
|
blanchet@49265
|
39 |
open Sledgehammer_Fact
|
blanchet@41335
|
40 |
open Sledgehammer_Provers
|
nipkow@33492
|
41 |
|
blanchet@36370
|
42 |
(* wrapper for calling external prover *)
|
wenzelm@31236
|
43 |
|
blanchet@40242
|
44 |
fun n_facts names =
|
blanchet@38937
|
45 |
let val n = length names in
|
blanchet@40242
|
46 |
string_of_int n ^ " fact" ^ plural_s n ^
|
blanchet@38338
|
47 |
(if n > 0 then
|
blanchet@49100
|
48 |
": " ^ (names |> map fst |> sort string_ord |> space_implode " ")
|
blanchet@38338
|
49 |
else
|
blanchet@38338
|
50 |
"")
|
blanchet@38338
|
51 |
end
|
blanchet@38338
|
52 |
|
blanchet@41339
|
53 |
fun print silent f = if silent then () else Output.urgent_message (f ())
|
blanchet@41339
|
54 |
|
blanchet@43589
|
55 |
fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
|
blanchet@47129
|
56 |
max_new_mono_instances, type_enc, strict, lam_trans,
|
blanchet@47237
|
57 |
uncurried_aliases, isar_proof, isar_shrink_factor,
|
blanchet@47237
|
58 |
preplay_timeout, ...} : params)
|
blanchet@43905
|
59 |
silent (prover : prover) timeout i n state facts =
|
wenzelm@31236
|
60 |
let
|
blanchet@41525
|
61 |
val _ =
|
blanchet@41525
|
62 |
print silent (fn () =>
|
blanchet@41525
|
63 |
"Testing " ^ n_facts (map fst facts) ^
|
blanchet@41525
|
64 |
(if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
|
blanchet@43926
|
65 |
else "") ^ "...")
|
blanchet@42613
|
66 |
val {goal, ...} = Proof.goal state
|
blanchet@45320
|
67 |
val facts =
|
blanchet@45320
|
68 |
facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
|
blanchet@38346
|
69 |
val params =
|
blanchet@42915
|
70 |
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
|
blanchet@47129
|
71 |
provers = provers, type_enc = type_enc, strict = strict,
|
blanchet@47237
|
72 |
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
|
blanchet@49336
|
73 |
learn = false, fact_filter = NONE, max_facts = SOME (length facts),
|
blanchet@49329
|
74 |
fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
|
blanchet@43605
|
75 |
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
|
blanchet@46577
|
76 |
isar_shrink_factor = isar_shrink_factor, slice = false,
|
blanchet@46578
|
77 |
minimize = SOME false, timeout = timeout,
|
blanchet@46578
|
78 |
preplay_timeout = preplay_timeout, expect = ""}
|
blanchet@40246
|
79 |
val problem =
|
blanchet@40246
|
80 |
{state = state, goal = goal, subgoal = i, subgoal_count = n,
|
blanchet@48402
|
81 |
facts = facts}
|
blanchet@46231
|
82 |
val result as {outcome, used_facts, run_time, ...} =
|
blanchet@46391
|
83 |
prover params (K (K (K ""))) problem
|
blanchet@36223
|
84 |
in
|
blanchet@44100
|
85 |
print silent
|
blanchet@44100
|
86 |
(fn () =>
|
blanchet@44100
|
87 |
case outcome of
|
blanchet@44100
|
88 |
SOME failure => string_for_failure failure
|
blanchet@44100
|
89 |
| NONE =>
|
blanchet@44100
|
90 |
"Found proof" ^
|
blanchet@44100
|
91 |
(if length used_facts = length facts then ""
|
blanchet@46231
|
92 |
else " with " ^ n_facts used_facts) ^
|
blanchet@46231
|
93 |
" (" ^ string_from_time run_time ^ ").");
|
blanchet@38338
|
94 |
result
|
blanchet@36223
|
95 |
end
|
wenzelm@31236
|
96 |
|
blanchet@40445
|
97 |
(* minimalization of facts *)
|
wenzelm@31236
|
98 |
|
blanchet@46233
|
99 |
(* Give the external prover some slack. The ATP gets further slack because the
|
blanchet@46233
|
100 |
Sledgehammer preprocessing time is included in the estimate below but isn't
|
blanchet@46233
|
101 |
part of the timeout. *)
|
blanchet@46233
|
102 |
val slack_msecs = 200
|
blanchet@46233
|
103 |
|
blanchet@46233
|
104 |
fun new_timeout timeout run_time =
|
blanchet@46233
|
105 |
Int.min (Time.toMilliseconds timeout,
|
blanchet@46233
|
106 |
Time.toMilliseconds run_time + slack_msecs)
|
blanchet@46233
|
107 |
|> Time.fromMilliseconds
|
blanchet@46233
|
108 |
|
blanchet@46228
|
109 |
(* The linear algorithm usually outperforms the binary algorithm when over 60%
|
blanchet@46228
|
110 |
of the facts are actually needed. The binary algorithm is much more
|
blanchet@46228
|
111 |
appropriate for provers that cannot return the list of used facts and hence
|
blanchet@46228
|
112 |
returns all facts as used. Since we cannot know in advance how many facts are
|
blanchet@46228
|
113 |
actually needed, we heuristically set the threshold to 10 facts. *)
|
blanchet@43517
|
114 |
val binary_min_facts =
|
blanchet@43517
|
115 |
Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
|
blanchet@46229
|
116 |
(K 20)
|
blanchet@49265
|
117 |
val auto_minimize_min_facts =
|
blanchet@49265
|
118 |
Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
|
blanchet@49265
|
119 |
(fn generic => Config.get_generic generic binary_min_facts)
|
blanchet@49265
|
120 |
val auto_minimize_max_time =
|
blanchet@49265
|
121 |
Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
|
blanchet@49265
|
122 |
(K 5.0)
|
blanchet@41223
|
123 |
|
blanchet@46229
|
124 |
fun linear_minimize test timeout result xs =
|
blanchet@46229
|
125 |
let
|
blanchet@46229
|
126 |
fun min _ [] p = p
|
blanchet@46229
|
127 |
| min timeout (x :: xs) (seen, result) =
|
blanchet@46229
|
128 |
case test timeout (xs @ seen) of
|
blanchet@46233
|
129 |
result as {outcome = NONE, used_facts, run_time, ...}
|
blanchet@46233
|
130 |
: prover_result =>
|
blanchet@46233
|
131 |
min (new_timeout timeout run_time) (filter_used_facts used_facts xs)
|
blanchet@46233
|
132 |
(filter_used_facts used_facts seen, result)
|
blanchet@46229
|
133 |
| _ => min timeout xs (x :: seen, result)
|
blanchet@46229
|
134 |
in min timeout xs ([], result) end
|
blanchet@38249
|
135 |
|
blanchet@46229
|
136 |
fun binary_minimize test timeout result xs =
|
blanchet@41223
|
137 |
let
|
blanchet@46233
|
138 |
fun min depth (result as {run_time, ...} : prover_result) sup
|
blanchet@46233
|
139 |
(xs as _ :: _ :: _) =
|
blanchet@42614
|
140 |
let
|
blanchet@46228
|
141 |
val (l0, r0) = chop (length xs div 2) xs
|
blanchet@42614
|
142 |
(*
|
blanchet@46227
|
143 |
val _ = warning (replicate_string depth " " ^ "{ " ^
|
blanchet@46227
|
144 |
"sup: " ^ n_facts (map fst sup))
|
blanchet@46227
|
145 |
val _ = warning (replicate_string depth " " ^ " " ^
|
blanchet@46227
|
146 |
"xs: " ^ n_facts (map fst xs))
|
blanchet@46227
|
147 |
val _ = warning (replicate_string depth " " ^ " " ^
|
blanchet@46227
|
148 |
"l0: " ^ n_facts (map fst l0))
|
blanchet@46227
|
149 |
val _ = warning (replicate_string depth " " ^ " " ^
|
blanchet@46227
|
150 |
"r0: " ^ n_facts (map fst r0))
|
blanchet@42614
|
151 |
*)
|
blanchet@46228
|
152 |
val depth = depth + 1
|
blanchet@46233
|
153 |
val timeout = new_timeout timeout run_time
|
blanchet@42614
|
154 |
in
|
blanchet@46229
|
155 |
case test timeout (sup @ l0) of
|
blanchet@46233
|
156 |
result as {outcome = NONE, used_facts, ...} =>
|
blanchet@46228
|
157 |
min depth result (filter_used_facts used_facts sup)
|
blanchet@46228
|
158 |
(filter_used_facts used_facts l0)
|
blanchet@46228
|
159 |
| _ =>
|
blanchet@46229
|
160 |
case test timeout (sup @ r0) of
|
blanchet@46228
|
161 |
result as {outcome = NONE, used_facts, ...} =>
|
blanchet@46228
|
162 |
min depth result (filter_used_facts used_facts sup)
|
blanchet@46228
|
163 |
(filter_used_facts used_facts r0)
|
blanchet@46228
|
164 |
| _ =>
|
blanchet@46228
|
165 |
let
|
blanchet@46228
|
166 |
val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
|
blanchet@46228
|
167 |
val (sup, r0) =
|
blanchet@46228
|
168 |
(sup, r0) |> pairself (filter_used_facts (map fst sup_r0))
|
blanchet@46228
|
169 |
val (sup_l, (r, result)) = min depth result (sup @ l) r0
|
blanchet@46228
|
170 |
val sup = sup |> filter_used_facts (map fst sup_l)
|
blanchet@46228
|
171 |
in (sup, (l @ r, result)) end
|
blanchet@41223
|
172 |
end
|
blanchet@42614
|
173 |
(*
|
blanchet@42614
|
174 |
|> tap (fn _ => warning (replicate_string depth " " ^ "}"))
|
blanchet@42614
|
175 |
*)
|
blanchet@46228
|
176 |
| min _ result sup xs = (sup, (xs, result))
|
blanchet@46228
|
177 |
in
|
blanchet@46228
|
178 |
case snd (min 0 result [] xs) of
|
blanchet@46233
|
179 |
([x], result as {run_time, ...}) =>
|
blanchet@46233
|
180 |
(case test (new_timeout timeout run_time) [] of
|
blanchet@46228
|
181 |
result as {outcome = NONE, ...} => ([], result)
|
blanchet@46228
|
182 |
| _ => ([x], result))
|
blanchet@46228
|
183 |
| p => p
|
blanchet@46228
|
184 |
end
|
blanchet@41223
|
185 |
|
blanchet@49336
|
186 |
fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent
|
blanchet@49336
|
187 |
i n state facts =
|
wenzelm@31236
|
188 |
let
|
blanchet@41189
|
189 |
val ctxt = Proof.context_of state
|
blanchet@46445
|
190 |
val prover =
|
blanchet@46445
|
191 |
get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
|
blanchet@43899
|
192 |
val _ = print silent (fn () => "Sledgehammer minimizer: " ^
|
blanchet@41223
|
193 |
quote prover_name ^ ".")
|
blanchet@46229
|
194 |
fun test timeout = test_facts params silent prover timeout i n state
|
wenzelm@31236
|
195 |
in
|
blanchet@46229
|
196 |
(case test timeout facts of
|
blanchet@46232
|
197 |
result as {outcome = NONE, used_facts, run_time, ...} =>
|
blanchet@38249
|
198 |
let
|
blanchet@41223
|
199 |
val facts = filter_used_facts used_facts facts
|
blanchet@46233
|
200 |
val min =
|
blanchet@46229
|
201 |
if length facts >= Config.get ctxt binary_min_facts then
|
blanchet@46229
|
202 |
binary_minimize
|
blanchet@46229
|
203 |
else
|
blanchet@46229
|
204 |
linear_minimize
|
blanchet@44439
|
205 |
val (min_facts, {preplay, message, message_tail, ...}) =
|
blanchet@46232
|
206 |
min test (new_timeout timeout run_time) result facts
|
blanchet@49336
|
207 |
in
|
blanchet@49336
|
208 |
print silent (fn () => cat_lines
|
blanchet@49336
|
209 |
["Minimized to " ^ n_facts (map fst min_facts)] ^
|
blanchet@49336
|
210 |
(case min_facts |> filter (fn ((_, (sc, _)), _) => sc = Chained)
|
blanchet@49336
|
211 |
|> length of
|
blanchet@49336
|
212 |
0 => ""
|
blanchet@49336
|
213 |
| n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
|
blanchet@49336
|
214 |
(if learn then do_learn (maps snd min_facts) else ());
|
blanchet@49336
|
215 |
(SOME min_facts, (preplay, message, message_tail))
|
blanchet@49336
|
216 |
end
|
blanchet@43893
|
217 |
| {outcome = SOME TimedOut, preplay, ...} =>
|
blanchet@43893
|
218 |
(NONE,
|
blanchet@43893
|
219 |
(preplay,
|
blanchet@43893
|
220 |
fn _ => "Timeout: You can increase the time limit using the \
|
blanchet@43893
|
221 |
\\"timeout\" option (e.g., \"timeout = " ^
|
blanchet@46232
|
222 |
string_of_int (10 + Time.toMilliseconds timeout div 1000) ^
|
blanchet@46232
|
223 |
"\").",
|
blanchet@44102
|
224 |
""))
|
blanchet@43893
|
225 |
| {preplay, message, ...} =>
|
blanchet@44102
|
226 |
(NONE, (preplay, prefix "Prover error: " o message, "")))
|
blanchet@44007
|
227 |
handle ERROR msg =>
|
blanchet@46390
|
228 |
(NONE, (K (Failed_to_Play plain_metis), fn _ => "Error: " ^ msg, ""))
|
immler@31037
|
229 |
end
|
immler@31037
|
230 |
|
blanchet@49265
|
231 |
fun adjust_reconstructor_params override_params
|
blanchet@49265
|
232 |
({debug, verbose, overlord, blocking, provers, type_enc, strict,
|
blanchet@49336
|
233 |
lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
|
blanchet@49336
|
234 |
fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proof,
|
blanchet@49336
|
235 |
isar_shrink_factor, slice, minimize, timeout, preplay_timeout, expect}
|
blanchet@49336
|
236 |
: params) =
|
blanchet@49265
|
237 |
let
|
blanchet@49265
|
238 |
fun lookup_override name default_value =
|
blanchet@49265
|
239 |
case AList.lookup (op =) override_params name of
|
blanchet@49265
|
240 |
SOME [s] => SOME s
|
blanchet@49265
|
241 |
| _ => default_value
|
blanchet@49265
|
242 |
(* Only those options that reconstructors are interested in are considered
|
blanchet@49265
|
243 |
here. *)
|
blanchet@49265
|
244 |
val type_enc = lookup_override "type_enc" type_enc
|
blanchet@49265
|
245 |
val lam_trans = lookup_override "lam_trans" lam_trans
|
blanchet@49265
|
246 |
in
|
blanchet@49265
|
247 |
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
|
blanchet@49265
|
248 |
provers = provers, type_enc = type_enc, strict = strict,
|
blanchet@49265
|
249 |
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
|
blanchet@49336
|
250 |
learn = learn, fact_filter = fact_filter, max_facts = max_facts,
|
blanchet@49329
|
251 |
fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
|
blanchet@49265
|
252 |
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
|
blanchet@49265
|
253 |
isar_shrink_factor = isar_shrink_factor, slice = slice,
|
blanchet@49265
|
254 |
minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
|
blanchet@49265
|
255 |
expect = expect}
|
blanchet@49265
|
256 |
end
|
blanchet@49265
|
257 |
|
blanchet@49399
|
258 |
fun maybe_minimize ctxt mode do_learn name
|
blanchet@49409
|
259 |
(params as {verbose, isar_proof, minimize, ...})
|
blanchet@49399
|
260 |
({state, subgoal, subgoal_count, facts, ...} : prover_problem)
|
blanchet@49399
|
261 |
(result as {outcome, used_facts, run_time, preplay, message,
|
blanchet@49399
|
262 |
message_tail} : prover_result) =
|
blanchet@49265
|
263 |
if is_some outcome orelse null used_facts then
|
blanchet@49265
|
264 |
result
|
blanchet@49265
|
265 |
else
|
blanchet@49265
|
266 |
let
|
blanchet@49265
|
267 |
val num_facts = length used_facts
|
blanchet@49265
|
268 |
val ((perhaps_minimize, (minimize_name, params)), preplay) =
|
blanchet@49265
|
269 |
if mode = Normal then
|
blanchet@49265
|
270 |
if num_facts >= Config.get ctxt auto_minimize_min_facts then
|
blanchet@49265
|
271 |
((true, (name, params)), preplay)
|
blanchet@49265
|
272 |
else
|
blanchet@49265
|
273 |
let
|
blanchet@49265
|
274 |
fun can_min_fast_enough time =
|
blanchet@49265
|
275 |
0.001
|
blanchet@49265
|
276 |
* Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
|
blanchet@49265
|
277 |
<= Config.get ctxt auto_minimize_max_time
|
blanchet@49265
|
278 |
fun prover_fast_enough () = can_min_fast_enough run_time
|
blanchet@49265
|
279 |
in
|
blanchet@49265
|
280 |
if isar_proof then
|
blanchet@49265
|
281 |
((prover_fast_enough (), (name, params)), preplay)
|
blanchet@49265
|
282 |
else
|
blanchet@49265
|
283 |
let val preplay = preplay () in
|
blanchet@49265
|
284 |
(case preplay of
|
blanchet@49265
|
285 |
Played (reconstr, timeout) =>
|
blanchet@49265
|
286 |
if can_min_fast_enough timeout then
|
blanchet@49265
|
287 |
(true, extract_reconstructor params reconstr
|
blanchet@49265
|
288 |
||> (fn override_params =>
|
blanchet@49265
|
289 |
adjust_reconstructor_params
|
blanchet@49265
|
290 |
override_params params))
|
blanchet@49265
|
291 |
else
|
blanchet@49265
|
292 |
(prover_fast_enough (), (name, params))
|
blanchet@49265
|
293 |
| _ => (prover_fast_enough (), (name, params)),
|
blanchet@49265
|
294 |
K preplay)
|
blanchet@49265
|
295 |
end
|
blanchet@49265
|
296 |
end
|
blanchet@49265
|
297 |
else
|
blanchet@49265
|
298 |
((false, (name, params)), preplay)
|
blanchet@49265
|
299 |
val minimize = minimize |> the_default perhaps_minimize
|
blanchet@49265
|
300 |
val (used_facts, (preplay, message, _)) =
|
blanchet@49265
|
301 |
if minimize then
|
blanchet@49407
|
302 |
minimize_facts do_learn minimize_name params
|
blanchet@49407
|
303 |
(mode <> Normal orelse not verbose) subgoal
|
blanchet@49265
|
304 |
subgoal_count state
|
blanchet@49265
|
305 |
(filter_used_facts used_facts
|
blanchet@49265
|
306 |
(map (apsnd single o untranslated_fact) facts))
|
blanchet@49265
|
307 |
|>> Option.map (map fst)
|
blanchet@49265
|
308 |
else
|
blanchet@49265
|
309 |
(SOME used_facts, (preplay, message, ""))
|
blanchet@49265
|
310 |
in
|
blanchet@49265
|
311 |
case used_facts of
|
blanchet@49265
|
312 |
SOME used_facts =>
|
blanchet@49409
|
313 |
{outcome = NONE, used_facts = used_facts, run_time = run_time,
|
blanchet@49409
|
314 |
preplay = preplay, message = message, message_tail = message_tail}
|
blanchet@49265
|
315 |
| NONE => result
|
blanchet@49265
|
316 |
end
|
blanchet@49265
|
317 |
|
blanchet@49336
|
318 |
fun get_minimizing_prover ctxt mode do_learn name params minimize_command
|
blanchet@49336
|
319 |
problem =
|
blanchet@49265
|
320 |
get_prover ctxt mode name params minimize_command problem
|
blanchet@49399
|
321 |
|> maybe_minimize ctxt mode do_learn name params problem
|
blanchet@49265
|
322 |
|
blanchet@49336
|
323 |
fun run_minimize (params as {provers, ...}) do_learn i refs state =
|
blanchet@38291
|
324 |
let
|
blanchet@38291
|
325 |
val ctxt = Proof.context_of state
|
blanchet@38935
|
326 |
val reserved = reserved_isar_keyword_table ()
|
blanchet@49307
|
327 |
val chained_ths = #facts (Proof.goal state)
|
blanchet@49411
|
328 |
val css = clasimpset_rule_table_of ctxt
|
blanchet@40445
|
329 |
val facts =
|
blanchet@47216
|
330 |
refs |> maps (map (apsnd single)
|
blanchet@49411
|
331 |
o fact_from_ref ctxt reserved chained_ths css)
|
blanchet@38291
|
332 |
in
|
blanchet@38291
|
333 |
case subgoal_count state of
|
wenzelm@40392
|
334 |
0 => Output.urgent_message "No subgoal!"
|
blanchet@41513
|
335 |
| n => case provers of
|
blanchet@41513
|
336 |
[] => error "No prover is set."
|
blanchet@41513
|
337 |
| prover :: _ =>
|
blanchet@41513
|
338 |
(kill_provers ();
|
blanchet@49336
|
339 |
minimize_facts do_learn prover params false i n state facts
|
blanchet@44102
|
340 |
|> (fn (_, (preplay, message, message_tail)) =>
|
blanchet@44102
|
341 |
message (preplay ()) ^ message_tail
|
blanchet@44102
|
342 |
|> Output.urgent_message))
|
blanchet@38291
|
343 |
end
|
blanchet@38291
|
344 |
|
blanchet@35866
|
345 |
end;
|