118 ("dont_slice", "slice"), |
118 ("dont_slice", "slice"), |
119 ("dont_minimize", "minimize"), |
119 ("dont_minimize", "minimize"), |
120 ("dont_try0_isar", "isar_try0")] |
120 ("dont_try0_isar", "isar_try0")] |
121 |
121 |
122 val params_not_for_minimize = |
122 val params_not_for_minimize = |
123 ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", |
123 ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"]; |
124 "minimize"]; |
|
125 |
124 |
126 val property_dependent_params = ["provers", "timeout"] |
125 val property_dependent_params = ["provers", "timeout"] |
127 |
126 |
128 fun is_known_raw_param s = |
127 fun is_known_raw_param s = |
129 AList.defined (op =) default_default_params s orelse |
128 AList.defined (op =) default_default_params s orelse |
223 let |
222 let |
224 val raw_params = rev override_params @ rev default_params |
223 val raw_params = rev override_params @ rev default_params |
225 val lookup = Option.map implode_param o AList.lookup (op =) raw_params |
224 val lookup = Option.map implode_param o AList.lookup (op =) raw_params |
226 val lookup_string = the_default "" o lookup |
225 val lookup_string = the_default "" o lookup |
227 fun general_lookup_bool option default_value name = |
226 fun general_lookup_bool option default_value name = |
228 case lookup name of |
227 (case lookup name of |
229 SOME s => parse_bool_option option name s |
228 SOME s => parse_bool_option option name s |
230 | NONE => default_value |
229 | NONE => default_value) |
231 val lookup_bool = the o general_lookup_bool false (SOME false) |
230 val lookup_bool = the o general_lookup_bool false (SOME false) |
232 fun lookup_time name = |
231 fun lookup_time name = |
233 case lookup name of |
232 (case lookup name of |
234 SOME s => parse_time_option name s |
233 SOME s => parse_time name s |
235 | NONE => NONE |
234 | NONE => Time.zeroTime) |
236 fun lookup_int name = |
235 fun lookup_int name = |
237 case lookup name of |
236 (case lookup name of |
238 NONE => 0 |
237 NONE => 0 |
239 | SOME s => case Int.fromString s of |
238 | SOME s => |
240 SOME n => n |
239 (case Int.fromString s of |
241 | NONE => error ("Parameter " ^ quote name ^ |
240 SOME n => n |
242 " must be assigned an integer value.") |
241 | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value."))) |
243 fun lookup_real name = |
242 fun lookup_real name = |
244 case lookup name of |
243 (case lookup name of |
245 NONE => 0.0 |
244 NONE => 0.0 |
246 | SOME s => case Real.fromString s of |
245 | SOME s => |
247 SOME n => n |
246 (case Real.fromString s of |
248 | NONE => error ("Parameter " ^ quote name ^ |
247 SOME n => n |
249 " must be assigned a real value.") |
248 | NONE => error ("Parameter " ^ quote name ^ " must be assigned a real value."))) |
250 fun lookup_real_pair name = |
249 fun lookup_real_pair name = |
251 case lookup name of |
250 (case lookup name of |
252 NONE => (0.0, 0.0) |
251 NONE => (0.0, 0.0) |
253 | SOME s => case s |> space_explode " " |> map Real.fromString of |
252 | SOME s => |
254 [SOME r1, SOME r2] => (r1, r2) |
253 (case s |> space_explode " " |> map Real.fromString of |
255 | _ => error ("Parameter " ^ quote name ^ |
254 [SOME r1, SOME r2] => (r1, r2) |
256 " must be assigned a pair of floating-point \ |
255 | _ => error ("Parameter " ^ quote name ^ " must be assigned a pair of floating-point \ |
257 \values (e.g., \"0.6 0.95\")") |
256 \values (e.g., \"0.6 0.95\")"))) |
258 fun lookup_option lookup' name = |
257 fun lookup_option lookup' name = |
259 case lookup name of |
258 (case lookup name of |
260 SOME "smart" => NONE |
259 SOME "smart" => NONE |
261 | _ => SOME (lookup' name) |
260 | _ => SOME (lookup' name)) |
262 val debug = mode <> Auto_Try andalso lookup_bool "debug" |
261 val debug = mode <> Auto_Try andalso lookup_bool "debug" |
263 val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") |
262 val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose") |
264 val overlord = lookup_bool "overlord" |
263 val overlord = lookup_bool "overlord" |
265 val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" |
264 val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" |
266 val blocking = |
265 val blocking = |
289 val isar_proofs = lookup_option lookup_bool "isar_proofs" |
288 val isar_proofs = lookup_option lookup_bool "isar_proofs" |
290 val isar_compress = Real.max (1.0, lookup_real "isar_compress") |
289 val isar_compress = Real.max (1.0, lookup_real "isar_compress") |
291 val isar_try0 = lookup_bool "isar_try0" |
290 val isar_try0 = lookup_bool "isar_try0" |
292 val slice = mode <> Auto_Try andalso lookup_bool "slice" |
291 val slice = mode <> Auto_Try andalso lookup_bool "slice" |
293 val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize" |
292 val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize" |
294 val timeout = if mode = Auto_Try then NONE else lookup_time "timeout" |
293 val timeout = lookup_time "timeout" |
295 val preplay_timeout = |
294 val preplay_timeout = if mode = Auto_Try then Time.zeroTime else lookup_time "preplay_timeout" |
296 if mode = Auto_Try then SOME Time.zeroTime else lookup_time "preplay_timeout" |
|
297 val expect = lookup_string "expect" |
295 val expect = lookup_string "expect" |
298 in |
296 in |
299 {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking, |
297 {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking, |
300 provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, |
298 provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, |
301 uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, |
299 uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter, |