1.1 --- a/src/HOL/TPTP/MaSh_Eval.thy	Thu Jan 17 18:43:59 2013 +0100
     1.2 +++ b/src/HOL/TPTP/MaSh_Eval.thy	Thu Jan 17 18:53:13 2013 +0100
     1.3 @@ -41,9 +41,10 @@
     1.4  
     1.5  ML {*
     1.6  if do_it then
     1.7 -  evaluate_mash_suggestions @{context} params (1, NONE) (SOME prob_dir)
     1.8 -      (prefix ^ "mash_suggestions") (prefix ^ "mash_prover_suggestions")
     1.9 -      (prefix ^ "mash_eval")
    1.10 +  evaluate_mash_suggestions @{context} params (1, NONE)
    1.11 +      [MePoN, MaSh_IsarN, MaSh_ProverN, MeSh_IsarN, MeSh_ProverN, IsarN]
    1.12 +      (SOME prob_dir) (prefix ^ "mash_suggestions")
    1.13 +      (prefix ^ "mash_prover_suggestions") (prefix ^ "mash_eval")
    1.14  else
    1.15    ()
    1.16  *}

     2.1 --- a/src/HOL/TPTP/mash_eval.ML	Thu Jan 17 18:43:59 2013 +0100
     2.2 +++ b/src/HOL/TPTP/mash_eval.ML	Thu Jan 17 18:53:13 2013 +0100
     2.3 @@ -9,9 +9,15 @@
     2.4  sig
     2.5    type params = Sledgehammer_Provers.params
     2.6  
     2.7 +  val MePoN : string
     2.8 +  val MaSh_IsarN : string
     2.9 +  val MaSh_ProverN : string
    2.10 +  val MeSh_IsarN : string
    2.11 +  val MeSh_ProverN : string
    2.12 +  val IsarN : string
    2.13    val evaluate_mash_suggestions :
    2.14 -    Proof.context -> params -> int * int option -> string option -> string
    2.15 -    -> string -> string -> unit
    2.16 +    Proof.context -> params -> int * int option -> string list -> string option
    2.17 +    -> string -> string -> string -> unit
    2.18  end;
    2.19  
    2.20  structure MaSh_Eval : MASH_EVAL =
    2.21 @@ -34,7 +40,7 @@
    2.22  fun in_range (from, to) j =
    2.23    j >= from andalso (to = NONE orelse j <= the to)
    2.24  
    2.25 -fun evaluate_mash_suggestions ctxt params range prob_dir_name
    2.26 +fun evaluate_mash_suggestions ctxt params range methods prob_dir_name
    2.27          isar_sugg_file_name prover_sugg_file_name report_file_name =
    2.28    let
    2.29      val report_path = report_file_name |> Path.explode
    2.30 @@ -55,11 +61,11 @@
    2.31      val name_tabs = build_name_tables nickname_of_thm facts
    2.32      fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
    2.33      fun index_str (j, s) = s ^ "@" ^ string_of_int j
    2.34 -    val str_of_heading = enclose "  " ": "
    2.35 -    fun str_of_result heading facts ({outcome, run_time, used_facts, ...}
    2.36 +    val str_of_method = enclose "  " ": "
    2.37 +    fun str_of_result method facts ({outcome, run_time, used_facts, ...}
    2.38                                       : prover_result) =
    2.39        let val facts = facts |> map (fn ((name, _), _) => name ()) in
    2.40 -        str_of_heading heading ^
    2.41 +        str_of_method method ^
    2.42          (if is_none outcome then
    2.43             "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
    2.44             (used_facts |> map (with_index facts o fst)
    2.45 @@ -110,20 +116,21 @@
    2.46            val isar_facts =
    2.47              find_suggested_facts (map (rpair 1.0) isar_deps) facts
    2.48            (* adapted from "mirabelle_sledgehammer.ML" *)
    2.49 -          fun set_file_name heading (SOME dir) =
    2.50 +          fun set_file_name method (SOME dir) =
    2.51                let
    2.52                  val prob_prefix =
    2.53                    "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^
    2.54 -                  heading
    2.55 +                  method
    2.56                in
    2.57                  Config.put dest_dir dir
    2.58                  #> Config.put problem_prefix (prob_prefix ^ "__")
    2.59                  #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
    2.60                end
    2.61              | set_file_name _ NONE = I
    2.62 -          fun prove heading get facts =
    2.63 -            if null facts andalso heading <> IsarN then
    2.64 -              (str_of_heading heading ^ "Skipped", 0)
    2.65 +          fun prove method get facts =
    2.66 +            if not (member (op =) methods method) orelse
    2.67 +               (null facts andalso method <> IsarN) then
    2.68 +              (str_of_method method ^ "Skipped", 0)
    2.69              else
    2.70                let
    2.71                  fun nickify ((_, stature), th) =
    2.72 @@ -133,11 +140,11 @@
    2.73                    |> map (get #> nickify)
    2.74                    |> maybe_instantiate_inducts ctxt hyp_ts concl_t
    2.75                    |> take (the max_facts)
    2.76 -                val ctxt = ctxt |> set_file_name heading prob_dir_name
    2.77 +                val ctxt = ctxt |> set_file_name method prob_dir_name
    2.78                  val res as {outcome, ...} =
    2.79                    run_prover_for_mash ctxt params prover facts goal
    2.80                  val ok = if is_none outcome then 1 else 0
    2.81 -              in (str_of_result heading facts res, ok) end
    2.82 +              in (str_of_result method facts res, ok) end
    2.83            val ress =
    2.84              [fn () => prove MePoN fst mepo_facts,
    2.85               fn () => prove MaSh_IsarN fst mash_isar_facts,
    2.86 @@ -153,8 +160,8 @@
    2.87          end
    2.88        else
    2.89          [0, 0, 0, 0, 0, 0]
    2.90 -    fun total_of heading ok n =
    2.91 -      "  " ^ heading ^ ": " ^ string_of_int ok ^ " (" ^
    2.92 +    fun total_of method ok n =
    2.93 +      str_of_method method ^ string_of_int ok ^ " (" ^
    2.94        Real.fmt (StringCvt.FIX (SOME 1))
    2.95                 (100.0 * Real.fromInt ok / Real.fromInt n) ^ "%)"
    2.96      val inst_inducts = Config.get ctxt instantiate_inducts