1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Mar 27 16:59:13 2012 +0300
1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Mar 27 16:59:13 2012 +0300
1.3 @@ -125,7 +125,7 @@
1.4 (string * string) problem -> (string * string) problem
1.5 val filter_cnf_ueq_problem :
1.6 (string * string) problem -> (string * string) problem
1.7 - val declared_syms_in_problem : (string * ''a) problem -> (string * ''a) list
1.8 + val declared_syms_in_problem : 'a problem -> 'a list
1.9 val nice_atp_problem :
1.10 bool -> atp_format -> ('a * (string * string) problem_line list) list
1.11 -> ('a * string problem_line list) list
1.12 @@ -689,7 +689,7 @@
1.13
1.14 (** Symbol declarations **)
1.15
1.16 -fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = insert (op =) sym
1.17 +fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = cons sym
1.18 | add_declared_syms_in_problem_line _ = I
1.19 fun declared_syms_in_problem problem =
1.20 fold (fold add_declared_syms_in_problem_line o snd) problem []
1.21 @@ -785,9 +785,9 @@
1.22 if n < 2 orelse (n = 2 andalso String.sub (s, 0) = String.sub (s, 1)) orelse
1.23 String.isSubstring "_" s then
1.24 s
1.25 - else if s = "Dl" orelse s = "DL" then
1.26 + else if is_tptp_variable s then
1.27 (* "DL" appears to be a SPASS 3.7 keyword *)
1.28 - s ^ "_"
1.29 + if s = "DL" then s ^ "_" else s
1.30 else
1.31 String.substring (s, 0, n - 1) ^
1.32 String.str (Char.toUpper (String.sub (s, n - 1)))
2.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Mar 27 16:59:13 2012 +0300
2.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Mar 27 16:59:13 2012 +0300
2.3 @@ -131,8 +131,8 @@
2.4 val avoid_first_order_ghost_type_vars = false
2.5
2.6 val bound_var_prefix = "B_"
2.7 -val all_bound_var_prefix = "BA_"
2.8 -val exist_bound_var_prefix = "BE_"
2.9 +val all_bound_var_prefix = "A_"
2.10 +val exist_bound_var_prefix = "E_"
2.11 val schematic_var_prefix = "V_"
2.12 val fixed_var_prefix = "v_"
2.13 val tvar_prefix = "T_"
2.14 @@ -824,10 +824,10 @@
2.15
2.16 fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
2.17
2.18 -fun insert_type ctxt get_T x xs =
2.19 +fun insert_type thy get_T x xs =
2.20 let val T = get_T x in
2.21 - if exists (type_instance ctxt T o get_T) xs then xs
2.22 - else x :: filter_out (type_generalization ctxt T o get_T) xs
2.23 + if exists (type_instance thy T o get_T) xs then xs
2.24 + else x :: filter_out (type_generalization thy T o get_T) xs
2.25 end
2.26
2.27 (* The Booleans indicate whether all type arguments should be kept. *)
2.28 @@ -1342,20 +1342,24 @@
2.29 | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
2.30 maybe_nonmono_Ts, ...}
2.31 (Noninf_Nonmono_Types (strictness, grain)) T =
2.32 - grain = Ghost_Type_Arg_Vars orelse
2.33 - (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
2.34 - not (exists (type_instance ctxt T) surely_infinite_Ts orelse
2.35 - (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso
2.36 - is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
2.37 - T)))
2.38 + let val thy = Proof_Context.theory_of ctxt in
2.39 + grain = Ghost_Type_Arg_Vars orelse
2.40 + (exists (type_intersect thy T) maybe_nonmono_Ts andalso
2.41 + not (exists (type_instance thy T) surely_infinite_Ts orelse
2.42 + (not (member (type_equiv thy) maybe_finite_Ts T) andalso
2.43 + is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
2.44 + T)))
2.45 + end
2.46 | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
2.47 maybe_nonmono_Ts, ...}
2.48 (Fin_Nonmono_Types grain) T =
2.49 - grain = Ghost_Type_Arg_Vars orelse
2.50 - (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
2.51 - (exists (type_generalization ctxt T) surely_finite_Ts orelse
2.52 - (not (member (type_equiv ctxt) maybe_infinite_Ts T) andalso
2.53 - is_type_surely_finite ctxt T)))
2.54 + let val thy = Proof_Context.theory_of ctxt in
2.55 + grain = Ghost_Type_Arg_Vars orelse
2.56 + (exists (type_intersect thy T) maybe_nonmono_Ts andalso
2.57 + (exists (type_generalization thy T) surely_finite_Ts orelse
2.58 + (not (member (type_equiv thy) maybe_infinite_Ts T) andalso
2.59 + is_type_surely_finite ctxt T)))
2.60 + end
2.61 | should_encode_type _ _ _ _ = false
2.62
2.63 fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
2.64 @@ -1425,8 +1429,8 @@
2.65 fun consider_var_ary const_T var_T max_ary =
2.66 let
2.67 fun iter ary T =
2.68 - if ary = max_ary orelse type_instance ctxt var_T T orelse
2.69 - type_instance ctxt T var_T then
2.70 + if ary = max_ary orelse type_instance thy var_T T orelse
2.71 + type_instance thy T var_T then
2.72 ary
2.73 else
2.74 iter (ary + 1) (range_type T)
2.75 @@ -1445,7 +1449,7 @@
2.76 min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
2.77 max_ary = max_ary, types = types, in_conj = in_conj}
2.78 val fun_var_Ts' =
2.79 - fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
2.80 + fun_var_Ts |> can dest_funT T ? insert_type thy I T
2.81 in
2.82 if bool_vars' = bool_vars andalso
2.83 pointer_eq (fun_var_Ts', fun_var_Ts) then
2.84 @@ -1473,7 +1477,7 @@
2.85 let
2.86 val pred_sym =
2.87 pred_sym andalso top_level andalso not bool_vars
2.88 - val types' = types |> insert_type ctxt I T
2.89 + val types' = types |> insert_type thy I T
2.90 val in_conj = in_conj orelse conj_fact
2.91 val min_ary =
2.92 if (app_op_level = Sufficient_App_Op orelse
2.93 @@ -2070,7 +2074,7 @@
2.94 map (decl_line_for_class order) classes
2.95 | _ => []
2.96
2.97 -fun sym_decl_table_for_facts ctxt format type_enc sym_tab
2.98 +fun sym_decl_table_for_facts thy format type_enc sym_tab
2.99 (conjs, facts, extra_tms) =
2.100 let
2.101 fun add_iterm_syms tm =
2.102 @@ -2091,8 +2095,8 @@
2.103 in
2.104 if decl_sym then
2.105 Symtab.map_default (s, [])
2.106 - (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
2.107 - in_conj))
2.108 + (insert_type thy #3 (s', T_args, T, pred_sym, length args,
2.109 + in_conj))
2.110 else
2.111 I
2.112 end
2.113 @@ -2102,7 +2106,7 @@
2.114 end
2.115 val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> fact_lift
2.116 fun add_formula_var_types (AQuant (_, xs, phi)) =
2.117 - fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
2.118 + fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs
2.119 #> add_formula_var_types phi
2.120 | add_formula_var_types (AConn (_, phis)) =
2.121 fold add_formula_var_types phis
2.122 @@ -2119,12 +2123,12 @@
2.123 | _ => I)
2.124 in
2.125 Symtab.map_default (s, [])
2.126 - (insert_type ctxt #3 (s', [T], T, false, 0, false))
2.127 + (insert_type thy #3 (s', [T], T, false, 0, false))
2.128 end
2.129 fun add_TYPE_const () =
2.130 let val (s, s') = TYPE_name in
2.131 Symtab.map_default (s, [])
2.132 - (insert_type ctxt #3
2.133 + (insert_type thy #3
2.134 (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
2.135 end
2.136 in
2.137 @@ -2158,44 +2162,46 @@
2.138 (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
2.139 (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
2.140 surely_infinite_Ts, maybe_nonmono_Ts}) =
2.141 - if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
2.142 - case level of
2.143 - Noninf_Nonmono_Types (strictness, _) =>
2.144 - if exists (type_instance ctxt T) surely_infinite_Ts orelse
2.145 - member (type_equiv ctxt) maybe_finite_Ts T then
2.146 - mono
2.147 - else if is_type_kind_of_surely_infinite ctxt strictness
2.148 - surely_infinite_Ts T then
2.149 - {maybe_finite_Ts = maybe_finite_Ts,
2.150 - surely_finite_Ts = surely_finite_Ts,
2.151 - maybe_infinite_Ts = maybe_infinite_Ts,
2.152 - surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
2.153 - maybe_nonmono_Ts = maybe_nonmono_Ts}
2.154 - else
2.155 - {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv ctxt) T,
2.156 - surely_finite_Ts = surely_finite_Ts,
2.157 - maybe_infinite_Ts = maybe_infinite_Ts,
2.158 - surely_infinite_Ts = surely_infinite_Ts,
2.159 - maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
2.160 - | Fin_Nonmono_Types _ =>
2.161 - if exists (type_instance ctxt T) surely_finite_Ts orelse
2.162 - member (type_equiv ctxt) maybe_infinite_Ts T then
2.163 - mono
2.164 - else if is_type_surely_finite ctxt T then
2.165 - {maybe_finite_Ts = maybe_finite_Ts,
2.166 - surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T,
2.167 - maybe_infinite_Ts = maybe_infinite_Ts,
2.168 - surely_infinite_Ts = surely_infinite_Ts,
2.169 - maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
2.170 - else
2.171 - {maybe_finite_Ts = maybe_finite_Ts,
2.172 - surely_finite_Ts = surely_finite_Ts,
2.173 - maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv ctxt) T,
2.174 - surely_infinite_Ts = surely_infinite_Ts,
2.175 - maybe_nonmono_Ts = maybe_nonmono_Ts}
2.176 - | _ => mono
2.177 - else
2.178 - mono
2.179 + let val thy = Proof_Context.theory_of ctxt in
2.180 + if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
2.181 + case level of
2.182 + Noninf_Nonmono_Types (strictness, _) =>
2.183 + if exists (type_instance thy T) surely_infinite_Ts orelse
2.184 + member (type_equiv thy) maybe_finite_Ts T then
2.185 + mono
2.186 + else if is_type_kind_of_surely_infinite ctxt strictness
2.187 + surely_infinite_Ts T then
2.188 + {maybe_finite_Ts = maybe_finite_Ts,
2.189 + surely_finite_Ts = surely_finite_Ts,
2.190 + maybe_infinite_Ts = maybe_infinite_Ts,
2.191 + surely_infinite_Ts = surely_infinite_Ts |> insert_type thy I T,
2.192 + maybe_nonmono_Ts = maybe_nonmono_Ts}
2.193 + else
2.194 + {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv thy) T,
2.195 + surely_finite_Ts = surely_finite_Ts,
2.196 + maybe_infinite_Ts = maybe_infinite_Ts,
2.197 + surely_infinite_Ts = surely_infinite_Ts,
2.198 + maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
2.199 + | Fin_Nonmono_Types _ =>
2.200 + if exists (type_instance thy T) surely_finite_Ts orelse
2.201 + member (type_equiv thy) maybe_infinite_Ts T then
2.202 + mono
2.203 + else if is_type_surely_finite ctxt T then
2.204 + {maybe_finite_Ts = maybe_finite_Ts,
2.205 + surely_finite_Ts = surely_finite_Ts |> insert_type thy I T,
2.206 + maybe_infinite_Ts = maybe_infinite_Ts,
2.207 + surely_infinite_Ts = surely_infinite_Ts,
2.208 + maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
2.209 + else
2.210 + {maybe_finite_Ts = maybe_finite_Ts,
2.211 + surely_finite_Ts = surely_finite_Ts,
2.212 + maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv thy) T,
2.213 + surely_infinite_Ts = surely_infinite_Ts,
2.214 + maybe_nonmono_Ts = maybe_nonmono_Ts}
2.215 + | _ => mono
2.216 + else
2.217 + mono
2.218 + end
2.219 | add_iterm_mononotonicity_info _ _ _ _ mono = mono
2.220 fun add_fact_mononotonicity_info ctxt level
2.221 ({kind, iformula, ...} : translated_formula) =
2.222 @@ -2210,9 +2216,10 @@
2.223
2.224 fun add_iformula_monotonic_types ctxt mono type_enc =
2.225 let
2.226 + val thy = Proof_Context.theory_of ctxt
2.227 val level = level_of_type_enc type_enc
2.228 val should_encode = should_encode_type ctxt mono level
2.229 - fun add_type T = not (should_encode T) ? insert_type ctxt I T
2.230 + fun add_type T = not (should_encode T) ? insert_type thy I T
2.231 fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
2.232 | add_args _ = I
2.233 and add_term tm = add_type (ityp_of tm) #> add_args tm
2.234 @@ -2360,12 +2367,12 @@
2.235
2.236 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
2.237
2.238 -fun rationalize_decls ctxt (decls as decl :: (decls' as _ :: _)) =
2.239 +fun rationalize_decls thy (decls as decl :: (decls' as _ :: _)) =
2.240 let
2.241 val T = result_type_of_decl decl
2.242 |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
2.243 in
2.244 - if forall (type_generalization ctxt T o result_type_of_decl) decls' then
2.245 + if forall (type_generalization thy T o result_type_of_decl) decls' then
2.246 [decl]
2.247 else
2.248 decls
2.249 @@ -2378,7 +2385,8 @@
2.250 Simple_Types _ => [decl_line_for_sym ctxt format mono type_enc s (hd decls)]
2.251 | Guards (_, level) =>
2.252 let
2.253 - val decls = decls |> rationalize_decls ctxt
2.254 + val thy = Proof_Context.theory_of ctxt
2.255 + val decls = decls |> rationalize_decls thy
2.256 val n = length decls
2.257 val decls =
2.258 decls |> filter (should_encode_type ctxt mono level
2.259 @@ -2517,10 +2525,9 @@
2.260
2.261 fun undeclared_syms_in_problem type_enc problem =
2.262 let
2.263 - val declared = declared_syms_in_problem problem
2.264 fun do_sym (name as (s, _)) ty =
2.265 - if is_tptp_user_symbol s andalso not (member (op =) declared name) then
2.266 - AList.default (op =) (name, ty)
2.267 + if is_tptp_user_symbol s then
2.268 + Symtab.default (s, (name, ty))
2.269 else
2.270 I
2.271 fun do_type (AType (name, tys)) =
2.272 @@ -2539,17 +2546,19 @@
2.273 fun do_problem_line (Decl (_, _, ty)) = do_type ty
2.274 | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
2.275 in
2.276 - fold (fold do_problem_line o snd) problem []
2.277 - |> filter_out (is_built_in_tptp_symbol o fst o fst)
2.278 + Symtab.empty
2.279 + |> fold (fn (s, _) => Symtab.default (s, (("", ""), K tvar_a_atype)))
2.280 + (declared_syms_in_problem problem)
2.281 + |> fold (fold do_problem_line o snd) problem
2.282 end
2.283
2.284 fun declare_undeclared_syms_in_atp_problem type_enc problem =
2.285 let
2.286 val decls =
2.287 - problem
2.288 - |> undeclared_syms_in_problem type_enc
2.289 - |> sort_wrt (fst o fst)
2.290 - |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ()))
2.291 + Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
2.292 + | (s, (sym, ty)) =>
2.293 + cons (Decl (type_decl_prefix ^ s, sym, ty ())))
2.294 + (undeclared_syms_in_problem type_enc problem) []
2.295 in (implicit_declsN, decls) :: problem end
2.296
2.297 fun exists_subdtype P =
2.298 @@ -2622,7 +2631,7 @@
2.299 conj_sym_kind mono type_enc uncurried_aliases sym_tab0 sym_tab
2.300 val sym_decl_lines =
2.301 (conjs, helpers @ facts, uncurried_alias_eq_tms)
2.302 - |> sym_decl_table_for_facts ctxt format type_enc sym_tab
2.303 + |> sym_decl_table_for_facts thy format type_enc sym_tab
2.304 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
2.305 type_enc mono_Ts
2.306 val num_facts = length facts
3.1 --- a/src/HOL/Tools/ATP/atp_util.ML Tue Mar 27 16:59:13 2012 +0300
3.2 +++ b/src/HOL/Tools/ATP/atp_util.ML Tue Mar 27 16:59:13 2012 +0300
3.3 @@ -16,10 +16,10 @@
3.4 val maybe_quote : string -> string
3.5 val string_from_ext_time : bool * Time.time -> string
3.6 val string_from_time : Time.time -> string
3.7 - val type_instance : Proof.context -> typ -> typ -> bool
3.8 - val type_generalization : Proof.context -> typ -> typ -> bool
3.9 - val type_intersect : Proof.context -> typ -> typ -> bool
3.10 - val type_equiv : Proof.context -> typ * typ -> bool
3.11 + val type_instance : theory -> typ -> typ -> bool
3.12 + val type_generalization : theory -> typ -> typ -> bool
3.13 + val type_intersect : theory -> typ -> typ -> bool
3.14 + val type_equiv : theory -> typ * typ -> bool
3.15 val varify_type : Proof.context -> typ -> typ
3.16 val instantiate_type : theory -> typ -> typ -> typ -> typ
3.17 val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
3.18 @@ -123,14 +123,12 @@
3.19
3.20 val string_from_time = string_from_ext_time o pair false
3.21
3.22 -fun type_instance ctxt T T' =
3.23 - Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T')
3.24 -fun type_generalization ctxt T T' = type_instance ctxt T' T
3.25 -fun type_intersect ctxt T T' =
3.26 - can (Sign.typ_unify (Proof_Context.theory_of ctxt)
3.27 - (T, Logic.incr_tvar (maxidx_of_typ T + 1) T'))
3.28 +fun type_instance thy T T' = Sign.typ_instance thy (T, T')
3.29 +fun type_generalization thy T T' = Sign.typ_instance thy (T', T)
3.30 +fun type_intersect thy T T' =
3.31 + can (Sign.typ_unify thy (T, Logic.incr_tvar (maxidx_of_typ T + 1) T'))
3.32 (Vartab.empty, 0)
3.33 -val type_equiv = Sign.typ_equiv o Proof_Context.theory_of
3.34 +val type_equiv = Sign.typ_equiv
3.35
3.36 fun varify_type ctxt T =
3.37 Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
3.38 @@ -177,7 +175,7 @@
3.39 fun aux slack avoid T =
3.40 if member (op =) avoid T then
3.41 0
3.42 - else case AList.lookup (type_equiv ctxt) assigns T of
3.43 + else case AList.lookup (type_equiv thy) assigns T of
3.44 SOME k => k
3.45 | NONE =>
3.46 case T of