73 (K 5.0) |
73 (K 5.0) |
74 |
74 |
75 fun adjust_reconstructor_params override_params |
75 fun adjust_reconstructor_params override_params |
76 ({debug, verbose, overlord, blocking, provers, type_enc, sound, |
76 ({debug, verbose, overlord, blocking, provers, type_enc, sound, |
77 lam_trans, relevance_thresholds, max_relevant, max_mono_iters, |
77 lam_trans, relevance_thresholds, max_relevant, max_mono_iters, |
78 max_new_mono_instances, isar_proof, isar_shrink_factor, slice, timeout, |
78 max_new_mono_instances, isar_proof, isar_shrink_factor, slice, |
79 preplay_timeout, expect} : params) = |
79 minimize, timeout, preplay_timeout, expect} : params) = |
80 let |
80 let |
81 fun lookup_override name default_value = |
81 fun lookup_override name default_value = |
82 case AList.lookup (op =) override_params name of |
82 case AList.lookup (op =) override_params name of |
83 SOME [s] => SOME s |
83 SOME [s] => SOME s |
84 | _ => default_value |
84 | _ => default_value |
91 provers = provers, type_enc = type_enc, sound = sound, |
91 provers = provers, type_enc = type_enc, sound = sound, |
92 lam_trans = lam_trans, max_relevant = max_relevant, |
92 lam_trans = lam_trans, max_relevant = max_relevant, |
93 relevance_thresholds = relevance_thresholds, |
93 relevance_thresholds = relevance_thresholds, |
94 max_mono_iters = max_mono_iters, |
94 max_mono_iters = max_mono_iters, |
95 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
95 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
96 isar_shrink_factor = isar_shrink_factor, slice = slice, timeout = timeout, |
96 isar_shrink_factor = isar_shrink_factor, slice = slice, |
97 preplay_timeout = preplay_timeout, expect = expect} |
97 minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
|
98 expect = expect} |
98 end |
99 end |
99 |
100 |
100 fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...}) |
101 fun minimize ctxt mode name |
|
102 (params as {debug, verbose, isar_proof, minimize, ...}) |
101 ({state, subgoal, subgoal_count, facts, ...} : prover_problem) |
103 ({state, subgoal, subgoal_count, facts, ...} : prover_problem) |
102 (result as {outcome, used_facts, run_time, preplay, message, |
104 (result as {outcome, used_facts, run_time, preplay, message, |
103 message_tail} : prover_result) = |
105 message_tail} : prover_result) = |
104 if is_some outcome orelse null used_facts then |
106 if is_some outcome orelse null used_facts then |
105 result |
107 result |
106 else |
108 else |
107 let |
109 let |
108 val num_facts = length used_facts |
110 val num_facts = length used_facts |
109 val ((minimize, (minimize_name, params)), preplay) = |
111 val ((perhaps_minimize, (minimize_name, params)), preplay) = |
110 if mode = Normal then |
112 if mode = Normal then |
111 if num_facts >= Config.get ctxt auto_minimize_min_facts then |
113 if num_facts >= Config.get ctxt auto_minimize_min_facts then |
112 ((true, (name, params)), preplay) |
114 ((true, (name, params)), preplay) |
113 else |
115 else |
114 let |
116 let |
115 fun can_min_fast_enough time = |
117 fun can_min_fast_enough time = |
116 0.001 |
118 0.001 |
117 * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time) |
119 * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time) |
118 <= Config.get ctxt auto_minimize_max_time |
120 <= Config.get ctxt auto_minimize_max_time |
119 val prover_fast_enough = can_min_fast_enough run_time |
121 fun prover_fast_enough () = can_min_fast_enough run_time |
120 in |
122 in |
121 if isar_proof then |
123 if isar_proof then |
122 ((prover_fast_enough, (name, params)), preplay) |
124 ((prover_fast_enough (), (name, params)), preplay) |
123 else |
125 else |
124 let val preplay = preplay () in |
126 let val preplay = preplay () in |
125 (case preplay of |
127 (case preplay of |
126 Played (reconstr, timeout) => |
128 Played (reconstr, timeout) => |
127 if can_min_fast_enough timeout then |
129 if can_min_fast_enough timeout then |
128 (true, extract_reconstructor params reconstr |
130 (true, extract_reconstructor params reconstr |
129 ||> (fn override_params => |
131 ||> (fn override_params => |
130 adjust_reconstructor_params |
132 adjust_reconstructor_params |
131 override_params params)) |
133 override_params params)) |
132 else |
134 else |
133 (prover_fast_enough, (name, params)) |
135 (prover_fast_enough (), (name, params)) |
134 | _ => (prover_fast_enough, (name, params)), |
136 | _ => (prover_fast_enough (), (name, params)), |
135 K preplay) |
137 K preplay) |
136 end |
138 end |
137 end |
139 end |
138 else |
140 else |
139 ((false, (name, params)), preplay) |
141 ((false, (name, params)), preplay) |
|
142 val minimize = minimize |> the_default perhaps_minimize |
140 val (used_facts, (preplay, message, _)) = |
143 val (used_facts, (preplay, message, _)) = |
141 if minimize then |
144 if minimize then |
142 minimize_facts minimize_name params (not verbose) subgoal |
145 minimize_facts minimize_name params (not verbose) subgoal |
143 subgoal_count state |
146 subgoal_count state |
144 (filter_used_facts used_facts |
147 (filter_used_facts used_facts |