--- a/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200
@@ -41,24 +41,8 @@
val isar_ok = Unsynchronized.ref 0
fun sugg_facts hyp_ts concl_t suggs =
suggested_facts suggs
- #> take (max_facts_slack * the max_facts)
- #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
- fun mesh_facts fsp =
- let
- val (fs1, fs2) =
- fsp |> pairself (map (apfst (apfst (fn name => name ()))))
- val fact_eq = (op =) o pairself fst
- fun score_in f fs =
- case find_index (curry fact_eq f) fs of
- ~1 => length fs
- | j => j
- fun score_of f = score_in f fs1 + score_in f fs2
- in
- union fact_eq fs1 fs2
- |> map (`score_of) |> sort (int_ord o pairself fst) |> map snd
- |> take (the max_facts)
- |> map (apfst (apfst K))
- end
+ #> chop (max_facts_slack * the max_facts)
+ #>> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
fun index_string (j, s) = s ^ "@" ^ string_of_int j
fun str_of_res label facts {outcome, run_time, used_facts, ...} =
@@ -97,13 +81,15 @@
val goal = goal_of_thm thy th
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
- val isar_facts = facts |> sugg_facts hyp_ts concl_t isar_deps
+ val (isar_facts, _) = facts |> sugg_facts hyp_ts concl_t isar_deps
val iter_facts =
Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
prover_name (max_facts_slack * the max_facts) NONE hyp_ts concl_t
facts
- val mash_facts = facts |> sugg_facts hyp_ts concl_t suggs
- val mesh_facts = mesh_facts (iter_facts, mash_facts)
+ val (mash_facts, mash_rejects) =
+ facts |> sugg_facts hyp_ts concl_t suggs
+ val mesh_facts =
+ mesh_facts (the max_facts) iter_facts mash_facts mash_rejects
val iter_s = prove iter_ok iterN iter_facts goal
val mash_s = prove mash_ok mashN mash_facts goal
val mesh_s = prove mesh_ok meshN mesh_facts goal
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200
@@ -20,12 +20,13 @@
val unescape_meta : string -> string
val unescape_metas : string -> string list
val extract_query : string -> string * string list
- val suggested_facts : string list -> ('a * thm) list -> ('a * thm) list
+ val suggested_facts : string list -> fact list -> fact list
+ val mesh_facts : int -> fact list -> fact list -> fact list -> fact list
val all_non_tautological_facts_of :
theory -> status Termtab.table -> fact list
val theory_ord : theory * theory -> order
val thm_ord : thm * thm -> order
- val thy_facts_from_thms : ('a * thm) list -> string list Symtab.table
+ val thy_facts_from_thms : fact list -> string list Symtab.table
val has_thy : theory -> thm -> bool
val parent_facts : theory -> string list Symtab.table -> string list
val features_of : theory -> status -> term list -> string list
@@ -99,12 +100,29 @@
fun extract_query line =
case space_explode ":" line of
[goal_name, suggs] => (unescape_meta goal_name, explode_suggs suggs)
- | _ => ("", explode_suggs line)
+ | _ => ("", [])
fun find_suggested facts sugg =
find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts
fun suggested_facts suggs facts = map_filter (find_suggested facts) suggs
+fun mesh_facts max_facts iter_facts mash_facts mash_rejects =
+ let
+ val fact_eq = Thm.eq_thm o pairself snd
+ val num_iter = length iter_facts
+ val num_mash = length mash_facts
+ fun score_in f fs n =
+ case find_index (curry fact_eq f) fs of
+ ~1 => length fs
+ | j => j
+ fun score_of fact =
+ score_in fact iter_facts num_iter + score_in fact mash_facts num_mash
+ in
+ union fact_eq iter_facts mash_facts
+ |> map (`score_of) |> sort (int_ord o pairself fst) |> map snd
+ |> take max_facts
+ end
+
val thy_feature_prefix = "y_"
val thy_feature_name_of = prefix thy_feature_prefix
@@ -506,12 +524,11 @@
val iter_facts =
iterative_relevant_facts ctxt params prover max_facts NONE hyp_ts
concl_t facts
- val (mash_facts, mash_antifacts) =
+ val (mash_facts, mash_rejects) =
facts |> mash_suggest_facts ctxt params prover hyp_ts concl_t
|> chop max_facts
- val mesh_facts = iter_facts (* ### *)
in
- mesh_facts
+ mesh_facts max_facts iter_facts mash_facts mash_rejects
|> not (null add_ths) ? prepend_facts add_ths
end