92 ("fact_thresholds", "0.45 0.85"), |
92 ("fact_thresholds", "0.45 0.85"), |
93 ("max_mono_iters", "smart"), |
93 ("max_mono_iters", "smart"), |
94 ("max_new_mono_instances", "smart"), |
94 ("max_new_mono_instances", "smart"), |
95 ("isar_proofs", "smart"), |
95 ("isar_proofs", "smart"), |
96 ("isar_compress", "10"), |
96 ("isar_compress", "10"), |
97 ("isar_compress_degree", "2"), (* TODO: document *) |
|
98 ("isar_try0", "true"), (* TODO: document *) |
97 ("isar_try0", "true"), (* TODO: document *) |
99 ("isar_minimize", "true"), (* TODO: document *) |
98 ("isar_minimize", "true"), (* TODO: document *) |
100 ("slice", "true"), |
99 ("slice", "true"), |
101 ("minimize", "smart"), |
100 ("minimize", "smart"), |
102 ("preplay_timeout", "3")] |
101 ("preplay_timeout", "3")] |
302 val max_mono_iters = lookup_option lookup_int "max_mono_iters" |
301 val max_mono_iters = lookup_option lookup_int "max_mono_iters" |
303 val max_new_mono_instances = |
302 val max_new_mono_instances = |
304 lookup_option lookup_int "max_new_mono_instances" |
303 lookup_option lookup_int "max_new_mono_instances" |
305 val isar_proofs = lookup_option lookup_bool "isar_proofs" |
304 val isar_proofs = lookup_option lookup_bool "isar_proofs" |
306 val isar_compress = Real.max (1.0, lookup_real "isar_compress") |
305 val isar_compress = Real.max (1.0, lookup_real "isar_compress") |
307 val isar_compress_degree = Int.max (1, lookup_int "isar_compress_degree") |
|
308 val isar_try0 = lookup_bool "isar_try0" |
306 val isar_try0 = lookup_bool "isar_try0" |
309 val isar_minimize = lookup_bool "isar_minimize" |
307 val isar_minimize = lookup_bool "isar_minimize" |
310 val slice = mode <> Auto_Try andalso lookup_bool "slice" |
308 val slice = mode <> Auto_Try andalso lookup_bool "slice" |
311 val minimize = |
309 val minimize = |
312 if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize" |
310 if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize" |
320 provers = provers, type_enc = type_enc, strict = strict, |
318 provers = provers, type_enc = type_enc, strict = strict, |
321 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, |
319 lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, |
322 learn = learn, fact_filter = fact_filter, max_facts = max_facts, |
320 learn = learn, fact_filter = fact_filter, max_facts = max_facts, |
323 fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, |
321 fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters, |
324 max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, |
322 max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs, |
325 isar_compress = isar_compress, isar_compress_degree = isar_compress_degree, |
323 isar_compress = isar_compress, isar_try0 = isar_try0, |
326 isar_try0 = isar_try0, isar_minimize = isar_minimize, slice = slice, |
324 isar_minimize = isar_minimize, slice = slice, minimize = minimize, |
327 minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
325 timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} |
328 expect = expect} |
|
329 end |
326 end |
330 |
327 |
331 fun get_params mode = extract_params mode o default_raw_params |
328 fun get_params mode = extract_params mode o default_raw_params |
332 fun default_params thy = get_params Normal thy o map (apsnd single) |
329 fun default_params thy = get_params Normal thy o map (apsnd single) |
333 |
330 |