# HG changeset patch
# User blanchet
# Date 1626268691 -7200
# Node ID e5322146e7e81a425d9a162c839683720ad6800b
# Parent  906ecb04914141ea2a676dbcb51add177c3ecd29
tuning

diff -r 906ecb049141 -r e5322146e7e8 src/HOL/TPTP/mash_eval.ML
--- 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
diff -r 906ecb049141 -r e5322146e7e8 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- 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
 
diff -r 906ecb049141 -r e5322146e7e8 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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 () =
diff -r 906ecb049141 -r e5322146e7e8 src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- 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;