# HG changeset patch # User blanchet # Date 1269430233 -3600 # Node ID f8c738abaed890a23a5ba6cb7ba4579cd070e680 # Parent 0fce6db7babdca3de295feaa44440b9d1aff7b1f honor the newly introduced Sledgehammer parameters and fixed the parsing; e.g. the prover "e_isar" (formely "e_full") is gone, instead do sledgehammer [atps = e, isar_proof] to get the same effect diff -r 0fce6db7babd -r f8c738abaed8 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Mar 23 14:43:22 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed Mar 24 12:30:33 2010 +0100 @@ -9,11 +9,16 @@ type axiom_name = Sledgehammer_HOL_Clause.axiom_name type hol_clause = Sledgehammer_HOL_Clause.hol_clause type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id + type relevance_override = + {add: Facts.ref list, + del: Facts.ref list, + only: bool} + val tvar_classes_of_terms : term list -> string list val tfree_classes_of_terms : term list -> string list val type_consts_of_terms : theory -> term list -> string list val get_relevant_facts : - real -> bool option -> bool -> int -> bool + real -> bool option -> bool -> int -> bool -> relevance_override -> Proof.context * (thm list * 'a) -> thm list -> (thm * (string * int)) list val prepare_clauses : bool option -> bool -> thm list -> thm list -> @@ -31,9 +36,10 @@ open Sledgehammer_Fact_Preprocessor open Sledgehammer_HOL_Clause -type axiom_name = axiom_name -type hol_clause = hol_clause -type hol_clause_id = hol_clause_id +type relevance_override = + {add: Facts.ref list, + del: Facts.ref list, + only: bool} (********************************************************************) (* some settings for both background automatic ATP calling procedure*) @@ -257,8 +263,12 @@ end end; -fun relevant_clauses follow_defs max_new thy ctab p rel_consts = - let fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*) +fun relevant_clauses ctxt follow_defs max_new + (relevance_override as {add, del, only}) thy ctab p + rel_consts = + let val add_thms = maps (ProofContext.get_fact ctxt) add + val del_thms = maps (ProofContext.get_fact ctxt) del + fun relevant ([],_) [] = [] : (thm * (string * int)) list (*Nothing added this iteration*) | relevant (newpairs,rejects) [] = let val (newrels,more_rejects) = take_best max_new newpairs val new_consts = maps #2 newrels @@ -266,12 +276,17 @@ val newp = p + (1.0-p) / convergence in trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels)); - (map #1 newrels) @ - (relevant_clauses follow_defs max_new thy ctab newp rel_consts' - (more_rejects @ rejects)) + map #1 newrels @ + relevant_clauses ctxt follow_defs max_new relevance_override thy ctab + newp rel_consts' (more_rejects @ rejects) end - | relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) = - let val weight = clause_weight ctab rel_consts consts_typs + | relevant (newrels, rejects) + ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) = + let + val weight = if member Thm.eq_thm del_thms thm then 0.0 + else if member Thm.eq_thm add_thms thm then 1.0 + else if only then 0.0 + else clause_weight ctab rel_consts consts_typs in if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts) then (trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ @@ -280,12 +295,12 @@ else relevant (newrels, ax::rejects) axs end in trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p)); - relevant ([],[]) + relevant ([],[]) end; -fun relevance_filter relevance_threshold follow_defs max_new add_theory_const - thy axioms goals = - if relevance_threshold >= 0.1 then +fun relevance_filter ctxt relevance_threshold follow_defs max_new + add_theory_const relevance_override thy axioms goals = + if relevance_threshold > 0.0 then let val const_tab = List.foldl (count_axiom_consts add_theory_const thy) Symtab.empty axioms @@ -294,8 +309,8 @@ trace_msg (fn () => "Initial constants: " ^ commas (Symtab.keys goal_const_tab)) val relevant = - relevant_clauses follow_defs max_new thy const_tab - relevance_threshold goal_const_tab + relevant_clauses ctxt follow_defs max_new relevance_override thy + const_tab relevance_threshold goal_const_tab (map (pair_consts_typs_axiom add_theory_const thy) axioms) in @@ -534,7 +549,8 @@ | SOME b => not b fun get_relevant_facts relevance_threshold higher_order follow_defs max_new - add_theory_const (ctxt, (chain_ths, th)) goal_cls = + add_theory_const relevance_override + (ctxt, (chain_ths, th)) goal_cls = let val thy = ProofContext.theory_of ctxt val is_FO = is_first_order thy higher_order goal_cls @@ -543,14 +559,18 @@ |> restrict_to_logic thy is_FO |> remove_unwanted_clauses in - relevance_filter relevance_threshold follow_defs max_new add_theory_const - thy included_cls (map prop_of goal_cls) + relevance_filter ctxt relevance_threshold follow_defs max_new + add_theory_const relevance_override thy included_cls + (map prop_of goal_cls) end; (* prepare for passing to writer, create additional clauses based on the information from extra_cls *) fun prepare_clauses higher_order dfg goal_cls chain_ths axcls extra_cls thy = let +(* ### *) +val _ = priority ("prepare clauses: axiom " ^ Int.toString (length axcls) ^ + ", extra " ^ Int.toString (length extra_cls)) (* add chain thms *) val chain_cls = cnf_rules_pairs thy (filter check_named (map pairname chain_ths)) diff -r 0fce6db7babd -r f8c738abaed8 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Mar 23 14:43:22 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Mar 24 12:30:33 2010 +0100 @@ -21,23 +21,25 @@ structure K = OuterKeyword and P = OuterParse -datatype facta = Facta of {add: Facts.ref list, del: Facts.ref list, only: bool} - -fun add_to_facta ns = Facta {add = ns, del = [], only = false}; -fun del_from_facta ns = Facta {add = [], del = ns, only = false}; -fun only_facta ns = Facta {add = ns, del = [], only = true}; -val default_facta = add_to_facta [] -fun merge_facta_pairwise (Facta f1) (Facta f2) = - Facta {add = #add f1 @ #add f2, del = #del f1 @ #del f2, - only = #only f1 orelse #only f2} -fun merge_facta fs = fold merge_facta_pairwise fs default_facta +fun add_to_relevance_override ns : relevance_override = + {add = ns, del = [], only = false} +fun del_from_relevance_override ns : relevance_override = + {add = [], del = ns, only = false} +fun only_relevance_override ns : relevance_override = + {add = ns, del = [], only = true} +val default_relevance_override = add_to_relevance_override [] +fun merge_relevance_override_pairwise r1 r2 : relevance_override = + {add = #add r1 @ #add r2, del = #del r1 @ #del r2, + only = #only r1 orelse #only r2} +fun merge_relevance_overrides rs = + fold merge_relevance_override_pairwise rs default_relevance_override type raw_param = string * string list val default_default_params = [("debug", "false"), ("verbose", "false"), - ("relevance_threshold", "0.5"), + ("relevance_threshold", "50"), ("higher_order", "smart"), ("respect_no_atp", "true"), ("follow_defs", "false"), @@ -105,15 +107,19 @@ the_timeout (case lookup name of NONE => NONE | SOME s => parse_time_option name s) - fun lookup_real name = + fun lookup_int name = case lookup name of - NONE => 0.0 - | SOME s => 0.0 (* FIXME ### *) + NONE => 0 + | SOME s => case Int.fromString s of + SOME n => n + | NONE => error ("Parameter " ^ quote name ^ + " must be assigned an integer value.") val debug = lookup_bool "debug" val verbose = debug orelse lookup_bool "verbose" val atps = lookup_string "atps" |> space_explode " " val full_types = lookup_bool "full_types" - val relevance_threshold = lookup_real "relevance_threshold" + val relevance_threshold = + 0.01 * Real.fromInt (lookup_int "relevance_threshold") val higher_order = lookup_bool_option "higher_order" val respect_no_atp = lookup_bool "respect_no_atp" val follow_defs = lookup_bool "follow_defs" @@ -180,15 +186,16 @@ val delN = "del" val onlyN = "only" -fun hammer_away override_params subcommand opt_i (Facta f) state = +fun hammer_away override_params subcommand opt_i relevance_override state = let val thy = Proof.theory_of state val _ = List.app check_raw_param override_params in if subcommand = runN then - sledgehammer (get_params thy override_params) (the_default 1 opt_i) state + sledgehammer (get_params thy override_params) (the_default 1 opt_i) + relevance_override state else if subcommand = minimizeN then - atp_minimize_command override_params [] (#add f) state + atp_minimize_command override_params [] (#add relevance_override) state else if subcommand = messagesN then messages opt_i else if subcommand = available_atpsN then @@ -203,8 +210,9 @@ error ("Unknown subcommand: " ^ quote subcommand ^ ".") end -fun sledgehammer_trans (((params, subcommand), opt_i), facta) = - Toplevel.keep (hammer_away params subcommand opt_i facta o Toplevel.proof_of) +fun sledgehammer_trans (((subcommand, params), relevance_override), opt_i) = + Toplevel.keep (hammer_away params subcommand opt_i relevance_override + o Toplevel.proof_of) fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value @@ -221,32 +229,35 @@ |> sort_strings |> cat_lines))))) val parse_key = Scan.repeat1 P.typ_group >> space_implode " " -val parse_value = - Scan.repeat1 (P.minus >> single - || Scan.repeat1 (Scan.unless P.minus P.name)) >> flat +val parse_value = Scan.repeat1 P.xname val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) [] val parse_params = Scan.optional (Args.bracks (P.list parse_param)) [] val parse_fact_refs = - Scan.repeat (P.xname -- Scan.option Attrib.thm_sel - >> (fn (name, interval) => - Facts.Named ((name, Position.none), interval))) -val parse_slew = - (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_facta) - || (Args.del |-- Args.colon |-- parse_fact_refs >> del_from_facta) - || (P.$$$ onlyN |-- Args.colon |-- parse_fact_refs >> only_facta) -val parse_facta = - Args.parens (Scan.optional (parse_fact_refs >> only_facta) default_facta - -- Scan.repeat parse_slew) >> op :: >> merge_facta + Scan.repeat1 (Scan.unless (P.name -- Args.colon) + (P.xname -- Scan.option Attrib.thm_sel) + >> (fn (name, interval) => + Facts.Named ((name, Position.none), interval))) +val parse_relevance_chunk = + (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override) + || (Args.del |-- Args.colon |-- parse_fact_refs + >> del_from_relevance_override) + || (P.$$$ onlyN |-- Args.colon |-- parse_fact_refs >> only_relevance_override) +val parse_relevance_override = + Scan.optional (Args.parens + (Scan.optional (parse_fact_refs >> only_relevance_override) + default_relevance_override + -- Scan.repeat parse_relevance_chunk) + >> op :: >> merge_relevance_overrides) + default_relevance_override val parse_sledgehammer_command = - (parse_params -- Scan.optional P.name runN -- Scan.option P.nat - -- parse_facta) - #>> sledgehammer_trans + (Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override + -- Scan.option P.nat) #>> sledgehammer_trans val parse_sledgehammer_params_command = parse_params #>> sledgehammer_params_trans val parse_minimize_args = - Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) [] - + Scan.optional (Args.bracks (P.list (P.short_ident --| P.$$$ "=" -- P.xname))) + [] val _ = OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_atps)) diff -r 0fce6db7babd -r f8c738abaed8 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Mar 23 14:43:22 2010 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Mar 24 12:30:33 2010 +0100 @@ -339,18 +339,18 @@ let val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n") val string_of_term = PrintMode.setmp [] (Syntax.string_of_term ctxt) - fun have_or_show "show" _ = "show \"" - | have_or_show have lname = have ^ " " ^ lname ^ ": \"" + fun have_or_show "show" _ = " show \"" + | have_or_show have lname = " " ^ have ^ " " ^ lname ^ ": \"" fun do_line _ (lname, t, []) = (* No deps: it's a conjecture clause, with no proof. *) (case permuted_clause t ctms of - SOME u => "assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n" + SOME u => " assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n" | NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body", [t])) | do_line have (lname, t, deps) = have_or_show have lname ^ string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^ - "\"\n by (metis " ^ space_implode " " deps ^ ")\n" + "\"\n by (metis " ^ space_implode " " deps ^ ")\n" fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)] | do_lines ((lname, t, deps) :: lines) = do_line "have" (lname, t, deps) :: do_lines lines @@ -535,19 +535,20 @@ val kill_chained = filter_out (curry (op =) chained_hint) (* metis-command *) -fun metis_line [] = "apply metis" - | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")" +fun metis_line [] = "by metis" + | metis_line xs = "by (metis " ^ space_implode " " xs ^ ")" -(* atp_minimize [atp=] *) fun minimize_line _ [] = "" | minimize_line name lemmas = "To minimize the number of lemmas, try this command:\n" ^ - Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^ - space_implode " " (kill_chained lemmas)) + Markup.markup Markup.sendback + ("sledgehammer minimize [atps = " ^ name ^ "] (" ^ + space_implode " " (kill_chained lemmas) ^ ")") ^ "." fun metis_lemma_list dfg name result = let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in - (Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ "\n" ^ + ("Try this command: " ^ + Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ ".\n" ^ minimize_line name lemmas ^ (if used_conj then ""