# HG changeset patch
# User blanchet
# Date 1354812484 -3600
# Node ID e83ab94e3e6eeece73cf9a8b1b6df43c1dd58492
# Parent  c9023d78d1a6b3ca47161d696232978f063e027d
use proper entry point for MaSh in test driver

diff -r c9023d78d1a6 -r e83ab94e3e6e src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Thu Dec 06 16:49:48 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Thu Dec 06 17:48:04 2012 +0100
@@ -23,8 +23,6 @@
 val MeshN = "Mesh"
 val IsarN = "Isar"
 
-val max_facts_slack = 2
-
 val all_names = map (rpair () o nickname_of) #> Symtab.make
 
 fun evaluate_mash_suggestions ctxt params file_name =
@@ -32,7 +30,7 @@
     val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} =
       Sledgehammer_Isar.default_params ctxt []
     val prover = hd provers
-    val slack_max_facts = max_facts_slack * the max_facts
+    val slack_max_facts = generous_max_facts (the max_facts)
     val path = file_name |> Path.explode
     val lines = path |> File.read_lines
     val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
@@ -78,10 +76,12 @@
           Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
               slack_max_facts NONE hyp_ts concl_t facts
           |> Sledgehammer_MePo.weight_mepo_facts
-        val mash_facts = suggested_facts suggs facts
+        val mash_facts =
+          find_mash_suggestions slack_max_facts suggs facts [] []
+          |> weight_mash_facts
         val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, []))]
         val mesh_facts = mesh_facts slack_max_facts mess
-        val isar_facts = suggested_facts (map (rpair 1.0) isar_deps) facts
+        val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts
         fun prove ok heading get facts =
           let
             val facts =
diff -r c9023d78d1a6 -r e83ab94e3e6e src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 16:49:48 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 17:48:04 2012 +0100
@@ -41,7 +41,7 @@
     -> (string * real) list
   val mash_unlearn : Proof.context -> unit
   val nickname_of : thm -> string
-  val suggested_facts :
+  val find_suggested_facts :
     (string * 'a) list -> ('b * thm) list -> (('b * thm) * 'a) list
   val mesh_facts :
     int -> (real * ((('a * thm) * real) list * ('a * thm) list)) list
@@ -59,6 +59,9 @@
     Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
     -> thm -> bool * string list option
   val weight_mash_facts : ('a * thm) list -> (('a * thm) * real) list
+  val find_mash_suggestions :
+    int -> (Symtab.key * 'a) list -> ('b * thm) list -> ('b * thm) list
+    -> ('b * thm) list -> ('b * thm) list
   val mash_suggested_facts :
     Proof.context -> params -> string -> int -> term list -> term -> fact list
     -> fact list
@@ -69,6 +72,7 @@
     Proof.context -> params -> fact_override -> thm list -> bool -> unit
   val is_mash_enabled : unit -> bool
   val mash_can_suggest_facts : Proof.context -> bool
+  val generous_max_facts : int -> int
   val relevant_facts :
     Proof.context -> params -> string -> int -> fact_override -> term list
     -> term -> fact list -> fact list
@@ -410,7 +414,7 @@
   else
     backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th
 
-fun suggested_facts suggs facts =
+fun find_suggested_facts suggs facts =
   let
     fun add_fact (fact as (_, th)) = Symtab.default (nickname_of th, fact)
     val tab = Symtab.empty |> fold add_fact facts
@@ -732,6 +736,20 @@
 fun weight_proximity_facts facts =
   facts ~~ map weight_of_proximity_fact (0 upto length facts - 1)
 
+fun find_mash_suggestions max_facts suggs facts chained unknown =
+  let
+    val raw_mash =
+      facts |> find_suggested_facts suggs
+            (* The weights currently returned by "mash.py" are too spaced out to
+               make any sense. *)
+            |> map fst
+    val proximity = facts |> sort (thm_ord o pairself snd o swap)
+    val mess =
+      [(0.8000 (* FUDGE *), (map (rpair 1.0) chained, [])),
+       (0.1333 (* FUDGE *), (weight_raw_mash_facts raw_mash, unknown)),
+       (0.0667 (* FUDGE *), (weight_proximity_facts proximity, []))]
+  in mesh_facts max_facts mess end
+
 fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
                          concl_t facts =
   let
@@ -749,18 +767,8 @@
               (fact_G, mash_QUERY ctxt overlord max_facts (parents, feats))
             end)
     val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
-    val raw_mash =
-      facts |> suggested_facts suggs
-            (* The weights currently returned by "mash.py" are too spaced out to
-               make any sense. *)
-            |> map fst
-    val proximity = facts |> sort (thm_ord o pairself snd o swap)
     val unknown = facts |> filter_out (is_fact_in_graph fact_G)
-    val mess =
-      [(0.8000 (* FUDGE *), (map (rpair 1.0) chained, [])),
-       (0.1333 (* FUDGE *), (weight_raw_mash_facts raw_mash, unknown)),
-       (0.0667 (* FUDGE *), (weight_proximity_facts proximity, []))]
-  in mesh_facts max_facts mess end
+  in find_mash_suggestions max_facts suggs facts chained unknown end
 
 fun add_wrt_fact_graph ctxt (name, parents, feats, deps) (adds, graph) =
   let