67 ("verbose", "false"), |
67 ("verbose", "false"), |
68 ("overlord", "false"), |
68 ("overlord", "false"), |
69 ("explicit_apply", "false"), |
69 ("explicit_apply", "false"), |
70 ("relevance_threshold", "50"), |
70 ("relevance_threshold", "50"), |
71 ("relevance_convergence", "320"), |
71 ("relevance_convergence", "320"), |
|
72 ("max_relevant_per_iter", "smart"), |
72 ("theory_relevant", "smart"), |
73 ("theory_relevant", "smart"), |
73 ("defs_relevant", "false"), |
74 ("defs_relevant", "false"), |
74 ("isar_proof", "false"), |
75 ("isar_proof", "false"), |
75 ("isar_shrink_factor", "1"), |
76 ("isar_shrink_factor", "1"), |
76 ("minimize_timeout", "5 s")] |
77 ("minimize_timeout", "5 s")] |
156 NONE => 0 |
157 NONE => 0 |
157 | SOME s => case Int.fromString s of |
158 | SOME s => case Int.fromString s of |
158 SOME n => n |
159 SOME n => n |
159 | NONE => error ("Parameter " ^ quote name ^ |
160 | NONE => error ("Parameter " ^ quote name ^ |
160 " must be assigned an integer value.") |
161 " must be assigned an integer value.") |
|
162 fun lookup_int_option name = |
|
163 case lookup name of |
|
164 SOME "smart" => NONE |
|
165 | _ => SOME (lookup_int name) |
161 val debug = lookup_bool "debug" |
166 val debug = lookup_bool "debug" |
162 val verbose = debug orelse lookup_bool "verbose" |
167 val verbose = debug orelse lookup_bool "verbose" |
163 val overlord = lookup_bool "overlord" |
168 val overlord = lookup_bool "overlord" |
164 val atps = lookup_string "atps" |> space_explode " " |
169 val atps = lookup_string "atps" |> space_explode " " |
165 val full_types = lookup_bool "full_types" |
170 val full_types = lookup_bool "full_types" |
166 val explicit_apply = lookup_bool "explicit_apply" |
171 val explicit_apply = lookup_bool "explicit_apply" |
167 val relevance_threshold = |
172 val relevance_threshold = |
168 0.01 * Real.fromInt (lookup_int "relevance_threshold") |
173 0.01 * Real.fromInt (lookup_int "relevance_threshold") |
169 val relevance_convergence = |
174 val relevance_convergence = |
170 0.01 * Real.fromInt (lookup_int "relevance_convergence") |
175 0.01 * Real.fromInt (lookup_int "relevance_convergence") |
|
176 val max_relevant_per_iter = lookup_int_option "max_relevant_per_iter" |
171 val theory_relevant = lookup_bool_option "theory_relevant" |
177 val theory_relevant = lookup_bool_option "theory_relevant" |
172 val defs_relevant = lookup_bool "defs_relevant" |
178 val defs_relevant = lookup_bool "defs_relevant" |
173 val isar_proof = lookup_bool "isar_proof" |
179 val isar_proof = lookup_bool "isar_proof" |
174 val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") |
180 val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") |
175 val timeout = lookup_time "timeout" |
181 val timeout = lookup_time "timeout" |
177 in |
183 in |
178 {debug = debug, verbose = verbose, overlord = overlord, atps = atps, |
184 {debug = debug, verbose = verbose, overlord = overlord, atps = atps, |
179 full_types = full_types, explicit_apply = explicit_apply, |
185 full_types = full_types, explicit_apply = explicit_apply, |
180 relevance_threshold = relevance_threshold, |
186 relevance_threshold = relevance_threshold, |
181 relevance_convergence = relevance_convergence, |
187 relevance_convergence = relevance_convergence, |
|
188 max_relevant_per_iter = max_relevant_per_iter, |
182 theory_relevant = theory_relevant, defs_relevant = defs_relevant, |
189 theory_relevant = theory_relevant, defs_relevant = defs_relevant, |
183 isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, |
190 isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, |
184 timeout = timeout, minimize_timeout = minimize_timeout} |
191 timeout = timeout, minimize_timeout = minimize_timeout} |
185 end |
192 end |
186 |
193 |