--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Jul 18 08:44:03 2012 +0200
@@ -470,7 +470,8 @@
val problem =
{state = st', goal = goal, subgoal = i,
subgoal_count = Sledgehammer_Util.subgoal_count st,
- facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
+ facts = facts |> map (apfst (apfst (fn name => name ())))
+ |> map Sledgehammer_Provers.Untranslated_Fact}
in prover params (K (K (K ""))) problem end)) ()
handle TimeLimit.TimeOut => failed ATP_Proof.TimedOut
| Fail "inappropriate" => failed ATP_Proof.Inappropriate
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Jul 18 08:44:03 2012 +0200
@@ -128,14 +128,14 @@
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal
val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
val facts =
- Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
- Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts concl_t
- |> filter (is_appropriate_prop o prop_of o snd)
- |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
- default_prover (the_default default_max_relevant max_relevant)
- (SOME relevance_fudge) Sledgehammer_Fact.no_relevance_override
- chained_ths hyp_ts concl_t
- |> map (fst o fst)
+ Sledgehammer_Fact.nearly_all_facts ctxt ho_atp
+ Sledgehammer_Fact.no_relevance_override chained_ths hyp_ts concl_t
+ |> filter (is_appropriate_prop o prop_of o snd)
+ |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params
+ default_prover (the_default default_max_relevant max_relevant)
+ (SOME relevance_fudge) Sledgehammer_Fact.no_relevance_override
+ chained_ths hyp_ts concl_t
+ |> map ((fn name => name ()) o fst o fst)
val (found_facts, lost_facts) =
flat proofs |> sort_distinct string_ord
|> map (fn fact => (find_index (curry (op =) fact) facts, fact))
--- a/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:03 2012 +0200
@@ -57,9 +57,10 @@
map_filter (find_sugg facts o of_fact_name)
#> take (max_relevant_slack * the max_relevant)
#> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
- #> map (apfst (apfst (fn name => name ())))
- fun iter_mash_facts fs1 fs2 =
+ fun hybrid_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
@@ -70,29 +71,30 @@
union fact_eq fs1 fs2
|> map (`score_of) |> sort (int_ord o pairself fst) |> map snd
|> take (the max_relevant)
+ |> map (apfst (apfst K))
end
- fun with_index facts s =
- (find_index (fn ((s', _), _) => s = s') facts + 1, s)
+ 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, ...} =
- " " ^ label ^ ": " ^
- (if is_none outcome then
- "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
- (used_facts |> map (with_index facts o fst)
- |> sort (int_ord o pairself fst)
- |> map index_string
- |> space_implode " ") ^
- (if length facts < the max_relevant then
- " (of " ^ string_of_int (length facts) ^ ")"
- else
- "")
- else
- "Failure: " ^
- (facts |> map (fst o fst)
- |> take (the max_relevant)
- |> tag_list 1
- |> map index_string
- |> space_implode " "))
+ let val facts = facts |> map (fn ((name, _), _) => name ()) in
+ " " ^ label ^ ": " ^
+ (if is_none outcome then
+ "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
+ (used_facts |> map (with_index facts o fst)
+ |> sort (int_ord o pairself fst)
+ |> map index_string
+ |> space_implode " ") ^
+ (if length facts < the max_relevant then
+ " (of " ^ string_of_int (length facts) ^ ")"
+ else
+ "")
+ else
+ "Failure: " ^
+ (facts |> take (the max_relevant)
+ |> tag_list 1
+ |> map index_string
+ |> space_implode " "))
+ end
fun prove ok heading facts goal =
let
val facts = facts |> take (the max_relevant)
@@ -115,7 +117,7 @@
iter_facts ctxt params (max_relevant_slack * the max_relevant) goal
facts
val mash_facts = sugg_facts hyp_ts concl_t facts suggs
- val iter_mash_facts = iter_mash_facts iter_facts mash_facts
+ val iter_mash_facts = hybrid_facts (iter_facts, mash_facts)
val iter_s = prove iter_ok iterN iter_facts goal
val mash_s = prove mash_ok mashN mash_facts goal
val iter_mash_s = prove iter_mash_ok iter_mashN iter_mash_facts goal
--- a/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:03 2012 +0200
@@ -64,7 +64,7 @@
let
val suggs =
old_facts |> iter_facts ctxt params max_relevant goal
- |> map (fact_name_of o fst o fst)
+ |> map (fn ((name, _), _) => fact_name_of (name ()))
|> sort string_ord
val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n"
in File.append path s end
--- a/src/HOL/TPTP/sledgehammer_tactics.ML Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML Wed Jul 18 08:44:03 2012 +0200
@@ -42,7 +42,8 @@
chained_ths hyp_ts concl_t
val problem =
{state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
- facts = map Sledgehammer_Provers.Untranslated_Fact facts}
+ facts = facts |> map (apfst (apfst (fn name => name ())))
+ |> map Sledgehammer_Provers.Untranslated_Fact}
in
(case prover params (K (K (K ""))) problem of
{outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML Wed Jul 18 08:44:03 2012 +0200
@@ -22,7 +22,7 @@
Proof.context -> params -> string -> int -> relevance_fudge option
-> relevance_override -> thm list -> term list -> term
-> (((unit -> string) * stature) * thm) list
- -> ((string * stature) * thm) list
+ -> (((unit -> string) * stature) * thm) list
end;
structure Sledgehammer_Filter_Iter : SLEDGEHAMMER_FILTER_ITER =
@@ -537,7 +537,6 @@
relevance_filter ctxt thres0 decay max_relevant is_built_in_const
fudge override facts (chained_ths |> map prop_of) hyp_ts
(concl_t |> theory_constify fudge (Context.theory_name thy)))
- |> map (apfst (apfst (fn f => f ())))
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:03 2012 +0200
@@ -27,9 +27,9 @@
val iter_facts :
Proof.context -> params -> int -> thm
-> (((unit -> string) * stature) * thm) list
- -> ((string * stature) * thm) list
+ -> (((unit -> string) * stature) * thm) list
val run_prover :
- Proof.context -> params -> ((string * stature) * thm) list -> thm
+ Proof.context -> params -> (((unit -> string) * stature) * thm) list -> thm
-> prover_result
val generate_accessibility : theory -> bool -> string -> unit
val generate_features : theory -> bool -> string -> unit
@@ -47,7 +47,7 @@
val relevant_facts :
Proof.context -> params -> string -> int -> relevance_override -> thm list
-> term list -> term -> (((unit -> string) * stature) * thm) list
- -> ((string * stature) * thm) list
+ -> (((unit -> string) * stature) * thm) list
end;
structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
@@ -265,7 +265,8 @@
let
val problem =
{state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
- facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
+ facts = facts |> map (apfst (apfst (fn name => name ())))
+ |> map Sledgehammer_Provers.Untranslated_Fact}
val prover =
Sledgehammer_Minimize.get_minimizing_prover ctxt
Sledgehammer_Provers.Normal (hd provers)
@@ -339,10 +340,10 @@
if exists (is_dep dep) accum then
accum
else case find_first (is_dep dep) facts of
- SOME ((name, status), th) => accum @ [((name (), status), th)]
+ SOME ((name, status), th) => accum @ [((name, status), th)]
| NONE => accum (* shouldn't happen *)
fun fix_name ((_, stature), th) =
- ((th |> Thm.get_name_hint |> fact_name_of, stature), th)
+ ((fn () => th |> Thm.get_name_hint |> fact_name_of, stature), th)
fun do_thm th =
let
val name = Thm.get_name_hint th
@@ -391,7 +392,7 @@
(override as {add, only, ...}) chained_ths hyp_ts concl_t
facts =
if only then
- facts |> map (apfst (apfst (fn f => f ()))) (* ###*)
+ facts
else if max_relevant <= 0 then
[]
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Jul 18 08:44:03 2012 +0200
@@ -225,6 +225,7 @@
| NONE => I)
|> relevant_facts ctxt params (hd provers) max_max_relevant
relevance_override chained_ths hyp_ts concl_t
+ |> map (apfst (apfst (fn name => name ())))
|> tap (fn facts =>
if debug then
label ^ plural_s (length provers) ^ ": " ^