1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Fri Jul 01 15:53:37 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Fri Jul 01 15:53:38 2011 +0200
1.3 @@ -26,7 +26,7 @@
1.4 No_Types
1.5 datatype type_heaviness = Heavyweight | Lightweight
1.6
1.7 - datatype type_sys =
1.8 + datatype type_enc =
1.9 Simple_Types of order * type_level |
1.10 Preds of polymorphism * type_level * type_heaviness |
1.11 Tags of polymorphism * type_level * type_heaviness
1.12 @@ -75,12 +75,12 @@
1.13 val atp_irrelevant_consts : string list
1.14 val atp_schematic_consts_of : term -> typ list Symtab.table
1.15 val is_locality_global : locality -> bool
1.16 - val type_sys_from_string : string -> type_sys
1.17 - val polymorphism_of_type_sys : type_sys -> polymorphism
1.18 - val level_of_type_sys : type_sys -> type_level
1.19 - val is_type_sys_virtually_sound : type_sys -> bool
1.20 - val is_type_sys_fairly_sound : type_sys -> bool
1.21 - val choose_format : format list -> type_sys -> format * type_sys
1.22 + val type_enc_from_string : string -> type_enc
1.23 + val polymorphism_of_type_enc : type_enc -> polymorphism
1.24 + val level_of_type_enc : type_enc -> type_level
1.25 + val is_type_enc_virtually_sound : type_enc -> bool
1.26 + val is_type_enc_fairly_sound : type_enc -> bool
1.27 + val choose_format : format list -> type_enc -> format * type_enc
1.28 val mk_aconns :
1.29 connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
1.30 val unmangled_const : string -> string * string fo_term list
1.31 @@ -88,7 +88,7 @@
1.32 val helper_table : ((string * bool) * thm list) list
1.33 val factsN : string
1.34 val prepare_atp_problem :
1.35 - Proof.context -> format -> formula_kind -> formula_kind -> type_sys -> bool
1.36 + Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
1.37 -> bool -> bool -> bool -> term list -> term
1.38 -> ((string * locality) * term) list
1.39 -> string problem * string Symtab.table * int * int
1.40 @@ -509,7 +509,7 @@
1.41 No_Types
1.42 datatype type_heaviness = Heavyweight | Lightweight
1.43
1.44 -datatype type_sys =
1.45 +datatype type_enc =
1.46 Simple_Types of order * type_level |
1.47 Preds of polymorphism * type_level * type_heaviness |
1.48 Tags of polymorphism * type_level * type_heaviness
1.49 @@ -517,7 +517,7 @@
1.50 fun try_unsuffixes ss s =
1.51 fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
1.52
1.53 -fun type_sys_from_string s =
1.54 +fun type_enc_from_string s =
1.55 (case try (unprefix "poly_") s of
1.56 SOME s => (SOME Polymorphic, s)
1.57 | NONE =>
1.58 @@ -557,29 +557,29 @@
1.59 | _ => raise Same.SAME)
1.60 handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
1.61
1.62 -fun is_type_sys_higher_order (Simple_Types (Higher_Order, _)) = true
1.63 - | is_type_sys_higher_order _ = false
1.64 +fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true
1.65 + | is_type_enc_higher_order _ = false
1.66
1.67 -fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
1.68 - | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
1.69 - | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
1.70 +fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
1.71 + | polymorphism_of_type_enc (Preds (poly, _, _)) = poly
1.72 + | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
1.73
1.74 -fun level_of_type_sys (Simple_Types (_, level)) = level
1.75 - | level_of_type_sys (Preds (_, level, _)) = level
1.76 - | level_of_type_sys (Tags (_, level, _)) = level
1.77 +fun level_of_type_enc (Simple_Types (_, level)) = level
1.78 + | level_of_type_enc (Preds (_, level, _)) = level
1.79 + | level_of_type_enc (Tags (_, level, _)) = level
1.80
1.81 -fun heaviness_of_type_sys (Simple_Types _) = Heavyweight
1.82 - | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness
1.83 - | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness
1.84 +fun heaviness_of_type_enc (Simple_Types _) = Heavyweight
1.85 + | heaviness_of_type_enc (Preds (_, _, heaviness)) = heaviness
1.86 + | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness
1.87
1.88 fun is_type_level_virtually_sound level =
1.89 level = All_Types orelse level = Noninf_Nonmono_Types
1.90 -val is_type_sys_virtually_sound =
1.91 - is_type_level_virtually_sound o level_of_type_sys
1.92 +val is_type_enc_virtually_sound =
1.93 + is_type_level_virtually_sound o level_of_type_enc
1.94
1.95 fun is_type_level_fairly_sound level =
1.96 is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
1.97 -val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
1.98 +val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
1.99
1.100 fun choose_format formats (Simple_Types (order, level)) =
1.101 if member (op =) formats THF then
1.102 @@ -588,15 +588,15 @@
1.103 (TFF, Simple_Types (First_Order, level))
1.104 else
1.105 choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
1.106 - | choose_format formats type_sys =
1.107 + | choose_format formats type_enc =
1.108 (case hd formats of
1.109 CNF_UEQ =>
1.110 - (CNF_UEQ, case type_sys of
1.111 + (CNF_UEQ, case type_enc of
1.112 Preds stuff =>
1.113 - (if is_type_sys_fairly_sound type_sys then Tags else Preds)
1.114 + (if is_type_enc_fairly_sound type_enc then Tags else Preds)
1.115 stuff
1.116 - | _ => type_sys)
1.117 - | format => (format, type_sys))
1.118 + | _ => type_enc)
1.119 + | format => (format, type_enc))
1.120
1.121 type translated_formula =
1.122 {name : string,
1.123 @@ -628,30 +628,30 @@
1.124
1.125 fun should_drop_arg_type_args (Simple_Types _) =
1.126 false (* since TFF doesn't support overloading *)
1.127 - | should_drop_arg_type_args type_sys =
1.128 - level_of_type_sys type_sys = All_Types andalso
1.129 - heaviness_of_type_sys type_sys = Heavyweight
1.130 + | should_drop_arg_type_args type_enc =
1.131 + level_of_type_enc type_enc = All_Types andalso
1.132 + heaviness_of_type_enc type_enc = Heavyweight
1.133
1.134 fun general_type_arg_policy (Tags (_, All_Types, Heavyweight)) = No_Type_Args
1.135 - | general_type_arg_policy type_sys =
1.136 - if level_of_type_sys type_sys = No_Types then
1.137 + | general_type_arg_policy type_enc =
1.138 + if level_of_type_enc type_enc = No_Types then
1.139 No_Type_Args
1.140 - else if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
1.141 - Mangled_Type_Args (should_drop_arg_type_args type_sys)
1.142 + else if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
1.143 + Mangled_Type_Args (should_drop_arg_type_args type_enc)
1.144 else
1.145 - Explicit_Type_Args (should_drop_arg_type_args type_sys)
1.146 + Explicit_Type_Args (should_drop_arg_type_args type_enc)
1.147
1.148 -fun type_arg_policy type_sys s =
1.149 +fun type_arg_policy type_enc s =
1.150 if s = @{const_name HOL.eq} orelse
1.151 - (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
1.152 + (s = app_op_name andalso level_of_type_enc type_enc = Const_Arg_Types) then
1.153 No_Type_Args
1.154 else if s = type_tag_name then
1.155 - (if polymorphism_of_type_sys type_sys = Mangled_Monomorphic then
1.156 + (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
1.157 Mangled_Type_Args
1.158 else
1.159 Explicit_Type_Args) false
1.160 else
1.161 - general_type_arg_policy type_sys
1.162 + general_type_arg_policy type_enc
1.163
1.164 (*Make literals for sorted type variables*)
1.165 fun generic_add_sorts_on_type (_, []) = I
1.166 @@ -669,8 +669,8 @@
1.167 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
1.168 | add_sorts_on_tvar _ = I
1.169
1.170 -fun type_literals_for_types type_sys add_sorts_on_typ Ts =
1.171 - [] |> level_of_type_sys type_sys <> No_Types ? fold add_sorts_on_typ Ts
1.172 +fun type_literals_for_types type_enc add_sorts_on_typ Ts =
1.173 + [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
1.174
1.175 fun mk_aconns c phis =
1.176 let val (phis', phi') = split_last phis in
1.177 @@ -705,10 +705,10 @@
1.178 val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
1.179 val homo_infinite_type = Type (homo_infinite_type_name, [])
1.180
1.181 -fun fo_term_from_typ format type_sys =
1.182 +fun fo_term_from_typ format type_enc =
1.183 let
1.184 fun term (Type (s, Ts)) =
1.185 - ATerm (case (is_type_sys_higher_order type_sys, s) of
1.186 + ATerm (case (is_type_enc_higher_order type_enc, s) of
1.187 (true, @{type_name bool}) => `I tptp_bool_type
1.188 | (true, @{type_name fun}) => `I tptp_fun_type
1.189 | _ => if s = homo_infinite_type_name andalso
1.190 @@ -722,8 +722,8 @@
1.191 ATerm ((make_schematic_type_var x, s), [])
1.192 in term end
1.193
1.194 -fun fo_term_for_type_arg format type_sys T =
1.195 - if T = dummyT then NONE else SOME (fo_term_from_typ format type_sys T)
1.196 +fun fo_term_for_type_arg format type_enc T =
1.197 + if T = dummyT then NONE else SOME (fo_term_from_typ format type_enc T)
1.198
1.199 (* This shouldn't clash with anything else. *)
1.200 val mangled_type_sep = "\000"
1.201 @@ -742,7 +742,7 @@
1.202 else
1.203 simple_type_prefix ^ ascii_of s
1.204
1.205 -fun ho_type_from_fo_term type_sys pred_sym ary =
1.206 +fun ho_type_from_fo_term type_enc pred_sym ary =
1.207 let
1.208 fun to_atype ty =
1.209 AType ((make_simple_type (generic_mangled_type_name fst ty),
1.210 @@ -752,15 +752,15 @@
1.211 | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
1.212 fun to_ho (ty as ATerm ((s, _), tys)) =
1.213 if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
1.214 - in if is_type_sys_higher_order type_sys then to_ho else to_fo ary end
1.215 + in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
1.216
1.217 -fun mangled_type format type_sys pred_sym ary =
1.218 - ho_type_from_fo_term type_sys pred_sym ary
1.219 - o fo_term_from_typ format type_sys
1.220 +fun mangled_type format type_enc pred_sym ary =
1.221 + ho_type_from_fo_term type_enc pred_sym ary
1.222 + o fo_term_from_typ format type_enc
1.223
1.224 -fun mangled_const_name format type_sys T_args (s, s') =
1.225 +fun mangled_const_name format type_enc T_args (s, s') =
1.226 let
1.227 - val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_sys)
1.228 + val ty_args = T_args |> map_filter (fo_term_for_type_arg format type_enc)
1.229 fun type_suffix f g =
1.230 fold_rev (curry (op ^) o g o prefix mangled_type_sep
1.231 o generic_mangled_type_name f) ty_args ""
1.232 @@ -789,14 +789,14 @@
1.233 (hd ss, map unmangled_type (tl ss))
1.234 end
1.235
1.236 -fun introduce_proxies type_sys =
1.237 +fun introduce_proxies type_enc =
1.238 let
1.239 fun intro top_level (CombApp (tm1, tm2)) =
1.240 CombApp (intro top_level tm1, intro false tm2)
1.241 | intro top_level (CombConst (name as (s, _), T, T_args)) =
1.242 (case proxify_const s of
1.243 SOME proxy_base =>
1.244 - if top_level orelse is_type_sys_higher_order type_sys then
1.245 + if top_level orelse is_type_enc_higher_order type_enc then
1.246 case (top_level, s) of
1.247 (_, "c_False") => (`I tptp_false, [])
1.248 | (_, "c_True") => (`I tptp_true, [])
1.249 @@ -815,11 +815,11 @@
1.250 | intro _ tm = tm
1.251 in intro true end
1.252
1.253 -fun combformula_from_prop thy type_sys eq_as_iff =
1.254 +fun combformula_from_prop thy type_enc eq_as_iff =
1.255 let
1.256 fun do_term bs t atomic_types =
1.257 combterm_from_term thy bs (Envir.eta_contract t)
1.258 - |>> (introduce_proxies type_sys #> AAtom)
1.259 + |>> (introduce_proxies type_enc #> AAtom)
1.260 ||> union (op =) atomic_types
1.261 fun do_quant bs q s T t' =
1.262 let val s = singleton (Name.variant_list (map fst bs)) s in
1.263 @@ -940,27 +940,27 @@
1.264 end
1.265
1.266 (* making fact and conjecture formulas *)
1.267 -fun make_formula thy type_sys eq_as_iff name loc kind t =
1.268 +fun make_formula thy type_enc eq_as_iff name loc kind t =
1.269 let
1.270 val (combformula, atomic_types) =
1.271 - combformula_from_prop thy type_sys eq_as_iff t []
1.272 + combformula_from_prop thy type_enc eq_as_iff t []
1.273 in
1.274 {name = name, locality = loc, kind = kind, combformula = combformula,
1.275 atomic_types = atomic_types}
1.276 end
1.277
1.278 -fun make_fact ctxt format type_sys eq_as_iff preproc presimp_consts
1.279 +fun make_fact ctxt format type_enc eq_as_iff preproc presimp_consts
1.280 ((name, loc), t) =
1.281 let val thy = Proof_Context.theory_of ctxt in
1.282 case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
1.283 - |> make_formula thy type_sys (eq_as_iff andalso format <> CNF) name
1.284 + |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
1.285 loc Axiom of
1.286 formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
1.287 if s = tptp_true then NONE else SOME formula
1.288 | formula => SOME formula
1.289 end
1.290
1.291 -fun make_conjecture ctxt format prem_kind type_sys preproc presimp_consts ts =
1.292 +fun make_conjecture ctxt format prem_kind type_enc preproc presimp_consts ts =
1.293 let
1.294 val thy = Proof_Context.theory_of ctxt
1.295 val last = length ts - 1
1.296 @@ -977,7 +977,7 @@
1.297 in
1.298 t |> preproc ?
1.299 (preprocess_prop ctxt presimp_consts kind #> freeze_term)
1.300 - |> make_formula thy type_sys (format <> CNF) (string_of_int j)
1.301 + |> make_formula thy type_enc (format <> CNF) (string_of_int j)
1.302 Local kind
1.303 |> maybe_negate
1.304 end)
1.305 @@ -1231,7 +1231,7 @@
1.306 end
1.307 handle TYPE _ => T_args
1.308
1.309 -fun enforce_type_arg_policy_in_combterm ctxt format type_sys =
1.310 +fun enforce_type_arg_policy_in_combterm ctxt format type_enc =
1.311 let
1.312 val thy = Proof_Context.theory_of ctxt
1.313 fun aux arity (CombApp (tm1, tm2)) =
1.314 @@ -1245,11 +1245,11 @@
1.315 fun filtered_T_args false = T_args
1.316 | filtered_T_args true = filter_type_args thy s'' arity T_args
1.317 in
1.318 - case type_arg_policy type_sys s'' of
1.319 + case type_arg_policy type_enc s'' of
1.320 Explicit_Type_Args drop_args =>
1.321 (name, filtered_T_args drop_args)
1.322 | Mangled_Type_Args drop_args =>
1.323 - (mangled_const_name format type_sys (filtered_T_args drop_args)
1.324 + (mangled_const_name format type_enc (filtered_T_args drop_args)
1.325 name, [])
1.326 | No_Type_Args => (name, [])
1.327 end)
1.328 @@ -1257,14 +1257,14 @@
1.329 | aux _ tm = tm
1.330 in aux 0 end
1.331
1.332 -fun repair_combterm ctxt format type_sys sym_tab =
1.333 - not (is_type_sys_higher_order type_sys)
1.334 +fun repair_combterm ctxt format type_enc sym_tab =
1.335 + not (is_type_enc_higher_order type_enc)
1.336 ? (introduce_explicit_apps_in_combterm sym_tab
1.337 #> introduce_predicators_in_combterm sym_tab)
1.338 - #> enforce_type_arg_policy_in_combterm ctxt format type_sys
1.339 -fun repair_fact ctxt format type_sys sym_tab =
1.340 + #> enforce_type_arg_policy_in_combterm ctxt format type_enc
1.341 +fun repair_fact ctxt format type_enc sym_tab =
1.342 update_combformula (formula_map
1.343 - (repair_combterm ctxt format type_sys sym_tab))
1.344 + (repair_combterm ctxt format type_enc sym_tab))
1.345
1.346 (** Helper facts **)
1.347
1.348 @@ -1313,12 +1313,12 @@
1.349 |> close_formula_universally, simp_info, NONE)
1.350 end
1.351
1.352 -fun should_specialize_helper type_sys t =
1.353 - case general_type_arg_policy type_sys of
1.354 +fun should_specialize_helper type_enc t =
1.355 + case general_type_arg_policy type_enc of
1.356 Mangled_Type_Args _ => not (null (Term.hidden_polymorphism t))
1.357 | _ => false
1.358
1.359 -fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
1.360 +fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
1.361 case strip_prefix_and_unascii const_prefix s of
1.362 SOME mangled_s =>
1.363 let
1.364 @@ -1331,14 +1331,14 @@
1.365 else untyped_helper_suffix),
1.366 Helper),
1.367 let val t = th |> prop_of in
1.368 - t |> should_specialize_helper type_sys t
1.369 + t |> should_specialize_helper type_enc t
1.370 ? (case types of
1.371 [T] => specialize_type thy (invert_const unmangled_s, T)
1.372 | _ => I)
1.373 end)
1.374 val make_facts =
1.375 - map_filter (make_fact ctxt format type_sys false false [])
1.376 - val fairly_sound = is_type_sys_fairly_sound type_sys
1.377 + map_filter (make_fact ctxt format type_enc false false [])
1.378 + val fairly_sound = is_type_enc_fairly_sound type_enc
1.379 in
1.380 helper_table
1.381 |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
1.382 @@ -1351,8 +1351,8 @@
1.383 |> make_facts)
1.384 end
1.385 | NONE => []
1.386 -fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
1.387 - Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_sys) sym_tab
1.388 +fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
1.389 + Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
1.390 []
1.391
1.392 (***************************************************************)
1.393 @@ -1393,13 +1393,13 @@
1.394 fun type_constrs_of_terms thy ts =
1.395 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
1.396
1.397 -fun translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
1.398 +fun translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
1.399 facts =
1.400 let
1.401 val thy = Proof_Context.theory_of ctxt
1.402 val fact_ts = facts |> map snd
1.403 val presimp_consts = Meson.presimplified_consts ctxt
1.404 - val make_fact = make_fact ctxt format type_sys true preproc presimp_consts
1.405 + val make_fact = make_fact ctxt format type_enc true preproc presimp_consts
1.406 val (facts, fact_names) =
1.407 facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
1.408 |> map_filter (try (apfst the))
1.409 @@ -1416,9 +1416,9 @@
1.410 val tycons = type_constrs_of_terms thy all_ts
1.411 val conjs =
1.412 hyp_ts @ [concl_t]
1.413 - |> make_conjecture ctxt format prem_kind type_sys preproc presimp_consts
1.414 + |> make_conjecture ctxt format prem_kind type_enc preproc presimp_consts
1.415 val (supers', arity_clauses) =
1.416 - if level_of_type_sys type_sys = No_Types then ([], [])
1.417 + if level_of_type_enc type_enc = No_Types then ([], [])
1.418 else make_arity_clauses thy tycons supers
1.419 val class_rel_clauses = make_class_rel_clauses thy subs supers'
1.420 in
1.421 @@ -1434,9 +1434,9 @@
1.422
1.423 val type_pred = `make_fixed_const type_pred_name
1.424
1.425 -fun type_pred_combterm ctxt format type_sys T tm =
1.426 +fun type_pred_combterm ctxt format type_enc T tm =
1.427 CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
1.428 - |> enforce_type_arg_policy_in_combterm ctxt format type_sys, tm)
1.429 + |> enforce_type_arg_policy_in_combterm ctxt format type_enc, tm)
1.430
1.431 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
1.432 | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
1.433 @@ -1445,15 +1445,15 @@
1.434 formula_fold pos (is_var_positively_naked_in_term name) phi false
1.435 | should_predicate_on_var_in_formula _ _ _ _ = true
1.436
1.437 -fun mk_const_aterm format type_sys x T_args args =
1.438 - ATerm (x, map_filter (fo_term_for_type_arg format type_sys) T_args @ args)
1.439 +fun mk_const_aterm format type_enc x T_args args =
1.440 + ATerm (x, map_filter (fo_term_for_type_arg format type_enc) T_args @ args)
1.441
1.442 -fun tag_with_type ctxt format nonmono_Ts type_sys pos T tm =
1.443 +fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
1.444 CombConst (type_tag, T --> T, [T])
1.445 - |> enforce_type_arg_policy_in_combterm ctxt format type_sys
1.446 - |> term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
1.447 + |> enforce_type_arg_policy_in_combterm ctxt format type_enc
1.448 + |> term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
1.449 |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
1.450 -and term_from_combterm ctxt format nonmono_Ts type_sys =
1.451 +and term_from_combterm ctxt format nonmono_Ts type_enc =
1.452 let
1.453 fun aux site u =
1.454 let
1.455 @@ -1469,32 +1469,32 @@
1.456 (pos, if is_tptp_equal s then Eq_Arg pos else Elsewhere)
1.457 | Eq_Arg pos => (pos, Elsewhere)
1.458 | Elsewhere => (NONE, Elsewhere)
1.459 - val t = mk_const_aterm format type_sys x T_args
1.460 + val t = mk_const_aterm format type_enc x T_args
1.461 (map (aux arg_site) args)
1.462 val T = combtyp_of u
1.463 in
1.464 - t |> (if should_tag_with_type ctxt nonmono_Ts type_sys site u T then
1.465 - tag_with_type ctxt format nonmono_Ts type_sys pos T
1.466 + t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then
1.467 + tag_with_type ctxt format nonmono_Ts type_enc pos T
1.468 else
1.469 I)
1.470 end
1.471 in aux end
1.472 -and formula_from_combformula ctxt format nonmono_Ts type_sys
1.473 +and formula_from_combformula ctxt format nonmono_Ts type_enc
1.474 should_predicate_on_var =
1.475 let
1.476 fun do_term pos =
1.477 - term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
1.478 + term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
1.479 val do_bound_type =
1.480 - case type_sys of
1.481 + case type_enc of
1.482 Simple_Types (_, level) =>
1.483 homogenized_type ctxt nonmono_Ts level 0
1.484 - #> mangled_type format type_sys false 0 #> SOME
1.485 + #> mangled_type format type_enc false 0 #> SOME
1.486 | _ => K NONE
1.487 fun do_out_of_bound_type pos phi universal (name, T) =
1.488 - if should_predicate_on_type ctxt nonmono_Ts type_sys
1.489 + if should_predicate_on_type ctxt nonmono_Ts type_enc
1.490 (fn () => should_predicate_on_var pos phi universal name) T then
1.491 CombVar (name, T)
1.492 - |> type_pred_combterm ctxt format type_sys T
1.493 + |> type_pred_combterm ctxt format type_enc T
1.494 |> do_term pos |> AAtom |> SOME
1.495 else
1.496 NONE
1.497 @@ -1517,23 +1517,23 @@
1.498 | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
1.499 in do_formula end
1.500
1.501 -fun bound_tvars type_sys Ts =
1.502 +fun bound_tvars type_enc Ts =
1.503 mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
1.504 - (type_literals_for_types type_sys add_sorts_on_tvar Ts))
1.505 + (type_literals_for_types type_enc add_sorts_on_tvar Ts))
1.506
1.507 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
1.508 of monomorphization). The TPTP explicitly forbids name clashes, and some of
1.509 the remote provers might care. *)
1.510 fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
1.511 - type_sys (j, {name, locality, kind, combformula, atomic_types}) =
1.512 + type_enc (j, {name, locality, kind, combformula, atomic_types}) =
1.513 (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name,
1.514 kind,
1.515 combformula
1.516 |> close_combformula_universally
1.517 - |> formula_from_combformula ctxt format nonmono_Ts type_sys
1.518 + |> formula_from_combformula ctxt format nonmono_Ts type_enc
1.519 should_predicate_on_var_in_formula
1.520 (if pos then SOME true else NONE)
1.521 - |> bound_tvars type_sys atomic_types
1.522 + |> bound_tvars type_enc atomic_types
1.523 |> close_formula_universally,
1.524 NONE,
1.525 case locality of
1.526 @@ -1566,45 +1566,45 @@
1.527 (fo_literal_from_arity_literal concl_lits))
1.528 |> close_formula_universally, intro_info, NONE)
1.529
1.530 -fun formula_line_for_conjecture ctxt format nonmono_Ts type_sys
1.531 +fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc
1.532 ({name, kind, combformula, atomic_types, ...} : translated_formula) =
1.533 Formula (conjecture_prefix ^ name, kind,
1.534 - formula_from_combformula ctxt format nonmono_Ts type_sys
1.535 + formula_from_combformula ctxt format nonmono_Ts type_enc
1.536 should_predicate_on_var_in_formula (SOME false)
1.537 (close_combformula_universally combformula)
1.538 - |> bound_tvars type_sys atomic_types
1.539 + |> bound_tvars type_enc atomic_types
1.540 |> close_formula_universally, NONE, NONE)
1.541
1.542 -fun free_type_literals type_sys ({atomic_types, ...} : translated_formula) =
1.543 - atomic_types |> type_literals_for_types type_sys add_sorts_on_tfree
1.544 +fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) =
1.545 + atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree
1.546 |> map fo_literal_from_type_literal
1.547
1.548 fun formula_line_for_free_type j lit =
1.549 Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
1.550 formula_from_fo_literal lit, NONE, NONE)
1.551 -fun formula_lines_for_free_types type_sys facts =
1.552 +fun formula_lines_for_free_types type_enc facts =
1.553 let
1.554 - val litss = map (free_type_literals type_sys) facts
1.555 + val litss = map (free_type_literals type_enc) facts
1.556 val lits = fold (union (op =)) litss []
1.557 in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
1.558
1.559 (** Symbol declarations **)
1.560
1.561 -fun should_declare_sym type_sys pred_sym s =
1.562 +fun should_declare_sym type_enc pred_sym s =
1.563 is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso
1.564 - (case type_sys of
1.565 + (case type_enc of
1.566 Simple_Types _ => true
1.567 | Tags (_, _, Lightweight) => true
1.568 | _ => not pred_sym)
1.569
1.570 -fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) =
1.571 +fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) =
1.572 let
1.573 fun add_combterm in_conj tm =
1.574 let val (head, args) = strip_combterm_comb tm in
1.575 (case head of
1.576 CombConst ((s, s'), T, T_args) =>
1.577 let val pred_sym = is_pred_sym repaired_sym_tab s in
1.578 - if should_declare_sym type_sys pred_sym s then
1.579 + if should_declare_sym type_enc pred_sym s then
1.580 Symtab.map_default (s, [])
1.581 (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
1.582 in_conj))
1.583 @@ -1618,7 +1618,7 @@
1.584 fact_lift (formula_fold NONE (K (add_combterm in_conj)))
1.585 in
1.586 Symtab.empty
1.587 - |> is_type_sys_fairly_sound type_sys
1.588 + |> is_type_enc_fairly_sound type_enc
1.589 ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
1.590 end
1.591
1.592 @@ -1641,8 +1641,8 @@
1.593 formula_fold (SOME (kind <> Conjecture))
1.594 (add_combterm_nonmonotonic_types ctxt level sound locality)
1.595 combformula
1.596 -fun nonmonotonic_types_for_facts ctxt type_sys sound facts =
1.597 - let val level = level_of_type_sys type_sys in
1.598 +fun nonmonotonic_types_for_facts ctxt type_enc sound facts =
1.599 + let val level = level_of_type_enc type_enc in
1.600 if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
1.601 [] |> fold (add_fact_nonmonotonic_types ctxt level sound) facts
1.602 (* We must add "bool" in case the helper "True_or_False" is added
1.603 @@ -1653,21 +1653,21 @@
1.604 []
1.605 end
1.606
1.607 -fun decl_line_for_sym ctxt format nonmono_Ts type_sys s
1.608 +fun decl_line_for_sym ctxt format nonmono_Ts type_enc s
1.609 (s', T_args, T, pred_sym, ary, _) =
1.610 let
1.611 val (T_arg_Ts, level) =
1.612 - case type_sys of
1.613 + case type_enc of
1.614 Simple_Types (_, level) => ([], level)
1.615 | _ => (replicate (length T_args) homo_infinite_type, No_Types)
1.616 in
1.617 Decl (sym_decl_prefix ^ s, (s, s'),
1.618 (T_arg_Ts ---> (T |> homogenized_type ctxt nonmono_Ts level ary))
1.619 - |> mangled_type format type_sys pred_sym (length T_arg_Ts + ary))
1.620 + |> mangled_type format type_enc pred_sym (length T_arg_Ts + ary))
1.621 end
1.622
1.623 fun formula_line_for_preds_sym_decl ctxt format conj_sym_kind nonmono_Ts
1.624 - poly_nonmono_Ts type_sys n s j (s', T_args, T, _, ary, in_conj) =
1.625 + poly_nonmono_Ts type_enc n s j (s', T_args, T, _, ary, in_conj) =
1.626 let
1.627 val (kind, maybe_negate) =
1.628 if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
1.629 @@ -1681,7 +1681,7 @@
1.630 val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args
1.631 fun should_keep_arg_type T =
1.632 sym_needs_arg_types orelse
1.633 - not (should_predicate_on_type ctxt nonmono_Ts type_sys (K false) T)
1.634 + not (should_predicate_on_type ctxt nonmono_Ts type_enc (K false) T)
1.635 val bound_Ts =
1.636 arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
1.637 in
1.638 @@ -1689,18 +1689,18 @@
1.639 (if n > 1 then "_" ^ string_of_int j else ""), kind,
1.640 CombConst ((s, s'), T, T_args)
1.641 |> fold (curry (CombApp o swap)) bounds
1.642 - |> type_pred_combterm ctxt format type_sys res_T
1.643 + |> type_pred_combterm ctxt format type_enc res_T
1.644 |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
1.645 - |> formula_from_combformula ctxt format poly_nonmono_Ts type_sys
1.646 + |> formula_from_combformula ctxt format poly_nonmono_Ts type_enc
1.647 (K (K (K (K true)))) (SOME true)
1.648 - |> n > 1 ? bound_tvars type_sys (atyps_of T)
1.649 + |> n > 1 ? bound_tvars type_enc (atyps_of T)
1.650 |> close_formula_universally
1.651 |> maybe_negate,
1.652 intro_info, NONE)
1.653 end
1.654
1.655 fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
1.656 - poly_nonmono_Ts type_sys n s
1.657 + poly_nonmono_Ts type_enc n s
1.658 (j, (s', T_args, T, pred_sym, ary, in_conj)) =
1.659 let
1.660 val ident_base =
1.661 @@ -1713,22 +1713,22 @@
1.662 val bound_names =
1.663 1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
1.664 val bounds = bound_names |> map (fn name => ATerm (name, []))
1.665 - val cst = mk_const_aterm format type_sys (s, s') T_args
1.666 + val cst = mk_const_aterm format type_enc (s, s') T_args
1.667 val atomic_Ts = atyps_of T
1.668 fun eq tms =
1.669 (if pred_sym then AConn (AIff, map AAtom tms)
1.670 else AAtom (ATerm (`I tptp_equal, tms)))
1.671 - |> bound_tvars type_sys atomic_Ts
1.672 + |> bound_tvars type_enc atomic_Ts
1.673 |> close_formula_universally
1.674 |> maybe_negate
1.675 (* See also "should_tag_with_type". *)
1.676 fun should_encode T =
1.677 should_encode_type ctxt poly_nonmono_Ts All_Types T orelse
1.678 - (case type_sys of
1.679 + (case type_enc of
1.680 Tags (Polymorphic, level, Lightweight) =>
1.681 level <> All_Types andalso Monomorph.typ_has_tvars T
1.682 | _ => false)
1.683 - val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_sys NONE
1.684 + val tag_with = tag_with_type ctxt format poly_nonmono_Ts type_enc NONE
1.685 val add_formula_for_res =
1.686 if should_encode res_T then
1.687 cons (Formula (ident_base ^ "_res", kind,
1.688 @@ -1757,10 +1757,10 @@
1.689 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
1.690
1.691 fun problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts
1.692 - poly_nonmono_Ts type_sys (s, decls) =
1.693 - case type_sys of
1.694 + poly_nonmono_Ts type_enc (s, decls) =
1.695 + case type_enc of
1.696 Simple_Types _ =>
1.697 - decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_sys s)
1.698 + decls |> map (decl_line_for_sym ctxt format nonmono_Ts type_enc s)
1.699 | Preds _ =>
1.700 let
1.701 val decls =
1.702 @@ -1776,13 +1776,13 @@
1.703 | _ => decls
1.704 val n = length decls
1.705 val decls =
1.706 - decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_sys
1.707 + decls |> filter (should_predicate_on_type ctxt poly_nonmono_Ts type_enc
1.708 (K true)
1.709 o result_type_of_decl)
1.710 in
1.711 (0 upto length decls - 1, decls)
1.712 |-> map2 (formula_line_for_preds_sym_decl ctxt format conj_sym_kind
1.713 - nonmono_Ts poly_nonmono_Ts type_sys n s)
1.714 + nonmono_Ts poly_nonmono_Ts type_enc n s)
1.715 end
1.716 | Tags (_, _, heaviness) =>
1.717 (case heaviness of
1.718 @@ -1791,17 +1791,17 @@
1.719 let val n = length decls in
1.720 (0 upto n - 1 ~~ decls)
1.721 |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
1.722 - conj_sym_kind poly_nonmono_Ts type_sys n s)
1.723 + conj_sym_kind poly_nonmono_Ts type_enc n s)
1.724 end)
1.725
1.726 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
1.727 - poly_nonmono_Ts type_sys sym_decl_tab =
1.728 + poly_nonmono_Ts type_enc sym_decl_tab =
1.729 sym_decl_tab
1.730 |> Symtab.dest
1.731 |> sort_wrt fst
1.732 |> rpair []
1.733 |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
1.734 - nonmono_Ts poly_nonmono_Ts type_sys)
1.735 + nonmono_Ts poly_nonmono_Ts type_enc)
1.736
1.737 fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
1.738 poly <> Mangled_Monomorphic andalso
1.739 @@ -1825,39 +1825,39 @@
1.740
1.741 val explicit_apply = NONE (* for experimental purposes *)
1.742
1.743 -fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_sys sound
1.744 +fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
1.745 exporter readable_names preproc hyp_ts concl_t facts =
1.746 let
1.747 - val (format, type_sys) = choose_format [format] type_sys
1.748 + val (format, type_enc) = choose_format [format] type_enc
1.749 val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
1.750 - translate_formulas ctxt format prem_kind type_sys preproc hyp_ts concl_t
1.751 + translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
1.752 facts
1.753 val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
1.754 val nonmono_Ts =
1.755 - conjs @ facts |> nonmonotonic_types_for_facts ctxt type_sys sound
1.756 - val repair = repair_fact ctxt format type_sys sym_tab
1.757 + conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc sound
1.758 + val repair = repair_fact ctxt format type_enc sym_tab
1.759 val (conjs, facts) = (conjs, facts) |> pairself (map repair)
1.760 val repaired_sym_tab =
1.761 conjs @ facts |> sym_table_for_facts ctxt (SOME false)
1.762 val helpers =
1.763 - repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
1.764 + repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
1.765 |> map repair
1.766 val poly_nonmono_Ts =
1.767 if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
1.768 - polymorphism_of_type_sys type_sys <> Polymorphic then
1.769 + polymorphism_of_type_enc type_enc <> Polymorphic then
1.770 nonmono_Ts
1.771 else
1.772 [TVar (("'a", 0), HOLogic.typeS)]
1.773 val sym_decl_lines =
1.774 (conjs, helpers @ facts)
1.775 - |> sym_decl_table_for_facts ctxt type_sys repaired_sym_tab
1.776 + |> sym_decl_table_for_facts ctxt type_enc repaired_sym_tab
1.777 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
1.778 - poly_nonmono_Ts type_sys
1.779 + poly_nonmono_Ts type_enc
1.780 val helper_lines =
1.781 0 upto length helpers - 1 ~~ helpers
1.782 |> map (formula_line_for_fact ctxt format helper_prefix I false true
1.783 - poly_nonmono_Ts type_sys)
1.784 - |> (if needs_type_tag_idempotence type_sys then
1.785 + poly_nonmono_Ts type_enc)
1.786 + |> (if needs_type_tag_idempotence type_enc then
1.787 cons (type_tag_idempotence_fact ())
1.788 else
1.789 I)
1.790 @@ -1868,15 +1868,15 @@
1.791 (factsN,
1.792 map (formula_line_for_fact ctxt format fact_prefix ascii_of
1.793 (not exporter) (not exporter) nonmono_Ts
1.794 - type_sys)
1.795 + type_enc)
1.796 (0 upto length facts - 1 ~~ facts)),
1.797 (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
1.798 (aritiesN, map formula_line_for_arity_clause arity_clauses),
1.799 (helpersN, helper_lines),
1.800 (conjsN,
1.801 - map (formula_line_for_conjecture ctxt format nonmono_Ts type_sys)
1.802 + map (formula_line_for_conjecture ctxt format nonmono_Ts type_enc)
1.803 conjs),
1.804 - (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
1.805 + (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
1.806 val problem =
1.807 problem
1.808 |> (case format of