# HG changeset patch # User paulson # Date 1163586839 -3600 # Node ID 18f519614978a48d1271efb256926592316e508e # Parent 4a0a83378669827c2a14768536f89820f579f807 Arity clauses are now produced only for types and type classes actually used. diff -r 4a0a83378669 -r 18f519614978 src/HOL/Tools/res_atp.ML --- 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 diff -r 4a0a83378669 -r 18f519614978 src/HOL/Tools/res_clause.ML --- 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 ^ ")")