--- a/NEWS Wed Jul 09 11:35:52 2014 +0200
+++ b/NEWS Wed Jul 09 11:35:52 2014 +0200
@@ -367,7 +367,7 @@
* Sledgehammer:
- Z3 can now produce Isar proofs.
- MaSh overhaul:
- . New SML-based learning engines eliminate the dependency on
+ . New SML-based learning algorithms eliminate the dependency on
Python and increase performance and reliability.
. MaSh and MeSh are now used by default together with the
traditional MePo (Meng-Paulson) relevance filter. To disable
--- a/src/Doc/Sledgehammer/document/root.tex Wed Jul 09 11:35:52 2014 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Jul 09 11:35:52 2014 +0200
@@ -1056,7 +1056,7 @@
The traditional memoryless MePo relevance filter.
\item[\labelitemi] \textbf{\textit{mash}:}
-The MaSh machine learner. Three learning engines are provided:
+The MaSh machine learner. Three learning algorithms are provided:
\begin{enum}
\item[\labelitemi] \textbf{\textit{nb}} is an implementation of naive Bayes.
@@ -1072,20 +1072,21 @@
In addition, the special value \textit{none} is used to disable machine learning by
default (cf.\ \textit{smart} below).
-The default engine is \textit{nb\_knn}. The engine can be selected by setting
-\texttt{MASH} to the name of the desired engine---either in the environment in
-which Isabelle is launched, in your
+The default algorithm is \textit{nb\_knn}. The algorithm can be selected by
+setting \texttt{MASH}---either in the environment in which Isabelle is launched,
+in your
\texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak etc/\allowbreak settings}
file, or via the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle >
-General'' in Isabelle/jEdit. Persistent data for both engines is stored in the
-directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak mash}.
+General'' in Isabelle/jEdit. Persistent data for both algorithms is stored in
+the directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak
+mash}.
\item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
rankings from MePo and MaSh.
\item[\labelitemi] \textbf{\textit{smart}:} A combination of MePo, MaSh, and
-MeSh. If the learning engine is set to be \textit{none}, \textit{smart} behaves
-like MePo.
+MeSh. If the learning algorithm is set to be \textit{none}, \textit{smart}
+behaves like MePo.
\end{enum}
\opdefault{max\_facts}{smart\_int}{smart}
--- a/src/HOL/TPTP/mash_export.ML Wed Jul 09 11:35:52 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML Wed Jul 09 11:35:52 2014 +0200
@@ -284,8 +284,8 @@
not (Config.get ctxt Sledgehammer_MaSh.duplicates) ? Sledgehammer_Fact.drop_duplicate_facts
#> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
-fun generate_mash_suggestions engine =
- (Options.put_default @{system_option MaSh} engine;
+fun generate_mash_suggestions algorithm =
+ (Options.put_default @{system_option MaSh} algorithm;
Sledgehammer_MaSh.mash_unlearn ();
generate_mepo_or_mash_suggestions
(fn ctxt => fn thy => fn params as {provers = prover :: _, ...} => fn max_suggs => fn hyp_ts =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Jul 09 11:35:52 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Jul 09 11:35:52 2014 +0200
@@ -33,7 +33,7 @@
val decode_str : string -> string
val decode_strs : string -> string list
- datatype mash_engine =
+ datatype mash_algorithm =
MaSh_NB
| MaSh_kNN
| MaSh_NB_kNN
@@ -41,7 +41,7 @@
| MaSh_kNN_Ext
val is_mash_enabled : unit -> bool
- val the_mash_engine : unit -> mash_engine
+ val the_mash_algorithm : unit -> mash_algorithm
val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list
val nickname_of_thm : thm -> string
@@ -138,14 +138,14 @@
()
end
-datatype mash_engine =
+datatype mash_algorithm =
MaSh_NB
| MaSh_kNN
| MaSh_NB_kNN
| MaSh_NB_Ext
| MaSh_kNN_Ext
-fun mash_engine () =
+fun mash_algorithm () =
let val flag1 = Options.default_string @{system_option MaSh} in
(case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
"yes" => SOME MaSh_NB_kNN
@@ -155,11 +155,11 @@
| "nb_knn" => SOME MaSh_NB_kNN
| "nb_ext" => SOME MaSh_NB_Ext
| "knn_ext" => SOME MaSh_kNN_Ext
- | engine => (warning ("Unknown MaSh engine: " ^ quote engine ^ "."); NONE))
+ | algorithm => (warning ("Unknown MaSh algorithm: " ^ quote algorithm ^ "."); NONE))
end
-val is_mash_enabled = is_some o mash_engine
-val the_mash_engine = the_default MaSh_NB_kNN o mash_engine
+val is_mash_enabled = is_some o mash_algorithm
+val the_mash_algorithm = the_default MaSh_NB_kNN o mash_algorithm
fun scaled_avg [] = 0
| scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
@@ -481,13 +481,13 @@
external_tool ("newknn/knn" ^ " " ^ string_of_int number_of_nearest_neighbors)
val naive_bayes_ext = external_tool "predict/nbayes"
-fun query_external ctxt engine max_suggs learns goal_feats =
+fun query_external ctxt algorithm max_suggs learns goal_feats =
(trace_msg ctxt (fn () => "MaSh query external " ^ commas (map fst goal_feats));
- (case engine of
+ (case algorithm of
MaSh_NB_Ext => naive_bayes_ext max_suggs learns goal_feats
| MaSh_kNN_Ext => k_nearest_neighbors_ext max_suggs learns goal_feats))
-fun query_internal ctxt engine num_facts num_feats (fact_names, featss, depss)
+fun query_internal ctxt algorithm num_facts num_feats (fact_names, featss, depss)
(freqs as (_, _, dffreq)) visible_facts max_suggs goal_feats int_goal_feats =
let
fun nb () =
@@ -500,7 +500,7 @@
in
(trace_msg ctxt (fn () => "MaSh query internal " ^ commas (map fst goal_feats) ^ " from {" ^
elide_string 1000 (space_implode " " (Vector.foldr (op ::) [] fact_names)) ^ "}");
- (case engine of
+ (case algorithm of
MaSh_NB => nb ()
| MaSh_kNN => knn ()
| MaSh_NB_kNN =>
@@ -1152,7 +1152,7 @@
fun mash_suggested_facts ctxt thy ({debug, ...} : params) max_suggs hyp_ts concl_t facts =
let
val thy_name = Context.theory_name thy
- val engine = the_mash_engine ()
+ val algorithm = the_mash_algorithm ()
val facts = facts
|> rev_sort_list_prefix (crude_thm_ord o pairself snd)
@@ -1191,19 +1191,19 @@
val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
val suggs =
- if engine = MaSh_NB_Ext orelse engine = MaSh_kNN_Ext then
+ if algorithm = MaSh_NB_Ext orelse algorithm = MaSh_kNN_Ext then
let
val learns =
Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
in
- MaSh.query_external ctxt engine max_suggs learns goal_feats
+ MaSh.query_external ctxt algorithm max_suggs learns goal_feats
end
else
let
val int_goal_feats =
map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats
in
- MaSh.query_internal ctxt engine num_facts num_feats ffds freqs visible_facts max_suggs
+ MaSh.query_internal ctxt algorithm num_facts num_feats ffds freqs visible_facts max_suggs
goal_feats int_goal_feats
end
--- a/src/HOL/Tools/etc/options Wed Jul 09 11:35:52 2014 +0200
+++ b/src/HOL/Tools/etc/options Wed Jul 09 11:35:52 2014 +0200
@@ -36,4 +36,4 @@
-- "status of Z3 activation for non-commercial use (yes, no, unknown)"
public option MaSh : string = "sml"
- -- "machine learning engine to use by Sledgehammer (nb_knn, nb, knn, none)"
+ -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"