82 ("blocking", "false"), |
82 ("blocking", "false"), |
83 ("type_enc", "smart"), |
83 ("type_enc", "smart"), |
84 ("strict", "false"), |
84 ("strict", "false"), |
85 ("lam_trans", "smart"), |
85 ("lam_trans", "smart"), |
86 ("uncurried_aliases", "smart"), |
86 ("uncurried_aliases", "smart"), |
|
87 ("fact_filter", "smart"), |
|
88 ("max_facts", "smart"), |
87 ("fact_thresholds", "0.45 0.85"), |
89 ("fact_thresholds", "0.45 0.85"), |
88 ("max_facts", "smart"), |
|
89 ("max_mono_iters", "smart"), |
90 ("max_mono_iters", "smart"), |
90 ("max_new_mono_instances", "smart"), |
91 ("max_new_mono_instances", "smart"), |
91 ("isar_proof", "false"), |
92 ("isar_proof", "false"), |
92 ("isar_shrink_factor", "1"), |
93 ("isar_shrink_factor", "1"), |
93 ("slice", "true"), |
94 ("slice", "true"), |
145 | _ => value) |
146 | _ => value) |
146 | NONE => (name, value) |
147 | NONE => (name, value) |
147 |
148 |
148 val any_type_enc = type_enc_from_string Strict "erased" |
149 val any_type_enc = type_enc_from_string Strict "erased" |
149 |
150 |
150 (* "provers =", "type_enc =", and "lam_trans" can be omitted. For the last two, |
151 (* "provers =", "type_enc =", "lam_trans =", and "fact_filter =" can be omitted. |
151 this is a secret feature. *) |
152 For the last three, this is a secret feature. *) |
152 fun normalize_raw_param ctxt = |
153 fun normalize_raw_param ctxt = |
153 unalias_raw_param |
154 unalias_raw_param |
154 #> (fn (name, value) => |
155 #> (fn (name, value) => |
155 if is_known_raw_param name then |
156 if is_known_raw_param name then |
156 (name, value) |
157 (name, value) |
159 else if can (type_enc_from_string Strict) name andalso null value then |
160 else if can (type_enc_from_string Strict) name andalso null value then |
160 ("type_enc", [name]) |
161 ("type_enc", [name]) |
161 else if can (trans_lams_from_string ctxt any_type_enc) name andalso |
162 else if can (trans_lams_from_string ctxt any_type_enc) name andalso |
162 null value then |
163 null value then |
163 ("lam_trans", [name]) |
164 ("lam_trans", [name]) |
|
165 else if member (op =) fact_filters name then |
|
166 ("fact_filter", [name]) |
164 else |
167 else |
165 error ("Unknown parameter: " ^ quote name ^ ".")) |
168 error ("Unknown parameter: " ^ quote name ^ ".")) |
166 |
169 |
167 |
170 |
168 (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are |
171 (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are |
289 "smart" => NONE |
292 "smart" => NONE |
290 | s => (type_enc_from_string Strict s; SOME s) |
293 | s => (type_enc_from_string Strict s; SOME s) |
291 val strict = mode = Auto_Try orelse lookup_bool "strict" |
294 val strict = mode = Auto_Try orelse lookup_bool "strict" |
292 val lam_trans = lookup_option lookup_string "lam_trans" |
295 val lam_trans = lookup_option lookup_string "lam_trans" |
293 val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" |
296 val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases" |
|
297 val fact_filter = lookup_option lookup_string "fact_filter" |
|
298 val max_facts = lookup_option lookup_int "max_facts" |
294 val fact_thresholds = lookup_real_pair "fact_thresholds" |
299 val fact_thresholds = lookup_real_pair "fact_thresholds" |
295 val max_facts = lookup_option lookup_int "max_facts" |
|
296 val max_mono_iters = lookup_option lookup_int "max_mono_iters" |
300 val max_mono_iters = lookup_option lookup_int "max_mono_iters" |
297 val max_new_mono_instances = |
301 val max_new_mono_instances = |
298 lookup_option lookup_int "max_new_mono_instances" |
302 lookup_option lookup_int "max_new_mono_instances" |
299 val isar_proof = lookup_bool "isar_proof" |
303 val isar_proof = lookup_bool "isar_proof" |
300 val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") |
304 val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") |
309 val expect = lookup_string "expect" |
313 val expect = lookup_string "expect" |
310 in |
314 in |
311 {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, |
315 {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, |
312 provers = provers, type_enc = type_enc, strict = strict, |
316 provers = provers, type_enc = type_enc, strict = strict, |
313 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, |
317 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, |
314 fact_thresholds = fact_thresholds, max_facts = max_facts, |
318 fact_filter = fact_filter, max_facts = max_facts, |
315 max_mono_iters = max_mono_iters, |
319 fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, |
316 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
320 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
317 isar_shrink_factor = isar_shrink_factor, slice = slice, |
321 isar_shrink_factor = isar_shrink_factor, slice = slice, |
318 minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
322 minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
319 expect = expect} |
323 expect = expect} |
320 end |
324 end |