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
--- 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))
--- 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))
--- 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=<prover>] <lemmas> *)
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
""