# HG changeset patch
# User blanchet
# Date 1359651245 -3600
# Node ID 198cb05fb35b5c42effde95cbdc49e194fa7fd11
# Parent  496013a6eb38fc236d2539b8a1653fceb6cb13fe
report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices

diff -r 496013a6eb38 -r 198cb05fb35b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jan 31 17:42:12 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -477,6 +477,7 @@
           |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name
                  (the_default default_max_facts max_facts)
                  Sledgehammer_Fact.no_fact_override hyp_ts concl_t
+          |> #1 (*###*)
           |> map (apfst (apfst (fn name => name ())))
           |> tap (fn facts =>
                      "Line " ^ str0 (Position.line_of pos) ^ ": " ^
diff -r 496013a6eb38 -r 198cb05fb35b src/HOL/TPTP/sledgehammer_tactics.ML
--- a/src/HOL/TPTP/sledgehammer_tactics.ML	Thu Jan 31 17:42:12 2013 +0100
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -42,6 +42,7 @@
       |> relevant_facts ctxt params name
              (the_default default_max_facts max_facts) fact_override hyp_ts
              concl_t
+      |> #1
     val problem =
       {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
        facts = facts |> map (apfst (apfst (fn name => name ())))
diff -r 496013a6eb38 -r 198cb05fb35b src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 31 17:42:12 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -85,7 +85,7 @@
   val mash_weight : real
   val relevant_facts :
     Proof.context -> params -> string -> int -> fact_override -> term list
-    -> term -> fact list -> fact list
+    -> term -> fact list -> fact list * fact list * fact list
   val kill_learners : unit -> unit
   val running_learners : unit -> unit
 end;
@@ -1099,9 +1099,9 @@
   if not (subset (op =) (the_list fact_filter, fact_filters)) then
     error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
   else if only then
-    facts
+    (facts, facts, facts)
   else if max_facts <= 0 orelse null facts then
-    []
+    ([], [], [])
   else
     let
       fun maybe_learn () =
@@ -1129,9 +1129,11 @@
           else
             mepoN
       val add_ths = Attrib.eval_thms ctxt add
-      fun prepend_facts ths accepts =
-        ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
-         (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
+      val in_add = member Thm.eq_thm_prop add_ths o snd
+      fun add_and_take accepts =
+        (case add_ths of
+           [] => accepts
+         | _ => (facts |> filter in_add) @ (accepts |> filter_out in_add))
         |> take max_facts
       fun mepo () =
         mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t
@@ -1142,13 +1144,19 @@
             hyp_ts concl_t facts
         |>> weight_mash_facts
       val mess =
-        [] |> (if fact_filter <> mashN then cons (mepo_weight, (mepo (), []))
+        (* the order is important for the "case" expression below *)
+        [] |> (if fact_filter <> mepoN then cons (mash_weight, (mash ()))
                else I)
-           |> (if fact_filter <> mepoN then cons (mash_weight, (mash ()))
+           |> (if fact_filter <> mashN then cons (mepo_weight, (mepo (), []))
                else I)
+      val mesh =
+        mesh_facts (Thm.eq_thm_prop o pairself snd) max_facts mess
+        |> add_and_take
     in
-      mesh_facts (Thm.eq_thm_prop o pairself snd) max_facts mess
-      |> not (null add_ths) ? prepend_facts add_ths
+      case mess of
+        [(_, (mepo, _)), (_, (mash, _))] =>
+        (mesh, mepo |> map fst |> add_and_take, mash |> map fst |> add_and_take)
+      | _ => (mesh, mesh, mesh)
     end
 
 fun kill_learners () = Async_Manager.kill_threads MaShN "learner"
diff -r 496013a6eb38 -r 198cb05fb35b src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jan 31 17:42:12 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Jan 31 17:54:05 2013 +0100
@@ -236,6 +236,7 @@
               | NONE => I)
           |> relevant_facts ctxt params (hd provers) max_max_facts fact_override
                             hyp_ts concl_t
+          |> #1 (*###*)
           |> map (apfst (apfst (fn name => name ())))
           |> tap (fn facts =>
                      if verbose then