160 fun normalize_raw_param ctxt = |
160 fun normalize_raw_param ctxt = |
161 unalias_raw_param |
161 unalias_raw_param |
162 #> (fn (name, value) => |
162 #> (fn (name, value) => |
163 if is_known_raw_param name then |
163 if is_known_raw_param name then |
164 (name, value) |
164 (name, value) |
165 else if is_prover_list ctxt name andalso null value then |
165 else if null value then |
166 ("provers", [name]) |
166 if is_prover_list ctxt name then |
167 else if can (type_enc_from_string Strict) name andalso null value then |
167 ("provers", [name]) |
168 ("type_enc", [name]) |
168 else if can (type_enc_from_string Strict) name then |
169 else if can (trans_lams_from_string ctxt any_type_enc) name andalso |
169 ("type_enc", [name]) |
170 null value then |
170 else if can (trans_lams_from_string ctxt any_type_enc) name then |
171 ("lam_trans", [name]) |
171 ("lam_trans", [name]) |
172 else if member (op =) fact_filters name then |
172 else if member (op =) fact_filters name then |
173 ("fact_filter", [name]) |
173 ("fact_filter", [name]) |
174 else if can Int.fromString name then |
174 else if is_some (Int.fromString name) then |
175 ("max_facts", [name]) |
175 ("max_facts", [name]) |
|
176 else |
|
177 error ("Unknown parameter: " ^ quote name ^ ".") |
176 else |
178 else |
177 error ("Unknown parameter: " ^ quote name ^ ".")) |
179 error ("Unknown parameter: " ^ quote name ^ ".")) |
178 |
|
179 |
180 |
180 (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are |
181 (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are |
181 read correctly. *) |
182 read correctly. *) |
182 val implode_param = strip_spaces_except_between_idents o space_implode " " |
183 val implode_param = strip_spaces_except_between_idents o space_implode " " |
183 |
184 |