distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jan 31 17:54:05 2013 +0100
@@ -478,7 +478,6 @@
(the_default default_max_facts max_facts)
Sledgehammer_Fact.no_fact_override hyp_ts concl_t
|> #1 (*###*)
- |> map (apfst (apfst (fn name => name ())))
|> tap (fn facts =>
"Line " ^ str0 (Position.line_of pos) ^ ": " ^
(if null facts then
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Thu Jan 31 17:54:05 2013 +0100
@@ -136,7 +136,7 @@
|> Sledgehammer_MePo.mepo_suggested_facts ctxt params
default_prover (the_default default_max_facts max_facts)
(SOME relevance_fudge) hyp_ts concl_t
- |> map ((fn name => name ()) o fst o fst)
+ |> map (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 Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Thu Jan 31 17:54:05 2013 +0100
@@ -71,7 +71,7 @@
val str_of_method = enclose " " ": "
fun str_of_result method facts ({outcome, run_time, used_facts, ...}
: prover_result) =
- let val facts = facts |> map (fn ((name, _), _) => name ()) in
+ let val facts = facts |> map (fst o fst) in
str_of_method method ^
(if is_none outcome then
"Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
@@ -111,7 +111,7 @@
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
val isar_deps = isar_dependencies_of name_tabs th
val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
- val find_suggs = find_suggested_facts facts
+ val find_suggs = find_suggested_facts facts #> map fact_of_raw_fact
fun get_facts [] compute = compute facts
| get_facts suggs _ = find_suggs suggs
val mepo_facts =
@@ -121,7 +121,8 @@
|> weight_mepo_facts
fun mash_of suggs =
get_facts suggs (fn _ =>
- find_mash_suggestions slack_max_facts suggs facts [] [] |> fst)
+ find_mash_suggestions slack_max_facts suggs facts [] []
+ |> fst |> map fact_of_raw_fact)
|> weight_mash_facts
val mash_isar_facts = mash_of mash_isar_suggs
val mash_prover_facts = mash_of mash_prover_suggs
@@ -160,6 +161,7 @@
|> map (get #> nickify)
|> maybe_instantiate_inducts ctxt hyp_ts concl_t
|> take (the max_facts)
+ |> map fact_of_raw_fact
val ctxt = ctxt |> set_file_name method prob_dir_name
val res as {outcome, ...} =
run_prover_for_mash ctxt params prover facts goal
--- a/src/HOL/TPTP/sledgehammer_tactics.ML Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML Thu Jan 31 17:54:05 2013 +0100
@@ -45,8 +45,7 @@
|> #1
val problem =
{state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
- facts = facts |> map (apfst (apfst (fn name => name ())))
- |> map Untranslated_Fact}
+ facts = facts |> map 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_fact.ML Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Jan 31 17:54:05 2013 +0100
@@ -10,7 +10,8 @@
type status = ATP_Problem_Generate.status
type stature = ATP_Problem_Generate.stature
- type fact = ((unit -> string) * stature) * thm
+ type raw_fact = ((unit -> string) * stature) * thm
+ type fact = (string * stature) * thm
type fact_override =
{add : (Facts.ref * Attrib.src list) list,
@@ -33,12 +34,13 @@
Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
-> (((unit -> string) * 'a) * thm) list
val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
+ val fact_of_raw_fact : raw_fact -> fact
val all_facts :
Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list
- -> status Termtab.table -> fact list
+ -> status Termtab.table -> raw_fact list
val nearly_all_facts :
Proof.context -> bool -> fact_override -> unit Symtab.table
- -> status Termtab.table -> thm list -> term list -> term -> fact list
+ -> status Termtab.table -> thm list -> term list -> term -> raw_fact list
end;
structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
@@ -49,7 +51,8 @@
open Metis_Tactic
open Sledgehammer_Util
-type fact = ((unit -> string) * stature) * thm
+type raw_fact = ((unit -> string) * stature) * thm
+type fact = (string * stature) * thm
type fact_override =
{add : (Facts.ref * Attrib.src list) list,
@@ -419,6 +422,8 @@
fun maybe_filter_no_atps ctxt =
not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
+fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th)
+
fun all_facts ctxt generous ho_atp reserved add_ths chained css =
let
val thy = Proof_Context.theory_of ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Jan 31 17:54:05 2013 +0100
@@ -7,6 +7,7 @@
signature SLEDGEHAMMER_MASH =
sig
type stature = ATP_Problem_Generate.stature
+ type raw_fact = Sledgehammer_Fact.raw_fact
type fact = Sledgehammer_Fact.fact
type fact_override = Sledgehammer_Fact.fact_override
type params = Sledgehammer_Provers.params
@@ -62,7 +63,7 @@
val isar_dependencies_of :
string Symtab.table * string Symtab.table -> thm -> string list
val prover_dependencies_of :
- Proof.context -> params -> string -> int -> fact list
+ Proof.context -> params -> string -> int -> raw_fact list
-> string Symtab.table * string Symtab.table -> thm
-> bool * string list
val weight_mepo_facts : 'a list -> ('a * real) list
@@ -71,8 +72,8 @@
int -> string list -> ('b * thm) list -> ('b * thm) list -> ('b * thm) list
-> ('b * thm) list * ('b * thm) list
val mash_suggested_facts :
- Proof.context -> params -> string -> int -> term list -> term -> fact list
- -> fact list * fact list
+ Proof.context -> params -> string -> int -> term list -> term
+ -> raw_fact list -> fact list * fact list
val mash_learn_proof :
Proof.context -> params -> string -> term -> ('a * thm) list -> thm list
-> unit
@@ -85,7 +86,7 @@
val mash_weight : real
val relevant_facts :
Proof.context -> params -> string -> int -> fact_override -> term list
- -> term -> fact list -> fact list * fact list * fact list
+ -> term -> raw_fact list -> fact list * fact list * fact list
val kill_learners : unit -> unit
val running_learners : unit -> unit
end;
@@ -531,8 +532,7 @@
let
val problem =
{state = Proof.init ctxt, goal = goal, subgoal = 1, subgoal_count = 1,
- facts = facts |> map (apfst (apfst (fn name => name ())))
- |> map Untranslated_Fact}
+ facts = facts |> map Untranslated_Fact}
in
get_minimizing_isar_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
problem
@@ -687,14 +687,13 @@
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)
- fun nickify ((_, stature), th) =
- ((fn () => nickname_of_thm th, stature), th)
+ fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th)
fun is_dep dep (_, th) = nickname_of_thm th = dep
fun add_isar_dep facts dep accum =
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 ((_, status), th) => accum @ [(("", status), th)]
| NONE => accum (* shouldn't happen *)
val facts =
facts
@@ -825,7 +824,10 @@
(parents, feats, hints))
end)
val unknown = facts |> filter_out (is_fact_in_graph access_G snd)
- in find_mash_suggestions max_facts suggs facts chained unknown end
+ in
+ find_mash_suggestions max_facts suggs facts chained unknown
+ |> pairself (map fact_of_raw_fact)
+ end
fun learn_wrt_access_graph ctxt (name, parents, feats, deps) (learns, graph) =
let
@@ -1099,7 +1101,9 @@
if not (subset (op =) (the_list fact_filter, fact_filters)) then
error ("Unknown fact filter: " ^ quote (the fact_filter) ^ ".")
else if only then
- (facts, facts, facts)
+ let val facts = facts |> map fact_of_raw_fact in
+ (facts, facts, facts)
+ end
else if max_facts <= 0 orelse null facts then
([], [], [])
else
@@ -1129,11 +1133,12 @@
else
mepoN
val add_ths = Attrib.eval_thms ctxt add
- val in_add = member Thm.eq_thm_prop add_ths o snd
+ fun in_add (_, th) = member Thm.eq_thm_prop add_ths th
fun add_and_take accepts =
(case add_ths of
[] => accepts
- | _ => (facts |> filter in_add) @ (accepts |> filter_out in_add))
+ | _ => (facts |> filter in_add |> map fact_of_raw_fact) @
+ (accepts |> filter_out in_add))
|> take max_facts
fun mepo () =
mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Thu Jan 31 17:54:05 2013 +0100
@@ -8,6 +8,7 @@
signature SLEDGEHAMMER_MEPO =
sig
type stature = ATP_Problem_Generate.stature
+ type raw_fact = Sledgehammer_Fact.raw_fact
type fact = Sledgehammer_Fact.fact
type params = Sledgehammer_Provers.params
type relevance_fudge = Sledgehammer_Provers.relevance_fudge
@@ -20,7 +21,7 @@
-> string list
val mepo_suggested_facts :
Proof.context -> params -> string -> int -> relevance_fudge option
- -> term list -> term -> fact list -> fact list
+ -> term list -> term -> raw_fact list -> fact list
end;
structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
@@ -337,7 +338,7 @@
fun take_most_relevant ctxt max_facts remaining_max
({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
- (candidates : ((fact * (string * ptype) list) * real) list) =
+ (candidates : ((raw_fact * (string * ptype) list) * real) list) =
let
val max_imperfect =
Real.ceil (Math.pow (max_imperfect,
@@ -533,6 +534,7 @@
relevance_filter ctxt thres0 decay max_facts is_built_in_const fudge
facts hyp_ts
(concl_t |> theory_constify fudge (Context.theory_name thy)))
+ |> map fact_of_raw_fact
end
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 31 17:54:05 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Jan 31 17:54:05 2013 +0100
@@ -237,7 +237,6 @@
|> relevant_facts ctxt params (hd provers) max_max_facts fact_override
hyp_ts concl_t
|> #1 (*###*)
- |> map (apfst (apfst (fn name => name ())))
|> tap (fn facts =>
if verbose then
label ^ plural_s (length provers) ^ ": " ^