49 ("isar_proof", "false"), |
49 ("isar_proof", "false"), |
50 ("modulus", "1"), |
50 ("modulus", "1"), |
51 ("sorts", "false"), |
51 ("sorts", "false"), |
52 ("minimize_timeout", "5 s")] |
52 ("minimize_timeout", "5 s")] |
53 |
53 |
54 val negated_params = |
54 val alias_params = |
|
55 [("atp", "atps")] |
|
56 val negated_alias_params = |
55 [("no_debug", "debug"), |
57 [("no_debug", "debug"), |
56 ("quiet", "verbose"), |
58 ("quiet", "verbose"), |
57 ("ignore_no_atp", "respect_no_atp"), |
59 ("ignore_no_atp", "respect_no_atp"), |
58 ("partial_types", "full_types"), |
60 ("partial_types", "full_types"), |
59 ("no_theory_const", "theory_const"), |
61 ("no_theory_const", "theory_const"), |
64 |
66 |
65 val property_dependent_params = ["atps", "full_types", "timeout"] |
67 val property_dependent_params = ["atps", "full_types", "timeout"] |
66 |
68 |
67 fun is_known_raw_param s = |
69 fun is_known_raw_param s = |
68 AList.defined (op =) default_default_params s orelse |
70 AList.defined (op =) default_default_params s orelse |
69 AList.defined (op =) negated_params s orelse |
71 AList.defined (op =) alias_params s orelse |
|
72 AList.defined (op =) negated_alias_params s orelse |
70 member (op =) property_dependent_params s |
73 member (op =) property_dependent_params s |
71 |
74 |
72 fun check_raw_param (s, _) = |
75 fun check_raw_param (s, _) = |
73 if is_known_raw_param s then () |
76 if is_known_raw_param s then () |
74 else error ("Unknown parameter: " ^ quote s ^ ".") |
77 else error ("Unknown parameter: " ^ quote s ^ ".") |
75 |
78 |
76 fun unnegate_raw_param (name, value) = |
79 fun unalias_raw_param (name, value) = |
77 case AList.lookup (op =) negated_params name of |
80 case AList.lookup (op =) alias_params name of |
78 SOME name' => (name', case value of |
81 SOME name' => (name', value) |
79 ["false"] => ["true"] |
82 | NONE => |
80 | ["true"] => ["false"] |
83 case AList.lookup (op =) negated_alias_params name of |
81 | [] => ["false"] |
84 SOME name' => (name', case value of |
82 | _ => value) |
85 ["false"] => ["true"] |
83 | NONE => (name, value) |
86 | ["true"] => ["false"] |
|
87 | [] => ["false"] |
|
88 | _ => value) |
|
89 | NONE => (name, value) |
84 |
90 |
85 structure Data = Theory_Data( |
91 structure Data = Theory_Data( |
86 type T = raw_param list |
92 type T = raw_param list |
87 val empty = default_default_params |> map (apsnd single) |
93 val empty = default_default_params |> map (apsnd single) |
88 val extend = I |
94 val extend = I |
89 fun merge p : T = AList.merge (op =) (K true) p) |
95 fun merge p : T = AList.merge (op =) (K true) p) |
90 |
96 |
91 val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param |
97 val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param |
92 fun default_raw_params thy = |
98 fun default_raw_params thy = |
93 [("atps", [!atps]), |
|
94 ("full_types", [if !full_types then "true" else "false"]), |
|
95 ("timeout", [string_of_int (!timeout) ^ " s"])] @ |
|
96 Data.get thy |
99 Data.get thy |
|
100 |> fold (AList.default (op =)) |
|
101 [("atps", [!atps]), |
|
102 ("full_types", [if !full_types then "true" else "false"]), |
|
103 ("timeout", [string_of_int (!timeout) ^ " s"])] |
97 |
104 |
98 val infinity_time_in_secs = 60 * 60 * 24 * 365 |
105 val infinity_time_in_secs = 60 * 60 * 24 * 365 |
99 val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs) |
106 val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs) |
100 |
107 |
101 fun extract_params thy default_params override_params = |
108 fun extract_params thy default_params override_params = |
102 let |
109 let |
103 val override_params = map unnegate_raw_param override_params |
110 val override_params = map unalias_raw_param override_params |
104 val raw_params = rev override_params @ rev default_params |
111 val raw_params = rev override_params @ rev default_params |
105 val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params |
112 val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params |
106 val lookup_string = the_default "" o lookup |
113 val lookup_string = the_default "" o lookup |
107 fun general_lookup_bool option default_value name = |
114 fun general_lookup_bool option default_value name = |
108 case lookup name of |
115 case lookup name of |