Corrected a silly old bug in merge_tsigs.
authornipkow
Fri Mar 17 15:52:55 1995 +0100 (1995-03-17)
changeset 9637a78fda77104
parent 962 136308504cd9
child 964 5f690b184f91
Corrected a silly old bug in merge_tsigs.
Rewrote a lot of Nimmermann's code.
src/Pure/sign.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/sign.ML	Fri Mar 17 15:49:37 1995 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Mar 17 15:52:55 1995 +0100
     1.3 @@ -138,7 +138,7 @@
     1.4      fun pretty_default cls = Pretty.block
     1.5        [Pretty.str "default:", Pretty.brk 1, pretty_sort cls];
     1.6  
     1.7 -    fun pretty_arg (ty, n) = Pretty.str (ty ^ " " ^ string_of_int n);
     1.8 +    fun pretty_ty (ty, n) = Pretty.str (ty ^ " " ^ string_of_int n);
     1.9  
    1.10      fun pretty_abbr syn (ty, (vs, rhs)) = Pretty.block
    1.11        [prt_typ syn (Type (ty, map (fn v => TVar ((v, 0), [])) vs)),
    1.12 @@ -151,24 +151,26 @@
    1.13              Pretty.list "(" ")" (map pretty_sort srts),
    1.14              Pretty.brk 1, Pretty.str cl];
    1.15  
    1.16 -    fun pretty_coreg (ty, ars) = map (pretty_arity ty) ars;
    1.17 +    fun pretty_arities (ty, ars) = map (pretty_arity ty) ars;
    1.18  
    1.19      fun pretty_const syn (c, ty) = Pretty.block
    1.20        [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ syn ty];
    1.21  
    1.22  
    1.23      val Sg {tsig, const_tab, syn, stamps} = sg;
    1.24 -    val {classes, subclass, default, args, abbrs, coreg} = rep_tsig tsig;
    1.25 +    val {classes, subclass, default, tycons, abbrs, arities} = rep_tsig tsig;
    1.26    in
    1.27      Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps));
    1.28      Pretty.writeln (Pretty.strs ("classes:" :: classes));
    1.29 -    Pretty.writeln (Pretty.big_list "subclass:" (map pretty_subclass subclass));
    1.30 +    Pretty.writeln (Pretty.big_list "subclass:"
    1.31 +                      (map pretty_subclass subclass));
    1.32      Pretty.writeln (pretty_default default);
    1.33 -    Pretty.writeln (Pretty.big_list "types:" (map pretty_arg args));
    1.34 +    Pretty.writeln (Pretty.big_list "types:" (map pretty_ty tycons));
    1.35      Pretty.writeln (Pretty.big_list "abbrs:" (map (pretty_abbr syn) abbrs));
    1.36 -    Pretty.writeln (Pretty.big_list "coreg:" (flat (map pretty_coreg coreg)));
    1.37 +    Pretty.writeln (Pretty.big_list "arities:"
    1.38 +                      (flat (map pretty_arities arities)));
    1.39      Pretty.writeln (Pretty.big_list "consts:"
    1.40 -      (map (pretty_const syn) (Symtab.dest const_tab)))
    1.41 +                      (map (pretty_const syn) (Symtab.dest const_tab)))
    1.42    end;
    1.43  
    1.44  
     2.1 --- a/src/Pure/type.ML	Fri Mar 17 15:49:37 1995 +0100
     2.2 +++ b/src/Pure/type.ML	Fri Mar 17 15:52:55 1995 +0100
     2.3 @@ -6,7 +6,6 @@
     2.4  
     2.5  TODO:
     2.6    move type unification and inference to type_unify.ML (TypeUnify) (?)
     2.7 -  rename args -> tycons, coreg -> arities (?)
     2.8  *)
     2.9  
    2.10  signature TYPE =
    2.11 @@ -23,9 +22,9 @@
    2.12      {classes: class list,
    2.13       subclass: (class * class list) list,
    2.14       default: sort,
    2.15 -     args: (string * int) list,
    2.16 +     tycons: (string * int) list,
    2.17       abbrs: (string * (string list * typ)) list,
    2.18 -     coreg: (string * (class * sort list) list) list}
    2.19 +     arities: (string * (class * sort list) list) list}
    2.20    val defaultS: type_sig -> sort
    2.21    val tsig0: type_sig
    2.22    val logical_types: type_sig -> string list
    2.23 @@ -34,7 +33,7 @@
    2.24    val ext_tsig_defsort: type_sig -> sort -> type_sig
    2.25    val ext_tsig_types: type_sig -> (string * int) list -> type_sig
    2.26    val ext_tsig_abbrs: type_sig -> (string * string list * typ) list -> type_sig
    2.27 -  val ext_tsig_arities: type_sig -> (string * sort list * sort) list -> type_sig
    2.28 +  val ext_tsig_arities: type_sig -> (string * sort list * sort)list -> type_sig
    2.29    val merge_tsigs: type_sig * type_sig -> type_sig
    2.30    val subsort: type_sig -> sort * sort -> bool
    2.31    val norm_sort: type_sig -> sort -> sort
    2.32 @@ -134,14 +133,14 @@
    2.33    default:
    2.34      the default sort attached to all unconstrained type vars;
    2.35  
    2.36 -  args:
    2.37 +  tycons:
    2.38      an association list of all declared types with the number of their
    2.39      arguments;
    2.40  
    2.41    abbrs:
    2.42      an association list of type abbreviations;
    2.43  
    2.44 -  coreg:
    2.45 +  arities:
    2.46      a two-fold association list of all type arities; (t, al) means that type
    2.47      constructor t has the arities in al; an element (c, ss) of al represents
    2.48      the arity (ss)c;
    2.49 @@ -152,9 +151,9 @@
    2.50      classes: class list,
    2.51      subclass: (class * class list) list,
    2.52      default: sort,
    2.53 -    args: (string * int) list,
    2.54 +    tycons: (string * int) list,
    2.55      abbrs: (string * (string list * typ)) list,
    2.56 -    coreg: (string * (class * domain) list) list};
    2.57 +    arities: (string * (class * domain) list) list};
    2.58  
    2.59  fun rep_tsig (TySg comps) = comps;
    2.60  
    2.61 @@ -203,12 +202,12 @@
    2.62  
    2.63  fun logical_types tsig =
    2.64    let
    2.65 -    val TySg {subclass, coreg, args, ...} = tsig;
    2.66 +    val TySg {subclass, arities, tycons, ...} = tsig;
    2.67  
    2.68      fun log_class c = leq subclass (c, logicC);
    2.69 -    fun log_type t = exists (log_class o #1) (assocs coreg t);
    2.70 +    fun log_type t = exists (log_class o #1) (assocs arities t);
    2.71    in
    2.72 -    filter log_type (map #1 args)
    2.73 +    filter log_type (map #1 tycons)
    2.74    end;
    2.75  
    2.76  
    2.77 @@ -303,12 +302,12 @@
    2.78  (* 'least_sort' returns for a given type its maximum sort:
    2.79     - type variables, free types: the sort brought with
    2.80     - type constructors: recursive determination of the maximum sort of the
    2.81 -                    arguments if the type is declared in 'coreg' of the
    2.82 +                    arguments if the type is declared in 'arities' of the
    2.83                      given type signature  *)
    2.84  
    2.85 -fun least_sort (tsig as TySg{subclass, coreg, ...}) =
    2.86 +fun least_sort (tsig as TySg{subclass, arities, ...}) =
    2.87    let fun ls(T as Type(a, Ts)) =
    2.88 -                 (case assoc (coreg, a) of
    2.89 +                 (case assoc (arities, a) of
    2.90                            Some(ars) => cod_above(subclass, map ls Ts, ars)
    2.91                          | None => raise TYPE(undcl_type a, [T], []))
    2.92          | ls(TFree(a, S)) = S
    2.93 @@ -316,7 +315,7 @@
    2.94    in ls end;
    2.95  
    2.96  
    2.97 -fun check_has_sort(tsig as TySg{subclass, coreg, ...}, T, S) =
    2.98 +fun check_has_sort(tsig as TySg{subclass, arities, ...}, T, S) =
    2.99    if sortorder subclass ((least_sort tsig T), S) then ()
   2.100    else raise TYPE("Type not of sort " ^ (str_of_sort S), [T], [])
   2.101  
   2.102 @@ -380,9 +379,9 @@
   2.103  
   2.104  (** build type signatures **)
   2.105  
   2.106 -fun make_tsig (classes, subclass, default, args, abbrs, coreg) =
   2.107 +fun make_tsig (classes, subclass, default, tycons, abbrs, arities) =
   2.108    TySg {classes = classes, subclass = subclass, default = default,
   2.109 -    args = args, abbrs = abbrs, coreg = coreg};
   2.110 +    tycons = tycons, abbrs = abbrs, arities = arities};
   2.111  
   2.112  val tsig0 = make_tsig ([], [], [], [], [], []);
   2.113  
   2.114 @@ -406,7 +405,7 @@
   2.115  
   2.116  fun typ_errors tsig (typ, errors) =
   2.117    let
   2.118 -    val TySg {classes, args, abbrs, ...} = tsig;
   2.119 +    val TySg {classes, tycons, abbrs, ...} = tsig;
   2.120  
   2.121      fun class_err (errs, c) =
   2.122        if c mem classes then errs
   2.123 @@ -421,7 +420,7 @@
   2.124                if n = length Us then errs'
   2.125                else ("Wrong number of arguments: " ^ quote c) ins errs';
   2.126            in
   2.127 -            (case assoc (args, c) of
   2.128 +            (case assoc (tycons, c) of
   2.129                Some n => nargs n
   2.130              | None =>
   2.131                  (case assoc (abbrs, c) of
   2.132 @@ -475,67 +474,54 @@
   2.133  
   2.134  (* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *)
   2.135  
   2.136 -fun is_unique_decl coreg (t, (s, w)) = case assoc2 (coreg, (t, s)) of
   2.137 +fun is_unique_decl ars (t,(C,w)) = case assoc (ars, C) of
   2.138        Some(w1) => if w = w1 then () else
   2.139          error("There are two declarations\n" ^
   2.140 -              str_of_arity(t, w, [s]) ^ " and\n" ^
   2.141 -              str_of_arity(t, w1, [s]) ^ "\n" ^
   2.142 +              str_of_arity(t, w, [C]) ^ " and\n" ^
   2.143 +              str_of_arity(t, w1, [C]) ^ "\n" ^
   2.144                "with the same result class.")
   2.145      | None => ();
   2.146  
   2.147 -(* 'restr2' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2
   2.148 +(* 'coreg' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2
   2.149     such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *)
   2.150  
   2.151 -fun subs (classes, subclass) C =
   2.152 -  let fun sub (rl, l) = if leq subclass (l, C) then l::rl else rl
   2.153 -  in foldl sub ([], classes) end;
   2.154 -
   2.155 -fun coreg_err(t, (w1, C), (w2, D)) =
   2.156 -    error("Declarations " ^ str_of_arity(t, w1, [C]) ^ " and "
   2.157 -                          ^ str_of_arity(t, w2, [D]) ^ " are in conflict");
   2.158 +fun coreg_err(t, (C1,w1), (C2,w2)) =
   2.159 +    error("Declarations " ^ str_of_arity(t, w1, [C1]) ^ " and "
   2.160 +                          ^ str_of_arity(t, w2, [C2]) ^ " are in conflict");
   2.161  
   2.162 -fun restr2 classes (subclass, coreg) (t, (s, w)) =
   2.163 -  let fun restr ([], test) = ()
   2.164 -        | restr (s1::Ss, test) =
   2.165 -            (case assoc2 (coreg, (t, s1)) of
   2.166 -              Some dom =>
   2.167 -                if lew subclass (test (w, dom))
   2.168 -                then restr (Ss, test)
   2.169 -                else coreg_err (t, (w, s), (dom, s1))
   2.170 -            | None => restr (Ss, test))
   2.171 -      fun forward (t, (s, w)) =
   2.172 -        let val s_sups = case assoc (subclass, s) of
   2.173 -                   Some(s_sups) => s_sups | None => err_undcl_class(s);
   2.174 -        in restr (s_sups, I) end
   2.175 -      fun backward (t, (s, w)) =
   2.176 -        let val s_subs = subs (classes, subclass) s
   2.177 -        in restr (s_subs, fn (x, y) => (y, x)) end
   2.178 -  in (backward (t, (s, w)); forward (t, (s, w))) end;
   2.179 +fun coreg subclass (t, Cw1) =
   2.180 +  let fun check1(Cw1 as (C1,w1), Cw2 as (C2,w2)) =
   2.181 +        if leq subclass (C1,C2)
   2.182 +        then if lew subclass (w1,w2) then () else coreg_err(t, Cw1, Cw2)
   2.183 +        else ()
   2.184 +      fun check(Cw2) = (check1(Cw1,Cw2); check1(Cw2,Cw1))
   2.185 +  in seq check end;
   2.186  
   2.187 +fun add_arity subclass ars (tCw as (_,Cw)) =
   2.188 +      (is_unique_decl ars tCw; coreg subclass tCw ars; Cw ins ars);
   2.189  
   2.190  fun varying_decls t =
   2.191    error ("Type constructor " ^ quote t ^ " has varying number of arguments");
   2.192  
   2.193  
   2.194 -(* 'merge_coreg' builds the union of two 'coreg' lists;
   2.195 +(* 'merge_arities' builds the union of two 'arities' lists;
   2.196     it only checks the two restriction conditions and inserts afterwards
   2.197     all elements of the second list into the first one *)
   2.198  
   2.199 -fun merge_coreg classes subclass1 =
   2.200 -  let fun test_ar classes (t, ars1) (coreg1, (s, w)) =
   2.201 -        (is_unique_decl coreg1 (t, (s, w));
   2.202 -         restr2 classes (subclass1, coreg1) (t, (s, w));
   2.203 -         overwrite (coreg1, (t, (s, w) ins ars1)));
   2.204 +fun merge_arities subclass =
   2.205 +  let fun test_ar t (ars1, sw) = add_arity subclass ars1 (t,sw);
   2.206  
   2.207 -      fun merge_c (coreg1, (c as (t, ars2))) = case assoc (coreg1, t) of
   2.208 -          Some(ars1) => foldl (test_ar classes (t, ars1)) (coreg1, ars2)
   2.209 -        | None => c::coreg1
   2.210 +      fun merge_c (arities1, (c as (t, ars2))) = case assoc (arities1, t) of
   2.211 +          Some(ars1) =>
   2.212 +            let val ars = foldl (test_ar t) (ars1, ars2)
   2.213 +            in overwrite (arities1, (t,ars)) end
   2.214 +        | None => c::arities1
   2.215    in foldl merge_c end;
   2.216  
   2.217 -fun merge_args (args, (t, n)) =
   2.218 -  (case assoc (args, t) of
   2.219 -    Some m => if m = n then args else varying_decls t
   2.220 -  | None => (t, n) :: args);
   2.221 +fun add_tycons (tycons, tn as (t,n)) =
   2.222 +  (case assoc (tycons, t) of
   2.223 +    Some m => if m = n then tycons else varying_decls t
   2.224 +  | None => tn :: tycons);
   2.225  
   2.226  fun merge_abbrs (abbrs1, abbrs2) =
   2.227    let val abbrs = abbrs1 union abbrs2 in
   2.228 @@ -548,19 +534,17 @@
   2.229  (* 'merge_tsigs' takes the above declared functions to merge two type
   2.230    signatures *)
   2.231  
   2.232 -fun merge_tsigs(TySg{classes=classes1, default=default1, subclass=subclass1, args=args1,
   2.233 -           coreg=coreg1, abbrs=abbrs1},
   2.234 -          TySg{classes=classes2, default=default2, subclass=subclass2, args=args2,
   2.235 -           coreg=coreg2, abbrs=abbrs2}) =
   2.236 +fun merge_tsigs(TySg{classes=classes1, default=default1, subclass=subclass1,
   2.237 +                     tycons=tycons1, arities=arities1, abbrs=abbrs1},
   2.238 +                TySg{classes=classes2, default=default2, subclass=subclass2,
   2.239 +                     tycons=tycons2, arities=arities2, abbrs=abbrs2}) =
   2.240    let val classes' = classes1 union classes2;
   2.241        val subclass' = merge_subclass (subclass1, subclass2);
   2.242 -      val args' = foldl merge_args (args1, args2)
   2.243 -      val coreg' = merge_coreg classes' subclass' (coreg1, coreg2);
   2.244 +      val tycons' = foldl add_tycons (tycons1, tycons2)
   2.245 +      val arities' = merge_arities subclass' (arities1, arities2);
   2.246        val default' = min_sort subclass' (default1 @ default2);
   2.247        val abbrs' = merge_abbrs(abbrs1, abbrs2);
   2.248 -  in TySg{classes=classes' , default=default', subclass=subclass', args=args',
   2.249 -          coreg=coreg' , abbrs = abbrs' }
   2.250 -  end;
   2.251 +  in make_tsig(classes', subclass', default', tycons', abbrs', arities') end;
   2.252  
   2.253  
   2.254  
   2.255 @@ -610,10 +594,10 @@
   2.256  
   2.257  fun ext_tsig_classes tsig new_classes =
   2.258    let
   2.259 -    val TySg {classes, subclass, default, args, abbrs, coreg} = tsig;
   2.260 -    val (classes', subclass') = extend_classes (classes, subclass, new_classes);
   2.261 +    val TySg {classes, subclass, default, tycons, abbrs, arities} = tsig;
   2.262 +    val (classes',subclass') = extend_classes (classes,subclass,new_classes);
   2.263    in
   2.264 -    make_tsig (classes', subclass', default, args, abbrs, coreg)
   2.265 +    make_tsig (classes', subclass', default, tycons, abbrs, arities)
   2.266    end;
   2.267  
   2.268  
   2.269 @@ -621,36 +605,36 @@
   2.270  
   2.271  fun ext_tsig_subclass tsig pairs =
   2.272    let
   2.273 -    val TySg {classes, subclass, default, args, abbrs, coreg} = tsig;
   2.274 +    val TySg {classes, subclass, default, tycons, abbrs, arities} = tsig;
   2.275  
   2.276      (* FIXME clean! *)
   2.277      val subclass' =
   2.278        merge_subclass (subclass, map (fn (c1, c2) => (c1, [c2])) pairs);
   2.279    in
   2.280 -    make_tsig (classes, subclass', default, args, abbrs, coreg)
   2.281 +    make_tsig (classes, subclass', default, tycons, abbrs, arities)
   2.282    end;
   2.283  
   2.284  
   2.285  (* ext_tsig_defsort *)
   2.286  
   2.287 -fun ext_tsig_defsort (TySg {classes, subclass, args, abbrs, coreg, ...}) default =
   2.288 -  make_tsig (classes, subclass, default, args, abbrs, coreg);
   2.289 +fun ext_tsig_defsort(TySg{classes,subclass,tycons,abbrs,arities,...}) default =
   2.290 +  make_tsig (classes, subclass, default, tycons, abbrs, arities);
   2.291  
   2.292  
   2.293  
   2.294  (** add types **)
   2.295  
   2.296 -fun ext_tsig_types (TySg {classes, subclass, default, args, abbrs, coreg}) ts =
   2.297 +fun ext_tsig_types (TySg {classes, subclass, default, tycons, abbrs, arities}) ts =
   2.298    let
   2.299      fun check_type (c, n) =
   2.300        if n < 0 then err_neg_args c
   2.301 -      else if is_some (assoc (args, c)) then err_dup_tycon c
   2.302 +      else if is_some (assoc (tycons, c)) then err_dup_tycon c
   2.303        else if is_some (assoc (abbrs, c)) then err_ty_confl c
   2.304        else ();
   2.305    in
   2.306      seq check_type ts;
   2.307 -    make_tsig (classes, subclass, default, ts @ args, abbrs,
   2.308 -      map (rpair [] o #1) ts @ coreg)
   2.309 +    make_tsig (classes, subclass, default, ts @ tycons, abbrs,
   2.310 +      map (rpair [] o #1) ts @ arities)
   2.311    end;
   2.312  
   2.313  
   2.314 @@ -659,7 +643,7 @@
   2.315  
   2.316  fun abbr_errors tsig (a, (lhs_vs, rhs)) =
   2.317    let
   2.318 -    val TySg {args, abbrs, ...} = tsig;
   2.319 +    val TySg {tycons, abbrs, ...} = tsig;
   2.320      val rhs_vs = map (#1 o #1) (typ_tvars rhs);
   2.321  
   2.322      val dup_lhs_vars =
   2.323 @@ -673,7 +657,7 @@
   2.324        | vs => ["Extra variables on rhs: " ^ commas_quote vs]);
   2.325  
   2.326      val tycon_confl =
   2.327 -      if is_none (assoc (args, a)) then []
   2.328 +      if is_none (assoc (tycons, a)) then []
   2.329        else [ty_confl a];
   2.330  
   2.331      val dup_abbr =
   2.332 @@ -698,9 +682,10 @@
   2.333      | msgs => err msgs)
   2.334    end;
   2.335  
   2.336 -fun add_abbr (tsig as TySg {classes, subclass, default, args, coreg, abbrs}, abbr) =
   2.337 +fun add_abbr (tsig as TySg{classes,subclass,default,tycons,arities,abbrs},
   2.338 +              abbr) =
   2.339    make_tsig
   2.340 -    (classes, subclass, default, args, prep_abbr tsig abbr :: abbrs, coreg);
   2.341 +    (classes,subclass,default,tycons, prep_abbr tsig abbr :: abbrs, arities);
   2.342  
   2.343  fun ext_tsig_abbrs tsig raw_abbrs = foldl add_abbr (tsig, raw_abbrs);
   2.344  
   2.345 @@ -709,40 +694,37 @@
   2.346  (** add arities **)
   2.347  
   2.348  (* 'coregular' checks
   2.349 -   - the two restriction conditions 'is_unique_decl' and 'restr2'
   2.350 +   - the two restrictions 'is_unique_decl' and 'coreg'
   2.351     - if the classes in the new type declarations are known in the
   2.352       given type signature
   2.353     - if one type constructor has always the same number of arguments;
   2.354     if one type declaration has passed all checks it is inserted into
   2.355 -   the 'coreg' association list of the given type signatrure  *)
   2.356 +   the 'arities' association list of the given type signatrure  *)
   2.357  
   2.358 -fun coregular (classes, subclass, args) =
   2.359 +fun coregular (classes, subclass, tycons) =
   2.360    let fun ex C = if C mem classes then () else err_undcl_class(C);
   2.361  
   2.362 -      fun addar(w, C) (coreg, t) = case assoc(args, t) of
   2.363 +      fun addar(arities, (t, (w, C))) = case assoc(tycons, t) of
   2.364              Some(n) => if n <> length w then varying_decls(t) else
   2.365 -                     (is_unique_decl coreg (t, (C, w));
   2.366 -                      (seq o seq) ex w;
   2.367 -                      restr2 classes (subclass, coreg) (t, (C, w));
   2.368 -                      let val ars = the (assoc(coreg, t))
   2.369 -                      in overwrite(coreg, (t, (C, w) ins ars)) end)
   2.370 +                     ((seq o seq) ex w; ex C;
   2.371 +                      let val ars = the (assoc(arities, t))
   2.372 +                          val ars' = add_arity subclass ars (t,(C,w))
   2.373 +                      in overwrite(arities, (t,ars')) end)
   2.374            | None => err_undcl_type(t);
   2.375  
   2.376 -      fun addts(coreg, (ts, ar)) = foldl (addar ar) (coreg, ts)
   2.377 -
   2.378 -  in addts end;
   2.379 +  in addar end;
   2.380  
   2.381  
   2.382 -(* 'close' extends the 'coreg' association list after all new type
   2.383 +(* 'close' extends the 'arities' association list after all new type
   2.384     declarations have been inserted successfully:
   2.385     for every declaration t:(Ss)C , for all classses D with C <= D:
   2.386        if there is no declaration t:(Ss')C' with C < C' and C' <= D
   2.387 -      then insert the declaration t:(Ss)D into 'coreg'
   2.388 +      then insert the declaration t:(Ss)D into 'arities'
   2.389     this means, if there exists a declaration t:(Ss)C and there is
   2.390     no declaration t:(Ss')D with C <=D then the declaration holds
   2.391     for all range classes more general than C *)
   2.392  
   2.393 -fun close subclass coreg =
   2.394 +fun close subclass arities =
   2.395    let fun check sl (l, (s, dom)) = case assoc (subclass, s) of
   2.396            Some sups =>
   2.397              let fun close_sup (l, sup) =
   2.398 @@ -753,22 +735,21 @@
   2.399              in foldl close_sup (l, sups) end
   2.400          | None => l;
   2.401        fun ext (s, l) = (s, foldl (check (map #1 l)) (l, l));
   2.402 -  in map ext coreg end;
   2.403 +  in map ext arities end;
   2.404  
   2.405  
   2.406  (* ext_tsig_arities *)
   2.407  
   2.408  fun ext_tsig_arities tsig sarities =
   2.409    let
   2.410 -    val TySg {classes, subclass, default, args, coreg, abbrs} = tsig;
   2.411 -    val arities =
   2.412 -      flat (map (fn (t, ss, cs) => map (fn c => ([t], (ss, c))) cs) sarities);
   2.413 -    val coreg' =
   2.414 -      foldl (coregular (classes, subclass, args))
   2.415 -        (coreg, min_domain subclass arities)
   2.416 +    val TySg {classes, subclass, default, tycons, arities, abbrs} = tsig;
   2.417 +    val arities1 =
   2.418 +      flat (map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
   2.419 +    val arities2 = foldl (coregular (classes, subclass, tycons))
   2.420 +                         (arities, min_domain subclass arities1)
   2.421        |> close subclass;
   2.422    in
   2.423 -    make_tsig (classes, subclass, default, args, abbrs, coreg')
   2.424 +    make_tsig (classes, subclass, default, tycons, abbrs, arities2)
   2.425    end;
   2.426  
   2.427  
   2.428 @@ -837,7 +818,7 @@
   2.429  (* 'dom' returns for a type constructor t the list of those domains
   2.430     which deliver a given range class C *)
   2.431  
   2.432 -fun dom coreg t C = case assoc2 (coreg, (t, C)) of
   2.433 +fun dom arities t C = case assoc2 (arities, (t, C)) of
   2.434      Some(Ss) => Ss
   2.435    | None => raise TUNIFY;
   2.436  
   2.437 @@ -846,14 +827,14 @@
   2.438     (i.e. a set of range classes ); the union is carried out elementwise
   2.439     for the seperate sorts in the domains *)
   2.440  
   2.441 -fun Dom (subclass, coreg) (t, S) =
   2.442 -  let val domlist = map (dom coreg t) S;
   2.443 +fun Dom (subclass, arities) (t, S) =
   2.444 +  let val domlist = map (dom arities t) S;
   2.445    in if null domlist then []
   2.446       else foldl (elementwise_union subclass) (hd domlist, tl domlist)
   2.447    end;
   2.448  
   2.449  
   2.450 -fun W ((T, S), tsig as TySg{subclass, coreg, ...}, tye) =
   2.451 +fun W ((T, S), tsig as TySg{subclass, arities, ...}, tye) =
   2.452    let fun Wd ((T, S), tye) = W ((devar (T, tye), S), tsig, tye)
   2.453        fun Wk(T as TVar(v, S')) =
   2.454                if sortorder subclass (S', S) then tye
   2.455 @@ -862,14 +843,14 @@
   2.456                                   else raise TUNIFY
   2.457          | Wk(T as Type(f, Ts)) =
   2.458             if null S then tye
   2.459 -           else foldr Wd (Ts~~(Dom (subclass, coreg) (f, S)) , tye)
   2.460 +           else foldr Wd (Ts~~(Dom (subclass, arities) (f, S)) , tye)
   2.461    in Wk(T) end;
   2.462  
   2.463  
   2.464  (* Order-sorted Unification of Types (U)  *)
   2.465  
   2.466  (* Precondition: both types are well-formed w.r.t. type constructor arities *)
   2.467 -fun unify (tsig as TySg{subclass, coreg, ...}) =
   2.468 +fun unify (tsig as TySg{subclass, arities, ...}) =
   2.469    let fun unif ((T, U), tye) =
   2.470          case (devar(T, tye), devar(U, tye)) of
   2.471            (T as TVar(v, S1), U as TVar(w, S2)) =>
   2.472 @@ -879,9 +860,9 @@
   2.473               else let val nu = gen_tyvar (union_sort subclass (S1, S2))
   2.474                    in (v, nu)::(w, nu)::tye end
   2.475          | (T as TVar(v, S), U) =>
   2.476 -             if occ v tye U then raise TUNIFY else W ((U, S), tsig, (v, U)::tye)
   2.477 +             if occ v tye U then raise TUNIFY else W ((U,S), tsig, (v, U)::tye)
   2.478          | (U, T as TVar (v, S)) =>
   2.479 -             if occ v tye U then raise TUNIFY else W ((U, S), tsig, (v, U)::tye)
   2.480 +             if occ v tye U then raise TUNIFY else W ((U,S), tsig, (v, U)::tye)
   2.481          | (Type(a, Ts), Type(b, Us)) =>
   2.482               if a<>b then raise TUNIFY else foldr unif (Ts~~Us, tye)
   2.483          | (T, U) => if T=U then tye else raise TUNIFY