# HG changeset patch
# User blanchet
# Date 1359651245 -3600
# Node ID e096c0dc538b6a1f723798e448549aa33851cda8
# Parent  4f694d52bf625fa9f8c2868876f16d5bdb61d4dc
more precise output of selected facts

diff -r 4f694d52bf62 -r e096c0dc538b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -479,14 +479,9 @@
           |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name
                  (the_default default_max_facts max_facts)
                  Sledgehammer_Fact.no_fact_override hyp_ts concl_t
-          |> tap (fn (facts, _, _) => (* FIXME *)
+          |> tap (fn fact_triple =>
                      "Line " ^ str0 (Position.line_of pos) ^ ": " ^
-                     (if null facts then
-                        "Found no relevant facts."
-                      else
-                        "Including " ^ string_of_int (length facts) ^
-                        " relevant fact(s):\n" ^
-                        (facts |> map (fst o fst) |> space_implode " ") ^ ".")
+                     Sledgehammer_Run.string_of_fact_triple fact_triple
                      |> Output.urgent_message)
         val prover = get_prover ctxt prover_name params goal facts
         val problem =
diff -r 4f694d52bf62 -r e096c0dc538b src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -9,7 +9,6 @@
 sig
   type params = Sledgehammer_Provers.params
 
-  val MePoN : string
   val MaSh_IsarN : string
   val MaSh_ProverN : string
   val MeSh_IsarN : string
@@ -30,11 +29,10 @@
 open Sledgehammer_Provers
 open Sledgehammer_Isar
 
-val MePoN = "MePo"
-val MaSh_IsarN = "MaSh-Isar"
-val MaSh_ProverN = "MaSh-Prover"
-val MeSh_IsarN = "MeSh-Isar"
-val MeSh_ProverN = "MeSh-Prover"
+val MaSh_IsarN = MaShN ^ "-Isar"
+val MaSh_ProverN = MaShN ^ "-Prover"
+val MeSh_IsarN = MeShN ^ "-Isar"
+val MeSh_ProverN = MeShN ^ "-Prover"
 val IsarN = "Isar"
 
 fun in_range (from, to) j =
diff -r 4f694d52bf62 -r e096c0dc538b src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -15,7 +15,9 @@
   type prover_result = Sledgehammer_Provers.prover_result
 
   val trace : bool Config.T
+  val MePoN : string
   val MaShN : string
+  val MeShN : string
   val mepoN : string
   val mashN : string
   val meshN : string
@@ -106,7 +108,9 @@
   Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 
+val MePoN = "MePo"
 val MaShN = "MaSh"
+val MeShN = "MeSh"
 
 val mepoN = "mepo"
 val mashN = "mash"
diff -r 4f694d52bf62 -r e096c0dc538b src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -8,6 +8,7 @@
 
 signature SLEDGEHAMMER_RUN =
 sig
+  type fact = Sledgehammer_Fact.fact
   type fact_override = Sledgehammer_Fact.fact_override
   type minimize_command = Sledgehammer_Reconstruct.minimize_command
   type mode = Sledgehammer_Provers.mode
@@ -17,6 +18,7 @@
   val noneN : string
   val timeoutN : string
   val unknownN : string
+  val string_of_fact_triple : fact list * fact list * fact list -> string
   val run_sledgehammer :
     params -> mode -> int -> fact_override
     -> ((string * string list) list -> string -> minimize_command)
@@ -164,6 +166,22 @@
 
 val auto_try_max_facts_divisor = 2 (* FUDGE *)
 
+fun string_of_facts facts =
+  "Including " ^ string_of_int (length facts) ^
+  " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
+  (facts |> map (fst o fst) |> space_implode " ") ^ "."
+
+fun eq_facts p = eq_list (op = o pairself fst) p
+
+fun string_of_fact_triple ([], [], []) = "Found no relevant facts."
+  | string_of_fact_triple (mesh, mepo, mash) =
+    if eq_facts (mesh, mepo) andalso eq_facts (mesh, mash) then
+      string_of_facts mesh
+    else
+      MeShN ^ ": " ^ string_of_facts mesh ^ "\n\n" ^
+      MePoN ^ ": " ^ string_of_facts mepo ^ "\n\n" ^
+      MaShN ^ ": " ^ string_of_facts mash
+
 fun run_sledgehammer (params as {debug, verbose, blocking, provers, max_facts,
                                  slice, ...})
         mode i (fact_override as {only, ...}) minimize_command state =
@@ -210,15 +228,10 @@
               | NONE => I)
           |> relevant_facts ctxt params (hd provers) max_max_facts fact_override
                             hyp_ts concl_t
-          |> tap (fn (facts, _, _) => (* FIXME *)
+          |> tap (fn fact_triple =>
                      if verbose then
                        label ^ plural_s (length provers) ^ ": " ^
-                       (if null facts then
-                          "Found no relevant facts."
-                        else
-                          "Including " ^ string_of_int (length facts) ^
-                          " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
-                          (facts |> map (fst o fst) |> space_implode " ") ^ ".")
+                       string_of_fact_triple fact_triple
                        |> print
                      else
                        ())