--- a/src/HOL/TPTP/mash_eval.ML Fri Jan 11 16:30:56 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Fri Jan 11 16:30:56 2013 +0100
@@ -98,7 +98,7 @@
fun set_file_name heading (SOME dir) =
let
val prob_prefix =
- "goal_" ^ string_of_int j ^ "__" ^ escape_meta name ^ "__" ^
+ "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^
heading
in
Config.put dest_dir dir
@@ -109,7 +109,7 @@
fun prove heading get facts =
let
fun nickify ((_, stature), th) =
- ((K (escape_meta (nickname_of_thm th)), stature), th)
+ ((K (encode_str (nickname_of_thm th)), stature), th)
val facts =
facts
|> map (get #> nickify)
--- a/src/HOL/TPTP/mash_export.ML Fri Jan 11 16:30:56 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML Fri Jan 11 16:30:56 2013 +0100
@@ -54,7 +54,7 @@
val _ = File.write path ""
fun do_fact fact prevs =
let
- val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n"
+ val s = encode_str fact ^ ": " ^ encode_strs prevs ^ "\n"
val _ = File.append path s
in [fact] end
val facts =
@@ -76,7 +76,7 @@
val feats =
features_of ctxt prover (theory_of_thm th) stature [prop_of th]
val s =
- escape_meta name ^ ": " ^ encode_features (sort_wrt fst feats) ^ "\n"
+ encode_str name ^ ": " ^ encode_features (sort_wrt fst feats) ^ "\n"
in File.append path s end
in List.app do_fact facts end
@@ -105,7 +105,7 @@
val deps =
isar_or_prover_dependencies_of ctxt params_opt facts name_tabs th
NONE
- in escape_meta name ^ ": " ^ escape_metas deps ^ "\n" end
+ in encode_str name ^ ": " ^ encode_strs deps ^ "\n" end
else
""
val lines = Par_List.map do_fact (tag_list 1 facts)
@@ -140,14 +140,14 @@
isar_or_prover_dependencies_of ctxt params_opt facts name_tabs th
(SOME isar_deps)
val core =
- escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
+ encode_str name ^ ": " ^ encode_strs prevs ^ "; " ^
encode_features (sort_wrt fst feats)
val query =
if is_bad_query ctxt ho_atp th isar_deps then ""
else "? " ^ core ^ "\n"
val update =
"! " ^ core ^ "; " ^
- escape_metas (these (trim_dependencies th deps)) ^ "\n"
+ encode_strs (these (trim_dependencies th deps)) ^ "\n"
in query ^ update end
else
""
@@ -189,7 +189,7 @@
|> Sledgehammer_MePo.mepo_suggested_facts ctxt params prover
max_suggs NONE hyp_ts concl_t
|> map (nickname_of_thm o snd)
- in escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" end
+ in encode_str name ^ ": " ^ encode_strs suggs ^ "\n" end
end
fun accum x (yss as ys :: _) = (x :: ys) :: yss
val old_factss = tl (fold accum new_facts [old_facts])
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jan 11 16:30:56 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jan 11 16:30:56 2013 +0100
@@ -24,10 +24,10 @@
val relearn_isarN : string
val relearn_proverN : string
val fact_filters : string list
- val escape_meta : string -> string
- val escape_metas : string list -> string
- val unescape_meta : string -> string
- val unescape_metas : string -> string list
+ val encode_str : string -> string
+ val encode_strs : string list -> string
+ val unencode_str : string -> string
+ val unencode_strs : string -> string list
val encode_features : (string * real) list -> string
val extract_suggestions : string -> string * (string * real) list
@@ -40,7 +40,8 @@
val relearn :
Proof.context -> bool -> (string * string list) list -> unit
val suggest :
- Proof.context -> bool -> int -> string list * (string * real) list
+ Proof.context -> bool -> int
+ -> string list * (string * real) list * string list
-> (string * real) list
end
@@ -189,40 +190,40 @@
| unmeta_chars _ (#"%" :: _) = "" (* error *)
| unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
-val escape_meta = String.translate meta_char
-val escape_metas = map escape_meta #> space_implode " "
-val unescape_meta = String.explode #> unmeta_chars []
-val unescape_metas =
- space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta
+val encode_str = String.translate meta_char
+val encode_strs = map encode_str #> space_implode " "
+val unencode_str = String.explode #> unmeta_chars []
+val unencode_strs =
+ space_explode " " #> filter_out (curry (op =) "") #> map unencode_str
fun encode_feature (name, weight) =
- escape_meta name ^
+ encode_str name ^
(if Real.== (weight, 1.0) then "" else "=" ^ Real.toString weight)
val encode_features = map encode_feature #> space_implode " "
fun str_of_learn (name, parents, feats, deps) =
- "! " ^ escape_meta name ^ ": " ^ escape_metas parents ^ "; " ^
- encode_features feats ^ "; " ^ escape_metas deps ^ "\n"
+ "! " ^ encode_str name ^ ": " ^ encode_strs parents ^ "; " ^
+ encode_features feats ^ "; " ^ encode_strs deps ^ "\n"
fun str_of_relearn (name, deps) =
- "p " ^ escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
+ "p " ^ encode_str name ^ ": " ^ encode_strs deps ^ "\n"
-fun str_of_query (parents, feats) =
- "? " ^ escape_metas parents ^ "; " ^ encode_features feats ^ "\n"
+fun str_of_query (parents, feats, hints) =
+ "? " ^ encode_strs parents ^ "; " ^ encode_features feats ^
+ (if null hints then "" else "; " ^ encode_strs hints) ^ "\n"
fun extract_suggestion sugg =
case space_explode "=" sugg of
[name, weight] =>
- SOME (unescape_meta name, Real.fromString weight |> the_default 1.0)
- | [name] => SOME (unescape_meta name, 1.0)
+ SOME (unencode_str name, Real.fromString weight |> the_default 1.0)
+ | [name] => SOME (unencode_str name, 1.0)
| _ => NONE
fun extract_suggestions line =
case space_explode ":" line of
[goal, suggs] =>
- (unescape_meta goal,
- map_filter extract_suggestion (space_explode " " suggs))
+ (unencode_str goal, map_filter extract_suggestion (space_explode " " suggs))
| _ => ("", [])
structure MaSh =
@@ -249,9 +250,9 @@
elide_string 1000 (space_implode " " (map #1 relearns)));
run_mash_tool ctxt overlord true 0 (relearns, str_of_relearn) (K ()))
-fun suggest ctxt overlord max_suggs (query as (_, feats)) =
+fun suggest ctxt overlord max_suggs (query as (_, feats, hints)) =
(trace_msg ctxt (fn () => "MaSh suggest " ^ encode_features feats);
- run_mash_tool ctxt overlord false max_suggs
+ run_mash_tool ctxt overlord (not (null hints)) max_suggs
([query], str_of_query)
(fn suggs =>
case suggs () of
@@ -321,7 +322,7 @@
[head, parents] =>
(case space_explode " " head of
[kind, name] =>
- SOME (unescape_meta name, unescape_metas parents,
+ SOME (unencode_str name, unencode_strs parents,
try proof_kind_of_str kind |> the_default Isar_Proof)
| _ => NONE)
| _ => NONE
@@ -361,8 +362,8 @@
| save ctxt {access_G, dirty} =
let
fun str_of_entry (name, parents, kind) =
- str_of_proof_kind kind ^ " " ^ escape_meta name ^ ": " ^
- escape_metas parents ^ "\n"
+ str_of_proof_kind kind ^ " " ^ encode_str name ^ ": " ^
+ encode_strs parents ^ "\n"
fun append_entry (name, (kind, (parents, _))) =
cons (name, Graph.Keys.dest parents, kind)
val (banner, entries) =
@@ -777,6 +778,7 @@
concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
+ val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
val (access_G, suggs) =
peek_state ctxt (fn {access_G, ...} =>
if Graph.is_empty access_G then
@@ -786,10 +788,11 @@
val parents = maximal_in_graph access_G facts
val feats =
features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts)
+ val hints = map (nickname_of_thm o snd) chained
in
- (access_G, MaSh.suggest ctxt overlord max_facts (parents, feats))
+ (access_G,
+ MaSh.suggest ctxt overlord max_facts (parents, feats, hints))
end)
- val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained)
val unknown = facts |> filter_out (is_fact_in_graph access_G)
in find_mash_suggestions max_facts suggs facts chained unknown end