src/Pure/sign.ML
author wenzelm
Thu Jun 09 12:03:24 2005 +0200 (2005-06-09)
changeset 16337 5734de2f7ace
parent 16288 df2b550a17f6
child 16354 6f0ca9628840
permissions -rw-r--r--
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;
     1 (*  Title:      Pure/sign.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson and Markus Wenzel
     4 
     5 The abstract type "sg" of signatures.
     6 *)
     7 
     8 signature SIGN =
     9 sig
    10   type sg
    11   type sg_ref
    12   type data
    13   val rep_sg: sg ->
    14    {self: sg_ref,
    15     tsig: Type.tsig,
    16     consts: (typ * stamp) Symtab.table,
    17     naming: NameSpace.naming,
    18     spaces: {class: NameSpace.T, tycon: NameSpace.T, const: NameSpace.T},
    19     data: data}
    20   val stamp_names_of: sg -> string list
    21   val exists_stamp: string -> sg -> bool
    22   val pretty_sg: sg -> Pretty.T
    23   val pprint_sg: sg -> pprint_args -> unit
    24   val pretty_abbrev_sg: sg -> Pretty.T
    25   val str_of_sg: sg -> string
    26   val is_stale: sg -> bool
    27   val self_ref: sg -> sg_ref
    28   val deref: sg_ref -> sg
    29   val name_of: sg -> string
    30   val is_draft: sg -> bool
    31   val eq_sg: sg * sg -> bool
    32   val subsig: sg * sg -> bool
    33   val same_sg: sg * sg -> bool
    34   val joinable: sg * sg -> bool
    35   val prep_ext: sg -> sg
    36   val copy: sg -> sg
    37   val add_name: string -> sg -> sg
    38   val data_kinds: data -> string list
    39   val print_all_data: sg -> unit
    40   val pre_pure: sg
    41   val PureN: string
    42   val CPureN: string
    43   val naming_of: sg -> NameSpace.naming
    44   val base_name: string -> bstring
    45   val full_name: sg -> bstring -> string
    46   val full_name_path: sg -> string -> bstring -> string
    47   val declare_name: sg -> string -> NameSpace.T -> NameSpace.T
    48   val syn_of: sg -> Syntax.syntax
    49   val tsig_of: sg -> Type.tsig
    50   val classes: sg -> class list
    51   val defaultS: sg -> sort
    52   val subsort: sg -> sort * sort -> bool
    53   val of_sort: sg -> typ * sort -> bool
    54   val witness_sorts: sg -> sort list -> sort list -> (typ * sort) list
    55   val universal_witness: sg -> (typ * sort) option
    56   val typ_instance: sg -> typ * typ -> bool
    57   val is_logtype: sg -> string -> bool
    58   val const_type: sg -> string -> typ option
    59   val the_const_type: sg -> string -> typ
    60   val declared_tyname: sg -> string -> bool
    61   val declared_const: sg -> string -> bool
    62   val classK: string
    63   val typeK: string
    64   val constK: string
    65   val intern: sg -> string -> xstring -> string
    66   val extern: sg -> string -> string -> xstring
    67   val extern_table: sg -> string -> 'a Symtab.table -> (xstring * 'a) list
    68   val intern_class: sg -> xstring -> string
    69   val extern_class: sg -> string -> xstring
    70   val intern_tycon: sg -> xstring -> string
    71   val extern_tycon: sg -> string -> xstring
    72   val intern_const: sg -> xstring -> string
    73   val extern_const: sg -> string -> xstring
    74   val intern_sort: sg -> sort -> sort
    75   val extern_sort: sg -> sort -> sort
    76   val intern_typ: sg -> typ -> typ
    77   val extern_typ: sg -> typ -> typ
    78   val intern_term: sg -> term -> term
    79   val extern_term: sg -> term -> term
    80   val intern_tycons: sg -> typ -> typ
    81   val pretty_term': Syntax.syntax -> sg -> term -> Pretty.T
    82   val pretty_term: sg -> term -> Pretty.T
    83   val pretty_typ: sg -> typ -> Pretty.T
    84   val pretty_sort: sg -> sort -> Pretty.T
    85   val pretty_classrel: sg -> class list -> Pretty.T
    86   val pretty_arity: sg -> arity -> Pretty.T
    87   val string_of_term: sg -> term -> string
    88   val string_of_typ: sg -> typ -> string
    89   val string_of_sort: sg -> sort -> string
    90   val string_of_classrel: sg -> class list -> string
    91   val string_of_arity: sg -> arity -> string
    92   val pprint_term: sg -> term -> pprint_args -> unit
    93   val pprint_typ: sg -> typ -> pprint_args -> unit
    94   val pp: sg -> Pretty.pp
    95   val certify_class: sg -> class -> class
    96   val certify_sort: sg -> sort -> sort
    97   val certify_typ: sg -> typ -> typ
    98   val certify_typ_syntax: sg -> typ -> typ
    99   val certify_typ_abbrev: sg -> typ -> typ
   100   val certify_term: Pretty.pp -> sg -> term -> term * typ * int
   101   val read_sort': Syntax.syntax -> sg -> string -> sort
   102   val read_sort: sg -> string -> sort
   103   val read_typ': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   104   val read_typ_syntax': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   105   val read_typ_abbrev': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
   106   val read_typ: sg * (indexname -> sort option) -> string -> typ
   107   val read_typ_syntax: sg * (indexname -> sort option) -> string -> typ
   108   val read_typ_abbrev: sg * (indexname -> sort option) -> string -> typ
   109   val read_tyname: sg -> string -> typ        (*exception TYPE*)
   110   val read_const: sg -> string -> term        (*exception TYPE*)
   111   val infer_types_simult: Pretty.pp -> sg -> (indexname -> typ option) ->
   112     (indexname -> sort option) -> string list -> bool
   113     -> (term list * typ) list -> term list * (indexname * typ) list
   114   val infer_types: Pretty.pp -> sg -> (indexname -> typ option) ->
   115     (indexname -> sort option) -> string list -> bool
   116     -> term list * typ -> term * (indexname * typ) list
   117   val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax ->
   118     sg * (indexname -> typ option) * (indexname -> sort option) ->
   119     string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
   120   val read_def_terms:
   121     sg * (indexname -> typ option) * (indexname -> sort option) ->
   122     string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
   123   val simple_read_term: sg -> typ -> string -> term
   124   val add_defsort: string -> sg -> sg
   125   val add_defsort_i: sort -> sg -> sg
   126   val add_types: (bstring * int * mixfix) list -> sg -> sg
   127   val add_nonterminals: bstring list -> sg -> sg
   128   val add_tyabbrs: (bstring * string list * string * mixfix) list -> sg -> sg
   129   val add_tyabbrs_i: (bstring * string list * typ * mixfix) list -> sg -> sg
   130   val add_arities: (xstring * string list * string) list -> sg -> sg
   131   val add_arities_i: (string * sort list * sort) list -> sg -> sg
   132   val add_syntax: (bstring * string * mixfix) list -> sg -> sg
   133   val add_syntax_i: (bstring * typ * mixfix) list -> sg -> sg
   134   val add_modesyntax: (string * bool) * (bstring * string * mixfix) list -> sg -> sg
   135   val add_modesyntax_i: (string * bool) * (bstring * typ * mixfix) list -> sg -> sg
   136   val del_modesyntax: (string * bool) * (bstring * string * mixfix) list -> sg -> sg
   137   val del_modesyntax_i: (string * bool) * (bstring * typ * mixfix) list -> sg -> sg
   138   val add_consts: (bstring * string * mixfix) list -> sg -> sg
   139   val add_consts_i: (bstring * typ * mixfix) list -> sg -> sg
   140   val const_of_class: class -> string
   141   val class_of_const: string -> class
   142   val add_classes: (bstring * xstring list) list -> sg -> sg
   143   val add_classes_i: (bstring * class list) list -> sg -> sg
   144   val add_classrel: (xstring * xstring) list -> sg -> sg
   145   val add_classrel_i: (class * class) list -> sg -> sg
   146   val add_trfuns:
   147     (string * (ast list -> ast)) list *
   148     (string * (term list -> term)) list *
   149     (string * (term list -> term)) list *
   150     (string * (ast list -> ast)) list -> sg -> sg
   151   val add_trfunsT:
   152     (string * (bool -> typ -> term list -> term)) list -> sg -> sg
   153   val add_advanced_trfuns:
   154     (string * (sg -> ast list -> ast)) list *
   155     (string * (sg -> term list -> term)) list *
   156     (string * (sg -> term list -> term)) list *
   157     (string * (sg -> ast list -> ast)) list -> sg -> sg
   158   val add_advanced_trfunsT:
   159     (string * (sg -> bool -> typ -> term list -> term)) list -> sg -> sg
   160   val add_tokentrfuns:
   161     (string * string * (string -> string * real)) list -> sg -> sg
   162   val add_trrules: (xstring * string) Syntax.trrule list -> sg -> sg
   163   val add_trrules_i: ast Syntax.trrule list -> sg -> sg
   164   val add_path: string -> sg -> sg
   165   val qualified_names: sg -> sg
   166   val no_base_names: sg -> sg
   167   val custom_accesses: (string list -> string list list) -> sg -> sg
   168   val set_policy: (string -> bstring -> string) * (string list -> string list list) -> sg -> sg
   169   val restore_naming: sg -> sg -> sg
   170   val hide_space: bool -> string * string list -> sg -> sg
   171   val hide_space_i: bool -> string * string list -> sg -> sg
   172   val merge_refs: sg_ref * sg_ref -> sg_ref
   173   val merge: sg * sg -> sg
   174   val prep_ext_merge: sg list -> sg
   175 end;
   176 
   177 signature PRIVATE_SIGN =
   178 sig
   179   include SIGN
   180   val init_data: Object.kind * (Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
   181     (Object.T * Object.T -> Object.T) * (sg -> Object.T -> unit)) -> sg -> sg
   182   val get_data: Object.kind -> (Object.T -> 'a) -> sg -> 'a
   183   val put_data: Object.kind -> ('a -> Object.T) -> 'a -> sg -> sg
   184   val print_data: Object.kind -> sg -> unit
   185 end;
   186 
   187 structure Sign: PRIVATE_SIGN =
   188 struct
   189 
   190 (** datatype sg **)
   191 
   192 (* types sg, data, syn, sg_ref *)
   193 
   194 datatype sg =
   195   Sg of
   196    {id: string ref,
   197     stamps: string ref list,                      (*unique theory indentifier*)
   198     syn: syn} *                                   (*syntax for parsing and printing*)
   199    {self: sg_ref,                                 (*mutable self reference*)
   200     tsig: Type.tsig,                              (*order-sorted signature of types*)
   201     consts: (typ * stamp) Symtab.table,           (*type schemes of constants*)
   202     naming: NameSpace.naming,
   203     spaces: {class: NameSpace.T, tycon: NameSpace.T, const: NameSpace.T},
   204     data: data}
   205 and data =
   206   Data of
   207     (Object.kind *                                (*kind (for authorization)*)
   208       (Object.T *                                 (*value*)
   209         ((Object.T -> Object.T) *                 (*copy method*)
   210           (Object.T -> Object.T) *                (*prepare extend method*)
   211           (Object.T * Object.T -> Object.T) *     (*merge and prepare extend method*)
   212           (sg -> Object.T -> unit))))             (*print method*)
   213     Symtab.table
   214 and syn =
   215   Syn of
   216     Syntax.syntax *
   217      (((sg -> ast list -> ast) * stamp) Symtab.table *
   218       ((sg -> term list -> term) * stamp) Symtab.table *
   219       ((sg -> bool -> typ -> term list -> term) * stamp) list Symtab.table *
   220       ((sg -> ast list -> ast) * stamp) list Symtab.table)
   221 and sg_ref =
   222   SgRef of sg ref option;
   223 
   224 (* FIXME assign!??? *)
   225 fun make_sg (id, self, stamps) naming data (syn, tsig, consts, spaces) =
   226   Sg ({id = id, stamps = stamps, syn = syn}, {self = self, tsig = tsig,
   227     consts = consts, naming = naming, spaces = spaces, data = data});
   228 
   229 fun rep_sg (Sg (_, args)) = args;
   230 
   231 
   232 (* stamps *)
   233 
   234 fun stamps_of (Sg ({stamps, ...}, _)) = stamps;
   235 val stamp_names_of = rev o map ! o stamps_of;
   236 fun exists_stamp name = exists (equal name o !) o stamps_of;
   237 
   238 fun pretty_sg sg = Pretty.str_list "{" "}" (stamp_names_of sg);
   239 val pprint_sg = Pretty.pprint o pretty_sg;
   240 
   241 fun pretty_abbrev_sg sg =
   242   let
   243     val stamps = map ! (stamps_of sg);
   244     val abbrev = if length stamps > 5 then "..." :: rev (List.take (stamps, 5)) else rev stamps;
   245   in Pretty.str_list "{" "}" abbrev end;
   246 
   247 val str_of_sg = Pretty.str_of o pretty_abbrev_sg;
   248 
   249 
   250 (* id and self *)
   251 
   252 fun check_stale pos (sg as Sg ({id, ...},
   253         {self = SgRef (SOME (ref (Sg ({id = id', ...}, _)))), ...})) =
   254       if id = id' then sg
   255       else raise TERM ("Stale signature (in " ^ pos ^ "): " ^ str_of_sg sg, [])
   256   | check_stale _ _ = sys_error "Sign.check_stale";
   257 
   258 val is_stale = not o can (check_stale "Sign.is_stale");
   259 
   260 fun self_ref (sg as Sg (_, {self, ...})) = (check_stale "Sign.self_ref" sg; self);
   261 
   262 fun deref (SgRef (SOME (ref sg))) = sg
   263   | deref (SgRef NONE) = sys_error "Sign.deref";
   264 
   265 fun assign (SgRef (SOME r)) sg = r := sg
   266   | assign (SgRef NONE) _ = sys_error "Sign.assign";
   267 
   268 fun name_of (sg as Sg ({id = ref name, ...}, _)) =
   269   if name = "" orelse ord name = ord "#" then
   270     raise TERM ("Nameless signature " ^ str_of_sg sg, [])
   271   else name;
   272 
   273 fun is_draft (Sg ({stamps = ref name :: _, ...}, _)) =
   274       name = "" orelse ord name = ord "#"
   275   | is_draft _ = sys_error "Sign.is_draft";
   276 
   277 
   278 (* inclusion and equality *)
   279 
   280 local
   281   (*avoiding polymorphic equality: factor 10 speedup*)
   282   fun mem_stamp (_: string ref, []) = false
   283     | mem_stamp (x, y :: ys) = x = y orelse mem_stamp (x, ys);
   284 
   285   fun subset_stamp ([], ys) = true
   286     | subset_stamp (x :: xs, ys) =
   287         mem_stamp (x, ys) andalso subset_stamp (xs, ys);
   288 in
   289   fun eq_sg (sg1 as Sg ({id = id1, ...}, _), sg2 as Sg ({id = id2, ...}, _)) =
   290     (check_stale "Sign.eq_sg" sg1; check_stale "Sign.eq_sg" sg2; id1 = id2);
   291 
   292   fun subsig (sg1, sg2) =
   293     eq_sg (sg1, sg2) orelse mem_stamp (hd (stamps_of sg1), stamps_of sg2);
   294 
   295   fun subsig_internal (sg1, sg2) =
   296     eq_sg (sg1, sg2) orelse subset_stamp (stamps_of sg1, stamps_of sg2);
   297 end;
   298 
   299 
   300 fun joinable (sg1, sg2) = subsig (sg1, sg2) orelse subsig (sg2, sg1);
   301 
   302 (*test if same theory names are contained in signatures' stamps,
   303   i.e. if signatures belong to same theory but not necessarily to the
   304   same version of it*)
   305 fun same_sg (sg1, sg2) =
   306   eq_sg (sg1, sg2) orelse eq_set_string (pairself (map ! o stamps_of) (sg1, sg2));
   307 
   308 
   309 (* data operations *)
   310 
   311 fun err_method name kind e =    (* FIXME wrap exn msg!? *)
   312   (warning ("Error while invoking " ^ quote kind ^ " " ^ name ^ " method"); raise e);
   313 
   314 fun err_inconsistent kinds =
   315   error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " data");
   316 
   317 val empty_data = Data Symtab.empty;
   318 
   319 fun merge_data (Data tab1, Data tab2) =
   320   let
   321     val data1 = map snd (Symtab.dest tab1);
   322     val data2 = map snd (Symtab.dest tab2);
   323     val all_data = data1 @ data2;
   324     val kinds = gen_distinct Object.eq_kind (map fst all_data);
   325 
   326    fun entry data kind =
   327      (case gen_assoc Object.eq_kind (data, kind) of
   328        NONE => []
   329      | SOME x => [(kind, x)]);
   330 
   331     fun merge_entries [(kind, (e, mths as (_, ext, _, _)))] =
   332           (kind, (ext e handle exn => err_method "prep_ext" (Object.name_of_kind kind) exn, mths))
   333       | merge_entries [(kind, (e1, mths as (_, _, mrg, _))), (_, (e2, _))] =
   334           (kind, (mrg (e1, e2)
   335             handle exn => err_method "merge" (Object.name_of_kind kind) exn, mths))
   336       | merge_entries _ = sys_error "merge_entries";
   337 
   338     val data = map (fn k => merge_entries (entry data1 k @ entry data2 k)) kinds;
   339     val data_idx = map (fn (k, x) => (Object.name_of_kind k, (k, x))) data;
   340   in
   341     Data (Symtab.make data_idx)
   342       handle Symtab.DUPS dups => err_inconsistent dups
   343   end;
   344 
   345 fun prep_ext_data data = merge_data (data, empty_data);
   346 
   347 fun copy_data (Data tab) =
   348   let
   349     fun cp_data (k, (e, mths as (cp, _, _, _))) =
   350       (k, (cp e handle exn => err_method "copy" (Object.name_of_kind k) exn, mths));
   351   in Data (Symtab.map cp_data tab) end;
   352 
   353 
   354 
   355 (** build signatures **)
   356 
   357 fun create_sg name self stamps naming data sign =
   358   let
   359     val id = ref name;
   360     val stamps' = (case stamps of ref "#" :: ss => ss | ss => ss);
   361     val _ = conditional (exists (equal name o !) stamps')
   362       (fn () => error ("Theory already contains a " ^ quote name ^ " component"));
   363     val sg = make_sg (id, self, id :: stamps') naming data sign;
   364   in assign self sg; sg end;
   365 
   366 fun new_sg f (sg as Sg ({stamps, syn, ...}, {self = _, tsig, consts, naming, spaces, data})) =
   367   let
   368     val _ = check_stale "Sign.new_sg" sg;
   369     val self' = SgRef (SOME (ref sg));
   370     val data' = f data;
   371   in create_sg "#" self' stamps naming data' (syn, tsig, consts, spaces) end;
   372 
   373 val prep_ext = new_sg prep_ext_data;
   374 val copy = new_sg copy_data;
   375 
   376 fun add_name name (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, spaces, data})) =
   377  (check_stale "Sign.add_name" sg;
   378   create_sg name self stamps naming data (syn, tsig, consts, spaces));
   379 
   380 fun map_sg f (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, spaces, data})) =
   381   let
   382     val _ = check_stale "Sign.map_sg" sg;
   383     val (naming', data', sign') = f (naming, data, (syn, tsig, consts, spaces));
   384   in create_sg "#" self stamps naming' data' sign' end;
   385 
   386 fun map_naming f = map_sg (fn (naming, data, sign) => (f naming, data, sign));
   387 fun map_data f = map_sg (fn (naming, data, sign) => (naming, f data, sign));
   388 fun map_sign f = map_sg (fn (naming, data, sign) => (naming, data, f sign));
   389 fun map_syn f = map_sign (fn (syn, tsig, consts, spaces) => (f syn, tsig, consts, spaces));
   390 
   391 
   392 
   393 (** signature data **)
   394 
   395 (* errors *)
   396 
   397 fun of_theory sg = "\nof theory " ^ str_of_sg sg;
   398 
   399 fun err_dup_init sg kind =
   400   error ("Duplicate initialization of " ^ quote kind ^ " data" ^ of_theory sg);
   401 
   402 fun err_uninit sg kind =
   403   error ("Tried to access uninitialized " ^ quote kind ^ " data" ^ of_theory sg);
   404 
   405 fun err_access sg kind =
   406   error ("Unauthorized access to " ^ quote kind ^ " data" ^ of_theory sg);
   407 
   408 
   409 (* access data *)
   410 
   411 fun data_kinds (Data tab) = Symtab.keys tab;
   412 
   413 fun lookup_data sg tab kind =
   414   let val name = Object.name_of_kind kind in
   415     (case Symtab.lookup (tab, name) of
   416       SOME (k, x) =>
   417         if Object.eq_kind (kind, k) then x
   418         else err_access sg name
   419     | NONE => err_uninit sg name)
   420   end;
   421 
   422 fun init_data (kind, (e, cp, ext, mrg, prt)) sg = sg |> map_data (fn Data tab =>
   423   Data (Symtab.update_new ((Object.name_of_kind kind, (kind, (e, (cp, ext, mrg, prt)))), tab))
   424     handle Symtab.DUP name => err_dup_init sg name);
   425 
   426 fun get_data kind dest (sg as Sg (_, {data = Data tab, ...})) =
   427   let val x = fst (lookup_data sg tab kind)
   428   in dest x handle Match => Object.kind_error kind end;
   429 
   430 fun put_data kind mk x sg = sg |> map_data (fn Data tab =>
   431   Data (Symtab.update ((Object.name_of_kind kind,
   432     (kind, (mk x, snd (lookup_data sg tab kind)))), tab)));
   433 
   434 fun print_data kind (sg as Sg (_, {data = Data tab, ...})) =
   435   let val (e, (_, _, _, prt)) = lookup_data sg tab kind in
   436     prt sg e handle exn =>
   437       err_method ("print" ^ of_theory sg) (Object.name_of_kind kind) exn
   438   end;
   439 
   440 fun print_all_data (sg as Sg (_, {data = Data tab, ...})) =
   441   List.app (fn kind => print_data kind sg) (map (#1 o #2) (Symtab.dest tab));
   442 
   443 
   444 
   445 (** primitive signatures **)
   446 
   447 val empty_spaces =
   448   {class = NameSpace.empty, tycon = NameSpace.empty, const = NameSpace.empty};
   449 
   450 fun merge_spaces
   451   ({class = class1, tycon = tycon1, const = const1},
   452     {class = class2, tycon = tycon2, const = const2}) =
   453   {class = NameSpace.merge (class1, class2),
   454    tycon = NameSpace.merge (tycon1, tycon2),
   455    const = NameSpace.merge (const1, const2)};
   456 
   457 val pure_syn =
   458   Syn (Syntax.pure_syn, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
   459 
   460 val dummy_sg = make_sg (ref "", SgRef NONE, []) NameSpace.default_naming empty_data
   461   (pure_syn, Type.empty_tsig, Symtab.empty, empty_spaces);
   462 
   463 val pre_pure =
   464   create_sg "#" (SgRef (SOME (ref dummy_sg))) [] NameSpace.default_naming empty_data
   465     (pure_syn, Type.empty_tsig, Symtab.empty, empty_spaces);
   466 
   467 val PureN = "Pure";
   468 val CPureN = "CPure";
   469 
   470 
   471 
   472 (** signature content **)
   473 
   474 (* naming *)
   475 
   476 fun naming_of (Sg (_, {naming, ...})) = naming;
   477 
   478 val base_name = NameSpace.base;
   479 val full_name = NameSpace.full o naming_of;
   480 fun full_name_path sg elems = NameSpace.full (NameSpace.add_path elems (naming_of sg));
   481 val declare_name = NameSpace.declare o naming_of;
   482 
   483 
   484 (* syntax *)
   485 
   486 fun map_syntax f (Syn (syntax, trfuns)) = Syn (f syntax, trfuns);
   487 
   488 fun make_syntax sg (Syn (syntax, (atrs, trs, tr's, atr's))) =
   489   let
   490     fun apply (c, (f, s)) = (c, (f sg, s));
   491     fun prep tab = map apply (Symtab.dest tab);
   492     fun prep' tab = map apply (Symtab.dest_multi tab);
   493   in syntax |> Syntax.extend_trfuns (prep atrs, prep trs, prep' tr's, prep' atr's) end;
   494 
   495 fun syn_of (sg as Sg ({syn, ...}, _)) = make_syntax sg syn;
   496 
   497 
   498 (* advanced translation functions *)
   499 
   500 fun extend_trfuns (atrs, trs, tr's, atr's)
   501     (Syn (syn, (parse_ast_trtab, parse_trtab, print_trtab, print_ast_trtab))) =
   502   Syn (syn, (Syntax.extend_trtab "parse ast translation" atrs parse_ast_trtab,
   503     Syntax.extend_trtab "parse translation" trs parse_trtab,
   504     Syntax.extend_tr'tab tr's print_trtab,
   505     Syntax.extend_tr'tab atr's print_ast_trtab));
   506 
   507 fun merge_trfuns
   508     (parse_ast_trtab1, parse_trtab1, print_trtab1, print_ast_trtab1)
   509     (parse_ast_trtab2, parse_trtab2, print_trtab2, print_ast_trtab2) =
   510   (Syntax.merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
   511     Syntax.merge_trtabs "parse translation" parse_trtab1 parse_trtab2,
   512     Syntax.merge_tr'tabs print_trtab1 print_trtab2,
   513     Syntax.merge_tr'tabs print_ast_trtab1 print_ast_trtab2);
   514 
   515 
   516 (* type signature *)
   517 
   518 val tsig_of = #tsig o rep_sg;
   519 
   520 val classes = Type.classes o tsig_of;
   521 val defaultS = Type.defaultS o tsig_of;
   522 val subsort = Type.subsort o tsig_of;
   523 val of_sort = Type.of_sort o tsig_of;
   524 val witness_sorts = Type.witness_sorts o tsig_of;
   525 val universal_witness = Type.universal_witness o tsig_of;
   526 val typ_instance = Type.typ_instance o tsig_of;
   527 fun is_logtype sg c = c mem_string Type.logical_types (tsig_of sg);
   528 
   529 
   530 (* consts signature *)
   531 
   532 fun const_type (Sg (_, {consts, ...})) c = Option.map #1 (Symtab.lookup (consts, c));
   533 
   534 fun the_const_type sg c =
   535   (case const_type sg c of SOME T => T
   536   | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
   537 
   538 fun declared_tyname sg c = is_some (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c));
   539 fun declared_const sg c = is_some (const_type sg c);
   540 
   541 
   542 (* name spaces *)
   543 
   544 val classK = "class";
   545 val typeK = "type";
   546 val constK = "const";
   547 
   548 fun illegal_space kind = "Illegal signature name space: " ^ quote kind;
   549 
   550 fun space_of sg kind = #spaces (rep_sg sg) |>
   551  (if kind = classK then #class
   552   else if kind = typeK then #tycon
   553   else if kind = constK then #const
   554   else raise TERM (illegal_space kind, []));
   555 
   556 fun map_space kind f {class, tycon, const} =
   557   let
   558     val (class', tycon', const') =
   559       if kind = classK then (f class, tycon, const)
   560       else if kind = typeK then (class, f tycon, const)
   561       else if kind = constK then (class, tycon, f const)
   562       else raise TERM (illegal_space kind, []);
   563   in {class = class', tycon = tycon', const = const'} end;
   564 
   565 fun declare_names sg kind = map_space kind o fold (declare_name sg);
   566 fun hide_names kind = map_space kind oo (fold o NameSpace.hide);
   567 
   568 
   569 
   570 (** intern / extern names **)
   571 
   572 val intern = NameSpace.intern oo space_of;
   573 val extern = NameSpace.extern oo space_of;
   574 fun extern_table sg = curry NameSpace.extern_table o space_of sg;
   575 
   576 fun intern_class sg = intern sg classK;
   577 fun extern_class sg = extern sg classK;
   578 fun intern_tycon sg = intern sg typeK;
   579 fun extern_tycon sg = extern sg typeK;
   580 fun intern_const sg = intern sg constK;
   581 fun extern_const sg = extern sg constK;
   582 
   583 val intern_sort = map o intern_class;
   584 val extern_sort = map o extern_class;
   585 
   586 local
   587 
   588 fun mapping add_names f t =
   589   let
   590     fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end;
   591     val tab = List.mapPartial f' (add_names (t, []));
   592     fun get x = if_none (assoc_string (tab, x)) x;
   593   in get end;
   594 
   595 fun typ_mapping f g sg T =
   596   T |> Term.map_typ
   597     (mapping add_typ_classes (f sg) T)
   598     (mapping add_typ_tycons (g sg) T);
   599 
   600 fun term_mapping f g h sg t =
   601   t |> Term.map_term
   602     (mapping add_term_classes (f sg) t)
   603     (mapping add_term_tycons (g sg) t)
   604     (mapping add_term_consts (h sg) t);
   605 
   606 in
   607 
   608 val intern_typ = typ_mapping intern_class intern_tycon;
   609 val extern_typ = typ_mapping extern_class extern_tycon;
   610 val intern_term = term_mapping intern_class intern_tycon intern_const;
   611 val extern_term = term_mapping extern_class extern_tycon extern_const;
   612 val intern_tycons = typ_mapping (K I) intern_tycon;
   613 
   614 end;
   615 
   616 
   617 
   618 (** pretty printing of terms, types etc. **)
   619 
   620 fun pretty_term' syn sg t = Syntax.pretty_term syn (exists_stamp CPureN sg) (extern_term sg t);
   621 fun pretty_term sg t = pretty_term' (syn_of sg) sg t;
   622 fun pretty_typ sg T = Syntax.pretty_typ (syn_of sg) (extern_typ sg T);
   623 fun pretty_sort sg S = Syntax.pretty_sort (syn_of sg) (extern_sort sg S);
   624 
   625 fun pretty_classrel sg cs = Pretty.block (List.concat
   626   (separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort sg o single) cs)));
   627 
   628 fun pretty_arity sg (a, Ss, S) =
   629   let
   630     val a' = extern_tycon sg a;
   631     val dom =
   632       if null Ss then []
   633       else [Pretty.list "(" ")" (map (pretty_sort sg) Ss), Pretty.brk 1];
   634   in Pretty.block ([Pretty.str (a' ^ " ::"), Pretty.brk 1] @ dom @ [pretty_sort sg S]) end;
   635 
   636 val string_of_term = Pretty.string_of oo pretty_term;
   637 val string_of_typ = Pretty.string_of oo pretty_typ;
   638 val string_of_sort = Pretty.string_of oo pretty_sort;
   639 val string_of_classrel = Pretty.string_of oo pretty_classrel;
   640 val string_of_arity = Pretty.string_of oo pretty_arity;
   641 
   642 val pprint_term = (Pretty.pprint o Pretty.quote) oo pretty_term;
   643 val pprint_typ = (Pretty.pprint o Pretty.quote) oo pretty_typ;
   644 
   645 fun pp sg = Pretty.pp (pretty_term sg, pretty_typ sg, pretty_sort sg,
   646   pretty_classrel sg, pretty_arity sg);
   647 
   648 
   649 
   650 (** certify entities **)    (*exception TYPE*)
   651 
   652 (* certify wrt. type signature *)
   653 
   654 fun certify cert = cert o tsig_of o check_stale "Sign.certify";
   655 
   656 val certify_class      = certify Type.cert_class;
   657 val certify_sort       = certify Type.cert_sort;
   658 val certify_typ        = certify Type.cert_typ;
   659 val certify_typ_syntax = certify Type.cert_typ_syntax;
   660 val certify_typ_abbrev = certify Type.cert_typ_abbrev;
   661 
   662 
   663 (* certify_term *)
   664 
   665 local
   666 
   667 (*determine and check the type of a term*)
   668 fun type_check pp tm =
   669   let
   670     fun err_appl why bs t T u U =
   671       let
   672         val xs = map Free bs;           (*we do not rename here*)
   673         val t' = subst_bounds (xs, t);
   674         val u' = subst_bounds (xs, u);
   675         val msg = cat_lines
   676           (TypeInfer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
   677       in raise TYPE (msg, [T, U], [t', u']) end;
   678 
   679     fun typ_of (_, Const (_, T)) = T
   680       | typ_of (_, Free  (_, T)) = T
   681       | typ_of (_, Var (_, T)) = T
   682       | typ_of (bs, Bound i) = snd (List.nth (bs, i) handle Subscript =>
   683           raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], [Bound i]))
   684       | typ_of (bs, Abs (x, T, body)) = T --> typ_of ((x, T) :: bs, body)
   685       | typ_of (bs, t $ u) =
   686           let val T = typ_of (bs, t) and U = typ_of (bs, u) in
   687             (case T of
   688               Type ("fun", [T1, T2]) =>
   689                 if T1 = U then T2 else err_appl "Incompatible operand type" bs t T u U
   690             | _ => err_appl "Operator not of function type" bs t T u U)
   691           end;
   692 
   693   in typ_of ([], tm) end;
   694 
   695 in
   696 
   697 fun certify_term pp sg tm =
   698   let
   699     val _ = check_stale "Sign.certify_term" sg;
   700 
   701     val tm' = map_term_types (Type.cert_typ (tsig_of sg)) tm;
   702     val tm' = if tm = tm' then tm else tm';  (*avoid copying of already normal term*)
   703 
   704     fun err msg = raise TYPE (msg, [], [tm']);
   705 
   706     fun show_const a T = quote a ^ " :: " ^ Pretty.string_of_typ pp T;
   707 
   708     fun check_atoms (t $ u) = (check_atoms t; check_atoms u)
   709       | check_atoms (Abs (_, _, t)) = check_atoms t
   710       | check_atoms (Const (a, T)) =
   711           (case const_type sg a of
   712             NONE => err ("Undeclared constant " ^ show_const a T)
   713           | SOME U =>
   714               if typ_instance sg (T, U) then ()
   715               else err ("Illegal type for constant " ^ show_const a T))
   716       | check_atoms (Var ((x, i), _)) =
   717           if i < 0 then err ("Malformed variable: " ^ quote x) else ()
   718       | check_atoms _ = ();
   719   in
   720     check_atoms tm';
   721     (tm', type_check pp tm', maxidx_of_term tm')
   722   end;
   723 
   724 end;
   725 
   726 
   727 
   728 (** read and certify entities **)    (*exception ERROR*)
   729 
   730 (* sorts *)
   731 
   732 fun read_sort' syn sg str =
   733   let
   734     val _ = check_stale "Sign.read_sort'" sg;
   735     val S = intern_sort sg (Syntax.read_sort syn str);
   736   in Type.cert_sort (tsig_of sg) S handle TYPE (msg, _, _) => error msg end;
   737 
   738 fun read_sort sg str = read_sort' (syn_of sg) sg str;
   739 
   740 
   741 (* types *)
   742 
   743 local
   744 
   745 fun gen_read_typ' cert syn (sg, def_sort) str =
   746   let
   747     val _ = check_stale "Sign.gen_read_typ'" sg;
   748     val get_sort = TypeInfer.get_sort (tsig_of sg) def_sort (intern_sort sg);
   749     val T = intern_tycons sg (Syntax.read_typ syn get_sort (intern_sort sg) str);
   750   in cert (tsig_of sg) T handle TYPE (msg, _, _) => error msg end
   751   handle ERROR => error ("The error(s) above occurred in type " ^ quote str);
   752 
   753 fun gen_read_typ cert (sg, def_sort) str = gen_read_typ' cert (syn_of sg) (sg, def_sort) str;
   754 
   755 in
   756 
   757 fun no_def_sort sg = (sg, K NONE);
   758 
   759 val read_typ'        = gen_read_typ' Type.cert_typ;
   760 val read_typ_syntax' = gen_read_typ' Type.cert_typ_syntax;
   761 val read_typ_abbrev' = gen_read_typ' Type.cert_typ_abbrev;
   762 val read_typ         = gen_read_typ Type.cert_typ;
   763 val read_typ_syntax  = gen_read_typ Type.cert_typ_syntax;
   764 val read_typ_abbrev  = gen_read_typ Type.cert_typ_abbrev;
   765 
   766 end;
   767 
   768 
   769 (* type and constant names *)    (*exception TYPE*)   (* FIXME really!? *)
   770 
   771 fun read_tyname sg raw_c =
   772   let val c = intern_tycon sg raw_c in
   773     (case Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c) of
   774       SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT)
   775     | _ => raise TYPE ("Undeclared type constructor: " ^ quote c, [], []))
   776   end;
   777 
   778 fun read_const sg raw_c =
   779   let val c = intern_const sg raw_c
   780   in the_const_type sg c; Const (c, dummyT) end;
   781 
   782 
   783 
   784 (** infer_types **)         (*exception ERROR*)
   785 
   786 (*
   787   def_type: partial map from indexnames to types (constrains Frees and Vars)
   788   def_sort: partial map from indexnames to sorts (constrains TFrees and TVars)
   789   used: list of already used type variables
   790   freeze: if true then generated parameters are turned into TFrees, else TVars
   791 
   792   termss: lists of alternative parses (only one combination should be type-correct)
   793   typs: expected types
   794 *)
   795 
   796 fun infer_types_simult pp sg def_type def_sort used freeze args =
   797   let
   798     val tsig = tsig_of sg;
   799 
   800     val termss = foldr multiply [[]] (map fst args);
   801     val typs =
   802       map (fn (_, T) => certify_typ sg T handle TYPE (msg, _, _) => error msg) args;
   803 
   804     fun infer ts = OK (TypeInfer.infer_types (Syntax.pp_show_brackets pp) tsig
   805         (const_type sg) def_type def_sort (intern_const sg) (intern_tycons sg)
   806         (intern_sort sg) used freeze typs ts)
   807       handle TYPE (msg, _, _) => Error msg;
   808 
   809     val err_results = map infer termss;
   810     val errs = List.mapPartial get_error err_results;
   811     val results = List.mapPartial get_ok err_results;
   812 
   813     val ambiguity = length termss;
   814 
   815     fun ambig_msg () =
   816       if ambiguity > 1 andalso ambiguity <= ! Syntax.ambiguity_level
   817       then
   818         error_msg "Got more than one parse tree.\n\
   819           \Retry with smaller Syntax.ambiguity_level for more information."
   820       else ();
   821   in
   822     if null results then (ambig_msg (); error (cat_lines errs))
   823     else if length results = 1 then
   824       (if ambiguity > ! Syntax.ambiguity_level then
   825         warning "Fortunately, only one parse tree is type correct.\n\
   826           \You may still want to disambiguate your grammar or your input."
   827       else (); hd results)
   828     else (ambig_msg (); error ("More than one term is type correct:\n" ^
   829       cat_lines (map (Pretty.string_of_term pp) (List.concat (map fst results)))))
   830   end;
   831 
   832 
   833 fun infer_types pp sg def_type def_sort used freeze tsT =
   834   apfst hd (infer_types_simult pp sg def_type def_sort used freeze [tsT]);
   835 
   836 
   837 
   838 (** read_def_terms -- read terms and infer types **)
   839 
   840 fun read_def_terms' pp is_logtype syn (sg, types, sorts) used freeze sTs =
   841   let
   842     fun read (s, T) =
   843       let val T' = certify_typ sg T handle TYPE (msg, _, _) => error msg
   844       in (Syntax.read is_logtype syn T' s, T') end;
   845   in infer_types_simult pp sg types sorts used freeze (map read sTs) end;
   846 
   847 fun read_def_terms (sg, types, sorts) =
   848   read_def_terms' (pp sg) (is_logtype sg) (syn_of sg) (sg, types, sorts);
   849 
   850 fun simple_read_term sg T s =
   851   let val ([t], _) = read_def_terms (sg, K NONE, K NONE) [] true [(s, T)]
   852   in t end
   853   handle ERROR => error ("The error(s) above occurred for term " ^ s);
   854 
   855 
   856 
   857 (** signature extension functions **)  (*exception ERROR/TYPE*)
   858 
   859 (* add default sort *)
   860 
   861 fun gen_add_defsort prep_sort s sg = sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   862   (syn, Type.set_defsort (prep_sort sg s) tsig, consts, spaces));
   863 
   864 val add_defsort = gen_add_defsort read_sort;
   865 val add_defsort_i = gen_add_defsort certify_sort;
   866 
   867 
   868 (* add type constructors *)
   869 
   870 fun add_types types sg = sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   871   let
   872     val syn' = map_syntax (Syntax.extend_type_gram types) syn;
   873     val decls = map (fn (a, n, mx) => (full_name sg (Syntax.type_name a mx), n)) types;
   874     val tsig' = Type.add_types decls tsig;
   875     val spaces' = declare_names sg typeK (map #1 decls) spaces;
   876   in (syn', tsig', consts, spaces') end);
   877 
   878 
   879 (* add nonterminals *)
   880 
   881 fun add_nonterminals bnames sg = sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   882   let
   883     val syn' = map_syntax (Syntax.extend_consts bnames) syn;
   884     val names = map (full_name sg) bnames;
   885     val tsig' = Type.add_nonterminals names tsig;
   886     val spaces' = declare_names sg typeK names spaces;
   887   in (syn', tsig', consts, spaces') end);
   888 
   889 
   890 (* add type abbreviations *)
   891 
   892 fun gen_add_tyabbr prep_typ (a, vs, rhs, mx) sg =
   893   sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   894     let
   895       val syn' = map_syntax (Syntax.extend_type_gram [(a, length vs, mx)]) syn;
   896       val a' = full_name sg (Syntax.type_name a mx);
   897       val abbr = (a', vs, prep_typ sg rhs) handle ERROR =>
   898         error ("in type abbreviation " ^ quote (Syntax.type_name a' mx));
   899       val tsig' = Type.add_abbrevs [abbr] tsig;
   900       val spaces' = declare_names sg typeK [a'] spaces;
   901     in (syn', tsig', consts, spaces') end);
   902 
   903 val add_tyabbrs = fold (gen_add_tyabbr (read_typ_syntax o no_def_sort));
   904 val add_tyabbrs_i = fold (gen_add_tyabbr certify_typ_syntax);
   905 
   906 
   907 (* add type arities *)
   908 
   909 fun gen_add_arities int_tycon prep_sort arities sg =
   910   sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   911     let
   912       fun prep_arity (a, Ss, S) = (int_tycon sg a, map (prep_sort sg) Ss, prep_sort sg S)
   913         handle ERROR => error ("in arity for type " ^ quote a);
   914       val tsig' = Type.add_arities (pp sg) (map prep_arity arities) tsig;
   915     in (syn, tsig', consts, spaces) end);
   916 
   917 val add_arities = gen_add_arities intern_tycon read_sort;
   918 val add_arities_i = gen_add_arities (K I) certify_sort;
   919 
   920 
   921 (* modify syntax *)
   922 
   923 fun gen_syntax change_gram prep_typ (prmode, args) sg =
   924   let
   925     fun prep (c, T, mx) = (c, prep_typ sg T, mx) handle ERROR =>
   926       error ("in syntax declaration " ^ quote (Syntax.const_name c mx));
   927   in sg |> map_syn (map_syntax (change_gram (is_logtype sg) prmode (map prep args))) end;
   928 
   929 fun gen_add_syntax x = gen_syntax Syntax.extend_const_gram x;
   930 
   931 val add_modesyntax = gen_add_syntax (read_typ_syntax o no_def_sort);
   932 val add_modesyntax_i = gen_add_syntax certify_typ_syntax;
   933 val add_syntax = curry add_modesyntax Syntax.default_mode;
   934 val add_syntax_i = curry add_modesyntax_i Syntax.default_mode;
   935 val del_modesyntax = gen_syntax Syntax.remove_const_gram (read_typ_syntax o no_def_sort);
   936 val del_modesyntax_i = gen_syntax Syntax.remove_const_gram certify_typ_syntax;
   937 
   938 
   939 (* add constants *)
   940 
   941 fun err_dup_consts cs =
   942   error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
   943 
   944 fun gen_add_consts prep_typ raw_args sg =
   945   let
   946     val prepT = compress_type o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ sg;
   947     fun prep (c, T, mx) = ((c, prepT T, mx) handle TYPE (msg, _, _) => error msg)
   948       handle ERROR => error ("in declaration of constant " ^ quote (Syntax.const_name c mx));
   949     val args = map prep raw_args;
   950     val decls = args |> map (fn (c, T, mx) =>
   951       (full_name sg (Syntax.const_name c mx), (T, stamp ())));
   952   in
   953     sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   954       (syn, tsig,
   955         Symtab.extend (consts, decls) handle Symtab.DUPS cs => err_dup_consts cs,
   956         declare_names sg constK (map #1 decls) spaces))
   957     |> add_syntax_i args
   958   end;
   959 
   960 val add_consts = gen_add_consts (read_typ o no_def_sort);
   961 val add_consts_i = gen_add_consts certify_typ;
   962 
   963 
   964 (* add type classes *)
   965 
   966 val classN = "_class";
   967 
   968 val const_of_class = suffix classN;
   969 fun class_of_const c = unsuffix classN c
   970   handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
   971 
   972 fun gen_add_class int_class (bclass, raw_classes) sg =
   973   sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   974     let
   975       val class = full_name sg bclass;
   976       val classes = map (int_class sg) raw_classes;
   977       val syn' = map_syntax (Syntax.extend_consts [bclass]) syn;
   978       val tsig' = Type.add_classes (pp sg) [(class, classes)] tsig;
   979       val spaces' = declare_names sg classK [class] spaces;
   980     in (syn', tsig', consts, spaces') end)
   981   |> add_consts_i [(const_of_class bclass, a_itselfT --> propT, Syntax.NoSyn)];
   982 
   983 val add_classes = fold (gen_add_class intern_class);
   984 val add_classes_i = fold (gen_add_class (K I));
   985 
   986 
   987 (* add to classrel *)
   988 
   989 fun gen_add_classrel int_class raw_pairs sg =
   990   sg |> map_sign (fn (syn, tsig, consts, spaces) =>
   991     let
   992       val pairs = map (pairself (int_class sg)) raw_pairs;
   993       val tsig' = Type.add_classrel (pp sg) pairs tsig;
   994     in (syn, tsig', consts, spaces) end);
   995 
   996 val add_classrel = gen_add_classrel intern_class;
   997 val add_classrel_i = gen_add_classrel (K I);
   998 
   999 
  1000 (* add translation functions *)
  1001 
  1002 local
  1003 
  1004 fun mk trs = map Syntax.mk_trfun trs;
  1005 
  1006 fun gen_add_trfuns ext non_typed (atrs, trs, tr's, atr's) sg = sg |> map_syn (fn syn =>
  1007   let val syn' = syn |> ext (mk atrs, mk trs, mk (map (apsnd non_typed) tr's), mk atr's)
  1008   in make_syntax sg syn'; syn' end);
  1009 
  1010 fun gen_add_trfunsT ext tr's sg = sg |> map_syn (fn syn =>
  1011   let val syn' = syn |> ext ([], [], mk tr's, [])
  1012   in make_syntax sg syn'; syn' end);
  1013 
  1014 in
  1015 
  1016 val add_trfuns = gen_add_trfuns (map_syntax o Syntax.extend_trfuns) Syntax.non_typed_tr';
  1017 val add_trfunsT = gen_add_trfunsT (map_syntax o Syntax.extend_trfuns);
  1018 val add_advanced_trfuns = gen_add_trfuns extend_trfuns Syntax.non_typed_tr'';
  1019 val add_advanced_trfunsT = gen_add_trfunsT extend_trfuns;
  1020 
  1021 end;
  1022 
  1023 val add_tokentrfuns = map_syn o map_syntax o Syntax.extend_tokentrfuns;
  1024 
  1025 
  1026 (* add translation rules *)
  1027 
  1028 fun add_trrules args sg = sg |> map_syn (fn syn =>
  1029   let val rules = map (Syntax.map_trrule (apfst (intern_tycon sg))) args
  1030   in map_syntax (Syntax.extend_trrules (is_logtype sg) (make_syntax sg syn) rules) syn end);
  1031 
  1032 val add_trrules_i = map_syn o map_syntax o Syntax.extend_trrules_i;
  1033 
  1034 
  1035 (* modify naming *)
  1036 
  1037 val add_path        = map_naming o NameSpace.add_path;
  1038 val qualified_names = map_naming NameSpace.qualified_names;
  1039 val no_base_names   = map_naming NameSpace.no_base_names;
  1040 val custom_accesses = map_naming o NameSpace.custom_accesses;
  1041 val set_policy      = map_naming o NameSpace.set_policy;
  1042 val restore_naming  = map_naming o K o naming_of;
  1043 
  1044 
  1045 (* hide names *)
  1046 
  1047 fun hide_space fully (kind, xnames) sg = sg |> map_sign (fn (syn, tsig, consts, spaces) =>
  1048   let
  1049     val names = map (intern sg kind) xnames;
  1050     val spaces' = hide_names kind fully names spaces;
  1051   in (syn, tsig, consts, spaces') end);
  1052 
  1053 fun hide_space_i fully (kind, names) = map_sign (fn (syn, tsig, consts, spaces) =>
  1054   (syn, tsig, consts, hide_names kind fully names spaces));
  1055 
  1056 
  1057 
  1058 (** merge signatures **)
  1059 
  1060 fun merge_stamps stamps1 stamps2 =
  1061   let val stamps = merge_lists' stamps1 stamps2 in
  1062     (case duplicates (map ! stamps) of
  1063       [] => stamps
  1064     | dups => error ("Attempt to merge different versions of theories " ^ commas_quote dups))
  1065   end;
  1066 
  1067 
  1068 (* trivial merge *)
  1069 
  1070 fun merge_refs (sgr1 as SgRef (SOME (ref (sg1 as Sg ({stamps = s1, ...}, _)))),
  1071         sgr2 as SgRef (SOME (ref (sg2 as Sg ({stamps = s2, ...}, _))))) =
  1072       if subsig (sg2, sg1) then sgr1
  1073       else if subsig (sg1, sg2) then sgr2
  1074       else (merge_stamps s1 s2;  (*check for different versions*)
  1075         error ("Attempt to do non-trivial merge of signature\n" ^
  1076           str_of_sg sg1 ^ " and " ^ str_of_sg sg2))
  1077   | merge_refs _ = sys_error "Sign.merge_refs";
  1078 
  1079 val merge = deref o merge_refs o pairself self_ref;
  1080 
  1081 
  1082 (* non-trivial merge *)              (*exception TERM/ERROR*)
  1083 
  1084 local
  1085 
  1086 fun nontriv_merge (sg1, sg2) =
  1087   if subsig_internal (sg2, sg1) then sg1
  1088   else if subsig_internal (sg1, sg2) then sg2
  1089   else
  1090     if exists_stamp CPureN sg1 <> exists_stamp CPureN sg2
  1091     then error "Cannot merge Pure and CPure developments"
  1092   else
  1093     let
  1094       val Sg ({id = _, stamps = stamps1, syn = Syn (syntax1, trfuns1)},
  1095           {self = _, tsig = tsig1, consts = consts1,
  1096             naming = _, spaces = spaces1, data = data1}) = sg1;
  1097       val Sg ({id = _, stamps = stamps2, syn = Syn (syntax2, trfuns2)},
  1098           {self = _, tsig = tsig2, consts = consts2,
  1099             naming = _, spaces = spaces2, data = data2}) = sg2;
  1100 
  1101       val stamps = merge_stamps stamps1 stamps2;
  1102       val syntax = Syntax.merge_syntaxes syntax1 syntax2;
  1103       val trfuns = merge_trfuns trfuns1 trfuns2;
  1104       val syn = Syn (syntax, trfuns);
  1105       val consts = Symtab.merge eq_snd (consts1, consts2)
  1106         handle Symtab.DUPS cs => err_dup_consts cs;
  1107       val naming = NameSpace.default_naming;
  1108       val spaces = merge_spaces (spaces1, spaces2);
  1109       val data = merge_data (data1, data2);
  1110 
  1111       val pre_sg = make_sg (ref "", SgRef (SOME (ref dummy_sg)), ref "#" :: stamps1)
  1112         naming data (syn, tsig1, consts, spaces);
  1113       val tsig = Type.merge_tsigs (pp pre_sg) (tsig1, tsig2);
  1114 
  1115       val self = SgRef (SOME (ref dummy_sg));
  1116       val sg = make_sg (ref "", self, stamps) naming data (syn, tsig, consts, spaces);
  1117     in assign self sg; syn_of sg; sg end;
  1118 
  1119 in
  1120 
  1121 fun prep_ext_merge sgs =
  1122   if null sgs then
  1123     error "Merge: no parent theories"
  1124   else if exists is_draft sgs then
  1125     error "Attempt to merge draft theories"
  1126   else
  1127     Library.foldl nontriv_merge (hd sgs, tl sgs)
  1128     |> prep_ext
  1129     |> add_path "/";
  1130 
  1131 end;
  1132 
  1133 end;