109 AList.defined (op =) default_default_params s orelse |
109 AList.defined (op =) default_default_params s orelse |
110 AList.defined (op =) alias_params s orelse |
110 AList.defined (op =) alias_params s orelse |
111 AList.defined (op =) negated_alias_params s orelse |
111 AList.defined (op =) negated_alias_params s orelse |
112 member (op =) property_dependent_params s orelse s = "expect" |
112 member (op =) property_dependent_params s orelse s = "expect" |
113 |
113 |
114 fun check_raw_param (s, _) = |
114 fun is_prover_list ctxt s = |
115 if is_known_raw_param s then () |
115 case space_explode " " s of |
116 else error ("Unknown parameter: " ^ quote s ^ ".") |
116 ss as _ :: _ => forall (is_prover_available ctxt) ss |
|
117 | _ => false |
|
118 |
|
119 fun check_and_repair_raw_param ctxt (name, value) = |
|
120 if is_known_raw_param name then (name, value) |
|
121 else if is_prover_list ctxt name andalso null value then ("provers", [name]) |
|
122 else error ("Unknown parameter: " ^ quote name ^ ".") |
117 |
123 |
118 fun unalias_raw_param (name, value) = |
124 fun unalias_raw_param (name, value) = |
119 case AList.lookup (op =) alias_params name of |
125 case AList.lookup (op =) alias_params name of |
120 SOME name' => (name', value) |
126 SOME name' => (name', value) |
121 | NONE => |
127 | NONE => |
280 (if i = 1 then "" else " " ^ string_of_int i) |
286 (if i = 1 then "" else " " ^ string_of_int i) |
281 |
287 |
282 fun hammer_away override_params subcommand opt_i relevance_override state = |
288 fun hammer_away override_params subcommand opt_i relevance_override state = |
283 let |
289 let |
284 val ctxt = Proof.context_of state |
290 val ctxt = Proof.context_of state |
285 val _ = app check_raw_param override_params |
291 val override_params = |
|
292 override_params |> map (check_and_repair_raw_param ctxt) |
286 in |
293 in |
287 if subcommand = runN then |
294 if subcommand = runN then |
288 let val i = the_default 1 opt_i in |
295 let val i = the_default 1 opt_i in |
289 run_sledgehammer (get_params false ctxt override_params) false i |
296 run_sledgehammer (get_params false ctxt override_params) false i |
290 relevance_override (minimize_command override_params i) |
297 relevance_override (minimize_command override_params i) |
321 let val ctxt = ProofContext.init_global thy in |
328 let val ctxt = ProofContext.init_global thy in |
322 writeln ("Default parameters for Sledgehammer:\n" ^ |
329 writeln ("Default parameters for Sledgehammer:\n" ^ |
323 (case default_raw_params ctxt |> rev of |
330 (case default_raw_params ctxt |> rev of |
324 [] => "none" |
331 [] => "none" |
325 | params => |
332 | params => |
326 (map check_raw_param params; |
333 params |> map (check_and_repair_raw_param ctxt) |
327 params |> map string_for_raw_param |
334 |> map string_for_raw_param |
328 |> sort_strings |> cat_lines))) |
335 |> sort_strings |> cat_lines)) |
329 end)) |
336 end)) |
330 |
337 |
331 val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " " |
338 val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " " |
332 val parse_value = Scan.repeat1 (Parse.xname || Parse.float_number) |
339 val parse_value = Scan.repeat1 (Parse.xname || Parse.float_number) |
333 val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) [] |
340 val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) [] |