1.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  
     1.5  ML {*
     1.6  if do_it then
     1.7 -  generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions"
     1.8 +  generate_mepo_suggestions @{context} params thy 500 "/tmp/mash_mepo_suggestions"
     1.9  else
    1.10    ()
    1.11  *}

     2.1 --- a/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:45 2012 +0200
     2.2 +++ b/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:45 2012 +0200
     2.3 @@ -19,10 +19,10 @@
     2.4  open Sledgehammer_Fact
     2.5  open Sledgehammer_Filter_MaSh
     2.6  
     2.7 -val isarN = "Isar"
     2.8 -val iterN = "Iter"
     2.9 -val mashN = "MaSh"
    2.10 -val meshN = "Mesh"
    2.11 +val MePoN = "MePo"
    2.12 +val MaShN = "MaSh"
    2.13 +val MeshN = "Mesh"
    2.14 +val IsarN = "Isar"
    2.15  
    2.16  val max_facts_slack = 2
    2.17  
    2.18 @@ -41,7 +41,7 @@
    2.19      val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    2.20      val facts = all_facts_of thy css_table
    2.21      val all_names = all_names (facts |> map snd)
    2.22 -    val iter_ok = Unsynchronized.ref 0
    2.23 +    val mepo_ok = Unsynchronized.ref 0
    2.24      val mash_ok = Unsynchronized.ref 0
    2.25      val mesh_ok = Unsynchronized.ref 0
    2.26      val isar_ok = Unsynchronized.ref 0
    2.27 @@ -77,13 +77,13 @@
    2.28          val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
    2.29          val isar_deps = isabelle_dependencies_of all_names th
    2.30          val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
    2.31 -        val isar_facts = suggested_facts isar_deps facts
    2.32 -        val iter_facts =
    2.33 +        val mepo_facts =
    2.34            Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
    2.35                prover slack_max_facts NONE hyp_ts concl_t facts
    2.36          val mash_facts = facts |> suggested_facts suggs
    2.37 -        val mess = [(iter_facts, []), (mash_facts, [])]
    2.38 +        val mess = [(mepo_facts, []), (mash_facts, [])]
    2.39          val mesh_facts = mesh_facts slack_max_facts mess
    2.40 +        val isar_facts = suggested_facts isar_deps facts
    2.41          fun prove ok heading facts =
    2.42            let
    2.43              val facts =
    2.44 @@ -94,17 +94,17 @@
    2.45                run_prover_for_mash ctxt params prover facts goal
    2.46              val _ = if is_none outcome then ok := !ok + 1 else ()
    2.47            in str_of_res heading facts res end
    2.48 -        val iter_s = prove iter_ok iterN iter_facts
    2.49 -        val mash_s = prove mash_ok mashN mash_facts
    2.50 -        val mesh_s = prove mesh_ok meshN mesh_facts
    2.51 -        val isar_s = prove isar_ok isarN isar_facts
    2.52 +        val mepo_s = prove mepo_ok MePoN mepo_facts
    2.53 +        val mash_s = prove mash_ok MaShN mash_facts
    2.54 +        val mesh_s = prove mesh_ok MeshN mesh_facts
    2.55 +        val isar_s = prove isar_ok IsarN isar_facts
    2.56        in
    2.57 -        ["Goal " ^ string_of_int j ^ ": " ^ name, iter_s, mash_s, mesh_s,
    2.58 +        ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
    2.59           isar_s]
    2.60          |> cat_lines |> tracing
    2.61        end
    2.62      fun total_of heading ok n =
    2.63 -      " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
    2.64 +      "  " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
    2.65        Real.fmt (StringCvt.FIX (SOME 1))
    2.66                 (100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
    2.67      val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts
    2.68 @@ -119,10 +119,10 @@
    2.69      tracing ("Options: " ^ commas options);
    2.70      List.app solve_goal (tag_list 1 lines);
    2.71      ["Successes (of " ^ string_of_int n ^ " goals)",
    2.72 -     total_of iterN iter_ok n,
    2.73 -     total_of mashN mash_ok n,
    2.74 -     total_of meshN mesh_ok n,
    2.75 -     total_of isarN isar_ok n]
    2.76 +     total_of MePoN mepo_ok n,
    2.77 +     total_of MaShN mash_ok n,
    2.78 +     total_of MeshN mesh_ok n,
    2.79 +     total_of IsarN isar_ok n]
    2.80      |> cat_lines |> tracing
    2.81    end
    2.82  

     3.1 --- a/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:45 2012 +0200
     3.2 +++ b/src/HOL/TPTP/mash_export.ML	Fri Jul 20 22:19:45 2012 +0200
     3.3 @@ -17,7 +17,7 @@
     3.4    val generate_atp_dependencies :
     3.5      Proof.context -> params -> theory -> bool -> string -> unit
     3.6    val generate_commands : Proof.context -> string -> theory -> string -> unit
     3.7 -  val generate_iter_suggestions :
     3.8 +  val generate_mepo_suggestions :
     3.9      Proof.context -> params -> theory -> int -> string -> unit
    3.10  end;
    3.11  
    3.12 @@ -182,7 +182,7 @@
    3.13      val parents = parent_facts thy thy_map
    3.14    in fold do_fact new_facts parents; () end
    3.15  
    3.16 -fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant
    3.17 +fun generate_mepo_suggestions ctxt (params as {provers, ...}) thy max_relevant
    3.18                                file_name =
    3.19    let
    3.20      val path = file_name |> Path.explode

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML	Fri Jul 20 22:19:45 2012 +0200
     4.3 @@ -16,9 +16,9 @@
     4.4  
     4.5    val trace : bool Config.T
     4.6    val MaShN : string
     4.7 +  val mepoN : string
     4.8 +  val mashN : string
     4.9    val meshN : string
    4.10 -  val iterN : string
    4.11 -  val mashN : string
    4.12    val fact_filters : string list
    4.13    val escape_meta : string -> string
    4.14    val escape_metas : string list -> string
    4.15 @@ -81,11 +81,11 @@
    4.16  
    4.17  val MaShN = "MaSh"
    4.18  
    4.19 +val mepoN = "mepo"
    4.20 +val mashN = "mash"
    4.21  val meshN = "mesh"
    4.22 -val iterN = "iter"
    4.23 -val mashN = "mash"
    4.24  
    4.25 -val fact_filters = [meshN, iterN, mashN]
    4.26 +val fact_filters = [meshN, mepoN, mashN]
    4.27  
    4.28  fun mash_home () = getenv "MASH_HOME"
    4.29  fun mash_state_dir () =
    4.30 @@ -662,11 +662,11 @@
    4.31            ()
    4.32        val fact_filter =
    4.33          case fact_filter of
    4.34 -          SOME ff => (() |> ff <> iterN ? maybe_learn; ff)
    4.35 +          SOME ff => (() |> ff <> mepoN ? maybe_learn; ff)
    4.36          | NONE =>
    4.37            if mash_can_suggest_facts ctxt then (maybe_learn (); meshN)
    4.38 -          else if mash_could_suggest_facts () then (maybe_learn (); iterN)
    4.39 -          else iterN
    4.40 +          else if mash_could_suggest_facts () then (maybe_learn (); mepoN)
    4.41 +          else mepoN
    4.42        val add_ths = Attrib.eval_thms ctxt add
    4.43        fun prepend_facts ths accepts =
    4.44          ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
    4.45 @@ -679,7 +679,7 @@
    4.46          mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts
    4.47        val mess =
    4.48          [] |> (if fact_filter <> mashN then cons (iter (), []) else I)
    4.49 -           |> (if fact_filter <> iterN then cons (mash ()) else I)
    4.50 +           |> (if fact_filter <> mepoN then cons (mash ()) else I)
    4.51      in
    4.52        mesh_facts max_facts mess
    4.53        |> not (null add_ths) ? prepend_facts add_ths