39 |
39 |
40 val default_default_params = |
40 val default_default_params = |
41 [("debug", "false"), |
41 [("debug", "false"), |
42 ("verbose", "false"), |
42 ("verbose", "false"), |
43 ("overlord", "false"), |
43 ("overlord", "false"), |
|
44 ("explicit_apply", "false"), |
44 ("respect_no_atp", "true"), |
45 ("respect_no_atp", "true"), |
45 ("relevance_threshold", "50"), |
46 ("relevance_threshold", "50"), |
46 ("convergence", "320"), |
47 ("convergence", "320"), |
47 ("theory_relevant", "smart"), |
48 ("theory_relevant", "smart"), |
48 ("higher_order", "smart"), |
49 ("higher_order", "smart"), |
56 [("atp", "atps")] |
57 [("atp", "atps")] |
57 val negated_alias_params = |
58 val negated_alias_params = |
58 [("no_debug", "debug"), |
59 [("no_debug", "debug"), |
59 ("quiet", "verbose"), |
60 ("quiet", "verbose"), |
60 ("no_overlord", "overlord"), |
61 ("no_overlord", "overlord"), |
|
62 ("implicit_apply", "explicit_apply"), |
61 ("ignore_no_atp", "respect_no_atp"), |
63 ("ignore_no_atp", "respect_no_atp"), |
62 ("partial_types", "full_types"), |
64 ("partial_types", "full_types"), |
63 ("theory_irrelevant", "theory_relevant"), |
65 ("theory_irrelevant", "theory_relevant"), |
64 ("first_order", "higher_order"), |
66 ("first_order", "higher_order"), |
65 ("dont_follow_defs", "follow_defs"), |
67 ("dont_follow_defs", "follow_defs"), |
144 val debug = lookup_bool "debug" |
146 val debug = lookup_bool "debug" |
145 val verbose = debug orelse lookup_bool "verbose" |
147 val verbose = debug orelse lookup_bool "verbose" |
146 val overlord = lookup_bool "overlord" |
148 val overlord = lookup_bool "overlord" |
147 val atps = lookup_string "atps" |> space_explode " " |
149 val atps = lookup_string "atps" |> space_explode " " |
148 val full_types = lookup_bool "full_types" |
150 val full_types = lookup_bool "full_types" |
|
151 val explicit_apply = lookup_bool "explicit_apply" |
149 val respect_no_atp = lookup_bool "respect_no_atp" |
152 val respect_no_atp = lookup_bool "respect_no_atp" |
150 val relevance_threshold = |
153 val relevance_threshold = |
151 0.01 * Real.fromInt (lookup_int "relevance_threshold") |
154 0.01 * Real.fromInt (lookup_int "relevance_threshold") |
152 val convergence = 0.01 * Real.fromInt (lookup_int "convergence") |
155 val convergence = 0.01 * Real.fromInt (lookup_int "convergence") |
153 val theory_relevant = lookup_bool_option "theory_relevant" |
156 val theory_relevant = lookup_bool_option "theory_relevant" |
158 val sorts = lookup_bool "sorts" |
161 val sorts = lookup_bool "sorts" |
159 val timeout = lookup_time "timeout" |
162 val timeout = lookup_time "timeout" |
160 val minimize_timeout = lookup_time "minimize_timeout" |
163 val minimize_timeout = lookup_time "minimize_timeout" |
161 in |
164 in |
162 {debug = debug, verbose = verbose, overlord = overlord, atps = atps, |
165 {debug = debug, verbose = verbose, overlord = overlord, atps = atps, |
163 full_types = full_types, respect_no_atp = respect_no_atp, |
166 full_types = full_types, explicit_apply = explicit_apply, |
164 relevance_threshold = relevance_threshold, convergence = convergence, |
167 respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold, |
165 theory_relevant = theory_relevant, higher_order = higher_order, |
168 convergence = convergence, theory_relevant = theory_relevant, |
166 follow_defs = follow_defs, isar_proof = isar_proof, modulus = modulus, |
169 higher_order = higher_order, follow_defs = follow_defs, |
167 sorts = sorts, timeout = timeout, minimize_timeout = minimize_timeout} |
170 isar_proof = isar_proof, modulus = modulus, sorts = sorts, |
|
171 timeout = timeout, minimize_timeout = minimize_timeout} |
168 end |
172 end |
169 |
173 |
170 fun get_params thy = extract_params thy (default_raw_params thy) |
174 fun get_params thy = extract_params thy (default_raw_params thy) |
171 fun default_params thy = get_params thy o map (apsnd single) |
175 fun default_params thy = get_params thy o map (apsnd single) |
172 |
176 |