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