# HG changeset patch # User blanchet # Date 1406897037 -7200 # Node ID 056a55b44ec7610c2ea29c7b1c6ffc8b76dee7ae # Parent 18bb3e1ff6f6a7758db11644adcaa5c77c44dba6 eliminated Sledgehammer's "min" subcommand (and lots of complications in the code) diff -r 18bb3e1ff6f6 -r 056a55b44ec7 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Aug 01 14:43:57 2014 +0200 @@ -10,7 +10,6 @@ sig type fact = Sledgehammer_Fact.fact type fact_override = Sledgehammer_Fact.fact_override - type minimize_command = Sledgehammer_Proof_Methods.minimize_command type mode = Sledgehammer_Prover.mode type params = Sledgehammer_Prover.params @@ -21,8 +20,7 @@ val string_of_factss : (string * fact list) list -> string val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override -> - ((string * string list) list -> string -> minimize_command) -> Proof.state -> - bool * (string * Proof.state) + Proof.state -> bool * (string * Proof.state) end; structure Sledgehammer : SLEDGEHAMMER = @@ -90,7 +88,7 @@ end fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, preplay_timeout, - expect, ...}) mode output_result minimize_command only learn + expect, ...}) mode output_result only learn {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = let val ctxt = Proof.context_of state @@ -154,7 +152,7 @@ fun really_go () = problem - |> get_minimizing_prover ctxt mode learn name params minimize_command + |> get_minimizing_prover ctxt mode learn name params |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => print_used_facts used_facts used_from | _ => ()) @@ -235,7 +233,7 @@ (if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss) fun run_sledgehammer (params as {verbose, spy, blocking, provers, max_facts, ...}) mode - output_result i (fact_override as {only, ...}) minimize_command state = + output_result i (fact_override as {only, ...}) state = if null provers then error "No prover is set." else @@ -292,7 +290,7 @@ {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = factss} val learn = mash_learn_proof ctxt params (prop_of goal) all_facts - val launch = launch_prover params mode output_result minimize_command only learn + val launch = launch_prover params mode output_result only learn in if mode = Auto_Try then (unknownN, state) diff -r 18bb3e1ff6f6 -r 056a55b44ec7 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Aug 01 14:43:57 2014 +0200 @@ -31,7 +31,6 @@ val z3N = "z3" val runN = "run" -val minN = "min" val messagesN = "messages" val supported_proversN = "supported_provers" val kill_allN = "kill_all" @@ -119,9 +118,6 @@ ("dont_try0", "try0"), ("no_smt_proofs", "smt_proofs")] -val params_not_for_minimize = - ["provers", "blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"]; - val property_dependent_params = ["provers", "timeout"] fun is_known_raw_param s = @@ -318,31 +314,6 @@ (* Sledgehammer the given subgoal *) -fun is_raw_param_relevant_for_minimize (name, _) = not (member (op =) params_not_for_minimize name) - -fun string_of_raw_param (key, values) = - key ^ (case implode_param values of "" => "" | value => " = " ^ value) - -fun nice_string_of_raw_param (p as (key, ["false"])) = - (case AList.find (op =) negated_alias_params key of - [neg] => neg - | _ => string_of_raw_param p) - | nice_string_of_raw_param p = string_of_raw_param p - -fun minimize_command override_params i more_override_params prover_name fact_names = - let - val params = - (override_params |> filter_out (AList.defined (op =) more_override_params o fst)) @ - more_override_params - |> filter is_raw_param_relevant_for_minimize - |> map nice_string_of_raw_param - |> cons prover_name - |> space_implode ", " - in - sledgehammerN ^ " " ^ minN ^ (if params = "" then "" else enclose " [" "]" params) ^ - " (" ^ space_implode " " fact_names ^ ")" ^ (if i = 1 then "" else " " ^ string_of_int i) - end - val default_learn_prover_timeout = 2.0 fun hammer_away override_params subcommand opt_i fact_override state = @@ -355,19 +326,9 @@ in if subcommand = runN then let val i = the_default 1 opt_i in - run_sledgehammer (get_params Normal thy override_params) Normal NONE i fact_override - (minimize_command override_params i) state - |> K () + ignore (run_sledgehammer (get_params Normal thy override_params) Normal NONE i fact_override + state) end - else if subcommand = minN then - let - val ctxt = ctxt |> Config.put instantiate_inducts false - val i = the_default 1 opt_i - val params = get_params Minimize thy override_params - val goal = prop_of (#goal (Proof.goal state)) - val facts = nearly_all_facts ctxt false fact_override Symtab.empty Termtab.empty [] [] goal - val learn = mash_learn_proof ctxt params goal facts - in run_minimize params learn i (#add fact_override) state end else if subcommand = messagesN then messages opt_i else if subcommand = supported_proversN then @@ -403,7 +364,8 @@ Toplevel.unknown_proof o Toplevel.keep (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of) -fun string_of_raw_param (name, value) = name ^ " = " ^ implode_param value +fun string_of_raw_param (key, values) = + key ^ (case implode_param values of "" => "" | value => " = " ^ value) fun sledgehammer_params_trans params = Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => @@ -442,8 +404,7 @@ val mode = if auto then Auto_Try else Try val i = 1 in - run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override (minimize_command [] i) - state + run_sledgehammer (get_params mode thy []) mode NONE i no_fact_override state end val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer)) @@ -452,23 +413,23 @@ Query_Operation.register sledgehammerN (fn {state = st, args, output_result} => (case try Toplevel.proof_of st of SOME state => - let - val thy = Proof.theory_of state - val ctxt = Proof.context_of state - val [provers_arg, isar_proofs_arg] = args + let + val thy = Proof.theory_of state + val ctxt = Proof.context_of state + val [provers_arg, isar_proofs_arg] = args - val override_params = - ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @ - [("isar_proofs", [isar_proofs_arg]), - ("blocking", ["true"]), - ("debug", ["false"]), - ("verbose", ["false"]), - ("overlord", ["false"])]) - |> map (normalize_raw_param ctxt) - - val _ = run_sledgehammer (get_params Normal thy override_params) Normal - (SOME output_result) 1 no_fact_override (minimize_command override_params 1) state - in () end + val override_params = + ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @ + [("isar_proofs", [isar_proofs_arg]), + ("blocking", ["true"]), + ("debug", ["false"]), + ("verbose", ["false"]), + ("overlord", ["false"])]) + |> map (normalize_raw_param ctxt) + in + ignore (run_sledgehammer (get_params Normal thy override_params) Normal + (SOME output_result) 1 no_fact_override state) + end | NONE => error "Unknown proof context")) end; diff -r 18bb3e1ff6f6 -r 056a55b44ec7 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Aug 01 14:43:57 2014 +0200 @@ -127,8 +127,7 @@ val skolem_methods = basic_systematic_methods fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params - (one_line_params as ((_, one_line_play), banner, used_facts, minimize_command, subgoal, - subgoal_count)) = + (one_line_params as ((_, one_line_play), banner, used_facts, subgoal, subgoal_count)) = let val _ = if debug then Output.urgent_message "Constructing Isar proof..." else () @@ -352,8 +351,7 @@ (case isar_proof of Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) => let val used_facts' = filter (member (op =) gfs o fst) used_facts in - ((meth, play_outcome), banner, used_facts', minimize_command, subgoal, - subgoal_count) + ((meth, play_outcome), banner, used_facts', subgoal, subgoal_count) end) else one_line_params) ^ @@ -389,7 +387,7 @@ | Play_Failed => true) fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained - (one_line_params as (preplay, _, _, _, _, _)) = + (one_line_params as (preplay, _, _, _, _)) = (if isar_proofs = SOME true orelse (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then isar_proof_text ctxt debug isar_proofs smt_proofs isar_params diff -r 18bb3e1ff6f6 -r 056a55b44ec7 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Aug 01 14:43:57 2014 +0200 @@ -814,7 +814,7 @@ {comment = "Goal: " ^ goal_name, state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1, factss = [("", facts)]} in - get_minimizing_prover ctxt MaSh (K ()) prover params (K (K (K ""))) problem + get_minimizing_prover ctxt MaSh (K ()) prover params problem end val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] diff -r 18bb3e1ff6f6 -r 056a55b44ec7 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Fri Aug 01 14:43:57 2014 +0200 @@ -29,9 +29,8 @@ Play_Timed_Out of Time.time | Play_Failed - type minimize_command = string list -> string type one_line_params = - (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int + (proof_method * play_outcome) * string * (string * stature) list * int * int val is_proof_method_direct : proof_method -> bool val string_of_proof_method : Proof.context -> string list -> proof_method -> string @@ -69,9 +68,7 @@ Play_Timed_Out of Time.time | Play_Failed -type minimize_command = string list -> string -type one_line_params = - (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int +type one_line_params = (proof_method * play_outcome) * string * (string * stature) list * int * int fun is_proof_method_direct (Metis_Method _) = true | is_proof_method_direct Meson_Method = true @@ -179,29 +176,18 @@ (s |> s <> "" ? enclose " (" ")") ^ "." end -fun minimize_line _ [] = "" - | minimize_line minimize_command ss = - (case minimize_command ss of - "" => "" - | command => "\nTo minimize: " ^ Active.sendback_markup [Markup.padding_command] command ^ ".") - fun split_used_facts facts = facts |> List.partition (fn (_, (sc, _)) => sc = Chained) |> pairself (sort_distinct (string_ord o pairself fst)) fun one_line_proof_text ctxt num_chained - ((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) = - let - val (chained, extra) = split_used_facts used_facts - - val try_line = - map fst extra - |> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained - |> (if play = Play_Failed then enclose "One-line proof reconstruction failed: " "." - else try_command_line banner play) - in - try_line ^ minimize_line minimize_command (map fst (extra @ chained)) + ((meth, play), banner, used_facts, subgoal, subgoal_count) = + let val (chained, extra) = split_used_facts used_facts in + map fst extra + |> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained + |> (if play = Play_Failed then enclose "One-line proof reconstruction failed: " "." + else try_command_line banner play) end end; diff -r 18bb3e1ff6f6 -r 056a55b44ec7 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Aug 01 14:43:57 2014 +0200 @@ -14,7 +14,6 @@ type fact = Sledgehammer_Fact.fact type proof_method = Sledgehammer_Proof_Methods.proof_method type play_outcome = Sledgehammer_Proof_Methods.play_outcome - type minimize_command = Sledgehammer_Proof_Methods.minimize_command datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize @@ -62,9 +61,7 @@ message : proof_method * play_outcome -> string, message_tail : string} - type prover = - params -> ((string * string list) list -> string -> minimize_command) -> prover_problem -> - prover_result + type prover = params -> prover_problem -> prover_result val SledgehammerN : string val str_of_mode : mode -> string @@ -156,9 +153,7 @@ message : proof_method * play_outcome -> string, message_tail : string} -type prover = - params -> ((string * string list) list -> string -> minimize_command) - -> prover_problem -> prover_result +type prover = params -> prover_problem -> prover_result fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover) diff -r 18bb3e1ff6f6 -r 056a55b44ec7 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Aug 01 14:43:57 2014 +0200 @@ -135,7 +135,6 @@ ({debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases, fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, slice, minimize, timeout, preplay_timeout, ...} : params) - minimize_command ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = let val thy = Proof.theory_of state @@ -388,8 +387,7 @@ end val one_line_params = - (preplay, proof_banner mode name, used_facts, minimize_command [] name, subgoal, - subgoal_count) + (preplay, proof_banner mode name, used_facts, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params diff -r 18bb3e1ff6f6 -r 056a55b44ec7 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Aug 01 14:43:57 2014 +0200 @@ -102,7 +102,7 @@ val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = [("", facts)]} - val result as {outcome, used_facts, run_time, ...} = prover params (K (K (K ""))) problem + val result as {outcome, used_facts, run_time, ...} = prover params problem in print silent (fn () => (case outcome of @@ -253,8 +253,8 @@ | NONE => result) end -fun get_minimizing_prover ctxt mode do_learn name params minimize_command problem = - get_prover ctxt mode name params minimize_command problem +fun get_minimizing_prover ctxt mode do_learn name params problem = + get_prover ctxt mode name params problem |> maybe_minimize mode do_learn name params problem fun run_minimize (params as {provers, ...}) do_learn i refs state = diff -r 18bb3e1ff6f6 -r 056a55b44ec7 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri Aug 01 14:43:57 2014 +0200 @@ -179,7 +179,7 @@ fun run_smt2_solver mode name (params as {debug, verbose, isar_proofs, compress, try0, smt_proofs, minimize, preplay_timeout, ...}) - minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = + ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) = let val thy = Proof.theory_of state val ctxt = Proof.context_of state @@ -209,8 +209,7 @@ goal) val one_line_params = - (preplay, proof_banner mode name, used_facts, minimize_command [] name, subgoal, - subgoal_count) + (preplay, proof_banner mode name, used_facts, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params