1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Jul 11 21:43:19 2012 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Jul 11 21:43:19 2012 +0200
1.3 @@ -2,50 +2,17 @@
1.4 Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
1.5 Author: Jasmin Blanchette, TU Muenchen
1.6
1.7 -Sledgehammer's relevance filter.
1.8 +Sledgehammer's hybrid relevance filter.
1.9 *)
1.10
1.11 signature SLEDGEHAMMER_FILTER =
1.12 sig
1.13 type status = ATP_Problem_Generate.status
1.14 type stature = ATP_Problem_Generate.stature
1.15 + type relevance_fudge = Sledgehammer_Filter_Iter.relevance_fudge
1.16 + type relevance_override = Sledgehammer_Filter_Iter.relevance_override
1.17
1.18 - type relevance_fudge =
1.19 - {local_const_multiplier : real,
1.20 - worse_irrel_freq : real,
1.21 - higher_order_irrel_weight : real,
1.22 - abs_rel_weight : real,
1.23 - abs_irrel_weight : real,
1.24 - skolem_irrel_weight : real,
1.25 - theory_const_rel_weight : real,
1.26 - theory_const_irrel_weight : real,
1.27 - chained_const_irrel_weight : real,
1.28 - intro_bonus : real,
1.29 - elim_bonus : real,
1.30 - simp_bonus : real,
1.31 - local_bonus : real,
1.32 - assum_bonus : real,
1.33 - chained_bonus : real,
1.34 - max_imperfect : real,
1.35 - max_imperfect_exp : real,
1.36 - threshold_divisor : real,
1.37 - ridiculous_threshold : real}
1.38 -
1.39 - type relevance_override =
1.40 - {add : (Facts.ref * Attrib.src list) list,
1.41 - del : (Facts.ref * Attrib.src list) list,
1.42 - only : bool}
1.43 -
1.44 - val trace : bool Config.T
1.45 - val ignore_no_atp : bool Config.T
1.46 - val instantiate_inducts : bool Config.T
1.47 - val pseudo_abs_name : string
1.48 - val pseudo_skolem_prefix : string
1.49 val no_relevance_override : relevance_override
1.50 - val const_names_in_fact :
1.51 - theory -> (string * typ -> term list -> bool * term list) -> term
1.52 - -> string list
1.53 - val clasimpset_rule_table_of : Proof.context -> status Termtab.table
1.54 val fact_from_ref :
1.55 Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
1.56 -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
1.57 @@ -53,6 +20,7 @@
1.58 Proof.context -> bool -> 'a Symtab.table -> bool -> thm list
1.59 -> thm list -> status Termtab.table
1.60 -> (((unit -> string) * stature) * thm) list
1.61 + val clasimpset_rule_table_of : Proof.context -> status Termtab.table
1.62 val maybe_instantiate_inducts :
1.63 Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
1.64 -> (((unit -> string) * 'a) * thm) list
1.65 @@ -74,104 +42,12 @@
1.66 open ATP_Problem_Generate
1.67 open Metis_Tactic
1.68 open Sledgehammer_Util
1.69 +open Sledgehammer_Filter_Iter
1.70
1.71 -val trace =
1.72 - Attrib.setup_config_bool @{binding sledgehammer_filter_trace} (K false)
1.73 -fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
1.74 -
1.75 -(* experimental features *)
1.76 -val ignore_no_atp =
1.77 - Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
1.78 -val instantiate_inducts =
1.79 - Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
1.80 -
1.81 -type relevance_fudge =
1.82 - {local_const_multiplier : real,
1.83 - worse_irrel_freq : real,
1.84 - higher_order_irrel_weight : real,
1.85 - abs_rel_weight : real,
1.86 - abs_irrel_weight : real,
1.87 - skolem_irrel_weight : real,
1.88 - theory_const_rel_weight : real,
1.89 - theory_const_irrel_weight : real,
1.90 - chained_const_irrel_weight : real,
1.91 - intro_bonus : real,
1.92 - elim_bonus : real,
1.93 - simp_bonus : real,
1.94 - local_bonus : real,
1.95 - assum_bonus : real,
1.96 - chained_bonus : real,
1.97 - max_imperfect : real,
1.98 - max_imperfect_exp : real,
1.99 - threshold_divisor : real,
1.100 - ridiculous_threshold : real}
1.101 -
1.102 -type relevance_override =
1.103 - {add : (Facts.ref * Attrib.src list) list,
1.104 - del : (Facts.ref * Attrib.src list) list,
1.105 - only : bool}
1.106 +val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
1.107
1.108 val no_relevance_override = {add = [], del = [], only = false}
1.109
1.110 -val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
1.111 -val pseudo_abs_name = sledgehammer_prefix ^ "abs"
1.112 -val pseudo_skolem_prefix = sledgehammer_prefix ^ "sko"
1.113 -val theory_const_suffix = Long_Name.separator ^ " 1"
1.114 -
1.115 -(* unfolding these can yield really huge terms *)
1.116 -val risky_defs = @{thms Bit0_def Bit1_def}
1.117 -
1.118 -fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
1.119 -fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
1.120 - | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
1.121 - | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
1.122 - | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
1.123 - | is_rec_def _ = false
1.124 -
1.125 -fun clasimpset_rule_table_of ctxt =
1.126 - let
1.127 - val thy = Proof_Context.theory_of ctxt
1.128 - val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
1.129 - fun add stature normalizers get_th =
1.130 - fold (fn rule =>
1.131 - let
1.132 - val th = rule |> get_th
1.133 - val t =
1.134 - th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of
1.135 - in
1.136 - fold (fn normalize => Termtab.update (normalize t, stature))
1.137 - (I :: normalizers)
1.138 - end)
1.139 - val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
1.140 - ctxt |> claset_of |> Classical.rep_cs
1.141 - val intros = Item_Net.content safeIs @ Item_Net.content hazIs
1.142 -(* Add once it is used:
1.143 - val elims =
1.144 - Item_Net.content safeEs @ Item_Net.content hazEs
1.145 - |> map Classical.classical_rule
1.146 -*)
1.147 - val simps = ctxt |> simpset_of |> dest_ss |> #simps
1.148 - val specs = ctxt |> Spec_Rules.get
1.149 - val (rec_defs, nonrec_defs) =
1.150 - specs |> filter (curry (op =) Spec_Rules.Equational o fst)
1.151 - |> maps (snd o snd)
1.152 - |> filter_out (member Thm.eq_thm_prop risky_defs)
1.153 - |> List.partition (is_rec_def o prop_of)
1.154 - val spec_intros =
1.155 - specs |> filter (member (op =) [Spec_Rules.Inductive,
1.156 - Spec_Rules.Co_Inductive] o fst)
1.157 - |> maps (snd o snd)
1.158 - in
1.159 - Termtab.empty |> add Simp [atomize] snd simps
1.160 - |> add Simp [] I rec_defs
1.161 - |> add Def [] I nonrec_defs
1.162 -(* Add once it is used:
1.163 - |> add Elim [] I elims
1.164 -*)
1.165 - |> add Intro [] I intros
1.166 - |> add Inductive [] I spec_intros
1.167 - end
1.168 -
1.169 fun needs_quoting reserved s =
1.170 Symtab.defined reserved s orelse
1.171 exists (not o Lexicon.is_identifier) (Long_Name.explode s)
1.172 @@ -187,6 +63,16 @@
1.173 val backquote =
1.174 raw_explode #> map (fn "`" => "\\`" | s => s) #> implode #> enclose "`" "`"
1.175
1.176 +(* unfolding these can yield really huge terms *)
1.177 +val risky_defs = @{thms Bit0_def Bit1_def}
1.178 +
1.179 +fun is_rec_eq lhs = Term.exists_subterm (curry (op =) (head_of lhs))
1.180 +fun is_rec_def (@{const Trueprop} $ t) = is_rec_def t
1.181 + | is_rec_def (@{const ==>} $ _ $ t2) = is_rec_def t2
1.182 + | is_rec_def (Const (@{const_name "=="}, _) $ t1 $ t2) = is_rec_eq t1 t2
1.183 + | is_rec_def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) = is_rec_eq t1 t2
1.184 + | is_rec_def _ = false
1.185 +
1.186 fun is_assum assms th = exists (fn ct => prop_of th aconv term_of ct) assms
1.187 fun is_chained chained_ths = member Thm.eq_thm_prop chained_ths
1.188
1.189 @@ -240,571 +126,6 @@
1.190 |> snd
1.191 end
1.192
1.193 -(* This is a terrible hack. Free variables are sometimes coded as "M__" when
1.194 - they are displayed as "M" and we want to avoid clashes with these. But
1.195 - sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
1.196 - prefixes of all free variables. In the worse case scenario, where the fact
1.197 - won't be resolved correctly, the user can fix it manually, e.g., by naming
1.198 - the fact in question. Ideally we would need nothing of it, but backticks
1.199 - simply don't work with schematic variables. *)
1.200 -fun all_prefixes_of s =
1.201 - map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
1.202 -fun close_form t =
1.203 - (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
1.204 - |> fold (fn ((s, i), T) => fn (t', taken) =>
1.205 - let val s' = singleton (Name.variant_list taken) s in
1.206 - ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
1.207 - else Logic.all_const) T
1.208 - $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
1.209 - s' :: taken)
1.210 - end)
1.211 - (Term.add_vars t [] |> sort_wrt (fst o fst))
1.212 - |> fst
1.213 -
1.214 -fun string_for_term ctxt t =
1.215 - Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
1.216 - (print_mode_value ())) (Syntax.string_of_term ctxt) t
1.217 - |> String.translate (fn c => if Char.isPrint c then str c else "")
1.218 - |> simplify_spaces
1.219 -
1.220 -(** Structural induction rules **)
1.221 -
1.222 -fun struct_induct_rule_on th =
1.223 - case Logic.strip_horn (prop_of th) of
1.224 - (prems, @{const Trueprop}
1.225 - $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
1.226 - if not (is_TVar ind_T) andalso length prems > 1 andalso
1.227 - exists (exists_subterm (curry (op aconv) p)) prems andalso
1.228 - not (exists (exists_subterm (curry (op aconv) a)) prems) then
1.229 - SOME (p_name, ind_T)
1.230 - else
1.231 - NONE
1.232 - | _ => NONE
1.233 -
1.234 -fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
1.235 - let
1.236 - fun varify_noninducts (t as Free (s, T)) =
1.237 - if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
1.238 - | varify_noninducts t = t
1.239 - val p_inst =
1.240 - concl_prop |> map_aterms varify_noninducts |> close_form
1.241 - |> lambda (Free ind_x)
1.242 - |> string_for_term ctxt
1.243 - in
1.244 - ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
1.245 - stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
1.246 - end
1.247 -
1.248 -fun type_match thy (T1, T2) =
1.249 - (Sign.typ_match thy (T2, T1) Vartab.empty; true)
1.250 - handle Type.TYPE_MATCH => false
1.251 -
1.252 -fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
1.253 - case struct_induct_rule_on th of
1.254 - SOME (p_name, ind_T) =>
1.255 - let val thy = Proof_Context.theory_of ctxt in
1.256 - stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
1.257 - |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
1.258 - end
1.259 - | NONE => [ax]
1.260 -
1.261 -(***************************************************************)
1.262 -(* Relevance Filtering *)
1.263 -(***************************************************************)
1.264 -
1.265 -(*** constants with types ***)
1.266 -
1.267 -fun order_of_type (Type (@{type_name fun}, [T1, T2])) =
1.268 - Int.max (order_of_type T1 + 1, order_of_type T2)
1.269 - | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0
1.270 - | order_of_type _ = 0
1.271 -
1.272 -(* An abstraction of Isabelle types and first-order terms *)
1.273 -datatype pattern = PVar | PApp of string * pattern list
1.274 -datatype ptype = PType of int * pattern list
1.275 -
1.276 -fun string_for_pattern PVar = "_"
1.277 - | string_for_pattern (PApp (s, ps)) =
1.278 - if null ps then s else s ^ string_for_patterns ps
1.279 -and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
1.280 -fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
1.281 -
1.282 -(*Is the second type an instance of the first one?*)
1.283 -fun match_pattern (PVar, _) = true
1.284 - | match_pattern (PApp _, PVar) = false
1.285 - | match_pattern (PApp (s, ps), PApp (t, qs)) =
1.286 - s = t andalso match_patterns (ps, qs)
1.287 -and match_patterns (_, []) = true
1.288 - | match_patterns ([], _) = false
1.289 - | match_patterns (p :: ps, q :: qs) =
1.290 - match_pattern (p, q) andalso match_patterns (ps, qs)
1.291 -fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs)
1.292 -
1.293 -(* Is there a unifiable constant? *)
1.294 -fun pconst_mem f consts (s, ps) =
1.295 - exists (curry (match_ptype o f) ps)
1.296 - (map snd (filter (curry (op =) s o fst) consts))
1.297 -fun pconst_hyper_mem f const_tab (s, ps) =
1.298 - exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s))
1.299 -
1.300 -fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts)
1.301 - | pattern_for_type (TFree (s, _)) = PApp (s, [])
1.302 - | pattern_for_type (TVar _) = PVar
1.303 -
1.304 -(* Pairs a constant with the list of its type instantiations. *)
1.305 -fun ptype thy const x =
1.306 - (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
1.307 - else [])
1.308 -fun rich_ptype thy const (s, T) =
1.309 - PType (order_of_type T, ptype thy const (s, T))
1.310 -fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T))
1.311 -
1.312 -fun string_for_hyper_pconst (s, ps) =
1.313 - s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
1.314 -
1.315 -(* Add a pconstant to the table, but a [] entry means a standard
1.316 - connective, which we ignore.*)
1.317 -fun add_pconst_to_table also_skolem (s, p) =
1.318 - if (not also_skolem andalso String.isPrefix pseudo_skolem_prefix s) then I
1.319 - else Symtab.map_default (s, [p]) (insert (op =) p)
1.320 -
1.321 -(* Set constants tend to pull in too many irrelevant facts. We limit the damage
1.322 - by treating them more or less as if they were built-in but add their
1.323 - axiomatization at the end. *)
1.324 -val set_consts = [@{const_name Collect}, @{const_name Set.member}]
1.325 -val set_thms = @{thms Collect_mem_eq mem_Collect_eq Collect_cong}
1.326 -
1.327 -fun add_pconsts_in_term thy is_built_in_const also_skolems pos =
1.328 - let
1.329 - val flip = Option.map not
1.330 - (* We include free variables, as well as constants, to handle locales. For
1.331 - each quantifiers that must necessarily be skolemized by the automatic
1.332 - prover, we introduce a fresh constant to simulate the effect of
1.333 - Skolemization. *)
1.334 - fun do_const const ext_arg (x as (s, _)) ts =
1.335 - let val (built_in, ts) = is_built_in_const x ts in
1.336 - if member (op =) set_consts s then
1.337 - fold (do_term ext_arg) ts
1.338 - else
1.339 - (not built_in
1.340 - ? add_pconst_to_table also_skolems (rich_pconst thy const x))
1.341 - #> fold (do_term false) ts
1.342 - end
1.343 - and do_term ext_arg t =
1.344 - case strip_comb t of
1.345 - (Const x, ts) => do_const true ext_arg x ts
1.346 - | (Free x, ts) => do_const false ext_arg x ts
1.347 - | (Abs (_, T, t'), ts) =>
1.348 - ((null ts andalso not ext_arg)
1.349 - (* Since lambdas on the right-hand side of equalities are usually
1.350 - extensionalized later by "abs_extensionalize_term", we don't
1.351 - penalize them here. *)
1.352 - ? add_pconst_to_table true (pseudo_abs_name,
1.353 - PType (order_of_type T + 1, [])))
1.354 - #> fold (do_term false) (t' :: ts)
1.355 - | (_, ts) => fold (do_term false) ts
1.356 - fun do_quantifier will_surely_be_skolemized abs_T body_t =
1.357 - do_formula pos body_t
1.358 - #> (if also_skolems andalso will_surely_be_skolemized then
1.359 - add_pconst_to_table true (pseudo_skolem_prefix ^ serial_string (),
1.360 - PType (order_of_type abs_T, []))
1.361 - else
1.362 - I)
1.363 - and do_term_or_formula ext_arg T =
1.364 - if T = HOLogic.boolT then do_formula NONE else do_term ext_arg
1.365 - and do_formula pos t =
1.366 - case t of
1.367 - Const (@{const_name all}, _) $ Abs (_, T, t') =>
1.368 - do_quantifier (pos = SOME false) T t'
1.369 - | @{const "==>"} $ t1 $ t2 =>
1.370 - do_formula (flip pos) t1 #> do_formula pos t2
1.371 - | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
1.372 - do_term_or_formula false T t1 #> do_term_or_formula true T t2
1.373 - | @{const Trueprop} $ t1 => do_formula pos t1
1.374 - | @{const False} => I
1.375 - | @{const True} => I
1.376 - | @{const Not} $ t1 => do_formula (flip pos) t1
1.377 - | Const (@{const_name All}, _) $ Abs (_, T, t') =>
1.378 - do_quantifier (pos = SOME false) T t'
1.379 - | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
1.380 - do_quantifier (pos = SOME true) T t'
1.381 - | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
1.382 - | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
1.383 - | @{const HOL.implies} $ t1 $ t2 =>
1.384 - do_formula (flip pos) t1 #> do_formula pos t2
1.385 - | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
1.386 - do_term_or_formula false T t1 #> do_term_or_formula true T t2
1.387 - | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
1.388 - $ t1 $ t2 $ t3 =>
1.389 - do_formula NONE t1 #> fold (do_term_or_formula false T) [t2, t3]
1.390 - | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
1.391 - do_quantifier (is_some pos) T t'
1.392 - | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
1.393 - do_quantifier (pos = SOME false) T
1.394 - (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
1.395 - | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
1.396 - do_quantifier (pos = SOME true) T
1.397 - (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
1.398 - | (t0 as Const (_, @{typ bool})) $ t1 =>
1.399 - do_term false t0 #> do_formula pos t1 (* theory constant *)
1.400 - | _ => do_term false t
1.401 - in do_formula pos end
1.402 -
1.403 -fun pconsts_in_fact thy is_built_in_const t =
1.404 - Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
1.405 - (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true
1.406 - (SOME true) t) []
1.407 -
1.408 -val const_names_in_fact = map fst ooo pconsts_in_fact
1.409 -
1.410 -(* Inserts a dummy "constant" referring to the theory name, so that relevance
1.411 - takes the given theory into account. *)
1.412 -fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...}
1.413 - : relevance_fudge) thy_name t =
1.414 - if exists (curry (op <) 0.0) [theory_const_rel_weight,
1.415 - theory_const_irrel_weight] then
1.416 - Const (thy_name ^ theory_const_suffix, @{typ bool}) $ t
1.417 - else
1.418 - t
1.419 -
1.420 -fun theory_const_prop_of fudge th =
1.421 - theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
1.422 -
1.423 -fun pair_consts_fact thy is_built_in_const fudge fact =
1.424 - case fact |> snd |> theory_const_prop_of fudge
1.425 - |> pconsts_in_fact thy is_built_in_const of
1.426 - [] => NONE
1.427 - | consts => SOME ((fact, consts), NONE)
1.428 -
1.429 -
1.430 -(**** Constant / Type Frequencies ****)
1.431 -
1.432 -(* A two-dimensional symbol table counts frequencies of constants. It's keyed
1.433 - first by constant name and second by its list of type instantiations. For the
1.434 - latter, we need a linear ordering on "pattern list". *)
1.435 -
1.436 -fun pattern_ord p =
1.437 - case p of
1.438 - (PVar, PVar) => EQUAL
1.439 - | (PVar, PApp _) => LESS
1.440 - | (PApp _, PVar) => GREATER
1.441 - | (PApp q1, PApp q2) =>
1.442 - prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2)
1.443 -fun ptype_ord (PType p, PType q) =
1.444 - prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q)
1.445 -
1.446 -structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
1.447 -
1.448 -fun count_fact_consts thy fudge =
1.449 - let
1.450 - fun do_const const (s, T) ts =
1.451 - (* Two-dimensional table update. Constant maps to types maps to count. *)
1.452 - PType_Tab.map_default (rich_ptype thy const (s, T), 0) (Integer.add 1)
1.453 - |> Symtab.map_default (s, PType_Tab.empty)
1.454 - #> fold do_term ts
1.455 - and do_term t =
1.456 - case strip_comb t of
1.457 - (Const x, ts) => do_const true x ts
1.458 - | (Free x, ts) => do_const false x ts
1.459 - | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
1.460 - | (_, ts) => fold do_term ts
1.461 - in do_term o theory_const_prop_of fudge o snd end
1.462 -
1.463 -
1.464 -(**** Actual Filtering Code ****)
1.465 -
1.466 -fun pow_int _ 0 = 1.0
1.467 - | pow_int x 1 = x
1.468 - | pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x
1.469 -
1.470 -(*The frequency of a constant is the sum of those of all instances of its type.*)
1.471 -fun pconst_freq match const_tab (c, ps) =
1.472 - PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
1.473 - (the (Symtab.lookup const_tab c)) 0
1.474 -
1.475 -
1.476 -(* A surprising number of theorems contain only a few significant constants.
1.477 - These include all induction rules, and other general theorems. *)
1.478 -
1.479 -(* "log" seems best in practice. A constant function of one ignores the constant
1.480 - frequencies. Rare constants give more points if they are relevant than less
1.481 - rare ones. *)
1.482 -fun rel_weight_for _ freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
1.483 -
1.484 -(* Irrelevant constants are treated differently. We associate lower penalties to
1.485 - very rare constants and very common ones -- the former because they can't
1.486 - lead to the inclusion of too many new facts, and the latter because they are
1.487 - so common as to be of little interest. *)
1.488 -fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...}
1.489 - : relevance_fudge) order freq =
1.490 - let val (k, x) = worse_irrel_freq |> `Real.ceil in
1.491 - (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
1.492 - else rel_weight_for order freq / rel_weight_for order k)
1.493 - * pow_int higher_order_irrel_weight (order - 1)
1.494 - end
1.495 -
1.496 -fun multiplier_for_const_name local_const_multiplier s =
1.497 - if String.isSubstring "." s then 1.0 else local_const_multiplier
1.498 -
1.499 -(* Computes a constant's weight, as determined by its frequency. *)
1.500 -fun generic_pconst_weight local_const_multiplier abs_weight skolem_weight
1.501 - theory_const_weight chained_const_weight weight_for f
1.502 - const_tab chained_const_tab (c as (s, PType (m, _))) =
1.503 - if s = pseudo_abs_name then
1.504 - abs_weight
1.505 - else if String.isPrefix pseudo_skolem_prefix s then
1.506 - skolem_weight
1.507 - else if String.isSuffix theory_const_suffix s then
1.508 - theory_const_weight
1.509 - else
1.510 - multiplier_for_const_name local_const_multiplier s
1.511 - * weight_for m (pconst_freq (match_ptype o f) const_tab c)
1.512 - |> (if chained_const_weight < 1.0 andalso
1.513 - pconst_hyper_mem I chained_const_tab c then
1.514 - curry (op *) chained_const_weight
1.515 - else
1.516 - I)
1.517 -
1.518 -fun rel_pconst_weight ({local_const_multiplier, abs_rel_weight,
1.519 - theory_const_rel_weight, ...} : relevance_fudge)
1.520 - const_tab =
1.521 - generic_pconst_weight local_const_multiplier abs_rel_weight 0.0
1.522 - theory_const_rel_weight 0.0 rel_weight_for I const_tab
1.523 - Symtab.empty
1.524 -
1.525 -fun irrel_pconst_weight (fudge as {local_const_multiplier, abs_irrel_weight,
1.526 - skolem_irrel_weight,
1.527 - theory_const_irrel_weight,
1.528 - chained_const_irrel_weight, ...})
1.529 - const_tab chained_const_tab =
1.530 - generic_pconst_weight local_const_multiplier abs_irrel_weight
1.531 - skolem_irrel_weight theory_const_irrel_weight
1.532 - chained_const_irrel_weight (irrel_weight_for fudge) swap
1.533 - const_tab chained_const_tab
1.534 -
1.535 -fun stature_bonus ({intro_bonus, ...} : relevance_fudge) (_, Intro) =
1.536 - intro_bonus
1.537 - | stature_bonus {elim_bonus, ...} (_, Elim) = elim_bonus
1.538 - | stature_bonus {simp_bonus, ...} (_, Simp) = simp_bonus
1.539 - | stature_bonus {local_bonus, ...} (Local, _) = local_bonus
1.540 - | stature_bonus {assum_bonus, ...} (Assum, _) = assum_bonus
1.541 - | stature_bonus {chained_bonus, ...} (Chained, _) = chained_bonus
1.542 - | stature_bonus _ _ = 0.0
1.543 -
1.544 -fun is_odd_const_name s =
1.545 - s = pseudo_abs_name orelse String.isPrefix pseudo_skolem_prefix s orelse
1.546 - String.isSuffix theory_const_suffix s
1.547 -
1.548 -fun fact_weight fudge stature const_tab relevant_consts chained_consts
1.549 - fact_consts =
1.550 - case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
1.551 - ||> filter_out (pconst_hyper_mem swap relevant_consts) of
1.552 - ([], _) => 0.0
1.553 - | (rel, irrel) =>
1.554 - if forall (forall (is_odd_const_name o fst)) [rel, irrel] then
1.555 - 0.0
1.556 - else
1.557 - let
1.558 - val irrel = irrel |> filter_out (pconst_mem swap rel)
1.559 - val rel_weight =
1.560 - 0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
1.561 - val irrel_weight =
1.562 - ~ (stature_bonus fudge stature)
1.563 - |> fold (curry (op +)
1.564 - o irrel_pconst_weight fudge const_tab chained_consts) irrel
1.565 - val res = rel_weight / (rel_weight + irrel_weight)
1.566 - in if Real.isFinite res then res else 0.0 end
1.567 -
1.568 -type annotated_thm =
1.569 - (((unit -> string) * stature) * thm) * (string * ptype) list
1.570 -
1.571 -fun take_most_relevant ctxt max_relevant remaining_max
1.572 - ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
1.573 - (candidates : (annotated_thm * real) list) =
1.574 - let
1.575 - val max_imperfect =
1.576 - Real.ceil (Math.pow (max_imperfect,
1.577 - Math.pow (Real.fromInt remaining_max
1.578 - / Real.fromInt max_relevant, max_imperfect_exp)))
1.579 - val (perfect, imperfect) =
1.580 - candidates |> sort (Real.compare o swap o pairself snd)
1.581 - |> take_prefix (fn (_, w) => w > 0.99999)
1.582 - val ((accepts, more_rejects), rejects) =
1.583 - chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
1.584 - in
1.585 - trace_msg ctxt (fn () =>
1.586 - "Actually passed (" ^ string_of_int (length accepts) ^ " of " ^
1.587 - string_of_int (length candidates) ^ "): " ^
1.588 - (accepts |> map (fn ((((name, _), _), _), weight) =>
1.589 - name () ^ " [" ^ Real.toString weight ^ "]")
1.590 - |> commas));
1.591 - (accepts, more_rejects @ rejects)
1.592 - end
1.593 -
1.594 -fun if_empty_replace_with_scope thy is_built_in_const facts sc tab =
1.595 - if Symtab.is_empty tab then
1.596 - Symtab.empty
1.597 - |> fold (add_pconsts_in_term thy is_built_in_const false (SOME false))
1.598 - (map_filter (fn ((_, (sc', _)), th) =>
1.599 - if sc' = sc then SOME (prop_of th) else NONE) facts)
1.600 - else
1.601 - tab
1.602 -
1.603 -fun consider_arities is_built_in_const th =
1.604 - let
1.605 - fun aux _ _ NONE = NONE
1.606 - | aux t args (SOME tab) =
1.607 - case t of
1.608 - t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 []
1.609 - | Const (x as (s, _)) =>
1.610 - (if is_built_in_const x args |> fst then
1.611 - SOME tab
1.612 - else case Symtab.lookup tab s of
1.613 - NONE => SOME (Symtab.update (s, length args) tab)
1.614 - | SOME n => if n = length args then SOME tab else NONE)
1.615 - | _ => SOME tab
1.616 - in aux (prop_of th) [] end
1.617 -
1.618 -(* FIXME: This is currently only useful for polymorphic type encodings. *)
1.619 -fun could_benefit_from_ext is_built_in_const facts =
1.620 - fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
1.621 - |> is_none
1.622 -
1.623 -(* High enough so that it isn't wrongly considered as very relevant (e.g., for E
1.624 - weights), but low enough so that it is unlikely to be truncated away if few
1.625 - facts are included. *)
1.626 -val special_fact_index = 75
1.627 -
1.628 -fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
1.629 - (fudge as {threshold_divisor, ridiculous_threshold, ...})
1.630 - ({add, del, ...} : relevance_override) facts chained_ts hyp_ts concl_t =
1.631 - let
1.632 - val thy = Proof_Context.theory_of ctxt
1.633 - val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
1.634 - val add_pconsts = add_pconsts_in_term thy is_built_in_const false o SOME
1.635 - val chained_const_tab = Symtab.empty |> fold (add_pconsts true) chained_ts
1.636 - val goal_const_tab =
1.637 - Symtab.empty |> fold (add_pconsts true) hyp_ts
1.638 - |> add_pconsts false concl_t
1.639 - |> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
1.640 - |> fold (if_empty_replace_with_scope thy is_built_in_const facts)
1.641 - [Chained, Assum, Local]
1.642 - val add_ths = Attrib.eval_thms ctxt add
1.643 - val del_ths = Attrib.eval_thms ctxt del
1.644 - val facts = facts |> filter_out (member Thm.eq_thm_prop del_ths o snd)
1.645 - fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
1.646 - let
1.647 - fun relevant [] _ [] =
1.648 - (* Nothing has been added this iteration. *)
1.649 - if j = 0 andalso threshold >= ridiculous_threshold then
1.650 - (* First iteration? Try again. *)
1.651 - iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
1.652 - hopeless hopeful
1.653 - else
1.654 - []
1.655 - | relevant candidates rejects [] =
1.656 - let
1.657 - val (accepts, more_rejects) =
1.658 - take_most_relevant ctxt max_relevant remaining_max fudge
1.659 - candidates
1.660 - val rel_const_tab' =
1.661 - rel_const_tab
1.662 - |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
1.663 - fun is_dirty (c, _) =
1.664 - Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
1.665 - val (hopeful_rejects, hopeless_rejects) =
1.666 - (rejects @ hopeless, ([], []))
1.667 - |-> fold (fn (ax as (_, consts), old_weight) =>
1.668 - if exists is_dirty consts then
1.669 - apfst (cons (ax, NONE))
1.670 - else
1.671 - apsnd (cons (ax, old_weight)))
1.672 - |>> append (more_rejects
1.673 - |> map (fn (ax as (_, consts), old_weight) =>
1.674 - (ax, if exists is_dirty consts then NONE
1.675 - else SOME old_weight)))
1.676 - val threshold =
1.677 - 1.0 - (1.0 - threshold)
1.678 - * Math.pow (decay, Real.fromInt (length accepts))
1.679 - val remaining_max = remaining_max - length accepts
1.680 - in
1.681 - trace_msg ctxt (fn () => "New or updated constants: " ^
1.682 - commas (rel_const_tab' |> Symtab.dest
1.683 - |> subtract (op =) (rel_const_tab |> Symtab.dest)
1.684 - |> map string_for_hyper_pconst));
1.685 - map (fst o fst) accepts @
1.686 - (if remaining_max = 0 then
1.687 - []
1.688 - else
1.689 - iter (j + 1) remaining_max threshold rel_const_tab'
1.690 - hopeless_rejects hopeful_rejects)
1.691 - end
1.692 - | relevant candidates rejects
1.693 - (((ax as (((_, stature), _), fact_consts)), cached_weight)
1.694 - :: hopeful) =
1.695 - let
1.696 - val weight =
1.697 - case cached_weight of
1.698 - SOME w => w
1.699 - | NONE => fact_weight fudge stature const_tab rel_const_tab
1.700 - chained_const_tab fact_consts
1.701 - in
1.702 - if weight >= threshold then
1.703 - relevant ((ax, weight) :: candidates) rejects hopeful
1.704 - else
1.705 - relevant candidates ((ax, weight) :: rejects) hopeful
1.706 - end
1.707 - in
1.708 - trace_msg ctxt (fn () =>
1.709 - "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
1.710 - Real.toString threshold ^ ", constants: " ^
1.711 - commas (rel_const_tab |> Symtab.dest
1.712 - |> filter (curry (op <>) [] o snd)
1.713 - |> map string_for_hyper_pconst));
1.714 - relevant [] [] hopeful
1.715 - end
1.716 - fun prepend_facts ths accepts =
1.717 - ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
1.718 - (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
1.719 - |> take max_relevant
1.720 - fun uses_const s t =
1.721 - fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
1.722 - false
1.723 - fun uses_const_anywhere accepts s =
1.724 - exists (uses_const s o prop_of o snd) accepts orelse
1.725 - exists (uses_const s) (concl_t :: hyp_ts)
1.726 - fun add_set_const_thms accepts =
1.727 - exists (uses_const_anywhere accepts) set_consts ? append set_thms
1.728 - fun insert_into_facts accepts [] = accepts
1.729 - | insert_into_facts accepts ths =
1.730 - let
1.731 - val add = facts |> filter (member Thm.eq_thm_prop ths o snd)
1.732 - val (bef, after) =
1.733 - accepts |> filter_out (member Thm.eq_thm_prop ths o snd)
1.734 - |> take (max_relevant - length add)
1.735 - |> chop special_fact_index
1.736 - in bef @ add @ after end
1.737 - fun insert_special_facts accepts =
1.738 - (* FIXME: get rid of "ext" here once it is treated as a helper *)
1.739 - [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
1.740 - |> add_set_const_thms accepts
1.741 - |> insert_into_facts accepts
1.742 - in
1.743 - facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
1.744 - |> iter 0 max_relevant threshold0 goal_const_tab []
1.745 - |> not (null add_ths) ? prepend_facts add_ths
1.746 - |> insert_special_facts
1.747 - |> tap (fn accepts => trace_msg ctxt (fn () =>
1.748 - "Total relevant: " ^ string_of_int (length accepts)))
1.749 - end
1.750 -
1.751 -
1.752 -(***************************************************************)
1.753 -(* Retrieving and filtering lemmas *)
1.754 -(***************************************************************)
1.755 -
1.756 -(*** retrieve lemmas and filter them ***)
1.757 -
1.758 (*Reject theorems with names like "List.filter.filter_list_def" or
1.759 "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
1.760 fun is_package_def a =
1.761 @@ -813,10 +134,6 @@
1.762 String.isSuffix "_def" a) orelse String.isSuffix "_defs" a
1.763 end
1.764
1.765 -fun uniquify xs =
1.766 - Termtab.fold (cons o snd)
1.767 - (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) []
1.768 -
1.769 (* FIXME: put other record thms here, or declare as "no_atp" *)
1.770 fun multi_base_blacklist ctxt ho_atp =
1.771 ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
1.772 @@ -877,9 +194,6 @@
1.773 andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
1.774 | _ => false) (prop_of th)
1.775
1.776 -(**** Predicates to detect unwanted facts (prolific or likely to cause
1.777 - unsoundness) ****)
1.778 -
1.779 fun is_theorem_bad_for_atps ho_atp exporter thm =
1.780 is_metastrange_theorem thm orelse
1.781 (not exporter andalso
1.782 @@ -889,6 +203,34 @@
1.783 is_that_fact thm
1.784 end)
1.785
1.786 +fun string_for_term ctxt t =
1.787 + Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
1.788 + (print_mode_value ())) (Syntax.string_of_term ctxt) t
1.789 + |> String.translate (fn c => if Char.isPrint c then str c else "")
1.790 + |> simplify_spaces
1.791 +
1.792 +(* This is a terrible hack. Free variables are sometimes coded as "M__" when
1.793 + they are displayed as "M" and we want to avoid clashes with these. But
1.794 + sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
1.795 + prefixes of all free variables. In the worse case scenario, where the fact
1.796 + won't be resolved correctly, the user can fix it manually, e.g., by naming
1.797 + the fact in question. Ideally we would need nothing of it, but backticks
1.798 + simply don't work with schematic variables. *)
1.799 +fun all_prefixes_of s =
1.800 + map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
1.801 +
1.802 +fun close_form t =
1.803 + (t, [] |> Term.add_free_names t |> maps all_prefixes_of)
1.804 + |> fold (fn ((s, i), T) => fn (t', taken) =>
1.805 + let val s' = singleton (Name.variant_list taken) s in
1.806 + ((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
1.807 + else Logic.all_const) T
1.808 + $ Abs (s', T, abstract_over (Var ((s, i), T), t')),
1.809 + s' :: taken)
1.810 + end)
1.811 + (Term.add_vars t [] |> sort_wrt (fst o fst))
1.812 + |> fst
1.813 +
1.814 fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths css_table =
1.815 let
1.816 val thy = Proof_Context.theory_of ctxt
1.817 @@ -960,6 +302,93 @@
1.818 |> op @
1.819 end
1.820
1.821 +fun clasimpset_rule_table_of ctxt =
1.822 + let
1.823 + val thy = Proof_Context.theory_of ctxt
1.824 + val atomize = HOLogic.mk_Trueprop o Object_Logic.atomize_term thy
1.825 + fun add stature normalizers get_th =
1.826 + fold (fn rule =>
1.827 + let
1.828 + val th = rule |> get_th
1.829 + val t =
1.830 + th |> Thm.maxidx_of th > 0 ? zero_var_indexes |> prop_of
1.831 + in
1.832 + fold (fn normalize => Termtab.update (normalize t, stature))
1.833 + (I :: normalizers)
1.834 + end)
1.835 + val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} =
1.836 + ctxt |> claset_of |> Classical.rep_cs
1.837 + val intros = Item_Net.content safeIs @ Item_Net.content hazIs
1.838 +(* Add once it is used:
1.839 + val elims =
1.840 + Item_Net.content safeEs @ Item_Net.content hazEs
1.841 + |> map Classical.classical_rule
1.842 +*)
1.843 + val simps = ctxt |> simpset_of |> dest_ss |> #simps
1.844 + val specs = ctxt |> Spec_Rules.get
1.845 + val (rec_defs, nonrec_defs) =
1.846 + specs |> filter (curry (op =) Spec_Rules.Equational o fst)
1.847 + |> maps (snd o snd)
1.848 + |> filter_out (member Thm.eq_thm_prop risky_defs)
1.849 + |> List.partition (is_rec_def o prop_of)
1.850 + val spec_intros =
1.851 + specs |> filter (member (op =) [Spec_Rules.Inductive,
1.852 + Spec_Rules.Co_Inductive] o fst)
1.853 + |> maps (snd o snd)
1.854 + in
1.855 + Termtab.empty |> add Simp [atomize] snd simps
1.856 + |> add Simp [] I rec_defs
1.857 + |> add Def [] I nonrec_defs
1.858 +(* Add once it is used:
1.859 + |> add Elim [] I elims
1.860 +*)
1.861 + |> add Intro [] I intros
1.862 + |> add Inductive [] I spec_intros
1.863 + end
1.864 +
1.865 +fun uniquify xs =
1.866 + Termtab.fold (cons o snd)
1.867 + (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) []
1.868 +
1.869 +fun struct_induct_rule_on th =
1.870 + case Logic.strip_horn (prop_of th) of
1.871 + (prems, @{const Trueprop}
1.872 + $ ((p as Var ((p_name, 0), _)) $ (a as Var (_, ind_T)))) =>
1.873 + if not (is_TVar ind_T) andalso length prems > 1 andalso
1.874 + exists (exists_subterm (curry (op aconv) p)) prems andalso
1.875 + not (exists (exists_subterm (curry (op aconv) a)) prems) then
1.876 + SOME (p_name, ind_T)
1.877 + else
1.878 + NONE
1.879 + | _ => NONE
1.880 +
1.881 +fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x =
1.882 + let
1.883 + fun varify_noninducts (t as Free (s, T)) =
1.884 + if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T)
1.885 + | varify_noninducts t = t
1.886 + val p_inst =
1.887 + concl_prop |> map_aterms varify_noninducts |> close_form
1.888 + |> lambda (Free ind_x)
1.889 + |> string_for_term ctxt
1.890 + in
1.891 + ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]",
1.892 + stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)])
1.893 + end
1.894 +
1.895 +fun type_match thy (T1, T2) =
1.896 + (Sign.typ_match thy (T2, T1) Vartab.empty; true)
1.897 + handle Type.TYPE_MATCH => false
1.898 +
1.899 +fun instantiate_if_induct_rule ctxt stmt stmt_xs (ax as (_, th)) =
1.900 + case struct_induct_rule_on th of
1.901 + SOME (p_name, ind_T) =>
1.902 + let val thy = Proof_Context.theory_of ctxt in
1.903 + stmt_xs |> filter (fn (_, T) => type_match thy (T, ind_T))
1.904 + |> map_filter (try (instantiate_induct_rule ctxt stmt p_name ax))
1.905 + end
1.906 + | NONE => [ax]
1.907 +
1.908 fun external_frees t =
1.909 [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
1.910
1.911 @@ -998,26 +427,6 @@
1.912 |> uniquify
1.913 end
1.914
1.915 -fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_built_in_const
1.916 - fudge (override as {only, ...}) chained_ths hyp_ts concl_t
1.917 - facts =
1.918 - let
1.919 - val thy = Proof_Context.theory_of ctxt
1.920 - val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
1.921 - 1.0 / Real.fromInt (max_relevant + 1))
1.922 - in
1.923 - trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
1.924 - " facts");
1.925 - (if only orelse threshold1 < 0.0 then
1.926 - facts
1.927 - else if threshold0 > 1.0 orelse threshold0 > threshold1 orelse
1.928 - max_relevant = 0 then
1.929 - []
1.930 - else
1.931 - relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
1.932 - fudge override facts (chained_ths |> map prop_of) hyp_ts
1.933 - (concl_t |> theory_constify fudge (Context.theory_name thy)))
1.934 - |> map (apfst (apfst (fn f => f ())))
1.935 - end
1.936 +val relevant_facts = iterative_relevant_facts
1.937
1.938 end;
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML Wed Jul 11 21:43:19 2012 +0200
2.3 @@ -0,0 +1,600 @@
2.4 +(* Title: HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML
2.5 + Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
2.6 + Author: Jasmin Blanchette, TU Muenchen
2.7 +
2.8 +Sledgehammer's iterative relevance filter.
2.9 +*)
2.10 +
2.11 +signature SLEDGEHAMMER_FILTER_ITER =
2.12 +sig
2.13 + type stature = ATP_Problem_Generate.stature
2.14 +
2.15 + type relevance_fudge =
2.16 + {local_const_multiplier : real,
2.17 + worse_irrel_freq : real,
2.18 + higher_order_irrel_weight : real,
2.19 + abs_rel_weight : real,
2.20 + abs_irrel_weight : real,
2.21 + skolem_irrel_weight : real,
2.22 + theory_const_rel_weight : real,
2.23 + theory_const_irrel_weight : real,
2.24 + chained_const_irrel_weight : real,
2.25 + intro_bonus : real,
2.26 + elim_bonus : real,
2.27 + simp_bonus : real,
2.28 + local_bonus : real,
2.29 + assum_bonus : real,
2.30 + chained_bonus : real,
2.31 + max_imperfect : real,
2.32 + max_imperfect_exp : real,
2.33 + threshold_divisor : real,
2.34 + ridiculous_threshold : real}
2.35 +
2.36 + type relevance_override =
2.37 + {add : (Facts.ref * Attrib.src list) list,
2.38 + del : (Facts.ref * Attrib.src list) list,
2.39 + only : bool}
2.40 +
2.41 + val trace : bool Config.T
2.42 + val ignore_no_atp : bool Config.T
2.43 + val instantiate_inducts : bool Config.T
2.44 + val pseudo_abs_name : string
2.45 + val pseudo_skolem_prefix : string
2.46 + val const_names_in_fact :
2.47 + theory -> (string * typ -> term list -> bool * term list) -> term
2.48 + -> string list
2.49 + val iterative_relevant_facts :
2.50 + Proof.context -> real * real -> int
2.51 + -> (string * typ -> term list -> bool * term list) -> relevance_fudge
2.52 + -> relevance_override -> thm list -> term list -> term
2.53 + -> (((unit -> string) * stature) * thm) list
2.54 + -> ((string * stature) * thm) list
2.55 +end;
2.56 +
2.57 +structure Sledgehammer_Filter_Iter : SLEDGEHAMMER_FILTER_ITER =
2.58 +struct
2.59 +
2.60 +open ATP_Problem_Generate
2.61 +
2.62 +val trace =
2.63 + Attrib.setup_config_bool @{binding sledgehammer_filter_trace} (K false)
2.64 +fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
2.65 +
2.66 +(* experimental features *)
2.67 +val ignore_no_atp =
2.68 + Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
2.69 +val instantiate_inducts =
2.70 + Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
2.71 +
2.72 +type relevance_fudge =
2.73 + {local_const_multiplier : real,
2.74 + worse_irrel_freq : real,
2.75 + higher_order_irrel_weight : real,
2.76 + abs_rel_weight : real,
2.77 + abs_irrel_weight : real,
2.78 + skolem_irrel_weight : real,
2.79 + theory_const_rel_weight : real,
2.80 + theory_const_irrel_weight : real,
2.81 + chained_const_irrel_weight : real,
2.82 + intro_bonus : real,
2.83 + elim_bonus : real,
2.84 + simp_bonus : real,
2.85 + local_bonus : real,
2.86 + assum_bonus : real,
2.87 + chained_bonus : real,
2.88 + max_imperfect : real,
2.89 + max_imperfect_exp : real,
2.90 + threshold_divisor : real,
2.91 + ridiculous_threshold : real}
2.92 +
2.93 +type relevance_override =
2.94 + {add : (Facts.ref * Attrib.src list) list,
2.95 + del : (Facts.ref * Attrib.src list) list,
2.96 + only : bool}
2.97 +
2.98 +val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
2.99 +val pseudo_abs_name = sledgehammer_prefix ^ "abs"
2.100 +val pseudo_skolem_prefix = sledgehammer_prefix ^ "sko"
2.101 +val theory_const_suffix = Long_Name.separator ^ " 1"
2.102 +
2.103 +fun order_of_type (Type (@{type_name fun}, [T1, T2])) =
2.104 + Int.max (order_of_type T1 + 1, order_of_type T2)
2.105 + | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0
2.106 + | order_of_type _ = 0
2.107 +
2.108 +(* An abstraction of Isabelle types and first-order terms *)
2.109 +datatype pattern = PVar | PApp of string * pattern list
2.110 +datatype ptype = PType of int * pattern list
2.111 +
2.112 +fun string_for_pattern PVar = "_"
2.113 + | string_for_pattern (PApp (s, ps)) =
2.114 + if null ps then s else s ^ string_for_patterns ps
2.115 +and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
2.116 +fun string_for_ptype (PType (_, ps)) = string_for_patterns ps
2.117 +
2.118 +(*Is the second type an instance of the first one?*)
2.119 +fun match_pattern (PVar, _) = true
2.120 + | match_pattern (PApp _, PVar) = false
2.121 + | match_pattern (PApp (s, ps), PApp (t, qs)) =
2.122 + s = t andalso match_patterns (ps, qs)
2.123 +and match_patterns (_, []) = true
2.124 + | match_patterns ([], _) = false
2.125 + | match_patterns (p :: ps, q :: qs) =
2.126 + match_pattern (p, q) andalso match_patterns (ps, qs)
2.127 +fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs)
2.128 +
2.129 +(* Is there a unifiable constant? *)
2.130 +fun pconst_mem f consts (s, ps) =
2.131 + exists (curry (match_ptype o f) ps)
2.132 + (map snd (filter (curry (op =) s o fst) consts))
2.133 +fun pconst_hyper_mem f const_tab (s, ps) =
2.134 + exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s))
2.135 +
2.136 +fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts)
2.137 + | pattern_for_type (TFree (s, _)) = PApp (s, [])
2.138 + | pattern_for_type (TVar _) = PVar
2.139 +
2.140 +(* Pairs a constant with the list of its type instantiations. *)
2.141 +fun ptype thy const x =
2.142 + (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x))
2.143 + else [])
2.144 +fun rich_ptype thy const (s, T) =
2.145 + PType (order_of_type T, ptype thy const (s, T))
2.146 +fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T))
2.147 +
2.148 +fun string_for_hyper_pconst (s, ps) =
2.149 + s ^ "{" ^ commas (map string_for_ptype ps) ^ "}"
2.150 +
2.151 +(* Add a pconstant to the table, but a [] entry means a standard
2.152 + connective, which we ignore.*)
2.153 +fun add_pconst_to_table also_skolem (s, p) =
2.154 + if (not also_skolem andalso String.isPrefix pseudo_skolem_prefix s) then I
2.155 + else Symtab.map_default (s, [p]) (insert (op =) p)
2.156 +
2.157 +(* Set constants tend to pull in too many irrelevant facts. We limit the damage
2.158 + by treating them more or less as if they were built-in but add their
2.159 + axiomatization at the end. *)
2.160 +val set_consts = [@{const_name Collect}, @{const_name Set.member}]
2.161 +val set_thms = @{thms Collect_mem_eq mem_Collect_eq Collect_cong}
2.162 +
2.163 +fun add_pconsts_in_term thy is_built_in_const also_skolems pos =
2.164 + let
2.165 + val flip = Option.map not
2.166 + (* We include free variables, as well as constants, to handle locales. For
2.167 + each quantifiers that must necessarily be skolemized by the automatic
2.168 + prover, we introduce a fresh constant to simulate the effect of
2.169 + Skolemization. *)
2.170 + fun do_const const ext_arg (x as (s, _)) ts =
2.171 + let val (built_in, ts) = is_built_in_const x ts in
2.172 + if member (op =) set_consts s then
2.173 + fold (do_term ext_arg) ts
2.174 + else
2.175 + (not built_in
2.176 + ? add_pconst_to_table also_skolems (rich_pconst thy const x))
2.177 + #> fold (do_term false) ts
2.178 + end
2.179 + and do_term ext_arg t =
2.180 + case strip_comb t of
2.181 + (Const x, ts) => do_const true ext_arg x ts
2.182 + | (Free x, ts) => do_const false ext_arg x ts
2.183 + | (Abs (_, T, t'), ts) =>
2.184 + ((null ts andalso not ext_arg)
2.185 + (* Since lambdas on the right-hand side of equalities are usually
2.186 + extensionalized later by "abs_extensionalize_term", we don't
2.187 + penalize them here. *)
2.188 + ? add_pconst_to_table true (pseudo_abs_name,
2.189 + PType (order_of_type T + 1, [])))
2.190 + #> fold (do_term false) (t' :: ts)
2.191 + | (_, ts) => fold (do_term false) ts
2.192 + fun do_quantifier will_surely_be_skolemized abs_T body_t =
2.193 + do_formula pos body_t
2.194 + #> (if also_skolems andalso will_surely_be_skolemized then
2.195 + add_pconst_to_table true (pseudo_skolem_prefix ^ serial_string (),
2.196 + PType (order_of_type abs_T, []))
2.197 + else
2.198 + I)
2.199 + and do_term_or_formula ext_arg T =
2.200 + if T = HOLogic.boolT then do_formula NONE else do_term ext_arg
2.201 + and do_formula pos t =
2.202 + case t of
2.203 + Const (@{const_name all}, _) $ Abs (_, T, t') =>
2.204 + do_quantifier (pos = SOME false) T t'
2.205 + | @{const "==>"} $ t1 $ t2 =>
2.206 + do_formula (flip pos) t1 #> do_formula pos t2
2.207 + | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
2.208 + do_term_or_formula false T t1 #> do_term_or_formula true T t2
2.209 + | @{const Trueprop} $ t1 => do_formula pos t1
2.210 + | @{const False} => I
2.211 + | @{const True} => I
2.212 + | @{const Not} $ t1 => do_formula (flip pos) t1
2.213 + | Const (@{const_name All}, _) $ Abs (_, T, t') =>
2.214 + do_quantifier (pos = SOME false) T t'
2.215 + | Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
2.216 + do_quantifier (pos = SOME true) T t'
2.217 + | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
2.218 + | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
2.219 + | @{const HOL.implies} $ t1 $ t2 =>
2.220 + do_formula (flip pos) t1 #> do_formula pos t2
2.221 + | Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2 =>
2.222 + do_term_or_formula false T t1 #> do_term_or_formula true T t2
2.223 + | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
2.224 + $ t1 $ t2 $ t3 =>
2.225 + do_formula NONE t1 #> fold (do_term_or_formula false T) [t2, t3]
2.226 + | Const (@{const_name Ex1}, _) $ Abs (_, T, t') =>
2.227 + do_quantifier (is_some pos) T t'
2.228 + | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') =>
2.229 + do_quantifier (pos = SOME false) T
2.230 + (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t'))
2.231 + | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') =>
2.232 + do_quantifier (pos = SOME true) T
2.233 + (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t'))
2.234 + | (t0 as Const (_, @{typ bool})) $ t1 =>
2.235 + do_term false t0 #> do_formula pos t1 (* theory constant *)
2.236 + | _ => do_term false t
2.237 + in do_formula pos end
2.238 +
2.239 +fun pconsts_in_fact thy is_built_in_const t =
2.240 + Symtab.fold (fn (s, pss) => fold (cons o pair s) pss)
2.241 + (Symtab.empty |> add_pconsts_in_term thy is_built_in_const true
2.242 + (SOME true) t) []
2.243 +
2.244 +val const_names_in_fact = map fst ooo pconsts_in_fact
2.245 +
2.246 +(* Inserts a dummy "constant" referring to the theory name, so that relevance
2.247 + takes the given theory into account. *)
2.248 +fun theory_constify ({theory_const_rel_weight, theory_const_irrel_weight, ...}
2.249 + : relevance_fudge) thy_name t =
2.250 + if exists (curry (op <) 0.0) [theory_const_rel_weight,
2.251 + theory_const_irrel_weight] then
2.252 + Const (thy_name ^ theory_const_suffix, @{typ bool}) $ t
2.253 + else
2.254 + t
2.255 +
2.256 +fun theory_const_prop_of fudge th =
2.257 + theory_constify fudge (Context.theory_name (theory_of_thm th)) (prop_of th)
2.258 +
2.259 +fun pair_consts_fact thy is_built_in_const fudge fact =
2.260 + case fact |> snd |> theory_const_prop_of fudge
2.261 + |> pconsts_in_fact thy is_built_in_const of
2.262 + [] => NONE
2.263 + | consts => SOME ((fact, consts), NONE)
2.264 +
2.265 +(* A two-dimensional symbol table counts frequencies of constants. It's keyed
2.266 + first by constant name and second by its list of type instantiations. For the
2.267 + latter, we need a linear ordering on "pattern list". *)
2.268 +
2.269 +fun pattern_ord p =
2.270 + case p of
2.271 + (PVar, PVar) => EQUAL
2.272 + | (PVar, PApp _) => LESS
2.273 + | (PApp _, PVar) => GREATER
2.274 + | (PApp q1, PApp q2) =>
2.275 + prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2)
2.276 +fun ptype_ord (PType p, PType q) =
2.277 + prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q)
2.278 +
2.279 +structure PType_Tab = Table(type key = ptype val ord = ptype_ord)
2.280 +
2.281 +fun count_fact_consts thy fudge =
2.282 + let
2.283 + fun do_const const (s, T) ts =
2.284 + (* Two-dimensional table update. Constant maps to types maps to count. *)
2.285 + PType_Tab.map_default (rich_ptype thy const (s, T), 0) (Integer.add 1)
2.286 + |> Symtab.map_default (s, PType_Tab.empty)
2.287 + #> fold do_term ts
2.288 + and do_term t =
2.289 + case strip_comb t of
2.290 + (Const x, ts) => do_const true x ts
2.291 + | (Free x, ts) => do_const false x ts
2.292 + | (Abs (_, _, t'), ts) => fold do_term (t' :: ts)
2.293 + | (_, ts) => fold do_term ts
2.294 + in do_term o theory_const_prop_of fudge o snd end
2.295 +
2.296 +fun pow_int _ 0 = 1.0
2.297 + | pow_int x 1 = x
2.298 + | pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x
2.299 +
2.300 +(*The frequency of a constant is the sum of those of all instances of its type.*)
2.301 +fun pconst_freq match const_tab (c, ps) =
2.302 + PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m)
2.303 + (the (Symtab.lookup const_tab c)) 0
2.304 +
2.305 +
2.306 +(* A surprising number of theorems contain only a few significant constants.
2.307 + These include all induction rules, and other general theorems. *)
2.308 +
2.309 +(* "log" seems best in practice. A constant function of one ignores the constant
2.310 + frequencies. Rare constants give more points if they are relevant than less
2.311 + rare ones. *)
2.312 +fun rel_weight_for _ freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0)
2.313 +
2.314 +(* Irrelevant constants are treated differently. We associate lower penalties to
2.315 + very rare constants and very common ones -- the former because they can't
2.316 + lead to the inclusion of too many new facts, and the latter because they are
2.317 + so common as to be of little interest. *)
2.318 +fun irrel_weight_for ({worse_irrel_freq, higher_order_irrel_weight, ...}
2.319 + : relevance_fudge) order freq =
2.320 + let val (k, x) = worse_irrel_freq |> `Real.ceil in
2.321 + (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x
2.322 + else rel_weight_for order freq / rel_weight_for order k)
2.323 + * pow_int higher_order_irrel_weight (order - 1)
2.324 + end
2.325 +
2.326 +fun multiplier_for_const_name local_const_multiplier s =
2.327 + if String.isSubstring "." s then 1.0 else local_const_multiplier
2.328 +
2.329 +(* Computes a constant's weight, as determined by its frequency. *)
2.330 +fun generic_pconst_weight local_const_multiplier abs_weight skolem_weight
2.331 + theory_const_weight chained_const_weight weight_for f
2.332 + const_tab chained_const_tab (c as (s, PType (m, _))) =
2.333 + if s = pseudo_abs_name then
2.334 + abs_weight
2.335 + else if String.isPrefix pseudo_skolem_prefix s then
2.336 + skolem_weight
2.337 + else if String.isSuffix theory_const_suffix s then
2.338 + theory_const_weight
2.339 + else
2.340 + multiplier_for_const_name local_const_multiplier s
2.341 + * weight_for m (pconst_freq (match_ptype o f) const_tab c)
2.342 + |> (if chained_const_weight < 1.0 andalso
2.343 + pconst_hyper_mem I chained_const_tab c then
2.344 + curry (op *) chained_const_weight
2.345 + else
2.346 + I)
2.347 +
2.348 +fun rel_pconst_weight ({local_const_multiplier, abs_rel_weight,
2.349 + theory_const_rel_weight, ...} : relevance_fudge)
2.350 + const_tab =
2.351 + generic_pconst_weight local_const_multiplier abs_rel_weight 0.0
2.352 + theory_const_rel_weight 0.0 rel_weight_for I const_tab
2.353 + Symtab.empty
2.354 +
2.355 +fun irrel_pconst_weight (fudge as {local_const_multiplier, abs_irrel_weight,
2.356 + skolem_irrel_weight,
2.357 + theory_const_irrel_weight,
2.358 + chained_const_irrel_weight, ...})
2.359 + const_tab chained_const_tab =
2.360 + generic_pconst_weight local_const_multiplier abs_irrel_weight
2.361 + skolem_irrel_weight theory_const_irrel_weight
2.362 + chained_const_irrel_weight (irrel_weight_for fudge) swap
2.363 + const_tab chained_const_tab
2.364 +
2.365 +fun stature_bonus ({intro_bonus, ...} : relevance_fudge) (_, Intro) =
2.366 + intro_bonus
2.367 + | stature_bonus {elim_bonus, ...} (_, Elim) = elim_bonus
2.368 + | stature_bonus {simp_bonus, ...} (_, Simp) = simp_bonus
2.369 + | stature_bonus {local_bonus, ...} (Local, _) = local_bonus
2.370 + | stature_bonus {assum_bonus, ...} (Assum, _) = assum_bonus
2.371 + | stature_bonus {chained_bonus, ...} (Chained, _) = chained_bonus
2.372 + | stature_bonus _ _ = 0.0
2.373 +
2.374 +fun is_odd_const_name s =
2.375 + s = pseudo_abs_name orelse String.isPrefix pseudo_skolem_prefix s orelse
2.376 + String.isSuffix theory_const_suffix s
2.377 +
2.378 +fun fact_weight fudge stature const_tab relevant_consts chained_consts
2.379 + fact_consts =
2.380 + case fact_consts |> List.partition (pconst_hyper_mem I relevant_consts)
2.381 + ||> filter_out (pconst_hyper_mem swap relevant_consts) of
2.382 + ([], _) => 0.0
2.383 + | (rel, irrel) =>
2.384 + if forall (forall (is_odd_const_name o fst)) [rel, irrel] then
2.385 + 0.0
2.386 + else
2.387 + let
2.388 + val irrel = irrel |> filter_out (pconst_mem swap rel)
2.389 + val rel_weight =
2.390 + 0.0 |> fold (curry (op +) o rel_pconst_weight fudge const_tab) rel
2.391 + val irrel_weight =
2.392 + ~ (stature_bonus fudge stature)
2.393 + |> fold (curry (op +)
2.394 + o irrel_pconst_weight fudge const_tab chained_consts) irrel
2.395 + val res = rel_weight / (rel_weight + irrel_weight)
2.396 + in if Real.isFinite res then res else 0.0 end
2.397 +
2.398 +type annotated_thm =
2.399 + (((unit -> string) * stature) * thm) * (string * ptype) list
2.400 +
2.401 +fun take_most_relevant ctxt max_relevant remaining_max
2.402 + ({max_imperfect, max_imperfect_exp, ...} : relevance_fudge)
2.403 + (candidates : (annotated_thm * real) list) =
2.404 + let
2.405 + val max_imperfect =
2.406 + Real.ceil (Math.pow (max_imperfect,
2.407 + Math.pow (Real.fromInt remaining_max
2.408 + / Real.fromInt max_relevant, max_imperfect_exp)))
2.409 + val (perfect, imperfect) =
2.410 + candidates |> sort (Real.compare o swap o pairself snd)
2.411 + |> take_prefix (fn (_, w) => w > 0.99999)
2.412 + val ((accepts, more_rejects), rejects) =
2.413 + chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
2.414 + in
2.415 + trace_msg ctxt (fn () =>
2.416 + "Actually passed (" ^ string_of_int (length accepts) ^ " of " ^
2.417 + string_of_int (length candidates) ^ "): " ^
2.418 + (accepts |> map (fn ((((name, _), _), _), weight) =>
2.419 + name () ^ " [" ^ Real.toString weight ^ "]")
2.420 + |> commas));
2.421 + (accepts, more_rejects @ rejects)
2.422 + end
2.423 +
2.424 +fun if_empty_replace_with_scope thy is_built_in_const facts sc tab =
2.425 + if Symtab.is_empty tab then
2.426 + Symtab.empty
2.427 + |> fold (add_pconsts_in_term thy is_built_in_const false (SOME false))
2.428 + (map_filter (fn ((_, (sc', _)), th) =>
2.429 + if sc' = sc then SOME (prop_of th) else NONE) facts)
2.430 + else
2.431 + tab
2.432 +
2.433 +fun consider_arities is_built_in_const th =
2.434 + let
2.435 + fun aux _ _ NONE = NONE
2.436 + | aux t args (SOME tab) =
2.437 + case t of
2.438 + t1 $ t2 => SOME tab |> aux t1 (t2 :: args) |> aux t2 []
2.439 + | Const (x as (s, _)) =>
2.440 + (if is_built_in_const x args |> fst then
2.441 + SOME tab
2.442 + else case Symtab.lookup tab s of
2.443 + NONE => SOME (Symtab.update (s, length args) tab)
2.444 + | SOME n => if n = length args then SOME tab else NONE)
2.445 + | _ => SOME tab
2.446 + in aux (prop_of th) [] end
2.447 +
2.448 +(* FIXME: This is currently only useful for polymorphic type encodings. *)
2.449 +fun could_benefit_from_ext is_built_in_const facts =
2.450 + fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
2.451 + |> is_none
2.452 +
2.453 +(* High enough so that it isn't wrongly considered as very relevant (e.g., for E
2.454 + weights), but low enough so that it is unlikely to be truncated away if few
2.455 + facts are included. *)
2.456 +val special_fact_index = 75
2.457 +
2.458 +fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
2.459 + (fudge as {threshold_divisor, ridiculous_threshold, ...})
2.460 + ({add, del, ...} : relevance_override) facts chained_ts hyp_ts concl_t =
2.461 + let
2.462 + val thy = Proof_Context.theory_of ctxt
2.463 + val const_tab = fold (count_fact_consts thy fudge) facts Symtab.empty
2.464 + val add_pconsts = add_pconsts_in_term thy is_built_in_const false o SOME
2.465 + val chained_const_tab = Symtab.empty |> fold (add_pconsts true) chained_ts
2.466 + val goal_const_tab =
2.467 + Symtab.empty |> fold (add_pconsts true) hyp_ts
2.468 + |> add_pconsts false concl_t
2.469 + |> (fn tab => if Symtab.is_empty tab then chained_const_tab else tab)
2.470 + |> fold (if_empty_replace_with_scope thy is_built_in_const facts)
2.471 + [Chained, Assum, Local]
2.472 + val add_ths = Attrib.eval_thms ctxt add
2.473 + val del_ths = Attrib.eval_thms ctxt del
2.474 + val facts = facts |> filter_out (member Thm.eq_thm_prop del_ths o snd)
2.475 + fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
2.476 + let
2.477 + fun relevant [] _ [] =
2.478 + (* Nothing has been added this iteration. *)
2.479 + if j = 0 andalso threshold >= ridiculous_threshold then
2.480 + (* First iteration? Try again. *)
2.481 + iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
2.482 + hopeless hopeful
2.483 + else
2.484 + []
2.485 + | relevant candidates rejects [] =
2.486 + let
2.487 + val (accepts, more_rejects) =
2.488 + take_most_relevant ctxt max_relevant remaining_max fudge
2.489 + candidates
2.490 + val rel_const_tab' =
2.491 + rel_const_tab
2.492 + |> fold (add_pconst_to_table false) (maps (snd o fst) accepts)
2.493 + fun is_dirty (c, _) =
2.494 + Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
2.495 + val (hopeful_rejects, hopeless_rejects) =
2.496 + (rejects @ hopeless, ([], []))
2.497 + |-> fold (fn (ax as (_, consts), old_weight) =>
2.498 + if exists is_dirty consts then
2.499 + apfst (cons (ax, NONE))
2.500 + else
2.501 + apsnd (cons (ax, old_weight)))
2.502 + |>> append (more_rejects
2.503 + |> map (fn (ax as (_, consts), old_weight) =>
2.504 + (ax, if exists is_dirty consts then NONE
2.505 + else SOME old_weight)))
2.506 + val threshold =
2.507 + 1.0 - (1.0 - threshold)
2.508 + * Math.pow (decay, Real.fromInt (length accepts))
2.509 + val remaining_max = remaining_max - length accepts
2.510 + in
2.511 + trace_msg ctxt (fn () => "New or updated constants: " ^
2.512 + commas (rel_const_tab' |> Symtab.dest
2.513 + |> subtract (op =) (rel_const_tab |> Symtab.dest)
2.514 + |> map string_for_hyper_pconst));
2.515 + map (fst o fst) accepts @
2.516 + (if remaining_max = 0 then
2.517 + []
2.518 + else
2.519 + iter (j + 1) remaining_max threshold rel_const_tab'
2.520 + hopeless_rejects hopeful_rejects)
2.521 + end
2.522 + | relevant candidates rejects
2.523 + (((ax as (((_, stature), _), fact_consts)), cached_weight)
2.524 + :: hopeful) =
2.525 + let
2.526 + val weight =
2.527 + case cached_weight of
2.528 + SOME w => w
2.529 + | NONE => fact_weight fudge stature const_tab rel_const_tab
2.530 + chained_const_tab fact_consts
2.531 + in
2.532 + if weight >= threshold then
2.533 + relevant ((ax, weight) :: candidates) rejects hopeful
2.534 + else
2.535 + relevant candidates ((ax, weight) :: rejects) hopeful
2.536 + end
2.537 + in
2.538 + trace_msg ctxt (fn () =>
2.539 + "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
2.540 + Real.toString threshold ^ ", constants: " ^
2.541 + commas (rel_const_tab |> Symtab.dest
2.542 + |> filter (curry (op <>) [] o snd)
2.543 + |> map string_for_hyper_pconst));
2.544 + relevant [] [] hopeful
2.545 + end
2.546 + fun prepend_facts ths accepts =
2.547 + ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
2.548 + (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
2.549 + |> take max_relevant
2.550 + fun uses_const s t =
2.551 + fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
2.552 + false
2.553 + fun uses_const_anywhere accepts s =
2.554 + exists (uses_const s o prop_of o snd) accepts orelse
2.555 + exists (uses_const s) (concl_t :: hyp_ts)
2.556 + fun add_set_const_thms accepts =
2.557 + exists (uses_const_anywhere accepts) set_consts ? append set_thms
2.558 + fun insert_into_facts accepts [] = accepts
2.559 + | insert_into_facts accepts ths =
2.560 + let
2.561 + val add = facts |> filter (member Thm.eq_thm_prop ths o snd)
2.562 + val (bef, after) =
2.563 + accepts |> filter_out (member Thm.eq_thm_prop ths o snd)
2.564 + |> take (max_relevant - length add)
2.565 + |> chop special_fact_index
2.566 + in bef @ add @ after end
2.567 + fun insert_special_facts accepts =
2.568 + (* FIXME: get rid of "ext" here once it is treated as a helper *)
2.569 + [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
2.570 + |> add_set_const_thms accepts
2.571 + |> insert_into_facts accepts
2.572 + in
2.573 + facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
2.574 + |> iter 0 max_relevant threshold0 goal_const_tab []
2.575 + |> not (null add_ths) ? prepend_facts add_ths
2.576 + |> insert_special_facts
2.577 + |> tap (fn accepts => trace_msg ctxt (fn () =>
2.578 + "Total relevant: " ^ string_of_int (length accepts)))
2.579 + end
2.580 +
2.581 +fun iterative_relevant_facts ctxt (threshold0, threshold1) max_relevant
2.582 + is_built_in_const fudge (override as {only, ...})
2.583 + chained_ths hyp_ts concl_t facts =
2.584 + let
2.585 + val thy = Proof_Context.theory_of ctxt
2.586 + val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
2.587 + 1.0 / Real.fromInt (max_relevant + 1))
2.588 + in
2.589 + trace_msg ctxt (fn () => "Considering " ^ string_of_int (length facts) ^
2.590 + " facts");
2.591 + (if only orelse threshold1 < 0.0 then
2.592 + facts
2.593 + else if threshold0 > 1.0 orelse threshold0 > threshold1 orelse
2.594 + max_relevant = 0 then
2.595 + []
2.596 + else
2.597 + relevance_filter ctxt threshold0 decay max_relevant is_built_in_const
2.598 + fudge override facts (chained_ths |> map prop_of) hyp_ts
2.599 + (concl_t |> theory_constify fudge (Context.theory_name thy)))
2.600 + |> map (apfst (apfst (fn f => f ())))
2.601 + end
2.602 +
2.603 +end;
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 11 21:43:19 2012 +0200
3.3 @@ -0,0 +1,13 @@
3.4 +(* Title: HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML
3.5 + Author: Jasmin Blanchette, TU Muenchen
3.6 +
3.7 +Sledgehammer's machine-learning-based relevance filter (MaSh).
3.8 +*)
3.9 +
3.10 +signature SLEDGEHAMMER_FILTER_MASH =
3.11 +sig
3.12 +end;
3.13 +
3.14 +structure Sledgehammer_Filter_MaSh : SLEDGEHAMMER_FILTER_MASH =
3.15 +struct
3.16 +end;