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