# HG changeset patch
# User blanchet
# Date 1377069940 -7200
# Node ID 5f727525b1acad420ab150626446f01471a7c319
# Parent  43d5f3d6d04e467169748482d742cc7bc961c5d7
only generate feature weights for queries -- they're not used elsewhere

diff -r 43d5f3d6d04e -r 5f727525b1ac src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Wed Aug 21 09:25:40 2013 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Wed Aug 21 09:25:40 2013 +0200
@@ -159,6 +159,7 @@
           val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
           val feats =
             features_of ctxt prover (theory_of_thm th) stature [prop_of th]
+            |> sort_wrt fst
           val isar_deps = isar_dependencies_of name_tabs th
           val access_facts =
             (if linearize then take (j - 1) new_facts
@@ -167,14 +168,17 @@
             smart_dependencies_of ctxt params_opt access_facts name_tabs th
                                   (SOME isar_deps)
           val parents = if linearize then prevs else parents
-          val core =
-            encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
-            encode_features (sort_wrt fst feats)
           val query =
-            if is_bad_query ctxt ho_atp step j th isar_deps then ""
-            else "? " ^ string_of_int max_suggs ^ " # " ^ core ^ "\n"
+            if is_bad_query ctxt ho_atp step j th isar_deps then
+              ""
+            else
+              "? " ^ string_of_int max_suggs ^ " # " ^
+              encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
+              encode_features feats ^ "\n"
           val update =
-            "! " ^ core ^ "; " ^ marker ^ " " ^ encode_strs deps ^ "\n"
+            "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
+            encode_strs (map fst feats) ^ "; " ^ marker ^ " " ^
+            encode_strs deps ^ "\n"
         in query ^ update end
       else
         ""
diff -r 43d5f3d6d04e -r 5f727525b1ac src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Aug 21 09:25:40 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Aug 21 09:25:40 2013 +0200
@@ -39,12 +39,12 @@
     val unlearn : Proof.context -> unit
     val learn :
       Proof.context -> bool
-      -> (string * string list * (string * real) list * string list) list -> unit
+      -> (string * string list * string list * string list) list -> unit
     val relearn :
       Proof.context -> bool -> (string * string list) list -> unit
     val query :
       Proof.context -> bool -> int
-      -> (string * string list * (string * real) list * string list) list
+      -> (string * string list * string list * string list) list
          * string list * string list * (string * real) list
       -> string list
   end
@@ -222,7 +222,7 @@
 
 fun str_of_learn (name, parents, feats, deps) =
   "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
-  encode_features feats ^ "; " ^ encode_strs deps ^ "\n"
+  encode_strs feats ^ "; " ^ encode_strs deps ^ "\n"
 
 fun str_of_relearn (name, deps) =
   "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n"
@@ -989,7 +989,7 @@
       let
         val thy = Proof_Context.theory_of ctxt
         val name = freshish_name ()
-        val feats = features_of ctxt prover thy (Local, General) [t]
+        val feats = features_of ctxt prover thy (Local, General) [t] |> map fst
       in
         peek_state ctxt (fn {access_G, ...} =>
             let
@@ -1087,6 +1087,7 @@
               val name = nickname_of_thm th
               val feats =
                 features_of ctxt prover (theory_of_thm th) stature [prop_of th]
+                |> map fst
               val deps = deps_of status th |> these
               val n = n |> not (null deps) ? Integer.add 1
               val learns = (name, parents, feats, deps) :: learns