if "debug" is on, print list of relevant facts (poweruser request);
internal renaming
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Oct 26 21:01:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Oct 26 21:34:01 2010 +0200
@@ -169,8 +169,8 @@
sort_strings (available_atps thy) @ smt_prover_names
|> List.partition (String.isPrefix remote_prefix)
in
- Output.urgent_message ("Available provers: " ^ commas (local_provers @ remote_provers) ^
- ".")
+ Output.urgent_message ("Available provers: " ^
+ commas (local_provers @ remote_provers) ^ ".")
end
fun kill_provers () = Async_Manager.kill_threads das_Tool "provers"
@@ -254,6 +254,8 @@
| dest_Untranslated (Translated _) = raise Fail "dest_Untranslated"
fun translated_fact ctxt (Untranslated p) = translate_fact ctxt p
| translated_fact _ (Translated p) = p
+fun fact_name (Untranslated ((name, _), _)) = SOME name
+ | fact_name (Translated (_, p)) = Option.map (fst o fst) p
fun int_option_add (SOME m) (SOME n) = SOME (m + n)
| int_option_add _ _ = NONE
@@ -490,7 +492,7 @@
(false, state))
end
-fun run_sledgehammer (params as {blocking, provers, full_types,
+fun run_sledgehammer (params as {blocking, debug, provers, full_types,
relevance_thresholds, max_relevant, ...})
auto i (relevance_override as {only, ...}) minimize_command
state =
@@ -508,7 +510,7 @@
val _ = () |> not blocking ? kill_provers
val _ = if auto then () else Output.urgent_message "Sledgehammering..."
val (smts, atps) = provers |> List.partition is_smt_prover
- fun run_provers full_types irrelevant_consts relevance_fudge
+ fun run_provers label full_types irrelevant_consts relevance_fudge
maybe_translate provers (res as (success, state)) =
if success orelse null provers then
res
@@ -531,6 +533,17 @@
facts = facts, only = only}
val run_prover = run_prover params auto minimize_command
in
+ if debug then
+ Output.urgent_message (label ^ ": " ^
+ (if null facts then
+ "Found no relevant facts."
+ else
+ "Including (up to) " ^ string_of_int (length facts) ^
+ " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
+ (facts |> map_filter fact_name
+ |> space_implode " ") ^ "."))
+ else
+ ();
if auto then
fold (fn prover => fn (true, state) => (true, state)
| (false, _) => run_prover problem prover)
@@ -541,11 +554,11 @@
|> exists fst |> rpair state
end
val run_atps =
- run_provers full_types atp_irrelevant_consts atp_relevance_fudge
+ run_provers "ATPs" full_types atp_irrelevant_consts atp_relevance_fudge
(Translated o translate_fact ctxt) atps
val run_smts =
- run_provers true smt_irrelevant_consts smt_relevance_fudge Untranslated
- smts
+ run_provers "SMT" true smt_irrelevant_consts smt_relevance_fudge
+ Untranslated smts
fun run_atps_and_smt_solvers () =
[run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Oct 26 21:01:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Oct 26 21:34:01 2010 +0200
@@ -34,7 +34,7 @@
only : bool}
val trace : bool Unsynchronized.ref
- val name_thm_pairs_from_ref :
+ val fact_from_ref :
Proof.context -> unit Symtab.table -> thm list
-> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
val relevant_facts :
@@ -90,7 +90,7 @@
(name |> Symtab.defined reserved name ? quote) ^
(if multi then "(" ^ Int.toString j ^ ")" else "")
-fun name_thm_pairs_from_ref ctxt reserved chained_ths (xthm as (xref, args)) =
+fun fact_from_ref ctxt reserved chained_ths (xthm as (xref, args)) =
let
val ths = Attrib.eval_thms ctxt [xthm]
val bracket =
@@ -522,12 +522,10 @@
(*Reject theorems with names like "List.filter.filter_list_def" or
"Accessible_Part.acc.defs", as these are definitions arising from packages.*)
fun is_package_def a =
- let val names = Long_Name.explode a
- in
- length names > 2 andalso
- not (hd names = "local") andalso
- String.isSuffix "_def" a orelse String.isSuffix "_defs" a
- end;
+ let val names = Long_Name.explode a in
+ (length names > 2 andalso not (hd names = "local") andalso
+ String.isSuffix "_def" a) orelse String.isSuffix "_defs" a
+ end
fun mk_fact_table f xs =
fold (Termtab.update o `(prop_of o f)) xs Termtab.empty
@@ -690,9 +688,9 @@
(Term.add_vars t [] |> sort_wrt (fst o fst))
|> fst
-fun all_name_thms_pairs ctxt reserved full_types
- ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge) add_ths
- chained_ths =
+fun all_facts ctxt reserved full_types
+ ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge)
+ add_ths chained_ths =
let
val thy = ProofContext.theory_of ctxt
val global_facts = Global_Theory.facts_of thy
@@ -777,7 +775,7 @@
(* The single-name theorems go after the multiple-name ones, so that single
names are preferred when both are available. *)
-fun name_thm_pairs ctxt respect_no_atp =
+fun rearrange_facts ctxt respect_no_atp =
List.partition (fst o snd) #> op @ #> map (apsnd snd)
#> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd)
@@ -796,10 +794,10 @@
val facts =
(if only then
maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
- o name_thm_pairs_from_ref ctxt reserved chained_ths) add
+ o fact_from_ref ctxt reserved chained_ths) add
else
- all_name_thms_pairs ctxt reserved full_types fudge add_ths chained_ths)
- |> name_thm_pairs ctxt (respect_no_atp andalso not only)
+ all_facts ctxt reserved full_types fudge add_ths chained_ths)
+ |> rearrange_facts ctxt (respect_no_atp andalso not only)
|> uniquify
in
trace_msg (fn () => "Considering " ^ Int.toString (length facts) ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Oct 26 21:01:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Oct 26 21:34:01 2010 +0200
@@ -141,8 +141,7 @@
val reserved = reserved_isar_keyword_table ()
val chained_ths = #facts (Proof.goal state)
val facts =
- maps (map (apsnd single)
- o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
+ maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths) refs
in
case subgoal_count state of
0 => Output.urgent_message "No subgoal!"