# HG changeset patch # User blanchet # Date 1342815585 -7200 # Node ID 2b5ad61e2ccc95f27c887ebcec9bf26a64e9f328 # Parent 9e96486d53ad9883f6532b495e4ec360cc1f5996 renamed "iter" fact filter to "MePo" (Meng--Paulson) diff -r 9e96486d53ad -r 2b5ad61e2ccc src/HOL/TPTP/MaSh_Export.thy --- 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 () *} diff -r 9e96486d53ad -r 2b5ad61e2ccc src/HOL/TPTP/mash_eval.ML --- 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 diff -r 9e96486d53ad -r 2b5ad61e2ccc src/HOL/TPTP/mash_export.ML --- 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 diff -r 9e96486d53ad -r 2b5ad61e2ccc src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML --- 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