equal
deleted
inserted
replaced
76 [("blocking", "false"), |
76 [("blocking", "false"), |
77 ("debug", "false"), |
77 ("debug", "false"), |
78 ("verbose", "false"), |
78 ("verbose", "false"), |
79 ("overlord", "false"), |
79 ("overlord", "false"), |
80 ("explicit_apply", "false"), |
80 ("explicit_apply", "false"), |
81 ("relevance_thresholds", "45 85"), |
81 ("relevance_thresholds", "0.45 0.85"), |
82 ("max_relevant", "smart"), |
82 ("max_relevant", "smart"), |
83 ("isar_proof", "false"), |
83 ("isar_proof", "false"), |
84 ("isar_shrink_factor", "1")] |
84 ("isar_shrink_factor", "1")] |
85 |
85 |
86 val alias_params = |
86 val alias_params = |
204 NONE => 0 |
204 NONE => 0 |
205 | SOME s => case Int.fromString s of |
205 | SOME s => case Int.fromString s of |
206 SOME n => n |
206 SOME n => n |
207 | NONE => error ("Parameter " ^ quote name ^ |
207 | NONE => error ("Parameter " ^ quote name ^ |
208 " must be assigned an integer value.") |
208 " must be assigned an integer value.") |
209 fun lookup_int_pair name = |
209 fun lookup_real_pair name = |
210 case lookup name of |
210 case lookup name of |
211 NONE => (0, 0) |
211 NONE => (0.0, 0.0) |
212 | SOME s => case s |> space_explode " " |> map Int.fromString of |
212 | SOME s => case s |> space_explode " " |> map Real.fromString of |
213 [SOME n1, SOME n2] => (n1, n2) |
213 [SOME r1, SOME r2] => (r1, r2) |
214 | _ => error ("Parameter " ^ quote name ^ |
214 | _ => error ("Parameter " ^ quote name ^ |
215 "must be assigned a pair of integer values \ |
215 "must be assigned a pair of floating-point \ |
216 \(e.g., \"60 95\")") |
216 \values (e.g., \"0.6 0.95\")") |
217 fun lookup_int_option name = |
217 fun lookup_int_option name = |
218 case lookup name of |
218 case lookup name of |
219 SOME "smart" => NONE |
219 SOME "smart" => NONE |
220 | _ => SOME (lookup_int name) |
220 | _ => SOME (lookup_int name) |
221 val blocking = auto orelse lookup_bool "blocking" |
221 val blocking = auto orelse lookup_bool "blocking" |
224 val overlord = lookup_bool "overlord" |
224 val overlord = lookup_bool "overlord" |
225 val provers = lookup_string "provers" |> space_explode " " |
225 val provers = lookup_string "provers" |> space_explode " " |
226 |> auto ? single o hd |
226 |> auto ? single o hd |
227 val full_types = lookup_bool "full_types" |
227 val full_types = lookup_bool "full_types" |
228 val explicit_apply = lookup_bool "explicit_apply" |
228 val explicit_apply = lookup_bool "explicit_apply" |
229 val relevance_thresholds = |
229 val relevance_thresholds = lookup_real_pair "relevance_thresholds" |
230 lookup_int_pair "relevance_thresholds" |
|
231 |> pairself (fn n => 0.01 * Real.fromInt n) |
|
232 val max_relevant = lookup_int_option "max_relevant" |
230 val max_relevant = lookup_int_option "max_relevant" |
233 val isar_proof = lookup_bool "isar_proof" |
231 val isar_proof = lookup_bool "isar_proof" |
234 val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") |
232 val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") |
235 val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout |
233 val timeout = (if auto then NONE else lookup_time "timeout") |> the_timeout |
236 val expect = lookup_string "expect" |
234 val expect = lookup_string "expect" |