# HG changeset patch
# User blanchet
# Date 1288121641 -7200
# Node ID 277508b0741802f7ed15e371c433de1237822791
# Parent  da97d75e20e6f6ff445bddcdb9d2c1a69c4a23f3
if "debug" is on, print list of relevant facts (poweruser request);
internal renaming

diff -r da97d75e20e6 -r 277508b07418 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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
diff -r da97d75e20e6 -r 277508b07418 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- 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) ^
diff -r da97d75e20e6 -r 277508b07418 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- 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!"