32 max_facts : int option, |
32 max_facts : int option, |
33 fact_thresholds : real * real, |
33 fact_thresholds : real * real, |
34 max_mono_iters : int option, |
34 max_mono_iters : int option, |
35 max_new_mono_instances : int option, |
35 max_new_mono_instances : int option, |
36 isar_proofs : bool, |
36 isar_proofs : bool, |
37 isar_shrinkage : real, |
37 isar_shrink : real, |
38 slice : bool, |
38 slice : bool, |
39 minimize : bool option, |
39 minimize : bool option, |
40 timeout : Time.time, |
40 timeout : Time.time, |
41 preplay_timeout : Time.time, |
41 preplay_timeout : Time.time, |
42 expect : string} |
42 expect : string} |
325 max_facts : int option, |
325 max_facts : int option, |
326 fact_thresholds : real * real, |
326 fact_thresholds : real * real, |
327 max_mono_iters : int option, |
327 max_mono_iters : int option, |
328 max_new_mono_instances : int option, |
328 max_new_mono_instances : int option, |
329 isar_proofs : bool, |
329 isar_proofs : bool, |
330 isar_shrinkage : real, |
330 isar_shrink : real, |
331 slice : bool, |
331 slice : bool, |
332 minimize : bool option, |
332 minimize : bool option, |
333 timeout : Time.time, |
333 timeout : Time.time, |
334 preplay_timeout : Time.time, |
334 preplay_timeout : Time.time, |
335 expect : string} |
335 expect : string} |
640 fun run_atp mode name |
640 fun run_atp mode name |
641 ({exec, arguments, proof_delims, known_failures, prem_role, best_slices, |
641 ({exec, arguments, proof_delims, known_failures, prem_role, best_slices, |
642 best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config) |
642 best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config) |
643 (params as {debug, verbose, overlord, type_enc, strict, lam_trans, |
643 (params as {debug, verbose, overlord, type_enc, strict, lam_trans, |
644 uncurried_aliases, max_facts, max_mono_iters, |
644 uncurried_aliases, max_facts, max_mono_iters, |
645 max_new_mono_instances, isar_proofs, isar_shrinkage, |
645 max_new_mono_instances, isar_proofs, isar_shrink, |
646 slice, timeout, preplay_timeout, ...}) |
646 slice, timeout, preplay_timeout, ...}) |
647 minimize_command |
647 minimize_command |
648 ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) = |
648 ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) = |
649 let |
649 let |
650 val thy = Proof.theory_of state |
650 val thy = Proof.theory_of state |
886 if verbose then |
886 if verbose then |
887 Output.urgent_message "Generating proof text..." |
887 Output.urgent_message "Generating proof text..." |
888 else |
888 else |
889 () |
889 () |
890 val isar_params = |
890 val isar_params = |
891 (debug, verbose, preplay_timeout, isar_shrinkage, |
891 (debug, verbose, preplay_timeout, isar_shrink, |
892 pool, fact_names, sym_tab, atp_proof, goal) |
892 pool, fact_names, sym_tab, atp_proof, goal) |
893 val one_line_params = |
893 val one_line_params = |
894 (preplay, proof_banner mode name, used_facts, |
894 (preplay, proof_banner mode name, used_facts, |
895 choose_minimize_command params minimize_command name preplay, |
895 choose_minimize_command params minimize_command name preplay, |
896 subgoal, subgoal_count) |
896 subgoal, subgoal_count) |