more abstract interface to classes/arities;
authorwenzelm
Tue May 16 13:01:24 2006 +0200 (2006-05-16)
changeset 19642ea7162f84677
parent 19641 f1de44e61ec1
child 19643 213e12ad2c03
more abstract interface to classes/arities;
src/HOL/Tools/refute.ML
src/HOL/Tools/res_clause.ML
src/Pure/axclass.ML
src/Pure/display.ML
src/Pure/sign.ML
src/Pure/type.ML
     1.1 --- a/src/HOL/Tools/refute.ML	Tue May 16 13:01:23 2006 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Tue May 16 13:01:24 2006 +0200
     1.3 @@ -507,7 +507,7 @@
     1.4  					| _               => raise REFUTE ("collect_axioms", "type " ^ Sign.string_of_typ (sign_of thy) T ^ " is not a variable"))
     1.5  				(* obtain all superclasses of classes in 'sort' *)
     1.6  				(* string list *)
     1.7 -				val superclasses = Graph.all_succs ((#2 o #classes o Type.rep_tsig o Sign.tsig_of o sign_of) thy) sort
     1.8 +				val superclasses = distinct (op =) (sort @ maps (Sign.super_classes thy) sort)
     1.9  			in
    1.10  				Library.foldl collect_class_axioms (axs, superclasses)
    1.11  			end
     2.1 --- a/src/HOL/Tools/res_clause.ML	Tue May 16 13:01:23 2006 +0200
     2.2 +++ b/src/HOL/Tools/res_clause.ML	Tue May 16 13:01:24 2006 +0200
     2.3 @@ -689,12 +689,8 @@
     2.4  
     2.5  fun classrelClauses_of (sub,sups) = classrelClauses_of_aux 0 sub sups;
     2.6  
     2.7 -val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of;
     2.8 -
     2.9 -fun classrel_clauses_classrel (C: Sorts.classes) =
    2.10 -  map classrelClauses_of (Graph.dest C);
    2.11 -
    2.12 -val classrel_clauses_thy = List.concat o classrel_clauses_classrel o classrel_of;
    2.13 +val classrel_clauses_thy =
    2.14 +  maps classrelClauses_of o Graph.dest o #classes o Sorts.rep_algebra o Sign.classes_of;
    2.15  
    2.16  
    2.17  (** Isabelle arities **)
    2.18 @@ -713,8 +709,9 @@
    2.19        multi_arity_clause tc_arlists 
    2.20  
    2.21  fun arity_clause_thy thy =
    2.22 -  let val arities =
    2.23 -    Symtab.dest (Sign.arities_of thy) |> map (apsnd (map (fn (c, (_, Ss)) => (c, Ss))));
    2.24 +  let val arities = thy |> Sign.classes_of
    2.25 +    |> Sorts.rep_algebra |> #arities |> Symtab.dest
    2.26 +    |> map (apsnd (map (fn (c, (_, Ss)) => (c, Ss))));
    2.27    in multi_arity_clause (rev arities) end;
    2.28  
    2.29  
     3.1 --- a/src/Pure/axclass.ML	Tue May 16 13:01:23 2006 +0200
     3.2 +++ b/src/Pure/axclass.ML	Tue May 16 13:01:24 2006 +0200
     3.3 @@ -392,8 +392,7 @@
     3.4                | _ => I) typ [];
     3.5          val hyps = vars
     3.6            |> map (fn (T, S) => (T, Drule.sort_triv thy (T, S) ~~ S));
     3.7 -        val ths = (typ, sort)
     3.8 -          |> Sorts.of_sort_derivation (Sign.pp thy) (Sign.classes_of thy, Sign.arities_of thy)
     3.9 +        val ths = (typ, sort) |> Sorts.of_sort_derivation (Sign.pp thy) (Sign.classes_of thy)
    3.10             {classrel =
    3.11                fn (th, c1) => fn c2 => th RS the_classrel thy (c1, c2),
    3.12              constructor =
     4.1 --- a/src/Pure/display.ML	Tue May 16 13:01:23 2006 +0200
     4.2 +++ b/src/Pure/display.ML	Tue May 16 13:01:24 2006 +0200
     4.3 @@ -212,9 +212,11 @@
     4.4      val {axioms, defs = _, oracles} = Theory.rep_theory thy;
     4.5      val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
     4.6      val {constants, constraints} = Consts.dest consts;
     4.7 -    val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
     4.8 +    val {classes = (class_space, class_algebra),
     4.9 +      default, types, log_types = _, witness} = Type.rep_tsig tsig;
    4.10 +    val {classes, arities} = Sorts.rep_algebra class_algebra;
    4.11  
    4.12 -    val clsses = NameSpace.dest_table (apsnd (Symtab.make o Graph.dest) classes);
    4.13 +    val clsses = NameSpace.dest_table (class_space, Symtab.make (Graph.dest classes));
    4.14      val tdecls = NameSpace.dest_table types;
    4.15      val arties = NameSpace.dest_table (Sign.type_space thy, arities);
    4.16      val cnsts = NameSpace.extern_table constants;
     5.1 --- a/src/Pure/sign.ML	Tue May 16 13:01:23 2006 +0200
     5.2 +++ b/src/Pure/sign.ML	Tue May 16 13:01:24 2006 +0200
     5.3 @@ -94,8 +94,7 @@
     5.4    val declare_name: theory -> string -> NameSpace.T -> NameSpace.T
     5.5    val syn_of: theory -> Syntax.syntax
     5.6    val tsig_of: theory -> Type.tsig
     5.7 -  val classes_of: theory -> Sorts.classes
     5.8 -  val arities_of: theory -> Sorts.arities
     5.9 +  val classes_of: theory -> Sorts.algebra
    5.10    val classes: theory -> class list
    5.11    val super_classes: theory -> class -> class list
    5.12    val defaultS: theory -> sort
    5.13 @@ -267,10 +266,9 @@
    5.14  (* type signature *)
    5.15  
    5.16  val tsig_of = #tsig o rep_sg;
    5.17 -val classes_of = snd o #classes o Type.rep_tsig o tsig_of;
    5.18 -val arities_of = #arities o Type.rep_tsig o tsig_of;
    5.19 -val classes = Type.classes o tsig_of;
    5.20 -val super_classes = Graph.imm_succs o classes_of;
    5.21 +val classes_of = #2 o #classes o Type.rep_tsig o tsig_of;
    5.22 +val classes = Sorts.classes o classes_of;
    5.23 +val super_classes = Sorts.super_classes o classes_of;
    5.24  val defaultS = Type.defaultS o tsig_of;
    5.25  val subsort = Type.subsort o tsig_of;
    5.26  val of_sort = Type.of_sort o tsig_of;
     6.1 --- a/src/Pure/type.ML	Tue May 16 13:01:23 2006 +0200
     6.2 +++ b/src/Pure/type.ML	Tue May 16 13:01:24 2006 +0200
     6.3 @@ -15,14 +15,12 @@
     6.4      Nonterminal
     6.5    type tsig
     6.6    val rep_tsig: tsig ->
     6.7 -   {classes: NameSpace.T * Sorts.classes,
     6.8 +   {classes: NameSpace.T * Sorts.algebra,
     6.9      default: sort,
    6.10      types: (decl * stamp) NameSpace.table,
    6.11 -    arities: Sorts.arities,
    6.12      log_types: string list,
    6.13      witness: (typ * sort) option}
    6.14    val empty_tsig: tsig
    6.15 -  val classes: tsig -> class list
    6.16    val defaultS: tsig -> sort
    6.17    val logical_types: tsig -> string list
    6.18    val universal_witness: tsig -> (typ * sort) option
    6.19 @@ -98,57 +96,51 @@
    6.20  
    6.21  datatype tsig =
    6.22    TSig of {
    6.23 -    classes: NameSpace.T * Sorts.classes,   (*declared classes with proper subclass relation*)
    6.24 +    classes: NameSpace.T * Sorts.algebra,   (*order-sorted algebra of type classes*)
    6.25      default: sort,                          (*default sort on input*)
    6.26      types: (decl * stamp) NameSpace.table,  (*declared types*)
    6.27 -    arities: Sorts.arities,                 (*image specification of types wrt. sorts*)
    6.28      log_types: string list,                 (*logical types sorted by number of arguments*)
    6.29      witness: (typ * sort) option};          (*witness for non-emptiness of strictest sort*)
    6.30  
    6.31  fun rep_tsig (TSig comps) = comps;
    6.32  
    6.33 -fun make_tsig (classes, default, types, arities, log_types, witness) =
    6.34 -  TSig {classes = classes, default = default, types = types, arities = arities,
    6.35 +fun make_tsig (classes, default, types, log_types, witness) =
    6.36 +  TSig {classes = classes, default = default, types = types,
    6.37      log_types = log_types, witness = witness};
    6.38  
    6.39 -fun build_tsig (classes, default, types, arities) =
    6.40 +fun build_tsig ((space, classes), default, types) =
    6.41    let
    6.42      val log_types =
    6.43        Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (snd types) []
    6.44        |> Library.sort (Library.int_ord o pairself snd) |> map fst;
    6.45      val witness =
    6.46 -      (case Sorts.witness_sorts (snd classes, arities) log_types [] [Graph.keys (snd classes)] of
    6.47 +      (case Sorts.witness_sorts classes log_types [] [Sorts.classes classes] of
    6.48          [w] => SOME w | _ => NONE);
    6.49 -  in make_tsig (classes, default, types, arities, log_types, witness) end;
    6.50 +  in make_tsig ((space, classes), default, types, log_types, witness) end;
    6.51  
    6.52 -fun map_tsig f (TSig {classes, default, types, arities, log_types = _, witness = _}) =
    6.53 -  build_tsig (f (classes, default, types, arities));
    6.54 +fun map_tsig f (TSig {classes, default, types, log_types = _, witness = _}) =
    6.55 +  build_tsig (f (classes, default, types));
    6.56  
    6.57  val empty_tsig =
    6.58 -  build_tsig ((NameSpace.empty, Graph.empty), [], NameSpace.empty_table, Symtab.empty);
    6.59 +  build_tsig ((NameSpace.empty, Sorts.empty_algebra), [], NameSpace.empty_table);
    6.60  
    6.61  
    6.62  (* classes and sorts *)
    6.63  
    6.64 -fun classes (TSig {classes = (_, C), ...}) = Graph.keys C;
    6.65  fun defaultS (TSig {default, ...}) = default;
    6.66  fun logical_types (TSig {log_types, ...}) = log_types;
    6.67  fun universal_witness (TSig {witness, ...}) = witness;
    6.68  
    6.69  fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq (#2 classes);
    6.70  fun subsort (TSig {classes, ...}) = Sorts.sort_le (#2 classes);
    6.71 -fun of_sort (TSig {classes, arities, ...}) = Sorts.of_sort (#2 classes, arities);
    6.72 +fun of_sort (TSig {classes, ...}) = Sorts.of_sort (#2 classes);
    6.73  fun inter_sort (TSig {classes, ...}) = Sorts.inter_sort (#2 classes);
    6.74  
    6.75 -fun cert_class (TSig {classes, ...}) c =
    6.76 -  if can (Graph.get_node (#2 classes)) c then c
    6.77 -  else raise TYPE ("Undeclared class: " ^ quote c, [], []);
    6.78 +fun cert_class (TSig {classes, ...}) = Sorts.certify_class (#2 classes);
    6.79 +fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort (#2 classes);
    6.80  
    6.81 -fun cert_sort (tsig as TSig {classes, ...}) =
    6.82 -  Sorts.norm_sort (#2 classes) o map (cert_class tsig);
    6.83 -
    6.84 -fun witness_sorts (tsig as TSig {classes, arities, log_types, ...}) =
    6.85 -  Sorts.witness_sorts (#2 classes, arities) log_types;
    6.86 +fun witness_sorts (tsig as TSig {classes, log_types, ...}) =
    6.87 +  Sorts.witness_sorts (#2 classes) log_types;
    6.88  
    6.89  
    6.90  (* certified types *)
    6.91 @@ -211,9 +203,8 @@
    6.92    | _ => error (undecl_type a));
    6.93  
    6.94  fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
    6.95 -  | arity_sorts pp (TSig {classes, arities, ...}) a S =
    6.96 -      Sorts.mg_domain (#2 classes, arities) a S
    6.97 -        handle Sorts.CLASS_ERROR err => Sorts.class_error pp err;
    6.98 +  | arity_sorts pp (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S
    6.99 +      handle Sorts.CLASS_ERROR err => Sorts.class_error pp err;
   6.100  
   6.101  
   6.102  
   6.103 @@ -379,13 +370,13 @@
   6.104    | devar tye T = T;
   6.105  
   6.106  (*order-sorted unification*)
   6.107 -fun unify (tsig as TSig {classes = (_, classes), arities, ...}) TU (tyenv, maxidx) =
   6.108 +fun unify (tsig as TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) =
   6.109    let
   6.110      val tyvar_count = ref maxidx;
   6.111      fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
   6.112  
   6.113 -    fun mg_domain a S =
   6.114 -      Sorts.mg_domain (classes, arities) a S handle Sorts.CLASS_ERROR _ => raise TUNIFY;
   6.115 +    fun mg_domain a S = Sorts.mg_domain classes a S
   6.116 +      handle Sorts.CLASS_ERROR _ => raise TUNIFY;
   6.117  
   6.118      fun meet (_, []) tye = tye
   6.119        | meet (TVar (xi, S'), S) tye =
   6.120 @@ -470,22 +461,22 @@
   6.121  (* classes *)
   6.122  
   6.123  fun add_class pp naming (c, cs) tsig =
   6.124 -  tsig |> map_tsig (fn ((space, classes), default, types, arities) =>
   6.125 +  tsig |> map_tsig (fn ((space, classes), default, types) =>
   6.126      let
   6.127        val c' = NameSpace.full naming c;
   6.128        val cs' = map (cert_class tsig) cs
   6.129          handle TYPE (msg, _, _) => error msg;
   6.130        val space' = space |> NameSpace.declare naming c';
   6.131        val classes' = classes |> Sorts.add_class pp (c', cs');
   6.132 -    in ((space', classes'), default, types, arities) end);
   6.133 +    in ((space', classes'), default, types) end);
   6.134  
   6.135 -fun hide_classes fully cs = map_tsig (fn ((space, classes), default, types, arities) =>
   6.136 -  ((fold (NameSpace.hide fully) cs space, classes), default, types, arities));
   6.137 +fun hide_classes fully cs = map_tsig (fn ((space, classes), default, types) =>
   6.138 +  ((fold (NameSpace.hide fully) cs space, classes), default, types));
   6.139  
   6.140  
   6.141  (* arities *)
   6.142  
   6.143 -fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn (classes, default, types, arities) =>
   6.144 +fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
   6.145    let
   6.146      val _ =
   6.147        (case Symtab.lookup (#2 types) t of
   6.148 @@ -494,27 +485,25 @@
   6.149        | NONE => error (undecl_type t));
   6.150      val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
   6.151        handle TYPE (msg, _, _) => error msg;
   6.152 -    val arities' = arities |> Sorts.add_arities pp (#2 classes) ((t, map (fn c' => (c', Ss')) S'));
   6.153 -  in (classes, default, types, arities') end);
   6.154 +    val classes' = classes |> Sorts.add_arities pp ((t, map (fn c' => (c', Ss')) S'));
   6.155 +  in ((space, classes'), default, types) end);
   6.156  
   6.157  
   6.158  (* classrel *)
   6.159  
   6.160  fun add_classrel pp rel tsig =
   6.161 -  tsig |> map_tsig (fn ((space, classes), default, types, arities) =>
   6.162 +  tsig |> map_tsig (fn ((space, classes), default, types) =>
   6.163      let
   6.164        val rel' = pairself (cert_class tsig) rel
   6.165          handle TYPE (msg, _, _) => error msg;
   6.166        val classes' = classes |> Sorts.add_classrel pp rel;
   6.167 -      val default' = default |> Sorts.norm_sort classes';
   6.168 -      val arities' = arities |> Sorts.rebuild_arities pp classes';
   6.169 -    in ((space, classes'), default', types, arities') end);
   6.170 +    in ((space, classes'), default, types) end);
   6.171  
   6.172  
   6.173  (* default sort *)
   6.174  
   6.175 -fun set_defsort S tsig = tsig |> map_tsig (fn (classes, _, types, arities) =>
   6.176 -  (classes, cert_sort tsig S handle TYPE (msg, _, _) => error msg, types, arities));
   6.177 +fun set_defsort S tsig = tsig |> map_tsig (fn (classes, _, types) =>
   6.178 +  (classes, cert_sort tsig S handle TYPE (msg, _, _) => error msg, types));
   6.179  
   6.180  
   6.181  (* types *)
   6.182 @@ -542,11 +531,11 @@
   6.183  
   6.184  fun the_decl (_, types) = fst o the o Symtab.lookup types;
   6.185  
   6.186 -fun map_types f = map_tsig (fn (classes, default, types, arities) =>
   6.187 +fun map_types f = map_tsig (fn (classes, default, types) =>
   6.188    let
   6.189      val (space', tab') = f types;
   6.190      val _ = assert (NameSpace.intern space' "dummy" = "dummy") "Illegal declaration of dummy type";
   6.191 -  in (classes, default, (space', tab'), arities) end);
   6.192 +  in (classes, default, (space', tab')) end);
   6.193  
   6.194  fun syntactic types (Type (c, Ts)) =
   6.195        (case Symtab.lookup types c of SOME (Nonterminal, _) => true | _ => false)
   6.196 @@ -583,8 +572,8 @@
   6.197  
   6.198  end;
   6.199  
   6.200 -fun hide_types fully cs = map_tsig (fn (classes, default, (space, types), arities) =>
   6.201 -  (classes, default, (fold (NameSpace.hide fully) cs space, types), arities));
   6.202 +fun hide_types fully cs = map_tsig (fn (classes, default, (space, types)) =>
   6.203 +  (classes, default, (fold (NameSpace.hide fully) cs space, types)));
   6.204  
   6.205  
   6.206  (* merge type signatures *)
   6.207 @@ -592,15 +581,14 @@
   6.208  fun merge_tsigs pp (tsig1, tsig2) =
   6.209    let
   6.210      val (TSig {classes = (space1, classes1), default = default1, types = types1,
   6.211 -      arities = arities1, log_types = _, witness = _}) = tsig1;
   6.212 +      log_types = _, witness = _}) = tsig1;
   6.213      val (TSig {classes = (space2, classes2), default = default2, types = types2,
   6.214 -      arities = arities2, log_types = _, witness = _}) = tsig2;
   6.215 +      log_types = _, witness = _}) = tsig2;
   6.216  
   6.217      val space' = NameSpace.merge (space1, space2);
   6.218 -    val classes' = Sorts.merge_classes pp (classes1, classes2);
   6.219 +    val classes' = Sorts.merge_algebra pp (classes1, classes2);
   6.220      val default' = Sorts.inter_sort classes' (default1, default2);
   6.221      val types' = merge_types (types1, types2);
   6.222 -    val arities' = Sorts.merge_arities pp classes' (arities1, arities2);
   6.223 -  in build_tsig ((space', classes'), default', types', arities') end;
   6.224 +  in build_tsig ((space', classes'), default', types') end;
   6.225  
   6.226  end;