Major cleanup:
authorwenzelm
Thu Jun 09 12:03:24 2005 +0200 (2005-06-09)
changeset 163375734de2f7ace
parent 16336 e3892698c57d
child 16338 3d1851acb4d0
Major cleanup:
got rid of types bclass, xclass, xsort, xtyp, xterm;
reorganized code to separate stamps/data/sign;
clarified name space inter/extern operations;
sane read/certify operations -- more picky about stale signatures;
sane implementation of signature extensions;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Thu Jun 09 12:03:23 2005 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Jun 09 12:03:24 2005 +0200
     1.3 @@ -5,14 +5,6 @@
     1.4  The abstract type "sg" of signatures.
     1.5  *)
     1.6  
     1.7 -(*base names*)
     1.8 -type bclass = class;
     1.9 -(*external forms*)
    1.10 -type xclass = class;
    1.11 -type xsort = sort;
    1.12 -type xtyp = typ;
    1.13 -type xterm = term;
    1.14 -
    1.15  signature SIGN =
    1.16  sig
    1.17    type sg
    1.18 @@ -23,27 +15,38 @@
    1.19      tsig: Type.tsig,
    1.20      consts: (typ * stamp) Symtab.table,
    1.21      naming: NameSpace.naming,
    1.22 -    spaces: (string * NameSpace.T) list,
    1.23 +    spaces: {class: NameSpace.T, tycon: NameSpace.T, const: NameSpace.T},
    1.24      data: data}
    1.25 -  val name_of: sg -> string
    1.26    val stamp_names_of: sg -> string list
    1.27    val exists_stamp: string -> sg -> bool
    1.28 -  val tsig_of: sg -> Type.tsig
    1.29 -  val is_logtype: sg -> string -> bool
    1.30 -  val deref: sg_ref -> sg
    1.31 +  val pretty_sg: sg -> Pretty.T
    1.32 +  val pprint_sg: sg -> pprint_args -> unit
    1.33 +  val pretty_abbrev_sg: sg -> Pretty.T
    1.34 +  val str_of_sg: sg -> string
    1.35 +  val is_stale: sg -> bool
    1.36    val self_ref: sg -> sg_ref
    1.37 +  val deref: sg_ref -> sg
    1.38 +  val name_of: sg -> string
    1.39 +  val is_draft: sg -> bool
    1.40 +  val eq_sg: sg * sg -> bool
    1.41    val subsig: sg * sg -> bool
    1.42 -  val joinable: sg * sg -> bool
    1.43 -  val eq_sg: sg * sg -> bool
    1.44    val same_sg: sg * sg -> bool
    1.45 -  val is_draft: sg -> bool
    1.46 -  val is_stale: sg -> bool
    1.47 -  val syn_of: sg -> Syntax.syntax
    1.48 +  val joinable: sg * sg -> bool
    1.49 +  val prep_ext: sg -> sg
    1.50 +  val copy: sg -> sg
    1.51 +  val add_name: string -> sg -> sg
    1.52 +  val data_kinds: data -> string list
    1.53 +  val print_all_data: sg -> unit
    1.54 +  val pre_pure: sg
    1.55 +  val PureN: string
    1.56 +  val CPureN: string
    1.57    val naming_of: sg -> NameSpace.naming
    1.58 -  val const_type: sg -> string -> typ option
    1.59 -  val the_const_type: sg -> string -> typ          (*exception TYPE*)
    1.60 -  val declared_tyname: sg -> string -> bool
    1.61 -  val declared_const: sg -> string -> bool
    1.62 +  val base_name: string -> bstring
    1.63 +  val full_name: sg -> bstring -> string
    1.64 +  val full_name_path: sg -> string -> bstring -> string
    1.65 +  val declare_name: sg -> string -> NameSpace.T -> NameSpace.T
    1.66 +  val syn_of: sg -> Syntax.syntax
    1.67 +  val tsig_of: sg -> Type.tsig
    1.68    val classes: sg -> class list
    1.69    val defaultS: sg -> sort
    1.70    val subsort: sg -> sort * sort -> bool
    1.71 @@ -51,32 +54,32 @@
    1.72    val witness_sorts: sg -> sort list -> sort list -> (typ * sort) list
    1.73    val universal_witness: sg -> (typ * sort) option
    1.74    val typ_instance: sg -> typ * typ -> bool
    1.75 +  val is_logtype: sg -> string -> bool
    1.76 +  val const_type: sg -> string -> typ option
    1.77 +  val the_const_type: sg -> string -> typ
    1.78 +  val declared_tyname: sg -> string -> bool
    1.79 +  val declared_const: sg -> string -> bool
    1.80    val classK: string
    1.81    val typeK: string
    1.82    val constK: string
    1.83 -  val base_name: string -> bstring
    1.84 -  val full_name: sg -> bstring -> string
    1.85 -  val full_name_path: sg -> string -> bstring -> string
    1.86 -  val declare_name: sg -> string -> NameSpace.T -> NameSpace.T
    1.87    val intern: sg -> string -> xstring -> string
    1.88    val extern: sg -> string -> string -> xstring
    1.89    val extern_table: sg -> string -> 'a Symtab.table -> (xstring * 'a) list
    1.90 -  val extern_typ: sg -> typ -> typ
    1.91 -  val intern_class: sg -> xclass -> class
    1.92 +  val intern_class: sg -> xstring -> string
    1.93 +  val extern_class: sg -> string -> xstring
    1.94    val intern_tycon: sg -> xstring -> string
    1.95 +  val extern_tycon: sg -> string -> xstring
    1.96    val intern_const: sg -> xstring -> string
    1.97 -  val intern_sort: sg -> xsort -> sort
    1.98 -  val intern_typ: sg -> xtyp -> typ
    1.99 -  val intern_term: sg -> xterm -> term
   1.100 -  val intern_tycons: sg -> xtyp -> typ
   1.101 -  val pretty_sg: sg -> Pretty.T
   1.102 -  val str_of_sg: sg -> string
   1.103 -  val pprint_sg: sg -> pprint_args -> unit
   1.104 -  val PureN: string
   1.105 -  val CPureN: string
   1.106 -  val pre_pure: sg
   1.107 +  val extern_const: sg -> string -> xstring
   1.108 +  val intern_sort: sg -> sort -> sort
   1.109 +  val extern_sort: sg -> sort -> sort
   1.110 +  val intern_typ: sg -> typ -> typ
   1.111 +  val extern_typ: sg -> typ -> typ
   1.112 +  val intern_term: sg -> term -> term
   1.113 +  val extern_term: sg -> term -> term
   1.114 +  val intern_tycons: sg -> typ -> typ
   1.115 +  val pretty_term': Syntax.syntax -> sg -> term -> Pretty.T
   1.116    val pretty_term: sg -> term -> Pretty.T
   1.117 -  val pretty_term': Syntax.syntax -> sg -> term -> Pretty.T
   1.118    val pretty_typ: sg -> typ -> Pretty.T
   1.119    val pretty_sort: sg -> sort -> Pretty.T
   1.120    val pretty_classrel: sg -> class list -> Pretty.T
   1.121 @@ -92,21 +95,25 @@
   1.122    val certify_class: sg -> class -> class
   1.123    val certify_sort: sg -> sort -> sort
   1.124    val certify_typ: sg -> typ -> typ
   1.125 -  val certify_typ_raw: sg -> typ -> typ
   1.126 +  val certify_typ_syntax: sg -> typ -> typ
   1.127 +  val certify_typ_abbrev: sg -> typ -> typ
   1.128    val certify_term: Pretty.pp -> sg -> term -> term * typ * int
   1.129 +  val read_sort': Syntax.syntax -> sg -> string -> sort
   1.130    val read_sort: sg -> string -> sort
   1.131 -  val read_raw_typ: sg * (indexname -> sort option) -> string -> typ
   1.132 +  val read_typ': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   1.133 +  val read_typ_syntax': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   1.134 +  val read_typ_abbrev': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   1.135    val read_typ: sg * (indexname -> sort option) -> string -> typ
   1.136 -  val read_typ': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   1.137 -  val read_typ_raw': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   1.138 -  val read_tyname: sg -> string -> typ
   1.139 +  val read_typ_syntax: sg * (indexname -> sort option) -> string -> typ
   1.140 +  val read_typ_abbrev: sg * (indexname -> sort option) -> string -> typ
   1.141 +  val read_tyname: sg -> string -> typ        (*exception TYPE*)
   1.142    val read_const: sg -> string -> term        (*exception TYPE*)
   1.143 +  val infer_types_simult: Pretty.pp -> sg -> (indexname -> typ option) ->
   1.144 +    (indexname -> sort option) -> string list -> bool
   1.145 +    -> (term list * typ) list -> term list * (indexname * typ) list
   1.146    val infer_types: Pretty.pp -> sg -> (indexname -> typ option) ->
   1.147      (indexname -> sort option) -> string list -> bool
   1.148 -    -> xterm list * typ -> term * (indexname * typ) list
   1.149 -  val infer_types_simult: Pretty.pp -> sg -> (indexname -> typ option) ->
   1.150 -    (indexname -> sort option) -> string list -> bool
   1.151 -    -> (xterm list * typ) list -> term list * (indexname * typ) list
   1.152 +    -> term list * typ -> term * (indexname * typ) list
   1.153    val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax ->
   1.154      sg * (indexname -> typ option) * (indexname -> sort option) ->
   1.155      string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
   1.156 @@ -114,12 +121,6 @@
   1.157      sg * (indexname -> typ option) * (indexname -> sort option) ->
   1.158      string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
   1.159    val simple_read_term: sg -> typ -> string -> term
   1.160 -  val const_of_class: class -> string
   1.161 -  val class_of_const: string -> class
   1.162 -  val add_classes: (bclass * xclass list) list -> sg -> sg
   1.163 -  val add_classes_i: (bclass * class list) list -> sg -> sg
   1.164 -  val add_classrel: (xclass * xclass) list -> sg -> sg
   1.165 -  val add_classrel_i: (class * class) list -> sg -> sg
   1.166    val add_defsort: string -> sg -> sg
   1.167    val add_defsort_i: sort -> sg -> sg
   1.168    val add_types: (bstring * int * mixfix) list -> sg -> sg
   1.169 @@ -128,14 +129,20 @@
   1.170    val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> sg -> sg
   1.171    val add_arities: (xstring * string list * string) list -> sg -> sg
   1.172    val add_arities_i: (string * sort list * sort) list -> sg -> sg
   1.173 -  val add_consts: (bstring * string * mixfix) list -> sg -> sg
   1.174 -  val add_consts_i: (bstring * typ * mixfix) list -> sg -> sg
   1.175    val add_syntax: (bstring * string * mixfix) list -> sg -> sg
   1.176    val add_syntax_i: (bstring * typ * mixfix) list -> sg -> sg
   1.177    val add_modesyntax: (string * bool) * (bstring * string * mixfix) list -> sg -> sg
   1.178    val add_modesyntax_i: (string * bool) * (bstring * typ * mixfix) list -> sg -> sg
   1.179    val del_modesyntax: (string * bool) * (bstring * string * mixfix) list -> sg -> sg
   1.180    val del_modesyntax_i: (string * bool) * (bstring * typ * mixfix) list -> sg -> sg
   1.181 +  val add_consts: (bstring * string * mixfix) list -> sg -> sg
   1.182 +  val add_consts_i: (bstring * typ * mixfix) list -> sg -> sg
   1.183 +  val const_of_class: class -> string
   1.184 +  val class_of_const: string -> class
   1.185 +  val add_classes: (bstring * xstring list) list -> sg -> sg
   1.186 +  val add_classes_i: (bstring * class list) list -> sg -> sg
   1.187 +  val add_classrel: (xstring * xstring) list -> sg -> sg
   1.188 +  val add_classrel_i: (class * class) list -> sg -> sg
   1.189    val add_trfuns:
   1.190      (string * (ast list -> ast)) list *
   1.191      (string * (term list -> term)) list *
   1.192 @@ -160,16 +167,10 @@
   1.193    val custom_accesses: (string list -> string list list) -> sg -> sg
   1.194    val set_policy: (string -> bstring -> string) * (string list -> string list list) -> sg -> sg
   1.195    val restore_naming: sg -> sg -> sg
   1.196 -  val add_space: string * string list -> sg -> sg
   1.197    val hide_space: bool -> string * string list -> sg -> sg
   1.198    val hide_space_i: bool -> string * string list -> sg -> sg
   1.199 -  val add_name: string -> sg -> sg
   1.200 -  val data_kinds: data -> string list
   1.201 -  val print_all_data: sg -> unit
   1.202    val merge_refs: sg_ref * sg_ref -> sg_ref
   1.203    val merge: sg * sg -> sg
   1.204 -  val copy: sg -> sg
   1.205 -  val prep_ext: sg -> sg
   1.206    val prep_ext_merge: sg list -> sg
   1.207  end;
   1.208  
   1.209 @@ -192,15 +193,15 @@
   1.210  
   1.211  datatype sg =
   1.212    Sg of
   1.213 -   {id: string ref,                               (*id*)
   1.214 +   {id: string ref,
   1.215      stamps: string ref list,                      (*unique theory indentifier*)
   1.216      syn: syn} *                                   (*syntax for parsing and printing*)
   1.217     {self: sg_ref,                                 (*mutable self reference*)
   1.218      tsig: Type.tsig,                              (*order-sorted signature of types*)
   1.219      consts: (typ * stamp) Symtab.table,           (*type schemes of constants*)
   1.220 -    naming: NameSpace.naming,                     (*name space declaration context*)
   1.221 -    spaces: (string * NameSpace.T) list,          (*name spaces for consts, types etc.*)
   1.222 -    data: data}                                   (*anytype data*)
   1.223 +    naming: NameSpace.naming,
   1.224 +    spaces: {class: NameSpace.T, tycon: NameSpace.T, const: NameSpace.T},
   1.225 +    data: data}
   1.226  and data =
   1.227    Data of
   1.228      (Object.kind *                                (*kind (for authorization)*)
   1.229 @@ -220,64 +221,65 @@
   1.230  and sg_ref =
   1.231    SgRef of sg ref option;
   1.232  
   1.233 -(*make signature*)
   1.234 -fun make_sign (id, self, tsig, consts, syn, naming, spaces, data, stamps) =
   1.235 +(* FIXME assign!??? *)
   1.236 +fun make_sg (id, self, stamps) naming data (syn, tsig, consts, spaces) =
   1.237    Sg ({id = id, stamps = stamps, syn = syn}, {self = self, tsig = tsig,
   1.238      consts = consts, naming = naming, spaces = spaces, data = data});
   1.239  
   1.240 +fun rep_sg (Sg (_, args)) = args;
   1.241  
   1.242 -(* basic operations *)
   1.243  
   1.244 -fun rep_sg (Sg (_, args)) = args;
   1.245 +(* stamps *)
   1.246  
   1.247  fun stamps_of (Sg ({stamps, ...}, _)) = stamps;
   1.248  val stamp_names_of = rev o map ! o stamps_of;
   1.249  fun exists_stamp name = exists (equal name o !) o stamps_of;
   1.250  
   1.251  fun pretty_sg sg = Pretty.str_list "{" "}" (stamp_names_of sg);
   1.252 -val str_of_sg = Pretty.str_of o pretty_sg;
   1.253  val pprint_sg = Pretty.pprint o pretty_sg;
   1.254  
   1.255 -fun naming_of (Sg (_, {naming, ...})) = naming;
   1.256 -val tsig_of = #tsig o rep_sg;
   1.257 -fun is_logtype sg c = c mem_string Type.logical_types (tsig_of sg);
   1.258 -
   1.259 -fun const_type (Sg (_, {consts, ...})) c = Option.map #1 (Symtab.lookup (consts, c));
   1.260 +fun pretty_abbrev_sg sg =
   1.261 +  let
   1.262 +    val stamps = map ! (stamps_of sg);
   1.263 +    val abbrev = if length stamps > 5 then "..." :: rev (List.take (stamps, 5)) else rev stamps;
   1.264 +  in Pretty.str_list "{" "}" abbrev end;
   1.265  
   1.266 -fun the_const_type sg c =
   1.267 -  (case const_type sg c of SOME T => T
   1.268 -  | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
   1.269 -
   1.270 -fun declared_tyname sg c = is_some (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c));
   1.271 -fun declared_const sg c = is_some (const_type sg c);
   1.272 +val str_of_sg = Pretty.str_of o pretty_abbrev_sg;
   1.273  
   1.274  
   1.275  (* id and self *)
   1.276  
   1.277 -fun check_stale (sg as Sg ({id, ...},
   1.278 +fun check_stale pos (sg as Sg ({id, ...},
   1.279          {self = SgRef (SOME (ref (Sg ({id = id', ...}, _)))), ...})) =
   1.280        if id = id' then sg
   1.281 -      else raise TERM ("Stale signature: " ^ str_of_sg sg, [])
   1.282 -  | check_stale _ = sys_error "Sign.check_stale";
   1.283 +      else raise TERM ("Stale signature (in " ^ pos ^ "): " ^ str_of_sg sg, [])
   1.284 +  | check_stale _ _ = sys_error "Sign.check_stale";
   1.285  
   1.286 -fun is_stale sg = (check_stale sg; false) handle TERM _ => true;
   1.287 +val is_stale = not o can (check_stale "Sign.is_stale");
   1.288  
   1.289 -fun self_ref (sg as Sg (_, {self, ...})) = (check_stale sg; self);
   1.290 +fun self_ref (sg as Sg (_, {self, ...})) = (check_stale "Sign.self_ref" sg; self);
   1.291  
   1.292  fun deref (SgRef (SOME (ref sg))) = sg
   1.293    | deref (SgRef NONE) = sys_error "Sign.deref";
   1.294  
   1.295 +fun assign (SgRef (SOME r)) sg = r := sg
   1.296 +  | assign (SgRef NONE) _ = sys_error "Sign.assign";
   1.297 +
   1.298  fun name_of (sg as Sg ({id = ref name, ...}, _)) =
   1.299    if name = "" orelse ord name = ord "#" then
   1.300      raise TERM ("Nameless signature " ^ str_of_sg sg, [])
   1.301    else name;
   1.302  
   1.303 +fun is_draft (Sg ({stamps = ref name :: _, ...}, _)) =
   1.304 +      name = "" orelse ord name = ord "#"
   1.305 +  | is_draft _ = sys_error "Sign.is_draft";
   1.306 +
   1.307  
   1.308  (* inclusion and equality *)
   1.309  
   1.310  local
   1.311    (*avoiding polymorphic equality: factor 10 speedup*)
   1.312 -  fun mem_stamp (_:string ref, []) = false
   1.313 +  fun mem_stamp (_: string ref, []) = false
   1.314      | mem_stamp (x, y :: ys) = x = y orelse mem_stamp (x, ys);
   1.315  
   1.316    fun subset_stamp ([], ys) = true
   1.317 @@ -285,7 +287,7 @@
   1.318          mem_stamp (x, ys) andalso subset_stamp (xs, ys);
   1.319  in
   1.320    fun eq_sg (sg1 as Sg ({id = id1, ...}, _), sg2 as Sg ({id = id2, ...}, _)) =
   1.321 -    (check_stale sg1; check_stale sg2; id1 = id2);
   1.322 +    (check_stale "Sign.eq_sg" sg1; check_stale "Sign.eq_sg" sg2; id1 = id2);
   1.323  
   1.324    fun subsig (sg1, sg2) =
   1.325      eq_sg (sg1, sg2) orelse mem_stamp (hd (stamps_of sg1), stamps_of sg2);
   1.326 @@ -303,9 +305,180 @@
   1.327  fun same_sg (sg1, sg2) =
   1.328    eq_sg (sg1, sg2) orelse eq_set_string (pairself (map ! o stamps_of) (sg1, sg2));
   1.329  
   1.330 -(*test for drafts*)
   1.331 -fun is_draft (Sg ({stamps = ref name :: _, ...}, _)) =
   1.332 -  name = "" orelse ord name = ord "#";
   1.333 +
   1.334 +(* data operations *)
   1.335 +
   1.336 +fun err_method name kind e =    (* FIXME wrap exn msg!? *)
   1.337 +  (warning ("Error while invoking " ^ quote kind ^ " " ^ name ^ " method"); raise e);
   1.338 +
   1.339 +fun err_inconsistent kinds =
   1.340 +  error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " data");
   1.341 +
   1.342 +val empty_data = Data Symtab.empty;
   1.343 +
   1.344 +fun merge_data (Data tab1, Data tab2) =
   1.345 +  let
   1.346 +    val data1 = map snd (Symtab.dest tab1);
   1.347 +    val data2 = map snd (Symtab.dest tab2);
   1.348 +    val all_data = data1 @ data2;
   1.349 +    val kinds = gen_distinct Object.eq_kind (map fst all_data);
   1.350 +
   1.351 +   fun entry data kind =
   1.352 +     (case gen_assoc Object.eq_kind (data, kind) of
   1.353 +       NONE => []
   1.354 +     | SOME x => [(kind, x)]);
   1.355 +
   1.356 +    fun merge_entries [(kind, (e, mths as (_, ext, _, _)))] =
   1.357 +          (kind, (ext e handle exn => err_method "prep_ext" (Object.name_of_kind kind) exn, mths))
   1.358 +      | merge_entries [(kind, (e1, mths as (_, _, mrg, _))), (_, (e2, _))] =
   1.359 +          (kind, (mrg (e1, e2)
   1.360 +            handle exn => err_method "merge" (Object.name_of_kind kind) exn, mths))
   1.361 +      | merge_entries _ = sys_error "merge_entries";
   1.362 +
   1.363 +    val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds;
   1.364 +    val data_idx = map (fn (k, x) => (Object.name_of_kind k, (k, x))) data;
   1.365 +  in
   1.366 +    Data (Symtab.make data_idx)
   1.367 +      handle Symtab.DUPS dups => err_inconsistent dups
   1.368 +  end;
   1.369 +
   1.370 +fun prep_ext_data data = merge_data (data, empty_data);
   1.371 +
   1.372 +fun copy_data (Data tab) =
   1.373 +  let
   1.374 +    fun cp_data (k, (e, mths as (cp, _, _, _))) =
   1.375 +      (k, (cp e handle exn => err_method "copy" (Object.name_of_kind k) exn, mths));
   1.376 +  in Data (Symtab.map cp_data tab) end;
   1.377 +
   1.378 +
   1.379 +
   1.380 +(** build signatures **)
   1.381 +
   1.382 +fun create_sg name self stamps naming data sign =
   1.383 +  let
   1.384 +    val id = ref name;
   1.385 +    val stamps' = (case stamps of ref "#" :: ss => ss | ss => ss);
   1.386 +    val _ = conditional (exists (equal name o !) stamps')
   1.387 +      (fn () => error ("Theory already contains a " ^ quote name ^ " component"));
   1.388 +    val sg = make_sg (id, self, id :: stamps') naming data sign;
   1.389 +  in assign self sg; sg end;
   1.390 +
   1.391 +fun new_sg f (sg as Sg ({stamps, syn, ...}, {self = _, tsig, consts, naming, spaces, data})) =
   1.392 +  let
   1.393 +    val _ = check_stale "Sign.new_sg" sg;
   1.394 +    val self' = SgRef (SOME (ref sg));
   1.395 +    val data' = f data;
   1.396 +  in create_sg "#" self' stamps naming data' (syn, tsig, consts, spaces) end;
   1.397 +
   1.398 +val prep_ext = new_sg prep_ext_data;
   1.399 +val copy = new_sg copy_data;
   1.400 +
   1.401 +fun add_name name (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, spaces, data})) =
   1.402 + (check_stale "Sign.add_name" sg;
   1.403 +  create_sg name self stamps naming data (syn, tsig, consts, spaces));
   1.404 +
   1.405 +fun map_sg f (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, spaces, data})) =
   1.406 +  let
   1.407 +    val _ = check_stale "Sign.map_sg" sg;
   1.408 +    val (naming', data', sign') = f (naming, data, (syn, tsig, consts, spaces));
   1.409 +  in create_sg "#" self stamps naming' data' sign' end;
   1.410 +
   1.411 +fun map_naming f = map_sg (fn (naming, data, sign) => (f naming, data, sign));
   1.412 +fun map_data f = map_sg (fn (naming, data, sign) => (naming, f data, sign));
   1.413 +fun map_sign f = map_sg (fn (naming, data, sign) => (naming, data, f sign));
   1.414 +fun map_syn f = map_sign (fn (syn, tsig, consts, spaces) => (f syn, tsig, consts, spaces));
   1.415 +
   1.416 +
   1.417 +
   1.418 +(** signature data **)
   1.419 +
   1.420 +(* errors *)
   1.421 +
   1.422 +fun of_theory sg = "\nof theory " ^ str_of_sg sg;
   1.423 +
   1.424 +fun err_dup_init sg kind =
   1.425 +  error ("Duplicate initialization of " ^ quote kind ^ " data" ^ of_theory sg);
   1.426 +
   1.427 +fun err_uninit sg kind =
   1.428 +  error ("Tried to access uninitialized " ^ quote kind ^ " data" ^ of_theory sg);
   1.429 +
   1.430 +fun err_access sg kind =
   1.431 +  error ("Unauthorized access to " ^ quote kind ^ " data" ^ of_theory sg);
   1.432 +
   1.433 +
   1.434 +(* access data *)
   1.435 +
   1.436 +fun data_kinds (Data tab) = Symtab.keys tab;
   1.437 +
   1.438 +fun lookup_data sg tab kind =
   1.439 +  let val name = Object.name_of_kind kind in
   1.440 +    (case Symtab.lookup (tab, name) of
   1.441 +      SOME (k, x) =>
   1.442 +        if Object.eq_kind (kind, k) then x
   1.443 +        else err_access sg name
   1.444 +    | NONE => err_uninit sg name)
   1.445 +  end;
   1.446 +
   1.447 +fun init_data (kind, (e, cp, ext, mrg, prt)) sg = sg |> map_data (fn Data tab =>
   1.448 +  Data (Symtab.update_new ((Object.name_of_kind kind, (kind, (e, (cp, ext, mrg, prt)))), tab))
   1.449 +    handle Symtab.DUP name => err_dup_init sg name);
   1.450 +
   1.451 +fun get_data kind dest (sg as Sg (_, {data = Data tab, ...})) =
   1.452 +  let val x = fst (lookup_data sg tab kind)
   1.453 +  in dest x handle Match => Object.kind_error kind end;
   1.454 +
   1.455 +fun put_data kind mk x sg = sg |> map_data (fn Data tab =>
   1.456 +  Data (Symtab.update ((Object.name_of_kind kind,
   1.457 +    (kind, (mk x, snd (lookup_data sg tab kind)))), tab)));
   1.458 +
   1.459 +fun print_data kind (sg as Sg (_, {data = Data tab, ...})) =
   1.460 +  let val (e, (_, _, _, prt)) = lookup_data sg tab kind in
   1.461 +    prt sg e handle exn =>
   1.462 +      err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) exn
   1.463 +  end;
   1.464 +
   1.465 +fun print_all_data (sg as Sg (_, {data = Data tab, ...})) =
   1.466 +  List.app (fn kind => print_data kind sg) (map (#1 o #2) (Symtab.dest tab));
   1.467 +
   1.468 +
   1.469 +
   1.470 +(** primitive signatures **)
   1.471 +
   1.472 +val empty_spaces =
   1.473 +  {class = NameSpace.empty, tycon = NameSpace.empty, const = NameSpace.empty};
   1.474 +
   1.475 +fun merge_spaces
   1.476 +  ({class = class1, tycon = tycon1, const = const1},
   1.477 +    {class = class2, tycon = tycon2, const = const2}) =
   1.478 +  {class = NameSpace.merge (class1, class2),
   1.479 +   tycon = NameSpace.merge (tycon1, tycon2),
   1.480 +   const = NameSpace.merge (const1, const2)};
   1.481 +
   1.482 +val pure_syn =
   1.483 +  Syn (Syntax.pure_syn, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
   1.484 +
   1.485 +val dummy_sg = make_sg (ref "", SgRef NONE, []) NameSpace.default_naming empty_data
   1.486 +  (pure_syn, Type.empty_tsig, Symtab.empty, empty_spaces);
   1.487 +
   1.488 +val pre_pure =
   1.489 +  create_sg "#" (SgRef (SOME (ref dummy_sg))) [] NameSpace.default_naming empty_data
   1.490 +    (pure_syn, Type.empty_tsig, Symtab.empty, empty_spaces);
   1.491 +
   1.492 +val PureN = "Pure";
   1.493 +val CPureN = "CPure";
   1.494 +
   1.495 +
   1.496 +
   1.497 +(** signature content **)
   1.498 +
   1.499 +(* naming *)
   1.500 +
   1.501 +fun naming_of (Sg (_, {naming, ...})) = naming;
   1.502 +
   1.503 +val base_name = NameSpace.base;
   1.504 +val full_name = NameSpace.full o naming_of;
   1.505 +fun full_name_path sg elems = NameSpace.full (NameSpace.add_path elems (naming_of sg));
   1.506 +val declare_name = NameSpace.declare o naming_of;
   1.507  
   1.508  
   1.509  (* syntax *)
   1.510 @@ -340,7 +513,9 @@
   1.511      Syntax.merge_tr'tabs print_ast_trtab1 print_ast_trtab2);
   1.512  
   1.513  
   1.514 -(* classes and sorts *)
   1.515 +(* type signature *)
   1.516 +
   1.517 +val tsig_of = #tsig o rep_sg;
   1.518  
   1.519  val classes = Type.classes o tsig_of;
   1.520  val defaultS = Type.defaultS o tsig_of;
   1.521 @@ -349,278 +524,114 @@
   1.522  val witness_sorts = Type.witness_sorts o tsig_of;
   1.523  val universal_witness = Type.universal_witness o tsig_of;
   1.524  val typ_instance = Type.typ_instance o tsig_of;
   1.525 -
   1.526 -
   1.527 -
   1.528 -(** signature data **)
   1.529 -
   1.530 -(* errors *)
   1.531 -
   1.532 -fun of_theory sg = "\nof theory " ^ str_of_sg sg;
   1.533 -
   1.534 -fun err_inconsistent kinds =
   1.535 -  error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " data");
   1.536 -
   1.537 -fun err_method name kind e =
   1.538 -  (writeln ("Error while invoking " ^ quote kind ^ " " ^ name ^ " method"); raise e);
   1.539 -
   1.540 -fun err_dup_init sg kind =
   1.541 -  error ("Duplicate initialization of " ^ quote kind ^ " data" ^ of_theory sg);
   1.542 -
   1.543 -fun err_uninit sg kind =
   1.544 -  error ("Tried to access uninitialized " ^ quote kind ^ " data" ^ of_theory sg);
   1.545 -
   1.546 -(*Trying to access theory data using get / put operations from a different
   1.547 -  instance of the TheoryDataFun result.  Typical cure: re-load all files*)
   1.548 -fun err_access sg kind =
   1.549 -  error ("Unauthorized access to " ^ quote kind ^ " data" ^ of_theory sg);
   1.550 -
   1.551 -
   1.552 -(* prepare data *)
   1.553 -
   1.554 -val empty_data = Data Symtab.empty;
   1.555 -
   1.556 -fun merge_data (Data tab1, Data tab2) =
   1.557 -  let
   1.558 -    val data1 = map snd (Symtab.dest tab1);
   1.559 -    val data2 = map snd (Symtab.dest tab2);
   1.560 -    val all_data = data1 @ data2;
   1.561 -    val kinds = gen_distinct Object.eq_kind (map fst all_data);
   1.562 -
   1.563 -   fun entry data kind =
   1.564 -     (case gen_assoc Object.eq_kind (data, kind) of
   1.565 -       NONE => []
   1.566 -     | SOME x => [(kind, x)]);
   1.567 -
   1.568 -    fun merge_entries [(kind, (e, mths as (_, ext, _, _)))] =
   1.569 -          (kind, (ext e handle exn => err_method "prep_ext" (Object.name_of_kind kind) exn, mths))
   1.570 -      | merge_entries [(kind, (e1, mths as (_, _, mrg, _))), (_, (e2, _))] =
   1.571 -          (kind, (mrg (e1, e2)
   1.572 -            handle exn => err_method "merge" (Object.name_of_kind kind) exn, mths))
   1.573 -      | merge_entries _ = sys_error "merge_entries";
   1.574 -
   1.575 -    val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds;
   1.576 -    val data_idx = map (fn (k, x) => (Object.name_of_kind k, (k, x))) data;
   1.577 -  in
   1.578 -    Data (Symtab.make data_idx)
   1.579 -      handle Symtab.DUPS dups => err_inconsistent dups
   1.580 -  end;
   1.581 -
   1.582 -fun prep_ext_data data = merge_data (data, empty_data);
   1.583 -
   1.584 -fun init_data_sg sg (Data tab) kind e cp ext mrg prt =
   1.585 -  let val name = Object.name_of_kind kind in
   1.586 -    Data (Symtab.update_new ((name, (kind, (e, (cp, ext, mrg, prt)))), tab))
   1.587 -      handle Symtab.DUP _ => err_dup_init sg name
   1.588 -  end;
   1.589 +fun is_logtype sg c = c mem_string Type.logical_types (tsig_of sg);
   1.590  
   1.591  
   1.592 -(* access data *)
   1.593 -
   1.594 -fun data_kinds (Data tab) = map fst (Symtab.dest tab);
   1.595 +(* consts signature *)
   1.596  
   1.597 -fun lookup_data sg tab kind =
   1.598 -  let val name = Object.name_of_kind kind in
   1.599 -    (case Symtab.lookup (tab, name) of
   1.600 -      SOME (k, x) =>
   1.601 -        if Object.eq_kind (kind, k) then x
   1.602 -        else err_access sg name
   1.603 -    | NONE => err_uninit sg name)
   1.604 -  end;
   1.605 +fun const_type (Sg (_, {consts, ...})) c = Option.map #1 (Symtab.lookup (consts, c));
   1.606  
   1.607 -fun get_data kind f (sg as Sg (_, {data = Data tab, ...})) =
   1.608 -  let val x = fst (lookup_data sg tab kind)
   1.609 -  in f x handle Match => Object.kind_error kind end;
   1.610 -
   1.611 -fun print_data kind (sg as Sg (_, {data = Data tab, ...})) =
   1.612 -  let val (e, (_, _, _, prt)) = lookup_data sg tab kind
   1.613 -  in prt sg e handle exn => err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) exn end;
   1.614 +fun the_const_type sg c =
   1.615 +  (case const_type sg c of SOME T => T
   1.616 +  | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
   1.617  
   1.618 -fun print_all_data (sg as Sg (_, {data = Data tab, ...})) =
   1.619 -  app (fn kind => print_data kind sg) (map (#1 o #2) (Symtab.dest tab));
   1.620 -
   1.621 -fun put_data_sg sg (Data tab) kind f x =
   1.622 -  Data (Symtab.update ((Object.name_of_kind kind,
   1.623 -    (kind, (f x, snd (lookup_data sg tab kind)))), tab));
   1.624 -
   1.625 +fun declared_tyname sg c = is_some (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c));
   1.626 +fun declared_const sg c = is_some (const_type sg c);
   1.627  
   1.628  
   1.629 -(** build signatures **)
   1.630 -
   1.631 -fun ext_stamps stamps (id as ref name) =
   1.632 -  let val stmps = (case stamps of ref "#" :: ss => ss | ss => ss) in
   1.633 -    if exists (equal name o !) stmps then
   1.634 -      error ("Theory already contains a " ^ quote name ^ " component")
   1.635 -    else id :: stmps
   1.636 -  end;
   1.637 -
   1.638 -fun create_sign self stamps name (syn, tsig, ctab, (naming, spaces), data) =
   1.639 -  let
   1.640 -    val id = ref name;
   1.641 -    val sign =
   1.642 -      make_sign (id, self, tsig, ctab, syn, naming, spaces, data, ext_stamps stamps id);
   1.643 -  in
   1.644 -    (case self of
   1.645 -      SgRef (SOME r) => r := sign
   1.646 -    | _ => sys_error "Sign.create_sign");
   1.647 -    sign
   1.648 -  end;
   1.649 -
   1.650 -fun extend_sign keep extfun name decls
   1.651 -    (sg as Sg ({id = _, stamps, syn}, {self, tsig, consts, naming, spaces, data})) =
   1.652 -  let
   1.653 -    val _ = check_stale sg;
   1.654 -    val (self', data') =
   1.655 -      if is_draft sg andalso keep then (self, data)
   1.656 -      else (SgRef (SOME (ref sg)), prep_ext_data data);
   1.657 -  in
   1.658 -    create_sign self' stamps name
   1.659 -      (extfun sg (syn, tsig, consts, (naming, spaces), data') decls)
   1.660 -  end;
   1.661 -
   1.662 -
   1.663 -
   1.664 -(** name spaces **)
   1.665 -
   1.666 -(* naming *)
   1.667 -
   1.668 -val base_name = NameSpace.base;
   1.669 -val full_name = NameSpace.full o naming_of;
   1.670 -fun full_name_path sg elems = NameSpace.full (NameSpace.add_path elems (naming_of sg));
   1.671 -val declare_name = NameSpace.declare o naming_of;
   1.672 -
   1.673 -
   1.674 -(* kinds *)
   1.675 +(* name spaces *)
   1.676  
   1.677  val classK = "class";
   1.678  val typeK = "type";
   1.679  val constK = "const";
   1.680  
   1.681 -
   1.682 -(* declare and retrieve names *)
   1.683 -
   1.684 -fun get_space spaces kind =
   1.685 -  if_none (assoc_string (spaces, kind)) NameSpace.empty;
   1.686 -
   1.687 -(*input and output of qualified names*)
   1.688 -val intrn = NameSpace.intern oo get_space;
   1.689 -val extrn = NameSpace.extern oo get_space;
   1.690 -fun extrn_table spaces = NameSpace.extern_table o (get_space spaces);
   1.691 -
   1.692 -(*add / hide names*)
   1.693 -fun change_space f kind names spaces =
   1.694 -  overwrite (spaces, (kind, f names (get_space spaces kind)));
   1.695 -
   1.696 -val add_names = change_space o fold o declare_name;
   1.697 -val hide_names = change_space o fold o NameSpace.hide;
   1.698 +fun illegal_space kind = "Illegal signature name space: " ^ quote kind;
   1.699  
   1.700 -
   1.701 -(* intern / extern names *)
   1.702 -
   1.703 -local
   1.704 -  (*prepare mapping of names*)
   1.705 -  fun mapping f add_xs t =
   1.706 -    let
   1.707 -      fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end;
   1.708 -      val table = List.mapPartial f' (add_xs (t, []));
   1.709 -      fun lookup x = if_none (assoc (table, x)) x;
   1.710 -    in lookup end;
   1.711 -
   1.712 -  (*intern / extern typ*)
   1.713 -  fun trn_typ trn T =
   1.714 -    T |> map_typ
   1.715 -      (mapping (trn classK) add_typ_classes T)
   1.716 -      (mapping (trn typeK) add_typ_tycons T);
   1.717 +fun space_of sg kind = #spaces (rep_sg sg) |>
   1.718 + (if kind = classK then #class
   1.719 +  else if kind = typeK then #tycon
   1.720 +  else if kind = constK then #const
   1.721 +  else raise TERM (illegal_space kind, []));
   1.722  
   1.723 -  (*intern / extern term*)
   1.724 -  fun trn_term trn t =
   1.725 -    t |> map_term
   1.726 -      (mapping (trn classK) add_term_classes t)
   1.727 -      (mapping (trn typeK) add_term_tycons t)
   1.728 -      (mapping (trn constK) add_term_consts t);
   1.729 -
   1.730 -  val spaces_of = #spaces o rep_sg;
   1.731 -in
   1.732 -  fun intrn_class spaces = intrn spaces classK;
   1.733 -  fun extrn_class spaces = extrn spaces classK;
   1.734 -
   1.735 -  val intrn_sort = map o intrn_class;
   1.736 -  val intrn_typ = trn_typ o intrn;
   1.737 -  val intrn_term = trn_term o intrn;
   1.738 -
   1.739 -  val extrn_sort = map o extrn_class;
   1.740 -  val extrn_typ = trn_typ o extrn;
   1.741 -  val extrn_term = trn_term o extrn;
   1.742 +fun map_space kind f {class, tycon, const} =
   1.743 +  let
   1.744 +    val (class', tycon', const') =
   1.745 +      if kind = classK then (f class, tycon, const)
   1.746 +      else if kind = typeK then (class, f tycon, const)
   1.747 +      else if kind = constK then (class, tycon, f const)
   1.748 +      else raise TERM (illegal_space kind, []);
   1.749 +  in {class = class', tycon = tycon', const = const'} end;
   1.750  
   1.751 -  fun intrn_tycons spaces T =
   1.752 -    map_typ I (mapping (intrn spaces typeK) add_typ_tycons T) T;
   1.753 -
   1.754 -  val intern = intrn o spaces_of;
   1.755 -  val extern = extrn o spaces_of;
   1.756 -  fun extern_table sg = extrn_table (spaces_of sg);
   1.757 -
   1.758 -  fun extern_typ (sg as Sg (_, {spaces, ...})) T =
   1.759 -       if ! NameSpace.long_names then T else extrn_typ spaces T;
   1.760 -
   1.761 -  val intern_class = intrn_class o spaces_of;
   1.762 -  val intern_sort = intrn_sort o spaces_of;
   1.763 -  val intern_typ = intrn_typ o spaces_of;
   1.764 -  val intern_term = intrn_term o spaces_of;
   1.765 -
   1.766 -  fun intern_tycon sg = intrn (spaces_of sg) typeK;
   1.767 -  fun intern_const sg = intrn (spaces_of sg) constK;
   1.768 -
   1.769 -  val intern_tycons = intrn_tycons o spaces_of;
   1.770 -end;
   1.771 +fun declare_names sg kind = map_space kind o fold (declare_name sg);
   1.772 +fun hide_names kind = map_space kind oo (fold o NameSpace.hide);
   1.773  
   1.774  
   1.775  
   1.776 -(** partial Pure signature **)
   1.777 +(** intern / extern names **)
   1.778 +
   1.779 +val intern = NameSpace.intern oo space_of;
   1.780 +val extern = NameSpace.extern oo space_of;
   1.781 +fun extern_table sg = curry NameSpace.extern_table o space_of sg;
   1.782  
   1.783 -val pure_syn =
   1.784 -  Syn (Syntax.pure_syn, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
   1.785 +fun intern_class sg = intern sg classK;
   1.786 +fun extern_class sg = extern sg classK;
   1.787 +fun intern_tycon sg = intern sg typeK;
   1.788 +fun extern_tycon sg = extern sg typeK;
   1.789 +fun intern_const sg = intern sg constK;
   1.790 +fun extern_const sg = extern sg constK;
   1.791 +
   1.792 +val intern_sort = map o intern_class;
   1.793 +val extern_sort = map o extern_class;
   1.794 +
   1.795 +local
   1.796  
   1.797 -val dummy_sg = make_sign (ref "", SgRef NONE, Type.empty_tsig,
   1.798 -  Symtab.empty, pure_syn, NameSpace.default_naming, [], empty_data, []);
   1.799 +fun mapping add_names f t =
   1.800 +  let
   1.801 +    fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end;
   1.802 +    val tab = List.mapPartial f' (add_names (t, []));
   1.803 +    fun get x = if_none (assoc_string (tab, x)) x;
   1.804 +  in get end;
   1.805 +
   1.806 +fun typ_mapping f g sg T =
   1.807 +  T |> Term.map_typ
   1.808 +    (mapping add_typ_classes (f sg) T)
   1.809 +    (mapping add_typ_tycons (g sg) T);
   1.810  
   1.811 -val pre_pure =
   1.812 -  create_sign (SgRef (SOME (ref dummy_sg))) [] "#"
   1.813 -    (pure_syn, Type.empty_tsig, Symtab.empty, (NameSpace.default_naming, []), empty_data);
   1.814 +fun term_mapping f g h sg t =
   1.815 +  t |> Term.map_term
   1.816 +    (mapping add_term_classes (f sg) t)
   1.817 +    (mapping add_term_tycons (g sg) t)
   1.818 +    (mapping add_term_consts (h sg) t);
   1.819 +
   1.820 +in
   1.821  
   1.822 -val PureN = "Pure";
   1.823 -val CPureN = "CPure";
   1.824 +val intern_typ = typ_mapping intern_class intern_tycon;
   1.825 +val extern_typ = typ_mapping extern_class extern_tycon;
   1.826 +val intern_term = term_mapping intern_class intern_tycon intern_const;
   1.827 +val extern_term = term_mapping extern_class extern_tycon extern_const;
   1.828 +val intern_tycons = typ_mapping (K I) intern_tycon;
   1.829 +
   1.830 +end;
   1.831  
   1.832  
   1.833  
   1.834  (** pretty printing of terms, types etc. **)
   1.835  
   1.836 -fun pretty_term' syn (sg as Sg ({stamps, ...}, {spaces, ...})) t =
   1.837 -  Syntax.pretty_term syn
   1.838 -    (exists (equal CPureN o !) stamps)
   1.839 -    (if ! NameSpace.long_names then t else extrn_term spaces t);
   1.840 -
   1.841 +fun pretty_term' syn sg t = Syntax.pretty_term syn (exists_stamp CPureN sg) (extern_term sg t);
   1.842  fun pretty_term sg t = pretty_term' (syn_of sg) sg t;
   1.843 -
   1.844 -fun pretty_typ sg T =
   1.845 -  Syntax.pretty_typ (syn_of sg) (extern_typ sg T);
   1.846 -
   1.847 -fun pretty_sort (sg as Sg (_, {spaces, ...})) S =
   1.848 -  Syntax.pretty_sort (syn_of sg)
   1.849 -    (if ! NameSpace.long_names then S else extrn_sort spaces S);
   1.850 +fun pretty_typ sg T = Syntax.pretty_typ (syn_of sg) (extern_typ sg T);
   1.851 +fun pretty_sort sg S = Syntax.pretty_sort (syn_of sg) (extern_sort sg S);
   1.852  
   1.853  fun pretty_classrel sg cs = Pretty.block (List.concat
   1.854    (separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort sg o single) cs)));
   1.855  
   1.856 -fun pretty_arity sg (t, Ss, S) =
   1.857 +fun pretty_arity sg (a, Ss, S) =
   1.858    let
   1.859 -    val t' = extern sg typeK t;
   1.860 +    val a' = extern_tycon sg a;
   1.861      val dom =
   1.862        if null Ss then []
   1.863        else [Pretty.list "(" ")" (map (pretty_sort sg) Ss), Pretty.brk 1];
   1.864 -  in
   1.865 -    Pretty.block
   1.866 -      ([Pretty.str (t' ^ " ::"), Pretty.brk 1] @ dom @ [pretty_sort sg S])
   1.867 -  end;
   1.868 +  in Pretty.block ([Pretty.str (a' ^ " ::"), Pretty.brk 1] @ dom @ [pretty_sort sg S]) end;
   1.869  
   1.870  val string_of_term = Pretty.string_of oo pretty_term;
   1.871  val string_of_typ = Pretty.string_of oo pretty_typ;
   1.872 @@ -628,84 +639,42 @@
   1.873  val string_of_classrel = Pretty.string_of oo pretty_classrel;
   1.874  val string_of_arity = Pretty.string_of oo pretty_arity;
   1.875  
   1.876 -fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg);
   1.877 -fun pprint_typ sg = Pretty.pprint o Pretty.quote o (pretty_typ sg);
   1.878 +val pprint_term = (Pretty.pprint o Pretty.quote) oo pretty_term;
   1.879 +val pprint_typ = (Pretty.pprint o Pretty.quote) oo pretty_typ;
   1.880  
   1.881  fun pp sg = Pretty.pp (pretty_term sg, pretty_typ sg, pretty_sort sg,
   1.882    pretty_classrel sg, pretty_arity sg);
   1.883  
   1.884  
   1.885  
   1.886 -(** read sorts **)  (*exception ERROR*)
   1.887 -
   1.888 -fun err_in_sort s =
   1.889 -  error ("The error(s) above occurred in sort " ^ quote s);
   1.890 -
   1.891 -fun rd_sort sg syn tsig spaces str =
   1.892 -  let val S = intrn_sort spaces (Syntax.read_sort (make_syntax sg syn) str
   1.893 -    handle ERROR => err_in_sort str)
   1.894 -  in Type.cert_sort tsig S handle TYPE (msg, _, _) => (error_msg msg; err_in_sort str) end;
   1.895 +(** certify entities **)    (*exception TYPE*)
   1.896  
   1.897 -(*read and certify sort wrt a signature*)
   1.898 -fun read_sort (sg as Sg ({syn, ...}, {tsig, spaces, ...})) str =
   1.899 -  (check_stale sg; rd_sort sg syn tsig spaces str);
   1.900 -
   1.901 -fun cert_sort _ _ tsig _ = Type.cert_sort tsig;
   1.902 +(* certify wrt. type signature *)
   1.903  
   1.904 -
   1.905 -
   1.906 -(** read types **)  (*exception ERROR*)
   1.907 -
   1.908 -fun err_in_type s =
   1.909 -  error ("The error(s) above occurred in type " ^ quote s);
   1.910 +fun certify cert = cert o tsig_of o check_stale "Sign.certify";
   1.911  
   1.912 -fun rd_raw_typ syn tsig spaces def_sort str =
   1.913 -  intrn_tycons spaces (Syntax.read_typ syn
   1.914 -    (TypeInfer.get_sort tsig def_sort (intrn_sort spaces)) (intrn_sort spaces) str
   1.915 -      handle ERROR => err_in_type str);
   1.916 -
   1.917 -fun read_raw_typ' syn (sg as Sg (_, {tsig, spaces, ...}), def_sort) str =
   1.918 -  (check_stale sg; rd_raw_typ syn tsig spaces def_sort str);
   1.919 -
   1.920 -fun read_raw_typ (sg, def_sort) = read_raw_typ' (syn_of sg) (sg, def_sort);
   1.921 -
   1.922 -(*read and certify typ wrt a signature*)
   1.923 -local
   1.924 -  fun read_typ_aux rd cert (sg, def_sort) str =
   1.925 -    cert (tsig_of sg) (rd (sg, def_sort) str)
   1.926 -      handle TYPE (msg, _, _) => (error_msg msg; err_in_type str);
   1.927 -in
   1.928 -  val read_typ          = read_typ_aux read_raw_typ Type.cert_typ;
   1.929 -  val read_typ_raw      = read_typ_aux read_raw_typ Type.cert_typ_raw;
   1.930 -  fun read_typ' syn     = read_typ_aux (read_raw_typ' syn) Type.cert_typ;
   1.931 -  fun read_typ_raw' syn = read_typ_aux (read_raw_typ' syn) Type.cert_typ_raw;
   1.932 -end;
   1.933 -
   1.934 -
   1.935 -
   1.936 -(** certify classes, sorts, types and terms **)   (*exception TYPE*)
   1.937 -
   1.938 -val certify_class = Type.cert_class o tsig_of;
   1.939 -val certify_sort = Type.cert_sort o tsig_of;
   1.940 -val certify_typ = Type.cert_typ o tsig_of;
   1.941 -val certify_typ_raw = Type.cert_typ_raw o tsig_of;
   1.942 +val certify_class      = certify Type.cert_class;
   1.943 +val certify_sort       = certify Type.cert_sort;
   1.944 +val certify_typ        = certify Type.cert_typ;
   1.945 +val certify_typ_syntax = certify Type.cert_typ_syntax;
   1.946 +val certify_typ_abbrev = certify Type.cert_typ_abbrev;
   1.947  
   1.948  
   1.949  (* certify_term *)
   1.950  
   1.951  local
   1.952  
   1.953 -(*compute and check type of the term*)
   1.954 -fun type_check pp sg tm =
   1.955 +(*determine and check the type of a term*)
   1.956 +fun type_check pp tm =
   1.957    let
   1.958      fun err_appl why bs t T u U =
   1.959        let
   1.960          val xs = map Free bs;           (*we do not rename here*)
   1.961          val t' = subst_bounds (xs, t);
   1.962          val u' = subst_bounds (xs, u);
   1.963 -        val text = cat_lines
   1.964 +        val msg = cat_lines
   1.965            (TypeInfer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
   1.966 -      in raise TYPE (text, [T, U], [t', u']) end;
   1.967 +      in raise TYPE (msg, [T, U], [t', u']) end;
   1.968  
   1.969      fun typ_of (_, Const (_, T)) = T
   1.970        | typ_of (_, Free  (_, T)) = T
   1.971 @@ -727,7 +696,7 @@
   1.972  
   1.973  fun certify_term pp sg tm =
   1.974    let
   1.975 -    val _ = check_stale sg;
   1.976 +    val _ = check_stale "Sign.certify_term" sg;
   1.977  
   1.978      val tm' = map_term_types (Type.cert_typ (tsig_of sg)) tm;
   1.979      val tm' = if tm = tm' then tm else tm';  (*avoid copying of already normal term*)
   1.980 @@ -749,13 +718,55 @@
   1.981        | check_atoms _ = ();
   1.982    in
   1.983      check_atoms tm';
   1.984 -    (tm', type_check pp sg tm', maxidx_of_term tm')
   1.985 +    (tm', type_check pp tm', maxidx_of_term tm')
   1.986    end;
   1.987  
   1.988  end;
   1.989  
   1.990  
   1.991 -(* type and constant names *)
   1.992 +
   1.993 +(** read and certify entities **)    (*exception ERROR*)
   1.994 +
   1.995 +(* sorts *)
   1.996 +
   1.997 +fun read_sort' syn sg str =
   1.998 +  let
   1.999 +    val _ = check_stale "Sign.read_sort'" sg;
  1.1000 +    val S = intern_sort sg (Syntax.read_sort syn str);
  1.1001 +  in Type.cert_sort (tsig_of sg) S handle TYPE (msg, _, _) => error msg end;
  1.1002 +
  1.1003 +fun read_sort sg str = read_sort' (syn_of sg) sg str;
  1.1004 +
  1.1005 +
  1.1006 +(* types *)
  1.1007 +
  1.1008 +local
  1.1009 +
  1.1010 +fun gen_read_typ' cert syn (sg, def_sort) str =
  1.1011 +  let
  1.1012 +    val _ = check_stale "Sign.gen_read_typ'" sg;
  1.1013 +    val get_sort = TypeInfer.get_sort (tsig_of sg) def_sort (intern_sort sg);
  1.1014 +    val T = intern_tycons sg (Syntax.read_typ syn get_sort (intern_sort sg) str);
  1.1015 +  in cert (tsig_of sg) T handle TYPE (msg, _, _) => error msg end
  1.1016 +  handle ERROR => error ("The error(s) above occurred in type " ^ quote str);
  1.1017 +
  1.1018 +fun gen_read_typ cert (sg, def_sort) str = gen_read_typ' cert (syn_of sg) (sg, def_sort) str;
  1.1019 +
  1.1020 +in
  1.1021 +
  1.1022 +fun no_def_sort sg = (sg, K NONE);
  1.1023 +
  1.1024 +val read_typ'        = gen_read_typ' Type.cert_typ;
  1.1025 +val read_typ_syntax' = gen_read_typ' Type.cert_typ_syntax;
  1.1026 +val read_typ_abbrev' = gen_read_typ' Type.cert_typ_abbrev;
  1.1027 +val read_typ         = gen_read_typ Type.cert_typ;
  1.1028 +val read_typ_syntax  = gen_read_typ Type.cert_typ_syntax;
  1.1029 +val read_typ_abbrev  = gen_read_typ Type.cert_typ_abbrev;
  1.1030 +
  1.1031 +end;
  1.1032 +
  1.1033 +
  1.1034 +(* type and constant names *)    (*exception TYPE*)   (* FIXME really!? *)
  1.1035  
  1.1036  fun read_tyname sg raw_c =
  1.1037    let val c = intern_tycon sg raw_c in
  1.1038 @@ -773,8 +784,8 @@
  1.1039  (** infer_types **)         (*exception ERROR*)
  1.1040  
  1.1041  (*
  1.1042 -  def_type: partial map from indexnames to types (constrains Frees, Vars)
  1.1043 -  def_sort: partial map from indexnames to sorts (constrains TFrees, TVars)
  1.1044 +  def_type: partial map from indexnames to types (constrains Frees and Vars)
  1.1045 +  def_sort: partial map from indexnames to sorts (constrains TFrees and TVars)
  1.1046    used: list of already used type variables
  1.1047    freeze: if true then generated parameters are turned into TFrees, else TVars
  1.1048  
  1.1049 @@ -823,189 +834,167 @@
  1.1050    apfst hd (infer_types_simult pp sg def_type def_sort used freeze [tsT]);
  1.1051  
  1.1052  
  1.1053 -(** read_def_terms **)
  1.1054  
  1.1055 -(*read terms, infer types*)
  1.1056 -fun read_def_terms' pp is_logtype syn (sign, types, sorts) used freeze sTs =
  1.1057 +(** read_def_terms -- read terms and infer types **)
  1.1058 +
  1.1059 +fun read_def_terms' pp is_logtype syn (sg, types, sorts) used freeze sTs =
  1.1060    let
  1.1061      fun read (s, T) =
  1.1062 -      let val T' = certify_typ sign T handle TYPE (msg, _, _) => error msg
  1.1063 +      let val T' = certify_typ sg T handle TYPE (msg, _, _) => error msg
  1.1064        in (Syntax.read is_logtype syn T' s, T') end;
  1.1065 -    val tsTs = map read sTs;
  1.1066 -  in infer_types_simult pp sign types sorts used freeze tsTs end;
  1.1067 +  in infer_types_simult pp sg types sorts used freeze (map read sTs) end;
  1.1068  
  1.1069 -fun read_def_terms (sign, types, sorts) =
  1.1070 -  read_def_terms' (pp sign) (is_logtype sign) (syn_of sign) (sign, types, sorts);
  1.1071 +fun read_def_terms (sg, types, sorts) =
  1.1072 +  read_def_terms' (pp sg) (is_logtype sg) (syn_of sg) (sg, types, sorts);
  1.1073  
  1.1074 -fun simple_read_term sign T s =
  1.1075 -  (read_def_terms (sign, K NONE, K NONE) [] true [(s, T)]
  1.1076 -    handle ERROR => error ("The error(s) above occurred for " ^ s)) |> #1 |> hd;
  1.1077 +fun simple_read_term sg T s =
  1.1078 +  let val ([t], _) = read_def_terms (sg, K NONE, K NONE) [] true [(s, T)]
  1.1079 +  in t end
  1.1080 +  handle ERROR => error ("The error(s) above occurred for term " ^ s);
  1.1081  
  1.1082  
  1.1083  
  1.1084 -(** extend signature **)    (*exception ERROR*)
  1.1085 -
  1.1086 -(** signature extension functions **)  (*exception ERROR*)
  1.1087 -
  1.1088 -fun decls_of sg name_of mfixs =
  1.1089 -  map (fn (x, y, mx) => (full_name sg (name_of x mx), y)) mfixs;
  1.1090 -
  1.1091 -fun no_read _ _ _ _ decl = decl;
  1.1092 -
  1.1093 +(** signature extension functions **)  (*exception ERROR/TYPE*)
  1.1094  
  1.1095  (* add default sort *)
  1.1096  
  1.1097 -fun ext_defS prep_sort sg (syn, tsig, ctab, (naming, spaces), data) S =
  1.1098 -  (syn, Type.set_defsort (prep_sort sg syn tsig spaces S) tsig,
  1.1099 -    ctab, (naming, spaces), data);
  1.1100 +fun gen_add_defsort prep_sort s sg = sg |> map_sign (fn (syn, tsig, consts, spaces) =>
  1.1101 +  (syn, Type.set_defsort (prep_sort sg s) tsig, consts, spaces));
  1.1102  
  1.1103 -fun ext_defsort arg = ext_defS rd_sort arg;
  1.1104 -fun ext_defsort_i arg = ext_defS cert_sort arg;
  1.1105 +val add_defsort = gen_add_defsort read_sort;
  1.1106 +val add_defsort_i = gen_add_defsort certify_sort;
  1.1107  
  1.1108  
  1.1109  (* add type constructors *)
  1.1110  
  1.1111 -fun ext_types sg (syn, tsig, ctab, (naming, spaces), data) types =
  1.1112 +fun add_types types sg = sg |> map_sign (fn (syn, tsig, consts, spaces) =>
  1.1113    let
  1.1114 -    val decls = decls_of sg Syntax.type_name types;
  1.1115      val syn' = map_syntax (Syntax.extend_type_gram types) syn;
  1.1116 +    val decls = map (fn (a, n, mx) => (full_name sg (Syntax.type_name a mx), n)) types;
  1.1117      val tsig' = Type.add_types decls tsig;
  1.1118 -  in (syn', tsig', ctab, (naming, add_names sg typeK (map fst decls) spaces), data) end;
  1.1119 +    val spaces' = declare_names sg typeK (map #1 decls) spaces;
  1.1120 +  in (syn', tsig', consts, spaces') end);
  1.1121 +
  1.1122 +
  1.1123 +(* add nonterminals *)
  1.1124 +
  1.1125 +fun add_nonterminals bnames sg = sg |> map_sign (fn (syn, tsig, consts, spaces) =>
  1.1126 +  let
  1.1127 +    val syn' = map_syntax (Syntax.extend_consts bnames) syn;
  1.1128 +    val names = map (full_name sg) bnames;
  1.1129 +    val tsig' = Type.add_nonterminals names tsig;
  1.1130 +    val spaces' = declare_names sg typeK names spaces;
  1.1131 +  in (syn', tsig', consts, spaces') end);
  1.1132  
  1.1133  
  1.1134  (* add type abbreviations *)
  1.1135  
  1.1136 -fun read_abbr sg syn tsig spaces (t, vs, rhs_src) =
  1.1137 -  (t, vs, rd_raw_typ (make_syntax sg syn) tsig spaces (K NONE) rhs_src)
  1.1138 -    handle ERROR => error ("in type abbreviation " ^ t);
  1.1139 -
  1.1140 -fun ext_abbrs rd_abbr sg (syn, tsig, ctab, (naming, spaces), data) abbrs =
  1.1141 -  let
  1.1142 -    fun mfix_of (t, vs, _, mx) = (t, length vs, mx);
  1.1143 -    val syn' = syn |> map_syntax (Syntax.extend_type_gram (map mfix_of abbrs));
  1.1144 +fun gen_add_tyabbr prep_typ (a, vs, rhs, mx) sg =
  1.1145 +  sg |> map_sign (fn (syn, tsig, consts, spaces) =>
  1.1146 +    let
  1.1147 +      val syn' = map_syntax (Syntax.extend_type_gram [(a, length vs, mx)]) syn;
  1.1148 +      val a' = full_name sg (Syntax.type_name a mx);
  1.1149 +      val abbr = (a', vs, prep_typ sg rhs) handle ERROR =>
  1.1150 +        error ("in type abbreviation " ^ quote (Syntax.type_name a' mx));
  1.1151 +      val tsig' = Type.add_abbrevs [abbr] tsig;
  1.1152 +      val spaces' = declare_names sg typeK [a'] spaces;
  1.1153 +    in (syn', tsig', consts, spaces') end);
  1.1154  
  1.1155 -    val abbrs' =
  1.1156 -      map (fn (t, vs, rhs, mx) =>
  1.1157 -        (full_name sg (Syntax.type_name t mx), vs, rhs)) abbrs;
  1.1158 -    val spaces' = add_names sg typeK (map #1 abbrs') spaces;
  1.1159 -    val decls = map (rd_abbr sg syn' tsig spaces') abbrs';
  1.1160 -  in (syn', Type.add_abbrs decls tsig, ctab, (naming, spaces'), data) end;
  1.1161 -
  1.1162 -fun ext_tyabbrs abbrs = ext_abbrs read_abbr abbrs;
  1.1163 -fun ext_tyabbrs_i abbrs = ext_abbrs no_read abbrs;
  1.1164 -
  1.1165 -
  1.1166 -(* add nonterminals *)
  1.1167 -
  1.1168 -fun ext_nonterminals sg (syn, tsig, ctab, (naming, spaces), data) bnames =
  1.1169 -  let val names = map (full_name sg) bnames in
  1.1170 -    (map_syntax (Syntax.extend_consts names) syn,
  1.1171 -      Type.add_nonterminals names tsig, ctab,
  1.1172 -      (naming, add_names sg typeK names spaces), data)
  1.1173 -  end;
  1.1174 +val add_tyabbrs = fold (gen_add_tyabbr (read_typ_syntax o no_def_sort));
  1.1175 +val add_tyabbrs_i = fold (gen_add_tyabbr certify_typ_syntax);
  1.1176  
  1.1177  
  1.1178  (* add type arities *)
  1.1179  
  1.1180 -fun ext_ars int prep_sort sg (syn, tsig, ctab, (naming, spaces), data) arities =
  1.1181 -  let
  1.1182 -    val prepS = prep_sort sg syn tsig spaces;
  1.1183 -    fun prep_arity (c, Ss, S) =
  1.1184 -      (if int then intrn spaces typeK c else c, map prepS Ss, prepS S);
  1.1185 -    val tsig' = Type.add_arities (pp sg) (map prep_arity arities) tsig;
  1.1186 -  in (syn, tsig', ctab, (naming, spaces), data) end;
  1.1187 +fun gen_add_arities int_tycon prep_sort arities sg =
  1.1188 +  sg |> map_sign (fn (syn, tsig, consts, spaces) =>
  1.1189 +    let
  1.1190 +      fun prep_arity (a, Ss, S) = (int_tycon sg a, map (prep_sort sg) Ss, prep_sort sg S)
  1.1191 +        handle ERROR => error ("in arity for type " ^ quote a);
  1.1192 +      val tsig' = Type.add_arities (pp sg) (map prep_arity arities) tsig;
  1.1193 +    in (syn, tsig', consts, spaces) end);
  1.1194  
  1.1195 -fun ext_arities arg = ext_ars true rd_sort arg;
  1.1196 -fun ext_arities_i arg = ext_ars false cert_sort arg;
  1.1197 +val add_arities = gen_add_arities intern_tycon read_sort;
  1.1198 +val add_arities_i = gen_add_arities (K I) certify_sort;
  1.1199  
  1.1200  
  1.1201 -(* add term constants and syntax *)
  1.1202 +(* modify syntax *)
  1.1203 +
  1.1204 +fun gen_syntax change_gram prep_typ (prmode, args) sg =
  1.1205 +  let
  1.1206 +    fun prep (c, T, mx) = (c, prep_typ sg T, mx) handle ERROR =>
  1.1207 +      error ("in syntax declaration " ^ quote (Syntax.const_name c mx));
  1.1208 +  in sg |> map_syn (map_syntax (change_gram (is_logtype sg) prmode (map prep args))) end;
  1.1209 +
  1.1210 +fun gen_add_syntax x = gen_syntax Syntax.extend_const_gram x;
  1.1211  
  1.1212 -fun const_name sg c mx =
  1.1213 -  full_name sg (Syntax.const_name c mx);
  1.1214 +val add_modesyntax = gen_add_syntax (read_typ_syntax o no_def_sort);
  1.1215 +val add_modesyntax_i = gen_add_syntax certify_typ_syntax;
  1.1216 +val add_syntax = curry add_modesyntax Syntax.default_mode;
  1.1217 +val add_syntax_i = curry add_modesyntax_i Syntax.default_mode;
  1.1218 +val del_modesyntax = gen_syntax Syntax.remove_const_gram (read_typ_syntax o no_def_sort);
  1.1219 +val del_modesyntax_i = gen_syntax Syntax.remove_const_gram certify_typ_syntax;
  1.1220  
  1.1221 -fun err_in_const c =
  1.1222 -  error ("in declaration of constant " ^ quote c);
  1.1223 +
  1.1224 +(* add constants *)
  1.1225  
  1.1226  fun err_dup_consts cs =
  1.1227    error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
  1.1228  
  1.1229 -
  1.1230 -fun read_cnst sg syn tsig (naming, spaces) (c, ty_src, mx) =
  1.1231 -  (c, rd_raw_typ (make_syntax sg syn) tsig spaces (K NONE) ty_src, mx)
  1.1232 -    handle ERROR => err_in_const (const_name sg c mx);
  1.1233 -
  1.1234 -fun change_cnsts change_gram rd_const syn_only prmode sg (syn, tsig, ctab, (naming, spaces), data)
  1.1235 -    raw_consts =
  1.1236 +fun gen_add_consts prep_typ raw_args sg =
  1.1237    let
  1.1238 -    val prep_typ = compress_type o Type.varifyT o Type.no_tvars o
  1.1239 -     (if syn_only then Type.cert_typ_syntax tsig else Term.no_dummyT o Type.cert_typ tsig);
  1.1240 -    fun prep_const (c, ty, mx) = (c, prep_typ ty, mx) handle TYPE (msg, _, _) =>
  1.1241 -      (error_msg msg; err_in_const (const_name sg c mx));
  1.1242 -
  1.1243 -    val consts = map (prep_const o rd_const sg syn tsig (naming, spaces)) raw_consts;
  1.1244 -    val decls =
  1.1245 -      if syn_only then []
  1.1246 -      else decls_of sg Syntax.const_name consts;
  1.1247 +    val prepT = compress_type o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ sg;
  1.1248 +    fun prep (c, T, mx) = ((c, prepT T, mx) handle TYPE (msg, _, _) => error msg)
  1.1249 +      handle ERROR => error ("in declaration of constant " ^ quote (Syntax.const_name c mx));
  1.1250 +    val args = map prep raw_args;
  1.1251 +    val decls = args |> map (fn (c, T, mx) =>
  1.1252 +      (full_name sg (Syntax.const_name c mx), (T, stamp ())));
  1.1253    in
  1.1254 -    (map_syntax (change_gram (is_logtype sg) prmode consts) syn, tsig,
  1.1255 -      Symtab.extend (ctab, map (fn (c, T) => (c, (T, stamp ()))) decls)
  1.1256 -        handle Symtab.DUPS cs => err_dup_consts cs,
  1.1257 -      (naming, add_names sg constK (map fst decls) spaces), data)
  1.1258 +    sg |> map_sign (fn (syn, tsig, consts, spaces) =>
  1.1259 +      (syn, tsig,
  1.1260 +        Symtab.extend (consts, decls) handle Symtab.DUPS cs => err_dup_consts cs,
  1.1261 +        declare_names sg constK (map #1 decls) spaces))
  1.1262 +    |> add_syntax_i args
  1.1263    end;
  1.1264  
  1.1265 -fun ext_cnsts rd = change_cnsts Syntax.extend_const_gram rd;
  1.1266 -fun rem_cnsts rd = change_cnsts Syntax.remove_const_gram rd;
  1.1267 -
  1.1268 -fun ext_consts_i x = ext_cnsts no_read false Syntax.default_mode x;
  1.1269 -fun ext_consts x   = ext_cnsts read_cnst false Syntax.default_mode x;
  1.1270 -fun ext_syntax_i x = ext_cnsts no_read true Syntax.default_mode x;
  1.1271 -fun ext_syntax x   = ext_cnsts read_cnst true Syntax.default_mode x;
  1.1272 -
  1.1273 -fun ext_modesyntax_i x y (m, cs) = ext_cnsts no_read true m x y cs;
  1.1274 -fun ext_modesyntax x y (m, cs)   = ext_cnsts read_cnst true m x y cs;
  1.1275 -fun rem_modesyntax_i x y (m, cs) = rem_cnsts no_read true m x y cs;
  1.1276 -fun rem_modesyntax x y (m, cs)   = rem_cnsts read_cnst true m x y cs;
  1.1277 +val add_consts = gen_add_consts (read_typ o no_def_sort);
  1.1278 +val add_consts_i = gen_add_consts certify_typ;
  1.1279  
  1.1280  
  1.1281  (* add type classes *)
  1.1282  
  1.1283 -fun const_of_class c = c ^ "_class";
  1.1284 +val classN = "_class";
  1.1285  
  1.1286 -fun class_of_const c_class =
  1.1287 -  let
  1.1288 -    val c = implode (Library.take (size c_class - size "_class", explode c_class));
  1.1289 -  in
  1.1290 -    if const_of_class c = c_class then c
  1.1291 -    else raise TERM ("class_of_const: bad name " ^ quote c_class, [])
  1.1292 -  end;
  1.1293 -
  1.1294 +val const_of_class = suffix classN;
  1.1295 +fun class_of_const c = unsuffix classN c
  1.1296 +  handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
  1.1297  
  1.1298 -fun ext_classes int sg (syn, tsig, ctab, (naming, spaces), data) classes =
  1.1299 -  let
  1.1300 -    val names = map fst classes;
  1.1301 -    val consts =
  1.1302 -      map (fn c => (const_of_class c, a_itselfT --> propT, NoSyn)) names;
  1.1303 +fun gen_add_class int_class (bclass, raw_classes) sg =
  1.1304 +  sg |> map_sign (fn (syn, tsig, consts, spaces) =>
  1.1305 +    let
  1.1306 +      val class = full_name sg bclass;
  1.1307 +      val classes = map (int_class sg) raw_classes;
  1.1308 +      val syn' = map_syntax (Syntax.extend_consts [bclass]) syn;
  1.1309 +      val tsig' = Type.add_classes (pp sg) [(class, classes)] tsig;
  1.1310 +      val spaces' = declare_names sg classK [class] spaces;
  1.1311 +    in (syn', tsig', consts, spaces') end)
  1.1312 +  |> add_consts_i [(const_of_class bclass, a_itselfT --> propT, Syntax.NoSyn)];
  1.1313  
  1.1314 -    val full_names = map (full_name sg) names;
  1.1315 -    val spaces' = add_names sg classK full_names spaces;
  1.1316 -    val intrn = if int then map (intrn_class spaces') else I;
  1.1317 -    val classes' =
  1.1318 -      ListPair.map (fn (c, (_, cs)) => (c, intrn cs)) (full_names, classes);
  1.1319 -  in
  1.1320 -    ext_consts_i sg
  1.1321 -      (map_syntax (Syntax.extend_consts names) syn,
  1.1322 -        Type.add_classes (pp sg) classes' tsig, ctab, (naming, spaces'), data)
  1.1323 -    consts
  1.1324 -  end;
  1.1325 +val add_classes = fold (gen_add_class intern_class);
  1.1326 +val add_classes_i = fold (gen_add_class (K I));
  1.1327  
  1.1328  
  1.1329  (* add to classrel *)
  1.1330  
  1.1331 -fun ext_classrel int sg (syn, tsig, ctab, (naming, spaces), data) pairs =
  1.1332 -  let val intrn = if int then map (pairself (intrn_class spaces)) else I in
  1.1333 -    (syn, Type.add_classrel (pp sg) (intrn pairs) tsig, ctab, (naming, spaces), data)
  1.1334 -  end;
  1.1335 +fun gen_add_classrel int_class raw_pairs sg =
  1.1336 +  sg |> map_sign (fn (syn, tsig, consts, spaces) =>
  1.1337 +    let
  1.1338 +      val pairs = map (pairself (int_class sg)) raw_pairs;
  1.1339 +      val tsig' = Type.add_classrel (pp sg) pairs tsig;
  1.1340 +    in (syn, tsig', consts, spaces) end);
  1.1341 +
  1.1342 +val add_classrel = gen_add_classrel intern_class;
  1.1343 +val add_classrel_i = gen_add_classrel (K I);
  1.1344  
  1.1345  
  1.1346  (* add translation functions *)
  1.1347 @@ -1014,128 +1003,59 @@
  1.1348  
  1.1349  fun mk trs = map Syntax.mk_trfun trs;
  1.1350  
  1.1351 -fun ext_trfs ext non_typed sg (syn, tsig, ctab, names, data) (atrs, trs, tr's, atr's) =
  1.1352 +fun gen_add_trfuns ext non_typed (atrs, trs, tr's, atr's) sg = sg |> map_syn (fn syn =>
  1.1353    let val syn' = syn |> ext (mk atrs, mk trs, mk (map (apsnd non_typed) tr's), mk atr's)
  1.1354 -  in make_syntax sg syn'; (syn', tsig, ctab, names, data) end;
  1.1355 +  in make_syntax sg syn'; syn' end);
  1.1356  
  1.1357 -fun ext_trfsT ext sg (syn, tsig, ctab, names, data) tr's =
  1.1358 +fun gen_add_trfunsT ext tr's sg = sg |> map_syn (fn syn =>
  1.1359    let val syn' = syn |> ext ([], [], mk tr's, [])
  1.1360 -  in make_syntax sg syn'; (syn', tsig, ctab, names, data) end;
  1.1361 +  in make_syntax sg syn'; syn' end);
  1.1362  
  1.1363  in
  1.1364  
  1.1365 -fun ext_trfuns sg = ext_trfs (map_syntax o Syntax.extend_trfuns) Syntax.non_typed_tr' sg;
  1.1366 -fun ext_trfunsT sg = ext_trfsT (map_syntax o Syntax.extend_trfuns) sg;
  1.1367 -fun ext_advanced_trfuns sg = ext_trfs extend_trfuns Syntax.non_typed_tr'' sg;
  1.1368 -fun ext_advanced_trfunsT sg = ext_trfsT extend_trfuns sg;
  1.1369 +val add_trfuns = gen_add_trfuns (map_syntax o Syntax.extend_trfuns) Syntax.non_typed_tr';
  1.1370 +val add_trfunsT = gen_add_trfunsT (map_syntax o Syntax.extend_trfuns);
  1.1371 +val add_advanced_trfuns = gen_add_trfuns extend_trfuns Syntax.non_typed_tr'';
  1.1372 +val add_advanced_trfunsT = gen_add_trfunsT extend_trfuns;
  1.1373  
  1.1374  end;
  1.1375  
  1.1376 -
  1.1377 -(* add token translation functions *)
  1.1378 -
  1.1379 -fun ext_tokentrfuns sg (syn, tsig, ctab, names, data) args =
  1.1380 -  (map_syntax (Syntax.extend_tokentrfuns args) syn, tsig, ctab, names, data);
  1.1381 +val add_tokentrfuns = map_syn o map_syntax o Syntax.extend_tokentrfuns;
  1.1382  
  1.1383  
  1.1384  (* add translation rules *)
  1.1385  
  1.1386 -fun ext_trrules sg (syn, tsig, ctab, (naming, spaces), data) args =
  1.1387 -  (syn |> map_syntax (Syntax.extend_trrules (is_logtype sg) (make_syntax sg syn)
  1.1388 -      (map (Syntax.map_trrule (fn (root, str) => (intrn spaces typeK root, str))) args)),
  1.1389 -    tsig, ctab, (naming, spaces), data);
  1.1390 -
  1.1391 -fun ext_trrules_i _ (syn, tsig, ctab, names, data) args =
  1.1392 -  (syn |> map_syntax (Syntax.extend_trrules_i args), tsig, ctab, names, data);
  1.1393 -
  1.1394 -
  1.1395 -(* change naming *)
  1.1396 -
  1.1397 -fun change_naming f _ (syn, tsig, ctab, (naming, spaces), data) args =
  1.1398 -  (syn, tsig, ctab, (f args naming, spaces), data);
  1.1399 -
  1.1400 -
  1.1401 -(* change name space *)
  1.1402 +fun add_trrules args sg = sg |> map_syn (fn syn =>
  1.1403 +  let val rules = map (Syntax.map_trrule (apfst (intern_tycon sg))) args
  1.1404 +  in map_syntax (Syntax.extend_trrules (is_logtype sg) (make_syntax sg syn) rules) syn end);
  1.1405  
  1.1406 -fun ext_add_space sg (syn, tsig, ctab, (naming, spaces), data) (kind, names) =
  1.1407 -  (syn, tsig, ctab, (naming, add_names sg kind names spaces), data);
  1.1408 -
  1.1409 -fun ext_hide_space _ (syn, tsig, ctab, (naming, spaces), data) (b, (kind, xnames)) =
  1.1410 -  (syn, tsig, ctab, (naming, hide_names b kind (map (intrn spaces kind) xnames) spaces), data);
  1.1411 -
  1.1412 -fun ext_hide_space_i _ (syn, tsig, ctab, (naming, spaces), data) (b, (kind, names)) =
  1.1413 -  (syn, tsig, ctab, (naming, hide_names b kind names spaces), data);
  1.1414 -
  1.1415 -
  1.1416 -(* signature data *)
  1.1417 -
  1.1418 -fun ext_init_data sg (syn, tsig, ctab, names, data) (kind, (e, cp, ext, mrg, prt)) =
  1.1419 -  (syn, tsig, ctab, names, init_data_sg sg data kind e cp ext mrg prt);
  1.1420 -
  1.1421 -fun ext_put_data sg (syn, tsig, ctab, names, data) (kind, f, x) =
  1.1422 -  (syn, tsig, ctab, names, put_data_sg sg data kind f x);
  1.1423 +val add_trrules_i = map_syn o map_syntax o Syntax.extend_trrules_i;
  1.1424  
  1.1425  
  1.1426 -fun copy_data (k, (e, mths as (cp, _, _, _))) =
  1.1427 -  (k, (cp e handle exn => err_method "copy" (Object.name_of_kind k) exn, mths));
  1.1428 +(* modify naming *)
  1.1429  
  1.1430 -fun copy (sg as Sg ({id = _, stamps, syn}, {self, tsig, consts, naming, spaces, data})) =
  1.1431 -  let
  1.1432 -    val _ = check_stale sg;
  1.1433 -    val self' = SgRef (SOME (ref sg));
  1.1434 -    val Data tab = data;
  1.1435 -    val data' = Data (Symtab.map copy_data tab);
  1.1436 -  in create_sign self' stamps "#" (syn, tsig, consts, (naming, spaces), data') end;
  1.1437 +val add_path        = map_naming o NameSpace.add_path;
  1.1438 +val qualified_names = map_naming NameSpace.qualified_names;
  1.1439 +val no_base_names   = map_naming NameSpace.no_base_names;
  1.1440 +val custom_accesses = map_naming o NameSpace.custom_accesses;
  1.1441 +val set_policy      = map_naming o NameSpace.set_policy;
  1.1442 +val restore_naming  = map_naming o K o naming_of;
  1.1443  
  1.1444  
  1.1445 -(* the external interfaces *)
  1.1446 +(* hide names *)
  1.1447  
  1.1448 -val add_classes          = extend_sign true (ext_classes true) "#";
  1.1449 -val add_classes_i        = extend_sign true (ext_classes false) "#";
  1.1450 -val add_classrel         = extend_sign true (ext_classrel true) "#";
  1.1451 -val add_classrel_i       = extend_sign true (ext_classrel false) "#";
  1.1452 -val add_defsort          = extend_sign true ext_defsort "#";
  1.1453 -val add_defsort_i        = extend_sign true ext_defsort_i "#";
  1.1454 -val add_types            = extend_sign true ext_types "#";
  1.1455 -val add_nonterminals     = extend_sign true ext_nonterminals "#";
  1.1456 -val add_tyabbrs          = extend_sign true ext_tyabbrs "#";
  1.1457 -val add_tyabbrs_i        = extend_sign true ext_tyabbrs_i "#";
  1.1458 -val add_arities          = extend_sign true ext_arities "#";
  1.1459 -val add_arities_i        = extend_sign true ext_arities_i "#";
  1.1460 -val add_consts           = extend_sign true ext_consts "#";
  1.1461 -val add_consts_i         = extend_sign true ext_consts_i "#";
  1.1462 -val add_syntax           = extend_sign true ext_syntax "#";
  1.1463 -val add_syntax_i         = extend_sign true ext_syntax_i "#";
  1.1464 -val add_modesyntax       = extend_sign true ext_modesyntax "#";
  1.1465 -val add_modesyntax_i     = extend_sign true ext_modesyntax_i "#";
  1.1466 -val del_modesyntax       = extend_sign true rem_modesyntax "#";
  1.1467 -val del_modesyntax_i     = extend_sign true rem_modesyntax_i "#";
  1.1468 -val add_trfuns           = extend_sign true ext_trfuns "#";
  1.1469 -val add_trfunsT          = extend_sign true ext_trfunsT "#";
  1.1470 -val add_advanced_trfuns  = extend_sign true ext_advanced_trfuns "#";
  1.1471 -val add_advanced_trfunsT = extend_sign true ext_advanced_trfunsT "#";
  1.1472 -val add_tokentrfuns      = extend_sign true ext_tokentrfuns "#";
  1.1473 -val add_trrules          = extend_sign true ext_trrules "#";
  1.1474 -val add_trrules_i        = extend_sign true ext_trrules_i "#";
  1.1475 -val add_path             = extend_sign true (change_naming NameSpace.add_path) "#";
  1.1476 -val qualified_names      = extend_sign true (change_naming (K NameSpace.qualified_names)) "#" ();
  1.1477 -val no_base_names        = extend_sign true (change_naming (K NameSpace.no_base_names)) "#" ();
  1.1478 -val custom_accesses      = extend_sign true (change_naming NameSpace.custom_accesses) "#";
  1.1479 -val set_policy           = extend_sign true (change_naming NameSpace.set_policy) "#";
  1.1480 -val restore_naming       = extend_sign true (change_naming (K o naming_of)) "#";
  1.1481 -val add_space            = extend_sign true ext_add_space "#";
  1.1482 -val hide_space           = curry (extend_sign true ext_hide_space "#");
  1.1483 -val hide_space_i         = curry (extend_sign true ext_hide_space_i "#");
  1.1484 -val init_data            = extend_sign true ext_init_data "#";
  1.1485 -fun put_data k f x       = extend_sign true ext_put_data "#" (k, f, x);
  1.1486 -fun add_name name        = extend_sign true (K K) name ();
  1.1487 -val prep_ext             = extend_sign false (K K) "#" ();
  1.1488 +fun hide_space fully (kind, xnames) sg = sg |> map_sign (fn (syn, tsig, consts, spaces) =>
  1.1489 +  let
  1.1490 +    val names = map (intern sg kind) xnames;
  1.1491 +    val spaces' = hide_names kind fully names spaces;
  1.1492 +  in (syn, tsig, consts, spaces') end);
  1.1493 +
  1.1494 +fun hide_space_i fully (kind, names) = map_sign (fn (syn, tsig, consts, spaces) =>
  1.1495 +  (syn, tsig, consts, hide_names kind fully names spaces));
  1.1496  
  1.1497  
  1.1498  
  1.1499 -(** merge signatures **)        (*exception TERM*)
  1.1500 -
  1.1501 -(* merge_stamps *)
  1.1502 +(** merge signatures **)
  1.1503  
  1.1504  fun merge_stamps stamps1 stamps2 =
  1.1505    let val stamps = merge_lists' stamps1 stamps2 in
  1.1506 @@ -1145,30 +1065,21 @@
  1.1507    end;
  1.1508  
  1.1509  
  1.1510 -(*** trivial merge ***)
  1.1511 -
  1.1512 -(*For concise error messages: the last few components only*)
  1.1513 -fun abbrev_stamp_names_of sg = rev (List.take(map ! (stamps_of sg), 5));
  1.1514 -
  1.1515 -fun abbrev_str_of sg = 
  1.1516 -  let val sts = "..., " ^ commas (abbrev_stamp_names_of sg)
  1.1517 -          handle Subscript => commas (stamp_names_of sg)
  1.1518 -  in "{" ^ sts ^ "}" end;
  1.1519 +(* trivial merge *)
  1.1520  
  1.1521  fun merge_refs (sgr1 as SgRef (SOME (ref (sg1 as Sg ({stamps = s1, ...}, _)))),
  1.1522          sgr2 as SgRef (SOME (ref (sg2 as Sg ({stamps = s2, ...}, _))))) =
  1.1523        if subsig (sg2, sg1) then sgr1
  1.1524        else if subsig (sg1, sg2) then sgr2
  1.1525 -      else (merge_stamps s1 s2; (*check for different versions*)
  1.1526 -            error ("Attempt to do non-trivial merge of signatures\n" ^ 
  1.1527 -                   abbrev_str_of sg1 ^ "\n" ^ 
  1.1528 -                   abbrev_str_of sg2 ^ "\n"))
  1.1529 +      else (merge_stamps s1 s2;  (*check for different versions*)
  1.1530 +        error ("Attempt to do non-trivial merge of signature\n" ^
  1.1531 +          str_of_sg sg1 ^ " and " ^ str_of_sg sg2))
  1.1532    | merge_refs _ = sys_error "Sign.merge_refs";
  1.1533  
  1.1534  val merge = deref o merge_refs o pairself self_ref;
  1.1535  
  1.1536  
  1.1537 -(* merge_list *)              (*exception TERM/ERROR*)
  1.1538 +(* non-trivial merge *)              (*exception TERM/ERROR*)
  1.1539  
  1.1540  local
  1.1541  
  1.1542 @@ -1190,27 +1101,20 @@
  1.1543        val stamps = merge_stamps stamps1 stamps2;
  1.1544        val syntax = Syntax.merge_syntaxes syntax1 syntax2;
  1.1545        val trfuns = merge_trfuns trfuns1 trfuns2;
  1.1546 +      val syn = Syn (syntax, trfuns);
  1.1547        val consts = Symtab.merge eq_snd (consts1, consts2)
  1.1548          handle Symtab.DUPS cs => err_dup_consts cs;
  1.1549 -
  1.1550        val naming = NameSpace.default_naming;
  1.1551 -      val kinds = distinct (map fst (spaces1 @ spaces2));
  1.1552 -      val spaces =
  1.1553 -        kinds ~~
  1.1554 -          ListPair.map NameSpace.merge
  1.1555 -            (map (get_space spaces1) kinds, map (get_space spaces2) kinds);
  1.1556 -
  1.1557 +      val spaces = merge_spaces (spaces1, spaces2);
  1.1558        val data = merge_data (data1, data2);
  1.1559  
  1.1560 -      val pre_sign = make_sign (ref "", SgRef (SOME (ref dummy_sg)),
  1.1561 -        tsig1, consts, Syn (syntax, trfuns), naming, spaces, data, ref "#" :: stamps1);
  1.1562 -      val tsig = Type.merge_tsigs (pp pre_sign) (tsig1, tsig2);
  1.1563 +      val pre_sg = make_sg (ref "", SgRef (SOME (ref dummy_sg)), ref "#" :: stamps1)
  1.1564 +        naming data (syn, tsig1, consts, spaces);
  1.1565 +      val tsig = Type.merge_tsigs (pp pre_sg) (tsig1, tsig2);
  1.1566  
  1.1567 -      val self_ref = ref dummy_sg;
  1.1568 -      val self = SgRef (SOME self_ref);
  1.1569 -      val sign = make_sign (ref "", self, tsig, consts, Syn (syntax, trfuns),
  1.1570 -        naming, spaces, data, stamps);
  1.1571 -    in self_ref := sign; syn_of sign; sign end;
  1.1572 +      val self = SgRef (SOME (ref dummy_sg));
  1.1573 +      val sg = make_sg (ref "", self, stamps) naming data (syn, tsig, consts, spaces);
  1.1574 +    in assign self sg; syn_of sg; sg end;
  1.1575  
  1.1576  in
  1.1577