# HG changeset patch # User blanchet # Date 1403590795 -7200 # Node ID bc06471cb7b7dc565c3029a260ec7b022a2606b6 # Parent 5483868da0d87c53350454cea59976223f0ba5cd move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects diff -r 5483868da0d8 -r bc06471cb7b7 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue Jun 24 08:19:54 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Tue Jun 24 08:19:55 2014 +0200 @@ -234,6 +234,7 @@ val raw_params = rev override_params @ rev default_params val lookup = Option.map implode_param o AList.lookup (op =) raw_params val lookup_string = the_default "" o lookup + fun general_lookup_bool option default_value name = (case lookup name of SOME s => parse_bool_option option name s @@ -275,8 +276,7 @@ val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy" val blocking = Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse lookup_bool "blocking" - val provers = lookup_string "provers" |> space_explode " " - |> mode = Auto_Try ? single o hd + val provers = lookup_string "provers" |> space_explode " " |> mode = Auto_Try ? single o hd val type_enc = if mode = Auto_Try then NONE @@ -322,40 +322,35 @@ val default_minimize_prover = metisN -fun is_raw_param_relevant_for_minimize (name, _) = - not (member (op =) params_not_for_minimize name) +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 = +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)) @ + (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 |> (if prover_name = default_minimize_prover then I else 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) + 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 state0 = +fun hammer_away override_params subcommand opt_i fact_override state = let - val state = - Proof.map_contexts (Try0.silence_methods false #> Config.put SMT2_Config.verbose false) state0 val thy = Proof.theory_of state val ctxt = Proof.context_of state @@ -415,25 +410,20 @@ fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) = Toplevel.unknown_proof o - Toplevel.keep (hammer_away params subcommand opt_i fact_override - o Toplevel.proof_of) + 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 sledgehammer_params_trans params = - Toplevel.theory - (fold set_default_raw_param params - #> tap (fn thy => - writeln ("Default parameters for Sledgehammer:\n" ^ - (case rev (default_raw_params Normal thy) of - [] => "none" - | params => params |> map string_of_raw_param |> sort_strings |> cat_lines)))) + Toplevel.theory (fold set_default_raw_param params #> tap (fn thy => + writeln ("Default parameters for Sledgehammer:\n" ^ + (case rev (default_raw_params Normal thy) of + [] => "none" + | params => params |> map string_of_raw_param |> sort_strings |> cat_lines)))) val parse_query_bang = @{keyword "?"} || @{keyword "!"} || @{keyword "!!"} -val parse_key = - Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param -val parse_value = - Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang) +val parse_key = Scan.repeat1 (Parse.typ_group || parse_query_bang) >> implode_param +val parse_value = Scan.repeat1 (Parse.xname || Parse.float_number || parse_query_bang) val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) [] val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) [] val parse_fact_refs = @@ -443,8 +433,7 @@ || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override) || (parse_fact_refs >> only_fact_override) val parse_fact_override = - Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk - >> merge_fact_overrides)) + Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk >> merge_fact_overrides)) no_fact_override val _ = diff -r 5483868da0d8 -r bc06471cb7b7 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Jun 24 08:19:54 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Tue Jun 24 08:19:55 2014 +0200 @@ -103,14 +103,21 @@ maybe_paren (space_implode " " (meth_s :: ss)) end +val silence_unifier = Try0.silence_methods false + fun tac_of_proof_method ctxt (local_facts, global_facts) meth = Method.insert_tac local_facts THEN' (case meth of Metis_Method (type_enc_opt, lam_trans_opt) => - Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)] - (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts + let val ctxt = Config.put Metis_Tactic.verbose false ctxt in + Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)] + (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts + end | Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts - | SMT2_Method => SMT2_Solver.smt2_tac ctxt global_facts + | SMT2_Method => + let val ctxt = Config.put SMT2_Config.verbose false ctxt in + SMT2_Solver.smt2_tac ctxt global_facts + end | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts) | _ => Method.insert_tac global_facts THEN' @@ -119,10 +126,11 @@ | Blast_Method => blast_tac ctxt | Simp_Size_Method => Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt) - | Auto_Method => K (Clasimp.auto_tac ctxt) - | Fastforce_Method => Clasimp.fast_force_tac ctxt - | Force_Method => Clasimp.force_tac ctxt - | Linarith_Method => Lin_Arith.tac ctxt + | Auto_Method => K (Clasimp.auto_tac (silence_unifier ctxt)) + | Fastforce_Method => Clasimp.fast_force_tac (silence_unifier ctxt) + | Force_Method => Clasimp.force_tac (silence_unifier ctxt) + | Linarith_Method => + let val ctxt = Config.put Lin_Arith.verbose false ctxt in Lin_Arith.tac ctxt end | Presburger_Method => Cooper.tac true [] [] ctxt | Algebra_Method => Groebner.algebra_tac [] [] ctxt))