src/Pure/type.ML
author wenzelm
Fri May 28 20:41:23 2010 +0200 (2010-05-28)
changeset 37174 6feaab4fc27d
parent 36621 2fd4e2c76636
child 39288 f1ae2493d93f
permissions -rw-r--r--
assume given SCALA_HOME, e.g. from component settings or external setup;
     1 (*  Title:      Pure/type.ML
     2     Author:     Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel
     3 
     4 Type signatures and certified types, special treatment of type vars,
     5 matching and unification of types, extend and merge type signatures.
     6 *)
     7 
     8 signature TYPE =
     9 sig
    10   (*type signatures and certified types*)
    11   datatype decl =
    12     LogicalType of int |
    13     Abbreviation of string list * typ * bool |
    14     Nonterminal
    15   type tsig
    16   val eq_tsig: tsig * tsig -> bool
    17   val rep_tsig: tsig ->
    18    {classes: Name_Space.T * Sorts.algebra,
    19     default: sort,
    20     types: decl Name_Space.table,
    21     log_types: string list}
    22   val empty_tsig: tsig
    23   val class_space: tsig -> Name_Space.T
    24   val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
    25   val intern_class: tsig -> xstring -> string
    26   val extern_class: tsig -> string -> xstring
    27   val defaultS: tsig -> sort
    28   val logical_types: tsig -> string list
    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 inter_sort: tsig -> sort * sort -> sort
    33   val cert_class: tsig -> class -> class
    34   val cert_sort: tsig -> sort -> sort
    35   val minimize_sort: tsig -> sort -> sort
    36   val witness_sorts: tsig -> (typ * sort) list -> sort list -> (typ * sort) list
    37   type mode
    38   val mode_default: mode
    39   val mode_syntax: mode
    40   val mode_abbrev: mode
    41   val get_mode: Proof.context -> mode
    42   val set_mode: mode -> Proof.context -> Proof.context
    43   val restore_mode: Proof.context -> Proof.context -> Proof.context
    44   val type_space: tsig -> Name_Space.T
    45   val type_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
    46   val intern_type: tsig -> xstring -> string
    47   val extern_type: tsig -> string -> xstring
    48   val is_logtype: tsig -> string -> bool
    49   val the_decl: tsig -> string -> decl
    50   val cert_typ_mode: mode -> tsig -> typ -> typ
    51   val cert_typ: tsig -> typ -> typ
    52   val arity_number: tsig -> string -> int
    53   val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
    54 
    55   (*special treatment of type vars*)
    56   val sort_of_atyp: typ -> sort
    57   val strip_sorts: typ -> typ
    58   val no_tvars: typ -> typ
    59   val varify_global: (string * sort) list -> term -> ((string * sort) * indexname) list * term
    60   val legacy_freeze_thaw_type: typ -> typ * (typ -> typ)
    61   val legacy_freeze_type: typ -> typ
    62   val legacy_freeze_thaw: term -> term * (term -> term)
    63   val legacy_freeze: term -> term
    64 
    65   (*matching and unification*)
    66   exception TYPE_MATCH
    67   type tyenv = (sort * typ) Vartab.table
    68   val lookup: tyenv -> indexname * sort -> typ option
    69   val devar: tyenv -> typ -> typ
    70   val typ_match: tsig -> typ * typ -> tyenv -> tyenv
    71   val typ_instance: tsig -> typ * typ -> bool
    72   val raw_match: typ * typ -> tyenv -> tyenv
    73   val raw_matches: typ list * typ list -> tyenv -> tyenv
    74   val raw_instance: typ * typ -> bool
    75   exception TUNIFY
    76   val unify: tsig -> typ * typ -> tyenv * int -> tyenv * int
    77   val raw_unify: typ * typ -> tyenv -> tyenv
    78   val raw_unifys: typ list * typ list -> tyenv -> tyenv
    79   val could_unify: typ * typ -> bool
    80   val could_unifys: typ list * typ list -> bool
    81   val eq_type: tyenv -> typ * typ -> bool
    82 
    83   (*extend and merge type signatures*)
    84   val add_class: Pretty.pp -> Name_Space.naming -> binding * class list -> tsig -> tsig
    85   val hide_class: bool -> string -> tsig -> tsig
    86   val set_defsort: sort -> tsig -> tsig
    87   val add_type: Name_Space.naming -> binding * int -> tsig -> tsig
    88   val add_abbrev: Name_Space.naming -> binding * string list * typ -> tsig -> tsig
    89   val add_nonterminal: Name_Space.naming -> binding -> tsig -> tsig
    90   val hide_type: bool -> string -> tsig -> tsig
    91   val add_arity: Pretty.pp -> arity -> tsig -> tsig
    92   val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
    93   val merge_tsig: Pretty.pp -> tsig * tsig -> tsig
    94 end;
    95 
    96 structure Type: TYPE =
    97 struct
    98 
    99 (** type signatures and certified types **)
   100 
   101 (* type declarations *)
   102 
   103 datatype decl =
   104   LogicalType of int |
   105   Abbreviation of string list * typ * bool |
   106   Nonterminal;
   107 
   108 
   109 (* type tsig *)
   110 
   111 datatype tsig =
   112   TSig of {
   113     classes: Name_Space.T * Sorts.algebra,  (*order-sorted algebra of type classes*)
   114     default: sort,                          (*default sort on input*)
   115     types: decl Name_Space.table,           (*declared types*)
   116     log_types: string list};                (*logical types sorted by number of arguments*)
   117 
   118 fun eq_tsig
   119    (TSig {classes = classes1, default = default1, types = types1, log_types = _},
   120     TSig {classes = classes2, default = default2, types = types2, log_types = _}) =
   121   pointer_eq (classes1, classes2) andalso
   122   default1 = default2 andalso
   123   pointer_eq (types1, types2);
   124 
   125 fun rep_tsig (TSig comps) = comps;
   126 
   127 fun make_tsig (classes, default, types, log_types) =
   128   TSig {classes = classes, default = default, types = types, log_types = log_types};
   129 
   130 fun build_tsig (classes, default, types) =
   131   let
   132     val log_types =
   133       Symtab.fold (fn (c, LogicalType n) => cons (c, n) | _ => I) (snd types) []
   134       |> Library.sort (int_ord o pairself snd) |> map fst;
   135   in make_tsig (classes, default, types, log_types) end;
   136 
   137 fun map_tsig f (TSig {classes, default, types, log_types = _}) =
   138   build_tsig (f (classes, default, types));
   139 
   140 val empty_tsig =
   141   build_tsig ((Name_Space.empty "class", Sorts.empty_algebra), [], Name_Space.empty_table "type");
   142 
   143 
   144 (* classes and sorts *)
   145 
   146 val class_space = #1 o #classes o rep_tsig;
   147 
   148 fun class_alias naming binding name = map_tsig (fn ((space, classes), default, types) =>
   149   ((Name_Space.alias naming binding name space, classes), default, types));
   150 
   151 val intern_class = Name_Space.intern o class_space;
   152 val extern_class = Name_Space.extern o class_space;
   153 
   154 fun defaultS (TSig {default, ...}) = default;
   155 fun logical_types (TSig {log_types, ...}) = log_types;
   156 
   157 fun eq_sort (TSig {classes, ...}) = Sorts.sort_eq (#2 classes);
   158 fun subsort (TSig {classes, ...}) = Sorts.sort_le (#2 classes);
   159 fun of_sort (TSig {classes, ...}) = Sorts.of_sort (#2 classes);
   160 fun inter_sort (TSig {classes, ...}) = Sorts.inter_sort (#2 classes);
   161 
   162 fun cert_class (TSig {classes, ...}) = Sorts.certify_class (#2 classes);
   163 fun cert_sort (TSig {classes, ...}) = Sorts.certify_sort (#2 classes);
   164 fun minimize_sort (TSig {classes, ...}) = Sorts.minimize_sort (#2 classes);
   165 
   166 fun witness_sorts (TSig {classes, log_types, ...}) =
   167   Sorts.witness_sorts (#2 classes) log_types;
   168 
   169 
   170 (* certification mode *)
   171 
   172 datatype mode = Mode of {normalize: bool, logical: bool};
   173 
   174 val mode_default = Mode {normalize = true, logical = true};
   175 val mode_syntax = Mode {normalize = true, logical = false};
   176 val mode_abbrev = Mode {normalize = false, logical = false};
   177 
   178 structure Mode = Proof_Data
   179 (
   180   type T = mode;
   181   fun init _ = mode_default;
   182 );
   183 
   184 val get_mode = Mode.get;
   185 fun set_mode mode = Mode.map (K mode);
   186 fun restore_mode ctxt = set_mode (get_mode ctxt);
   187 
   188 
   189 (* types *)
   190 
   191 val type_space = #1 o #types o rep_tsig;
   192 
   193 fun type_alias naming binding name = map_tsig (fn (classes, default, (space, types)) =>
   194   (classes, default, (Name_Space.alias naming binding name space, types)));
   195 
   196 val intern_type = Name_Space.intern o type_space;
   197 val extern_type = Name_Space.extern o type_space;
   198 
   199 val is_logtype = member (op =) o logical_types;
   200 
   201 
   202 fun undecl_type c = "Undeclared type constructor: " ^ quote c;
   203 
   204 fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
   205 
   206 fun the_decl tsig c =
   207   (case lookup_type tsig c of
   208     NONE => error (undecl_type c)
   209   | SOME decl => decl);
   210 
   211 
   212 (* certified types *)
   213 
   214 fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t;
   215 
   216 local
   217 
   218 fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts)
   219   | inst_typ env (T as TFree (x, _)) = the_default T (AList.lookup (op =) env x)
   220   | inst_typ _ T = T;
   221 
   222 in
   223 
   224 fun cert_typ_mode (Mode {normalize, logical}) tsig ty =
   225   let
   226     fun err msg = raise TYPE (msg, [ty], []);
   227 
   228     val check_logical =
   229       if logical then fn c => err ("Illegal occurrence of syntactic type: " ^ quote c)
   230       else fn _ => ();
   231 
   232     fun cert (T as Type (c, Ts)) =
   233           let
   234             val Ts' = map cert Ts;
   235             fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
   236           in
   237             (case the_decl tsig c of
   238               LogicalType n => (nargs n; Type (c, Ts'))
   239             | Abbreviation (vs, U, syn) =>
   240                (nargs (length vs);
   241                 if syn then check_logical c else ();
   242                 if normalize then inst_typ (vs ~~ Ts') U
   243                 else Type (c, Ts'))
   244             | Nonterminal => (nargs 0; check_logical c; T))
   245           end
   246       | cert (TFree (x, S)) = TFree (x, cert_sort tsig S)
   247       | cert (TVar (xi as (_, i), S)) =
   248           if i < 0 then
   249             err ("Malformed type variable: " ^ quote (Term.string_of_vname xi))
   250           else TVar (xi, cert_sort tsig S);
   251 
   252     val ty' = cert ty;
   253   in if ty = ty' then ty else ty' end;  (*avoid copying of already normal type*)
   254 
   255 val cert_typ = cert_typ_mode mode_default;
   256 
   257 end;
   258 
   259 
   260 (* type arities *)
   261 
   262 fun arity_number tsig a =
   263   (case lookup_type tsig a of
   264     SOME (LogicalType n) => n
   265   | _ => error (undecl_type a));
   266 
   267 fun arity_sorts _ tsig a [] = replicate (arity_number tsig a) []
   268   | arity_sorts pp (TSig {classes, ...}) a S = Sorts.mg_domain (#2 classes) a S
   269       handle Sorts.CLASS_ERROR err => error (Sorts.class_error pp err);
   270 
   271 
   272 
   273 (** special treatment of type vars **)
   274 
   275 (* sort_of_atyp *)
   276 
   277 fun sort_of_atyp (TFree (_, S)) = S
   278   | sort_of_atyp (TVar (_, S)) = S
   279   | sort_of_atyp T = raise TYPE ("sort_of_atyp", [T], []);
   280 
   281 
   282 (* strip_sorts *)
   283 
   284 fun strip_sorts (Type (a, Ts)) = Type (a, map strip_sorts Ts)
   285   | strip_sorts (TFree (x, _)) = TFree (x, [])
   286   | strip_sorts (TVar (xi, _)) = TVar (xi, []);
   287 
   288 
   289 (* no_tvars *)
   290 
   291 fun no_tvars T =
   292   (case Term.add_tvarsT T [] of [] => T
   293   | vs => raise TYPE ("Illegal schematic type variable(s): " ^
   294       commas_quote (map (Term.string_of_vname o #1) (rev vs)), [T], []));
   295 
   296 
   297 (* varify_global *)
   298 
   299 fun varify_global fixed t =
   300   let
   301     val fs = Term.fold_types (Term.fold_atyps
   302       (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
   303     val used = Name.context
   304       |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
   305     val fmap = fs ~~ map (rpair 0) (#1 (Name.variants (map fst fs) used));
   306     fun thaw (f as (_, S)) =
   307       (case AList.lookup (op =) fmap f of
   308         NONE => TFree f
   309       | SOME xi => TVar (xi, S));
   310   in (fmap, map_types (map_type_tfree thaw) t) end;
   311 
   312 
   313 (* freeze_thaw: freeze TVars in a term; return the "thaw" inverse *)
   314 
   315 local
   316 
   317 fun new_name (ix, (pairs, used)) =
   318   let val v = Name.variant used (string_of_indexname ix)
   319   in ((ix, v) :: pairs, v :: used) end;
   320 
   321 fun freeze_one alist (ix, sort) =
   322   TFree (the (AList.lookup (op =) alist ix), sort)
   323     handle Option =>
   324       raise TYPE ("Failure during freezing of ?" ^ string_of_indexname ix, [], []);
   325 
   326 fun thaw_one alist (a, sort) = TVar (the (AList.lookup (op =) alist a), sort)
   327   handle Option => TFree (a, sort);
   328 
   329 in
   330 
   331 fun legacy_freeze_thaw_type T =
   332   let
   333     val used = OldTerm.add_typ_tfree_names (T, [])
   334     and tvars = map #1 (OldTerm.add_typ_tvars (T, []));
   335     val (alist, _) = List.foldr new_name ([], used) tvars;
   336   in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
   337 
   338 val legacy_freeze_type = #1 o legacy_freeze_thaw_type;
   339 
   340 fun legacy_freeze_thaw t =
   341   let
   342     val used = OldTerm.it_term_types OldTerm.add_typ_tfree_names (t, [])
   343     and tvars = map #1 (OldTerm.it_term_types OldTerm.add_typ_tvars (t, []));
   344     val (alist, _) = List.foldr new_name ([], used) tvars;
   345   in
   346     (case alist of
   347       [] => (t, fn x => x) (*nothing to do!*)
   348     | _ => (map_types (map_type_tvar (freeze_one alist)) t,
   349       map_types (map_type_tfree (thaw_one (map swap alist)))))
   350   end;
   351 
   352 val legacy_freeze = #1 o legacy_freeze_thaw;
   353 
   354 end;
   355 
   356 
   357 
   358 (** matching and unification of types **)
   359 
   360 type tyenv = (sort * typ) Vartab.table;
   361 
   362 fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^
   363   quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
   364   [TVar (ixn, S), TVar (ixn, S')], []);
   365 
   366 fun lookup tye (ixn, S) =
   367   (case Vartab.lookup tye ixn of
   368     NONE => NONE
   369   | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S');
   370 
   371 
   372 (* matching *)
   373 
   374 exception TYPE_MATCH;
   375 
   376 fun typ_match tsig =
   377   let
   378     fun match (TVar (v, S), T) subs =
   379           (case lookup subs (v, S) of
   380             NONE =>
   381               if of_sort tsig (T, S) then Vartab.update_new (v, (S, T)) subs
   382               else raise TYPE_MATCH
   383           | SOME U => if U = T then subs else raise TYPE_MATCH)
   384       | match (Type (a, Ts), Type (b, Us)) subs =
   385           if a <> b then raise TYPE_MATCH
   386           else matches (Ts, Us) subs
   387       | match (TFree x, TFree y) subs =
   388           if x = y then subs else raise TYPE_MATCH
   389       | match _ _ = raise TYPE_MATCH
   390     and matches (T :: Ts, U :: Us) subs = matches (Ts, Us) (match (T, U) subs)
   391       | matches _ subs = subs;
   392   in match end;
   393 
   394 fun typ_instance tsig (T, U) =
   395   (typ_match tsig (U, T) Vartab.empty; true) handle TYPE_MATCH => false;
   396 
   397 (*purely structural matching*)
   398 fun raw_match (TVar (v, S), T) subs =
   399       (case lookup subs (v, S) of
   400         NONE => Vartab.update_new (v, (S, T)) subs
   401       | SOME U => if U = T then subs else raise TYPE_MATCH)
   402   | raw_match (Type (a, Ts), Type (b, Us)) subs =
   403       if a <> b then raise TYPE_MATCH
   404       else raw_matches (Ts, Us) subs
   405   | raw_match (TFree x, TFree y) subs =
   406       if x = y then subs else raise TYPE_MATCH
   407   | raw_match _ _ = raise TYPE_MATCH
   408 and raw_matches (T :: Ts, U :: Us) subs = raw_matches (Ts, Us) (raw_match (T, U) subs)
   409   | raw_matches ([], []) subs = subs
   410   | raw_matches _ _ = raise TYPE_MATCH;
   411 
   412 fun raw_instance (T, U) =
   413   (raw_match (U, T) Vartab.empty; true) handle TYPE_MATCH => false;
   414 
   415 
   416 (* unification *)
   417 
   418 exception TUNIFY;
   419 
   420 (*occurs check*)
   421 fun occurs v tye =
   422   let
   423     fun occ (Type (_, Ts)) = exists occ Ts
   424       | occ (TFree _) = false
   425       | occ (TVar (w, S)) =
   426           Term.eq_ix (v, w) orelse
   427             (case lookup tye (w, S) of
   428               NONE => false
   429             | SOME U => occ U);
   430   in occ end;
   431 
   432 (*chase variable assignments; if devar returns a type var then it must be unassigned*)
   433 fun devar tye (T as TVar v) =
   434       (case lookup tye v of
   435         SOME U => devar tye U
   436       | NONE => T)
   437   | devar _ T = T;
   438 
   439 (*order-sorted unification*)
   440 fun unify (TSig {classes = (_, classes), ...}) TU (tyenv, maxidx) =
   441   let
   442     val tyvar_count = Unsynchronized.ref maxidx;
   443     fun gen_tyvar S = TVar ((Name.aT, Unsynchronized.inc tyvar_count), S);
   444 
   445     fun mg_domain a S = Sorts.mg_domain classes a S
   446       handle Sorts.CLASS_ERROR _ => raise TUNIFY;
   447 
   448     fun meet (_, []) tye = tye
   449       | meet (TVar (xi, S'), S) tye =
   450           if Sorts.sort_le classes (S', S) then tye
   451           else Vartab.update_new
   452             (xi, (S', gen_tyvar (Sorts.inter_sort classes (S', S)))) tye
   453       | meet (TFree (_, S'), S) tye =
   454           if Sorts.sort_le classes (S', S) then tye
   455           else raise TUNIFY
   456       | meet (Type (a, Ts), S) tye = meets (Ts, mg_domain a S) tye
   457     and meets (T :: Ts, S :: Ss) tye = meets (Ts, Ss) (meet (devar tye T, S) tye)
   458       | meets _ tye = tye;
   459 
   460     fun unif (ty1, ty2) tye =
   461       (case (devar tye ty1, devar tye ty2) of
   462         (T as TVar (v, S1), U as TVar (w, S2)) =>
   463           if Term.eq_ix (v, w) then
   464             if S1 = S2 then tye else tvar_clash v S1 S2
   465           else if Sorts.sort_le classes (S1, S2) then
   466             Vartab.update_new (w, (S2, T)) tye
   467           else if Sorts.sort_le classes (S2, S1) then
   468             Vartab.update_new (v, (S1, U)) tye
   469           else
   470             let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in
   471               Vartab.update_new (v, (S1, S)) (Vartab.update_new (w, (S2, S)) tye)
   472             end
   473       | (TVar (v, S), T) =>
   474           if occurs v tye T then raise TUNIFY
   475           else meet (T, S) (Vartab.update_new (v, (S, T)) tye)
   476       | (T, TVar (v, S)) =>
   477           if occurs v tye T then raise TUNIFY
   478           else meet (T, S) (Vartab.update_new (v, (S, T)) tye)
   479       | (Type (a, Ts), Type (b, Us)) =>
   480           if a <> b then raise TUNIFY
   481           else unifs (Ts, Us) tye
   482       | (T, U) => if T = U then tye else raise TUNIFY)
   483     and unifs (T :: Ts, U :: Us) tye = unifs (Ts, Us) (unif (T, U) tye)
   484       | unifs _ tye = tye;
   485   in (unif TU tyenv, ! tyvar_count) end;
   486 
   487 (*purely structural unification*)
   488 fun raw_unify (ty1, ty2) tye =
   489   (case (devar tye ty1, devar tye ty2) of
   490     (T as TVar (v, S1), TVar (w, S2)) =>
   491       if Term.eq_ix (v, w) then
   492         if S1 = S2 then tye else tvar_clash v S1 S2
   493       else Vartab.update_new (w, (S2, T)) tye
   494   | (TVar (v, S), T) =>
   495       if occurs v tye T then raise TUNIFY
   496       else Vartab.update_new (v, (S, T)) tye
   497   | (T, TVar (v, S)) =>
   498       if occurs v tye T then raise TUNIFY
   499       else Vartab.update_new (v, (S, T)) tye
   500   | (Type (a, Ts), Type (b, Us)) =>
   501       if a <> b then raise TUNIFY
   502       else raw_unifys (Ts, Us) tye
   503   | (T, U) => if T = U then tye else raise TUNIFY)
   504 and raw_unifys (T :: Ts, U :: Us) tye = raw_unifys (Ts, Us) (raw_unify (T, U) tye)
   505   | raw_unifys ([], []) tye = tye
   506   | raw_unifys _ _ = raise TUNIFY;
   507 
   508 (*fast unification filter*)
   509 fun could_unify (Type (a, Ts), Type (b, Us)) = a = b andalso could_unifys (Ts, Us)
   510   | could_unify (TFree (a, _), TFree (b, _)) = a = b
   511   | could_unify (TVar _, _) = true
   512   | could_unify (_, TVar _) = true
   513   | could_unify _ = false
   514 and could_unifys (T :: Ts, U :: Us) = could_unify (T, U) andalso could_unifys (Ts, Us)
   515   | could_unifys ([], []) = true
   516   | could_unifys _ = false;
   517 
   518 
   519 (*equality with respect to a type environment*)
   520 fun equal_type tye (T, T') =
   521   (case (devar tye T, devar tye T') of
   522      (Type (s, Ts), Type (s', Ts')) =>
   523        s = s' andalso ListPair.all (equal_type tye) (Ts, Ts')
   524    | (U, U') => U = U');
   525 
   526 fun eq_type tye =
   527   if Vartab.is_empty tye then op = else equal_type tye;
   528 
   529 
   530 
   531 (** extend and merge type signatures **)
   532 
   533 (* classes *)
   534 
   535 fun add_class pp naming (c, cs) tsig =
   536   tsig |> map_tsig (fn ((space, classes), default, types) =>
   537     let
   538       val cs' = map (cert_class tsig) cs
   539         handle TYPE (msg, _, _) => error msg;
   540       val (c', space') = space |> Name_Space.declare true naming c;
   541       val classes' = classes |> Sorts.add_class pp (c', cs');
   542     in ((space', classes'), default, types) end);
   543 
   544 fun hide_class fully c = map_tsig (fn ((space, classes), default, types) =>
   545   ((Name_Space.hide fully c space, classes), default, types));
   546 
   547 
   548 (* arities *)
   549 
   550 fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
   551   let
   552     val _ =
   553       (case lookup_type tsig t of
   554         SOME (LogicalType n) => if length Ss <> n then error (bad_nargs t) else ()
   555       | SOME _ => error ("Logical type constructor expected: " ^ quote t)
   556       | NONE => error (undecl_type t));
   557     val (Ss', S') = (map (cert_sort tsig) Ss, cert_sort tsig S)
   558       handle TYPE (msg, _, _) => error msg;
   559     val classes' = classes |> Sorts.add_arities pp ((t, map (fn c' => (c', Ss')) S'));
   560   in ((space, classes'), default, types) end);
   561 
   562 
   563 (* classrel *)
   564 
   565 fun add_classrel pp rel tsig =
   566   tsig |> map_tsig (fn ((space, classes), default, types) =>
   567     let
   568       val rel' = pairself (cert_class tsig) rel
   569         handle TYPE (msg, _, _) => error msg;
   570       val classes' = classes |> Sorts.add_classrel pp rel';
   571     in ((space, classes'), default, types) end);
   572 
   573 
   574 (* default sort *)
   575 
   576 fun set_defsort S tsig = tsig |> map_tsig (fn (classes, _, types) =>
   577   (classes, cert_sort tsig S handle TYPE (msg, _, _) => error msg, types));
   578 
   579 
   580 (* types *)
   581 
   582 local
   583 
   584 fun new_decl naming (c, decl) types =
   585   #2 (Name_Space.define true naming (c, decl) types);
   586 
   587 fun map_types f = map_tsig (fn (classes, default, types) =>
   588   let
   589     val (space', tab') = f types;
   590     val _ = Name_Space.intern space' "dummy" = "dummy" orelse
   591       error "Illegal declaration of dummy type";
   592   in (classes, default, (space', tab')) end);
   593 
   594 fun syntactic types (Type (c, Ts)) =
   595       (case Symtab.lookup types c of SOME Nonterminal => true | _ => false)
   596         orelse exists (syntactic types) Ts
   597   | syntactic _ _ = false;
   598 
   599 in
   600 
   601 fun add_type naming (c, n) =
   602   if n < 0 then error ("Bad type constructor declaration " ^ quote (Binding.str_of c))
   603   else map_types (new_decl naming (c, LogicalType n));
   604 
   605 fun add_abbrev naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
   606   let
   607     fun err msg =
   608       cat_error msg ("The error(s) above occurred in type abbreviation " ^
   609         quote (Binding.str_of a));
   610     val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs))
   611       handle TYPE (msg, _, _) => err msg;
   612     val _ =
   613       (case duplicates (op =) vs of
   614         [] => []
   615       | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups));
   616     val _ =
   617       (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
   618         [] => []
   619       | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
   620   in types |> new_decl naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
   621 
   622 fun add_nonterminal naming = map_types o new_decl naming o rpair Nonterminal;
   623 
   624 end;
   625 
   626 fun hide_type fully c = map_tsig (fn (classes, default, (space, types)) =>
   627   (classes, default, (Name_Space.hide fully c space, types)));
   628 
   629 
   630 (* merge type signatures *)
   631 
   632 fun merge_tsig pp (tsig1, tsig2) =
   633   let
   634     val (TSig {classes = (space1, classes1), default = default1, types = types1,
   635       log_types = _}) = tsig1;
   636     val (TSig {classes = (space2, classes2), default = default2, types = types2,
   637       log_types = _}) = tsig2;
   638 
   639     val space' = Name_Space.merge (space1, space2);
   640     val classes' = Sorts.merge_algebra pp (classes1, classes2);
   641     val default' = Sorts.inter_sort classes' (default1, default2);
   642     val types' = Name_Space.merge_tables (types1, types2);
   643   in build_tsig ((space', classes'), default', types') end;
   644 
   645 end;