65 val default_default_params = |
65 val default_default_params = |
66 [("debug", "false"), |
66 [("debug", "false"), |
67 ("verbose", "false"), |
67 ("verbose", "false"), |
68 ("overlord", "false"), |
68 ("overlord", "false"), |
69 ("explicit_apply", "false"), |
69 ("explicit_apply", "false"), |
70 ("relevance_threshold", "40"), |
70 ("relevance_thresholds", "45 95"), |
71 ("relevance_decay", "smart"), |
|
72 ("max_relevant", "smart"), |
71 ("max_relevant", "smart"), |
73 ("theory_relevant", "smart"), |
72 ("theory_relevant", "smart"), |
74 ("isar_proof", "false"), |
73 ("isar_proof", "false"), |
75 ("isar_shrink_factor", "1")] |
74 ("isar_shrink_factor", "1")] |
76 |
75 |
154 NONE => 0 |
153 NONE => 0 |
155 | SOME s => case Int.fromString s of |
154 | SOME s => case Int.fromString s of |
156 SOME n => n |
155 SOME n => n |
157 | NONE => error ("Parameter " ^ quote name ^ |
156 | NONE => error ("Parameter " ^ quote name ^ |
158 " must be assigned an integer value.") |
157 " must be assigned an integer value.") |
|
158 fun lookup_int_pair name = |
|
159 case lookup name of |
|
160 NONE => (0, 0) |
|
161 | SOME s => case s |> space_explode " " |> map Int.fromString of |
|
162 [SOME n1, SOME n2] => (n1, n2) |
|
163 | _ => error ("Parameter " ^ quote name ^ |
|
164 "must be assigned a pair of integer values \ |
|
165 \(e.g., \"60 95\")") |
159 fun lookup_int_option name = |
166 fun lookup_int_option name = |
160 case lookup name of |
167 case lookup name of |
161 SOME "smart" => NONE |
168 SOME "smart" => NONE |
162 | _ => SOME (lookup_int name) |
169 | _ => SOME (lookup_int name) |
163 val debug = lookup_bool "debug" |
170 val debug = lookup_bool "debug" |
164 val verbose = debug orelse lookup_bool "verbose" |
171 val verbose = debug orelse lookup_bool "verbose" |
165 val overlord = lookup_bool "overlord" |
172 val overlord = lookup_bool "overlord" |
166 val atps = lookup_string "atps" |> space_explode " " |
173 val atps = lookup_string "atps" |> space_explode " " |
167 val full_types = lookup_bool "full_types" |
174 val full_types = lookup_bool "full_types" |
168 val explicit_apply = lookup_bool "explicit_apply" |
175 val explicit_apply = lookup_bool "explicit_apply" |
169 val relevance_threshold = |
176 val relevance_thresholds = |
170 0.01 * Real.fromInt (lookup_int "relevance_threshold") |
177 lookup_int_pair "relevance_thresholds" |
171 val relevance_decay = |
178 |> pairself (fn n => 0.01 * Real.fromInt n) |
172 lookup_int_option "relevance_decay" |
|
173 |> Option.map (fn n => 0.01 * Real.fromInt n) |
|
174 val max_relevant = lookup_int_option "max_relevant" |
179 val max_relevant = lookup_int_option "max_relevant" |
175 val theory_relevant = lookup_bool_option "theory_relevant" |
180 val theory_relevant = lookup_bool_option "theory_relevant" |
176 val isar_proof = lookup_bool "isar_proof" |
181 val isar_proof = lookup_bool "isar_proof" |
177 val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") |
182 val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") |
178 val timeout = lookup_time "timeout" |
183 val timeout = lookup_time "timeout" |
179 in |
184 in |
180 {debug = debug, verbose = verbose, overlord = overlord, atps = atps, |
185 {debug = debug, verbose = verbose, overlord = overlord, atps = atps, |
181 full_types = full_types, explicit_apply = explicit_apply, |
186 full_types = full_types, explicit_apply = explicit_apply, |
182 relevance_threshold = relevance_threshold, |
187 relevance_thresholds = relevance_thresholds, max_relevant = max_relevant, |
183 relevance_decay = relevance_decay, max_relevant = max_relevant, |
|
184 theory_relevant = theory_relevant, isar_proof = isar_proof, |
188 theory_relevant = theory_relevant, isar_proof = isar_proof, |
185 isar_shrink_factor = isar_shrink_factor, timeout = timeout} |
189 isar_shrink_factor = isar_shrink_factor, timeout = timeout} |
186 end |
190 end |
187 |
191 |
188 fun get_params thy = extract_params (default_raw_params thy) |
192 fun get_params thy = extract_params (default_raw_params thy) |