# HG changeset patch
# User blanchet
# Date 1405376492 -7200
# Node ID 242ce8d3d16b3a30b1e87faffa7475fe4e3c397e
# Parent  6180d81be977f3c7e33f89ba208a9644add05fd1
record MaSh algorithm in spying data

diff -r 6180d81be977 -r 242ce8d3d16b src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 15 00:21:32 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 15 00:21:32 2014 +0200
@@ -243,7 +243,8 @@
                 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers
                   |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor))
             val _ = spying spy (fn () => (state, i, "All",
-              "Filtering " ^ string_of_int (length all_facts) ^ " facts"));
+              "Filtering " ^ string_of_int (length all_facts) ^ " facts (MaSh algorithm: " ^
+              str_of_mash_algorithm (the_mash_algorithm ()) ^ ")"));
           in
             all_facts
             |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t
diff -r 6180d81be977 -r 242ce8d3d16b src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jul 15 00:21:32 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jul 15 00:21:32 2014 +0200
@@ -42,6 +42,7 @@
 
   val is_mash_enabled : unit -> bool
   val the_mash_algorithm : unit -> mash_algorithm
+  val str_of_mash_algorithm : mash_algorithm -> string
 
   val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list
   val nickname_of_thm : thm -> string
@@ -154,6 +155,12 @@
 val is_mash_enabled = is_some o mash_algorithm
 val the_mash_algorithm = the_default MaSh_NB_kNN o mash_algorithm
 
+fun str_of_mash_algorithm MaSh_NB = "nb"
+  | str_of_mash_algorithm MaSh_kNN = "knn"
+  | str_of_mash_algorithm MaSh_NB_kNN = "nb_knn"
+  | str_of_mash_algorithm MaSh_NB_Ext = "nb_ext"
+  | str_of_mash_algorithm MaSh_kNN_Ext = "knn_ext"
+
 fun scaled_avg [] = 0
   | scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs