# HG changeset patch
# User blanchet
# Date 1342593844 -7200
# Node ID b40722a81ac9a0ee8621583770e76aa9713f9e27
# Parent  3c4e10606567542b4e93d2c5222569bdc7d46a82
implemented meshing of Iter and MaSh results

diff -r 3c4e10606567 -r b40722a81ac9 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -41,24 +41,8 @@
     val isar_ok = Unsynchronized.ref 0
     fun sugg_facts hyp_ts concl_t suggs =
       suggested_facts suggs
-      #> take (max_facts_slack * the max_facts)
-      #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
-    fun mesh_facts fsp =
-      let
-        val (fs1, fs2) =
-          fsp |> pairself (map (apfst (apfst (fn name => name ()))))
-        val fact_eq = (op =) o pairself fst
-        fun score_in f fs =
-          case find_index (curry fact_eq f) fs of
-            ~1 => length fs
-          | j => j
-        fun score_of f = score_in f fs1 + score_in f fs2
-      in
-        union fact_eq fs1 fs2
-        |> map (`score_of) |> sort (int_ord o pairself fst) |> map snd
-        |> take (the max_facts)
-        |> map (apfst (apfst K))
-      end
+      #> chop (max_facts_slack * the max_facts)
+      #>> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
     fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
     fun index_string (j, s) = s ^ "@" ^ string_of_int j
     fun str_of_res label facts {outcome, run_time, used_facts, ...} =
@@ -97,13 +81,15 @@
         val goal = goal_of_thm thy th
         val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
         val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
-        val isar_facts = facts |> sugg_facts hyp_ts concl_t isar_deps
+        val (isar_facts, _) = facts |> sugg_facts hyp_ts concl_t isar_deps
         val iter_facts =
           Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
               prover_name (max_facts_slack * the max_facts) NONE hyp_ts concl_t
               facts
-        val mash_facts = facts |> sugg_facts hyp_ts concl_t suggs
-        val mesh_facts = mesh_facts (iter_facts, mash_facts)
+        val (mash_facts, mash_rejects) =
+          facts |> sugg_facts hyp_ts concl_t suggs
+        val mesh_facts =
+          mesh_facts (the max_facts) iter_facts mash_facts mash_rejects
         val iter_s = prove iter_ok iterN iter_facts goal
         val mash_s = prove mash_ok mashN mash_facts goal
         val mesh_s = prove mesh_ok meshN mesh_facts goal
diff -r 3c4e10606567 -r b40722a81ac9 src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Wed Jul 18 08:44:04 2012 +0200
@@ -20,12 +20,13 @@
   val unescape_meta : string -> string
   val unescape_metas : string -> string list
   val extract_query : string -> string * string list
-  val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
+  val suggested_facts : string list -> fact list -> fact list
+  val mesh_facts : int -> fact list -> fact list -> fact list -> fact list
   val all_non_tautological_facts_of :
     theory -> status Termtab.table -> fact list
   val theory_ord : theory * theory -> order
   val thm_ord : thm * thm -> order
-  val thy_facts_from_thms : ('a * thm) list -> string list Symtab.table
+  val thy_facts_from_thms : fact list -> string list Symtab.table
   val has_thy : theory -> thm -> bool
   val parent_facts : theory -> string list Symtab.table -> string list
   val features_of : theory -> status -> term list -> string list
@@ -99,12 +100,29 @@
 fun extract_query line =
   case space_explode ":" line of
     [goal_name, suggs] => (unescape_meta goal_name, explode_suggs suggs)
-  | _ => ("", explode_suggs line)
+  | _ => ("", [])
 
 fun find_suggested facts sugg =
   find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
 fun suggested_facts suggs facts = map_filter (find_suggested facts) suggs
 
+fun mesh_facts max_facts iter_facts mash_facts mash_rejects =
+  let
+    val fact_eq = Thm.eq_thm o pairself snd
+    val num_iter = length iter_facts
+    val num_mash = length mash_facts
+    fun score_in f fs n =
+      case find_index (curry fact_eq f) fs of
+        ~1 => length fs
+      | j => j
+    fun score_of fact =
+      score_in fact iter_facts num_iter + score_in fact mash_facts num_mash
+  in
+    union fact_eq iter_facts mash_facts
+    |> map (`score_of) |> sort (int_ord o pairself fst) |> map snd
+    |> take max_facts
+  end
+
 val thy_feature_prefix = "y_"
 
 val thy_feature_name_of = prefix thy_feature_prefix
@@ -506,12 +524,11 @@
       val iter_facts =
         iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts
                                  concl_t facts
-      val (mash_facts, mash_antifacts) =
+      val (mash_facts, mash_rejects) =
         facts |> mash_suggest_facts ctxt params prover hyp_ts concl_t
               |> chop max_facts
-      val mesh_facts = iter_facts (* ### *)
     in
-      mesh_facts
+      mesh_facts max_facts iter_facts mash_facts mash_rejects
       |> not (null add_ths) ? prepend_facts add_ths
     end