--- a/src/HOL/Tools/res_atp.ML Tue Nov 14 22:17:04 2006 +0100
+++ b/src/HOL/Tools/res_atp.ML Wed Nov 15 11:33:59 2006 +0100
@@ -660,6 +660,18 @@
let val sorts_list = map (map #2 o term_tfrees) ts
in Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list)) end;
+(*fold type constructors*)
+fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
+ | fold_type_consts f T x = x;
+
+val add_type_consts_in_type = fold_type_consts setinsert;
+
+val add_type_consts_in_term = fold_types add_type_consts_in_type;
+
+fun type_consts_of_terms ts =
+ Symtab.keys (fold add_type_consts_in_term ts Symtab.empty);
+
+
(***************************************************************)
(* ATP invocation methods setup *)
(***************************************************************)
@@ -708,12 +720,14 @@
user_cls (map prop_of goal_cls) |> make_unique
val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
val subs = tfree_classes_of_terms (map prop_of goal_cls)
- and supers = tvar_classes_of_terms (map (prop_of o #1) axclauses)
+ and axtms = map (prop_of o #1) axclauses
+ val supers = tvar_classes_of_terms axtms
+ and tycons = type_consts_of_terms axtms
(*TFrees in conjecture clauses; TVars in axiom clauses*)
val classrel_clauses =
if keep_types then ResClause.make_classrel_clauses thy subs supers
else []
- val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
+ val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers else []
val writer = if dfg then dfg_writer else tptp_writer
and file = atp_input_file()
and user_lemmas_names = map #1 user_rules
@@ -831,9 +845,6 @@
axcls_list
val keep_types = if is_fol_logic logic then !ResClause.keep_types
else is_typed_hol ()
- val arity_clauses = if keep_types then ResClause.arity_clause_thy thy
- else []
- val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
val writer = if !prover = "spass" then dfg_writer else tptp_writer
fun write_all [] [] _ = []
| write_all (ccls::ccls_list) (axcls::axcls_list) k =
@@ -841,12 +852,17 @@
val axcls = make_unique axcls
val ccls = subtract_cls ccls axcls
val subs = tfree_classes_of_terms (map prop_of ccls)
- and supers = tvar_classes_of_terms (map (prop_of o #1) axcls)
+ and axtms = map (prop_of o #1) axcls
+ val supers = tvar_classes_of_terms axtms
+ and tycons = type_consts_of_terms axtms
(*TFrees in conjecture clauses; TVars in axiom clauses*)
val classrel_clauses =
if keep_types then ResClause.make_classrel_clauses thy subs supers
else []
val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
+ val arity_clauses = if keep_types then ResClause.arity_clause_thy thy tycons supers
+ else []
+ val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
val thm_names = Array.fromList clnames
val _ = if !Output.show_debug_msgs
--- a/src/HOL/Tools/res_clause.ML Tue Nov 14 22:17:04 2006 +0100
+++ b/src/HOL/Tools/res_clause.ML Wed Nov 15 11:33:59 2006 +0100
@@ -490,8 +490,7 @@
| TVarLit of bool * (class * string);
datatype arityClause =
- ArityClause of {clause_id: clause_id,
- axiom_name: axiom_name,
+ ArityClause of {axiom_name: axiom_name,
kind: kind,
conclLit: arLit,
premLits: arLit list};
@@ -509,15 +508,14 @@
TConsLit(b, (make_type_class cls, make_fixed_type_const tcons, tvars));
(*Arity of type constructor tcon :: (arg1,...,argN)res*)
-fun make_axiom_arity_clause (tcons, n, (res,args)) =
+fun make_axiom_arity_clause (tcons, axiom_name, (res,args)) =
let val nargs = length args
val tvars = gen_TVars nargs
val tvars_srts = ListPair.zip (tvars,args)
val tvars_srts' = union_all(map pack_sort tvars_srts)
val false_tvars_srts' = map (pair false) tvars_srts'
in
- ArityClause {clause_id = n, kind = Axiom,
- axiom_name = lookup_type_const tcons,
+ ArityClause {axiom_name = axiom_name, kind = Axiom,
conclLit = make_TConsLit(true, (res,tcons,tvars)),
premLits = map make_TVarLit false_tvars_srts'}
end;
@@ -549,24 +547,34 @@
(** Isabelle arities **)
-fun arity_clause _ (tcons, []) = []
- | arity_clause n (tcons, ("HOL.type",_)::ars) = (*ignore*)
- arity_clause n (tcons,ars)
- | arity_clause n (tcons, ar::ars) =
- make_axiom_arity_clause (tcons,n,ar) ::
- arity_clause (n+1) (tcons,ars);
+fun arity_clause _ _ (tcons, []) = []
+ | arity_clause seen n (tcons, ("HOL.type",_)::ars) = (*ignore*)
+ arity_clause seen n (tcons,ars)
+ | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
+ if class mem_string seen then (*multiple arities for the same tycon, class pair*)
+ make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
+ arity_clause seen (n+1) (tcons,ars)
+ else
+ make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class, ar) ::
+ arity_clause (class::seen) n (tcons,ars)
fun multi_arity_clause [] = []
| multi_arity_clause ((tcons,ars) :: tc_arlists) =
- (*Reversal ensures that older entries always get the same axiom name*)
- arity_clause 0 (tcons, rev ars) @
+ arity_clause [] 1 (tcons, ars) @
multi_arity_clause tc_arlists
-fun arity_clause_thy thy =
- let val arities = thy |> Sign.classes_of
- |> Sorts.rep_algebra |> #arities |> Symtab.dest
- |> map (apsnd (map (fn (c, (_, Ss)) => (c, Ss))));
- in multi_arity_clause (rev arities) end;
+(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy.*)
+fun type_class_pairs thy tycons classes =
+ let val alg = Sign.classes_of thy
+ fun domain_sorts (tycon,class) = Sorts.mg_domain alg tycon [class]
+ fun add_class tycon (class,pairs) =
+ (class, domain_sorts(tycon,class))::pairs
+ handle Sorts.CLASS_ERROR _ => pairs
+ fun try_classes tycon = (tycon, foldl (add_class tycon) [] classes)
+ in map try_classes tycons end;
+
+fun arity_clause_thy thy tycons classes =
+ multi_arity_clause (type_class_pairs thy tycons classes);
(**** Find occurrences of predicates in clauses ****)
@@ -594,9 +602,14 @@
fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) =
Symtab.update (subclass,1) (Symtab.update (superclass,1) preds);
-fun add_arityClause_preds (ArityClause {conclLit,...}, preds) =
- let val TConsLit(_, (tclass, _, _)) = conclLit
- in Symtab.update (tclass,1) preds end;
+(*Not sure the TVar case is ever used*)
+fun class_of_arityLit (TConsLit(_, (tclass, _, _))) = tclass
+ | class_of_arityLit (TVarLit(_, (tclass, _))) = tclass;
+
+fun add_arityClause_preds (ArityClause {conclLit,premLits,...}, preds) =
+ let val classes = map class_of_arityLit (conclLit::premLits)
+ fun upd (class,preds) = Symtab.update (class,1) preds
+ in foldl upd preds classes end;
fun preds_of_clauses clauses clsrel_clauses arity_clauses =
Symtab.dest
@@ -755,8 +768,8 @@
fun dfg_tfree_clause tfree_lit =
"clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n"
-fun string_of_arClauseID (ArityClause {clause_id,axiom_name,...}) =
- arclause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id;
+fun string_of_arClauseID (ArityClause {axiom_name,...}) =
+ arclause_prefix ^ ascii_of axiom_name;
fun dfg_of_arLit (TConsLit(pol,(c,t,args))) =
dfg_sign pol (c ^ "(" ^ t ^ paren_pack args ^ ")")