tuned terminology
authorblanchet
Wed Jul 09 11:35:52 2014 +0200 (2014-07-09)
changeset 57532c7dc1f0a2b8a
parent 57531 4d9895d39b59
child 57533 99a8e1cc7e9e
tuned terminology
NEWS
src/Doc/Sledgehammer/document/root.tex
src/HOL/TPTP/mash_export.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/etc/options
     1.1 --- a/NEWS	Wed Jul 09 11:35:52 2014 +0200
     1.2 +++ b/NEWS	Wed Jul 09 11:35:52 2014 +0200
     1.3 @@ -367,7 +367,7 @@
     1.4  * Sledgehammer:
     1.5    - Z3 can now produce Isar proofs.
     1.6    - MaSh overhaul:
     1.7 -    . New SML-based learning engines eliminate the dependency on
     1.8 +    . New SML-based learning algorithms eliminate the dependency on
     1.9        Python and increase performance and reliability.
    1.10      . MaSh and MeSh are now used by default together with the
    1.11        traditional MePo (Meng-Paulson) relevance filter. To disable
     2.1 --- a/src/Doc/Sledgehammer/document/root.tex	Wed Jul 09 11:35:52 2014 +0200
     2.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Wed Jul 09 11:35:52 2014 +0200
     2.3 @@ -1056,7 +1056,7 @@
     2.4  The traditional memoryless MePo relevance filter.
     2.5  
     2.6  \item[\labelitemi] \textbf{\textit{mash}:}
     2.7 -The MaSh machine learner. Three learning engines are provided:
     2.8 +The MaSh machine learner. Three learning algorithms are provided:
     2.9  
    2.10  \begin{enum}
    2.11  \item[\labelitemi] \textbf{\textit{nb}} is an implementation of naive Bayes.
    2.12 @@ -1072,20 +1072,21 @@
    2.13  In addition, the special value \textit{none} is used to disable machine learning by
    2.14  default (cf.\ \textit{smart} below).
    2.15  
    2.16 -The default engine is \textit{nb\_knn}. The engine can be selected by setting
    2.17 -\texttt{MASH} to the name of the desired engine---either in the environment in
    2.18 -which Isabelle is launched, in your
    2.19 +The default algorithm is \textit{nb\_knn}. The algorithm can be selected by
    2.20 +setting \texttt{MASH}---either in the environment in which Isabelle is launched,
    2.21 +in your
    2.22  \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak etc/\allowbreak settings}
    2.23  file, or via the ``MaSh'' option under ``Plugins > Plugin Options > Isabelle >
    2.24 -General'' in Isabelle/jEdit. Persistent data for both engines is stored in the
    2.25 -directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak mash}.
    2.26 +General'' in Isabelle/jEdit. Persistent data for both algorithms is stored in
    2.27 +the directory \texttt{\$ISABELLE\_\allowbreak HOME\_\allowbreak USER/\allowbreak
    2.28 +mash}.
    2.29  
    2.30  \item[\labelitemi] \textbf{\textit{mesh}:} The MeSh filter, which combines the
    2.31  rankings from MePo and MaSh.
    2.32  
    2.33  \item[\labelitemi] \textbf{\textit{smart}:} A combination of MePo, MaSh, and
    2.34 -MeSh. If the learning engine is set to be \textit{none}, \textit{smart} behaves
    2.35 -like MePo.
    2.36 +MeSh. If the learning algorithm is set to be \textit{none}, \textit{smart}
    2.37 +behaves like MePo.
    2.38  \end{enum}
    2.39  
    2.40  \opdefault{max\_facts}{smart\_int}{smart}
     3.1 --- a/src/HOL/TPTP/mash_export.ML	Wed Jul 09 11:35:52 2014 +0200
     3.2 +++ b/src/HOL/TPTP/mash_export.ML	Wed Jul 09 11:35:52 2014 +0200
     3.3 @@ -284,8 +284,8 @@
     3.4         not (Config.get ctxt Sledgehammer_MaSh.duplicates) ? Sledgehammer_Fact.drop_duplicate_facts
     3.5         #> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
     3.6  
     3.7 -fun generate_mash_suggestions engine =
     3.8 -  (Options.put_default @{system_option MaSh} engine;
     3.9 +fun generate_mash_suggestions algorithm =
    3.10 +  (Options.put_default @{system_option MaSh} algorithm;
    3.11     Sledgehammer_MaSh.mash_unlearn ();
    3.12     generate_mepo_or_mash_suggestions
    3.13       (fn ctxt => fn thy => fn params as {provers = prover :: _, ...} => fn max_suggs => fn hyp_ts =>
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Jul 09 11:35:52 2014 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Jul 09 11:35:52 2014 +0200
     4.3 @@ -33,7 +33,7 @@
     4.4    val decode_str : string -> string
     4.5    val decode_strs : string -> string list
     4.6  
     4.7 -  datatype mash_engine =
     4.8 +  datatype mash_algorithm =
     4.9      MaSh_NB
    4.10    | MaSh_kNN
    4.11    | MaSh_NB_kNN
    4.12 @@ -41,7 +41,7 @@
    4.13    | MaSh_kNN_Ext
    4.14  
    4.15    val is_mash_enabled : unit -> bool
    4.16 -  val the_mash_engine : unit -> mash_engine
    4.17 +  val the_mash_algorithm : unit -> mash_algorithm
    4.18  
    4.19    val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list
    4.20    val nickname_of_thm : thm -> string
    4.21 @@ -138,14 +138,14 @@
    4.22      ()
    4.23    end
    4.24  
    4.25 -datatype mash_engine =
    4.26 +datatype mash_algorithm =
    4.27    MaSh_NB
    4.28  | MaSh_kNN
    4.29  | MaSh_NB_kNN
    4.30  | MaSh_NB_Ext
    4.31  | MaSh_kNN_Ext
    4.32  
    4.33 -fun mash_engine () =
    4.34 +fun mash_algorithm () =
    4.35    let val flag1 = Options.default_string @{system_option MaSh} in
    4.36      (case if flag1 <> "none" (* default *) then flag1 else getenv "MASH" of
    4.37        "yes" => SOME MaSh_NB_kNN
    4.38 @@ -155,11 +155,11 @@
    4.39      | "nb_knn" => SOME MaSh_NB_kNN
    4.40      | "nb_ext" => SOME MaSh_NB_Ext
    4.41      | "knn_ext" => SOME MaSh_kNN_Ext
    4.42 -    | engine => (warning ("Unknown MaSh engine: " ^ quote engine ^ "."); NONE))
    4.43 +    | algorithm => (warning ("Unknown MaSh algorithm: " ^ quote algorithm ^ "."); NONE))
    4.44    end
    4.45  
    4.46 -val is_mash_enabled = is_some o mash_engine
    4.47 -val the_mash_engine = the_default MaSh_NB_kNN o mash_engine
    4.48 +val is_mash_enabled = is_some o mash_algorithm
    4.49 +val the_mash_algorithm = the_default MaSh_NB_kNN o mash_algorithm
    4.50  
    4.51  fun scaled_avg [] = 0
    4.52    | scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
    4.53 @@ -481,13 +481,13 @@
    4.54    external_tool ("newknn/knn" ^ " " ^ string_of_int number_of_nearest_neighbors)
    4.55  val naive_bayes_ext = external_tool "predict/nbayes"
    4.56  
    4.57 -fun query_external ctxt engine max_suggs learns goal_feats =
    4.58 +fun query_external ctxt algorithm max_suggs learns goal_feats =
    4.59    (trace_msg ctxt (fn () => "MaSh query external " ^ commas (map fst goal_feats));
    4.60 -   (case engine of
    4.61 +   (case algorithm of
    4.62       MaSh_NB_Ext => naive_bayes_ext max_suggs learns goal_feats
    4.63     | MaSh_kNN_Ext => k_nearest_neighbors_ext max_suggs learns goal_feats))
    4.64  
    4.65 -fun query_internal ctxt engine num_facts num_feats (fact_names, featss, depss)
    4.66 +fun query_internal ctxt algorithm num_facts num_feats (fact_names, featss, depss)
    4.67      (freqs as (_, _, dffreq)) visible_facts max_suggs goal_feats int_goal_feats =
    4.68    let
    4.69      fun nb () =
    4.70 @@ -500,7 +500,7 @@
    4.71    in
    4.72      (trace_msg ctxt (fn () => "MaSh query internal " ^ commas (map fst goal_feats) ^ " from {" ^
    4.73         elide_string 1000 (space_implode " " (Vector.foldr (op ::) [] fact_names)) ^ "}");
    4.74 -     (case engine of
    4.75 +     (case algorithm of
    4.76         MaSh_NB => nb ()
    4.77       | MaSh_kNN => knn ()
    4.78       | MaSh_NB_kNN =>
    4.79 @@ -1152,7 +1152,7 @@
    4.80  fun mash_suggested_facts ctxt thy ({debug, ...} : params) max_suggs hyp_ts concl_t facts =
    4.81    let
    4.82      val thy_name = Context.theory_name thy
    4.83 -    val engine = the_mash_engine ()
    4.84 +    val algorithm = the_mash_algorithm ()
    4.85  
    4.86      val facts = facts
    4.87        |> rev_sort_list_prefix (crude_thm_ord o pairself snd)
    4.88 @@ -1191,19 +1191,19 @@
    4.89      val visible_facts = map_filter (Symtab.lookup fact_tab) (Graph.all_preds access_G parents)
    4.90  
    4.91      val suggs =
    4.92 -      if engine = MaSh_NB_Ext orelse engine = MaSh_kNN_Ext then
    4.93 +      if algorithm = MaSh_NB_Ext orelse algorithm = MaSh_kNN_Ext then
    4.94          let
    4.95            val learns =
    4.96              Graph.schedule (fn _ => fn (fact, (_, feats, deps)) => (fact, feats, deps)) access_G
    4.97          in
    4.98 -          MaSh.query_external ctxt engine max_suggs learns goal_feats
    4.99 +          MaSh.query_external ctxt algorithm max_suggs learns goal_feats
   4.100          end
   4.101        else
   4.102          let
   4.103            val int_goal_feats =
   4.104              map_filter (fn (s, w) => Option.map (rpair w) (Symtab.lookup feat_tab s)) goal_feats
   4.105          in
   4.106 -          MaSh.query_internal ctxt engine num_facts num_feats ffds freqs visible_facts max_suggs
   4.107 +          MaSh.query_internal ctxt algorithm num_facts num_feats ffds freqs visible_facts max_suggs
   4.108              goal_feats int_goal_feats
   4.109          end
   4.110  
     5.1 --- a/src/HOL/Tools/etc/options	Wed Jul 09 11:35:52 2014 +0200
     5.2 +++ b/src/HOL/Tools/etc/options	Wed Jul 09 11:35:52 2014 +0200
     5.3 @@ -36,4 +36,4 @@
     5.4    -- "status of Z3 activation for non-commercial use (yes, no, unknown)"
     5.5  
     5.6  public option MaSh : string = "sml"
     5.7 -  -- "machine learning engine to use by Sledgehammer (nb_knn, nb, knn, none)"
     5.8 +  -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)"