1.1 --- a/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:40 2012 +0200
1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:40 2012 +0200
1.3 @@ -112,8 +112,10 @@
1.4 fun add_inferences_to_problem infers =
1.5 map (apsnd (map (add_inferences_to_problem_line infers)))
1.6
1.7 -fun ident_of_problem_line (Type_Decl (ident, _, _, _)) = ident
1.8 +fun ident_of_problem_line (Class_Decl (ident, _, _)) = ident
1.9 + | ident_of_problem_line (Type_Decl (ident, _, _)) = ident
1.10 | ident_of_problem_line (Sym_Decl (ident, _, _)) = ident
1.11 + | ident_of_problem_line (Class_Memb (ident, _, _, _)) = ident
1.12 | ident_of_problem_line (Formula (ident, _, _, _, _)) = ident
1.13
1.14 fun run_some_atp ctxt format problem =
2.1 --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200
2.3 @@ -45,8 +45,9 @@
2.4 datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
2.5 datatype 'a problem_line =
2.6 Class_Decl of string * 'a * 'a list |
2.7 - Type_Decl of string * 'a * int * 'a list |
2.8 + Type_Decl of string * 'a * int |
2.9 Sym_Decl of string * 'a * 'a ho_type |
2.10 + Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a |
2.11 Formula of string * formula_role
2.12 * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
2.13 * (string, string ho_type) ho_term option
2.14 @@ -178,8 +179,9 @@
2.15 datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
2.16 datatype 'a problem_line =
2.17 Class_Decl of string * 'a * 'a list |
2.18 - Type_Decl of string * 'a * int * 'a list |
2.19 + Type_Decl of string * 'a * int |
2.20 Sym_Decl of string * 'a * 'a ho_type |
2.21 + Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a |
2.22 Formula of string * formula_role
2.23 * ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
2.24 * (string, string ho_type) ho_term option
2.25 @@ -463,7 +465,7 @@
2.26
2.27 fun nary_type_decl_type n = funpow n (curry AFun atype_of_types) atype_of_types
2.28
2.29 -fun tptp_string_for_line format (Type_Decl (ident, ty, ary, _)) =
2.30 +fun tptp_string_for_line format (Type_Decl (ident, ty, ary)) =
2.31 tptp_string_for_line format (Sym_Decl (ident, ty, nary_type_decl_type ary))
2.32 | tptp_string_for_line format (Sym_Decl (ident, sym, ty)) =
2.33 tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^
2.34 @@ -551,6 +553,14 @@
2.35 strip_atype ty |> fst
2.36 |>> (fn [] => [] | ty_vars => ["[" ^ commas ty_vars ^ "]"])
2.37 in "predicate(" ^ commas (sym :: ty_vars @ map str_for_typ tys) ^ ")." end
2.38 + fun str_for_bound_tvar (ty, []) = ty
2.39 + | str_for_bound_tvar (ty, cls) = ty ^ " : " ^ commas cls
2.40 + fun sort_decl xs ty cl =
2.41 + "sort(" ^
2.42 + (if null xs then ""
2.43 + else "[" ^ commas (map str_for_bound_tvar xs) ^ "], ") ^
2.44 + str_for_typ ty ^ ", " ^ cl ^ ")."
2.45 + fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")."
2.46 fun formula pred (Formula (ident, kind, phi, _, info)) =
2.47 if pred kind then
2.48 let val rank = extract_isabelle_rank info in
2.49 @@ -574,8 +584,8 @@
2.50 | _ => NONE)
2.51 |> flat |> commas |> maybe_enclose "predicates [" "]."
2.52 val sorts =
2.53 - filt (fn Type_Decl (_, ty, ary, _) => SOME (ty_ary ary ty)
2.54 - | _ => NONE) @ [[ty_ary 0 dfg_individual_type]]
2.55 + filt (fn Type_Decl (_, ty, ary) => SOME (ty_ary ary ty) | _ => NONE) @
2.56 + [[ty_ary 0 dfg_individual_type]]
2.57 |> flat |> commas |> maybe_enclose "sorts [" "]."
2.58 val classes =
2.59 filt (fn Class_Decl (_, cl, _) => SOME cl | _ => NONE)
2.60 @@ -586,18 +596,23 @@
2.61 |> map (spair o apsnd string_of_int) |> commas
2.62 |> maybe_enclose "weights [" "]."
2.63 val syms = [func_aries, pred_aries, do_term_order_weights, sorts, classes]
2.64 - val func_sigs =
2.65 + val func_decls =
2.66 filt (fn Sym_Decl (_, sym, ty) =>
2.67 if is_function_atype ty then SOME (fun_typ sym ty) else NONE
2.68 - | _ => NONE)
2.69 - |> flat
2.70 - val pred_sigs =
2.71 + | _ => NONE) |> flat
2.72 + val pred_decls =
2.73 filt (fn Sym_Decl (_, sym, ty) =>
2.74 if is_nontrivial_predicate_atype ty then SOME (pred_typ sym ty)
2.75 else NONE
2.76 - | _ => NONE)
2.77 - |> flat
2.78 - val decls = func_sigs @ pred_sigs
2.79 + | _ => NONE) |> flat
2.80 + val sort_decls =
2.81 + filt (fn Class_Memb (_, xs, ty, cl) => SOME (sort_decl xs ty cl)
2.82 + | _ => NONE) |> flat
2.83 + val subclass_decls =
2.84 + filt (fn Class_Decl (_, sub, supers) =>
2.85 + SOME (map (subclass_of sub) supers)
2.86 + | _ => NONE) |> flat |> flat
2.87 + val decls = func_decls @ pred_decls @ sort_decls @ subclass_decls
2.88 val axioms =
2.89 filt (formula (curry (op <>) Conjecture)) |> separate [""] |> flat
2.90 val conjs =
2.91 @@ -719,7 +734,7 @@
2.92 (** Symbol declarations **)
2.93
2.94 fun add_declared_in_line (Class_Decl (_, cl, _)) = apfst (apfst (cons cl))
2.95 - | add_declared_in_line (Type_Decl (_, ty, _, _)) = apfst (apsnd (cons ty))
2.96 + | add_declared_in_line (Type_Decl (_, ty, _)) = apfst (apsnd (cons ty))
2.97 | add_declared_in_line (Sym_Decl (_, sym, _)) = apsnd (cons sym)
2.98 | add_declared_in_line _ = I
2.99 fun declared_in_atp_problem problem =
2.100 @@ -847,7 +862,8 @@
2.101 ##>> pool_map nice_term args #>> AAbs
2.102 fun nice_formula (ATyQuant (q, xs, phi)) =
2.103 pool_map nice_type (map fst xs)
2.104 - ##>> pool_map (pool_map nice_name) (map snd xs) ##>> nice_formula phi
2.105 + ##>> pool_map (pool_map nice_name) (map snd xs)
2.106 + ##>> nice_formula phi
2.107 #>> (fn ((tys, cls), phi) => ATyQuant (q, tys ~~ cls, phi))
2.108 | nice_formula (AQuant (q, xs, phi)) =
2.109 pool_map nice_name (map fst xs)
2.110 @@ -861,14 +877,20 @@
2.111 fun nice_line (Class_Decl (ident, cl, cls)) =
2.112 nice_name cl ##>> pool_map nice_name cls
2.113 #>> (fn (cl, cls) => Class_Decl (ident, cl, cls))
2.114 - | nice_line (Type_Decl (ident, ty, ary, cls)) =
2.115 - nice_name ty ##>> pool_map nice_name cls
2.116 - #>> (fn (ty, cls) => Type_Decl (ident, ty, ary, cls))
2.117 + | nice_line (Type_Decl (ident, ty, ary)) =
2.118 + nice_name ty #>> (fn ty => Type_Decl (ident, ty, ary))
2.119 | nice_line (Sym_Decl (ident, sym, ty)) =
2.120 nice_name sym ##>> nice_type ty
2.121 #>> (fn (sym, ty) => Sym_Decl (ident, sym, ty))
2.122 + | nice_line (Class_Memb (ident, xs, ty, cl)) =
2.123 + pool_map nice_name (map fst xs)
2.124 + ##>> pool_map (pool_map nice_name) (map snd xs)
2.125 + ##>> nice_type ty ##>> nice_name cl
2.126 + #>> (fn (((tys, cls), ty), cl) =>
2.127 + Class_Memb (ident, tys ~~ cls, ty, cl))
2.128 | nice_line (Formula (ident, kind, phi, source, info)) =
2.129 - nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))
2.130 + nice_formula phi
2.131 + #>> (fn phi => Formula (ident, kind, phi, source, info))
2.132 fun nice_problem problem =
2.133 pool_map (fn (heading, lines) =>
2.134 pool_map nice_line lines #>> pair heading) problem
3.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
3.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
3.3 @@ -53,15 +53,17 @@
3.4 val old_skolem_const_prefix : string
3.5 val new_skolem_const_prefix : string
3.6 val combinator_prefix : string
3.7 + val class_decl_prefix : string
3.8 val type_decl_prefix : string
3.9 val sym_decl_prefix : string
3.10 + val class_memb_prefix : string
3.11 val guards_sym_formula_prefix : string
3.12 val tags_sym_formula_prefix : string
3.13 val fact_prefix : string
3.14 val conjecture_prefix : string
3.15 val helper_prefix : string
3.16 - val class_rel_clause_prefix : string
3.17 - val arity_clause_prefix : string
3.18 + val subclass_prefix : string
3.19 + val tcon_clause_prefix : string
3.20 val tfree_clause_prefix : string
3.21 val lam_fact_prefix : string
3.22 val typed_helper_suffix : string
3.23 @@ -207,16 +209,18 @@
3.24
3.25 val combinator_prefix = "COMB"
3.26
3.27 +val class_decl_prefix = "cl_"
3.28 val type_decl_prefix = "ty_"
3.29 val sym_decl_prefix = "sy_"
3.30 +val class_memb_prefix = "clmb_"
3.31 val guards_sym_formula_prefix = "gsy_"
3.32 val tags_sym_formula_prefix = "tsy_"
3.33 val uncurried_alias_eq_prefix = "unc_"
3.34 val fact_prefix = "fact_"
3.35 val conjecture_prefix = "conj_"
3.36 val helper_prefix = "help_"
3.37 -val class_rel_clause_prefix = "clar_"
3.38 -val arity_clause_prefix = "arity_"
3.39 +val subclass_prefix = "subcl_"
3.40 +val tcon_clause_prefix = "tcon_"
3.41 val tfree_clause_prefix = "tfree_"
3.42
3.43 val lam_fact_prefix = "ATP.lambda_"
3.44 @@ -357,9 +361,9 @@
3.45 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
3.46 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
3.47
3.48 -fun make_tvar (s, i) = tvar_prefix ^ (ascii_of_indexname (unprefix "'" s, i))
3.49 -fun make_tfree s = tfree_prefix ^ (ascii_of (unprefix "'" s))
3.50 -fun tvar_name (x as (s, _)) = (make_tvar x, s)
3.51 +fun make_tvar (s, i) = tvar_prefix ^ ascii_of_indexname (unprefix "'" s, i)
3.52 +fun make_tfree s = tfree_prefix ^ ascii_of (unprefix "'" s)
3.53 +fun tvar_name ((x as (s, _)), _) = (make_tvar x, s)
3.54
3.55 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
3.56 local
3.57 @@ -374,7 +378,7 @@
3.58
3.59 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
3.60
3.61 -fun make_type_class clas = class_prefix ^ ascii_of clas
3.62 +fun make_class clas = class_prefix ^ ascii_of clas
3.63
3.64 fun new_skolem_var_name_from_const s =
3.65 let val ss = s |> space_explode Long_Name.separator in
3.66 @@ -406,8 +410,9 @@
3.67 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
3.68
3.69 val tvar_a_str = "'a"
3.70 -val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
3.71 -val tvar_a_name = tvar_name (tvar_a_str, 0)
3.72 +val tvar_a_z = ((tvar_a_str, 0), HOLogic.typeS)
3.73 +val tvar_a = TVar tvar_a_z
3.74 +val tvar_a_name = tvar_name tvar_a_z
3.75 val itself_name = `make_fixed_type_const @{type_name itself}
3.76 val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
3.77 val tvar_a_atype = AType (tvar_a_name, [])
3.78 @@ -415,92 +420,77 @@
3.79
3.80 (** Definitions and functions for FOL clauses and formulas for TPTP **)
3.81
3.82 -(** Isabelle arities **)
3.83 +(** Type class membership **)
3.84
3.85 -val type_class = the_single @{sort type}
3.86 +(* In our data structures, [] exceptionally refers to the top class, not to
3.87 + the empty class. *)
3.88
3.89 -type arity_clause =
3.90 - {name : string,
3.91 - prems : (string * typ) list,
3.92 - concl : string * typ}
3.93 +val class_of_types = the_single @{sort type}
3.94
3.95 -fun add_prem_atom T = fold (fn s => s <> type_class ? cons (s, T))
3.96 +fun normalize_classes cls = if member (op =) cls class_of_types then [] else cls
3.97
3.98 -(* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
3.99 -fun make_axiom_arity_clause (tc, name, (class, args)) =
3.100 +(* Arity of type constructor "s :: (arg1, ..., argN) res" *)
3.101 +fun make_axiom_tcon_clause (s, name, (cl, args)) =
3.102 let
3.103 + val args = args |> map normalize_classes
3.104 val tvars =
3.105 - map (fn j => TVar ((tvar_a_str, j), @{sort HOL.type}))
3.106 - (1 upto length args)
3.107 - in
3.108 - {name = name, prems = fold (uncurry add_prem_atom) (tvars ~~ args) [],
3.109 - concl = (class, Type (tc, tvars))}
3.110 - end
3.111 + 1 upto length args |> map (fn j => TVar ((tvar_a_str, j), @{sort type}))
3.112 + in (name, args ~~ tvars, (cl, Type (s, tvars))) end
3.113
3.114 (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
3.115 theory thy provided its arguments have the corresponding sorts. *)
3.116 -fun type_class_pairs thy tycons classes =
3.117 +fun class_pairs thy tycons cls =
3.118 let
3.119 val alg = Sign.classes_of thy
3.120 fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
3.121 - fun add_class tycon class =
3.122 - cons (class, domain_sorts tycon class)
3.123 + fun add_class tycon cl =
3.124 + cons (cl, domain_sorts tycon cl)
3.125 handle Sorts.CLASS_ERROR _ => I
3.126 - fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
3.127 + fun try_classes tycon = (tycon, fold (add_class tycon) cls [])
3.128 in map try_classes tycons end
3.129
3.130 (* Proving one (tycon, class) membership may require proving others, so
3.131 iterate. *)
3.132 -fun iter_type_class_pairs _ _ [] = ([], [])
3.133 - | iter_type_class_pairs thy tycons classes =
3.134 +fun all_class_pairs _ _ [] = ([], [])
3.135 + | all_class_pairs thy tycons cls =
3.136 let
3.137 fun maybe_insert_class s =
3.138 - (s <> type_class andalso not (member (op =) classes s))
3.139 + (s <> class_of_types andalso not (member (op =) cls s))
3.140 ? insert (op =) s
3.141 - val cpairs = type_class_pairs thy tycons classes
3.142 - val newclasses =
3.143 - [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
3.144 - val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
3.145 - in (classes' @ classes, union (op =) cpairs' cpairs) end
3.146 + val pairs = class_pairs thy tycons cls
3.147 + val new_cls =
3.148 + [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) pairs
3.149 + val (cls', pairs') = all_class_pairs thy tycons new_cls
3.150 + in (cls' @ cls, union (op =) pairs' pairs) end
3.151
3.152 -fun arity_clause _ _ (_, []) = []
3.153 - | arity_clause seen n (tcons, ("HOL.type", _) :: ars) =
3.154 - arity_clause seen n (tcons, ars) (* ignore *)
3.155 - | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
3.156 - if member (op =) seen class then
3.157 - (* multiple arities for the same (tycon, class) pair *)
3.158 - make_axiom_arity_clause (tcons,
3.159 - lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
3.160 +fun tcon_clause _ _ (_, []) = []
3.161 + | tcon_clause seen n (tcons, (ar as (cl, _)) :: ars) =
3.162 + if cl = class_of_types then
3.163 + tcon_clause seen n (tcons, ars)
3.164 + else if member (op =) seen cl then
3.165 + (* multiple clauses for the same (tycon, cl) pair *)
3.166 + make_axiom_tcon_clause (tcons,
3.167 + lookup_const tcons ^ "___" ^ ascii_of cl ^ "_" ^ string_of_int n,
3.168 ar) ::
3.169 - arity_clause seen (n + 1) (tcons, ars)
3.170 + tcon_clause seen (n + 1) (tcons, ars)
3.171 else
3.172 - make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
3.173 - ascii_of class, ar) ::
3.174 - arity_clause (class :: seen) n (tcons, ars)
3.175 + make_axiom_tcon_clause (tcons, lookup_const tcons ^ "___" ^ ascii_of cl,
3.176 + ar) ::
3.177 + tcon_clause (cl :: seen) n (tcons, ars)
3.178
3.179 -fun make_arity_clauses thy tycons =
3.180 - iter_type_class_pairs thy tycons ##> maps (arity_clause [] 1)
3.181 +fun make_tcon_clauses thy tycons =
3.182 + all_class_pairs thy tycons ##> maps (tcon_clause [] 1)
3.183
3.184
3.185 (** Isabelle class relations **)
3.186
3.187 -type class_rel_clause =
3.188 - {name : string,
3.189 - subclass : string,
3.190 - superclass : string}
3.191 -
3.192 -(* Generate all pairs (sub, super) such that sub is a proper subclass of super
3.193 - in theory "thy". *)
3.194 -fun class_pairs thy subs supers =
3.195 +(* Generate a list ("sub", "supers") such that "sub" is a proper subclass of all
3.196 + "supers". *)
3.197 +fun make_subclass_pairs thy subs supers =
3.198 let
3.199 - val class_less = Sorts.class_less (Sign.classes_of thy)
3.200 - fun add_super sub super = class_less (sub, super) ? cons (sub, super)
3.201 - fun add_supers sub = fold (add_super sub) supers
3.202 - in fold add_supers subs [] end
3.203 -
3.204 -fun make_class_rel_clause (sub, super) =
3.205 - {name = sub ^ "_" ^ super, subclass = sub, superclass = super}
3.206 -fun make_class_rel_clauses thy = map make_class_rel_clause oo class_pairs thy
3.207 + val class_less = curry (Sorts.class_less (Sign.classes_of thy))
3.208 + fun supers_of sub = (sub, filter (class_less sub) supers)
3.209 + in map supers_of subs |> filter_out (null o snd) end
3.210
3.211 (* intermediate terms *)
3.212 datatype iterm =
3.213 @@ -885,7 +875,7 @@
3.214 `make_fixed_type_const s,
3.215 map term Ts)
3.216 | term (TFree (s, _)) = AType (`make_tfree s, [])
3.217 - | term (TVar (x, _)) = AType (tvar_name x, [])
3.218 + | term (TVar z) = AType (tvar_name z, [])
3.219 in term end
3.220
3.221 fun ho_term_from_ho_type (AType (name, tys)) = ATerm ((name, []), map ho_term_from_ho_type tys)
3.222 @@ -944,7 +934,7 @@
3.223 fun generic_add_sorts_on_type _ [] = I
3.224 | generic_add_sorts_on_type T (s :: ss) =
3.225 generic_add_sorts_on_type T ss
3.226 - #> (if s = the_single @{sort HOL.type} then I else insert (op =) (s, T))
3.227 + #> (if s = the_single @{sort type} then I else insert (op =) (s, T))
3.228 fun add_sorts_on_tfree (T as TFree (_, S)) = generic_add_sorts_on_type T S
3.229 | add_sorts_on_tfree _ = I
3.230 fun add_sorts_on_tvar (T as TVar (_, S)) = generic_add_sorts_on_type T S
3.231 @@ -957,9 +947,9 @@
3.232 ([], map_filter (Option.map ho_term_from_ho_type
3.233 o ho_type_for_type_arg type_enc) T_args)
3.234
3.235 -fun type_class_atom type_enc (class, T) =
3.236 +fun class_atom type_enc (cl, T) =
3.237 let
3.238 - val class = `make_type_class class
3.239 + val cl = `make_class cl
3.240 val (ty_args, tm_args) = process_type_args type_enc [T]
3.241 val tm_args =
3.242 tm_args @
3.243 @@ -967,12 +957,15 @@
3.244 Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
3.245 [ATerm ((TYPE_name, ty_args), [])]
3.246 | _ => [])
3.247 - in AAtom (ATerm ((class, ty_args), tm_args)) end
3.248 -fun formulas_for_types type_enc add_sorts_on_typ Ts =
3.249 + in AAtom (ATerm ((cl, ty_args), tm_args)) end
3.250 +
3.251 +fun class_atoms type_enc (cls, T) =
3.252 + map (fn cl => class_atom type_enc (cl, T)) cls
3.253 +
3.254 +fun class_membs_for_types type_enc add_sorts_on_typ Ts =
3.255 [] |> (polymorphism_of_type_enc type_enc <> Type_Class_Polymorphic andalso
3.256 level_of_type_enc type_enc <> No_Types)
3.257 ? fold add_sorts_on_typ Ts
3.258 - |> map (type_class_atom type_enc)
3.259
3.260 fun mk_aconns c = split_last #> uncurry (fold_rev (mk_aconn c))
3.261
3.262 @@ -1732,17 +1725,19 @@
3.263 case filter is_TVar Ts of
3.264 [] => I
3.265 | Ts =>
3.266 - (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
3.267 + (sorts ? mk_ahorn (Ts |> class_membs_for_types type_enc add_sorts_on_tvar
3.268 + |> map (class_atom type_enc)))
3.269 #> (case type_enc of
3.270 Native (_, poly, _) =>
3.271 - mk_atyquant AForall (map (fn TVar (x, S) =>
3.272 - (AType (tvar_name x, []),
3.273 - if poly = Type_Class_Polymorphic then
3.274 - map (`make_type_class) S
3.275 - else
3.276 - [])) Ts)
3.277 + mk_atyquant AForall
3.278 + (map (fn TVar (z as (_, S)) =>
3.279 + (AType (tvar_name z, []),
3.280 + if poly = Type_Class_Polymorphic then
3.281 + map (`make_class) (normalize_classes S)
3.282 + else
3.283 + [])) Ts)
3.284 | _ =>
3.285 - mk_aquant AForall (map (fn TVar (x, _) => (tvar_name x, NONE)) Ts))
3.286 + mk_aquant AForall (map (fn TVar z => (tvar_name z, NONE)) Ts))
3.287
3.288 fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
3.289 (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
3.290 @@ -1819,15 +1814,12 @@
3.291
3.292 fun set_insert (x, s) = Symtab.update (x, ()) s
3.293
3.294 -fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
3.295 -
3.296 -(* Remove this trivial type class (FIXME: similar code elsewhere) *)
3.297 -fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
3.298 +fun add_classes (cls, cset) = List.foldl set_insert cset (flat cls)
3.299
3.300 fun classes_of_terms get_Ts =
3.301 map (map snd o get_Ts)
3.302 - #> List.foldl add_classes Symtab.empty
3.303 - #> delete_type #> Symtab.keys
3.304 + #> List.foldl add_classes Symtab.empty #> Symtab.delete_safe class_of_types
3.305 + #> Symtab.keys
3.306
3.307 val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
3.308 val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
3.309 @@ -1950,13 +1942,13 @@
3.310 val subs = tfree_classes_of_terms all_ts
3.311 val supers = tvar_classes_of_terms all_ts
3.312 val tycons = type_constrs_of_terms thy all_ts
3.313 - val (supers, arity_clauses) =
3.314 + val (supers, tcon_clauses) =
3.315 if level_of_type_enc type_enc = No_Types then ([], [])
3.316 - else make_arity_clauses thy tycons supers
3.317 - val class_rel_clauses = make_class_rel_clauses thy subs supers
3.318 + else make_tcon_clauses thy tycons supers
3.319 + val subclass_pairs = make_subclass_pairs thy subs supers
3.320 in
3.321 (fact_names |> map single, union (op =) subs supers, conjs,
3.322 - facts @ lam_facts, class_rel_clauses, arity_clauses, lifted)
3.323 + facts @ lam_facts, subclass_pairs, tcon_clauses, lifted)
3.324 end
3.325
3.326 val type_guard = `(make_fixed_const NONE) type_guard_name
3.327 @@ -2121,26 +2113,33 @@
3.328 end)
3.329 |> Formula
3.330
3.331 -fun formula_line_for_class_rel_clause type_enc
3.332 - ({name, subclass, superclass, ...} : class_rel_clause) =
3.333 - Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
3.334 +fun formula_lines_for_subclass type_enc sub super =
3.335 + Formula (subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, Axiom,
3.336 AConn (AImplies,
3.337 - [type_class_atom type_enc (subclass, tvar_a),
3.338 - type_class_atom type_enc (superclass, tvar_a)])
3.339 + [sub, super] |> map (fn s => class_atom type_enc (s, tvar_a)))
3.340 |> bound_tvars type_enc false [tvar_a],
3.341 NONE, isabelle_info inductiveN helper_rank)
3.342
3.343 -fun formula_line_for_arity_clause type_enc
3.344 - ({name, prems, concl} : arity_clause) =
3.345 - let
3.346 - val atomic_Ts = fold (fold_atyps (insert (op =)) o snd) (concl :: prems) []
3.347 - in
3.348 - Formula (arity_clause_prefix ^ name, Axiom,
3.349 - mk_ahorn (map (type_class_atom type_enc) prems)
3.350 - (type_class_atom type_enc concl)
3.351 - |> bound_tvars type_enc true atomic_Ts,
3.352 +fun formula_lines_for_subclass_pair type_enc (sub, supers) =
3.353 + if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
3.354 + [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub,
3.355 + map (`make_class) supers)]
3.356 + else
3.357 + map (formula_lines_for_subclass type_enc sub) supers
3.358 +
3.359 +fun formula_line_for_tcon_clause type_enc (name, prems, (cl, T)) =
3.360 + if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
3.361 + Class_Memb (class_memb_prefix ^ name,
3.362 + map (fn (cls, T) =>
3.363 + (T |> dest_TVar |> tvar_name, map (`make_class) cls))
3.364 + prems,
3.365 + native_ho_type_from_typ type_enc false 0 T, `make_class cl)
3.366 + else
3.367 + Formula (tcon_clause_prefix ^ name, Axiom,
3.368 + mk_ahorn (maps (class_atoms type_enc) prems)
3.369 + (class_atom type_enc (cl, T))
3.370 + |> bound_tvars type_enc true (snd (dest_Type T)),
3.371 NONE, isabelle_info inductiveN helper_rank)
3.372 - end
3.373
3.374 fun formula_line_for_conjecture ctxt mono type_enc
3.375 ({name, role, iformula, atomic_types, ...} : ifact) =
3.376 @@ -2153,17 +2152,23 @@
3.377
3.378 fun formula_lines_for_free_types type_enc (facts : ifact list) =
3.379 let
3.380 - fun line j phi =
3.381 - Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
3.382 - val phis =
3.383 + fun line j (cl, T) =
3.384 + if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
3.385 + Class_Memb (class_memb_prefix ^ string_of_int j, [],
3.386 + native_ho_type_from_typ type_enc false 0 T,
3.387 + `make_class cl)
3.388 + else
3.389 + Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
3.390 + class_atom type_enc (cl, T), NONE, [])
3.391 + val membs =
3.392 fold (union (op =)) (map #atomic_types facts) []
3.393 - |> formulas_for_types type_enc add_sorts_on_tfree
3.394 - in map2 line (0 upto length phis - 1) phis end
3.395 + |> class_membs_for_types type_enc add_sorts_on_tfree
3.396 + in map2 line (0 upto length membs - 1) membs end
3.397
3.398 (** Symbol declarations **)
3.399
3.400 fun decl_line_for_class phantoms s =
3.401 - let val name as (s, _) = `make_type_class s in
3.402 + let val name as (s, _) = `make_class s in
3.403 Sym_Decl (sym_decl_prefix ^ s, name,
3.404 APi ([tvar_a_name],
3.405 if phantoms = Without_Phantom_Type_Vars then
3.406 @@ -2361,7 +2366,7 @@
3.407 T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
3.408 |> native_ho_type_from_typ type_enc pred_sym ary
3.409 |> not (null T_args)
3.410 - ? curry APi (map (tvar_name o fst o dest_TVar) T_args))
3.411 + ? curry APi (map (tvar_name o dest_TVar) T_args))
3.412 end
3.413
3.414 fun honor_conj_sym_role in_conj =
3.415 @@ -2555,11 +2560,11 @@
3.416 val explicit_declsN = "Explicit typings"
3.417 val uncurried_alias_eqsN = "Uncurried aliases"
3.418 val factsN = "Relevant facts"
3.419 -val class_relsN = "Class relationships"
3.420 -val aritiesN = "Arities"
3.421 +val subclassesN = "Subclasses"
3.422 +val tconsN = "Type constructors"
3.423 val helpersN = "Helper facts"
3.424 val conjsN = "Conjectures"
3.425 -val free_typesN = "Type variables"
3.426 +val free_typesN = "Free types"
3.427
3.428 (* TFF allows implicit declarations of types, function symbols, and predicate
3.429 symbols (with "$i" as the type of individuals), but some provers (e.g.,
3.430 @@ -2576,6 +2581,7 @@
3.431 let
3.432 fun do_sym (name as (s, _)) value =
3.433 if is_tptp_user_symbol s then Symtab.default (s, (name, value)) else I
3.434 + fun do_class name = apfst (apfst (do_sym name ()))
3.435 fun do_type (AType (name, tys)) =
3.436 apfst (apsnd (do_sym name (length tys))) #> fold do_type tys
3.437 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
3.438 @@ -2587,15 +2593,17 @@
3.439 | do_term _ (AAbs (((_, ty), tm), args)) =
3.440 do_type ty #> do_term false tm #> fold (do_term false) args
3.441 fun do_formula (ATyQuant (_, xs, phi)) =
3.442 - fold (do_type o fst) xs
3.443 - #> fold (fold (fn name => apfst (apfst (do_sym name ()))) o snd) xs
3.444 + fold (do_type o fst) xs #> fold (fold do_class o snd) xs
3.445 #> do_formula phi
3.446 | do_formula (AQuant (_, xs, phi)) =
3.447 fold do_type (map_filter snd xs) #> do_formula phi
3.448 | do_formula (AConn (_, phis)) = fold do_formula phis
3.449 | do_formula (AAtom tm) = do_term true tm
3.450 - fun do_line (Type_Decl _) = I
3.451 + fun do_line (Class_Decl (_, _, cls)) = fold do_class cls
3.452 + | do_line (Type_Decl _) = I
3.453 | do_line (Sym_Decl (_, _, ty)) = do_type ty
3.454 + | do_line (Class_Memb (_, xs, ty, cl)) =
3.455 + fold (fold do_class o snd) xs #> do_type ty #> do_class cl
3.456 | do_line (Formula (_, _, phi, _, _)) = do_formula phi
3.457 val ((cls, tys), syms) = declared_in_atp_problem problem
3.458 in
3.459 @@ -2611,16 +2619,16 @@
3.460 val ((cls, tys), syms) = undeclared_in_problem problem
3.461 val decls =
3.462 Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
3.463 - | (s, (sym, ())) =>
3.464 - cons (Class_Decl (type_decl_prefix ^ s, sym, [])))
3.465 + | (s, (cls, ())) =>
3.466 + cons (Class_Decl (class_decl_prefix ^ s, cls, [])))
3.467 cls [] @
3.468 Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
3.469 - | (s, (sym, ary)) =>
3.470 - cons (Type_Decl (type_decl_prefix ^ s, sym, ary, [])))
3.471 + | (s, (ty, ary)) =>
3.472 + cons (Type_Decl (type_decl_prefix ^ s, ty, ary)))
3.473 tys [] @
3.474 Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
3.475 | (s, (sym, ty)) =>
3.476 - cons (Sym_Decl (type_decl_prefix ^ s, sym, ty ())))
3.477 + cons (Sym_Decl (sym_decl_prefix ^ s, sym, ty ())))
3.478 syms []
3.479 in (heading, decls) :: problem end
3.480
3.481 @@ -2663,7 +2671,7 @@
3.482 liftingN
3.483 else
3.484 lam_trans
3.485 - val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
3.486 + val (fact_names, classes, conjs, facts, subclass_pairs, tcon_clauses,
3.487 lifted) =
3.488 translate_formulas ctxt prem_role format type_enc lam_trans preproc hyp_ts
3.489 concl_t facts
3.490 @@ -2700,15 +2708,10 @@
3.491 map (formula_line_for_fact ctxt fact_prefix ascii_of (not exporter)
3.492 (not exporter) mono type_enc (rank_of_fact_num num_facts))
3.493 (0 upto num_facts - 1 ~~ facts)
3.494 - val (class_rel_lines, arity_lines, free_type_lines) =
3.495 - if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
3.496 - ([],
3.497 - [],
3.498 - [])
3.499 - else
3.500 - (map (formula_line_for_class_rel_clause type_enc) class_rel_clauses,
3.501 - map (formula_line_for_arity_clause type_enc) arity_clauses,
3.502 - formula_lines_for_free_types type_enc (facts @ conjs))
3.503 + val subclass_lines =
3.504 + maps (formula_lines_for_subclass_pair type_enc) subclass_pairs
3.505 + val tcon_lines = map (formula_line_for_tcon_clause type_enc) tcon_clauses
3.506 + val free_type_lines = formula_lines_for_free_types type_enc (facts @ conjs)
3.507 val helper_lines =
3.508 0 upto length helpers - 1 ~~ helpers
3.509 |> map (formula_line_for_fact ctxt helper_prefix I false true mono
3.510 @@ -2718,8 +2721,8 @@
3.511 [(explicit_declsN, class_decl_lines @ sym_decl_lines),
3.512 (uncurried_alias_eqsN, uncurried_alias_eq_lines),
3.513 (factsN, fact_lines),
3.514 - (class_relsN, class_rel_lines),
3.515 - (aritiesN, arity_lines),
3.516 + (subclassesN, subclass_lines),
3.517 + (tconsN, tcon_lines),
3.518 (helpersN, helper_lines),
3.519 (free_typesN, free_type_lines),
3.520 (conjsN, map (formula_line_for_conjecture ctxt mono type_enc) conjs)]
3.521 @@ -2780,7 +2783,7 @@
3.522 |> add_conjectures_weights (get free_typesN @ get conjsN)
3.523 |> add_facts_weights (get factsN)
3.524 |> fold (fold (add_line_weights type_info_default_weight) o get)
3.525 - [explicit_declsN, class_relsN, aritiesN]
3.526 + [explicit_declsN, subclassesN, tconsN]
3.527 |> Symtab.dest
3.528 |> sort (prod_ord Real.compare string_ord o pairself swap)
3.529 end