1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 21:01:28 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 21:34:01 2010 +0200
     1.3 @@ -169,8 +169,8 @@
     1.4        sort_strings (available_atps thy) @ smt_prover_names
     1.5        |> List.partition (String.isPrefix remote_prefix)
     1.6    in
     1.7 -    Output.urgent_message ("Available provers: " ^ commas (local_provers @ remote_provers) ^
     1.8 -              ".")
     1.9 +    Output.urgent_message ("Available provers: " ^
    1.10 +                           commas (local_provers @ remote_provers) ^ ".")
    1.11    end
    1.12  
    1.13  fun kill_provers () = Async_Manager.kill_threads das_Tool "provers"
    1.14 @@ -254,6 +254,8 @@
    1.15    | dest_Untranslated (Translated _) = raise Fail "dest_Untranslated"
    1.16  fun translated_fact ctxt (Untranslated p) = translate_fact ctxt p
    1.17    | translated_fact _ (Translated p) = p
    1.18 +fun fact_name (Untranslated ((name, _), _)) = SOME name
    1.19 +  | fact_name (Translated (_, p)) = Option.map (fst o fst) p
    1.20  
    1.21  fun int_option_add (SOME m) (SOME n) = SOME (m + n)
    1.22    | int_option_add _ _ = NONE
    1.23 @@ -490,7 +492,7 @@
    1.24         (false, state))
    1.25    end
    1.26  
    1.27 -fun run_sledgehammer (params as {blocking, provers, full_types,
    1.28 +fun run_sledgehammer (params as {blocking, debug, provers, full_types,
    1.29                                   relevance_thresholds, max_relevant, ...})
    1.30                       auto i (relevance_override as {only, ...}) minimize_command
    1.31                       state =
    1.32 @@ -508,7 +510,7 @@
    1.33        val _ = () |> not blocking ? kill_provers
    1.34        val _ = if auto then () else Output.urgent_message "Sledgehammering..."
    1.35        val (smts, atps) = provers |> List.partition is_smt_prover
    1.36 -      fun run_provers full_types irrelevant_consts relevance_fudge
    1.37 +      fun run_provers label full_types irrelevant_consts relevance_fudge
    1.38                        maybe_translate provers (res as (success, state)) =
    1.39          if success orelse null provers then
    1.40            res
    1.41 @@ -531,6 +533,17 @@
    1.42                 facts = facts, only = only}
    1.43              val run_prover = run_prover params auto minimize_command
    1.44            in
    1.45 +            if debug then
    1.46 +              Output.urgent_message (label ^ ": " ^
    1.47 +                  (if null facts then
    1.48 +                     "Found no relevant facts."
    1.49 +                   else
    1.50 +                     "Including (up to) " ^ string_of_int (length facts) ^
    1.51 +                     " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
    1.52 +                     (facts |> map_filter fact_name
    1.53 +                            |> space_implode " ") ^ "."))
    1.54 +            else
    1.55 +              ();
    1.56              if auto then
    1.57                fold (fn prover => fn (true, state) => (true, state)
    1.58                                    | (false, _) => run_prover problem prover)
    1.59 @@ -541,11 +554,11 @@
    1.60                        |> exists fst |> rpair state
    1.61            end
    1.62        val run_atps =
    1.63 -        run_provers full_types atp_irrelevant_consts atp_relevance_fudge
    1.64 +        run_provers "ATPs" full_types atp_irrelevant_consts atp_relevance_fudge
    1.65                      (Translated o translate_fact ctxt) atps
    1.66        val run_smts =
    1.67 -        run_provers true smt_irrelevant_consts smt_relevance_fudge Untranslated
    1.68 -                    smts
    1.69 +        run_provers "SMT" true smt_irrelevant_consts smt_relevance_fudge
    1.70 +                    Untranslated smts
    1.71        fun run_atps_and_smt_solvers () =
    1.72          [run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
    1.73      in

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Oct 26 21:01:28 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Oct 26 21:34:01 2010 +0200
     2.3 @@ -34,7 +34,7 @@
     2.4       only : bool}
     2.5  
     2.6    val trace : bool Unsynchronized.ref
     2.7 -  val name_thm_pairs_from_ref :
     2.8 +  val fact_from_ref :
     2.9      Proof.context -> unit Symtab.table -> thm list
    2.10      -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
    2.11    val relevant_facts :
    2.12 @@ -90,7 +90,7 @@
    2.13    (name |> Symtab.defined reserved name ? quote) ^
    2.14    (if multi then "(" ^ Int.toString j ^ ")" else "")
    2.15  
    2.16 -fun name_thm_pairs_from_ref ctxt reserved chained_ths (xthm as (xref, args)) =
    2.17 +fun fact_from_ref ctxt reserved chained_ths (xthm as (xref, args)) =
    2.18    let
    2.19      val ths = Attrib.eval_thms ctxt [xthm]
    2.20      val bracket =
    2.21 @@ -522,12 +522,10 @@
    2.22  (*Reject theorems with names like "List.filter.filter_list_def" or
    2.23    "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
    2.24  fun is_package_def a =
    2.25 -  let val names = Long_Name.explode a
    2.26 -  in
    2.27 -     length names > 2 andalso
    2.28 -     not (hd names = "local") andalso
    2.29 -     String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a
    2.30 -  end;
    2.31 +  let val names = Long_Name.explode a in
    2.32 +    (length names > 2 andalso not (hd names = "local") andalso
    2.33 +     String.isSuffix "_def" a) orelse String.isSuffix "_defs" a
    2.34 +  end
    2.35  
    2.36  fun mk_fact_table f xs =
    2.37    fold (Termtab.update o `(prop_of o f)) xs Termtab.empty
    2.38 @@ -690,9 +688,9 @@
    2.39            (Term.add_vars t [] |> sort_wrt (fst o fst))
    2.40    |> fst
    2.41  
    2.42 -fun all_name_thms_pairs ctxt reserved full_types
    2.43 -        ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge) add_ths
    2.44 -        chained_ths =
    2.45 +fun all_facts ctxt reserved full_types
    2.46 +              ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge)
    2.47 +              add_ths chained_ths =
    2.48    let
    2.49      val thy = ProofContext.theory_of ctxt
    2.50      val global_facts = Global_Theory.facts_of thy
    2.51 @@ -777,7 +775,7 @@
    2.52  
    2.53  (* The single-name theorems go after the multiple-name ones, so that single
    2.54     names are preferred when both are available. *)
    2.55 -fun name_thm_pairs ctxt respect_no_atp =
    2.56 +fun rearrange_facts ctxt respect_no_atp =
    2.57    List.partition (fst o snd) #> op @ #> map (apsnd snd)
    2.58    #> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd)
    2.59  
    2.60 @@ -796,10 +794,10 @@
    2.61      val facts =
    2.62        (if only then
    2.63           maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
    2.64 -               o name_thm_pairs_from_ref ctxt reserved chained_ths) add
    2.65 +               o fact_from_ref ctxt reserved chained_ths) add
    2.66         else
    2.67 -         all_name_thms_pairs ctxt reserved full_types fudge add_ths chained_ths)
    2.68 -      |> name_thm_pairs ctxt (respect_no_atp andalso not only)
    2.69 +         all_facts ctxt reserved full_types fudge add_ths chained_ths)
    2.70 +      |> rearrange_facts ctxt (respect_no_atp andalso not only)
    2.71        |> uniquify
    2.72    in
    2.73      trace_msg (fn () => "Considering " ^ Int.toString (length facts) ^

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Oct 26 21:01:28 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Oct 26 21:34:01 2010 +0200
     3.3 @@ -141,8 +141,7 @@
     3.4      val reserved = reserved_isar_keyword_table ()
     3.5      val chained_ths = #facts (Proof.goal state)
     3.6      val facts =
     3.7 -      maps (map (apsnd single)
     3.8 -            o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
     3.9 +      maps (map (apsnd single) o fact_from_ref ctxt reserved chained_ths) refs
    3.10    in
    3.11      case subgoal_count state of
    3.12        0 => Output.urgent_message "No subgoal!"