1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 27 11:27:38 2010 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Fri Aug 27 13:12:23 2010 +0200
1.3 @@ -65,44 +65,37 @@
1.4
1.5 (*** constants with types ***)
1.6
1.7 -(*An abstraction of Isabelle types*)
1.8 -datatype pseudotype = PVar | PType of string * pseudotype list
1.9 +(* An abstraction of Isabelle types and first-order terms *)
1.10 +datatype pattern = PVar | PApp of string * pattern list
1.11
1.12 -fun string_for_pseudotype PVar = "_"
1.13 - | string_for_pseudotype (PType (s, Ts)) =
1.14 - (case Ts of
1.15 - [] => ""
1.16 - | [T] => string_for_pseudotype T ^ " "
1.17 - | Ts => string_for_pseudotypes Ts ^ " ") ^ s
1.18 -and string_for_pseudotypes Ts =
1.19 - "(" ^ commas (map string_for_pseudotype Ts) ^ ")"
1.20 +fun string_for_pattern PVar = "_"
1.21 + | string_for_pattern (PApp (s, ps)) =
1.22 + if null ps then s else s ^ string_for_patterns ps
1.23 +and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")"
1.24
1.25 (*Is the second type an instance of the first one?*)
1.26 -fun match_pseudotype (PType (a, T), PType (b, U)) =
1.27 - a = b andalso match_pseudotypes (T, U)
1.28 - | match_pseudotype (PVar, _) = true
1.29 - | match_pseudotype (_, PVar) = false
1.30 -and match_pseudotypes ([], []) = true
1.31 - | match_pseudotypes (T :: Ts, U :: Us) =
1.32 - match_pseudotype (T, U) andalso match_pseudotypes (Ts, Us)
1.33 +fun match_pattern (PApp (a, T), PApp (b, U)) =
1.34 + a = b andalso match_patterns (T, U)
1.35 + | match_pattern (PVar, _) = true
1.36 + | match_pattern (_, PVar) = false
1.37 +and match_patterns ([], []) = true
1.38 + | match_patterns (T :: Ts, U :: Us) =
1.39 + match_pattern (T, U) andalso match_patterns (Ts, Us)
1.40
1.41 -(*Is there a unifiable constant?*)
1.42 -fun pseudoconst_mem f const_tab (c, c_typ) =
1.43 - exists (curry (match_pseudotypes o f) c_typ)
1.44 - (these (Symtab.lookup const_tab c))
1.45 +(* Is there a unifiable constant? *)
1.46 +fun pconst_mem f const_tab (s, ps) =
1.47 + exists (curry (match_patterns o f) ps) (these (Symtab.lookup const_tab s))
1.48
1.49 -fun pseudotype_for (Type (c,typs)) = PType (c, map pseudotype_for typs)
1.50 - | pseudotype_for (TFree _) = PVar
1.51 - | pseudotype_for (TVar _) = PVar
1.52 +fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts)
1.53 + | pattern_for_type (TFree (s, _)) = PApp (s, [])
1.54 + | pattern_for_type (TVar _) = PVar
1.55 (* Pairs a constant with the list of its type instantiations. *)
1.56 -fun pseudoconst_for thy (c, T) =
1.57 - (c, map pseudotype_for (Sign.const_typargs thy (c, T)))
1.58 +fun pconst_for thy (c, T) =
1.59 + (c, map pattern_for_type (Sign.const_typargs thy (c, T)))
1.60 handle TYPE _ => (c, []) (* Variable (locale constant): monomorphic *)
1.61
1.62 -fun string_for_pseudoconst (s, []) = s
1.63 - | string_for_pseudoconst (s, Ts) = s ^ string_for_pseudotypes Ts
1.64 -fun string_for_super_pseudoconst (s, Tss) =
1.65 - s ^ "{" ^ commas (map string_for_pseudotypes Tss) ^ "}"
1.66 +fun string_for_super_pconst (s, pss) =
1.67 + s ^ "{" ^ commas (map string_for_patterns pss) ^ "}"
1.68
1.69 val abs_name = "Sledgehammer.abs"
1.70 val skolem_prefix = "Sledgehammer.sko"
1.71 @@ -113,9 +106,9 @@
1.72 [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let},
1.73 @{const_name "op ="}]
1.74
1.75 -(* Add a pseudoconstant to the table, but a [] entry means a standard
1.76 +(* Add a pconstant to the table, but a [] entry means a standard
1.77 connective, which we ignore.*)
1.78 -fun add_pseudoconst_to_table also_skolem (c, Ts) =
1.79 +fun add_pconst_to_table also_skolem (c, Ts) =
1.80 if member (op =) boring_consts c orelse
1.81 (not also_skolem andalso String.isPrefix skolem_prefix c) then
1.82 I
1.83 @@ -124,7 +117,7 @@
1.84
1.85 fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
1.86
1.87 -fun get_pseudoconsts thy also_skolems pos ts =
1.88 +fun get_pconsts thy also_skolems pos ts =
1.89 let
1.90 val flip = Option.map not
1.91 (* We include free variables, as well as constants, to handle locales. For
1.92 @@ -132,16 +125,16 @@
1.93 introduce a fresh constant to simulate the effect of Skolemization. *)
1.94 fun do_term t =
1.95 case t of
1.96 - Const x => add_pseudoconst_to_table also_skolems (pseudoconst_for thy x)
1.97 - | Free (s, _) => add_pseudoconst_to_table also_skolems (s, [])
1.98 + Const x => add_pconst_to_table also_skolems (pconst_for thy x)
1.99 + | Free (s, _) => add_pconst_to_table also_skolems (s, [])
1.100 | t1 $ t2 => fold do_term [t1, t2]
1.101 | Abs (_, _, t') =>
1.102 - do_term t' #> add_pseudoconst_to_table true (abs_name, [])
1.103 + do_term t' #> add_pconst_to_table true (abs_name, [])
1.104 | _ => I
1.105 fun do_quantifier will_surely_be_skolemized body_t =
1.106 do_formula pos body_t
1.107 #> (if also_skolems andalso will_surely_be_skolemized then
1.108 - add_pseudoconst_to_table true (gensym skolem_prefix, [])
1.109 + add_pconst_to_table true (gensym skolem_prefix, [])
1.110 else
1.111 I)
1.112 and do_term_or_formula T =
1.113 @@ -197,23 +190,23 @@
1.114
1.115 (* A two-dimensional symbol table counts frequencies of constants. It's keyed
1.116 first by constant name and second by its list of type instantiations. For the
1.117 - latter, we need a linear ordering on "pseudotype list". *)
1.118 + latter, we need a linear ordering on "pattern list". *)
1.119
1.120 -fun pseudotype_ord p =
1.121 +fun pattern_ord p =
1.122 case p of
1.123 (PVar, PVar) => EQUAL
1.124 - | (PVar, PType _) => LESS
1.125 - | (PType _, PVar) => GREATER
1.126 - | (PType q1, PType q2) =>
1.127 - prod_ord fast_string_ord (dict_ord pseudotype_ord) (q1, q2)
1.128 + | (PVar, PApp _) => LESS
1.129 + | (PApp _, PVar) => GREATER
1.130 + | (PApp q1, PApp q2) =>
1.131 + prod_ord fast_string_ord (dict_ord pattern_ord) (q1, q2)
1.132
1.133 structure CTtab =
1.134 - Table(type key = pseudotype list val ord = dict_ord pseudotype_ord)
1.135 + Table(type key = pattern list val ord = dict_ord pattern_ord)
1.136
1.137 fun count_axiom_consts theory_relevant thy (_, th) =
1.138 let
1.139 fun do_const (a, T) =
1.140 - let val (c, cts) = pseudoconst_for thy (a, T) in
1.141 + let val (c, cts) = pconst_for thy (a, T) in
1.142 (* Two-dimensional table update. Constant maps to types maps to
1.143 count. *)
1.144 CTtab.map_default (cts, 0) (Integer.add 1)
1.145 @@ -230,7 +223,7 @@
1.146 (**** Actual Filtering Code ****)
1.147
1.148 (*The frequency of a constant is the sum of those of all instances of its type.*)
1.149 -fun pseudoconst_freq match const_tab (c, Ts) =
1.150 +fun pconst_freq match const_tab (c, Ts) =
1.151 CTtab.fold (fn (Ts', m) => match (Ts, Ts') ? Integer.add m)
1.152 (the (Symtab.lookup const_tab c)) 0
1.153
1.154 @@ -256,7 +249,7 @@
1.155 fun generic_weight abs_weight skolem_weight logx f const_tab (c as (s, _)) =
1.156 if s = abs_name then abs_weight
1.157 else if String.isPrefix skolem_prefix s then skolem_weight
1.158 - else logx (pseudoconst_freq (match_pseudotypes o f) const_tab c)
1.159 + else logx (pconst_freq (match_patterns o f) const_tab c)
1.160
1.161 val rel_weight = generic_weight abs_rel_weight skolem_rel_weight rel_log I
1.162 val irrel_weight = generic_weight abs_irrel_weight skolem_irrel_weight irrel_log
1.163 @@ -269,8 +262,8 @@
1.164 | locality_multiplier Chained = 2.0
1.165
1.166 fun axiom_weight loc const_tab relevant_consts axiom_consts =
1.167 - case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
1.168 - ||> filter_out (pseudoconst_mem swap relevant_consts) of
1.169 + case axiom_consts |> List.partition (pconst_mem I relevant_consts)
1.170 + ||> filter_out (pconst_mem swap relevant_consts) of
1.171 ([], []) => 0.0
1.172 | (_, []) => 1.0
1.173 | (rel, irrel) =>
1.174 @@ -283,8 +276,8 @@
1.175
1.176 (* TODO: experiment
1.177 fun debug_axiom_weight const_tab relevant_consts axiom_consts =
1.178 - case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
1.179 - ||> filter_out (pseudoconst_mem swap relevant_consts) of
1.180 + case axiom_consts |> List.partition (pconst_mem I relevant_consts)
1.181 + ||> filter_out (pconst_mem swap relevant_consts) of
1.182 ([], []) => 0.0
1.183 | (_, []) => 1.0
1.184 | (rel, irrel) =>
1.185 @@ -297,15 +290,15 @@
1.186 in if Real.isFinite res then res else 0.0 end
1.187 *)
1.188
1.189 -fun pseudoconsts_in_axiom thy t =
1.190 +fun pconsts_in_axiom thy t =
1.191 Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys)
1.192 - (get_pseudoconsts thy true (SOME true) [t]) []
1.193 + (get_pconsts thy true (SOME true) [t]) []
1.194 fun pair_consts_axiom theory_relevant thy axiom =
1.195 (axiom, axiom |> snd |> theory_const_prop_of theory_relevant
1.196 - |> pseudoconsts_in_axiom thy)
1.197 + |> pconsts_in_axiom thy)
1.198
1.199 type annotated_thm =
1.200 - (((unit -> string) * locality) * thm) * (string * pseudotype list) list
1.201 + (((unit -> string) * locality) * thm) * (string * pattern list) list
1.202
1.203 fun take_most_relevant max_max_imperfect max_relevant remaining_max
1.204 (candidates : (annotated_thm * real) list) =
1.205 @@ -334,7 +327,7 @@
1.206
1.207 fun if_empty_replace_with_locality thy axioms loc tab =
1.208 if Symtab.is_empty tab then
1.209 - get_pseudoconsts thy false (SOME false)
1.210 + get_pconsts thy false (SOME false)
1.211 (map_filter (fn ((_, loc'), th) =>
1.212 if loc' = loc then SOME (prop_of th) else NONE) axioms)
1.213 else
1.214 @@ -352,7 +345,7 @@
1.215 val const_tab =
1.216 fold (count_axiom_consts theory_relevant thy) axioms Symtab.empty
1.217 val goal_const_tab =
1.218 - get_pseudoconsts thy false (SOME false) goal_ts
1.219 + get_pconsts thy false (SOME false) goal_ts
1.220 |> fold (if_empty_replace_with_locality thy axioms)
1.221 [Chained, Local, Theory]
1.222 val add_thms = maps (ProofContext.get_fact ctxt) add
1.223 @@ -384,7 +377,7 @@
1.224 candidates
1.225 val rel_const_tab' =
1.226 rel_const_tab
1.227 - |> fold (add_pseudoconst_to_table false)
1.228 + |> fold (add_pconst_to_table false)
1.229 (maps (snd o fst) accepts)
1.230 fun is_dirty (c, _) =
1.231 Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
1.232 @@ -407,7 +400,7 @@
1.233 trace_msg (fn () => "New or updated constants: " ^
1.234 commas (rel_const_tab' |> Symtab.dest
1.235 |> subtract (op =) (rel_const_tab |> Symtab.dest)
1.236 - |> map string_for_super_pseudoconst));
1.237 + |> map string_for_super_pconst));
1.238 map (fst o fst) accepts @
1.239 (if remaining_max = 0 then
1.240 game_over (hopeful_rejects @ map (apsnd SOME) hopeless_rejects)
1.241 @@ -442,7 +435,7 @@
1.242 Real.toString threshold ^ ", constants: " ^
1.243 commas (rel_const_tab |> Symtab.dest
1.244 |> filter (curry (op <>) [] o snd)
1.245 - |> map string_for_super_pseudoconst));
1.246 + |> map string_for_super_pconst));
1.247 relevant [] [] hopeless hopeful
1.248 end
1.249 in