57 |
57 |
58 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters, |
58 fun test_facts ({debug, verbose, overlord, provers, max_mono_iters, |
59 max_new_mono_instances, type_enc, strict, lam_trans, |
59 max_new_mono_instances, type_enc, strict, lam_trans, |
60 uncurried_aliases, isar_proofs, isar_compress, |
60 uncurried_aliases, isar_proofs, isar_compress, |
61 isar_compress_degree, merge_timeout_slack, |
61 isar_compress_degree, merge_timeout_slack, |
|
62 isar_try0, isar_minimize, |
62 preplay_timeout, preplay_trace, ...} : params) |
63 preplay_timeout, preplay_trace, ...} : params) |
63 silent (prover : prover) timeout i n state facts = |
64 silent (prover : prover) timeout i n state facts = |
64 let |
65 let |
65 val _ = |
66 val _ = |
66 print silent (fn () => |
67 print silent (fn () => |
81 fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, |
82 fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, |
82 max_new_mono_instances = max_new_mono_instances, |
83 max_new_mono_instances = max_new_mono_instances, |
83 isar_proofs = isar_proofs, isar_compress = isar_compress, |
84 isar_proofs = isar_proofs, isar_compress = isar_compress, |
84 isar_compress_degree = isar_compress_degree, |
85 isar_compress_degree = isar_compress_degree, |
85 merge_timeout_slack = merge_timeout_slack, |
86 merge_timeout_slack = merge_timeout_slack, |
|
87 isar_try0 = isar_try0, isar_minimize = isar_minimize, |
86 slice = false, minimize = SOME false, timeout = timeout, |
88 slice = false, minimize = SOME false, timeout = timeout, |
87 preplay_timeout = preplay_timeout, preplay_trace = preplay_trace, |
89 preplay_timeout = preplay_timeout, preplay_trace = preplay_trace, |
88 expect = ""} |
90 expect = ""} |
89 val problem = |
91 val problem = |
90 {state = state, goal = goal, subgoal = i, subgoal_count = n, |
92 {state = state, goal = goal, subgoal = i, subgoal_count = n, |
253 |
255 |
254 fun adjust_reconstructor_params override_params |
256 fun adjust_reconstructor_params override_params |
255 ({debug, verbose, overlord, blocking, provers, type_enc, strict, |
257 ({debug, verbose, overlord, blocking, provers, type_enc, strict, |
256 lam_trans, uncurried_aliases, learn, fact_filter, max_facts, |
258 lam_trans, uncurried_aliases, learn, fact_filter, max_facts, |
257 fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs, |
259 fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs, |
258 isar_compress, isar_compress_degree, merge_timeout_slack, slice, |
260 isar_compress, isar_compress_degree, merge_timeout_slack, isar_try0, |
|
261 isar_minimize, slice, |
259 minimize, timeout, preplay_timeout, preplay_trace, expect} : params) = |
262 minimize, timeout, preplay_timeout, preplay_trace, expect} : params) = |
260 let |
263 let |
261 fun lookup_override name default_value = |
264 fun lookup_override name default_value = |
262 case AList.lookup (op =) override_params name of |
265 case AList.lookup (op =) override_params name of |
263 SOME [s] => SOME s |
266 SOME [s] => SOME s |
272 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, |
275 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, |
273 learn = learn, fact_filter = fact_filter, max_facts = max_facts, |
276 learn = learn, fact_filter = fact_filter, max_facts = max_facts, |
274 fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, |
277 fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, |
275 max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, |
278 max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, |
276 isar_compress = isar_compress, isar_compress_degree = isar_compress_degree, |
279 isar_compress = isar_compress, isar_compress_degree = isar_compress_degree, |
277 merge_timeout_slack = merge_timeout_slack, slice = slice, |
280 merge_timeout_slack = merge_timeout_slack, |
|
281 isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = slice, |
278 minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
282 minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
279 preplay_trace = preplay_trace, expect = expect} |
283 preplay_trace = preplay_trace, expect = expect} |
280 end |
284 end |
281 |
285 |
282 fun maybe_minimize ctxt mode do_learn name |
286 fun maybe_minimize ctxt mode do_learn name |