equal
deleted
inserted
replaced
149 | _ => value) |
149 | _ => value) |
150 | NONE => (name, value) |
150 | NONE => (name, value) |
151 |
151 |
152 val any_type_enc = type_enc_from_string Strict "erased" |
152 val any_type_enc = type_enc_from_string Strict "erased" |
153 |
153 |
154 (* "provers =", "type_enc =", "lam_trans =", and "fact_filter =" can be omitted. |
154 (* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts =" |
155 For the last three, this is a secret feature. *) |
155 can be omitted. For the last four, this is a secret feature. *) |
156 fun normalize_raw_param ctxt = |
156 fun normalize_raw_param ctxt = |
157 unalias_raw_param |
157 unalias_raw_param |
158 #> (fn (name, value) => |
158 #> (fn (name, value) => |
159 if is_known_raw_param name then |
159 if is_known_raw_param name then |
160 (name, value) |
160 (name, value) |
165 else if can (trans_lams_from_string ctxt any_type_enc) name andalso |
165 else if can (trans_lams_from_string ctxt any_type_enc) name andalso |
166 null value then |
166 null value then |
167 ("lam_trans", [name]) |
167 ("lam_trans", [name]) |
168 else if member (op =) fact_filters name then |
168 else if member (op =) fact_filters name then |
169 ("fact_filter", [name]) |
169 ("fact_filter", [name]) |
170 else |
170 else case Int.fromString name of |
171 error ("Unknown parameter: " ^ quote name ^ ".")) |
171 SOME n => ("max_facts", [name]) |
|
172 | NONE => error ("Unknown parameter: " ^ quote name ^ ".")) |
172 |
173 |
173 |
174 |
174 (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are |
175 (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are |
175 read correctly. *) |
176 read correctly. *) |
176 val implode_param = strip_spaces_except_between_idents o space_implode " " |
177 val implode_param = strip_spaces_except_between_idents o space_implode " " |