--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jul 20 22:19:45 2012 +0200
@@ -466,7 +466,7 @@
Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
hyp_ts concl_t
|> filter (is_appropriate_prop o prop_of o snd)
- |> Sledgehammer_Filter_MaSh.relevant_facts ctxt params prover_name
+ |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name
(the_default default_max_facts max_facts)
Sledgehammer_Fact.no_fact_override hyp_ts concl_t
val problem =
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Fri Jul 20 22:19:45 2012 +0200
@@ -133,7 +133,7 @@
Sledgehammer_Fact.no_fact_override reserved css_table chained_ths
hyp_ts concl_t
|> filter (is_appropriate_prop o prop_of o snd)
- |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
+ |> Sledgehammer_MePo.iterative_relevant_facts ctxt params
default_prover (the_default default_max_facts max_facts)
(SOME relevance_fudge) hyp_ts concl_t
|> map ((fn name => name ()) o fst o fst)
--- a/src/HOL/TPTP/atp_theory_export.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Fri Jul 20 22:19:45 2012 +0200
@@ -115,7 +115,7 @@
fun all_non_tautological_facts_of thy css_table =
Sledgehammer_Fact.all_facts_of thy css_table
- |> filter_out (Sledgehammer_Filter_MaSh.is_likely_tautology_or_too_meta o snd)
+ |> filter_out (Sledgehammer_MaSh.is_likely_tautology_or_too_meta o snd)
fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name =
let
--- 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
@@ -17,7 +17,7 @@
struct
open Sledgehammer_Fact
-open Sledgehammer_Filter_MaSh
+open Sledgehammer_MaSh
val MePoN = "MePo"
val MaShN = "MaSh"
@@ -78,8 +78,8 @@
val isar_deps = isabelle_dependencies_of all_names th
val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
val mepo_facts =
- Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
- prover slack_max_facts NONE hyp_ts concl_t facts
+ Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
+ slack_max_facts NONE hyp_ts concl_t facts
val mash_facts = facts |> suggested_facts suggs
val mess = [(mepo_facts, []), (mash_facts, [])]
val mesh_facts = mesh_facts slack_max_facts mess
--- 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
@@ -25,8 +25,8 @@
struct
open Sledgehammer_Fact
-open Sledgehammer_Filter_Iter
-open Sledgehammer_Filter_MaSh
+open Sledgehammer_MePo
+open Sledgehammer_MaSh
fun thy_map_from_facts ths =
ths |> sort (thm_ord o swap o pairself snd)
@@ -204,8 +204,8 @@
let
val suggs =
old_facts
- |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
- prover max_relevant NONE hyp_ts concl_t
+ |> Sledgehammer_MePo.iterative_relevant_facts ctxt params prover
+ max_relevant NONE hyp_ts concl_t
|> map (fn ((name, _), _) => name ())
|> sort string_ord
val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n"
--- a/src/HOL/TPTP/sledgehammer_tactics.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML Fri Jul 20 22:19:45 2012 +0200
@@ -21,7 +21,7 @@
open Sledgehammer_Util
open Sledgehammer_Fact
open Sledgehammer_Provers
-open Sledgehammer_Filter_MaSh
+open Sledgehammer_MaSh
open Sledgehammer_Isar
fun run_prover override_params fact_override i n ctxt goal =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jul 20 22:19:45 2012 +0200
@@ -26,7 +26,7 @@
open Sledgehammer_Fact
open Sledgehammer_Provers
open Sledgehammer_Minimize
-open Sledgehammer_Filter_MaSh
+open Sledgehammer_MaSh
open Sledgehammer_Run
val runN = "run"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:45 2012 +0200
@@ -4,7 +4,7 @@
Sledgehammer's machine-learning-based relevance filter (MaSh).
*)
-signature SLEDGEHAMMER_FILTER_MASH =
+signature SLEDGEHAMMER_MASH =
sig
type status = ATP_Problem_Generate.status
type stature = ATP_Problem_Generate.stature
@@ -64,16 +64,16 @@
val running_learners : unit -> unit
end;
-structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
+structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH =
struct
open ATP_Util
open ATP_Problem_Generate
open Sledgehammer_Util
open Sledgehammer_Fact
-open Sledgehammer_Filter_Iter
open Sledgehammer_Provers
open Sledgehammer_Minimize
+open Sledgehammer_MePo
val trace =
Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
@@ -467,7 +467,7 @@
end
val global_state =
- Synchronized.var "Sledgehammer_Filter_MaSh.global_state" (false, empty_state)
+ Synchronized.var "Sledgehammer_MaSh.global_state" (false, empty_state)
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Fri Jul 20 22:19:45 2012 +0200
@@ -5,7 +5,7 @@
Sledgehammer's iterative relevance filter (MePo = Meng-Paulson).
*)
-signature SLEDGEHAMMER_FILTER_ITER =
+signature SLEDGEHAMMER_MEPO =
sig
type stature = ATP_Problem_Generate.stature
type fact = Sledgehammer_Fact.fact
@@ -23,7 +23,7 @@
-> term list -> term -> fact list -> fact list
end;
-structure Sledgehammer_Filter_Iter : SLEDGEHAMMER_FILTER_ITER =
+structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
struct
open ATP_Problem_Generate
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:45 2012 +0200
@@ -33,7 +33,7 @@
open Sledgehammer_Fact
open Sledgehammer_Provers
open Sledgehammer_Minimize
-open Sledgehammer_Filter_MaSh
+open Sledgehammer_MaSh
val someN = "some"
val noneN = "none"