# HG changeset patch
# User blanchet
# Date 1404898552 -7200
# Node ID c7dc1f0a2b8ac82b25f963a08f55c4ce205ea0a5
# Parent  4d9895d39b590ffa9f9402ff4ee2e21b3b1352d3
tuned terminology

diff -r 4d9895d39b59 -r c7dc1f0a2b8a NEWS
--- 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
diff -r 4d9895d39b59 -r c7dc1f0a2b8a src/Doc/Sledgehammer/document/root.tex
--- 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}
diff -r 4d9895d39b59 -r c7dc1f0a2b8a src/HOL/TPTP/mash_export.ML
--- 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 =>
diff -r 4d9895d39b59 -r c7dc1f0a2b8a src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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
 
diff -r 4d9895d39b59 -r c7dc1f0a2b8a src/HOL/Tools/etc/options
--- 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)"