--- 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 =
--- 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 =
--- 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"
--- 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
())