254 minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
254 minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
255 expect = expect} |
255 expect = expect} |
256 end |
256 end |
257 |
257 |
258 fun maybe_minimize ctxt mode do_learn name |
258 fun maybe_minimize ctxt mode do_learn name |
259 (params as {debug, verbose, isar_proof, minimize, ...}) |
259 (params as {verbose, isar_proof, minimize, ...}) |
260 ({state, subgoal, subgoal_count, facts, ...} : prover_problem) |
260 ({state, subgoal, subgoal_count, facts, ...} : prover_problem) |
261 (result as {outcome, used_facts, run_time, preplay, message, |
261 (result as {outcome, used_facts, run_time, preplay, message, |
262 message_tail} : prover_result) = |
262 message_tail} : prover_result) = |
263 if is_some outcome orelse null used_facts then |
263 if is_some outcome orelse null used_facts then |
264 result |
264 result |
308 else |
308 else |
309 (SOME used_facts, (preplay, message, "")) |
309 (SOME used_facts, (preplay, message, "")) |
310 in |
310 in |
311 case used_facts of |
311 case used_facts of |
312 SOME used_facts => |
312 SOME used_facts => |
313 (if debug andalso not (null used_facts) then |
313 {outcome = NONE, used_facts = used_facts, run_time = run_time, |
314 tag_list 1 facts |
314 preplay = preplay, message = message, message_tail = message_tail} |
315 |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j)) |
|
316 |> filter_used_facts used_facts |
|
317 |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |
|
318 |> commas |
|
319 |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ |
|
320 " proof (of " ^ string_of_int (length facts) ^ "): ") "." |
|
321 |> Output.urgent_message |
|
322 else |
|
323 (); |
|
324 {outcome = NONE, used_facts = used_facts, run_time = run_time, |
|
325 preplay = preplay, message = message, message_tail = message_tail}) |
|
326 | NONE => result |
315 | NONE => result |
327 end |
316 end |
328 |
317 |
329 fun get_minimizing_prover ctxt mode do_learn name params minimize_command |
318 fun get_minimizing_prover ctxt mode do_learn name params minimize_command |
330 problem = |
319 problem = |