# HG changeset patch # User blanchet # Date 1321457719 -3600 # Node ID 2b1dde0b1c309d9dfefadb8b3e59bac9f5c95850 # Parent cd6e78cb6ee847057374e8b2116e35d06f3ca013 thread in additional options to minimizer diff -r cd6e78cb6ee8 -r 2b1dde0b1c30 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Nov 16 13:22:36 2011 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Nov 16 16:35:19 2011 +0100 @@ -432,7 +432,7 @@ subgoal_count = Sledgehammer_Util.subgoal_count st, facts = facts |> map Sledgehammer_Provers.Untranslated_Fact, smt_filter = NONE} - in prover params (K (K "")) problem end)) () + in prover params (K (K (K ""))) problem end)) () handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut | Fail "inappropriate" => failed ATP_Proof.Inappropriate val time_prover = run_time |> Time.toMilliseconds diff -r cd6e78cb6ee8 -r 2b1dde0b1c30 src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Nov 16 13:22:36 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Nov 16 16:35:19 2011 +0100 @@ -30,6 +30,7 @@ * (string * locality) list vector * int Symtab.table * string proof * thm val metisN : string + val smtN : string val full_typesN : string val partial_typesN : string val no_typesN : string @@ -198,9 +199,10 @@ | _ => false) -(** Soft-core proof reconstruction: Metis one-liner **) +(** Soft-core proof reconstruction: one-liners **) val metisN = "metis" +val smtN = "smt" val full_typesN = "full_types" val partial_typesN = "partial_types" @@ -233,12 +235,12 @@ | _ => type_enc val opts = [] |> type_enc <> Metis_Tactic.partial_typesN ? cons type_enc |> lam_trans <> metis_default_lam_trans ? cons lam_trans - in "metis" ^ (if null opts then "" else " (" ^ commas opts ^ ")") end + in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end (* unfortunate leaking abstraction *) fun name_of_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans - | name_of_reconstructor SMT = "smt" + | name_of_reconstructor SMT = smtN fun string_for_label (s, num) = s ^ string_of_int num @@ -257,9 +259,9 @@ fun using_labels [] = "" | using_labels ls = "using " ^ space_implode " " (map string_for_label ls) ^ " " -fun reconstructor_command reconstructor i n (ls, ss) = +fun reconstructor_command reconstr i n (ls, ss) = using_labels ls ^ apply_on_subgoal i n ^ - command_call (name_of_reconstructor reconstructor) ss + command_call (name_of_reconstructor reconstr) ss fun minimize_line _ [] = "" | minimize_line minimize_command ss = case minimize_command ss of @@ -274,20 +276,19 @@ subgoal, subgoal_count) = let val (chained, extra) = split_used_facts used_facts - val (failed, reconstructor, ext_time) = + val (failed, reconstr, ext_time) = case preplay of - Played (reconstructor, time) => - (false, reconstructor, (SOME (false, time))) - | Trust_Playable (reconstructor, time) => - (false, reconstructor, + Played (reconstr, time) => (false, reconstr, (SOME (false, time))) + | Trust_Playable (reconstr, time) => + (false, reconstr, case time of NONE => NONE | SOME time => if time = Time.zeroTime then NONE else SOME (true, time)) - | Failed_to_Play reconstructor => (true, reconstructor, NONE) + | Failed_to_Play reconstr => (true, reconstr, NONE) val try_line = ([], map fst extra) - |> reconstructor_command reconstructor subgoal subgoal_count + |> reconstructor_command reconstr subgoal subgoal_count |> (if failed then enclose "One-line proof reconstruction failed: " "." else try_command_line banner ext_time) in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end @@ -1008,11 +1009,11 @@ else if member (op =) qs Show then "show" else "have") val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) - val reconstructor = + val reconstr = Metis (if full_types then Metis_Tactic.full_typesN else Metis_Tactic.partial_typesN, combinatorsN) fun do_facts (ls, ss) = - reconstructor_command reconstructor 1 1 + reconstructor_command reconstr 1 1 (ls |> sort_distinct (prod_ord string_ord int_ord), ss |> sort_distinct string_ord) and do_step ind (Fix xs) = diff -r cd6e78cb6ee8 -r 2b1dde0b1c30 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Nov 16 13:22:36 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Nov 16 16:35:19 2011 +0100 @@ -37,7 +37,6 @@ val combinatorsN : string val hybrid_lamsN : string val keep_lamsN : string - val smartN : string val schematic_var_prefix : string val fixed_var_prefix : string val tvar_prefix : string @@ -127,7 +126,6 @@ val combinatorsN = "combinators" val hybrid_lamsN = "hybrid_lams" val keep_lamsN = "keep_lams" -val smartN = "smart" (* TFF1 is still in development, and it is still unclear whether symbols will be allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with @@ -2344,10 +2342,8 @@ else SOME false val lam_trans = - if lam_trans = smartN then - if is_type_enc_higher_order type_enc then keep_lamsN else combinatorsN - else if lam_trans = keep_lamsN andalso - not (is_type_enc_higher_order type_enc) then + if lam_trans = keep_lamsN andalso + not (is_type_enc_higher_order type_enc) then error ("Lambda translation scheme incompatible with first-order \ \encoding.") else diff -r cd6e78cb6ee8 -r 2b1dde0b1c30 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Nov 16 13:22:36 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Nov 16 16:35:19 2011 +0100 @@ -282,7 +282,7 @@ "smart" => NONE | s => (type_enc_from_string Sound s; SOME s) val sound = mode = Auto_Try orelse lookup_bool "sound" - val lam_trans = lookup_string "lam_trans" + val lam_trans = lookup_option lookup_string "lam_trans" val relevance_thresholds = lookup_real_pair "relevance_thresholds" val max_relevant = lookup_option lookup_int "max_relevant" val max_mono_iters = lookup_int "max_mono_iters" @@ -318,10 +318,13 @@ fun string_for_raw_param (key, values) = key ^ (case implode_param values of "" => "" | value => " = " ^ value) -fun minimize_command override_params i prover_name fact_names = +fun minimize_command override_params i more_override_params prover_name + fact_names = let val params = - override_params + (override_params + |> filter_out (AList.defined (op =) more_override_params o fst)) @ + more_override_params |> filter is_raw_param_relevant_for_minimize |> map string_for_raw_param |> (if prover_name = default_minimize_prover then I else cons prover_name) diff -r cd6e78cb6ee8 -r 2b1dde0b1c30 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Nov 16 13:22:36 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Nov 16 16:35:19 2011 +0100 @@ -71,7 +71,7 @@ {state = state, goal = goal, subgoal = i, subgoal_count = n, facts = facts, smt_filter = NONE} val result as {outcome, used_facts, run_time, ...} = - prover params (K (K "")) problem + prover params (K (K (K ""))) problem in print silent (fn () => diff -r cd6e78cb6ee8 -r 2b1dde0b1c30 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Nov 16 13:22:36 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Nov 16 16:35:19 2011 +0100 @@ -26,7 +26,7 @@ provers: string list, type_enc: string option, sound: bool, - lam_trans: string, + lam_trans: string option, relevance_thresholds: real * real, max_relevant: int option, max_mono_iters: int, @@ -59,7 +59,8 @@ message_tail: string} type prover = - params -> (string -> minimize_command) -> prover_problem -> prover_result + params -> ((string * string list) list -> string -> minimize_command) + -> prover_problem -> prover_result val dest_dir : string Config.T val problem_prefix : string Config.T @@ -78,7 +79,8 @@ val das_tool : string val plain_metis : reconstructor val select_smt_solver : string -> Proof.context -> Proof.context - val prover_name_for_reconstructor : reconstructor -> string + val extract_reconstructor : + reconstructor -> string * (string * string list) list val is_reconstructor : string -> bool val is_atp : theory -> string -> bool val is_smt_prover : Proof.context -> string -> bool @@ -129,23 +131,26 @@ "Async_Manager". *) val das_tool = "Sledgehammer" -val metisN = metisN -val metis_full_typesN = metisN ^ "_" ^ full_typesN -val metis_no_typesN = metisN ^ "_" ^ no_typesN -val smtN = name_of_reconstructor SMT +fun extract_reconstructor (Metis (type_enc, lam_trans)) = + let + val override_params = + (if type_enc = hd partial_type_encs then [] + else [("type_enc", [type_enc])]) @ + (if lam_trans = metis_default_lam_trans then [] + else [("lam_trans", [lam_trans])]) + in (metisN, override_params) end + | extract_reconstructor SMT = (smtN, []) +val reconstructor_names = [metisN, smtN] val plain_metis = Metis (hd partial_type_encs, combinatorsN) -val reconstructor_infos = - [(metisN, plain_metis), - (metis_full_typesN, Metis (hd full_type_encs, combinatorsN)), - (metis_no_typesN, Metis (no_type_enc, combinatorsN)), - (smtN, SMT)] -val prover_name_for_reconstructor = AList.find (op =) reconstructor_infos #> hd +fun standard_reconstructors lam_trans = + [Metis (hd partial_type_encs, lam_trans), + Metis (hd full_type_encs, lam_trans), + Metis (no_type_enc, lam_trans), + SMT] -val all_reconstructors = map snd reconstructor_infos - -val is_reconstructor = AList.defined (op =) reconstructor_infos +val is_reconstructor = member (op =) reconstructor_names val is_atp = member (op =) o supported_atps val select_smt_solver = Context.proof_map o SMT_Config.select_solver @@ -276,7 +281,7 @@ let val thy = Proof_Context.theory_of ctxt val (remote_provers, local_provers) = - map fst reconstructor_infos @ + reconstructor_names @ sort_strings (supported_atps thy) @ sort_strings (SMT_Solver.available_solvers_of ctxt) |> List.partition (String.isPrefix remote_prefix) @@ -299,7 +304,7 @@ provers: string list, type_enc: string option, sound: bool, - lam_trans: string, + lam_trans: string option, relevance_thresholds: real * real, max_relevant: int option, max_mono_iters: int, @@ -332,7 +337,8 @@ message_tail: string} type prover = - params -> (string -> minimize_command) -> prover_problem -> prover_result + params -> ((string * string list) list -> string -> minimize_command) + -> prover_problem -> prover_result (* configuration attributes *) @@ -416,49 +422,48 @@ Metis_Tactic.metis_tac [type_enc] lam_trans | tac_for_reconstructor SMT = SMT_Solver.smt_tac -fun timed_reconstructor reconstructor debug timeout ths = +fun timed_reconstructor reconstr debug timeout ths = (Config.put Metis_Tactic.verbose debug - #> (fn ctxt => tac_for_reconstructor reconstructor ctxt ths)) + #> (fn ctxt => tac_for_reconstructor reconstr ctxt ths)) |> timed_apply timeout fun filter_used_facts used = filter (member (op =) used o fst) fun play_one_line_proof mode debug verbose timeout ths state i preferred - reconstructors = + reconstrs = let val _ = if mode = Minimize andalso Time.> (timeout, Time.zeroTime) then Output.urgent_message "Preplaying proof..." else () - fun get_preferred reconstructors = - if member (op =) reconstructors preferred then preferred - else List.last reconstructors - fun play [] [] = Failed_to_Play (get_preferred reconstructors) + fun get_preferred reconstrs = + if member (op =) reconstrs preferred then preferred + else List.last reconstrs + fun play [] [] = Failed_to_Play (get_preferred reconstrs) | play timed_outs [] = Trust_Playable (get_preferred timed_outs, SOME timeout) - | play timed_out (reconstructor :: reconstructors) = + | play timed_out (reconstr :: reconstrs) = let val _ = if verbose then - "Trying \"" ^ name_of_reconstructor reconstructor ^ "\" for " ^ + "Trying \"" ^ name_of_reconstructor reconstr ^ "\" for " ^ string_from_time timeout ^ "..." |> Output.urgent_message else () val timer = Timer.startRealTimer () in - case timed_reconstructor reconstructor debug timeout ths state i of - SOME (SOME _) => Played (reconstructor, Timer.checkRealTimer timer) - | _ => play timed_out reconstructors + case timed_reconstructor reconstr debug timeout ths state i of + SOME (SOME _) => Played (reconstr, Timer.checkRealTimer timer) + | _ => play timed_out reconstrs end - handle TimeLimit.TimeOut => - play (reconstructor :: timed_out) reconstructors + handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs in if timeout = Time.zeroTime then - Trust_Playable (get_preferred reconstructors, NONE) + Trust_Playable (get_preferred reconstrs, NONE) else - play [] reconstructors + play [] reconstrs end @@ -532,14 +537,16 @@ val metis_minimize_max_time = seconds 2.0 fun choose_minimize_command minimize_command name preplay = - (case preplay of - Played (reconstructor, time) => - if Time.<= (time, metis_minimize_max_time) then - prover_name_for_reconstructor reconstructor - else - name - | _ => name) - |> minimize_command + let + val (name, override_params) = + case preplay of + Played (reconstr, time) => + if Time.<= (time, metis_minimize_max_time) then + extract_reconstructor reconstr + else + (name, []) + | _ => (name, []) + in minimize_command override_params name end fun repair_monomorph_context max_iters max_new_instances = Config.put Monomorph.max_rounds max_iters @@ -668,6 +675,12 @@ else () val readable_names = not (Config.get ctxt atp_full_names) + val lam_trans = + case lam_trans of + SOME s => s + | NONE => + if is_type_enc_higher_order type_enc then keep_lamsN + else combinatorsN (* FIXME ### improve *) val (atp_problem, pool, conjecture_offset, facts_offset, fact_names, typed_helpers, _, sym_tab) = prepare_atp_problem ctxt format conj_sym_kind prem_kind @@ -725,7 +738,7 @@ | _ => outcome in ((pool, conjecture_shape, facts_offset, fact_names, - typed_helpers, sym_tab), + typed_helpers, sym_tab, lam_trans), (output, run_time, atp_proof, outcome)) end val timer = Timer.startRealTimer () @@ -744,8 +757,8 @@ end | maybe_run_slice _ result = result in - ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty), - ("", Time.zeroTime, [], SOME InternalError)) + ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty, + no_lamsN), ("", Time.zeroTime, [], SOME InternalError)) |> fold maybe_run_slice actual_slices end else @@ -761,7 +774,7 @@ else File.write (Path.explode (Path.implode prob_file ^ "_proof")) output val ((pool, conjecture_shape, facts_offset, fact_names, typed_helpers, - sym_tab), + sym_tab, lam_trans), (output, run_time, atp_proof, outcome)) = with_path cleanup export run_on problem_path_name val important_message = @@ -776,6 +789,7 @@ let val used_facts = used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof + val reconstrs = standard_reconstructors lam_trans in (used_facts, fn () => @@ -785,7 +799,7 @@ |> map snd in play_one_line_proof mode debug verbose preplay_timeout used_ths - state subgoal plain_metis all_reconstructors + state subgoal (hd reconstrs) reconstrs end, fn preplay => let @@ -966,7 +980,8 @@ NONE => (fn () => play_one_line_proof mode debug verbose preplay_timeout used_ths - state subgoal SMT all_reconstructors, + state subgoal SMT + (standard_reconstructors lam_liftingN), fn preplay => let val one_line_params = @@ -985,28 +1000,36 @@ preplay = preplay, message = message, message_tail = message_tail} end -fun run_reconstructor mode name ({debug, verbose, timeout, ...} : params) +fun run_reconstructor mode name + ({debug, verbose, timeout, type_enc, lam_trans, ...} : params) minimize_command ({state, subgoal, subgoal_count, facts, ...} : prover_problem) = let - val reconstructor = - case AList.lookup (op =) reconstructor_infos name of - SOME r => r - | NONE => raise Fail ("unknown Metis version: " ^ quote name) + val reconstr = + if name = metisN then + Metis (type_enc |> the_default (hd partial_type_encs), + lam_trans |> the_default metis_default_lam_trans) + else if name = smtN then + SMT + else + raise Fail ("unknown reconstructor: " ^ quote name) val (used_facts, used_ths) = facts |> map untranslated_fact |> ListPair.unzip in case play_one_line_proof (if mode = Minimize then Normal else mode) debug - verbose timeout used_ths state subgoal - reconstructor [reconstructor] of + verbose timeout used_ths state subgoal reconstr + [reconstr] of play as Played (_, time) => {outcome = NONE, used_facts = used_facts, run_time = time, preplay = K play, message = fn play => let + val (_, override_params (* FIXME ###: use these *)) = + extract_reconstructor reconstr val one_line_params = - (play, proof_banner mode name, used_facts, - minimize_command name, subgoal, subgoal_count) + (play, proof_banner mode name, used_facts, + minimize_command override_params name, subgoal, + subgoal_count) in one_line_proof_text one_line_params end, message_tail = ""} | play => diff -r cd6e78cb6ee8 -r 2b1dde0b1c30 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Nov 16 13:22:36 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Nov 16 16:35:19 2011 +0100 @@ -22,7 +22,8 @@ val auto_minimize_max_time : real Config.T val get_minimizing_prover : Proof.context -> mode -> string -> prover val run_sledgehammer : - params -> mode -> int -> relevance_override -> (string -> minimize_command) + params -> mode -> int -> relevance_override + -> ((string * string list) list -> string -> minimize_command) -> Proof.state -> bool * (string * Proof.state) end; @@ -71,6 +72,31 @@ Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time} (K 5.0) +fun adjust_reconstructor_params override_params + ({debug, verbose, overlord, blocking, provers, type_enc, sound, + lam_trans, relevance_thresholds, max_relevant, max_mono_iters, + max_new_mono_instances, isar_proof, isar_shrink_factor, slicing, + timeout, preplay_timeout, expect} : params) = + let + fun lookup_override name default_value = + case AList.lookup (op =) override_params name of + SOME [s] => SOME s + | _ => default_value + (* Only those options that reconstructors are interested in are considered + here. *) + val type_enc = lookup_override "type_enc" type_enc + val lam_trans = lookup_override "lam_trans" lam_trans + in + {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking, + provers = provers, type_enc = type_enc, sound = sound, + lam_trans = lam_trans, max_relevant = max_relevant, + relevance_thresholds = relevance_thresholds, + max_mono_iters = max_mono_iters, + max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, + isar_shrink_factor = isar_shrink_factor, slicing = slicing, + timeout = timeout, preplay_timeout = preplay_timeout, expect = expect} + end + fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...}) ({state, subgoal, subgoal_count, facts, ...} : prover_problem) (result as {outcome, used_facts, run_time, preplay, message, @@ -80,10 +106,10 @@ else let val num_facts = length used_facts - val ((minimize, minimize_name), preplay) = + val ((minimize, (minimize_name, params)), preplay) = if mode = Normal then if num_facts >= Config.get ctxt auto_minimize_min_facts then - ((true, name), preplay) + ((true, (name, params)), preplay) else let fun can_min_fast_enough time = @@ -93,21 +119,24 @@ val prover_fast_enough = can_min_fast_enough run_time in if isar_proof then - ((prover_fast_enough, name), preplay) + ((prover_fast_enough, (name, params)), preplay) else let val preplay = preplay () in (case preplay of - Played (reconstructor, timeout) => + Played (reconstr, timeout) => if can_min_fast_enough timeout then - (true, prover_name_for_reconstructor reconstructor) + (true, extract_reconstructor reconstr + ||> (fn override_params => + adjust_reconstructor_params + override_params params)) else - (prover_fast_enough, name) - | _ => (prover_fast_enough, name), + (prover_fast_enough, (name, params)) + | _ => (prover_fast_enough, (name, params)), K preplay) end end else - ((false, name), preplay) + ((false, (name, params)), preplay) val (used_facts, (preplay, message, _)) = if minimize then minimize_facts minimize_name params (not verbose) subgoal diff -r cd6e78cb6ee8 -r 2b1dde0b1c30 src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Wed Nov 16 13:22:36 2011 +0100 +++ b/src/HOL/ex/sledgehammer_tactics.ML Wed Nov 16 16:35:19 2011 +0100 @@ -49,7 +49,7 @@ facts = map Sledgehammer_Provers.Untranslated_Fact facts, smt_filter = NONE} in - (case prover params (K (K "")) problem of + (case prover params (K (K (K ""))) problem of {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME | _ => NONE) handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)