# HG changeset patch # User blanchet # Date 1283278798 -7200 # Node ID f0aa0c49fdbff15689ffb2f85bced78806da872d # Parent 2b93dbc07778dbc839e35a2332a40dde6c9df8f0 add a penalty for being higher-order diff -r 2b93dbc07778 -r f0aa0c49fdbf src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 31 13:12:56 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 31 20:19:58 2010 +0200 @@ -14,6 +14,7 @@ val trace : bool Unsynchronized.ref val worse_irrel_freq : real Unsynchronized.ref + val higher_order_irrel_weight : real Unsynchronized.ref val abs_rel_weight : real Unsynchronized.ref val abs_irrel_weight : real Unsynchronized.ref val skolem_irrel_weight : real Unsynchronized.ref @@ -80,13 +81,22 @@ (*** constants with types ***) +fun order_of_type (Type (@{type_name fun}, [T1, @{typ bool}])) = + order_of_type T1 (* cheat: pretend sets are first-order *) + | order_of_type (Type (@{type_name fun}, [T1, T2])) = + Int.max (order_of_type T1 + 1, order_of_type T2) + | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0 + | order_of_type _ = 0 + (* An abstraction of Isabelle types and first-order terms *) datatype pattern = PVar | PApp of string * pattern list +datatype ptype = PType of int * pattern list fun string_for_pattern PVar = "_" | string_for_pattern (PApp (s, ps)) = if null ps then s else s ^ string_for_patterns ps and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")" +fun string_for_ptype (PType (_, ps)) = string_for_patterns ps (*Is the second type an instance of the first one?*) fun match_pattern (PVar, _) = true @@ -97,17 +107,18 @@ | match_patterns ([], _) = false | match_patterns (p :: ps, q :: qs) = match_pattern (p, q) andalso match_patterns (ps, qs) +fun match_ptype (PType (_, ps), PType (_, qs)) = match_patterns (ps, qs) (* Is there a unifiable constant? *) fun pconst_mem f consts (s, ps) = - exists (curry (match_patterns o f) ps) + exists (curry (match_ptype o f) ps) (map snd (filter (curry (op =) s o fst) consts)) fun pconst_hyper_mem f const_tab (s, ps) = - exists (curry (match_patterns o f) ps) (these (Symtab.lookup const_tab s)) + exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s)) -fun ptype (Type (s, Ts)) = PApp (s, map ptype Ts) - | ptype (TFree (s, _)) = PApp (s, []) - | ptype (TVar _) = PVar +fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts) + | pattern_for_type (TFree (s, _)) = PApp (s, []) + | pattern_for_type (TVar _) = PVar fun pterm thy t = case strip_comb t of @@ -116,14 +127,17 @@ | (Var x, []) => PVar | _ => PApp ("?", []) (* equivalence class of higher-order constructs *) (* Pairs a constant with the list of its type instantiations. *) -and pconst_args thy const (s, T) ts = - (if const then map ptype (these (try (Sign.const_typargs thy) (s, T))) +and ptype thy const x ts = + (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x)) else []) @ (if term_patterns then map (pterm thy) ts else []) -and pconst thy const (s, T) ts = (s, pconst_args thy const (s, T) ts) +and pconst thy const (s, T) ts = (s, ptype thy const (s, T) ts) +and rich_ptype thy const (s, T) ts = + PType (order_of_type T, ptype thy const (s, T) ts) +and rich_pconst thy const (s, T) ts = (s, rich_ptype thy const (s, T) ts) -fun string_for_hyper_pconst (s, pss) = - s ^ "{" ^ commas (map string_for_patterns pss) ^ "}" +fun string_for_hyper_pconst (s, ps) = + s ^ "{" ^ commas (map string_for_ptype ps) ^ "}" val abs_name = "Sledgehammer.abs" val skolem_prefix = "Sledgehammer.sko" @@ -136,12 +150,12 @@ (* Add a pconstant to the table, but a [] entry means a standard connective, which we ignore.*) -fun add_pconst_to_table also_skolem (c, ps) = +fun add_pconst_to_table also_skolem (c, p) = if member (op =) boring_consts c orelse (not also_skolem andalso String.isPrefix skolem_prefix c) then I else - Symtab.map_default (c, [ps]) (insert (op =) ps) + Symtab.map_default (c, [p]) (insert (op =) p) fun is_formula_type T = (T = HOLogic.boolT orelse T = propT) @@ -152,38 +166,40 @@ each quantifiers that must necessarily be skolemized by the ATP, we introduce a fresh constant to simulate the effect of Skolemization. *) fun do_const const (s, T) ts = - add_pconst_to_table also_skolems (pconst thy const (s, T) ts) + add_pconst_to_table also_skolems (rich_pconst thy const (s, T) ts) #> fold do_term ts and do_term t = case strip_comb t of (Const x, ts) => do_const true x ts | (Free x, ts) => do_const false x ts - | (Abs (_, _, t'), ts) => - (null ts ? add_pconst_to_table true (abs_name, [])) + | (Abs (_, T, t'), ts) => + (null ts + ? add_pconst_to_table true (abs_name, PType (order_of_type T + 1, []))) #> fold do_term (t' :: ts) | (_, ts) => fold do_term ts - fun do_quantifier will_surely_be_skolemized body_t = + fun do_quantifier will_surely_be_skolemized abs_T body_t = do_formula pos body_t #> (if also_skolems andalso will_surely_be_skolemized then - add_pconst_to_table true (gensym skolem_prefix, []) + add_pconst_to_table true + (gensym skolem_prefix, PType (order_of_type abs_T, [])) else I) and do_term_or_formula T = if is_formula_type T then do_formula NONE else do_term and do_formula pos t = case t of - Const (@{const_name all}, _) $ Abs (_, _, body_t) => - do_quantifier (pos = SOME false) body_t + Const (@{const_name all}, _) $ Abs (_, T, t') => + do_quantifier (pos = SOME false) T t' | @{const "==>"} $ t1 $ t2 => do_formula (flip pos) t1 #> do_formula pos t2 | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 => fold (do_term_or_formula T) [t1, t2] | @{const Trueprop} $ t1 => do_formula pos t1 | @{const Not} $ t1 => do_formula (flip pos) t1 - | Const (@{const_name All}, _) $ Abs (_, _, body_t) => - do_quantifier (pos = SOME false) body_t - | Const (@{const_name Ex}, _) $ Abs (_, _, body_t) => - do_quantifier (pos = SOME true) body_t + | Const (@{const_name All}, _) $ Abs (_, T, t') => + do_quantifier (pos = SOME false) T t' + | Const (@{const_name Ex}, _) $ Abs (_, T, t') => + do_quantifier (pos = SOME true) T t' | @{const HOL.conj} $ t1 $ t2 => fold (do_formula pos) [t1, t2] | @{const HOL.disj} $ t1 $ t2 => fold (do_formula pos) [t1, t2] | @{const HOL.implies} $ t1 $ t2 => @@ -193,14 +209,14 @@ | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])])) $ t1 $ t2 $ t3 => do_formula NONE t1 #> fold (do_term_or_formula T) [t2, t3] - | Const (@{const_name Ex1}, _) $ Abs (_, _, body_t) => - do_quantifier (is_some pos) body_t - | Const (@{const_name Ball}, _) $ t1 $ Abs (_, _, body_t) => - do_quantifier (pos = SOME false) - (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, body_t)) - | Const (@{const_name Bex}, _) $ t1 $ Abs (_, _, body_t) => - do_quantifier (pos = SOME true) - (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, body_t)) + | Const (@{const_name Ex1}, _) $ Abs (_, T, t') => + do_quantifier (is_some pos) T t' + | Const (@{const_name Ball}, _) $ t1 $ Abs (_, T, t') => + do_quantifier (pos = SOME false) T + (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, t')) + | Const (@{const_name Bex}, _) $ t1 $ Abs (_, T, t') => + do_quantifier (pos = SOME true) T + (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, t')) | (t0 as Const (_, @{typ bool})) $ t1 => do_term t0 #> do_formula pos t1 (* theory constant *) | _ => do_term t @@ -230,16 +246,17 @@ | (PApp _, PVar) => GREATER | (PApp q1, PApp q2) => prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2) +fun ptype_ord (PType p, PType q) = + prod_ord (dict_ord pattern_ord) int_ord (swap p, swap q) -structure CTtab = - Table(type key = pattern list val ord = dict_ord pattern_ord) +structure PType_Tab = Table(type key = ptype val ord = ptype_ord) fun count_axiom_consts theory_relevant thy = let fun do_const const (s, T) ts = (* Two-dimensional table update. Constant maps to types maps to count. *) - CTtab.map_default (pconst_args thy const (s, T) ts, 0) (Integer.add 1) - |> Symtab.map_default (s, CTtab.empty) + PType_Tab.map_default (rich_ptype thy const (s, T) ts, 0) (Integer.add 1) + |> Symtab.map_default (s, PType_Tab.empty) #> fold do_term ts and do_term t = case strip_comb t of @@ -252,10 +269,14 @@ (**** Actual Filtering Code ****) +fun pow_int x 0 = 1.0 + | pow_int x 1 = x + | pow_int x n = if n > 0 then x * pow_int x (n - 1) else pow_int x (n + 1) / x + (*The frequency of a constant is the sum of those of all instances of its type.*) fun pconst_freq match const_tab (c, ps) = - CTtab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m) - (the (Symtab.lookup const_tab c)) 0 + PType_Tab.fold (fn (qs, m) => match (ps, qs) ? Integer.add m) + (the (Symtab.lookup const_tab c)) 0 (* A surprising number of theorems contain only a few significant constants. @@ -264,19 +285,21 @@ (* "log" seems best in practice. A constant function of one ignores the constant frequencies. Rare constants give more points if they are relevant than less rare ones. *) -fun rel_weight_for_freq n = 1.0 + 2.0 / Math.ln (Real.fromInt n + 1.0) +fun rel_weight_for order freq = 1.0 + 2.0 / Math.ln (Real.fromInt freq + 1.0) (* FUDGE *) val worse_irrel_freq = Unsynchronized.ref 100.0 +val higher_order_irrel_weight = Unsynchronized.ref 1.05 (* Irrelevant constants are treated differently. We associate lower penalties to very rare constants and very common ones -- the former because they can't lead to the inclusion of too many new facts, and the latter because they are so common as to be of little interest. *) -fun irrel_weight_for_freq n = +fun irrel_weight_for order freq = let val (k, x) = !worse_irrel_freq |> `Real.ceil in - if n < k then Math.ln (Real.fromInt (n + 1)) / Math.ln x - else rel_weight_for_freq n / rel_weight_for_freq k + (if freq < k then Math.ln (Real.fromInt (freq + 1)) / Math.ln x + else rel_weight_for order freq / rel_weight_for order k) + * pow_int (!higher_order_irrel_weight) (order - 1) end (* FUDGE *) @@ -285,17 +308,17 @@ val skolem_irrel_weight = Unsynchronized.ref 0.75 (* Computes a constant's weight, as determined by its frequency. *) -fun generic_pconst_weight abs_weight skolem_weight weight_for_freq f const_tab - (c as (s, _)) = +fun generic_pconst_weight abs_weight skolem_weight weight_for f const_tab + (c as (s, PType (m, _))) = if s = abs_name then abs_weight else if String.isPrefix skolem_prefix s then skolem_weight - else weight_for_freq (pconst_freq (match_patterns o f) const_tab c) + else weight_for m (pconst_freq (match_ptype o f) const_tab c) fun rel_pconst_weight const_tab = - generic_pconst_weight (!abs_rel_weight) 0.0 rel_weight_for_freq I const_tab + generic_pconst_weight (!abs_rel_weight) 0.0 rel_weight_for I const_tab fun irrel_pconst_weight const_tab = generic_pconst_weight (!abs_irrel_weight) (!skolem_irrel_weight) - irrel_weight_for_freq swap const_tab + irrel_weight_for swap const_tab (* FUDGE *) val intro_bonus = Unsynchronized.ref 0.15 @@ -340,7 +363,7 @@ ~ (locality_bonus loc) |> fold (curry (op +) o irrel_pconst_weight const_tab) irrel val _ = tracing (PolyML.makestring ("REL: ", map (`(rel_pconst_weight const_tab)) rel)) -val _ = tracing (PolyML.makestring ("IRREL: ", map (`(irrel_pconst_weight const_tab)) irrel))(*###*) +val _ = tracing (PolyML.makestring ("IRREL: ", map (`(irrel_pconst_weight const_tab)) irrel)) val res = rels_weight / (rels_weight + irrels_weight) in if Real.isFinite res then res else 0.0 end *) @@ -355,7 +378,7 @@ | consts => SOME ((axiom, consts), NONE) type annotated_thm = - (((unit -> string) * locality) * thm) * (string * pattern list) list + (((unit -> string) * locality) * thm) * (string * ptype) list (* FUDGE *) val max_imperfect = Unsynchronized.ref 11.5 diff -r 2b93dbc07778 -r f0aa0c49fdbf src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 31 13:12:56 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 31 20:19:58 2010 +0200 @@ -67,7 +67,7 @@ ("verbose", "false"), ("overlord", "false"), ("explicit_apply", "false"), - ("relevance_thresholds", "45 90"), + ("relevance_thresholds", "45 85"), ("max_relevant", "smart"), ("theory_relevant", "smart"), ("isar_proof", "false"),