# HG changeset patch
# User blanchet
# Date 1358445193 -3600
# Node ID c4c746bbf8368b5e8821b664a500b89907b53b50
# Parent  3fd83a0cc4bde3bac46b68a2240a904b1b815e81
provide a means to skip a method

diff -r 3fd83a0cc4bd -r c4c746bbf836 src/HOL/TPTP/MaSh_Eval.thy
--- a/src/HOL/TPTP/MaSh_Eval.thy	Thu Jan 17 18:43:59 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Thu Jan 17 18:53:13 2013 +0100
@@ -41,9 +41,10 @@
 
 ML {*
 if do_it then
-  evaluate_mash_suggestions @{context} params (1, NONE) (SOME prob_dir)
-      (prefix ^ "mash_suggestions") (prefix ^ "mash_prover_suggestions")
-      (prefix ^ "mash_eval")
+  evaluate_mash_suggestions @{context} params (1, NONE)
+      [MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN]
+      (SOME prob_dir) (prefix ^ "mash_suggestions")
+      (prefix ^ "mash_prover_suggestions") (prefix ^ "mash_eval")
 else
   ()
 *}
diff -r 3fd83a0cc4bd -r c4c746bbf836 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Thu Jan 17 18:43:59 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Thu Jan 17 18:53:13 2013 +0100
@@ -9,9 +9,15 @@
 sig
   type params = Sledgehammer_Provers.params
 
+  val MePoN : string
+  val MaSh_IsarN : string
+  val MaSh_ProverN : string
+  val MeSh_IsarN : string
+  val MeSh_ProverN : string
+  val IsarN : string
   val evaluate_mash_suggestions :
-    Proof.context -> params -> int * int option -> string option -> string
-    -> string -> string -> unit
+    Proof.context -> params -> int * int option -> string list -> string option
+    -> string -> string -> string -> unit
 end;
 
 structure MaSh_Eval : MASH_EVAL =
@@ -34,7 +40,7 @@
 fun in_range (from, to) j =
   j >= from andalso (to = NONE orelse j <= the to)
 
-fun evaluate_mash_suggestions ctxt params range prob_dir_name
+fun evaluate_mash_suggestions ctxt params range methods prob_dir_name
         isar_sugg_file_name prover_sugg_file_name report_file_name =
   let
     val report_path = report_file_name |> Path.explode
@@ -55,11 +61,11 @@
     val name_tabs = build_name_tables nickname_of_thm facts
     fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
     fun index_str (j, s) = s ^ "@" ^ string_of_int j
-    val str_of_heading = enclose "  " ": "
-    fun str_of_result heading facts ({outcome, run_time, used_facts, ...}
+    val str_of_method = enclose "  " ": "
+    fun str_of_result method facts ({outcome, run_time, used_facts, ...}
                                      : prover_result) =
       let val facts = facts |> map (fn ((name, _), _) => name ()) in
-        str_of_heading heading ^
+        str_of_method method ^
         (if is_none outcome then
            "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
            (used_facts |> map (with_index facts o fst)
@@ -110,20 +116,21 @@
           val isar_facts =
             find_suggested_facts (map (rpair 1.0) isar_deps) facts
           (* adapted from "mirabelle_sledgehammer.ML" *)
-          fun set_file_name heading (SOME dir) =
+          fun set_file_name method (SOME dir) =
               let
                 val prob_prefix =
                   "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^
-                  heading
+                  method
               in
                 Config.put dest_dir dir
                 #> Config.put problem_prefix (prob_prefix ^ "__")
                 #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
               end
             | set_file_name _ NONE = I
-          fun prove heading get facts =
-            if null facts andalso heading <> IsarN then
-              (str_of_heading heading ^ "Skipped", 0)
+          fun prove method get facts =
+            if not (member (op =) methods method) orelse
+               (null facts andalso method <> IsarN) then
+              (str_of_method method ^ "Skipped", 0)
             else
               let
                 fun nickify ((_, stature), th) =
@@ -133,11 +140,11 @@
                   |> map (get #> nickify)
                   |> maybe_instantiate_inducts ctxt hyp_ts concl_t
                   |> take (the max_facts)
-                val ctxt = ctxt |> set_file_name heading prob_dir_name
+                val ctxt = ctxt |> set_file_name method prob_dir_name
                 val res as {outcome, ...} =
                   run_prover_for_mash ctxt params prover facts goal
                 val ok = if is_none outcome then 1 else 0
-              in (str_of_result heading facts res, ok) end
+              in (str_of_result method facts res, ok) end
           val ress =
             [fn () => prove MePoN fst mepo_facts,
              fn () => prove MaSh_IsarN fst mash_isar_facts,
@@ -153,8 +160,8 @@
         end
       else
         [0, 0, 0, 0, 0, 0]
-    fun total_of heading ok n =
-      "  " ^ heading ^ ": " ^ string_of_int ok ^ " (" ^
+    fun total_of method ok n =
+      str_of_method method ^ string_of_int ok ^ " (" ^
       Real.fmt (StringCvt.FIX (SOME 1))
                (100.0 * Real.fromInt ok / Real.fromInt n) ^ "%)"
     val inst_inducts = Config.get ctxt instantiate_inducts