src/Pure/type.ML
changeset 14790 0d984ee030a1
parent 13666 a2730043029b
child 14830 faa4865ba1ce
     1.1 --- a/src/Pure/type.ML	Fri May 21 21:25:57 2004 +0200
     1.2 +++ b/src/Pure/type.ML	Fri May 21 21:26:19 2004 +0200
     1.3 @@ -1,13 +1,44 @@
     1.4  (*  Title:      Pure/type.ML
     1.5      ID:         $Id$
     1.6 -    Author:     Tobias Nipkow & Lawrence C Paulson
     1.7 +    Author:     Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel
     1.8  
     1.9 -Type signatures, unification of types, interface to type inference.
    1.10 +Type signatures and certified types, special treatment of type vars,
    1.11 +matching and unification of types, extend and merge type signatures.
    1.12  *)
    1.13  
    1.14  signature TYPE =
    1.15  sig
    1.16 -  (*TFrees and TVars*)
    1.17 +  (*type signatures and certified types*)
    1.18 +  datatype decl =
    1.19 +    LogicalType of int |
    1.20 +    Abbreviation of string list * typ |
    1.21 +    Nonterminal
    1.22 +  type tsig
    1.23 +  val rep_tsig: tsig ->
    1.24 +   {classes: Sorts.classes,
    1.25 +    default: sort,
    1.26 +    types: (decl * stamp) Symtab.table,
    1.27 +    arities: Sorts.arities,
    1.28 +    log_types: string list,
    1.29 +    witness: (typ * sort) option}
    1.30 +  val empty_tsig: tsig
    1.31 +  val classes: tsig -> class list
    1.32 +  val defaultS: tsig -> sort
    1.33 +  val logical_types: tsig -> string list
    1.34 +  val universal_witness: tsig -> (typ * sort) option
    1.35 +  val eq_sort: tsig -> sort * sort -> bool
    1.36 +  val subsort: tsig -> sort * sort -> bool
    1.37 +  val of_sort: tsig -> typ * sort -> bool
    1.38 +  val cert_class: tsig -> class -> class
    1.39 +  val cert_sort: tsig -> sort -> sort
    1.40 +  val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list
    1.41 +  val norm_typ: tsig -> typ -> typ
    1.42 +  val cert_typ: tsig -> typ -> typ
    1.43 +  val cert_typ_syntax: tsig -> typ -> typ
    1.44 +  val cert_typ_raw: tsig -> typ -> typ
    1.45 +
    1.46 +  (*special treatment of type vars*)
    1.47 +  val strip_sorts: typ -> typ
    1.48    val no_tvars: typ -> typ
    1.49    val varifyT: typ -> typ
    1.50    val unvarifyT: typ -> typ
    1.51 @@ -15,79 +46,187 @@
    1.52    val freeze_thaw_type : typ -> typ * (typ -> typ)
    1.53    val freeze_thaw : term -> term * (term -> term)
    1.54  
    1.55 -  (*type signatures*)
    1.56 -  type type_sig
    1.57 -  val rep_tsig: type_sig ->
    1.58 -    {classes: class list,
    1.59 -     classrel: Sorts.classrel,
    1.60 -     default: sort,
    1.61 -     tycons: int Symtab.table,
    1.62 -     log_types: string list,
    1.63 -     univ_witness: (typ * sort) option,
    1.64 -     abbrs: (string list * typ) Symtab.table,
    1.65 -     arities: Sorts.arities}
    1.66 -  val classes: type_sig -> class list
    1.67 -  val defaultS: type_sig -> sort
    1.68 -  val logical_types: type_sig -> string list
    1.69 -  val univ_witness: type_sig -> (typ * sort) option
    1.70 -  val subsort: type_sig -> sort * sort -> bool
    1.71 -  val eq_sort: type_sig -> sort * sort -> bool
    1.72 -  val norm_sort: type_sig -> sort -> sort
    1.73 -  val cert_class: type_sig -> class -> class
    1.74 -  val cert_sort: type_sig -> sort -> sort
    1.75 -  val witness_sorts: type_sig -> sort list -> sort list -> (typ * sort) list
    1.76 -  val rem_sorts: typ -> typ
    1.77 -  val tsig0: type_sig
    1.78 -  val ext_tsig_classes: type_sig -> (class * class list) list -> type_sig
    1.79 -  val ext_tsig_classrel: type_sig -> (class * class) list -> type_sig
    1.80 -  val ext_tsig_defsort: type_sig -> sort -> type_sig
    1.81 -  val ext_tsig_types: type_sig -> (string * int) list -> type_sig
    1.82 -  val ext_tsig_abbrs: type_sig -> (string * string list * typ) list -> type_sig
    1.83 -  val ext_tsig_arities: type_sig -> (string * sort list * sort)list -> type_sig
    1.84 -  val merge_tsigs: type_sig * type_sig -> type_sig
    1.85 -  val typ_errors: type_sig -> typ * string list -> string list
    1.86 -  val cert_typ: type_sig -> typ -> typ
    1.87 -  val cert_typ_no_norm: type_sig -> typ -> typ
    1.88 -  val norm_typ: type_sig -> typ -> typ
    1.89 -  val norm_term: type_sig -> term -> term
    1.90 -  val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term
    1.91 -  val inst_typ_tvars: type_sig * (indexname * typ) list -> typ -> typ
    1.92 -
    1.93 -  (*type matching*)
    1.94 +  (*matching and unification*)
    1.95 +  val inst_term_tvars: tsig -> (indexname * typ) list -> term -> term
    1.96 +  val inst_typ_tvars: tsig -> (indexname * typ) list -> typ -> typ
    1.97    exception TYPE_MATCH
    1.98 -  val typ_match: type_sig -> typ Vartab.table * (typ * typ)
    1.99 -    -> typ Vartab.table
   1.100 -  val typ_instance: type_sig * typ * typ -> bool
   1.101 -  val of_sort: type_sig -> typ * sort -> bool
   1.102 -
   1.103 -  (*type unification*)
   1.104 +  val typ_match: tsig -> typ Vartab.table * (typ * typ) -> typ Vartab.table
   1.105 +  val typ_instance: tsig -> typ * typ -> bool
   1.106    exception TUNIFY
   1.107 -  val unify: type_sig -> typ Vartab.table * int -> typ * typ -> typ Vartab.table * int
   1.108 +  val unify: tsig -> typ Vartab.table * int -> typ * typ -> typ Vartab.table * int
   1.109    val raw_unify: typ * typ -> bool
   1.110  
   1.111 -  (*type inference*)
   1.112 -  val get_sort: type_sig -> (indexname -> sort option) -> (sort -> sort)
   1.113 -    -> (indexname * sort) list -> indexname -> sort
   1.114 -  val constrain: term -> typ -> term
   1.115 -  val param: int -> string * sort -> typ
   1.116 -  val paramify_dummies: int * typ -> int * typ
   1.117 -  val infer_types: (term -> Pretty.T) -> (typ -> Pretty.T)
   1.118 -    -> type_sig -> (string -> typ option) -> (indexname -> typ option)
   1.119 -    -> (indexname -> sort option) -> (string -> string) -> (typ -> typ)
   1.120 -    -> (sort -> sort) -> string list -> bool -> typ list -> term list
   1.121 -    -> term list * (indexname * typ) list
   1.122 +  (*extend and merge type signatures*)
   1.123 +  val add_classes: (class * class list) list -> tsig -> tsig
   1.124 +  val add_classrel: (class * class) list -> tsig -> tsig
   1.125 +  val set_defsort: sort -> tsig -> tsig
   1.126 +  val add_types: (string * int) list -> tsig -> tsig
   1.127 +  val add_abbrs: (string * string list * typ) list -> tsig -> tsig
   1.128 +  val add_nonterminals: string list -> tsig -> tsig
   1.129 +  val add_arities: (string * sort list * sort) list -> tsig -> tsig
   1.130 +  val merge_tsigs: tsig * tsig -> tsig
   1.131  end;
   1.132  
   1.133  structure Type: TYPE =
   1.134  struct
   1.135  
   1.136 +(** type signatures and certified types **)
   1.137  
   1.138 -(*** TFrees and TVars ***)
   1.139 +(* type declarations *)
   1.140 +
   1.141 +datatype decl =
   1.142 +  LogicalType of int |
   1.143 +  Abbreviation of string list * typ |
   1.144 +  Nonterminal;
   1.145 +
   1.146 +fun str_of_decl (LogicalType _) = "logical type constructor"
   1.147 +  | str_of_decl (Abbreviation _) = "type abbreviation"
   1.148 +  | str_of_decl Nonterminal = "syntactic type";
   1.149 +
   1.150 +
   1.151 +(* type tsig *)
   1.152 +
   1.153 +datatype tsig =
   1.154 +  TSig of {
   1.155 +    classes: Sorts.classes,              (*declared classes with proper subclass relation*)
   1.156 +    default: sort,                       (*default sort on input*)
   1.157 +    types: (decl * stamp) Symtab.table,  (*declared types*)
   1.158 +    arities: Sorts.arities,              (*image specification of types wrt. sorts*)
   1.159 +    log_types: string list,              (*logical types sorted by number of arguments*)
   1.160 +    witness: (typ * sort) option};       (*witness for non-emptiness of strictest sort*)
   1.161 +
   1.162 +fun rep_tsig (TSig comps) = comps;
   1.163 +
   1.164 +fun make_tsig (classes, default, types, arities, log_types, witness) =
   1.165 +  TSig {classes = classes, default = default, types = types, arities = arities,
   1.166 +    log_types = log_types, witness = witness};
   1.167 +
   1.168 +fun map_tsig f (TSig {classes, default, types, arities, log_types, witness}) =
   1.169 +  make_tsig (f (classes, default, types, arities, log_types, witness));
   1.170 +
   1.171 +fun build_tsig (classes, default, types, arities) =
   1.172 +  let
   1.173 +    fun add_log_type (ts, (c, (LogicalType n, _))) = (c, n) :: ts
   1.174 +      | add_log_type (ts, _) = ts;
   1.175 +    val log_types =
   1.176 +      Symtab.foldl add_log_type ([], types)
   1.177 +      |> Library.sort (Library.int_ord o pairself #2) |> map #1;
   1.178 +    val witness =
   1.179 +      (case Sorts.witness_sorts (classes, arities) log_types [] [Graph.keys classes] of
   1.180 +        [w] => Some w | _ => None);
   1.181 +  in make_tsig (classes, default, types, arities, log_types, witness) end;
   1.182 +
   1.183 +fun change_tsig f (TSig {classes, default, types, arities, log_types = _, witness = _}) =
   1.184 +  build_tsig (f (classes, default, types, arities));
   1.185 +
   1.186 +val empty_tsig = build_tsig (Graph.empty, [], Symtab.empty, Symtab.empty);
   1.187 +
   1.188 +
   1.189 +(* classes and sorts *)
   1.190 +
   1.191 +fun classes (TSig {classes = C, ...}) = Graph.keys C;
   1.192 +fun defaultS (TSig {default, ...}) = default;
   1.193 +fun logical_types (TSig {log_types, ...}) = log_types;
   1.194 +fun universal_witness (TSig {witness, ...}) = witness;
   1.195 +
   1.196 +fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq classes;
   1.197 +fun subsort (TSig {classes, ...}) = Sorts.sort_le classes;
   1.198 +fun of_sort (TSig {classes, arities, ...}) = Sorts.of_sort (classes, arities);
   1.199 +fun norm_sort (TSig {classes, ...}) = Sorts.norm_sort classes;
   1.200 +
   1.201 +fun cert_class (TSig {classes, ...}) c =
   1.202 +  if can (Graph.get_node classes) c then c
   1.203 +  else raise TYPE ("Undeclared class: " ^ quote c, [], []);
   1.204 +
   1.205 +fun cert_sort tsig = norm_sort tsig o map (cert_class tsig);
   1.206 +
   1.207 +fun witness_sorts (tsig as TSig {classes, arities, log_types, ...}) =
   1.208 +  Sorts.witness_sorts (classes, arities) log_types;
   1.209 +
   1.210 +
   1.211 +(* certified types *)
   1.212 +
   1.213 +fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t;
   1.214 +
   1.215 +fun inst_typ tye =
   1.216 +  let
   1.217 +    fun inst (var as (v, _)) =
   1.218 +      (case assoc_string_int (tye, v) of
   1.219 +        Some U => inst_typ tye U
   1.220 +      | None => TVar var);
   1.221 +  in map_type_tvar inst end;
   1.222 +
   1.223 +(*expand type abbreviations and normalize sorts*)
   1.224 +fun norm_typ (tsig as TSig {types, ...}) ty =
   1.225 +  let
   1.226 +    val idx = Term.maxidx_of_typ ty + 1;
   1.227 +
   1.228 +    fun norm (Type (a, Ts)) =
   1.229 +          (case Symtab.lookup (types, a) of
   1.230 +            Some (Abbreviation (vs, U), _) =>
   1.231 +              norm (inst_typ (map (rpair idx) vs ~~ Ts) (incr_tvar idx U))
   1.232 +          | _ => Type (a, map norm Ts))
   1.233 +      | norm (TFree (x, S)) = TFree (x, norm_sort tsig S)
   1.234 +      | norm (TVar (xi, S)) = TVar (xi, norm_sort tsig S);
   1.235 +
   1.236 +    val ty' = norm ty;
   1.237 +  in if ty = ty' then ty else ty' end;  (*avoid copying of already normal type*)
   1.238 +
   1.239 +(*check validity of (not necessarily normal) type*)   (*exception TYPE*)
   1.240 +fun certify_typ normalize syntax tsig ty =
   1.241 +  let
   1.242 +    val TSig {types, ...} = tsig;
   1.243 +    fun err msg = raise TYPE (msg, [ty], []);
   1.244 +
   1.245 +    fun check_sort S = (map (cert_class tsig) S; ());
   1.246 +
   1.247 +    fun check_typ (Type (c, Ts)) =
   1.248 +          let fun nargs n = if length Ts <> n then err (bad_nargs c) else () in
   1.249 +            (case Symtab.lookup (types, c) of
   1.250 +              Some (LogicalType n, _) => nargs n
   1.251 +            | Some (Abbreviation (vs, _), _) => nargs (length vs)
   1.252 +            | Some (Nonterminal, _) => nargs 0
   1.253 +            | None => err ("Undeclared type constructor: " ^ quote c));
   1.254 +            seq check_typ Ts
   1.255 +          end
   1.256 +    | check_typ (TFree (_, S)) = check_sort S
   1.257 +    | check_typ (TVar ((x, i), S)) =
   1.258 +        if i < 0 then err ("Malformed type variable: " ^ quote (Term.string_of_vname (x, i)))
   1.259 +        else check_sort S;
   1.260 +
   1.261 +    fun no_syntax (Type (c, Ts)) =
   1.262 +          (case Symtab.lookup (types, c) of
   1.263 +            Some (Nonterminal, _) =>
   1.264 +              err ("Illegal occurrence of syntactic type: " ^ quote c)
   1.265 +          | _ => seq no_syntax Ts)
   1.266 +      | no_syntax _ = ();
   1.267 +
   1.268 +    val _ = check_typ ty;
   1.269 +    val ty' = if normalize orelse not syntax then norm_typ tsig ty else ty;
   1.270 +    val _ = if not syntax then no_syntax ty' else ();
   1.271 +  in ty' end;
   1.272 +
   1.273 +val cert_typ         = certify_typ true false;
   1.274 +val cert_typ_syntax  = certify_typ true true;
   1.275 +val cert_typ_raw     = certify_typ false true;
   1.276 +
   1.277 +
   1.278 +
   1.279 +(** special treatment of type vars **)
   1.280 +
   1.281 +(* strip_sorts *)
   1.282 +
   1.283 +fun strip_sorts (Type (a, Ts)) = Type (a, map strip_sorts Ts)
   1.284 +  | strip_sorts (TFree (x, _)) = TFree (x, [])
   1.285 +  | strip_sorts (TVar (xi, _)) = TVar (xi, []);
   1.286 +
   1.287 +
   1.288 +(* no_tvars *)
   1.289  
   1.290  fun no_tvars T =
   1.291    (case typ_tvars T of [] => T
   1.292    | vs => raise TYPE ("Illegal schematic type variable(s): " ^
   1.293 -      commas (map (Syntax.string_of_vname o #1) vs), [T], []));
   1.294 +      commas (map (Term.string_of_vname o #1) vs), [T], []));
   1.295  
   1.296  
   1.297  (* varify, unvarify *)
   1.298 @@ -152,557 +291,27 @@
   1.299  
   1.300  
   1.301  
   1.302 -(*** type signatures ***)
   1.303 -
   1.304 -(* type type_sig *)
   1.305 -
   1.306 -(*
   1.307 -  classes: list of all declared classes;
   1.308 -  classrel: (see Pure/sorts.ML)
   1.309 -  default: default sort attached to all unconstrained type vars;
   1.310 -  tycons: table of all declared types with the number of their arguments;
   1.311 -  log_types: list of logical type constructors sorted by number of arguments;
   1.312 -  univ_witness: type witnessing non-emptiness of least sort
   1.313 -  abbrs: table of type abbreviations;
   1.314 -  arities: (see Pure/sorts.ML)
   1.315 -*)
   1.316 -
   1.317 -datatype type_sig =
   1.318 -  TySg of {
   1.319 -    classes: class list,
   1.320 -    classrel: Sorts.classrel,
   1.321 -    default: sort,
   1.322 -    tycons: int Symtab.table,
   1.323 -    log_types: string list,
   1.324 -    univ_witness: (typ * sort) option,
   1.325 -    abbrs: (string list * typ) Symtab.table,
   1.326 -    arities: Sorts.arities};
   1.327 -
   1.328 -fun rep_tsig (TySg comps) = comps;
   1.329 -
   1.330 -fun classes (TySg {classes = cs, ...}) = cs;
   1.331 -fun defaultS (TySg {default, ...}) = default;
   1.332 -fun logical_types (TySg {log_types, ...}) = log_types;
   1.333 -fun univ_witness (TySg {univ_witness, ...}) = univ_witness;
   1.334 -
   1.335 -
   1.336 -(* error messages *)
   1.337 -
   1.338 -fun undeclared_class c = "Undeclared class: " ^ quote c;
   1.339 -fun undeclared_classes cs = "Undeclared class(es): " ^ commas_quote cs;
   1.340 -
   1.341 -fun err_undeclared_class s = error (undeclared_class s);
   1.342 -
   1.343 -fun err_dup_classes cs =
   1.344 -  error ("Duplicate declaration of class(es): " ^ commas_quote cs);
   1.345 -
   1.346 -fun undeclared_type c = "Undeclared type constructor: " ^ quote c;
   1.347 -
   1.348 -fun err_neg_args c =
   1.349 -  error ("Negative number of arguments of type constructor: " ^ quote c);
   1.350 -
   1.351 -fun err_dup_tycon c =
   1.352 -  error ("Duplicate declaration of type constructor: " ^ quote c);
   1.353 +(** matching and unification of types **)
   1.354  
   1.355 -fun dup_tyabbrs ts =
   1.356 -  "Duplicate declaration of type abbreviation(s): " ^ commas_quote ts;
   1.357 -
   1.358 -fun ty_confl c = "Conflicting type constructor and abbreviation: " ^ quote c;
   1.359 -
   1.360 -
   1.361 -(* sorts *)
   1.362 -
   1.363 -fun subsort (TySg {classrel, ...}) = Sorts.sort_le classrel;
   1.364 -fun eq_sort (TySg {classrel, ...}) = Sorts.sort_eq classrel;
   1.365 -fun norm_sort (TySg {classrel, ...}) = Sorts.norm_sort classrel;
   1.366 -
   1.367 -fun cert_class (TySg {classes, ...}) c =
   1.368 -  if c mem_string classes then c else raise TYPE (undeclared_class c, [], []);
   1.369 -
   1.370 -fun cert_sort tsig S = norm_sort tsig (map (cert_class tsig) S);
   1.371 -
   1.372 -fun witness_sorts (tsig as TySg {classrel, arities, log_types, ...}) =
   1.373 -  Sorts.witness_sorts (classrel, arities, log_types);
   1.374 -
   1.375 -fun rem_sorts (Type (a, tys)) = Type (a, map rem_sorts tys)
   1.376 -  | rem_sorts (TFree (x, _)) = TFree (x, [])
   1.377 -  | rem_sorts (TVar (xi, _)) = TVar (xi, []);
   1.378 -
   1.379 +(* instantiation *)
   1.380  
   1.381 -(* FIXME err_undeclared_class! *)
   1.382 -(* 'leq' checks the partial order on classes according to the
   1.383 -   statements in classrel 'a'
   1.384 -*)
   1.385 -
   1.386 -fun less a (C, D) = case Symtab.lookup (a, C) of
   1.387 -     Some ss => D mem_string ss
   1.388 -   | None => err_undeclared_class C;
   1.389 -
   1.390 -fun leq a (C, D)  =  C = D orelse less a (C, D);
   1.391 -
   1.392 -
   1.393 -
   1.394 -(* FIXME *)
   1.395 -(*Instantiation of type variables in types*)
   1.396 -(*Pre: instantiations obey restrictions! *)
   1.397 -fun inst_typ tye =
   1.398 -  let fun inst(var as (v, _)) = case assoc(tye, v) of
   1.399 -                                  Some U => inst_typ tye U
   1.400 -                                | None => TVar(var)
   1.401 -  in map_type_tvar inst end;
   1.402 -
   1.403 -
   1.404 -
   1.405 -fun of_sort (TySg {classrel, arities, ...}) = Sorts.of_sort (classrel, arities);
   1.406 -
   1.407 -fun check_has_sort (tsig, T, S) =
   1.408 -  if of_sort tsig (T, S) then ()
   1.409 +fun type_of_sort tsig (T, S) =
   1.410 +  if of_sort tsig (T, S) then T
   1.411    else raise TYPE ("Type not of sort " ^ Sorts.str_of_sort S, [T], []);
   1.412  
   1.413 -
   1.414 -(*Instantiation of type variables in types *)
   1.415 -fun inst_typ_tvars(tsig, tye) =
   1.416 -  let fun inst(var as (v, S)) = case assoc(tye, v) of
   1.417 -              Some U => (check_has_sort(tsig, U, S); U)
   1.418 -            | None => TVar(var)
   1.419 +fun inst_typ_tvars tsig tye =
   1.420 +  let
   1.421 +    fun inst (var as (v, S)) =
   1.422 +      (case assoc_string_int (tye, v) of
   1.423 +        Some U => type_of_sort tsig (U, S)
   1.424 +      | None => TVar var);
   1.425    in map_type_tvar inst end;
   1.426  
   1.427 -(*Instantiation of type variables in terms *)
   1.428 -fun inst_term_tvars (_,[]) t = t
   1.429 -  | inst_term_tvars arg    t = map_term_types (inst_typ_tvars arg) t;
   1.430 -
   1.431 -
   1.432 -(* norm_typ, norm_term *)
   1.433 -
   1.434 -(*expand abbreviations and normalize sorts*)
   1.435 -fun norm_typ (tsig as TySg {abbrs, ...}) ty =
   1.436 -  let
   1.437 -    val idx = maxidx_of_typ ty + 1;
   1.438 -
   1.439 -    fun norm (Type (a, Ts)) =
   1.440 -          (case Symtab.lookup (abbrs, a) of
   1.441 -            Some (vs, U) => norm (inst_typ (map (rpair idx) vs ~~ Ts) (incr_tvar idx U))
   1.442 -          | None => Type (a, map norm Ts))
   1.443 -      | norm (TFree (x, S)) = TFree (x, norm_sort tsig S)
   1.444 -      | norm (TVar (xi, S)) = TVar (xi, norm_sort tsig S);
   1.445 -
   1.446 -    val ty' = norm ty;
   1.447 -  in if ty = ty' then ty else ty' end;  (*dumb tuning to avoid copying*)
   1.448 -
   1.449 -fun norm_term tsig t =
   1.450 -  let val t' = map_term_types (norm_typ tsig) t
   1.451 -  in if t = t' then t else t' end;  (*dumb tuning to avoid copying*)
   1.452 -
   1.453 -
   1.454 -
   1.455 -(** build type signatures **)
   1.456 -
   1.457 -fun make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities) =
   1.458 -  TySg {classes = classes, classrel = classrel, default = default, tycons = tycons,
   1.459 -    log_types = log_types, univ_witness = univ_witness, abbrs = abbrs, arities = arities};
   1.460 -
   1.461 -fun rebuild_tsig (TySg {classes, classrel, default, tycons, log_types = _, univ_witness = _, abbrs, arities}) =
   1.462 -  let
   1.463 -    fun log_class c = Sorts.class_le classrel (c, logicC);
   1.464 -    fun log_type (t, _) = exists (log_class o #1) (Symtab.lookup_multi (arities, t));
   1.465 -    val ts = filter log_type (Symtab.dest tycons);
   1.466 -
   1.467 -    val log_types = map #1 (Library.sort (Library.int_ord o pairself #2) ts);
   1.468 -    val univ_witness =
   1.469 -      (case Sorts.witness_sorts (classrel, arities, log_types) [] [classes] of
   1.470 -        [w] => Some w | _ => None);
   1.471 -  in make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities) end;
   1.472 -
   1.473 -val tsig0 =
   1.474 -  make_tsig ([], Symtab.empty, [], Symtab.empty, [], None, Symtab.empty, Symtab.empty)
   1.475 -  |> rebuild_tsig;
   1.476 -
   1.477 -
   1.478 -(* typ_errors *)
   1.479 -
   1.480 -(*check validity of (not necessarily normal) type; accumulate error messages*)
   1.481 -
   1.482 -fun typ_errors tsig (typ, errors) =
   1.483 -  let
   1.484 -    val {classes, tycons, abbrs, ...} = rep_tsig tsig;
   1.485 -
   1.486 -    fun class_err (errs, c) =
   1.487 -      if c mem_string classes then errs
   1.488 -      else undeclared_class c ins_string errs;
   1.489 -
   1.490 -    val sort_err = foldl class_err;
   1.491 -
   1.492 -    fun typ_errs (errs, Type (c, Us)) =
   1.493 -          let
   1.494 -            val errs' = foldl typ_errs (errs, Us);
   1.495 -            fun nargs n =
   1.496 -              if n = length Us then errs'
   1.497 -              else ("Wrong number of arguments: " ^ quote c) ins_string errs';
   1.498 -          in
   1.499 -            (case Symtab.lookup (tycons, c) of
   1.500 -              Some n => nargs n
   1.501 -            | None =>
   1.502 -                (case Symtab.lookup (abbrs, c) of
   1.503 -                  Some (vs, _) => nargs (length vs)
   1.504 -                | None => undeclared_type c ins_string errs))
   1.505 -          end
   1.506 -    | typ_errs (errs, TFree (_, S)) = sort_err (errs, S)
   1.507 -    | typ_errs (errs, TVar ((x, i), S)) =
   1.508 -        if i < 0 then
   1.509 -          ("Negative index for TVar " ^ quote x) ins_string sort_err (errs, S)
   1.510 -        else sort_err (errs, S);
   1.511 -  in typ_errs (errors, typ) end;
   1.512 -
   1.513 -
   1.514 -(* cert_typ *)           (*exception TYPE*)
   1.515 -
   1.516 -fun cert_typ_no_norm tsig T =
   1.517 -  (case typ_errors tsig (T, []) of
   1.518 -    [] => T
   1.519 -  | errs => raise TYPE (cat_lines errs, [T], []));
   1.520 -
   1.521 -fun cert_typ tsig T = norm_typ tsig (cert_typ_no_norm tsig T);
   1.522 -
   1.523 -
   1.524 -
   1.525 -(** merge type signatures **)
   1.526 -
   1.527 -(* merge classrel *)
   1.528 -
   1.529 -fun assoc_union (as1, []) = as1
   1.530 -  | assoc_union (as1, (key, l2) :: as2) =
   1.531 -      (case assoc_string (as1, key) of
   1.532 -        Some l1 => assoc_union (overwrite (as1, (key, l1 union_string l2)), as2)
   1.533 -      | None => assoc_union ((key, l2) :: as1, as2));
   1.534 -
   1.535 -fun merge_classrel (classrel1, classrel2) =
   1.536 -  let
   1.537 -    val classrel = transitive_closure (assoc_union (Symtab.dest classrel1, Symtab.dest classrel2))
   1.538 -  in
   1.539 -    if exists (op mem_string) classrel then
   1.540 -      error ("Cyclic class structure!")   (* FIXME improve msg, raise TERM *)
   1.541 -    else Symtab.make classrel
   1.542 -  end;
   1.543 -
   1.544 -
   1.545 -(* coregularity *)
   1.546 -
   1.547 -local
   1.548 -
   1.549 -(* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *)
   1.550 -
   1.551 -fun is_unique_decl ars (t,(C,w)) = case assoc (ars, C) of
   1.552 -      Some(w1) => if w = w1 then () else
   1.553 -        error("There are two declarations\n" ^
   1.554 -              Sorts.str_of_arity(t, w, [C]) ^ " and\n" ^
   1.555 -              Sorts.str_of_arity(t, w1, [C]) ^ "\n" ^
   1.556 -              "with the same result class.")
   1.557 -    | None => ();
   1.558 -
   1.559 -(* 'coreg' checks if there are two declarations t:(Ss1)C1 and t:(Ss2)C2
   1.560 -   such that C1 >= C2 then Ss1 >= Ss2 (elementwise) *)
   1.561 -
   1.562 -fun coreg_err(t, (C1,w1), (C2,w2)) =
   1.563 -    error("Declarations " ^ Sorts.str_of_arity(t, w1, [C1]) ^ " and "
   1.564 -                          ^ Sorts.str_of_arity(t, w2, [C2]) ^ " are in conflict");
   1.565 -
   1.566 -fun coreg classrel (t, Cw1) =
   1.567 -  let
   1.568 -    fun check1(Cw1 as (C1,w1), Cw2 as (C2,w2)) =
   1.569 -      if leq classrel (C1,C2) then
   1.570 -        if Sorts.sorts_le classrel (w1,w2) then ()
   1.571 -        else coreg_err(t, Cw1, Cw2)
   1.572 -      else ()
   1.573 -    fun check(Cw2) = (check1(Cw1,Cw2); check1(Cw2,Cw1))
   1.574 -  in seq check end;
   1.575 -
   1.576 -in
   1.577 -
   1.578 -fun add_arity classrel ars (tCw as (_,Cw)) =
   1.579 -      (is_unique_decl ars tCw; coreg classrel tCw ars; Cw ins ars);
   1.580 -
   1.581 -end;
   1.582 +fun inst_term_tvars _ [] t = t
   1.583 +  | inst_term_tvars tsig tye t = map_term_types (inst_typ_tvars tsig tye) t;
   1.584  
   1.585  
   1.586 -(* 'merge_arities' builds the union of two 'arities' lists;
   1.587 -   it only checks the two restriction conditions and inserts afterwards
   1.588 -   all elements of the second list into the first one *)
   1.589 -
   1.590 -local
   1.591 -
   1.592 -fun merge_arities_aux classrel =
   1.593 -  let fun test_ar t (ars1, sw) = add_arity classrel ars1 (t,sw);
   1.594 -
   1.595 -      fun merge_c (arities1, (c as (t, ars2))) = case assoc (arities1, t) of
   1.596 -          Some(ars1) =>
   1.597 -            let val ars = foldl (test_ar t) (ars1, ars2)
   1.598 -            in overwrite (arities1, (t,ars)) end
   1.599 -        | None => c::arities1
   1.600 -  in foldl merge_c end;
   1.601 -
   1.602 -in
   1.603 -
   1.604 -fun merge_arities classrel (a1, a2) =
   1.605 -  Symtab.make (merge_arities_aux classrel (Symtab.dest a1, Symtab.dest a2));
   1.606 -
   1.607 -end;
   1.608 -
   1.609 -
   1.610 -(* tycons *)
   1.611 -
   1.612 -fun varying_decls t =
   1.613 -  error ("Type constructor " ^ quote t ^ " has varying number of arguments");
   1.614 -
   1.615 -fun add_tycons (tycons, tn as (t,n)) =
   1.616 -  (case Symtab.lookup (tycons, t) of
   1.617 -    Some m => if m = n then tycons else varying_decls t
   1.618 -  | None => Symtab.update (tn, tycons));
   1.619 -
   1.620 -
   1.621 -(* merge_abbrs *)
   1.622 -
   1.623 -fun merge_abbrs abbrs =
   1.624 -  Symtab.merge (op =) abbrs handle Symtab.DUPS dups => raise TERM (dup_tyabbrs dups, []);
   1.625 -
   1.626 -
   1.627 -(* merge_tsigs *)
   1.628 -
   1.629 -fun merge_tsigs
   1.630 - (TySg {classes = classes1, default = default1, classrel = classrel1, tycons = tycons1,
   1.631 -    log_types = _, univ_witness = _, arities = arities1, abbrs = abbrs1},
   1.632 -  TySg {classes = classes2, default = default2, classrel = classrel2, tycons = tycons2,
   1.633 -    log_types = _, univ_witness = _, arities = arities2, abbrs = abbrs2}) =
   1.634 -  let
   1.635 -    val classes' = classes1 union_string classes2;
   1.636 -    val classrel' = merge_classrel (classrel1, classrel2);
   1.637 -    val arities' = merge_arities classrel' (arities1, arities2);
   1.638 -    val tycons' = foldl add_tycons (tycons1, Symtab.dest tycons2);
   1.639 -    val default' = Sorts.norm_sort classrel' (default1 @ default2);
   1.640 -    val abbrs' = merge_abbrs (abbrs1, abbrs2);
   1.641 -  in
   1.642 -    make_tsig (classes', classrel', default', tycons', [], None, abbrs', arities')
   1.643 -    |> rebuild_tsig
   1.644 -  end;
   1.645 -
   1.646 -
   1.647 -
   1.648 -(*** extend type signatures ***)
   1.649 -
   1.650 -(** add classes and classrel relations **)
   1.651 -
   1.652 -fun add_classes classes cs =
   1.653 -  (case cs inter_string classes of
   1.654 -    [] => cs @ classes
   1.655 -  | dups => err_dup_classes cs);
   1.656 -
   1.657 -
   1.658 -(*'add_classrel' adds a tuple consisting of a new class (the new class has
   1.659 -  already been inserted into the 'classes' list) and its superclasses (they
   1.660 -  must be declared in 'classes' too) to the 'classrel' list of the given type
   1.661 -  signature; furthermore all inherited superclasses according to the
   1.662 -  superclasses brought with are inserted and there is a check that there are
   1.663 -  no cycles (i.e. C <= D <= C, with C <> D);*)
   1.664 -
   1.665 -fun add_classrel classes (classrel, (s, ges)) =
   1.666 -  let
   1.667 -    fun upd (classrel, s') =
   1.668 -      if s' mem_string classes then
   1.669 -        let val ges' = the (Symtab.lookup (classrel, s))
   1.670 -        in case Symtab.lookup (classrel, s') of
   1.671 -             Some sups => if s mem_string sups
   1.672 -                           then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s )
   1.673 -                           else Symtab.update ((s, sups union_string ges'), classrel)
   1.674 -           | None => classrel
   1.675 -        end
   1.676 -      else err_undeclared_class s'
   1.677 -  in foldl upd (Symtab.update ((s, ges), classrel), ges) end;
   1.678 -
   1.679 -
   1.680 -(* 'extend_classes' inserts all new classes into the corresponding
   1.681 -   lists ('classes', 'classrel') if possible *)
   1.682 -
   1.683 -fun extend_classes (classes, classrel, new_classes) =
   1.684 -  let
   1.685 -    val classes' = add_classes classes (map fst new_classes);
   1.686 -    val classrel' = foldl (add_classrel classes') (classrel, new_classes);
   1.687 -  in (classes', classrel') end;
   1.688 -
   1.689 -
   1.690 -(* ext_tsig_classes *)
   1.691 -
   1.692 -fun ext_tsig_classes tsig new_classes =
   1.693 -  let
   1.694 -    val TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;
   1.695 -    val (classes', classrel') = extend_classes (classes,classrel, new_classes);
   1.696 -  in
   1.697 -    make_tsig (classes', classrel', default, tycons, log_types, univ_witness, abbrs, arities)
   1.698 -    |> rebuild_tsig
   1.699 -  end;
   1.700 -
   1.701 -
   1.702 -(* ext_tsig_classrel *)
   1.703 -
   1.704 -fun ext_tsig_classrel tsig pairs =
   1.705 -  let
   1.706 -    val TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities} = tsig;
   1.707 -    val cert = cert_class tsig;
   1.708 -
   1.709 -    (* FIXME clean! *)
   1.710 -    val classrel' =
   1.711 -      merge_classrel (classrel, Symtab.make (map (fn (c1, c2) => (cert c1, [cert c2])) pairs));
   1.712 -  in
   1.713 -    make_tsig (classes, classrel', default, tycons, log_types, univ_witness, abbrs, arities)
   1.714 -    |> rebuild_tsig
   1.715 -  end;
   1.716 -
   1.717 -
   1.718 -(* ext_tsig_defsort *)
   1.719 -
   1.720 -fun ext_tsig_defsort
   1.721 -    (TySg {classes, classrel, default = _, tycons, log_types, univ_witness, abbrs, arities, ...}) default =
   1.722 -  make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities);
   1.723 -
   1.724 -
   1.725 -
   1.726 -(** add types **)
   1.727 -
   1.728 -fun ext_tsig_types (TySg {classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities}) ts =
   1.729 -  let
   1.730 -    fun check_type (c, n) =
   1.731 -      if n < 0 then err_neg_args c
   1.732 -      else if is_some (Symtab.lookup (tycons, c)) then err_dup_tycon c
   1.733 -      else if is_some (Symtab.lookup (abbrs, c)) then error (ty_confl c)
   1.734 -      else ();
   1.735 -    val _ = seq check_type ts;
   1.736 -    val tycons' = Symtab.extend (tycons, ts);
   1.737 -    val arities' = Symtab.extend (arities, map (rpair [] o #1) ts);
   1.738 -  in make_tsig (classes, classrel, default, tycons', log_types, univ_witness, abbrs, arities') end;
   1.739 -
   1.740 -
   1.741 -
   1.742 -(** add type abbreviations **)
   1.743 -
   1.744 -fun abbr_errors tsig (a, (lhs_vs, rhs)) =
   1.745 -  let
   1.746 -    val TySg {tycons, abbrs, ...} = tsig;
   1.747 -    val rhs_vs = map (#1 o #1) (typ_tvars rhs);
   1.748 -
   1.749 -    val dup_lhs_vars =
   1.750 -      (case duplicates lhs_vs of
   1.751 -        [] => []
   1.752 -      | vs => ["Duplicate variables on lhs: " ^ commas_quote vs]);
   1.753 -
   1.754 -    val extra_rhs_vars =
   1.755 -      (case gen_rems (op =) (rhs_vs, lhs_vs) of
   1.756 -        [] => []
   1.757 -      | vs => ["Extra variables on rhs: " ^ commas_quote vs]);
   1.758 -
   1.759 -    val tycon_confl =
   1.760 -      if is_none (Symtab.lookup (tycons, a)) then []
   1.761 -      else [ty_confl a];
   1.762 -
   1.763 -    val dup_abbr =
   1.764 -      if is_none (Symtab.lookup (abbrs, a)) then []
   1.765 -      else ["Duplicate declaration of abbreviation"];
   1.766 -  in
   1.767 -    dup_lhs_vars @ extra_rhs_vars @ tycon_confl @ dup_abbr @
   1.768 -      typ_errors tsig (rhs, [])
   1.769 -  end;
   1.770 -
   1.771 -fun prep_abbr tsig (a, vs, raw_rhs) =
   1.772 -  let
   1.773 -    fun err msgs = (seq error_msg msgs;
   1.774 -      error ("The error(s) above occurred in type abbreviation " ^ quote a));
   1.775 -
   1.776 -    val rhs = rem_sorts (varifyT (no_tvars raw_rhs))
   1.777 -      handle TYPE (msg, _, _) => err [msg];
   1.778 -    val abbr = (a, (vs, rhs));
   1.779 -  in
   1.780 -    (case abbr_errors tsig abbr of
   1.781 -      [] => abbr
   1.782 -    | msgs => err msgs)
   1.783 -  end;
   1.784 -
   1.785 -fun add_abbr
   1.786 -    (tsig as TySg {classes, classrel, default, tycons, log_types, univ_witness, arities, abbrs}, abbr) =
   1.787 -  make_tsig (classes, classrel, default, tycons, log_types, univ_witness,
   1.788 -    Symtab.update (prep_abbr tsig abbr, abbrs), arities);
   1.789 -
   1.790 -fun ext_tsig_abbrs tsig raw_abbrs = foldl add_abbr (tsig, raw_abbrs);
   1.791 -
   1.792 -
   1.793 -
   1.794 -(** add arities **)
   1.795 -
   1.796 -(* 'coregular' checks
   1.797 -   - the two restrictions 'is_unique_decl' and 'coreg'
   1.798 -   - if the classes in the new type declarations are known in the
   1.799 -     given type signature
   1.800 -   - if one type constructor has always the same number of arguments;
   1.801 -   if one type declaration has passed all checks it is inserted into
   1.802 -   the 'arities' association list of the given type signatrure  *)
   1.803 -
   1.804 -fun coregular (classes, classrel, tycons) =
   1.805 -  let fun ex C = if C mem_string classes then () else err_undeclared_class(C);
   1.806 -
   1.807 -      fun addar(arities, (t, (w, C))) = case Symtab.lookup (tycons, t) of
   1.808 -            Some(n) => if n <> length w then varying_decls(t) else
   1.809 -                     ((seq o seq) ex w; ex C;
   1.810 -                      let val ars = the (Symtab.lookup (arities, t))
   1.811 -                          val ars' = add_arity classrel ars (t,(C,w))
   1.812 -                      in Symtab.update ((t,ars'), arities) end)
   1.813 -          | None => error (undeclared_type t);
   1.814 -
   1.815 -  in addar end;
   1.816 -
   1.817 -
   1.818 -(* 'close' extends the 'arities' association list after all new type
   1.819 -   declarations have been inserted successfully:
   1.820 -   for every declaration t:(Ss)C , for all classses D with C <= D:
   1.821 -      if there is no declaration t:(Ss')C' with C < C' and C' <= D
   1.822 -      then insert the declaration t:(Ss)D into 'arities'
   1.823 -   this means, if there exists a declaration t:(Ss)C and there is
   1.824 -   no declaration t:(Ss')D with C <=D then the declaration holds
   1.825 -   for all range classes more general than C *)
   1.826 -
   1.827 -fun close classrel arities =
   1.828 -  let fun check sl (l, (s, dom)) = case Symtab.lookup (classrel, s) of
   1.829 -          Some sups =>
   1.830 -            let fun close_sup (l, sup) =
   1.831 -                  if exists (fn s'' => less classrel (s, s'') andalso
   1.832 -                                       leq classrel (s'', sup)) sl
   1.833 -                  then l
   1.834 -                  else (sup, dom)::l
   1.835 -            in foldl close_sup (l, sups) end
   1.836 -        | None => l;
   1.837 -      fun ext (s, l) = (s, foldl (check (map #1 l)) (l, l));
   1.838 -  in map ext arities end;
   1.839 -
   1.840 -
   1.841 -(* ext_tsig_arities *)
   1.842 -
   1.843 -fun norm_domain classrel =
   1.844 -  let fun one_min (f, (doms, ran)) = (f, (map (Sorts.norm_sort classrel) doms, ran))
   1.845 -  in map one_min end;
   1.846 -
   1.847 -fun ext_tsig_arities tsig sarities =
   1.848 -  let
   1.849 -    val TySg {classes, classrel, default, tycons, log_types, univ_witness, arities, abbrs} = tsig;
   1.850 -    val arities1 =
   1.851 -      flat (map (fn (t, ss, cs) => map (fn c => (t, (ss, c))) cs) sarities);
   1.852 -    val arities2 =
   1.853 -      foldl (coregular (classes, classrel, tycons)) (arities, norm_domain classrel arities1)
   1.854 -      |> Symtab.dest |> close classrel |> Symtab.make;
   1.855 -  in
   1.856 -    make_tsig (classes, classrel, default, tycons, log_types, univ_witness, abbrs, arities2)
   1.857 -    |> rebuild_tsig
   1.858 -  end;
   1.859 -
   1.860 -
   1.861 -
   1.862 -(*** type unification and friends ***)
   1.863 -
   1.864 -(** matching **)
   1.865 +(* matching *)
   1.866  
   1.867  exception TYPE_MATCH;
   1.868  
   1.869 @@ -710,7 +319,7 @@
   1.870    let
   1.871      fun match (subs, (TVar (v, S), T)) =
   1.872            (case Vartab.lookup (subs, v) of
   1.873 -            None => (Vartab.update_new ((v, (check_has_sort (tsig, T, S); T)), subs)
   1.874 +            None => (Vartab.update_new ((v, type_of_sort tsig (T, S)), subs)
   1.875                handle TYPE _ => raise TYPE_MATCH)
   1.876            | Some U => if U = T then subs else raise TYPE_MATCH)
   1.877        | match (subs, (Type (a, Ts), Type (b, Us))) =
   1.878 @@ -721,18 +330,15 @@
   1.879        | match _ = raise TYPE_MATCH;
   1.880    in match end;
   1.881  
   1.882 -fun typ_instance (tsig, T, U) =
   1.883 +fun typ_instance tsig (T, U) =
   1.884    (typ_match tsig (Vartab.empty, (U, T)); true) handle TYPE_MATCH => false;
   1.885  
   1.886  
   1.887 -
   1.888 -(** unification **)
   1.889 +(* unification *)
   1.890  
   1.891  exception TUNIFY;
   1.892  
   1.893 -
   1.894 -(* occurs check *)
   1.895 -
   1.896 +(*occurs_check*)
   1.897  fun occurs v tye =
   1.898    let
   1.899      fun occ (Type (_, Ts)) = exists occ Ts
   1.900 @@ -744,34 +350,28 @@
   1.901              | Some U => occ U);
   1.902    in occ end;
   1.903  
   1.904 -
   1.905 -(* chase variable assignments *)
   1.906 -
   1.907 -(*if devar returns a type var then it must be unassigned*)
   1.908 +(*chase variable assignments; if devar returns a type var then it must be unassigned*)
   1.909  fun devar (T as TVar (v, _), tye) =
   1.910        (case  Vartab.lookup (tye, v) of
   1.911          Some U => devar (U, tye)
   1.912        | None => T)
   1.913    | devar (T, tye) = T;
   1.914  
   1.915 -
   1.916 -(* unify *)
   1.917 -
   1.918 -fun unify (tsig as TySg {classrel, arities, ...}) (tyenv, maxidx) TU =
   1.919 +fun unify (tsig as TSig {classes, arities, ...}) (tyenv, maxidx) TU =
   1.920    let
   1.921      val tyvar_count = ref maxidx;
   1.922      fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
   1.923  
   1.924      fun mg_domain a S =
   1.925 -      Sorts.mg_domain (classrel, arities) a S handle Sorts.DOMAIN _ => raise TUNIFY;
   1.926 +      Sorts.mg_domain (classes, arities) a S handle Sorts.DOMAIN _ => raise TUNIFY;
   1.927  
   1.928      fun meet ((_, []), tye) = tye
   1.929        | meet ((TVar (xi, S'), S), tye) =
   1.930 -          if Sorts.sort_le classrel (S', S) then tye
   1.931 +          if Sorts.sort_le classes (S', S) then tye
   1.932            else Vartab.update_new ((xi,
   1.933 -            gen_tyvar (Sorts.inter_sort classrel (S', S))), tye)
   1.934 +            gen_tyvar (Sorts.inter_sort classes (S', S))), tye)
   1.935        | meet ((TFree (_, S'), S), tye) =
   1.936 -          if Sorts.sort_le classrel (S', S) then tye
   1.937 +          if Sorts.sort_le classes (S', S) then tye
   1.938            else raise TUNIFY
   1.939        | meet ((Type (a, Ts), S), tye) = meets ((Ts, mg_domain a S), tye)
   1.940      and meets (([], []), tye) = tye
   1.941 @@ -783,12 +383,12 @@
   1.942        (case (devar (ty1, tye), devar (ty2, tye)) of
   1.943          (T as TVar (v, S1), U as TVar (w, S2)) =>
   1.944            if eq_ix (v, w) then tye
   1.945 -          else if Sorts.sort_le classrel (S1, S2) then
   1.946 +          else if Sorts.sort_le classes (S1, S2) then
   1.947              Vartab.update_new ((w, T), tye)
   1.948 -          else if Sorts.sort_le classrel (S2, S1) then
   1.949 +          else if Sorts.sort_le classes (S2, S1) then
   1.950              Vartab.update_new ((v, U), tye)
   1.951            else
   1.952 -            let val S = gen_tyvar (Sorts.inter_sort classrel (S1, S2)) in
   1.953 +            let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in
   1.954                Vartab.update_new ((v, S), Vartab.update_new ((w, S), tye))
   1.955              end
   1.956        | (TVar (v, S), T) =>
   1.957 @@ -803,125 +403,206 @@
   1.958        | (T, U) => if T = U then tye else raise TUNIFY);
   1.959    in (unif (TU, tyenv), ! tyvar_count) end;
   1.960  
   1.961 -
   1.962 -(* raw_unify *)
   1.963 -
   1.964 -(*purely structural unification -- ignores sorts*)
   1.965 +(*purely structural unification *)
   1.966  fun raw_unify (ty1, ty2) =
   1.967 -  (unify tsig0 (Vartab.empty, 0) (rem_sorts ty1, rem_sorts ty2); true)
   1.968 +  (unify empty_tsig (Vartab.empty, 0) (strip_sorts ty1, strip_sorts ty2); true)
   1.969      handle TUNIFY => false;
   1.970  
   1.971  
   1.972  
   1.973 -(** type inference **)
   1.974 +(** extend and merge type signatures **)
   1.975 +
   1.976 +(* arities *)
   1.977 +
   1.978 +local
   1.979  
   1.980 -(* sort constraints *)
   1.981 +fun err_decl t decl = error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t);
   1.982 +fun err_undecl t = error ("Undeclared type constructor: " ^ quote t);
   1.983  
   1.984 -fun get_sort tsig def_sort map_sort raw_env =
   1.985 +fun err_conflict t (c1, c2) (c, Ss) (c', Ss') =
   1.986 +  error ("Conflict of type arities for classes " ^ quote c1 ^ " < " ^ quote c2 ^ ":\n  " ^
   1.987 +    Sorts.str_of_arity (t, Ss, [c]) ^ " and\n  " ^
   1.988 +    Sorts.str_of_arity (t, Ss', [c']));
   1.989 +
   1.990 +fun coregular C t (c, Ss) ars =
   1.991    let
   1.992 -    fun eq ((xi, S), (xi', S')) =
   1.993 -      xi = xi' andalso eq_sort tsig (S, S');
   1.994 +    fun conflict (c', Ss') =
   1.995 +      if Sorts.class_le C (c, c') andalso not (Sorts.sorts_le C (Ss, Ss')) then
   1.996 +        Some ((c, c'), (c', Ss'))
   1.997 +      else if Sorts.class_le C (c', c) andalso not (Sorts.sorts_le C (Ss', Ss)) then
   1.998 +        Some ((c', c), (c', Ss'))
   1.999 +      else None;
  1.1000 +  in
  1.1001 +    (case Library.get_first conflict ars of
  1.1002 +      Some ((c1, c2), (c', Ss')) => err_conflict t (c1, c2) (c, Ss) (c', Ss')
  1.1003 +    | None => (c, Ss) :: ars)
  1.1004 +  end;
  1.1005  
  1.1006 -    val env = gen_distinct eq (map (apsnd map_sort) raw_env);
  1.1007 -    val _ =
  1.1008 -      (case gen_duplicates eq_fst env of
  1.1009 -        [] => ()
  1.1010 -      | dups => error ("Inconsistent sort constraints for type variable(s) " ^
  1.1011 -          commas (map (quote o Syntax.string_of_vname' o fst) dups)));
  1.1012 +fun insert C t ((c, Ss), ars) =
  1.1013 +  (case assoc_string (ars, c) of
  1.1014 +    None => coregular C t (c, Ss) ars
  1.1015 +  | Some Ss' =>
  1.1016 +      if Sorts.sorts_le C (Ss, Ss') then ars
  1.1017 +      else if Sorts.sorts_le C (Ss', Ss)
  1.1018 +      then coregular C t (c, Ss) (ars \ (c, Ss'))
  1.1019 +      else coregular C t (c, Ss) ars);
  1.1020  
  1.1021 -    fun get xi =
  1.1022 -      (case (assoc (env, xi), def_sort xi) of
  1.1023 -        (None, None) => defaultS tsig
  1.1024 -      | (None, Some S) => S
  1.1025 -      | (Some S, None) => S
  1.1026 -      | (Some S, Some S') =>
  1.1027 -          if eq_sort tsig (S, S') then S'
  1.1028 -          else error ("Sort constraint inconsistent with default for type variable " ^
  1.1029 -            quote (Syntax.string_of_vname' xi)));
  1.1030 -  in get end;
  1.1031 +fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]);
  1.1032  
  1.1033 +fun insert_arities classes (arities, (t, ars)) =
  1.1034 +  let val ars' =
  1.1035 +    Symtab.lookup_multi (arities, t)
  1.1036 +    |> curry (foldr (insert classes t)) (flat (map (complete classes) ars))
  1.1037 +  in Symtab.update ((t, ars'), arities) end;
  1.1038  
  1.1039 -(* type constraints *)
  1.1040 +fun insert_table classes = Symtab.foldl (fn (arities, (t, ars)) =>
  1.1041 +  insert_arities classes (arities, (t, map (apsnd (map (Sorts.norm_sort classes))) ars)));
  1.1042 +
  1.1043 +in
  1.1044  
  1.1045 -fun constrain t T =
  1.1046 -  if T = dummyT then t
  1.1047 -  else Const ("_type_constraint_", T) $ t;
  1.1048 -
  1.1049 -
  1.1050 -(* user parameters *)
  1.1051 +fun add_arities decls tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
  1.1052 +  let
  1.1053 +    fun prep (t, Ss, S) =
  1.1054 +      (case Symtab.lookup (types, t) of
  1.1055 +        Some (LogicalType n, _) =>
  1.1056 +          if length Ss = n then
  1.1057 +            (t, map (cert_sort tsig) Ss, cert_sort tsig S)
  1.1058 +              handle TYPE (msg, _, _) => error msg
  1.1059 +          else error (bad_nargs t)
  1.1060 +      | Some (decl, _) => err_decl t decl
  1.1061 +      | None => err_undecl t);
  1.1062  
  1.1063 -fun is_param (x, _) = size x > 0 andalso ord x = ord "?";
  1.1064 -fun param i (x, S) = TVar (("?" ^ x, i), S);
  1.1065 +    val ars = decls |> map ((fn (t, Ss, S) => (t, map (fn c => (c, Ss)) S)) o prep);
  1.1066 +    val arities' = foldl (insert_arities classes) (arities, ars);
  1.1067 +  in (classes, default, types, arities') end);
  1.1068  
  1.1069 -fun paramify_dummies (maxidx, TFree ("'_dummy_", S)) =
  1.1070 -      (maxidx + 1, param (maxidx + 1) ("'dummy", S))
  1.1071 -  | paramify_dummies (maxidx, Type (a, Ts)) =
  1.1072 -      let val (maxidx', Ts') = foldl_map paramify_dummies (maxidx, Ts)
  1.1073 -      in (maxidx', Type (a, Ts')) end
  1.1074 -  | paramify_dummies arg = arg;
  1.1075 +fun rebuild_arities classes arities =
  1.1076 +  insert_table classes (Symtab.empty, arities);
  1.1077 +
  1.1078 +fun merge_arities classes (arities1, arities2) =
  1.1079 +  insert_table classes (insert_table classes (Symtab.empty, arities1), arities2);
  1.1080 +
  1.1081 +end;
  1.1082  
  1.1083  
  1.1084 -(* decode_types *)
  1.1085 +(* classes *)
  1.1086 +
  1.1087 +local
  1.1088  
  1.1089 -(*transform parse tree into raw term*)
  1.1090 -fun decode_types tsig is_const def_type def_sort map_const map_type map_sort tm =
  1.1091 +fun err_dup_classes cs =
  1.1092 +  error ("Duplicate declaration of class(es): " ^ commas_quote cs);
  1.1093 +
  1.1094 +fun err_cyclic_classes css =
  1.1095 +  error (cat_lines (map (fn cs =>
  1.1096 +    "Cycle in class relation: " ^ space_implode " < " (map quote cs)) css));
  1.1097 +
  1.1098 +fun add_class (c, cs) tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
  1.1099    let
  1.1100 -    fun get_type xi = if_none (def_type xi) dummyT;
  1.1101 -    fun is_free x = is_some (def_type (x, ~1));
  1.1102 -    val raw_env = Syntax.raw_term_sorts tm;
  1.1103 -    val sort_of = get_sort tsig def_sort map_sort raw_env;
  1.1104 +    val cs' = map (cert_class tsig) cs
  1.1105 +      handle TYPE (msg, _, _) => error msg;
  1.1106 +    val classes' = classes |> Graph.new_node (c, stamp ())
  1.1107 +      handle Graph.DUP d => err_dup_classes [d];
  1.1108 +    val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs')
  1.1109 +      handle Graph.CYCLES css => err_cyclic_classes css;
  1.1110 +  in (classes'', default, types, arities) end);
  1.1111  
  1.1112 -    val certT = cert_typ tsig o map_type;
  1.1113 -    fun decodeT t = certT (Syntax.typ_of_term sort_of map_sort t);
  1.1114 +in
  1.1115  
  1.1116 -    fun decode (Const ("_constrain", _) $ t $ typ) =
  1.1117 -          constrain (decode t) (decodeT typ)
  1.1118 -      | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
  1.1119 -          if T = dummyT then Abs (x, decodeT typ, decode t)
  1.1120 -          else constrain (Abs (x, certT T, decode t)) (decodeT typ --> dummyT)
  1.1121 -      | decode (Abs (x, T, t)) = Abs (x, certT T, decode t)
  1.1122 -      | decode (t $ u) = decode t $ decode u
  1.1123 -      | decode (Free (x, T)) =
  1.1124 -          let val c = map_const x in
  1.1125 -            if not (is_free x) andalso (is_const c orelse NameSpace.is_qualified c) then
  1.1126 -              Const (c, certT T)
  1.1127 -            else if T = dummyT then Free (x, get_type (x, ~1))
  1.1128 -            else constrain (Free (x, certT T)) (get_type (x, ~1))
  1.1129 -          end
  1.1130 -      | decode (Var (xi, T)) =
  1.1131 -          if T = dummyT then Var (xi, get_type xi)
  1.1132 -          else constrain (Var (xi, certT T)) (get_type xi)
  1.1133 -      | decode (t as Bound _) = t
  1.1134 -      | decode (Const (c, T)) = Const (map_const c, certT T);
  1.1135 -  in decode tm end;
  1.1136 +val add_classes = fold add_class;
  1.1137 +
  1.1138 +fun add_classrel ps tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
  1.1139 +  let
  1.1140 +    val ps' = map (pairself (cert_class tsig)) ps
  1.1141 +      handle TYPE (msg, _, _) => error msg;
  1.1142 +    val classes' = classes |> fold Graph.add_edge_trans_acyclic ps'
  1.1143 +      handle Graph.CYCLES css => err_cyclic_classes css;
  1.1144 +    val default' = default |> Sorts.norm_sort classes';
  1.1145 +    val arities' = arities |> rebuild_arities classes';
  1.1146 +  in (classes', default', types, arities') end);
  1.1147 +
  1.1148 +fun merge_classes CC = Graph.merge_trans_acyclic (op =) CC
  1.1149 +  handle Graph.DUPS cs => err_dup_classes cs
  1.1150 +    | Graph.CYCLES css => err_cyclic_classes css;
  1.1151 +
  1.1152 +end;
  1.1153 +
  1.1154 +
  1.1155 +(* default sort *)
  1.1156 +
  1.1157 +fun set_defsort S tsig = tsig |> change_tsig (fn (classes, _, types, arities) =>
  1.1158 +  (classes, cert_sort tsig S handle TYPE (msg, _, _) => error msg, types, arities));
  1.1159  
  1.1160  
  1.1161 -(* infer_types *)
  1.1162 +(* types *)
  1.1163 +
  1.1164 +local
  1.1165 +
  1.1166 +fun err_neg_args c =
  1.1167 +  error ("Negative number of arguments in type constructor declaration: " ^ quote c);
  1.1168  
  1.1169 -(*
  1.1170 -  Given [T1,...,Tn] and [t1,...,tn], ensure that the type of ti
  1.1171 -  unifies with Ti (for i=1,...,n).
  1.1172 +fun err_in_decls c decl decl' =
  1.1173 +  let
  1.1174 +    val s = str_of_decl decl;
  1.1175 +    val s' = str_of_decl decl';
  1.1176 +  in
  1.1177 +    if s = s' then error ("Duplicate declaration of " ^ s ^ ": " ^ quote c)
  1.1178 +    else error ("Conflicting declarations of " ^ s ^ " with " ^ s' ^ ": " ^ quote c)
  1.1179 +  end;
  1.1180 +
  1.1181 +fun new_decl (c, decl) types =
  1.1182 +  (case Symtab.lookup (types, c) of
  1.1183 +    Some (decl', _) => err_in_decls c decl decl'
  1.1184 +  | None => Symtab.update ((c, (decl, stamp ())), types));
  1.1185 +
  1.1186 +fun the_decl types c = fst (the (Symtab.lookup (types, c)));
  1.1187 +
  1.1188 +fun change_types f = change_tsig (fn (classes, default, types, arities) =>
  1.1189 +  (classes, default, f types, arities));
  1.1190  
  1.1191 -  tsig: type signature
  1.1192 -  const_type: name mapping and signature lookup
  1.1193 -  def_type: partial map from indexnames to types (constrains Frees, Vars)
  1.1194 -  def_sort: partial map from indexnames to sorts (constrains TFrees, TVars)
  1.1195 -  used: list of already used type variables
  1.1196 -  freeze: if true then generated parameters are turned into TFrees, else TVars
  1.1197 -*)
  1.1198 +fun add_abbr (a, vs, rhs) tsig = tsig |> change_types (fn types =>
  1.1199 +  let
  1.1200 +    fun err msg =
  1.1201 +      error (msg ^ "\nThe error(s) above occurred in type abbreviation " ^ quote a);
  1.1202 +    val rhs' = strip_sorts (varifyT (no_tvars (cert_typ_syntax tsig rhs)))
  1.1203 +      handle TYPE (msg, _, _) => err msg;
  1.1204 +  in
  1.1205 +    (case duplicates vs of
  1.1206 +      [] => []
  1.1207 +    | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups));
  1.1208 +    (case gen_rems (op =) (map (#1 o #1) (typ_tvars rhs'), vs) of
  1.1209 +      [] => []
  1.1210 +    | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
  1.1211 +    types |> new_decl (a, Abbreviation (vs, rhs'))
  1.1212 +  end);
  1.1213  
  1.1214 -fun infer_types prt prT tsig const_type def_type def_sort
  1.1215 -    map_const map_type map_sort used freeze pat_Ts raw_ts =
  1.1216 -  let
  1.1217 -    val TySg {classrel, arities, ...} = tsig;
  1.1218 -    val pat_Ts' = map (cert_typ tsig) pat_Ts;
  1.1219 -    val is_const = is_some o const_type;
  1.1220 -    val raw_ts' =
  1.1221 -      map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;
  1.1222 -    val (ts, Ts, unifier) =
  1.1223 -      TypeInfer.infer_types prt prT const_type classrel arities used freeze
  1.1224 -        is_param raw_ts' pat_Ts';
  1.1225 -  in (ts, unifier) end;
  1.1226 +in
  1.1227 +
  1.1228 +fun add_types ps = change_types (fold new_decl (ps |> map (fn (c, n) =>
  1.1229 +  if n < 0 then err_neg_args c else (c, LogicalType n))));
  1.1230 +
  1.1231 +val add_abbrs = fold add_abbr;
  1.1232 +val add_nonterminals = change_types o fold new_decl o map (rpair Nonterminal);
  1.1233 +
  1.1234 +fun merge_types (types1, types2) =
  1.1235 +  Symtab.merge Library.eq_snd (types1, types2) handle Symtab.DUPS (d :: _) =>
  1.1236 +    err_in_decls d (the_decl types1 d) (the_decl types2 d);
  1.1237 +
  1.1238 +end;
  1.1239  
  1.1240  
  1.1241 +(* merge type signatures *)
  1.1242 +
  1.1243 +fun merge_tsigs (tsig1, tsig2) =
  1.1244 +  let
  1.1245 +    val (TSig {classes = classes1, default = default1, types = types1, arities = arities1,
  1.1246 +      log_types = _, witness = _}) = tsig1;
  1.1247 +    val (TSig {classes = classes2, default = default2, types = types2, arities = arities2,
  1.1248 +      log_types = _, witness = _}) = tsig2;
  1.1249 +
  1.1250 +    val classes' = merge_classes (classes1, classes2);
  1.1251 +    val default' = Sorts.inter_sort classes' (default1, default2);
  1.1252 +    val types' = merge_types (types1, types2);
  1.1253 +    val arities' = merge_arities classes' (arities1, arities2);
  1.1254 +  in build_tsig (classes', default', types', arities') end;
  1.1255 +
  1.1256  end;