src/Pure/type.ML
author wenzelm
Fri May 21 21:26:19 2004 +0200 (2004-05-21 ago)
changeset 14790 0d984ee030a1
parent 13666 a2730043029b
child 14830 faa4865ba1ce
permissions -rw-r--r--
major cleanup of tsig datastructures and extend/merge operations; fixes old bugs in classes/arities code; proper treatment of nonterminals and syntax-only types;
     1 (*  Title:      Pure/type.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel
     4 
     5 Type signatures and certified types, special treatment of type vars,
     6 matching and unification of types, extend and merge type signatures.
     7 *)
     8 
     9 signature TYPE =
    10 sig
    11   (*type signatures and certified types*)
    12   datatype decl =
    13     LogicalType of int |
    14     Abbreviation of string list * typ |
    15     Nonterminal
    16   type tsig
    17   val rep_tsig: tsig ->
    18    {classes: Sorts.classes,
    19     default: sort,
    20     types: (decl * stamp) Symtab.table,
    21     arities: Sorts.arities,
    22     log_types: string list,
    23     witness: (typ * sort) option}
    24   val empty_tsig: tsig
    25   val classes: tsig -> class list
    26   val defaultS: tsig -> sort
    27   val logical_types: tsig -> string list
    28   val universal_witness: tsig -> (typ * sort) option
    29   val eq_sort: tsig -> sort * sort -> bool
    30   val subsort: tsig -> sort * sort -> bool
    31   val of_sort: tsig -> typ * sort -> bool
    32   val cert_class: tsig -> class -> class
    33   val cert_sort: tsig -> sort -> sort
    34   val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list
    35   val norm_typ: tsig -> typ -> typ
    36   val cert_typ: tsig -> typ -> typ
    37   val cert_typ_syntax: tsig -> typ -> typ
    38   val cert_typ_raw: tsig -> typ -> typ
    39 
    40   (*special treatment of type vars*)
    41   val strip_sorts: typ -> typ
    42   val no_tvars: typ -> typ
    43   val varifyT: typ -> typ
    44   val unvarifyT: typ -> typ
    45   val varify: term * string list -> term * (string * indexname) list
    46   val freeze_thaw_type : typ -> typ * (typ -> typ)
    47   val freeze_thaw : term -> term * (term -> term)
    48 
    49   (*matching and unification*)
    50   val inst_term_tvars: tsig -> (indexname * typ) list -> term -> term
    51   val inst_typ_tvars: tsig -> (indexname * typ) list -> typ -> typ
    52   exception TYPE_MATCH
    53   val typ_match: tsig -> typ Vartab.table * (typ * typ) -> typ Vartab.table
    54   val typ_instance: tsig -> typ * typ -> bool
    55   exception TUNIFY
    56   val unify: tsig -> typ Vartab.table * int -> typ * typ -> typ Vartab.table * int
    57   val raw_unify: typ * typ -> bool
    58 
    59   (*extend and merge type signatures*)
    60   val add_classes: (class * class list) list -> tsig -> tsig
    61   val add_classrel: (class * class) list -> tsig -> tsig
    62   val set_defsort: sort -> tsig -> tsig
    63   val add_types: (string * int) list -> tsig -> tsig
    64   val add_abbrs: (string * string list * typ) list -> tsig -> tsig
    65   val add_nonterminals: string list -> tsig -> tsig
    66   val add_arities: (string * sort list * sort) list -> tsig -> tsig
    67   val merge_tsigs: tsig * tsig -> tsig
    68 end;
    69 
    70 structure Type: TYPE =
    71 struct
    72 
    73 (** type signatures and certified types **)
    74 
    75 (* type declarations *)
    76 
    77 datatype decl =
    78   LogicalType of int |
    79   Abbreviation of string list * typ |
    80   Nonterminal;
    81 
    82 fun str_of_decl (LogicalType _) = "logical type constructor"
    83   | str_of_decl (Abbreviation _) = "type abbreviation"
    84   | str_of_decl Nonterminal = "syntactic type";
    85 
    86 
    87 (* type tsig *)
    88 
    89 datatype tsig =
    90   TSig of {
    91     classes: Sorts.classes,              (*declared classes with proper subclass relation*)
    92     default: sort,                       (*default sort on input*)
    93     types: (decl * stamp) Symtab.table,  (*declared types*)
    94     arities: Sorts.arities,              (*image specification of types wrt. sorts*)
    95     log_types: string list,              (*logical types sorted by number of arguments*)
    96     witness: (typ * sort) option};       (*witness for non-emptiness of strictest sort*)
    97 
    98 fun rep_tsig (TSig comps) = comps;
    99 
   100 fun make_tsig (classes, default, types, arities, log_types, witness) =
   101   TSig {classes = classes, default = default, types = types, arities = arities,
   102     log_types = log_types, witness = witness};
   103 
   104 fun map_tsig f (TSig {classes, default, types, arities, log_types, witness}) =
   105   make_tsig (f (classes, default, types, arities, log_types, witness));
   106 
   107 fun build_tsig (classes, default, types, arities) =
   108   let
   109     fun add_log_type (ts, (c, (LogicalType n, _))) = (c, n) :: ts
   110       | add_log_type (ts, _) = ts;
   111     val log_types =
   112       Symtab.foldl add_log_type ([], types)
   113       |> Library.sort (Library.int_ord o pairself #2) |> map #1;
   114     val witness =
   115       (case Sorts.witness_sorts (classes, arities) log_types [] [Graph.keys classes] of
   116         [w] => Some w | _ => None);
   117   in make_tsig (classes, default, types, arities, log_types, witness) end;
   118 
   119 fun change_tsig f (TSig {classes, default, types, arities, log_types = _, witness = _}) =
   120   build_tsig (f (classes, default, types, arities));
   121 
   122 val empty_tsig = build_tsig (Graph.empty, [], Symtab.empty, Symtab.empty);
   123 
   124 
   125 (* classes and sorts *)
   126 
   127 fun classes (TSig {classes = C, ...}) = Graph.keys C;
   128 fun defaultS (TSig {default, ...}) = default;
   129 fun logical_types (TSig {log_types, ...}) = log_types;
   130 fun universal_witness (TSig {witness, ...}) = witness;
   131 
   132 fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq classes;
   133 fun subsort (TSig {classes, ...}) = Sorts.sort_le classes;
   134 fun of_sort (TSig {classes, arities, ...}) = Sorts.of_sort (classes, arities);
   135 fun norm_sort (TSig {classes, ...}) = Sorts.norm_sort classes;
   136 
   137 fun cert_class (TSig {classes, ...}) c =
   138   if can (Graph.get_node classes) c then c
   139   else raise TYPE ("Undeclared class: " ^ quote c, [], []);
   140 
   141 fun cert_sort tsig = norm_sort tsig o map (cert_class tsig);
   142 
   143 fun witness_sorts (tsig as TSig {classes, arities, log_types, ...}) =
   144   Sorts.witness_sorts (classes, arities) log_types;
   145 
   146 
   147 (* certified types *)
   148 
   149 fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t;
   150 
   151 fun inst_typ tye =
   152   let
   153     fun inst (var as (v, _)) =
   154       (case assoc_string_int (tye, v) of
   155         Some U => inst_typ tye U
   156       | None => TVar var);
   157   in map_type_tvar inst end;
   158 
   159 (*expand type abbreviations and normalize sorts*)
   160 fun norm_typ (tsig as TSig {types, ...}) ty =
   161   let
   162     val idx = Term.maxidx_of_typ ty + 1;
   163 
   164     fun norm (Type (a, Ts)) =
   165           (case Symtab.lookup (types, a) of
   166             Some (Abbreviation (vs, U), _) =>
   167               norm (inst_typ (map (rpair idx) vs ~~ Ts) (incr_tvar idx U))
   168           | _ => Type (a, map norm Ts))
   169       | norm (TFree (x, S)) = TFree (x, norm_sort tsig S)
   170       | norm (TVar (xi, S)) = TVar (xi, norm_sort tsig S);
   171 
   172     val ty' = norm ty;
   173   in if ty = ty' then ty else ty' end;  (*avoid copying of already normal type*)
   174 
   175 (*check validity of (not necessarily normal) type*)   (*exception TYPE*)
   176 fun certify_typ normalize syntax tsig ty =
   177   let
   178     val TSig {types, ...} = tsig;
   179     fun err msg = raise TYPE (msg, [ty], []);
   180 
   181     fun check_sort S = (map (cert_class tsig) S; ());
   182 
   183     fun check_typ (Type (c, Ts)) =
   184           let fun nargs n = if length Ts <> n then err (bad_nargs c) else () in
   185             (case Symtab.lookup (types, c) of
   186               Some (LogicalType n, _) => nargs n
   187             | Some (Abbreviation (vs, _), _) => nargs (length vs)
   188             | Some (Nonterminal, _) => nargs 0
   189             | None => err ("Undeclared type constructor: " ^ quote c));
   190             seq check_typ Ts
   191           end
   192     | check_typ (TFree (_, S)) = check_sort S
   193     | check_typ (TVar ((x, i), S)) =
   194         if i < 0 then err ("Malformed type variable: " ^ quote (Term.string_of_vname (x, i)))
   195         else check_sort S;
   196 
   197     fun no_syntax (Type (c, Ts)) =
   198           (case Symtab.lookup (types, c) of
   199             Some (Nonterminal, _) =>
   200               err ("Illegal occurrence of syntactic type: " ^ quote c)
   201           | _ => seq no_syntax Ts)
   202       | no_syntax _ = ();
   203 
   204     val _ = check_typ ty;
   205     val ty' = if normalize orelse not syntax then norm_typ tsig ty else ty;
   206     val _ = if not syntax then no_syntax ty' else ();
   207   in ty' end;
   208 
   209 val cert_typ         = certify_typ true false;
   210 val cert_typ_syntax  = certify_typ true true;
   211 val cert_typ_raw     = certify_typ false true;
   212 
   213 
   214 
   215 (** special treatment of type vars **)
   216 
   217 (* strip_sorts *)
   218 
   219 fun strip_sorts (Type (a, Ts)) = Type (a, map strip_sorts Ts)
   220   | strip_sorts (TFree (x, _)) = TFree (x, [])
   221   | strip_sorts (TVar (xi, _)) = TVar (xi, []);
   222 
   223 
   224 (* no_tvars *)
   225 
   226 fun no_tvars T =
   227   (case typ_tvars T of [] => T
   228   | vs => raise TYPE ("Illegal schematic type variable(s): " ^
   229       commas (map (Term.string_of_vname o #1) vs), [T], []));
   230 
   231 
   232 (* varify, unvarify *)
   233 
   234 val varifyT = map_type_tfree (fn (a, S) => TVar ((a, 0), S));
   235 
   236 fun unvarifyT (Type (a, Ts)) = Type (a, map unvarifyT Ts)
   237   | unvarifyT (TVar ((a, 0), S)) = TFree (a, S)
   238   | unvarifyT T = T;
   239 
   240 fun varify (t, fixed) =
   241   let
   242     val fs = add_term_tfree_names (t, []) \\ fixed;
   243     val ixns = add_term_tvar_ixns (t, []);
   244     val fmap = fs ~~ map (rpair 0) (variantlist (fs, map #1 ixns))
   245     fun thaw (f as (a, S)) =
   246       (case assoc (fmap, a) of
   247         None => TFree f
   248       | Some b => TVar (b, S));
   249   in (map_term_types (map_type_tfree thaw) t, fmap) end;
   250 
   251 
   252 (* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)
   253 
   254 local
   255 
   256 fun new_name (ix, (pairs,used)) =
   257       let val v = variant used (string_of_indexname ix)
   258       in  ((ix,v)::pairs, v::used)  end;
   259 
   260 fun freeze_one alist (ix,sort) =
   261   TFree (the (assoc (alist, ix)), sort)
   262     handle OPTION =>
   263       raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
   264 
   265 fun thaw_one alist (a,sort) = TVar (the (assoc (alist,a)), sort)
   266       handle OPTION => TFree(a,sort);
   267 
   268 in
   269 
   270 (*this sort of code could replace unvarifyT*)
   271 fun freeze_thaw_type T =
   272   let
   273     val used = add_typ_tfree_names (T, [])
   274     and tvars = map #1 (add_typ_tvars (T, []));
   275     val (alist, _) = foldr new_name (tvars, ([], used));
   276   in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
   277 
   278 fun freeze_thaw t =
   279   let
   280     val used = it_term_types add_typ_tfree_names (t, [])
   281     and tvars = map #1 (it_term_types add_typ_tvars (t, []));
   282     val (alist, _) = foldr new_name (tvars, ([], used));
   283   in
   284     (case alist of
   285       [] => (t, fn x => x) (*nothing to do!*)
   286     | _ => (map_term_types (map_type_tvar (freeze_one alist)) t,
   287       map_term_types (map_type_tfree (thaw_one (map swap alist)))))
   288   end;
   289 
   290 end;
   291 
   292 
   293 
   294 (** matching and unification of types **)
   295 
   296 (* instantiation *)
   297 
   298 fun type_of_sort tsig (T, S) =
   299   if of_sort tsig (T, S) then T
   300   else raise TYPE ("Type not of sort " ^ Sorts.str_of_sort S, [T], []);
   301 
   302 fun inst_typ_tvars tsig tye =
   303   let
   304     fun inst (var as (v, S)) =
   305       (case assoc_string_int (tye, v) of
   306         Some U => type_of_sort tsig (U, S)
   307       | None => TVar var);
   308   in map_type_tvar inst end;
   309 
   310 fun inst_term_tvars _ [] t = t
   311   | inst_term_tvars tsig tye t = map_term_types (inst_typ_tvars tsig tye) t;
   312 
   313 
   314 (* matching *)
   315 
   316 exception TYPE_MATCH;
   317 
   318 fun typ_match tsig =
   319   let
   320     fun match (subs, (TVar (v, S), T)) =
   321           (case Vartab.lookup (subs, v) of
   322             None => (Vartab.update_new ((v, type_of_sort tsig (T, S)), subs)
   323               handle TYPE _ => raise TYPE_MATCH)
   324           | Some U => if U = T then subs else raise TYPE_MATCH)
   325       | match (subs, (Type (a, Ts), Type (b, Us))) =
   326           if a <> b then raise TYPE_MATCH
   327           else foldl match (subs, Ts ~~ Us)
   328       | match (subs, (TFree x, TFree y)) =
   329           if x = y then subs else raise TYPE_MATCH
   330       | match _ = raise TYPE_MATCH;
   331   in match end;
   332 
   333 fun typ_instance tsig (T, U) =
   334   (typ_match tsig (Vartab.empty, (U, T)); true) handle TYPE_MATCH => false;
   335 
   336 
   337 (* unification *)
   338 
   339 exception TUNIFY;
   340 
   341 (*occurs_check*)
   342 fun occurs v tye =
   343   let
   344     fun occ (Type (_, Ts)) = exists occ Ts
   345       | occ (TFree _) = false
   346       | occ (TVar (w, _)) =
   347           eq_ix (v, w) orelse
   348             (case Vartab.lookup (tye, w) of
   349               None => false
   350             | Some U => occ U);
   351   in occ end;
   352 
   353 (*chase variable assignments; if devar returns a type var then it must be unassigned*)
   354 fun devar (T as TVar (v, _), tye) =
   355       (case  Vartab.lookup (tye, v) of
   356         Some U => devar (U, tye)
   357       | None => T)
   358   | devar (T, tye) = T;
   359 
   360 fun unify (tsig as TSig {classes, arities, ...}) (tyenv, maxidx) TU =
   361   let
   362     val tyvar_count = ref maxidx;
   363     fun gen_tyvar S = TVar (("'a", inc tyvar_count), S);
   364 
   365     fun mg_domain a S =
   366       Sorts.mg_domain (classes, arities) a S handle Sorts.DOMAIN _ => raise TUNIFY;
   367 
   368     fun meet ((_, []), tye) = tye
   369       | meet ((TVar (xi, S'), S), tye) =
   370           if Sorts.sort_le classes (S', S) then tye
   371           else Vartab.update_new ((xi,
   372             gen_tyvar (Sorts.inter_sort classes (S', S))), tye)
   373       | meet ((TFree (_, S'), S), tye) =
   374           if Sorts.sort_le classes (S', S) then tye
   375           else raise TUNIFY
   376       | meet ((Type (a, Ts), S), tye) = meets ((Ts, mg_domain a S), tye)
   377     and meets (([], []), tye) = tye
   378       | meets ((T :: Ts, S :: Ss), tye) =
   379           meets ((Ts, Ss), meet ((devar (T, tye), S), tye))
   380       | meets _ = sys_error "meets";
   381 
   382     fun unif ((ty1, ty2), tye) =
   383       (case (devar (ty1, tye), devar (ty2, tye)) of
   384         (T as TVar (v, S1), U as TVar (w, S2)) =>
   385           if eq_ix (v, w) then tye
   386           else if Sorts.sort_le classes (S1, S2) then
   387             Vartab.update_new ((w, T), tye)
   388           else if Sorts.sort_le classes (S2, S1) then
   389             Vartab.update_new ((v, U), tye)
   390           else
   391             let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in
   392               Vartab.update_new ((v, S), Vartab.update_new ((w, S), tye))
   393             end
   394       | (TVar (v, S), T) =>
   395           if occurs v tye T then raise TUNIFY
   396           else meet ((T, S), Vartab.update_new ((v, T), tye))
   397       | (T, TVar (v, S)) =>
   398           if occurs v tye T then raise TUNIFY
   399           else meet ((T, S), Vartab.update_new ((v, T), tye))
   400       | (Type (a, Ts), Type (b, Us)) =>
   401           if a <> b then raise TUNIFY
   402           else foldr unif (Ts ~~ Us, tye)
   403       | (T, U) => if T = U then tye else raise TUNIFY);
   404   in (unif (TU, tyenv), ! tyvar_count) end;
   405 
   406 (*purely structural unification *)
   407 fun raw_unify (ty1, ty2) =
   408   (unify empty_tsig (Vartab.empty, 0) (strip_sorts ty1, strip_sorts ty2); true)
   409     handle TUNIFY => false;
   410 
   411 
   412 
   413 (** extend and merge type signatures **)
   414 
   415 (* arities *)
   416 
   417 local
   418 
   419 fun err_decl t decl = error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t);
   420 fun err_undecl t = error ("Undeclared type constructor: " ^ quote t);
   421 
   422 fun err_conflict t (c1, c2) (c, Ss) (c', Ss') =
   423   error ("Conflict of type arities for classes " ^ quote c1 ^ " < " ^ quote c2 ^ ":\n  " ^
   424     Sorts.str_of_arity (t, Ss, [c]) ^ " and\n  " ^
   425     Sorts.str_of_arity (t, Ss', [c']));
   426 
   427 fun coregular C t (c, Ss) ars =
   428   let
   429     fun conflict (c', Ss') =
   430       if Sorts.class_le C (c, c') andalso not (Sorts.sorts_le C (Ss, Ss')) then
   431         Some ((c, c'), (c', Ss'))
   432       else if Sorts.class_le C (c', c) andalso not (Sorts.sorts_le C (Ss', Ss)) then
   433         Some ((c', c), (c', Ss'))
   434       else None;
   435   in
   436     (case Library.get_first conflict ars of
   437       Some ((c1, c2), (c', Ss')) => err_conflict t (c1, c2) (c, Ss) (c', Ss')
   438     | None => (c, Ss) :: ars)
   439   end;
   440 
   441 fun insert C t ((c, Ss), ars) =
   442   (case assoc_string (ars, c) of
   443     None => coregular C t (c, Ss) ars
   444   | Some Ss' =>
   445       if Sorts.sorts_le C (Ss, Ss') then ars
   446       else if Sorts.sorts_le C (Ss', Ss)
   447       then coregular C t (c, Ss) (ars \ (c, Ss'))
   448       else coregular C t (c, Ss) ars);
   449 
   450 fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]);
   451 
   452 fun insert_arities classes (arities, (t, ars)) =
   453   let val ars' =
   454     Symtab.lookup_multi (arities, t)
   455     |> curry (foldr (insert classes t)) (flat (map (complete classes) ars))
   456   in Symtab.update ((t, ars'), arities) end;
   457 
   458 fun insert_table classes = Symtab.foldl (fn (arities, (t, ars)) =>
   459   insert_arities classes (arities, (t, map (apsnd (map (Sorts.norm_sort classes))) ars)));
   460 
   461 in
   462 
   463 fun add_arities decls tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
   464   let
   465     fun prep (t, Ss, S) =
   466       (case Symtab.lookup (types, t) of
   467         Some (LogicalType n, _) =>
   468           if length Ss = n then
   469             (t, map (cert_sort tsig) Ss, cert_sort tsig S)
   470               handle TYPE (msg, _, _) => error msg
   471           else error (bad_nargs t)
   472       | Some (decl, _) => err_decl t decl
   473       | None => err_undecl t);
   474 
   475     val ars = decls |> map ((fn (t, Ss, S) => (t, map (fn c => (c, Ss)) S)) o prep);
   476     val arities' = foldl (insert_arities classes) (arities, ars);
   477   in (classes, default, types, arities') end);
   478 
   479 fun rebuild_arities classes arities =
   480   insert_table classes (Symtab.empty, arities);
   481 
   482 fun merge_arities classes (arities1, arities2) =
   483   insert_table classes (insert_table classes (Symtab.empty, arities1), arities2);
   484 
   485 end;
   486 
   487 
   488 (* classes *)
   489 
   490 local
   491 
   492 fun err_dup_classes cs =
   493   error ("Duplicate declaration of class(es): " ^ commas_quote cs);
   494 
   495 fun err_cyclic_classes css =
   496   error (cat_lines (map (fn cs =>
   497     "Cycle in class relation: " ^ space_implode " < " (map quote cs)) css));
   498 
   499 fun add_class (c, cs) tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
   500   let
   501     val cs' = map (cert_class tsig) cs
   502       handle TYPE (msg, _, _) => error msg;
   503     val classes' = classes |> Graph.new_node (c, stamp ())
   504       handle Graph.DUP d => err_dup_classes [d];
   505     val classes'' = classes' |> fold Graph.add_edge_trans_acyclic (map (pair c) cs')
   506       handle Graph.CYCLES css => err_cyclic_classes css;
   507   in (classes'', default, types, arities) end);
   508 
   509 in
   510 
   511 val add_classes = fold add_class;
   512 
   513 fun add_classrel ps tsig = tsig |> change_tsig (fn (classes, default, types, arities) =>
   514   let
   515     val ps' = map (pairself (cert_class tsig)) ps
   516       handle TYPE (msg, _, _) => error msg;
   517     val classes' = classes |> fold Graph.add_edge_trans_acyclic ps'
   518       handle Graph.CYCLES css => err_cyclic_classes css;
   519     val default' = default |> Sorts.norm_sort classes';
   520     val arities' = arities |> rebuild_arities classes';
   521   in (classes', default', types, arities') end);
   522 
   523 fun merge_classes CC = Graph.merge_trans_acyclic (op =) CC
   524   handle Graph.DUPS cs => err_dup_classes cs
   525     | Graph.CYCLES css => err_cyclic_classes css;
   526 
   527 end;
   528 
   529 
   530 (* default sort *)
   531 
   532 fun set_defsort S tsig = tsig |> change_tsig (fn (classes, _, types, arities) =>
   533   (classes, cert_sort tsig S handle TYPE (msg, _, _) => error msg, types, arities));
   534 
   535 
   536 (* types *)
   537 
   538 local
   539 
   540 fun err_neg_args c =
   541   error ("Negative number of arguments in type constructor declaration: " ^ quote c);
   542 
   543 fun err_in_decls c decl decl' =
   544   let
   545     val s = str_of_decl decl;
   546     val s' = str_of_decl decl';
   547   in
   548     if s = s' then error ("Duplicate declaration of " ^ s ^ ": " ^ quote c)
   549     else error ("Conflicting declarations of " ^ s ^ " with " ^ s' ^ ": " ^ quote c)
   550   end;
   551 
   552 fun new_decl (c, decl) types =
   553   (case Symtab.lookup (types, c) of
   554     Some (decl', _) => err_in_decls c decl decl'
   555   | None => Symtab.update ((c, (decl, stamp ())), types));
   556 
   557 fun the_decl types c = fst (the (Symtab.lookup (types, c)));
   558 
   559 fun change_types f = change_tsig (fn (classes, default, types, arities) =>
   560   (classes, default, f types, arities));
   561 
   562 fun add_abbr (a, vs, rhs) tsig = tsig |> change_types (fn types =>
   563   let
   564     fun err msg =
   565       error (msg ^ "\nThe error(s) above occurred in type abbreviation " ^ quote a);
   566     val rhs' = strip_sorts (varifyT (no_tvars (cert_typ_syntax tsig rhs)))
   567       handle TYPE (msg, _, _) => err msg;
   568   in
   569     (case duplicates vs of
   570       [] => []
   571     | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups));
   572     (case gen_rems (op =) (map (#1 o #1) (typ_tvars rhs'), vs) of
   573       [] => []
   574     | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
   575     types |> new_decl (a, Abbreviation (vs, rhs'))
   576   end);
   577 
   578 in
   579 
   580 fun add_types ps = change_types (fold new_decl (ps |> map (fn (c, n) =>
   581   if n < 0 then err_neg_args c else (c, LogicalType n))));
   582 
   583 val add_abbrs = fold add_abbr;
   584 val add_nonterminals = change_types o fold new_decl o map (rpair Nonterminal);
   585 
   586 fun merge_types (types1, types2) =
   587   Symtab.merge Library.eq_snd (types1, types2) handle Symtab.DUPS (d :: _) =>
   588     err_in_decls d (the_decl types1 d) (the_decl types2 d);
   589 
   590 end;
   591 
   592 
   593 (* merge type signatures *)
   594 
   595 fun merge_tsigs (tsig1, tsig2) =
   596   let
   597     val (TSig {classes = classes1, default = default1, types = types1, arities = arities1,
   598       log_types = _, witness = _}) = tsig1;
   599     val (TSig {classes = classes2, default = default2, types = types2, arities = arities2,
   600       log_types = _, witness = _}) = tsig2;
   601 
   602     val classes' = merge_classes (classes1, classes2);
   603     val default' = Sorts.inter_sort classes' (default1, default2);
   604     val types' = merge_types (types1, types2);
   605     val arities' = merge_arities classes' (arities1, arities2);
   606   in build_tsig (classes', default', types', arities') end;
   607 
   608 end;