80 ("overlord", "false"), |
80 ("overlord", "false"), |
81 ("blocking", "false"), |
81 ("blocking", "false"), |
82 ("type_sys", "smart"), |
82 ("type_sys", "smart"), |
83 ("relevance_thresholds", "0.45 0.85"), |
83 ("relevance_thresholds", "0.45 0.85"), |
84 ("max_relevant", "smart"), |
84 ("max_relevant", "smart"), |
85 ("max_mono_iters", "4"), |
85 ("max_mono_iters", "5"), |
86 ("max_mono_instances", "500"), |
86 ("max_new_mono_instances", "250"), |
87 ("explicit_apply", "false"), |
87 ("explicit_apply", "false"), |
88 ("isar_proof", "false"), |
88 ("isar_proof", "false"), |
89 ("isar_shrink_factor", "1"), |
89 ("isar_shrink_factor", "1"), |
90 ("slicing", "true")] |
90 ("slicing", "true")] |
91 |
91 |
103 ("no_isar_proof", "isar_proof"), |
103 ("no_isar_proof", "isar_proof"), |
104 ("no_slicing", "slicing")] |
104 ("no_slicing", "slicing")] |
105 |
105 |
106 val params_for_minimize = |
106 val params_for_minimize = |
107 ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters", |
107 ["debug", "verbose", "overlord", "type_sys", "full_types", "max_mono_iters", |
108 "max_mono_instances", "isar_proof", "isar_shrink_factor", "timeout"] |
108 "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout"] |
109 |
109 |
110 val property_dependent_params = ["provers", "full_types", "timeout"] |
110 val property_dependent_params = ["provers", "full_types", "timeout"] |
111 |
111 |
112 fun is_known_raw_param s = |
112 fun is_known_raw_param s = |
113 AList.defined (op =) default_default_params s orelse |
113 AList.defined (op =) default_default_params s orelse |
247 "smart" => Smart_Type_Sys (lookup_bool "full_types") |
247 "smart" => Smart_Type_Sys (lookup_bool "full_types") |
248 | s => Dumb_Type_Sys (type_sys_from_string s) |
248 | s => Dumb_Type_Sys (type_sys_from_string s) |
249 val relevance_thresholds = lookup_real_pair "relevance_thresholds" |
249 val relevance_thresholds = lookup_real_pair "relevance_thresholds" |
250 val max_relevant = lookup_int_option "max_relevant" |
250 val max_relevant = lookup_int_option "max_relevant" |
251 val max_mono_iters = lookup_int "max_mono_iters" |
251 val max_mono_iters = lookup_int "max_mono_iters" |
252 val max_mono_instances = lookup_int "max_mono_instances" |
252 val max_new_mono_instances = lookup_int "max_new_mono_instances" |
253 val explicit_apply = lookup_bool "explicit_apply" |
253 val explicit_apply = lookup_bool "explicit_apply" |
254 val isar_proof = lookup_bool "isar_proof" |
254 val isar_proof = lookup_bool "isar_proof" |
255 val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") |
255 val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") |
256 val slicing = not auto andalso lookup_bool "slicing" |
256 val slicing = not auto andalso lookup_bool "slicing" |
257 val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout |
257 val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout |
258 val expect = lookup_string "expect" |
258 val expect = lookup_string "expect" |
259 in |
259 in |
260 {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, |
260 {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, |
261 provers = provers, relevance_thresholds = relevance_thresholds, |
261 provers = provers, relevance_thresholds = relevance_thresholds, |
262 max_relevant = max_relevant, max_mono_iters = max_mono_iters, |
262 max_relevant = max_relevant, max_mono_iters = max_mono_iters, |
263 max_mono_instances = max_mono_instances, type_sys = type_sys, |
263 max_new_mono_instances = max_new_mono_instances, type_sys = type_sys, |
264 explicit_apply = explicit_apply, isar_proof = isar_proof, |
264 explicit_apply = explicit_apply, isar_proof = isar_proof, |
265 isar_shrink_factor = isar_shrink_factor, slicing = slicing, |
265 isar_shrink_factor = isar_shrink_factor, slicing = slicing, |
266 timeout = timeout, expect = expect} |
266 timeout = timeout, expect = expect} |
267 end |
267 end |
268 |
268 |