1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Mar 27 16:59:13 2012 +0300
1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Mar 27 16:59:13 2012 +0300
1.3 @@ -131,8 +131,8 @@
1.4 val avoid_first_order_ghost_type_vars = false
1.5
1.6 val bound_var_prefix = "B_"
1.7 -val all_bound_var_prefix = "BA_"
1.8 -val exist_bound_var_prefix = "BE_"
1.9 +val all_bound_var_prefix = "A_"
1.10 +val exist_bound_var_prefix = "E_"
1.11 val schematic_var_prefix = "V_"
1.12 val fixed_var_prefix = "v_"
1.13 val tvar_prefix = "T_"
1.14 @@ -824,10 +824,10 @@
1.15
1.16 fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
1.17
1.18 -fun insert_type ctxt get_T x xs =
1.19 +fun insert_type thy get_T x xs =
1.20 let val T = get_T x in
1.21 - if exists (type_instance ctxt T o get_T) xs then xs
1.22 - else x :: filter_out (type_generalization ctxt T o get_T) xs
1.23 + if exists (type_instance thy T o get_T) xs then xs
1.24 + else x :: filter_out (type_generalization thy T o get_T) xs
1.25 end
1.26
1.27 (* The Booleans indicate whether all type arguments should be kept. *)
1.28 @@ -1342,20 +1342,24 @@
1.29 | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
1.30 maybe_nonmono_Ts, ...}
1.31 (Noninf_Nonmono_Types (strictness, grain)) T =
1.32 - grain = Ghost_Type_Arg_Vars orelse
1.33 - (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
1.34 - not (exists (type_instance ctxt T) surely_infinite_Ts orelse
1.35 - (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso
1.36 - is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
1.37 - T)))
1.38 + let val thy = Proof_Context.theory_of ctxt in
1.39 + grain = Ghost_Type_Arg_Vars orelse
1.40 + (exists (type_intersect thy T) maybe_nonmono_Ts andalso
1.41 + not (exists (type_instance thy T) surely_infinite_Ts orelse
1.42 + (not (member (type_equiv thy) maybe_finite_Ts T) andalso
1.43 + is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
1.44 + T)))
1.45 + end
1.46 | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
1.47 maybe_nonmono_Ts, ...}
1.48 (Fin_Nonmono_Types grain) T =
1.49 - grain = Ghost_Type_Arg_Vars orelse
1.50 - (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
1.51 - (exists (type_generalization ctxt T) surely_finite_Ts orelse
1.52 - (not (member (type_equiv ctxt) maybe_infinite_Ts T) andalso
1.53 - is_type_surely_finite ctxt T)))
1.54 + let val thy = Proof_Context.theory_of ctxt in
1.55 + grain = Ghost_Type_Arg_Vars orelse
1.56 + (exists (type_intersect thy T) maybe_nonmono_Ts andalso
1.57 + (exists (type_generalization thy T) surely_finite_Ts orelse
1.58 + (not (member (type_equiv thy) maybe_infinite_Ts T) andalso
1.59 + is_type_surely_finite ctxt T)))
1.60 + end
1.61 | should_encode_type _ _ _ _ = false
1.62
1.63 fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
1.64 @@ -1425,8 +1429,8 @@
1.65 fun consider_var_ary const_T var_T max_ary =
1.66 let
1.67 fun iter ary T =
1.68 - if ary = max_ary orelse type_instance ctxt var_T T orelse
1.69 - type_instance ctxt T var_T then
1.70 + if ary = max_ary orelse type_instance thy var_T T orelse
1.71 + type_instance thy T var_T then
1.72 ary
1.73 else
1.74 iter (ary + 1) (range_type T)
1.75 @@ -1445,7 +1449,7 @@
1.76 min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
1.77 max_ary = max_ary, types = types, in_conj = in_conj}
1.78 val fun_var_Ts' =
1.79 - fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
1.80 + fun_var_Ts |> can dest_funT T ? insert_type thy I T
1.81 in
1.82 if bool_vars' = bool_vars andalso
1.83 pointer_eq (fun_var_Ts', fun_var_Ts) then
1.84 @@ -1473,7 +1477,7 @@
1.85 let
1.86 val pred_sym =
1.87 pred_sym andalso top_level andalso not bool_vars
1.88 - val types' = types |> insert_type ctxt I T
1.89 + val types' = types |> insert_type thy I T
1.90 val in_conj = in_conj orelse conj_fact
1.91 val min_ary =
1.92 if (app_op_level = Sufficient_App_Op orelse
1.93 @@ -2070,7 +2074,7 @@
1.94 map (decl_line_for_class order) classes
1.95 | _ => []
1.96
1.97 -fun sym_decl_table_for_facts ctxt format type_enc sym_tab
1.98 +fun sym_decl_table_for_facts thy format type_enc sym_tab
1.99 (conjs, facts, extra_tms) =
1.100 let
1.101 fun add_iterm_syms tm =
1.102 @@ -2091,8 +2095,8 @@
1.103 in
1.104 if decl_sym then
1.105 Symtab.map_default (s, [])
1.106 - (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
1.107 - in_conj))
1.108 + (insert_type thy #3 (s', T_args, T, pred_sym, length args,
1.109 + in_conj))
1.110 else
1.111 I
1.112 end
1.113 @@ -2102,7 +2106,7 @@
1.114 end
1.115 val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> fact_lift
1.116 fun add_formula_var_types (AQuant (_, xs, phi)) =
1.117 - fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
1.118 + fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs
1.119 #> add_formula_var_types phi
1.120 | add_formula_var_types (AConn (_, phis)) =
1.121 fold add_formula_var_types phis
1.122 @@ -2119,12 +2123,12 @@
1.123 | _ => I)
1.124 in
1.125 Symtab.map_default (s, [])
1.126 - (insert_type ctxt #3 (s', [T], T, false, 0, false))
1.127 + (insert_type thy #3 (s', [T], T, false, 0, false))
1.128 end
1.129 fun add_TYPE_const () =
1.130 let val (s, s') = TYPE_name in
1.131 Symtab.map_default (s, [])
1.132 - (insert_type ctxt #3
1.133 + (insert_type thy #3
1.134 (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
1.135 end
1.136 in
1.137 @@ -2158,44 +2162,46 @@
1.138 (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
1.139 (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
1.140 surely_infinite_Ts, maybe_nonmono_Ts}) =
1.141 - if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
1.142 - case level of
1.143 - Noninf_Nonmono_Types (strictness, _) =>
1.144 - if exists (type_instance ctxt T) surely_infinite_Ts orelse
1.145 - member (type_equiv ctxt) maybe_finite_Ts T then
1.146 - mono
1.147 - else if is_type_kind_of_surely_infinite ctxt strictness
1.148 - surely_infinite_Ts T then
1.149 - {maybe_finite_Ts = maybe_finite_Ts,
1.150 - surely_finite_Ts = surely_finite_Ts,
1.151 - maybe_infinite_Ts = maybe_infinite_Ts,
1.152 - surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
1.153 - maybe_nonmono_Ts = maybe_nonmono_Ts}
1.154 - else
1.155 - {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv ctxt) T,
1.156 - surely_finite_Ts = surely_finite_Ts,
1.157 - maybe_infinite_Ts = maybe_infinite_Ts,
1.158 - surely_infinite_Ts = surely_infinite_Ts,
1.159 - maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
1.160 - | Fin_Nonmono_Types _ =>
1.161 - if exists (type_instance ctxt T) surely_finite_Ts orelse
1.162 - member (type_equiv ctxt) maybe_infinite_Ts T then
1.163 - mono
1.164 - else if is_type_surely_finite ctxt T then
1.165 - {maybe_finite_Ts = maybe_finite_Ts,
1.166 - surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T,
1.167 - maybe_infinite_Ts = maybe_infinite_Ts,
1.168 - surely_infinite_Ts = surely_infinite_Ts,
1.169 - maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
1.170 - else
1.171 - {maybe_finite_Ts = maybe_finite_Ts,
1.172 - surely_finite_Ts = surely_finite_Ts,
1.173 - maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv ctxt) T,
1.174 - surely_infinite_Ts = surely_infinite_Ts,
1.175 - maybe_nonmono_Ts = maybe_nonmono_Ts}
1.176 - | _ => mono
1.177 - else
1.178 - mono
1.179 + let val thy = Proof_Context.theory_of ctxt in
1.180 + if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
1.181 + case level of
1.182 + Noninf_Nonmono_Types (strictness, _) =>
1.183 + if exists (type_instance thy T) surely_infinite_Ts orelse
1.184 + member (type_equiv thy) maybe_finite_Ts T then
1.185 + mono
1.186 + else if is_type_kind_of_surely_infinite ctxt strictness
1.187 + surely_infinite_Ts T then
1.188 + {maybe_finite_Ts = maybe_finite_Ts,
1.189 + surely_finite_Ts = surely_finite_Ts,
1.190 + maybe_infinite_Ts = maybe_infinite_Ts,
1.191 + surely_infinite_Ts = surely_infinite_Ts |> insert_type thy I T,
1.192 + maybe_nonmono_Ts = maybe_nonmono_Ts}
1.193 + else
1.194 + {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv thy) T,
1.195 + surely_finite_Ts = surely_finite_Ts,
1.196 + maybe_infinite_Ts = maybe_infinite_Ts,
1.197 + surely_infinite_Ts = surely_infinite_Ts,
1.198 + maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
1.199 + | Fin_Nonmono_Types _ =>
1.200 + if exists (type_instance thy T) surely_finite_Ts orelse
1.201 + member (type_equiv thy) maybe_infinite_Ts T then
1.202 + mono
1.203 + else if is_type_surely_finite ctxt T then
1.204 + {maybe_finite_Ts = maybe_finite_Ts,
1.205 + surely_finite_Ts = surely_finite_Ts |> insert_type thy I T,
1.206 + maybe_infinite_Ts = maybe_infinite_Ts,
1.207 + surely_infinite_Ts = surely_infinite_Ts,
1.208 + maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
1.209 + else
1.210 + {maybe_finite_Ts = maybe_finite_Ts,
1.211 + surely_finite_Ts = surely_finite_Ts,
1.212 + maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv thy) T,
1.213 + surely_infinite_Ts = surely_infinite_Ts,
1.214 + maybe_nonmono_Ts = maybe_nonmono_Ts}
1.215 + | _ => mono
1.216 + else
1.217 + mono
1.218 + end
1.219 | add_iterm_mononotonicity_info _ _ _ _ mono = mono
1.220 fun add_fact_mononotonicity_info ctxt level
1.221 ({kind, iformula, ...} : translated_formula) =
1.222 @@ -2210,9 +2216,10 @@
1.223
1.224 fun add_iformula_monotonic_types ctxt mono type_enc =
1.225 let
1.226 + val thy = Proof_Context.theory_of ctxt
1.227 val level = level_of_type_enc type_enc
1.228 val should_encode = should_encode_type ctxt mono level
1.229 - fun add_type T = not (should_encode T) ? insert_type ctxt I T
1.230 + fun add_type T = not (should_encode T) ? insert_type thy I T
1.231 fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
1.232 | add_args _ = I
1.233 and add_term tm = add_type (ityp_of tm) #> add_args tm
1.234 @@ -2360,12 +2367,12 @@
1.235
1.236 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
1.237
1.238 -fun rationalize_decls ctxt (decls as decl :: (decls' as _ :: _)) =
1.239 +fun rationalize_decls thy (decls as decl :: (decls' as _ :: _)) =
1.240 let
1.241 val T = result_type_of_decl decl
1.242 |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
1.243 in
1.244 - if forall (type_generalization ctxt T o result_type_of_decl) decls' then
1.245 + if forall (type_generalization thy T o result_type_of_decl) decls' then
1.246 [decl]
1.247 else
1.248 decls
1.249 @@ -2378,7 +2385,8 @@
1.250 Simple_Types _ => [decl_line_for_sym ctxt format mono type_enc s (hd decls)]
1.251 | Guards (_, level) =>
1.252 let
1.253 - val decls = decls |> rationalize_decls ctxt
1.254 + val thy = Proof_Context.theory_of ctxt
1.255 + val decls = decls |> rationalize_decls thy
1.256 val n = length decls
1.257 val decls =
1.258 decls |> filter (should_encode_type ctxt mono level
1.259 @@ -2517,10 +2525,9 @@
1.260
1.261 fun undeclared_syms_in_problem type_enc problem =
1.262 let
1.263 - val declared = declared_syms_in_problem problem
1.264 fun do_sym (name as (s, _)) ty =
1.265 - if is_tptp_user_symbol s andalso not (member (op =) declared name) then
1.266 - AList.default (op =) (name, ty)
1.267 + if is_tptp_user_symbol s then
1.268 + Symtab.default (s, (name, ty))
1.269 else
1.270 I
1.271 fun do_type (AType (name, tys)) =
1.272 @@ -2539,17 +2546,19 @@
1.273 fun do_problem_line (Decl (_, _, ty)) = do_type ty
1.274 | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
1.275 in
1.276 - fold (fold do_problem_line o snd) problem []
1.277 - |> filter_out (is_built_in_tptp_symbol o fst o fst)
1.278 + Symtab.empty
1.279 + |> fold (fn (s, _) => Symtab.default (s, (("", ""), K tvar_a_atype)))
1.280 + (declared_syms_in_problem problem)
1.281 + |> fold (fold do_problem_line o snd) problem
1.282 end
1.283
1.284 fun declare_undeclared_syms_in_atp_problem type_enc problem =
1.285 let
1.286 val decls =
1.287 - problem
1.288 - |> undeclared_syms_in_problem type_enc
1.289 - |> sort_wrt (fst o fst)
1.290 - |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ()))
1.291 + Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
1.292 + | (s, (sym, ty)) =>
1.293 + cons (Decl (type_decl_prefix ^ s, sym, ty ())))
1.294 + (undeclared_syms_in_problem type_enc problem) []
1.295 in (implicit_declsN, decls) :: problem end
1.296
1.297 fun exists_subdtype P =
1.298 @@ -2622,7 +2631,7 @@
1.299 conj_sym_kind mono type_enc uncurried_aliases sym_tab0 sym_tab
1.300 val sym_decl_lines =
1.301 (conjs, helpers @ facts, uncurried_alias_eq_tms)
1.302 - |> sym_decl_table_for_facts ctxt format type_enc sym_tab
1.303 + |> sym_decl_table_for_facts thy format type_enc sym_tab
1.304 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
1.305 type_enc mono_Ts
1.306 val num_facts = length facts