# HG changeset patch
# User blanchet
# Date 1376931045 -7200
# Node ID 15fe0ca088b30e5b4e8bc0d1cd520587773409d0
# Parent  15483854c83ebdbbef6c09b5fa196484daa66b5d
MaSh tweaking: shorter names + killed (broken) SNoW

diff -r 15483854c83e -r 15fe0ca088b3 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Aug 19 16:50:25 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Aug 19 18:50:45 2013 +0200
@@ -15,7 +15,6 @@
   type prover_result = Sledgehammer_Provers.prover_result
 
   val trace : bool Config.T
-  val snow : bool Config.T
   val MePoN : string
   val MaShN : string
   val MeShN : string
@@ -110,8 +109,6 @@
 
 val trace =
   Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
-val snow =
-  Attrib.setup_config_bool @{binding sledgehammer_mash_snow} (K false)
 
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 
@@ -166,7 +163,6 @@
     val command =
       "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; " ^
       "./mash.py --quiet" ^
-      (if Config.get ctxt snow then " --snow" else "") ^
       " --outputDir " ^ model_dir ^
       " --modelFile=" ^ model_dir ^ "/model.pickle" ^
       " --dictsFile=" ^ model_dir ^ "/dict.pickle" ^
@@ -567,17 +563,21 @@
 val logical_consts =
   [@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts
 
-val crude_str_of_sort = space_implode ":" o subtract (op =) @{sort type}
+val pat_tvar_prefix = "_"
+val pat_var_prefix = "_"
+
+val massage_long_name = Long_Name.base_name
 
-fun crude_str_of_typ (Type (s, [])) = s
+val crude_str_of_sort =
+  space_implode ":" o map massage_long_name o subtract (op =) @{sort type}
+
+fun crude_str_of_typ (Type (s, [])) = massage_long_name s
   | crude_str_of_typ (Type (s, Ts)) =
-    s ^ enclose "(" ")" (space_implode "," (map crude_str_of_typ Ts))
+    massage_long_name s ^
+    enclose "(" ")" (space_implode "," (map crude_str_of_typ Ts))
   | crude_str_of_typ (TFree (_, S)) = crude_str_of_sort S
   | crude_str_of_typ (TVar (_, S)) = crude_str_of_sort S
 
-val pat_tvar_prefix = "$"
-val pat_var_prefix = "$"
-
 val max_pat_breadth = 10
 
 fun term_features_of ctxt prover thy_name term_max_depth type_max_depth ts =
@@ -596,13 +596,13 @@
       | add_classes S =
         fold (`(Sorts.super_classes classes)
               #> swap #> op ::
-              #> subtract (op =) @{sort type}
+              #> subtract (op =) @{sort type} #> map massage_long_name
               #> map class_feature_of
               #> union (op = o pairself fst)) S
 
     fun pattify_type 0 _ = []
       | pattify_type _ (Type (s, [])) =
-        if member (op =) bad_types s then [] else [s]
+        if member (op =) bad_types s then [] else [massage_long_name s]
       | pattify_type depth (Type (s, U :: Ts)) =
         let
           val T = Type (s, Ts)
@@ -624,10 +624,12 @@
 
     fun pattify_term _ _ 0 _ = []
       | pattify_term _ args _ (Const (x as (s, _))) =
-        if fst (is_built_in x args) then [] else [s]
+        if fst (is_built_in x args) then [] else [massage_long_name s]
       | pattify_term _ _ _ (Free (s, T)) =
-        if member (op =) fixes s then [thy_name ^ Long_Name.separator ^ s]
-        else [pat_var_prefix ^ crude_str_of_typ T]
+        if member (op =) fixes s then
+          [massage_long_name (thy_name ^ Long_Name.separator ^ s)]
+        else
+          [pat_var_prefix ^ crude_str_of_typ T]
       | pattify_term _ _ _ (Var (_, T)) = [pat_var_prefix ^ crude_str_of_typ T]
       | pattify_term Ts _ _ (Bound j) =
         [pat_var_prefix ^ crude_str_of_typ (nth Ts j)]