121 ("dont_minimize", "minimize"), |
121 ("dont_minimize", "minimize"), |
122 ("dont_try0_isar", "isar_try0"), |
122 ("dont_try0_isar", "isar_try0"), |
123 ("dont_minimize_isar", "isar_minimize"), |
123 ("dont_minimize_isar", "isar_minimize"), |
124 ("no_preplay_trace", "preplay_trace")] (* TODO: document *) |
124 ("no_preplay_trace", "preplay_trace")] (* TODO: document *) |
125 |
125 |
126 val params_for_minimize = |
126 val params_not_for_minimize = |
127 ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans", |
127 ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", |
128 "uncurried_aliases", "max_mono_iters", "max_new_mono_instances", |
128 "minimize"]; |
129 "learn", "isar_proofs", "isar_compress", "timeout", "preplay_timeout"] |
|
130 (* TODO: add isar_compress_degree, merge_timeout_slack, preplay_trace, |
|
131 isar_try0, isar_minimize? *) |
|
132 |
129 |
133 val property_dependent_params = ["provers", "timeout"] |
130 val property_dependent_params = ["provers", "timeout"] |
134 |
131 |
135 fun is_known_raw_param s = |
132 fun is_known_raw_param s = |
136 AList.defined (op =) default_default_params s orelse |
133 AList.defined (op =) default_default_params s orelse |
343 (* Sledgehammer the given subgoal *) |
340 (* Sledgehammer the given subgoal *) |
344 |
341 |
345 val default_minimize_prover = metisN |
342 val default_minimize_prover = metisN |
346 |
343 |
347 fun is_raw_param_relevant_for_minimize (name, _) = |
344 fun is_raw_param_relevant_for_minimize (name, _) = |
348 member (op =) params_for_minimize name |
345 not (member (op =) params_not_for_minimize name) |
349 fun string_of_raw_param (key, values) = |
346 fun string_of_raw_param (key, values) = |
350 key ^ (case implode_param values of "" => "" | value => " = " ^ value) |
347 key ^ (case implode_param values of "" => "" | value => " = " ^ value) |
351 fun nice_string_of_raw_param (p as (key, ["false"])) = |
348 fun nice_string_of_raw_param (p as (key, ["false"])) = |
352 (case AList.find (op =) negated_alias_params key of |
349 (case AList.find (op =) negated_alias_params key of |
353 [neg] => neg |
350 [neg] => neg |