--- 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
""
--- 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