src/HOL/Tools/res_clause.ML
changeset 21373 18f519614978
parent 21290 33b6bb5d6ab8
child 21416 f23e4e75dfd3
     1.1 --- a/src/HOL/Tools/res_clause.ML	Tue Nov 14 22:17:04 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Nov 15 11:33:59 2006 +0100
     1.3 @@ -490,8 +490,7 @@
     1.4                 | TVarLit of bool * (class * string);
     1.5   
     1.6  datatype arityClause =  
     1.7 -	 ArityClause of {clause_id: clause_id,
     1.8 -	  	         axiom_name: axiom_name,
     1.9 +	 ArityClause of {axiom_name: axiom_name,
    1.10  			 kind: kind,
    1.11  			 conclLit: arLit,
    1.12  			 premLits: arLit list};
    1.13 @@ -509,15 +508,14 @@
    1.14        TConsLit(b, (make_type_class cls, make_fixed_type_const tcons, tvars));
    1.15  
    1.16  (*Arity of type constructor tcon :: (arg1,...,argN)res*)
    1.17 -fun make_axiom_arity_clause (tcons, n, (res,args)) =
    1.18 +fun make_axiom_arity_clause (tcons, axiom_name, (res,args)) =
    1.19     let val nargs = length args
    1.20         val tvars = gen_TVars nargs
    1.21         val tvars_srts = ListPair.zip (tvars,args)
    1.22         val tvars_srts' = union_all(map pack_sort tvars_srts)
    1.23         val false_tvars_srts' = map (pair false) tvars_srts'
    1.24     in
    1.25 -      ArityClause {clause_id = n, kind = Axiom, 
    1.26 -                   axiom_name = lookup_type_const tcons,
    1.27 +      ArityClause {axiom_name = axiom_name, kind = Axiom, 
    1.28                     conclLit = make_TConsLit(true, (res,tcons,tvars)), 
    1.29                     premLits = map make_TVarLit false_tvars_srts'}
    1.30     end;
    1.31 @@ -549,24 +547,34 @@
    1.32  
    1.33  (** Isabelle arities **)
    1.34  
    1.35 -fun arity_clause _ (tcons, []) = []
    1.36 -  | arity_clause n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
    1.37 -      arity_clause n (tcons,ars)
    1.38 -  | arity_clause n (tcons, ar::ars) =
    1.39 -      make_axiom_arity_clause (tcons,n,ar) :: 
    1.40 -      arity_clause (n+1) (tcons,ars);
    1.41 +fun arity_clause _ _ (tcons, []) = []
    1.42 +  | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
    1.43 +      arity_clause seen n (tcons,ars)
    1.44 +  | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
    1.45 +      if class mem_string seen then (*multiple arities for the same tycon, class pair*)
    1.46 +	  make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: 
    1.47 +	  arity_clause seen (n+1) (tcons,ars)
    1.48 +      else
    1.49 +	  make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class, ar) :: 
    1.50 +	  arity_clause (class::seen) n (tcons,ars)
    1.51  
    1.52  fun multi_arity_clause [] = []
    1.53    | multi_arity_clause ((tcons,ars) :: tc_arlists) =
    1.54 -      (*Reversal ensures that older entries always get the same axiom name*)
    1.55 -      arity_clause 0 (tcons, rev ars)  @  
    1.56 +      arity_clause [] 1 (tcons, ars)  @  
    1.57        multi_arity_clause tc_arlists 
    1.58  
    1.59 -fun arity_clause_thy thy =
    1.60 -  let val arities = thy |> Sign.classes_of
    1.61 -    |> Sorts.rep_algebra |> #arities |> Symtab.dest
    1.62 -    |> map (apsnd (map (fn (c, (_, Ss)) => (c, Ss))));
    1.63 -  in multi_arity_clause (rev arities) end;
    1.64 +(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy.*)
    1.65 +fun type_class_pairs thy tycons classes =
    1.66 +  let val alg = Sign.classes_of thy
    1.67 +      fun domain_sorts (tycon,class) = Sorts.mg_domain alg tycon [class]
    1.68 +      fun add_class tycon (class,pairs) = 
    1.69 +            (class, domain_sorts(tycon,class))::pairs 
    1.70 +            handle Sorts.CLASS_ERROR _ => pairs
    1.71 +      fun try_classes tycon = (tycon, foldl (add_class tycon) [] classes)
    1.72 +  in  map try_classes tycons  end;
    1.73 +
    1.74 +fun arity_clause_thy thy tycons classes =
    1.75 +  multi_arity_clause (type_class_pairs thy tycons classes);
    1.76  
    1.77  
    1.78  (**** Find occurrences of predicates in clauses ****)
    1.79 @@ -594,9 +602,14 @@
    1.80  fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) =
    1.81    Symtab.update (subclass,1) (Symtab.update (superclass,1) preds);
    1.82  
    1.83 -fun add_arityClause_preds (ArityClause {conclLit,...}, preds) =
    1.84 -  let val TConsLit(_, (tclass, _, _)) = conclLit
    1.85 -  in  Symtab.update (tclass,1) preds  end;
    1.86 +(*Not sure the TVar case is ever used*)
    1.87 +fun class_of_arityLit (TConsLit(_, (tclass, _, _))) = tclass
    1.88 +  | class_of_arityLit (TVarLit(_, (tclass, _))) = tclass;
    1.89 +
    1.90 +fun add_arityClause_preds (ArityClause {conclLit,premLits,...}, preds) =
    1.91 +  let val classes = map class_of_arityLit (conclLit::premLits)
    1.92 +      fun upd (class,preds) = Symtab.update (class,1) preds
    1.93 +  in  foldl upd preds classes  end;
    1.94  
    1.95  fun preds_of_clauses clauses clsrel_clauses arity_clauses = 
    1.96    Symtab.dest
    1.97 @@ -755,8 +768,8 @@
    1.98  fun dfg_tfree_clause tfree_lit =
    1.99    "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n"
   1.100  
   1.101 -fun string_of_arClauseID (ArityClause {clause_id,axiom_name,...}) =
   1.102 -    arclause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id;
   1.103 +fun string_of_arClauseID (ArityClause {axiom_name,...}) =
   1.104 +    arclause_prefix ^ ascii_of axiom_name;
   1.105  
   1.106  fun dfg_of_arLit (TConsLit(pol,(c,t,args))) =
   1.107        dfg_sign pol (c ^ "(" ^ t ^ paren_pack args ^ ")")