--- a/src/HOL/TPTP/mash_eval.ML Wed Jul 14 14:24:55 2021 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 14 15:18:11 2021 +0200
@@ -123,10 +123,10 @@
val facts =
suggs
|> find_suggested_facts ctxt facts
- |> map (fact_of_raw_fact #> nickify)
+ |> map (fact_of_lazy_fact #> nickify)
|> inst_inducts ? instantiate_inducts ctxt hyp_ts concl_t
|> take (the max_facts)
- |> map fact_of_raw_fact
+ |> map fact_of_lazy_fact
val ctxt = ctxt |> set_file_name method prob_dir_name
val res as {outcome, ...} = run_prover_for_mash ctxt params prover name facts goal
val ok = if is_none outcome then 1 else 0
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Jul 14 14:24:55 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Jul 14 15:18:11 2021 +0200
@@ -10,7 +10,7 @@
type status = ATP_Problem_Generate.status
type stature = ATP_Problem_Generate.stature
- type raw_fact = ((unit -> string) * stature) * thm (* TODO: rename to lazy_fact *)
+ type lazy_fact = ((unit -> string) * stature) * thm
type fact = (string * stature) * thm
type fact_override =
@@ -30,15 +30,14 @@
val fact_distinct : (term * term -> bool) -> ('a * thm) list -> ('a * thm) list
val instantiate_inducts : Proof.context -> term list -> term ->
(((unit -> string) * 'a) * thm) list -> (((unit -> string) * 'a) * thm) list
- val fact_of_raw_fact : raw_fact -> fact
+ val fact_of_lazy_fact : lazy_fact -> fact
val is_useful_unnamed_local_fact : Proof.context -> thm -> bool
val all_facts : Proof.context -> bool -> Keyword.keywords -> thm list -> thm list ->
- status Termtab.table -> raw_fact list
+ status Termtab.table -> lazy_fact list
val nearly_all_facts : Proof.context -> bool -> fact_override -> Keyword.keywords ->
- status Termtab.table -> thm list -> term list -> term -> raw_fact list
- val drop_duplicate_facts : raw_fact list -> raw_fact list
-
+ status Termtab.table -> thm list -> term list -> term -> lazy_fact list
+ val drop_duplicate_facts : lazy_fact list -> lazy_fact list
end;
structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
@@ -48,7 +47,7 @@
open ATP_Problem_Generate
open Sledgehammer_Util
-type raw_fact = ((unit -> string) * stature) * thm
+type lazy_fact = ((unit -> string) * stature) * thm
type fact = (string * stature) * thm
type fact_override =
@@ -431,7 +430,7 @@
maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
end
-fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th)
+fun fact_of_lazy_fact ((name, stature), th) = ((name (), stature), th)
fun fact_count facts = Facts.fold_static (K (Integer.add 1)) facts 0
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Jul 14 14:24:55 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Jul 14 15:18:11 2021 +0200
@@ -8,7 +8,7 @@
signature SLEDGEHAMMER_MASH =
sig
type stature = ATP_Problem_Generate.stature
- type raw_fact = Sledgehammer_Fact.raw_fact
+ type lazy_fact = Sledgehammer_Fact.lazy_fact
type fact = Sledgehammer_Fact.fact
type fact_override = Sledgehammer_Fact.fact_override
type params = Sledgehammer_Prover.params
@@ -56,7 +56,7 @@
val features_of : Proof.context -> string -> stature -> term list -> string list
val trim_dependencies : string list -> string list option
val isar_dependencies_of : string Symtab.table * string Symtab.table -> thm -> string list option
- val prover_dependencies_of : Proof.context -> params -> string -> int -> raw_fact list ->
+ val prover_dependencies_of : Proof.context -> params -> string -> int -> lazy_fact list ->
string Symtab.table * string Symtab.table -> thm -> bool * string list
val attach_parents_to_facts : ('a * thm) list -> ('a * thm) list ->
(string list * ('a * thm)) list
@@ -67,12 +67,12 @@
val find_mash_suggestions : Proof.context -> int -> string list -> ('a * thm) list ->
('a * thm) list -> ('a * thm) list -> ('a * thm) list * ('a * thm) list
val mash_suggested_facts : Proof.context -> string -> params -> int -> term list -> term ->
- raw_fact list -> fact list * fact list
+ lazy_fact list -> fact list * fact list
val mash_unlearn : Proof.context -> unit
val mash_learn_proof : Proof.context -> params -> term -> thm list -> unit
val mash_learn_facts : Proof.context -> params -> string -> int -> bool -> Time.time ->
- raw_fact list -> string
+ lazy_fact list -> string
val mash_learn : Proof.context -> params -> fact_override -> thm list -> bool -> unit
val mash_can_suggest_facts : Proof.context -> bool
val mash_can_suggest_facts_fast : Proof.context -> bool
@@ -81,7 +81,7 @@
val mepo_weight : real
val mash_weight : real
val relevant_facts : Proof.context -> params -> string -> int -> fact_override -> term list ->
- term -> raw_fact list -> (string * fact list) list
+ term -> lazy_fact list -> (string * fact list) list
end;
structure Sledgehammer_MaSh : SLEDGEHAMMER_MASH =
@@ -1221,7 +1221,7 @@
val unknown = filter_out (is_fact_in_graph access_G o snd) facts
in
find_mash_suggestions ctxt max_suggs suggs facts chained unknown
- |> apply2 (map fact_of_raw_fact)
+ |> apply2 (map fact_of_lazy_fact)
end)
end
@@ -1537,7 +1537,7 @@
if not (subset (op =) (the_list fact_filter, fact_filters)) then
error ("Unknown fact filter: " ^ quote (the fact_filter))
else if only then
- [("", map fact_of_raw_fact facts)]
+ [("", map fact_of_lazy_fact facts)]
else if max_facts <= 0 orelse null facts then
[("", [])]
else
@@ -1604,7 +1604,8 @@
(case add_ths of
[] => accepts
| _ =>
- (unique_facts |> filter in_add |> map fact_of_raw_fact) @ (accepts |> filter_out in_add))
+ (unique_facts |> filter in_add |> map fact_of_lazy_fact)
+ @ (accepts |> filter_out in_add))
|> take max_facts
fun mepo () =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Jul 14 14:24:55 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed Jul 14 15:18:11 2021 +0200
@@ -8,7 +8,7 @@
signature SLEDGEHAMMER_MEPO =
sig
type stature = ATP_Problem_Generate.stature
- type raw_fact = Sledgehammer_Fact.raw_fact
+ type lazy_fact = Sledgehammer_Fact.lazy_fact
type fact = Sledgehammer_Fact.fact
type params = Sledgehammer_Prover.params
@@ -36,7 +36,7 @@
val pseudo_abs_name : string
val default_relevance_fudge : relevance_fudge
val mepo_suggested_facts : Proof.context -> params -> int -> relevance_fudge option ->
- term list -> term -> raw_fact list -> fact list
+ term list -> term -> lazy_fact list -> fact list
end;
structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =
@@ -355,7 +355,7 @@
fun take_most_relevant ctxt max_facts remaining_max
({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
- (candidates : ((raw_fact * (string * ptype) list) * real) list) =
+ (candidates : ((lazy_fact * (string * ptype) list) * real) list) =
let
val max_imperfect =
Real.ceil (Math.pow (max_imperfect,
@@ -547,7 +547,7 @@
else
relevance_filter ctxt thres0 decay max_facts fudge facts hyp_ts
(concl_t |> theory_constify fudge (Context.theory_name thy)))
- |> map fact_of_raw_fact
+ |> map fact_of_lazy_fact
end
end;