66 type prover_problem = |
66 type prover_problem = |
67 {state : Proof.state, |
67 {state : Proof.state, |
68 goal : thm, |
68 goal : thm, |
69 subgoal : int, |
69 subgoal : int, |
70 subgoal_count : int, |
70 subgoal_count : int, |
71 fact_triple : fact list * fact list * fact list} |
71 factss : (string * fact list) list} |
72 |
72 |
73 type prover_result = |
73 type prover_result = |
74 {outcome : failure option, |
74 {outcome : failure option, |
75 used_facts : (string * stature) list, |
75 used_facts : (string * stature) list, |
76 used_from : fact list, |
76 used_from : fact list, |
353 type prover_problem = |
353 type prover_problem = |
354 {state : Proof.state, |
354 {state : Proof.state, |
355 goal : thm, |
355 goal : thm, |
356 subgoal : int, |
356 subgoal : int, |
357 subgoal_count : int, |
357 subgoal_count : int, |
358 fact_triple : fact list * fact list * fact list} |
358 factss : (string * fact list) list} |
359 |
359 |
360 type prover_result = |
360 type prover_result = |
361 {outcome : failure option, |
361 {outcome : failure option, |
362 used_facts : (string * stature) list, |
362 used_facts : (string * stature) list, |
363 used_from : fact list, |
363 used_from : fact list, |
630 (params as {debug, verbose, overlord, type_enc, strict, lam_trans, |
630 (params as {debug, verbose, overlord, type_enc, strict, lam_trans, |
631 uncurried_aliases, max_facts, max_mono_iters, |
631 uncurried_aliases, max_facts, max_mono_iters, |
632 max_new_mono_instances, isar_proofs, isar_shrink, |
632 max_new_mono_instances, isar_proofs, isar_shrink, |
633 slice, timeout, preplay_timeout, ...}) |
633 slice, timeout, preplay_timeout, ...}) |
634 minimize_command |
634 minimize_command |
635 ({state, goal, subgoal, subgoal_count, fact_triple = (facts, _, _), (* FIXME *) |
635 ({state, goal, subgoal, subgoal_count, factss = (_, facts) :: _, (* FIXME *) |
636 ...} : prover_problem) = |
636 ...} : prover_problem) = |
637 let |
637 let |
638 val thy = Proof.theory_of state |
638 val thy = Proof.theory_of state |
639 val ctxt = Proof.context_of state |
639 val ctxt = Proof.context_of state |
640 val atp_mode = |
640 val atp_mode = |
1062 end |
1062 end |
1063 in do_slice timeout 1 NONE Time.zeroTime end |
1063 in do_slice timeout 1 NONE Time.zeroTime end |
1064 |
1064 |
1065 fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) |
1065 fun run_smt_solver mode name (params as {debug, verbose, preplay_timeout, ...}) |
1066 minimize_command |
1066 minimize_command |
1067 ({state, goal, subgoal, subgoal_count, fact_triple = (facts, _, _), (* FIXME *) |
1067 ({state, goal, subgoal, subgoal_count, factss = (_, facts) :: _, (* FIXME *) |
1068 ...} : prover_problem) = |
1068 ...} : prover_problem) = |
1069 let |
1069 let |
1070 val ctxt = Proof.context_of state |
1070 val ctxt = Proof.context_of state |
1071 val num_facts = length facts |
1071 val num_facts = length facts |
1072 val facts = |
1072 val facts = |
1106 end |
1106 end |
1107 |
1107 |
1108 fun run_reconstructor mode name |
1108 fun run_reconstructor mode name |
1109 (params as {debug, verbose, timeout, type_enc, lam_trans, ...}) |
1109 (params as {debug, verbose, timeout, type_enc, lam_trans, ...}) |
1110 minimize_command |
1110 minimize_command |
1111 ({state, subgoal, subgoal_count, fact_triple = (facts, _, _), ...} |
1111 ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} |
1112 : prover_problem) = |
1112 : prover_problem) = |
1113 let |
1113 let |
1114 val reconstr = |
1114 val reconstr = |
1115 if name = metisN then |
1115 if name = metisN then |
1116 Metis (type_enc |> the_default (hd partial_type_encs), |
1116 Metis (type_enc |> the_default (hd partial_type_encs), |