# HG changeset patch # User blanchet # Date 1356733911 -3600 # Node ID 87961472b4040f11f9f070ffdfd3f9a1ede69f86 # Parent 12c097ff32414cc8ae65b1c314bfb6b0b2785b0a tuned ML function name diff -r 12c097ff3241 -r 87961472b404 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Fri Dec 28 21:03:39 2012 +0100 +++ b/src/HOL/TPTP/mash_eval.ML Fri Dec 28 23:31:51 2012 +0100 @@ -72,7 +72,7 @@ fun solve_goal (j, line) = if in_range range j then let - val (name, suggs) = extract_query line + val (name, suggs) = extract_suggestions line val th = case find_first (fn (_, th) => nickname_of_thm th = name) facts of SOME (_, th) => th diff -r 12c097ff3241 -r 87961472b404 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Dec 28 21:03:39 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Dec 28 23:31:51 2012 +0100 @@ -29,7 +29,7 @@ val unescape_meta : string -> string val unescape_metas : string -> string list val encode_features : (string * real) list -> string - val extract_query : string -> string * (string * real) list + val extract_suggestions : string -> string * (string * real) list structure MaSh: sig @@ -39,7 +39,7 @@ -> (string * string list * (string * real) list * string list) list -> unit val relearn : Proof.context -> bool -> (string * string list) list -> unit - val query : + val suggest : Proof.context -> bool -> int -> string list * (string * real) list -> (string * real) list end @@ -213,7 +213,7 @@ | [name] => SOME (unescape_meta name, 1.0) | _ => NONE -fun extract_query line = +fun extract_suggestions line = case space_explode ":" line of [goal, suggs] => (unescape_meta goal, @@ -244,14 +244,14 @@ elide_string 1000 (space_implode " " (map #1 relearns))); run_mash_tool ctxt overlord true 0 (relearns, str_of_relearn) (K ())) -fun query ctxt overlord max_suggs (query as (_, feats)) = - (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats); +fun suggest ctxt overlord max_suggs (query as (_, feats)) = + (trace_msg ctxt (fn () => "MaSh suggest " ^ encode_features feats); run_mash_tool ctxt overlord false max_suggs ([query], str_of_query) (fn suggs => case suggs () of [] => [] - | suggs => snd (extract_query (List.last suggs))) + | suggs => snd (extract_suggestions (List.last suggs))) handle List.Empty => []) end; @@ -788,7 +788,7 @@ val feats = features_of ctxt prover thy (Local, General) (concl_t :: hyp_ts) in - (access_G, MaSh.query ctxt overlord max_facts (parents, feats)) + (access_G, MaSh.suggest ctxt overlord max_facts (parents, feats)) end) val chained = facts |> filter (fn ((_, (scope, _)), _) => scope = Chained) val unknown = facts |> filter_out (is_fact_in_graph access_G)