--- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:40 2012 +0200
@@ -45,8 +45,9 @@
datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Class_Decl of string * 'a * 'a list |
- Type_Decl of string * 'a * int * 'a list |
+ Type_Decl of string * 'a * int |
Sym_Decl of string * 'a * 'a ho_type |
+ Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a |
Formula of string * formula_role
* ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
* (string, string ho_type) ho_term option
@@ -178,8 +179,9 @@
datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture
datatype 'a problem_line =
Class_Decl of string * 'a * 'a list |
- Type_Decl of string * 'a * int * 'a list |
+ Type_Decl of string * 'a * int |
Sym_Decl of string * 'a * 'a ho_type |
+ Class_Memb of string * ('a * 'a list) list * 'a ho_type * 'a |
Formula of string * formula_role
* ('a, 'a ho_type, ('a, 'a ho_type) ho_term, 'a) formula
* (string, string ho_type) ho_term option
@@ -463,7 +465,7 @@
fun nary_type_decl_type n = funpow n (curry AFun atype_of_types) atype_of_types
-fun tptp_string_for_line format (Type_Decl (ident, ty, ary, _)) =
+fun tptp_string_for_line format (Type_Decl (ident, ty, ary)) =
tptp_string_for_line format (Sym_Decl (ident, ty, nary_type_decl_type ary))
| tptp_string_for_line format (Sym_Decl (ident, sym, ty)) =
tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^
@@ -551,6 +553,14 @@
strip_atype ty |> fst
|>> (fn [] => [] | ty_vars => ["[" ^ commas ty_vars ^ "]"])
in "predicate(" ^ commas (sym :: ty_vars @ map str_for_typ tys) ^ ")." end
+ fun str_for_bound_tvar (ty, []) = ty
+ | str_for_bound_tvar (ty, cls) = ty ^ " : " ^ commas cls
+ fun sort_decl xs ty cl =
+ "sort(" ^
+ (if null xs then ""
+ else "[" ^ commas (map str_for_bound_tvar xs) ^ "], ") ^
+ str_for_typ ty ^ ", " ^ cl ^ ")."
+ fun subclass_of sub super = "subclass(" ^ sub ^ ", " ^ super ^ ")."
fun formula pred (Formula (ident, kind, phi, _, info)) =
if pred kind then
let val rank = extract_isabelle_rank info in
@@ -574,8 +584,8 @@
| _ => NONE)
|> flat |> commas |> maybe_enclose "predicates [" "]."
val sorts =
- filt (fn Type_Decl (_, ty, ary, _) => SOME (ty_ary ary ty)
- | _ => NONE) @ [[ty_ary 0 dfg_individual_type]]
+ filt (fn Type_Decl (_, ty, ary) => SOME (ty_ary ary ty) | _ => NONE) @
+ [[ty_ary 0 dfg_individual_type]]
|> flat |> commas |> maybe_enclose "sorts [" "]."
val classes =
filt (fn Class_Decl (_, cl, _) => SOME cl | _ => NONE)
@@ -586,18 +596,23 @@
|> map (spair o apsnd string_of_int) |> commas
|> maybe_enclose "weights [" "]."
val syms = [func_aries, pred_aries, do_term_order_weights, sorts, classes]
- val func_sigs =
+ val func_decls =
filt (fn Sym_Decl (_, sym, ty) =>
if is_function_atype ty then SOME (fun_typ sym ty) else NONE
- | _ => NONE)
- |> flat
- val pred_sigs =
+ | _ => NONE) |> flat
+ val pred_decls =
filt (fn Sym_Decl (_, sym, ty) =>
if is_nontrivial_predicate_atype ty then SOME (pred_typ sym ty)
else NONE
- | _ => NONE)
- |> flat
- val decls = func_sigs @ pred_sigs
+ | _ => NONE) |> flat
+ val sort_decls =
+ filt (fn Class_Memb (_, xs, ty, cl) => SOME (sort_decl xs ty cl)
+ | _ => NONE) |> flat
+ val subclass_decls =
+ filt (fn Class_Decl (_, sub, supers) =>
+ SOME (map (subclass_of sub) supers)
+ | _ => NONE) |> flat |> flat
+ val decls = func_decls @ pred_decls @ sort_decls @ subclass_decls
val axioms =
filt (formula (curry (op <>) Conjecture)) |> separate [""] |> flat
val conjs =
@@ -719,7 +734,7 @@
(** Symbol declarations **)
fun add_declared_in_line (Class_Decl (_, cl, _)) = apfst (apfst (cons cl))
- | add_declared_in_line (Type_Decl (_, ty, _, _)) = apfst (apsnd (cons ty))
+ | add_declared_in_line (Type_Decl (_, ty, _)) = apfst (apsnd (cons ty))
| add_declared_in_line (Sym_Decl (_, sym, _)) = apsnd (cons sym)
| add_declared_in_line _ = I
fun declared_in_atp_problem problem =
@@ -847,7 +862,8 @@
##>> pool_map nice_term args #>> AAbs
fun nice_formula (ATyQuant (q, xs, phi)) =
pool_map nice_type (map fst xs)
- ##>> pool_map (pool_map nice_name) (map snd xs) ##>> nice_formula phi
+ ##>> pool_map (pool_map nice_name) (map snd xs)
+ ##>> nice_formula phi
#>> (fn ((tys, cls), phi) => ATyQuant (q, tys ~~ cls, phi))
| nice_formula (AQuant (q, xs, phi)) =
pool_map nice_name (map fst xs)
@@ -861,14 +877,20 @@
fun nice_line (Class_Decl (ident, cl, cls)) =
nice_name cl ##>> pool_map nice_name cls
#>> (fn (cl, cls) => Class_Decl (ident, cl, cls))
- | nice_line (Type_Decl (ident, ty, ary, cls)) =
- nice_name ty ##>> pool_map nice_name cls
- #>> (fn (ty, cls) => Type_Decl (ident, ty, ary, cls))
+ | nice_line (Type_Decl (ident, ty, ary)) =
+ nice_name ty #>> (fn ty => Type_Decl (ident, ty, ary))
| nice_line (Sym_Decl (ident, sym, ty)) =
nice_name sym ##>> nice_type ty
#>> (fn (sym, ty) => Sym_Decl (ident, sym, ty))
+ | nice_line (Class_Memb (ident, xs, ty, cl)) =
+ pool_map nice_name (map fst xs)
+ ##>> pool_map (pool_map nice_name) (map snd xs)
+ ##>> nice_type ty ##>> nice_name cl
+ #>> (fn (((tys, cls), ty), cl) =>
+ Class_Memb (ident, tys ~~ cls, ty, cl))
| nice_line (Formula (ident, kind, phi, source, info)) =
- nice_formula phi #>> (fn phi => Formula (ident, kind, phi, source, info))
+ nice_formula phi
+ #>> (fn phi => Formula (ident, kind, phi, source, info))
fun nice_problem problem =
pool_map (fn (heading, lines) =>
pool_map nice_line lines #>> pair heading) problem
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:40 2012 +0200
@@ -53,15 +53,17 @@
val old_skolem_const_prefix : string
val new_skolem_const_prefix : string
val combinator_prefix : string
+ val class_decl_prefix : string
val type_decl_prefix : string
val sym_decl_prefix : string
+ val class_memb_prefix : string
val guards_sym_formula_prefix : string
val tags_sym_formula_prefix : string
val fact_prefix : string
val conjecture_prefix : string
val helper_prefix : string
- val class_rel_clause_prefix : string
- val arity_clause_prefix : string
+ val subclass_prefix : string
+ val tcon_clause_prefix : string
val tfree_clause_prefix : string
val lam_fact_prefix : string
val typed_helper_suffix : string
@@ -207,16 +209,18 @@
val combinator_prefix = "COMB"
+val class_decl_prefix = "cl_"
val type_decl_prefix = "ty_"
val sym_decl_prefix = "sy_"
+val class_memb_prefix = "clmb_"
val guards_sym_formula_prefix = "gsy_"
val tags_sym_formula_prefix = "tsy_"
val uncurried_alias_eq_prefix = "unc_"
val fact_prefix = "fact_"
val conjecture_prefix = "conj_"
val helper_prefix = "help_"
-val class_rel_clause_prefix = "clar_"
-val arity_clause_prefix = "arity_"
+val subclass_prefix = "subcl_"
+val tcon_clause_prefix = "tcon_"
val tfree_clause_prefix = "tfree_"
val lam_fact_prefix = "ATP.lambda_"
@@ -357,9 +361,9 @@
fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
-fun make_tvar (s, i) = tvar_prefix ^ (ascii_of_indexname (unprefix "'" s, i))
-fun make_tfree s = tfree_prefix ^ (ascii_of (unprefix "'" s))
-fun tvar_name (x as (s, _)) = (make_tvar x, s)
+fun make_tvar (s, i) = tvar_prefix ^ ascii_of_indexname (unprefix "'" s, i)
+fun make_tfree s = tfree_prefix ^ ascii_of (unprefix "'" s)
+fun tvar_name ((x as (s, _)), _) = (make_tvar x, s)
(* "HOL.eq" and choice are mapped to the ATP's equivalents *)
local
@@ -374,7 +378,7 @@
fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
-fun make_type_class clas = class_prefix ^ ascii_of clas
+fun make_class clas = class_prefix ^ ascii_of clas
fun new_skolem_var_name_from_const s =
let val ss = s |> space_explode Long_Name.separator in
@@ -406,8 +410,9 @@
fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
val tvar_a_str = "'a"
-val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
-val tvar_a_name = tvar_name (tvar_a_str, 0)
+val tvar_a_z = ((tvar_a_str, 0), HOLogic.typeS)
+val tvar_a = TVar tvar_a_z
+val tvar_a_name = tvar_name tvar_a_z
val itself_name = `make_fixed_type_const @{type_name itself}
val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
val tvar_a_atype = AType (tvar_a_name, [])
@@ -415,92 +420,77 @@
(** Definitions and functions for FOL clauses and formulas for TPTP **)
-(** Isabelle arities **)
-
-val type_class = the_single @{sort type}
+(** Type class membership **)
-type arity_clause =
- {name : string,
- prems : (string * typ) list,
- concl : string * typ}
+(* In our data structures, [] exceptionally refers to the top class, not to
+ the empty class. *)
-fun add_prem_atom T = fold (fn s => s <> type_class ? cons (s, T))
+val class_of_types = the_single @{sort type}
-(* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
-fun make_axiom_arity_clause (tc, name, (class, args)) =
+fun normalize_classes cls = if member (op =) cls class_of_types then [] else cls
+
+(* Arity of type constructor "s :: (arg1, ..., argN) res" *)
+fun make_axiom_tcon_clause (s, name, (cl, args)) =
let
+ val args = args |> map normalize_classes
val tvars =
- map (fn j => TVar ((tvar_a_str, j), @{sort HOL.type}))
- (1 upto length args)
- in
- {name = name, prems = fold (uncurry add_prem_atom) (tvars ~~ args) [],
- concl = (class, Type (tc, tvars))}
- end
+ 1 upto length args |> map (fn j => TVar ((tvar_a_str, j), @{sort type}))
+ in (name, args ~~ tvars, (cl, Type (s, tvars))) end
(* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
theory thy provided its arguments have the corresponding sorts. *)
-fun type_class_pairs thy tycons classes =
+fun class_pairs thy tycons cls =
let
val alg = Sign.classes_of thy
fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
- fun add_class tycon class =
- cons (class, domain_sorts tycon class)
+ fun add_class tycon cl =
+ cons (cl, domain_sorts tycon cl)
handle Sorts.CLASS_ERROR _ => I
- fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
+ fun try_classes tycon = (tycon, fold (add_class tycon) cls [])
in map try_classes tycons end
(* Proving one (tycon, class) membership may require proving others, so
iterate. *)
-fun iter_type_class_pairs _ _ [] = ([], [])
- | iter_type_class_pairs thy tycons classes =
+fun all_class_pairs _ _ [] = ([], [])
+ | all_class_pairs thy tycons cls =
let
fun maybe_insert_class s =
- (s <> type_class andalso not (member (op =) classes s))
+ (s <> class_of_types andalso not (member (op =) cls s))
? insert (op =) s
- val cpairs = type_class_pairs thy tycons classes
- val newclasses =
- [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
- val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
- in (classes' @ classes, union (op =) cpairs' cpairs) end
+ val pairs = class_pairs thy tycons cls
+ val new_cls =
+ [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) pairs
+ val (cls', pairs') = all_class_pairs thy tycons new_cls
+ in (cls' @ cls, union (op =) pairs' pairs) end
-fun arity_clause _ _ (_, []) = []
- | arity_clause seen n (tcons, ("HOL.type", _) :: ars) =
- arity_clause seen n (tcons, ars) (* ignore *)
- | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
- if member (op =) seen class then
- (* multiple arities for the same (tycon, class) pair *)
- make_axiom_arity_clause (tcons,
- lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
+fun tcon_clause _ _ (_, []) = []
+ | tcon_clause seen n (tcons, (ar as (cl, _)) :: ars) =
+ if cl = class_of_types then
+ tcon_clause seen n (tcons, ars)
+ else if member (op =) seen cl then
+ (* multiple clauses for the same (tycon, cl) pair *)
+ make_axiom_tcon_clause (tcons,
+ lookup_const tcons ^ "___" ^ ascii_of cl ^ "_" ^ string_of_int n,
ar) ::
- arity_clause seen (n + 1) (tcons, ars)
+ tcon_clause seen (n + 1) (tcons, ars)
else
- make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
- ascii_of class, ar) ::
- arity_clause (class :: seen) n (tcons, ars)
+ make_axiom_tcon_clause (tcons, lookup_const tcons ^ "___" ^ ascii_of cl,
+ ar) ::
+ tcon_clause (cl :: seen) n (tcons, ars)
-fun make_arity_clauses thy tycons =
- iter_type_class_pairs thy tycons ##> maps (arity_clause [] 1)
+fun make_tcon_clauses thy tycons =
+ all_class_pairs thy tycons ##> maps (tcon_clause [] 1)
(** Isabelle class relations **)
-type class_rel_clause =
- {name : string,
- subclass : string,
- superclass : string}
-
-(* Generate all pairs (sub, super) such that sub is a proper subclass of super
- in theory "thy". *)
-fun class_pairs thy subs supers =
+(* Generate a list ("sub", "supers") such that "sub" is a proper subclass of all
+ "supers". *)
+fun make_subclass_pairs thy subs supers =
let
- val class_less = Sorts.class_less (Sign.classes_of thy)
- fun add_super sub super = class_less (sub, super) ? cons (sub, super)
- fun add_supers sub = fold (add_super sub) supers
- in fold add_supers subs [] end
-
-fun make_class_rel_clause (sub, super) =
- {name = sub ^ "_" ^ super, subclass = sub, superclass = super}
-fun make_class_rel_clauses thy = map make_class_rel_clause oo class_pairs thy
+ val class_less = curry (Sorts.class_less (Sign.classes_of thy))
+ fun supers_of sub = (sub, filter (class_less sub) supers)
+ in map supers_of subs |> filter_out (null o snd) end
(* intermediate terms *)
datatype iterm =
@@ -885,7 +875,7 @@
`make_fixed_type_const s,
map term Ts)
| term (TFree (s, _)) = AType (`make_tfree s, [])
- | term (TVar (x, _)) = AType (tvar_name x, [])
+ | term (TVar z) = AType (tvar_name z, [])
in term end
fun ho_term_from_ho_type (AType (name, tys)) = ATerm ((name, []), map ho_term_from_ho_type tys)
@@ -944,7 +934,7 @@
fun generic_add_sorts_on_type _ [] = I
| generic_add_sorts_on_type T (s :: ss) =
generic_add_sorts_on_type T ss
- #> (if s = the_single @{sort HOL.type} then I else insert (op =) (s, T))
+ #> (if s = the_single @{sort type} then I else insert (op =) (s, T))
fun add_sorts_on_tfree (T as TFree (_, S)) = generic_add_sorts_on_type T S
| add_sorts_on_tfree _ = I
fun add_sorts_on_tvar (T as TVar (_, S)) = generic_add_sorts_on_type T S
@@ -957,9 +947,9 @@
([], map_filter (Option.map ho_term_from_ho_type
o ho_type_for_type_arg type_enc) T_args)
-fun type_class_atom type_enc (class, T) =
+fun class_atom type_enc (cl, T) =
let
- val class = `make_type_class class
+ val cl = `make_class cl
val (ty_args, tm_args) = process_type_args type_enc [T]
val tm_args =
tm_args @
@@ -967,12 +957,15 @@
Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
[ATerm ((TYPE_name, ty_args), [])]
| _ => [])
- in AAtom (ATerm ((class, ty_args), tm_args)) end
-fun formulas_for_types type_enc add_sorts_on_typ Ts =
+ in AAtom (ATerm ((cl, ty_args), tm_args)) end
+
+fun class_atoms type_enc (cls, T) =
+ map (fn cl => class_atom type_enc (cl, T)) cls
+
+fun class_membs_for_types type_enc add_sorts_on_typ Ts =
[] |> (polymorphism_of_type_enc type_enc <> Type_Class_Polymorphic andalso
level_of_type_enc type_enc <> No_Types)
? fold add_sorts_on_typ Ts
- |> map (type_class_atom type_enc)
fun mk_aconns c = split_last #> uncurry (fold_rev (mk_aconn c))
@@ -1732,17 +1725,19 @@
case filter is_TVar Ts of
[] => I
| Ts =>
- (sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
+ (sorts ? mk_ahorn (Ts |> class_membs_for_types type_enc add_sorts_on_tvar
+ |> map (class_atom type_enc)))
#> (case type_enc of
Native (_, poly, _) =>
- mk_atyquant AForall (map (fn TVar (x, S) =>
- (AType (tvar_name x, []),
- if poly = Type_Class_Polymorphic then
- map (`make_type_class) S
- else
- [])) Ts)
+ mk_atyquant AForall
+ (map (fn TVar (z as (_, S)) =>
+ (AType (tvar_name z, []),
+ if poly = Type_Class_Polymorphic then
+ map (`make_class) (normalize_classes S)
+ else
+ [])) Ts)
| _ =>
- mk_aquant AForall (map (fn TVar (x, _) => (tvar_name x, NONE)) Ts))
+ mk_aquant AForall (map (fn TVar z => (tvar_name z, NONE)) Ts))
fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
(if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
@@ -1819,15 +1814,12 @@
fun set_insert (x, s) = Symtab.update (x, ()) s
-fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
-
-(* Remove this trivial type class (FIXME: similar code elsewhere) *)
-fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
+fun add_classes (cls, cset) = List.foldl set_insert cset (flat cls)
fun classes_of_terms get_Ts =
map (map snd o get_Ts)
- #> List.foldl add_classes Symtab.empty
- #> delete_type #> Symtab.keys
+ #> List.foldl add_classes Symtab.empty #> Symtab.delete_safe class_of_types
+ #> Symtab.keys
val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
@@ -1950,13 +1942,13 @@
val subs = tfree_classes_of_terms all_ts
val supers = tvar_classes_of_terms all_ts
val tycons = type_constrs_of_terms thy all_ts
- val (supers, arity_clauses) =
+ val (supers, tcon_clauses) =
if level_of_type_enc type_enc = No_Types then ([], [])
- else make_arity_clauses thy tycons supers
- val class_rel_clauses = make_class_rel_clauses thy subs supers
+ else make_tcon_clauses thy tycons supers
+ val subclass_pairs = make_subclass_pairs thy subs supers
in
(fact_names |> map single, union (op =) subs supers, conjs,
- facts @ lam_facts, class_rel_clauses, arity_clauses, lifted)
+ facts @ lam_facts, subclass_pairs, tcon_clauses, lifted)
end
val type_guard = `(make_fixed_const NONE) type_guard_name
@@ -2121,26 +2113,33 @@
end)
|> Formula
-fun formula_line_for_class_rel_clause type_enc
- ({name, subclass, superclass, ...} : class_rel_clause) =
- Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
+fun formula_lines_for_subclass type_enc sub super =
+ Formula (subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, Axiom,
AConn (AImplies,
- [type_class_atom type_enc (subclass, tvar_a),
- type_class_atom type_enc (superclass, tvar_a)])
+ [sub, super] |> map (fn s => class_atom type_enc (s, tvar_a)))
|> bound_tvars type_enc false [tvar_a],
NONE, isabelle_info inductiveN helper_rank)
-fun formula_line_for_arity_clause type_enc
- ({name, prems, concl} : arity_clause) =
- let
- val atomic_Ts = fold (fold_atyps (insert (op =)) o snd) (concl :: prems) []
- in
- Formula (arity_clause_prefix ^ name, Axiom,
- mk_ahorn (map (type_class_atom type_enc) prems)
- (type_class_atom type_enc concl)
- |> bound_tvars type_enc true atomic_Ts,
+fun formula_lines_for_subclass_pair type_enc (sub, supers) =
+ if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
+ [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub,
+ map (`make_class) supers)]
+ else
+ map (formula_lines_for_subclass type_enc sub) supers
+
+fun formula_line_for_tcon_clause type_enc (name, prems, (cl, T)) =
+ if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
+ Class_Memb (class_memb_prefix ^ name,
+ map (fn (cls, T) =>
+ (T |> dest_TVar |> tvar_name, map (`make_class) cls))
+ prems,
+ native_ho_type_from_typ type_enc false 0 T, `make_class cl)
+ else
+ Formula (tcon_clause_prefix ^ name, Axiom,
+ mk_ahorn (maps (class_atoms type_enc) prems)
+ (class_atom type_enc (cl, T))
+ |> bound_tvars type_enc true (snd (dest_Type T)),
NONE, isabelle_info inductiveN helper_rank)
- end
fun formula_line_for_conjecture ctxt mono type_enc
({name, role, iformula, atomic_types, ...} : ifact) =
@@ -2153,17 +2152,23 @@
fun formula_lines_for_free_types type_enc (facts : ifact list) =
let
- fun line j phi =
- Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
- val phis =
+ fun line j (cl, T) =
+ if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
+ Class_Memb (class_memb_prefix ^ string_of_int j, [],
+ native_ho_type_from_typ type_enc false 0 T,
+ `make_class cl)
+ else
+ Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
+ class_atom type_enc (cl, T), NONE, [])
+ val membs =
fold (union (op =)) (map #atomic_types facts) []
- |> formulas_for_types type_enc add_sorts_on_tfree
- in map2 line (0 upto length phis - 1) phis end
+ |> class_membs_for_types type_enc add_sorts_on_tfree
+ in map2 line (0 upto length membs - 1) membs end
(** Symbol declarations **)
fun decl_line_for_class phantoms s =
- let val name as (s, _) = `make_type_class s in
+ let val name as (s, _) = `make_class s in
Sym_Decl (sym_decl_prefix ^ s, name,
APi ([tvar_a_name],
if phantoms = Without_Phantom_Type_Vars then
@@ -2361,7 +2366,7 @@
T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
|> native_ho_type_from_typ type_enc pred_sym ary
|> not (null T_args)
- ? curry APi (map (tvar_name o fst o dest_TVar) T_args))
+ ? curry APi (map (tvar_name o dest_TVar) T_args))
end
fun honor_conj_sym_role in_conj =
@@ -2555,11 +2560,11 @@
val explicit_declsN = "Explicit typings"
val uncurried_alias_eqsN = "Uncurried aliases"
val factsN = "Relevant facts"
-val class_relsN = "Class relationships"
-val aritiesN = "Arities"
+val subclassesN = "Subclasses"
+val tconsN = "Type constructors"
val helpersN = "Helper facts"
val conjsN = "Conjectures"
-val free_typesN = "Type variables"
+val free_typesN = "Free types"
(* TFF allows implicit declarations of types, function symbols, and predicate
symbols (with "$i" as the type of individuals), but some provers (e.g.,
@@ -2576,6 +2581,7 @@
let
fun do_sym (name as (s, _)) value =
if is_tptp_user_symbol s then Symtab.default (s, (name, value)) else I
+ fun do_class name = apfst (apfst (do_sym name ()))
fun do_type (AType (name, tys)) =
apfst (apsnd (do_sym name (length tys))) #> fold do_type tys
| do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
@@ -2587,15 +2593,17 @@
| do_term _ (AAbs (((_, ty), tm), args)) =
do_type ty #> do_term false tm #> fold (do_term false) args
fun do_formula (ATyQuant (_, xs, phi)) =
- fold (do_type o fst) xs
- #> fold (fold (fn name => apfst (apfst (do_sym name ()))) o snd) xs
+ fold (do_type o fst) xs #> fold (fold do_class o snd) xs
#> do_formula phi
| do_formula (AQuant (_, xs, phi)) =
fold do_type (map_filter snd xs) #> do_formula phi
| do_formula (AConn (_, phis)) = fold do_formula phis
| do_formula (AAtom tm) = do_term true tm
- fun do_line (Type_Decl _) = I
+ fun do_line (Class_Decl (_, _, cls)) = fold do_class cls
+ | do_line (Type_Decl _) = I
| do_line (Sym_Decl (_, _, ty)) = do_type ty
+ | do_line (Class_Memb (_, xs, ty, cl)) =
+ fold (fold do_class o snd) xs #> do_type ty #> do_class cl
| do_line (Formula (_, _, phi, _, _)) = do_formula phi
val ((cls, tys), syms) = declared_in_atp_problem problem
in
@@ -2611,16 +2619,16 @@
val ((cls, tys), syms) = undeclared_in_problem problem
val decls =
Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
- | (s, (sym, ())) =>
- cons (Class_Decl (type_decl_prefix ^ s, sym, [])))
+ | (s, (cls, ())) =>
+ cons (Class_Decl (class_decl_prefix ^ s, cls, [])))
cls [] @
Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
- | (s, (sym, ary)) =>
- cons (Type_Decl (type_decl_prefix ^ s, sym, ary, [])))
+ | (s, (ty, ary)) =>
+ cons (Type_Decl (type_decl_prefix ^ s, ty, ary)))
tys [] @
Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
| (s, (sym, ty)) =>
- cons (Sym_Decl (type_decl_prefix ^ s, sym, ty ())))
+ cons (Sym_Decl (sym_decl_prefix ^ s, sym, ty ())))
syms []
in (heading, decls) :: problem end
@@ -2663,7 +2671,7 @@
liftingN
else
lam_trans
- val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses,
+ val (fact_names, classes, conjs, facts, subclass_pairs, tcon_clauses,
lifted) =
translate_formulas ctxt prem_role format type_enc lam_trans preproc hyp_ts
concl_t facts
@@ -2700,15 +2708,10 @@
map (formula_line_for_fact ctxt fact_prefix ascii_of (not exporter)
(not exporter) mono type_enc (rank_of_fact_num num_facts))
(0 upto num_facts - 1 ~~ facts)
- val (class_rel_lines, arity_lines, free_type_lines) =
- if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then
- ([],
- [],
- [])
- else
- (map (formula_line_for_class_rel_clause type_enc) class_rel_clauses,
- map (formula_line_for_arity_clause type_enc) arity_clauses,
- formula_lines_for_free_types type_enc (facts @ conjs))
+ val subclass_lines =
+ maps (formula_lines_for_subclass_pair type_enc) subclass_pairs
+ val tcon_lines = map (formula_line_for_tcon_clause type_enc) tcon_clauses
+ val free_type_lines = formula_lines_for_free_types type_enc (facts @ conjs)
val helper_lines =
0 upto length helpers - 1 ~~ helpers
|> map (formula_line_for_fact ctxt helper_prefix I false true mono
@@ -2718,8 +2721,8 @@
[(explicit_declsN, class_decl_lines @ sym_decl_lines),
(uncurried_alias_eqsN, uncurried_alias_eq_lines),
(factsN, fact_lines),
- (class_relsN, class_rel_lines),
- (aritiesN, arity_lines),
+ (subclassesN, subclass_lines),
+ (tconsN, tcon_lines),
(helpersN, helper_lines),
(free_typesN, free_type_lines),
(conjsN, map (formula_line_for_conjecture ctxt mono type_enc) conjs)]
@@ -2780,7 +2783,7 @@
|> add_conjectures_weights (get free_typesN @ get conjsN)
|> add_facts_weights (get factsN)
|> fold (fold (add_line_weights type_info_default_weight) o get)
- [explicit_declsN, class_relsN, aritiesN]
+ [explicit_declsN, subclassesN, tconsN]
|> Symtab.dest
|> sort (prod_ord Real.compare string_ord o pairself swap)
end