src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML
changeset 48248 b6eb45a52c28
parent 48237 d7ad89f60768
child 48250 1065c307fafe
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML	Wed Jul 11 21:43:19 2012 +0200
     1.3 @@ -0,0 +1,600 @@
     1.4 +(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML
     1.5 +    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     1.6 +    Author:     Jasmin Blanchette, TU Muenchen
     1.7 +
     1.8 +Sledgehammer's iterative relevance filter.
     1.9 +*)
    1.10 +
    1.11 +signature SLEDGEHAMMER_FILTER_ITER =
    1.12 +sig
    1.13 +  type stature = ATP_Problem_Generate.stature
    1.14 +
    1.15 +  type relevance_fudge =
    1.16 +    {local_const_multiplier : real,
    1.17 +     worse_irrel_freq : real,
    1.18 +     higher_order_irrel_weight : real,
    1.19 +     abs_rel_weight : real,
    1.20 +     abs_irrel_weight : real,
    1.21 +     skolem_irrel_weight : real,
    1.22 +     theory_const_rel_weight : real,
    1.23 +     theory_const_irrel_weight : real,
    1.24 +     chained_const_irrel_weight : real,
    1.25 +     intro_bonus : real,
    1.26 +     elim_bonus : real,
    1.27 +     simp_bonus : real,
    1.28 +     local_bonus : real,
    1.29 +     assum_bonus : real,
    1.30 +     chained_bonus : real,
    1.31 +     max_imperfect : real,
    1.32 +     max_imperfect_exp : real,
    1.33 +     threshold_divisor : real,
    1.34 +     ridiculous_threshold : real}
    1.35 +
    1.36 +  type relevance_override =
    1.37 +    {add : (Facts.ref * Attrib.src list) list,
    1.38 +     del : (Facts.ref * Attrib.src list) list,
    1.39 +     only : bool}
    1.40 +
    1.41 +  val trace : bool Config.T
    1.42 +  val ignore_no_atp : bool Config.T
    1.43 +  val instantiate_inducts : bool Config.T
    1.44 +  val pseudo_abs_name : string
    1.45 +  val pseudo_skolem_prefix : string
    1.46 +  val const_names_in_fact :
    1.47 +    theory -> (string * typ -> term list -> bool * term list) -> term
    1.48 +    -> string list
    1.49 +  val iterative_relevant_facts :
    1.50 +    Proof.context -> real * real -> int
    1.51 +    -> (string * typ -> term list -> bool * term list) -> relevance_fudge
    1.52 +    -> relevance_override -> thm list -> term list -> term
    1.53 +    -> (((unit -> string) * stature) * thm) list
    1.54 +    -> ((string * stature) * thm) list
    1.55 +end;
    1.56 +
    1.57 +structure Sledgehammer_Filter_Iter : SLEDGEHAMMER_FILTER_ITER =
    1.58 +struct
    1.59 +
    1.60 +open ATP_Problem_Generate
    1.61 +
    1.62 +val trace =
    1.63 +  Attrib.setup_config_bool @{binding sledgehammer_filter_trace} (K false)
    1.64 +fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    1.65 +
    1.66 +(* experimental features *)
    1.67 +val ignore_no_atp =
    1.68 +  Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
    1.69 +val instantiate_inducts =
    1.70 +  Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
    1.71 +
    1.72 +type relevance_fudge =
    1.73 +  {local_const_multiplier : real,
    1.74 +   worse_irrel_freq : real,
    1.75 +   higher_order_irrel_weight : real,
    1.76 +   abs_rel_weight : real,
    1.77 +   abs_irrel_weight : real,
    1.78 +   skolem_irrel_weight : real,
    1.79 +   theory_const_rel_weight : real,
    1.80 +   theory_const_irrel_weight : real,
    1.81 +   chained_const_irrel_weight : real,
    1.82 +   intro_bonus : real,
    1.83 +   elim_bonus : real,
    1.84 +   simp_bonus : real,
    1.85 +   local_bonus : real,
    1.86 +   assum_bonus : real,
    1.87 +   chained_bonus : real,
    1.88 +   max_imperfect : real,
    1.89 +   max_imperfect_exp : real,
    1.90 +   threshold_divisor : real,
    1.91 +   ridiculous_threshold : real}
    1.92 +
    1.93 +type relevance_override =
    1.94 +  {add : (Facts.ref * Attrib.src list) list,
    1.95 +   del : (Facts.ref * Attrib.src list) list,
    1.96 +   only : bool}
    1.97 +
    1.98 +val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
    1.99 +val pseudo_abs_name = sledgehammer_prefix ^ "abs"
   1.100 +val pseudo_skolem_prefix = sledgehammer_prefix ^ "sko"
   1.101 +val theory_const_suffix = Long_Name.separator ^ " 1"
   1.102 +
   1.103 +fun order_of_type (Type (@{type_name fun}, [T1, T2])) =
   1.104 +    Int.max (order_of_type T1 + 1, order_of_type T2)
   1.105 +  | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0
   1.106 +  | order_of_type _ = 0
   1.107 +
   1.108 +(* An abstraction of Isabelle types and first-order terms *)
   1.109 +datatype pattern = PVar | PApp of string * pattern list
   1.110 +datatype ptype = PType of int * pattern list
   1.111 +
   1.112 +fun string_for_pattern PVar = "_"
   1.113 +  | string_for_pattern (PApp (s, ps)) =
   1.114 +    if null ps then s else s ^ string_for_patterns ps
   1.115 +and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
   1.116 +fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
   1.117 +
   1.118 +(*Is the second type an instance of the first one?*)
   1.119 +fun match_pattern (PVar, _) = true
   1.120 +  | match_pattern (PApp _, PVar) = false
   1.121 +  | match_pattern (PApp (s, ps), PApp (t, qs)) =
   1.122 +    s = t andalso match_patterns (ps, qs)
   1.123 +and match_patterns (_, []) = true
   1.124 +  | match_patterns ([], _) = false
   1.125 +  | match_patterns (p :: ps, q :: qs) =
   1.126 +    match_pattern (p, q) andalso match_patterns (ps, qs)
   1.127 +fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs)
   1.128 +
   1.129 +(* Is there a unifiable constant? *)
   1.130 +fun pconst_mem f consts (s, ps) =
   1.131 +  exists (curry (match_ptype o f) ps)
   1.132 +         (map snd (filter (curry (op =) s o fst) consts))
   1.133 +fun pconst_hyper_mem f const_tab (s, ps) =
   1.134 +  exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s))
   1.135 +
   1.136 +fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts)
   1.137 +  | pattern_for_type (TFree (s, _)) = PApp (s, [])
   1.138 +  | pattern_for_type (TVar _) = PVar
   1.139 +
   1.140 +(* Pairs a constant with the list of its type instantiations. *)
   1.141 +fun ptype thy const x =
   1.142 +  (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
   1.143 +   else [])
   1.144 +fun rich_ptype thy const (s, T) =
   1.145 +  PType (order_of_type T, ptype thy const (s, T))
   1.146 +fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T))
   1.147 +
   1.148 +fun string_for_hyper_pconst (s, ps) =
   1.149 +  s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
   1.150 +
   1.151 +(* Add a pconstant to the table, but a [] entry means a standard
   1.152 +   connective, which we ignore.*)
   1.153 +fun add_pconst_to_table also_skolem (s, p) =
   1.154 +  if (not also_skolem andalso String.isPrefix pseudo_skolem_prefix s) then I
   1.155 +  else Symtab.map_default (s, [p]) (insert (op =) p)
   1.156 +
   1.157 +(* Set constants tend to pull in too many irrelevant facts. We limit the damage
   1.158 +   by treating them more or less as if they were built-in but add their
   1.159 +   axiomatization at the end. *)
   1.160 +val set_consts = [@{const_name Collect}, @{const_name Set.member}]
   1.161 +val set_thms = @{thms Collect_mem_eq mem_Collect_eq Collect_cong}
   1.162 +
   1.163 +fun add_pconsts_in_term thy is_built_in_const also_skolems pos =
   1.164 +  let
   1.165 +    val flip = Option.map not
   1.166 +    (* We include free variables, as well as constants, to handle locales. For
   1.167 +       each quantifiers that must necessarily be skolemized by the automatic
   1.168 +       prover, we introduce a fresh constant to simulate the effect of
   1.169 +       Skolemization. *)
   1.170 +    fun do_const const ext_arg (x as (s, _)) ts =
   1.171 +      let val (built_in, ts) = is_built_in_const x ts in
   1.172 +        if member (op =) set_consts s then
   1.173 +          fold (do_term ext_arg) ts
   1.174 +        else
   1.175 +          (not built_in
   1.176 +           ? add_pconst_to_table also_skolems (rich_pconst thy const x))
   1.177 +          #> fold (do_term false) ts
   1.178 +      end
   1.179 +    and do_term ext_arg t =
   1.180 +      case strip_comb t of
   1.181 +        (Const x, ts) => do_const true ext_arg x ts
   1.182 +      | (Free x, ts) => do_const false ext_arg x ts
   1.183 +      | (Abs (_, T, t'), ts) =>
   1.184 +        ((null ts andalso not ext_arg)
   1.185 +         (* Since lambdas on the right-hand side of equalities are usually
   1.186 +            extensionalized later by "abs_extensionalize_term", we don't
   1.187 +            penalize them here. *)
   1.188 +         ? add_pconst_to_table true (pseudo_abs_name,
   1.189 +                                     PType (order_of_type T + 1, [])))
   1.190 +        #> fold (do_term false) (t' :: ts)
   1.191 +      | (_, ts) => fold (do_term false) ts
   1.192 +    fun do_quantifier will_surely_be_skolemized abs_T body_t =
   1.193 +      do_formula pos body_t
   1.194 +      #> (if also_skolems andalso will_surely_be_skolemized then
   1.195 +            add_pconst_to_table true (pseudo_skolem_prefix ^ serial_string (),
   1.196 +                                      PType (order_of_type abs_T, []))
   1.197 +          else
   1.198 +            I)
   1.199 +    and do_term_or_formula ext_arg T =
   1.200 +      if T = HOLogic.boolT then do_formula NONE else do_term ext_arg
   1.201 +    and do_formula pos t =
   1.202 +      case t of
   1.203 +        Const (@{const_name all}, _) $ Abs (_, T, t') =>
   1.204 +        do_quantifier (pos = SOME false) T t'
   1.205 +      | @{const "==>"} $ t1 $ t2 =>
   1.206 +        do_formula (flip pos) t1 #> do_formula pos t2
   1.207 +      | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
   1.208 +        do_term_or_formula false T t1 #> do_term_or_formula true T t2
   1.209 +      | @{const Trueprop} $ t1 => do_formula pos t1
   1.210 +      | @{const False} => I
   1.211 +      | @{const True} => I
   1.212 +      | @{const Not} $ t1 => do_formula (flip pos) t1
   1.213 +      | Const (@{const_name All}, _) $ Abs (_, T, t') =>
   1.214 +        do_quantifier (pos = SOME false) T t'
   1.215 +      | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
   1.216 +        do_quantifier (pos = SOME true) T t'
   1.217 +      | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
   1.218 +      | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
   1.219 +      | @{const HOL.implies} $ t1 $ t2 =>
   1.220 +        do_formula (flip pos) t1 #> do_formula pos t2
   1.221 +      | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
   1.222 +        do_term_or_formula false T t1 #> do_term_or_formula true T t2
   1.223 +      | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
   1.224 +        $ t1 $ t2 $ t3 =>
   1.225 +        do_formula NONE t1 #> fold (do_term_or_formula false T) [t2, t3]
   1.226 +      | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
   1.227 +        do_quantifier (is_some pos) T t'
   1.228 +      | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
   1.229 +        do_quantifier (pos = SOME false) T
   1.230 +                      (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
   1.231 +      | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
   1.232 +        do_quantifier (pos = SOME true) T
   1.233 +                      (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
   1.234 +      | (t0 as Const (_, @{typ bool})) $ t1 =>
   1.235 +        do_term false t0 #> do_formula pos t1  (* theory constant *)
   1.236 +      | _ => do_term false t
   1.237 +  in do_formula pos end
   1.238 +
   1.239 +fun pconsts_in_fact thy is_built_in_const t =
   1.240 +  Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
   1.241 +              (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true
   1.242 +                                                   (SOME true) t) []
   1.243 +
   1.244 +val const_names_in_fact = map fst ooo pconsts_in_fact
   1.245 +
   1.246 +(* Inserts a dummy "constant" referring to the theory name, so that relevance
   1.247 +   takes the given theory into account. *)
   1.248 +fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...}
   1.249 +                     : relevance_fudge) thy_name t =
   1.250 +  if exists (curry (op <) 0.0) [theory_const_rel_weight,
   1.251 +                                theory_const_irrel_weight] then
   1.252 +    Const (thy_name ^ theory_const_suffix, @{typ bool}) $ t
   1.253 +  else
   1.254 +    t
   1.255 +
   1.256 +fun theory_const_prop_of fudge th =
   1.257 +  theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
   1.258 +
   1.259 +fun pair_consts_fact thy is_built_in_const fudge fact =
   1.260 +  case fact |> snd |> theory_const_prop_of fudge
   1.261 +            |> pconsts_in_fact thy is_built_in_const of
   1.262 +    [] => NONE
   1.263 +  | consts => SOME ((fact, consts), NONE)
   1.264 +
   1.265 +(* A two-dimensional symbol table counts frequencies of constants. It's keyed
   1.266 +   first by constant name and second by its list of type instantiations. For the
   1.267 +   latter, we need a linear ordering on "pattern list". *)
   1.268 +
   1.269 +fun pattern_ord p =
   1.270 +  case p of
   1.271 +    (PVar, PVar) => EQUAL
   1.272 +  | (PVar, PApp _) => LESS
   1.273 +  | (PApp _, PVar) => GREATER
   1.274 +  | (PApp q1, PApp q2) =>
   1.275 +    prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2)
   1.276 +fun ptype_ord (PType p, PType q) =
   1.277 +  prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q)
   1.278 +
   1.279 +structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
   1.280 +
   1.281 +fun count_fact_consts thy fudge =
   1.282 +  let
   1.283 +    fun do_const const (s, T) ts =
   1.284 +      (* Two-dimensional table update. Constant maps to types maps to count. *)
   1.285 +      PType_Tab.map_default (rich_ptype thy const (s, T), 0) (Integer.add 1)
   1.286 +      |> Symtab.map_default (s, PType_Tab.empty)
   1.287 +      #> fold do_term ts
   1.288 +    and do_term t =
   1.289 +      case strip_comb t of
   1.290 +        (Const x, ts) => do_const true x ts
   1.291 +      | (Free x, ts) => do_const false x ts
   1.292 +      | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
   1.293 +      | (_, ts) => fold do_term ts
   1.294 +  in do_term o theory_const_prop_of fudge o snd end
   1.295 +
   1.296 +fun pow_int _ 0 = 1.0
   1.297 +  | pow_int x 1 = x
   1.298 +  | pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x
   1.299 +
   1.300 +(*The frequency of a constant is the sum of those of all instances of its type.*)
   1.301 +fun pconst_freq match const_tab (c, ps) =
   1.302 +  PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
   1.303 +                 (the (Symtab.lookup const_tab c)) 0
   1.304 +
   1.305 +
   1.306 +(* A surprising number of theorems contain only a few significant constants.
   1.307 +   These include all induction rules, and other general theorems. *)
   1.308 +
   1.309 +(* "log" seems best in practice. A constant function of one ignores the constant
   1.310 +   frequencies. Rare constants give more points if they are relevant than less
   1.311 +   rare ones. *)
   1.312 +fun rel_weight_for _ freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
   1.313 +
   1.314 +(* Irrelevant constants are treated differently. We associate lower penalties to
   1.315 +   very rare constants and very common ones -- the former because they can't
   1.316 +   lead to the inclusion of too many new facts, and the latter because they are
   1.317 +   so common as to be of little interest. *)
   1.318 +fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...}
   1.319 +                      : relevance_fudge) order freq =
   1.320 +  let val (k, x) = worse_irrel_freq |> `Real.ceil in
   1.321 +    (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
   1.322 +     else rel_weight_for order freq / rel_weight_for order k)
   1.323 +    * pow_int higher_order_irrel_weight (order - 1)
   1.324 +  end
   1.325 +
   1.326 +fun multiplier_for_const_name local_const_multiplier s =
   1.327 +  if String.isSubstring "." s then 1.0 else local_const_multiplier
   1.328 +
   1.329 +(* Computes a constant's weight, as determined by its frequency. *)
   1.330 +fun generic_pconst_weight local_const_multiplier abs_weight skolem_weight
   1.331 +                          theory_const_weight chained_const_weight weight_for f
   1.332 +                          const_tab chained_const_tab (c as (s, PType (m, _))) =
   1.333 +  if s = pseudo_abs_name then
   1.334 +    abs_weight
   1.335 +  else if String.isPrefix pseudo_skolem_prefix s then
   1.336 +    skolem_weight
   1.337 +  else if String.isSuffix theory_const_suffix s then
   1.338 +    theory_const_weight
   1.339 +  else
   1.340 +    multiplier_for_const_name local_const_multiplier s
   1.341 +    * weight_for m (pconst_freq (match_ptype o f) const_tab c)
   1.342 +    |> (if chained_const_weight < 1.0 andalso
   1.343 +           pconst_hyper_mem I chained_const_tab c then
   1.344 +          curry (op *) chained_const_weight
   1.345 +        else
   1.346 +          I)
   1.347 +
   1.348 +fun rel_pconst_weight ({local_const_multiplier, abs_rel_weight,
   1.349 +                        theory_const_rel_weight, ...} : relevance_fudge)
   1.350 +                      const_tab =
   1.351 +  generic_pconst_weight local_const_multiplier abs_rel_weight 0.0
   1.352 +                        theory_const_rel_weight 0.0 rel_weight_for I const_tab
   1.353 +                        Symtab.empty
   1.354 +
   1.355 +fun irrel_pconst_weight (fudge as {local_const_multiplier, abs_irrel_weight,
   1.356 +                                   skolem_irrel_weight,
   1.357 +                                   theory_const_irrel_weight,
   1.358 +                                   chained_const_irrel_weight, ...})
   1.359 +                        const_tab chained_const_tab =
   1.360 +  generic_pconst_weight local_const_multiplier abs_irrel_weight
   1.361 +                        skolem_irrel_weight theory_const_irrel_weight
   1.362 +                        chained_const_irrel_weight (irrel_weight_for fudge) swap
   1.363 +                        const_tab chained_const_tab
   1.364 +
   1.365 +fun stature_bonus ({intro_bonus, ...} : relevance_fudge) (_, Intro) =
   1.366 +    intro_bonus
   1.367 +  | stature_bonus {elim_bonus, ...} (_, Elim) = elim_bonus
   1.368 +  | stature_bonus {simp_bonus, ...} (_, Simp) = simp_bonus
   1.369 +  | stature_bonus {local_bonus, ...} (Local, _) = local_bonus
   1.370 +  | stature_bonus {assum_bonus, ...} (Assum, _) = assum_bonus
   1.371 +  | stature_bonus {chained_bonus, ...} (Chained, _) = chained_bonus
   1.372 +  | stature_bonus _ _ = 0.0
   1.373 +
   1.374 +fun is_odd_const_name s =
   1.375 +  s = pseudo_abs_name orelse String.isPrefix pseudo_skolem_prefix s orelse
   1.376 +  String.isSuffix theory_const_suffix s
   1.377 +
   1.378 +fun fact_weight fudge stature const_tab relevant_consts chained_consts
   1.379 +                fact_consts =
   1.380 +  case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
   1.381 +                   ||> filter_out (pconst_hyper_mem swap relevant_consts) of
   1.382 +    ([], _) => 0.0
   1.383 +  | (rel, irrel) =>
   1.384 +    if forall (forall (is_odd_const_name o fst)) [rel, irrel] then
   1.385 +      0.0
   1.386 +    else
   1.387 +      let
   1.388 +        val irrel = irrel |> filter_out (pconst_mem swap rel)
   1.389 +        val rel_weight =
   1.390 +          0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
   1.391 +        val irrel_weight =
   1.392 +          ~ (stature_bonus fudge stature)
   1.393 +          |> fold (curry (op +)
   1.394 +                   o irrel_pconst_weight fudge const_tab chained_consts) irrel
   1.395 +        val res = rel_weight / (rel_weight + irrel_weight)
   1.396 +      in if Real.isFinite res then res else 0.0 end
   1.397 +
   1.398 +type annotated_thm =
   1.399 +  (((unit -> string) * stature) * thm) * (string * ptype) list
   1.400 +
   1.401 +fun take_most_relevant ctxt max_relevant remaining_max
   1.402 +        ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
   1.403 +        (candidates : (annotated_thm * real) list) =
   1.404 +  let
   1.405 +    val max_imperfect =
   1.406 +      Real.ceil (Math.pow (max_imperfect,
   1.407 +                    Math.pow (Real.fromInt remaining_max
   1.408 +                              / Real.fromInt max_relevant, max_imperfect_exp)))
   1.409 +    val (perfect, imperfect) =
   1.410 +      candidates |> sort (Real.compare o swap o pairself snd)
   1.411 +                 |> take_prefix (fn (_, w) => w > 0.99999)
   1.412 +    val ((accepts, more_rejects), rejects) =
   1.413 +      chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
   1.414 +  in
   1.415 +    trace_msg ctxt (fn () =>
   1.416 +        "Actually passed (" ^ string_of_int (length accepts) ^ " of " ^
   1.417 +        string_of_int (length candidates) ^ "): " ^
   1.418 +        (accepts |> map (fn ((((name, _), _), _), weight) =>
   1.419 +                            name () ^ " [" ^ Real.toString weight ^ "]")
   1.420 +                 |> commas));
   1.421 +    (accepts, more_rejects @ rejects)
   1.422 +  end
   1.423 +
   1.424 +fun if_empty_replace_with_scope thy is_built_in_const facts sc tab =
   1.425 +  if Symtab.is_empty tab then
   1.426 +    Symtab.empty
   1.427 +    |> fold (add_pconsts_in_term thy is_built_in_const false (SOME false))
   1.428 +            (map_filter (fn ((_, (sc', _)), th) =>
   1.429 +                            if sc' = sc then SOME (prop_of th) else NONE) facts)
   1.430 +  else
   1.431 +    tab
   1.432 +
   1.433 +fun consider_arities is_built_in_const th =
   1.434 +  let
   1.435 +    fun aux _ _ NONE = NONE
   1.436 +      | aux t args (SOME tab) =
   1.437 +        case t of
   1.438 +          t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 []
   1.439 +        | Const (x as (s, _)) =>
   1.440 +          (if is_built_in_const x args |> fst then
   1.441 +             SOME tab
   1.442 +           else case Symtab.lookup tab s of
   1.443 +             NONE => SOME (Symtab.update (s, length args) tab)
   1.444 +           | SOME n => if n = length args then SOME tab else NONE)
   1.445 +        | _ => SOME tab
   1.446 +  in aux (prop_of th) [] end
   1.447 +
   1.448 +(* FIXME: This is currently only useful for polymorphic type encodings. *)
   1.449 +fun could_benefit_from_ext is_built_in_const facts =
   1.450 +  fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
   1.451 +  |> is_none
   1.452 +
   1.453 +(* High enough so that it isn't wrongly considered as very relevant (e.g., for E
   1.454 +   weights), but low enough so that it is unlikely to be truncated away if few
   1.455 +   facts are included. *)
   1.456 +val special_fact_index = 75
   1.457 +
   1.458 +fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
   1.459 +        (fudge as {threshold_divisor, ridiculous_threshold, ...})
   1.460 +        ({add, del, ...} : relevance_override) facts chained_ts hyp_ts concl_t =
   1.461 +  let
   1.462 +    val thy = Proof_Context.theory_of ctxt
   1.463 +    val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
   1.464 +    val add_pconsts = add_pconsts_in_term thy is_built_in_const false o SOME
   1.465 +    val chained_const_tab = Symtab.empty |> fold (add_pconsts true) chained_ts
   1.466 +    val goal_const_tab =
   1.467 +      Symtab.empty |> fold (add_pconsts true) hyp_ts
   1.468 +                   |> add_pconsts false concl_t
   1.469 +      |> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
   1.470 +      |> fold (if_empty_replace_with_scope thy is_built_in_const facts)
   1.471 +              [Chained, Assum, Local]
   1.472 +    val add_ths = Attrib.eval_thms ctxt add
   1.473 +    val del_ths = Attrib.eval_thms ctxt del
   1.474 +    val facts = facts |> filter_out (member Thm.eq_thm_prop del_ths o snd)
   1.475 +    fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
   1.476 +      let
   1.477 +        fun relevant [] _ [] =
   1.478 +            (* Nothing has been added this iteration. *)
   1.479 +            if j = 0 andalso threshold >= ridiculous_threshold then
   1.480 +              (* First iteration? Try again. *)
   1.481 +              iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
   1.482 +                   hopeless hopeful
   1.483 +            else
   1.484 +              []
   1.485 +          | relevant candidates rejects [] =
   1.486 +            let
   1.487 +              val (accepts, more_rejects) =
   1.488 +                take_most_relevant ctxt max_relevant remaining_max fudge
   1.489 +                                   candidates
   1.490 +              val rel_const_tab' =
   1.491 +                rel_const_tab
   1.492 +                |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
   1.493 +              fun is_dirty (c, _) =
   1.494 +                Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
   1.495 +              val (hopeful_rejects, hopeless_rejects) =
   1.496 +                 (rejects @ hopeless, ([], []))
   1.497 +                 |-> fold (fn (ax as (_, consts), old_weight) =>
   1.498 +                              if exists is_dirty consts then
   1.499 +                                apfst (cons (ax, NONE))
   1.500 +                              else
   1.501 +                                apsnd (cons (ax, old_weight)))
   1.502 +                 |>> append (more_rejects
   1.503 +                             |> map (fn (ax as (_, consts), old_weight) =>
   1.504 +                                        (ax, if exists is_dirty consts then NONE
   1.505 +                                             else SOME old_weight)))
   1.506 +              val threshold =
   1.507 +                1.0 - (1.0 - threshold)
   1.508 +                      * Math.pow (decay, Real.fromInt (length accepts))
   1.509 +              val remaining_max = remaining_max - length accepts
   1.510 +            in
   1.511 +              trace_msg ctxt (fn () => "New or updated constants: " ^
   1.512 +                  commas (rel_const_tab' |> Symtab.dest
   1.513 +                          |> subtract (op =) (rel_const_tab |> Symtab.dest)
   1.514 +                          |> map string_for_hyper_pconst));
   1.515 +              map (fst o fst) accepts @
   1.516 +              (if remaining_max = 0 then
   1.517 +                 []
   1.518 +               else
   1.519 +                 iter (j + 1) remaining_max threshold rel_const_tab'
   1.520 +                      hopeless_rejects hopeful_rejects)
   1.521 +            end
   1.522 +          | relevant candidates rejects
   1.523 +                     (((ax as (((_, stature), _), fact_consts)), cached_weight)
   1.524 +                      :: hopeful) =
   1.525 +            let
   1.526 +              val weight =
   1.527 +                case cached_weight of
   1.528 +                  SOME w => w
   1.529 +                | NONE => fact_weight fudge stature const_tab rel_const_tab
   1.530 +                                      chained_const_tab fact_consts
   1.531 +            in
   1.532 +              if weight >= threshold then
   1.533 +                relevant ((ax, weight) :: candidates) rejects hopeful
   1.534 +              else
   1.535 +                relevant candidates ((ax, weight) :: rejects) hopeful
   1.536 +            end
   1.537 +        in
   1.538 +          trace_msg ctxt (fn () =>
   1.539 +              "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
   1.540 +              Real.toString threshold ^ ", constants: " ^
   1.541 +              commas (rel_const_tab |> Symtab.dest
   1.542 +                      |> filter (curry (op <>) [] o snd)
   1.543 +                      |> map string_for_hyper_pconst));
   1.544 +          relevant [] [] hopeful
   1.545 +        end
   1.546 +    fun prepend_facts ths accepts =
   1.547 +      ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
   1.548 +       (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
   1.549 +      |> take max_relevant
   1.550 +    fun uses_const s t =
   1.551 +      fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
   1.552 +                  false
   1.553 +    fun uses_const_anywhere accepts s =
   1.554 +      exists (uses_const s o prop_of o snd) accepts orelse
   1.555 +      exists (uses_const s) (concl_t :: hyp_ts)
   1.556 +    fun add_set_const_thms accepts =
   1.557 +      exists (uses_const_anywhere accepts) set_consts ? append set_thms
   1.558 +    fun insert_into_facts accepts [] = accepts
   1.559 +      | insert_into_facts accepts ths =
   1.560 +        let
   1.561 +          val add = facts |> filter (member Thm.eq_thm_prop ths o snd)
   1.562 +          val (bef, after) =
   1.563 +            accepts |> filter_out (member Thm.eq_thm_prop ths o snd)
   1.564 +                    |> take (max_relevant - length add)
   1.565 +                    |> chop special_fact_index
   1.566 +        in bef @ add @ after end
   1.567 +    fun insert_special_facts accepts =
   1.568 +       (* FIXME: get rid of "ext" here once it is treated as a helper *)
   1.569 +       [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
   1.570 +          |> add_set_const_thms accepts
   1.571 +          |> insert_into_facts accepts
   1.572 +  in
   1.573 +    facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
   1.574 +          |> iter 0 max_relevant threshold0 goal_const_tab []
   1.575 +          |> not (null add_ths) ? prepend_facts add_ths
   1.576 +          |> insert_special_facts
   1.577 +          |> tap (fn accepts => trace_msg ctxt (fn () =>
   1.578 +                      "Total relevant: " ^ string_of_int (length accepts)))
   1.579 +  end
   1.580 +
   1.581 +fun iterative_relevant_facts ctxt (threshold0, threshold1) max_relevant
   1.582 +                             is_built_in_const fudge (override as {only, ...})
   1.583 +                             chained_ths hyp_ts concl_t facts =
   1.584 +  let
   1.585 +    val thy = Proof_Context.theory_of ctxt
   1.586 +    val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
   1.587 +                          1.0 / Real.fromInt (max_relevant + 1))
   1.588 +  in
   1.589 +    trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
   1.590 +                             " facts");
   1.591 +    (if only orelse threshold1 < 0.0 then
   1.592 +       facts
   1.593 +     else if threshold0 > 1.0 orelse threshold0 > threshold1 orelse
   1.594 +             max_relevant = 0 then
   1.595 +       []
   1.596 +     else
   1.597 +       relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
   1.598 +           fudge override facts (chained_ths |> map prop_of) hyp_ts
   1.599 +           (concl_t |> theory_constify fudge (Context.theory_name thy)))
   1.600 +    |> map (apfst (apfst (fn f => f ())))
   1.601 +  end
   1.602 +
   1.603 +end;