--- a/src/HOL/TPTP/MaSh_Export.thy Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy Fri Jul 20 22:19:45 2012 +0200
@@ -54,7 +54,7 @@
ML {*
if do_it then
- generate_iter_suggestions @{context} params thy 500 "/tmp/mash_iter_suggestions"
+ generate_mepo_suggestions @{context} params thy 500 "/tmp/mash_mepo_suggestions"
else
()
*}
--- a/src/HOL/TPTP/mash_eval.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Fri Jul 20 22:19:45 2012 +0200
@@ -19,10 +19,10 @@
open Sledgehammer_Fact
open Sledgehammer_Filter_MaSh
-val isarN = "Isar"
-val iterN = "Iter"
-val mashN = "MaSh"
-val meshN = "Mesh"
+val MePoN = "MePo"
+val MaShN = "MaSh"
+val MeshN = "Mesh"
+val IsarN = "Isar"
val max_facts_slack = 2
@@ -41,7 +41,7 @@
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val facts = all_facts_of thy css_table
val all_names = all_names (facts |> map snd)
- val iter_ok = Unsynchronized.ref 0
+ val mepo_ok = Unsynchronized.ref 0
val mash_ok = Unsynchronized.ref 0
val mesh_ok = Unsynchronized.ref 0
val isar_ok = Unsynchronized.ref 0
@@ -77,13 +77,13 @@
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
val isar_deps = isabelle_dependencies_of all_names th
val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
- val isar_facts = suggested_facts isar_deps facts
- val iter_facts =
+ val mepo_facts =
Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
prover slack_max_facts NONE hyp_ts concl_t facts
val mash_facts = facts |> suggested_facts suggs
- val mess = [(iter_facts, []), (mash_facts, [])]
+ val mess = [(mepo_facts, []), (mash_facts, [])]
val mesh_facts = mesh_facts slack_max_facts mess
+ val isar_facts = suggested_facts isar_deps facts
fun prove ok heading facts =
let
val facts =
@@ -94,17 +94,17 @@
run_prover_for_mash ctxt params prover facts goal
val _ = if is_none outcome then ok := !ok + 1 else ()
in str_of_res heading facts res end
- val iter_s = prove iter_ok iterN iter_facts
- val mash_s = prove mash_ok mashN mash_facts
- val mesh_s = prove mesh_ok meshN mesh_facts
- val isar_s = prove isar_ok isarN isar_facts
+ val mepo_s = prove mepo_ok MePoN mepo_facts
+ val mash_s = prove mash_ok MaShN mash_facts
+ val mesh_s = prove mesh_ok MeshN mesh_facts
+ val isar_s = prove isar_ok IsarN isar_facts
in
- ["Goal " ^ string_of_int j ^ ": " ^ name, iter_s, mash_s, mesh_s,
+ ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
isar_s]
|> cat_lines |> tracing
end
fun total_of heading ok n =
- " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
+ " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^
Real.fmt (StringCvt.FIX (SOME 1))
(100.0 * Real.fromInt (!ok) / Real.fromInt n) ^ "%)"
val inst_inducts = Config.get ctxt Sledgehammer_Fact.instantiate_inducts
@@ -119,10 +119,10 @@
tracing ("Options: " ^ commas options);
List.app solve_goal (tag_list 1 lines);
["Successes (of " ^ string_of_int n ^ " goals)",
- total_of iterN iter_ok n,
- total_of mashN mash_ok n,
- total_of meshN mesh_ok n,
- total_of isarN isar_ok n]
+ total_of MePoN mepo_ok n,
+ total_of MaShN mash_ok n,
+ total_of MeshN mesh_ok n,
+ total_of IsarN isar_ok n]
|> cat_lines |> tracing
end
--- a/src/HOL/TPTP/mash_export.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML Fri Jul 20 22:19:45 2012 +0200
@@ -17,7 +17,7 @@
val generate_atp_dependencies :
Proof.context -> params -> theory -> bool -> string -> unit
val generate_commands : Proof.context -> string -> theory -> string -> unit
- val generate_iter_suggestions :
+ val generate_mepo_suggestions :
Proof.context -> params -> theory -> int -> string -> unit
end;
@@ -182,7 +182,7 @@
val parents = parent_facts thy thy_map
in fold do_fact new_facts parents; () end
-fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant
+fun generate_mepo_suggestions ctxt (params as {provers, ...}) thy max_relevant
file_name =
let
val path = file_name |> Path.explode
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Fri Jul 20 22:19:45 2012 +0200
@@ -16,9 +16,9 @@
val trace : bool Config.T
val MaShN : string
+ val mepoN : string
+ val mashN : string
val meshN : string
- val iterN : string
- val mashN : string
val fact_filters : string list
val escape_meta : string -> string
val escape_metas : string list -> string
@@ -81,11 +81,11 @@
val MaShN = "MaSh"
-val meshN = "mesh"
-val iterN = "iter"
+val mepoN = "mepo"
val mashN = "mash"
+val meshN = "mesh"
-val fact_filters = [meshN, iterN, mashN]
+val fact_filters = [meshN, mepoN, mashN]
fun mash_home () = getenv "MASH_HOME"
fun mash_state_dir () =
@@ -662,11 +662,11 @@
()
val fact_filter =
case fact_filter of
- SOME ff => (() |> ff <> iterN ? maybe_learn; ff)
+ SOME ff => (() |> ff <> mepoN ? maybe_learn; ff)
| NONE =>
if mash_can_suggest_facts ctxt then (maybe_learn (); meshN)
- else if mash_could_suggest_facts () then (maybe_learn (); iterN)
- else iterN
+ else if mash_could_suggest_facts () then (maybe_learn (); mepoN)
+ else mepoN
val add_ths = Attrib.eval_thms ctxt add
fun prepend_facts ths accepts =
((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
@@ -679,7 +679,7 @@
mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts
val mess =
[] |> (if fact_filter <> mashN then cons (iter (), []) else I)
- |> (if fact_filter <> iterN then cons (mash ()) else I)
+ |> (if fact_filter <> mepoN then cons (mash ()) else I)
in
mesh_facts max_facts mess
|> not (null add_ths) ? prepend_facts add_ths