src/Pure/sign.ML
author wenzelm
Wed Nov 13 10:59:53 1996 +0100 (1996-11-13)
changeset 2184 99805d7652a9
parent 2180 934572a94139
child 2185 f9686e7e6d4d
permissions -rw-r--r--
tuned subsig;
     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   val rep_sg: sg -> {tsig: Type.type_sig,
    12 		     const_tab: typ Symtab.table,
    13 		     syn: Syntax.syntax,
    14 		     stamps: string ref list}
    15   val subsig: sg * sg -> bool
    16   val eq_sg: sg * sg -> bool
    17   val same_sg: sg * sg -> bool
    18   val is_draft: sg -> bool
    19   val const_type: sg -> string -> typ option
    20   val classes: sg -> class list
    21   val subsort: sg -> sort * sort -> bool
    22   val nodup_Vars: term -> unit
    23   val norm_sort: sg -> sort -> sort
    24   val nonempty_sort: sg -> sort list -> sort -> bool
    25   val print_sg: sg -> unit
    26   val pretty_sg: sg -> Pretty.T
    27   val pprint_sg: sg -> pprint_args -> unit
    28   val pretty_term: sg -> term -> Pretty.T
    29   val pretty_typ: sg -> typ -> Pretty.T
    30   val pretty_sort: sort -> Pretty.T
    31   val string_of_term: sg -> term -> string
    32   val string_of_typ: sg -> typ -> string
    33   val pprint_term: sg -> term -> pprint_args -> unit
    34   val pprint_typ: sg -> typ -> pprint_args -> unit
    35   val certify_typ: sg -> typ -> typ
    36   val certify_term: sg -> term -> term * typ * int
    37   val read_typ: sg * (indexname -> sort option) -> string -> typ
    38   val exn_type_msg: sg -> string * typ list * term list -> string
    39   val infer_types: sg -> (indexname -> typ option) ->
    40     (indexname -> sort option) -> string list -> bool
    41     -> term list * typ -> int * term * (indexname * typ) list
    42   val add_classes: (class * class list) list -> sg -> sg
    43   val add_classrel: (class * class) list -> sg -> sg
    44   val add_defsort: sort -> sg -> sg
    45   val add_types: (string * int * mixfix) list -> sg -> sg
    46   val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg
    47   val add_tyabbrs_i: (string * string list * typ * mixfix) list -> sg -> sg
    48   val add_arities: (string * sort list * sort) list -> sg -> sg
    49   val add_consts: (string * string * mixfix) list -> sg -> sg
    50   val add_consts_i: (string * typ * mixfix) list -> sg -> sg
    51   val add_syntax: (string * string * mixfix) list -> sg -> sg
    52   val add_syntax_i: (string * typ * mixfix) list -> sg -> sg
    53   val add_trfuns:
    54     (string * (ast list -> ast)) list *
    55     (string * (term list -> term)) list *
    56     (string * (term list -> term)) list *
    57     (string * (ast list -> ast)) list -> sg -> sg
    58   val add_trrules: (string * string) Syntax.trrule list -> sg -> sg
    59   val add_trrules_i: ast Syntax.trrule list -> sg -> sg
    60   val add_name: string -> sg -> sg
    61   val make_draft: sg -> sg
    62   val merge: sg * sg -> sg
    63   val proto_pure: sg
    64   val pure: sg
    65   val cpure: sg
    66   val const_of_class: class -> string
    67   val class_of_const: string -> class
    68   end;
    69 
    70 structure Sign : SIGN =
    71 struct
    72 
    73 local open Type Syntax in
    74 
    75 (** datatype sg **)
    76 
    77 (*the "ref" in stamps ensures that no two signatures are identical -- it is
    78   impossible to forge a signature*)
    79 
    80 datatype sg =
    81   Sg of {
    82     tsig: Type.type_sig,                 (*order-sorted signature of types*)
    83     const_tab: typ Symtab.table,    (*types of constants*)
    84     syn: Syntax.syntax,             (*syntax for parsing and printing*)
    85     stamps: string ref list};       (*unique theory indentifier*)
    86 
    87 fun rep_sg (Sg args) = args;
    88 val tsig_of = #tsig o rep_sg;
    89 
    90 
    91 (*** Stamps ***)
    92 
    93 (*Avoiding polymorphic equality: 10* speedup*)
    94 fun mem_stamp (_:string ref, []) = false
    95   | mem_stamp (x, y::xs) = x=y orelse mem_stamp(x,xs);
    96 
    97 fun subset_stamp ([], ys) = true
    98   | subset_stamp (x :: xs, ys) = mem_stamp(x, ys) andalso subset_stamp(xs, ys);
    99 
   100 fun eq_set_stamp (xs, ys) =
   101     xs = ys orelse (subset_stamp (xs, ys) andalso subset_stamp (ys, xs));
   102 
   103 fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
   104   | is_draft _ = false;
   105 
   106 fun subsig (Sg{stamps=s1,...}, Sg{stamps=s2,...}) =
   107   s1 = s2 orelse subset_stamp (s1, s2);
   108 
   109 fun eq_sg (Sg{stamps=s1,...}, Sg{stamps=s2,...}) = eq_set_stamp(s1,s2);
   110 
   111 (* test if same theory names are contained in signatures' stamps,
   112    i.e. if signatures belong to same theory but not necessarily to the same
   113    version of it*)
   114 fun same_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) =
   115   eq_set_string (pairself (map (op !)) (s1, s2));
   116 
   117 
   118 (* consts *)
   119 
   120 fun const_type (Sg {const_tab, ...}) c =
   121   Symtab.lookup (const_tab, c);
   122 
   123 
   124 (* classes and sorts *)
   125 
   126 val classes = #classes o Type.rep_tsig o tsig_of;
   127 
   128 val subsort = Type.subsort o tsig_of;
   129 val norm_sort = Type.norm_sort o tsig_of;
   130 val nonempty_sort = Type.nonempty_sort o tsig_of;
   131 
   132 fun pretty_sort [c] = Pretty.str c
   133   | pretty_sort cs = Pretty.str_list "{" "}" cs;
   134 
   135 
   136 
   137 (** print signature **)
   138 
   139 val stamp_names = rev o map !;
   140 
   141 fun print_sg sg =
   142   let
   143     fun prt_typ syn ty = Pretty.quote (Syntax.pretty_typ syn ty);
   144 
   145     fun pretty_subclass (cl, cls) = Pretty.block
   146       (Pretty.str (cl ^ " <") :: Pretty.brk 1 ::
   147         Pretty.commas (map Pretty.str cls));
   148 
   149     fun pretty_default cls = Pretty.block
   150       [Pretty.str "default:", Pretty.brk 1, pretty_sort cls];
   151 
   152     fun pretty_ty (ty, n) = Pretty.str (ty ^ " " ^ string_of_int n);
   153 
   154     fun pretty_abbr syn (ty, (vs, rhs)) = Pretty.block
   155       [prt_typ syn (Type (ty, map (fn v => TVar ((v, 0), [])) vs)),
   156         Pretty.str " =", Pretty.brk 1, prt_typ syn rhs];
   157 
   158     fun pretty_arity ty (cl, []) = Pretty.block
   159           [Pretty.str (ty ^ " ::"), Pretty.brk 1, Pretty.str cl]
   160       | pretty_arity ty (cl, srts) = Pretty.block
   161           [Pretty.str (ty ^ " ::"), Pretty.brk 1,
   162             Pretty.list "(" ")" (map pretty_sort srts),
   163             Pretty.brk 1, Pretty.str cl];
   164 
   165     fun pretty_arities (ty, ars) = map (pretty_arity ty) ars;
   166 
   167     fun pretty_const syn (c, ty) = Pretty.block
   168       [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ syn ty];
   169 
   170 
   171     val Sg {tsig, const_tab, syn, stamps} = sg;
   172     val {classes, subclass, default, tycons, abbrs, arities} = rep_tsig tsig;
   173   in
   174     Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps));
   175     Pretty.writeln (Pretty.strs ("classes:" :: classes));
   176     Pretty.writeln (Pretty.big_list "subclass:"
   177                       (map pretty_subclass subclass));
   178     Pretty.writeln (pretty_default default);
   179     Pretty.writeln (Pretty.big_list "types:" (map pretty_ty tycons));
   180     Pretty.writeln (Pretty.big_list "abbrs:" (map (pretty_abbr syn) abbrs));
   181     Pretty.writeln (Pretty.big_list "arities:"
   182                       (flat (map pretty_arities arities)));
   183     Pretty.writeln (Pretty.big_list "consts:"
   184                       (map (pretty_const syn) (Symtab.dest const_tab)))
   185   end;
   186 
   187 
   188 fun pretty_sg (Sg {stamps, ...}) =
   189   Pretty.str_list "{" "}" (stamp_names stamps);
   190 
   191 val pprint_sg = Pretty.pprint o pretty_sg;
   192 
   193 
   194 
   195 (** pretty printing of terms and types **)
   196 
   197 fun pretty_term (Sg {syn, stamps, ...}) =
   198   let val curried = "CPure" mem_string (map ! stamps);
   199   in Syntax.pretty_term curried syn end;
   200 
   201 fun pretty_typ (Sg {syn, ...}) = Syntax.pretty_typ syn;
   202 
   203 fun string_of_term (Sg {syn, stamps, ...}) =
   204   let val curried = "CPure" mem_string (map ! stamps);
   205   in Syntax.string_of_term curried syn end;
   206 
   207 fun string_of_typ (Sg {syn, ...}) = Syntax.string_of_typ syn;
   208 
   209 fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg);
   210 fun pprint_typ sg = Pretty.pprint o Pretty.quote o (pretty_typ sg);
   211 
   212 
   213 
   214 (** read types **)  (*exception ERROR*)
   215 
   216 fun err_in_type s =
   217   error ("The error(s) above occurred in type " ^ quote s);
   218 
   219 fun read_raw_typ syn tsig sort_of str =
   220   Syntax.read_typ syn (fn x => if_none (sort_of x) (defaultS tsig)) str
   221     handle ERROR => err_in_type str;
   222 
   223 (*read and certify typ wrt a signature*)
   224 fun read_typ (Sg {tsig, syn, ...}, sort_of) str =
   225   cert_typ tsig (read_raw_typ syn tsig sort_of str)
   226     handle TYPE (msg, _, _) => (writeln msg; err_in_type str);
   227 
   228 
   229 
   230 (** certify types and terms **)   (*exception TYPE*)
   231 
   232 fun certify_typ (Sg {tsig, ...}) ty = cert_typ tsig ty;
   233 
   234 (* check for duplicate TVars with distinct sorts *)
   235 fun nodup_TVars(tvars,T) = (case T of
   236       Type(_,Ts) => nodup_TVars_list (tvars,Ts)
   237     | TFree _ => tvars
   238     | TVar(v as (a,S)) =>
   239         (case assoc_string_int(tvars,a) of
   240            Some(S') => if S=S' then tvars
   241                        else raise_type
   242                             ("Type variable "^Syntax.string_of_vname a^
   243                              " has two distinct sorts") [TVar(a,S'),T] []
   244          | None => v::tvars))
   245 and (*equivalent to foldl nodup_TVars_list, but 3X faster under Poly/ML*)
   246     nodup_TVars_list (tvars,[]) = tvars
   247   | nodup_TVars_list (tvars,T::Ts) = nodup_TVars_list(nodup_TVars(tvars,T), 
   248 						      Ts);
   249 
   250 (* check for duplicate Vars with distinct types *)
   251 fun nodup_Vars tm =
   252 let fun nodups vars tvars tm = (case tm of
   253           Const(c,T) => (vars, nodup_TVars(tvars,T))
   254         | Free(a,T) => (vars, nodup_TVars(tvars,T))
   255         | Var(v as (ixn,T)) =>
   256             (case assoc_string_int(vars,ixn) of
   257                Some(T') => if T=T' then (vars,nodup_TVars(tvars,T))
   258                            else raise_type
   259                              ("Variable "^Syntax.string_of_vname ixn^
   260                               " has two distinct types") [T',T] []
   261              | None => (v::vars,tvars))
   262         | Bound _ => (vars,tvars)
   263         | Abs(_,T,t) => nodups vars (nodup_TVars(tvars,T)) t
   264         | s$t => let val (vars',tvars') = nodups vars tvars s
   265                  in nodups vars' tvars' t end);
   266 in nodups [] [] tm; () end;
   267 
   268 fun mapfilt_atoms f (Abs (_, _, t)) = mapfilt_atoms f t
   269   | mapfilt_atoms f (t $ u) = mapfilt_atoms f t @ mapfilt_atoms f u
   270   | mapfilt_atoms f a = (case f a of Some y => [y] | None => []);
   271 
   272 fun certify_term (sg as Sg {tsig, ...}) tm =
   273   let
   274     fun valid_const a T =
   275       (case const_type sg a of
   276         Some U => typ_instance (tsig, T, U)
   277       | _ => false);
   278 
   279     fun atom_err (Const (a, T)) =
   280           if valid_const a T then None
   281           else Some ("Illegal type for constant " ^ quote a ^ " :: " ^
   282             quote (string_of_typ sg T))
   283       | atom_err (Var ((x, i), _)) =
   284           if i < 0 then Some ("Negative index for Var " ^ quote x) else None
   285       | atom_err _ = None;
   286 
   287     val norm_tm =
   288       (case it_term_types (typ_errors tsig) (tm, []) of
   289         [] => map_term_types (norm_typ tsig) tm
   290       | errs => raise_type (cat_lines errs) [] [tm]);
   291     val _ = nodup_Vars norm_tm;
   292   in
   293     (case mapfilt_atoms atom_err norm_tm of
   294       [] => (norm_tm, type_of norm_tm, maxidx_of_term norm_tm)
   295     | errs => raise_type (cat_lines errs) [] [norm_tm])
   296   end;
   297 
   298 
   299 (*Package error messages from type checking*)
   300 fun exn_type_msg sg (msg, Ts, ts) =
   301     let val show_typ = string_of_typ sg
   302 	val show_term = string_of_term sg
   303 	fun term_err [] = ""
   304 	  | term_err [t] = "\nInvolving this term:\n" ^ show_term t
   305 	  | term_err ts =
   306 	    "\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
   307     in  "\nType checking error: " ^ msg ^ "\n" ^
   308 	cat_lines (map show_typ Ts) ^ term_err ts ^ "\n"
   309     end; 
   310 
   311 
   312 
   313 (** infer_types **)         (*exception ERROR*)
   314 
   315 (*ts is the list of alternative parses; only one is hoped to be type-correct.
   316   T is the expected type for the correct term.
   317   Other standard arguments:
   318     types is a partial map from indexnames to types (constrains Free, Var).
   319     sorts is a partial map from indexnames to sorts (constrains TFree, TVar).
   320     used is the list of already used type variables.
   321     If freeze then internal TVars are turned into TFrees, else TVars.*)
   322 fun infer_types sg types sorts used freeze (ts, T) =
   323   let
   324     val Sg {tsig, ...} = sg;
   325 
   326     val T' = certify_typ sg T handle TYPE arg => error (exn_type_msg sg arg);
   327 
   328     val ct = const_type sg;
   329 
   330     fun warn() =
   331       if length ts > 1 andalso length ts <= !Syntax.ambiguity_level
   332       then (*no warning shown yet*)
   333            warning "Currently parsed input \
   334                    \produces more than one parse tree.\n\
   335                    \For more information lower Syntax.ambiguity_level."
   336       else ();
   337 
   338     datatype result = One of int * term * (indexname * typ) list
   339                     | Errs of (string * typ list * term list)list
   340                     | Ambigs of term list;
   341 
   342     fun process_term(res,(t,i)) =
   343        let val ([u],tye) = 
   344 	       Type.infer_types(tsig,ct,types,sorts,used,freeze,[T'],[t])
   345        in case res of
   346             One(_,t0,_) => Ambigs([u,t0])
   347           | Errs _ => One(i,u,tye)
   348           | Ambigs(us) => Ambigs(u::us)
   349        end
   350        handle TYPE arg => (case res of Errs(errs) => Errs(arg::errs)
   351                                      | _ => res);
   352 
   353   in case foldl process_term (Errs[], ts ~~ (0 upto (length ts - 1))) of
   354        One(res) =>
   355          (if length ts > !Syntax.ambiguity_level
   356           then writeln "Fortunately, only one parse tree is type correct.\n\
   357             \It helps (speed!) if you disambiguate your grammar or your input."
   358           else ();
   359           res)
   360      | Errs(errs) => (warn(); error(cat_lines(map (exn_type_msg sg) errs)))
   361      | Ambigs(us) =>
   362          (warn();
   363           let val old_show_brackets = !show_brackets
   364               val dummy = show_brackets := true;
   365               val errs = cat_lines(map (string_of_term sg) us)
   366           in show_brackets := old_show_brackets;
   367              error("Error: More than one term is type correct:\n" ^ errs)
   368           end)
   369   end;
   370 
   371 
   372 (** extend signature **)    (*exception ERROR*)
   373 
   374 (** signature extension functions **)  (*exception ERROR*)
   375 
   376 fun decls_of name_of mfixs =
   377   map (fn (x, y, mx) => (name_of x mx, y)) mfixs;
   378 
   379 
   380 (* add default sort *)
   381 
   382 fun ext_defsort (syn, tsig, ctab) defsort =
   383   (syn, ext_tsig_defsort tsig defsort, ctab);
   384 
   385 
   386 (* add type constructors *)
   387 
   388 fun ext_types (syn, tsig, ctab) types =
   389   (Syntax.extend_type_gram syn types,
   390     ext_tsig_types tsig (decls_of Syntax.type_name types),
   391     ctab);
   392 
   393 
   394 (* add type abbreviations *)
   395 
   396 fun read_abbr syn tsig (t, vs, rhs_src) =
   397   (t, vs, read_raw_typ syn tsig (K None) rhs_src)
   398     handle ERROR => error ("in type abbreviation " ^ t);
   399 
   400 fun ext_abbrs rd_abbr (syn, tsig, ctab) abbrs =
   401   let
   402     fun mfix_of (t, vs, _, mx) = (t, length vs, mx);
   403     val syn1 = Syntax.extend_type_gram syn (map mfix_of abbrs);
   404 
   405     fun decl_of (t, vs, rhs, mx) =
   406       rd_abbr syn1 tsig (Syntax.type_name t mx, vs, rhs);
   407   in
   408     (syn1, ext_tsig_abbrs tsig (map decl_of abbrs), ctab)
   409   end;
   410 
   411 val ext_tyabbrs_i = ext_abbrs (K (K I));
   412 val ext_tyabbrs = ext_abbrs read_abbr;
   413 
   414 
   415 (* add type arities *)
   416 
   417 fun ext_arities (syn, tsig, ctab) arities =
   418   let
   419     val tsig1 = ext_tsig_arities tsig arities;
   420     val log_types = logical_types tsig1;
   421   in
   422     (Syntax.extend_log_types syn log_types, tsig1, ctab)
   423   end;
   424 
   425 
   426 (* add term constants and syntax *)
   427 
   428 fun err_in_const c =
   429   error ("in declaration of constant " ^ quote c);
   430 
   431 fun err_dup_consts cs =
   432   error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
   433 
   434 
   435 fun read_const syn tsig (c, ty_src, mx) =
   436   (c, read_raw_typ syn tsig (K None) ty_src, mx)
   437     handle ERROR => err_in_const (Syntax.const_name c mx);
   438 
   439 fun ext_cnsts rd_const syn_only (syn, tsig, ctab) raw_consts =
   440   let
   441     fun prep_const (c, ty, mx) = 
   442 	  (c, 
   443 	   compress_type (varifyT (cert_typ tsig (no_tvars ty))), 
   444 	   mx)
   445       handle TYPE (msg, _, _) => (writeln msg; err_in_const (Syntax.const_name c mx));
   446 
   447     val consts = map (prep_const o rd_const syn tsig) raw_consts;
   448     val decls =
   449       if syn_only then []
   450       else filter_out (equal "" o fst) (decls_of Syntax.const_name consts);
   451   in
   452     (Syntax.extend_const_gram syn consts, tsig,
   453       Symtab.extend_new (ctab, decls)
   454         handle Symtab.DUPS cs => err_dup_consts cs)
   455   end;
   456 
   457 val ext_consts_i = ext_cnsts (K (K I)) false;
   458 val ext_consts = ext_cnsts read_const false;
   459 val ext_syntax_i = ext_cnsts (K (K I)) true;
   460 val ext_syntax = ext_cnsts read_const true;
   461 
   462 
   463 (* add type classes *)
   464 
   465 fun const_of_class c = c ^ "_class";
   466 
   467 fun class_of_const c_class =
   468   let
   469     val c = implode (take (size c_class - 6, explode c_class));
   470   in
   471     if const_of_class c = c_class then c
   472     else raise_term ("class_of_const: bad name " ^ quote c_class) []
   473   end;
   474 
   475 
   476 fun ext_classes (syn, tsig, ctab) classes =
   477   let
   478     val names = map fst classes;
   479     val consts =
   480       map (fn c => (const_of_class c, a_itselfT --> propT, NoSyn)) names;
   481   in
   482     ext_consts_i
   483       (Syntax.extend_consts syn names, ext_tsig_classes tsig classes, ctab)
   484       consts
   485   end;
   486 
   487 
   488 (* add to subclass relation *)
   489 
   490 fun ext_classrel (syn, tsig, ctab) pairs =
   491   (syn, ext_tsig_subclass tsig pairs, ctab);
   492 
   493 
   494 (* add to syntax *)
   495 
   496 fun ext_syn extfun (syn, tsig, ctab) args =
   497   (extfun syn args, tsig, ctab);
   498 
   499 
   500 (* build signature *)
   501 
   502 fun ext_stamps stamps name =
   503   let
   504     val stmps = (case stamps of ref "#" :: ss => ss | ss => ss);
   505   in
   506     if exists (equal name o !) stmps then
   507       error ("Theory already contains a " ^ quote name ^ " component")
   508     else ref name :: stmps
   509   end;
   510 
   511 fun make_sign (syn, tsig, ctab) stamps name =
   512   Sg {tsig = tsig, const_tab = ctab, syn = syn,
   513     stamps = ext_stamps stamps name};
   514 
   515 fun extend_sign extfun name decls (Sg {tsig, const_tab, syn, stamps}) =
   516   make_sign (extfun (syn, tsig, const_tab) decls) stamps name;
   517 
   518 
   519 (* the external interfaces *)
   520 
   521 val add_classes   = extend_sign ext_classes "#";
   522 val add_classrel  = extend_sign ext_classrel "#";
   523 val add_defsort   = extend_sign ext_defsort "#";
   524 val add_types     = extend_sign ext_types "#";
   525 val add_tyabbrs   = extend_sign ext_tyabbrs "#";
   526 val add_tyabbrs_i = extend_sign ext_tyabbrs_i "#";
   527 val add_arities   = extend_sign ext_arities "#";
   528 val add_consts    = extend_sign ext_consts "#";
   529 val add_consts_i  = extend_sign ext_consts_i "#";
   530 val add_syntax    = extend_sign ext_syntax "#";
   531 val add_syntax_i  = extend_sign ext_syntax_i "#";
   532 val add_trfuns    = extend_sign (ext_syn Syntax.extend_trfuns) "#";
   533 val add_trrules   = extend_sign (ext_syn Syntax.extend_trrules) "#";
   534 val add_trrules_i = extend_sign (ext_syn Syntax.extend_trrules_i) "#";
   535 
   536 fun add_name name sg = extend_sign K name () sg;
   537 val make_draft = add_name "#";
   538 
   539 
   540 
   541 (** merge signatures **)    (*exception TERM*) (*exception ERROR (* FIXME *)*)
   542 
   543 fun merge (sg1, sg2) =
   544   if subsig (sg2, sg1) then sg1
   545   else if subsig (sg1, sg2) then sg2
   546   else if is_draft sg1 orelse is_draft sg2 then
   547     raise_term "Illegal merge of draft signatures" []
   548   else
   549     (*neither is union already; must form union*)
   550     let
   551       val Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1,
   552         stamps = stamps1} = sg1;
   553       val Sg {tsig = tsig2, const_tab = const_tab2, syn = syn2,
   554         stamps = stamps2} = sg2;
   555 
   556 
   557       val stamps = merge_rev_lists stamps1 stamps2;
   558       val _ =
   559         (case duplicates (stamp_names stamps) of
   560           [] => ()
   561         | dups => raise_term ("Attempt to merge different versions of theories "
   562             ^ commas_quote dups) []);
   563 
   564       val tsig = merge_tsigs (tsig1, tsig2);
   565 
   566       val const_tab = Symtab.merge (op =) (const_tab1, const_tab2)
   567         handle Symtab.DUPS cs =>
   568           raise_term ("Incompatible types for constant(s) " ^ commas_quote cs) [];
   569 
   570       val syn = Syntax.merge_syntaxes syn1 syn2;
   571     in
   572       Sg {tsig = tsig, const_tab = const_tab, syn = syn, stamps = stamps}
   573     end;
   574 
   575 
   576 
   577 (** the Pure signature **)
   578 
   579 val proto_pure =
   580   make_sign (Syntax.pure_syn, tsig0, Symtab.null) [] "#"
   581   |> add_types
   582    (("fun", 2, NoSyn) ::
   583     ("prop", 0, NoSyn) ::
   584     ("itself", 1, NoSyn) ::
   585     Syntax.pure_types)
   586   |> add_classes [(logicC, [])]
   587   |> add_defsort logicS
   588   |> add_arities
   589    [("fun", [logicS, logicS], logicS),
   590     ("prop", [], logicS),
   591     ("itself", [logicS], logicS)]
   592   |> add_syntax Syntax.pure_syntax
   593   |> add_trfuns Syntax.pure_trfuns
   594   |> add_consts
   595    [("==", "['a::{}, 'a] => prop", Mixfix ("(_ ==/ _)", [3, 2], 2)),
   596     ("=?=", "['a::{}, 'a] => prop", Mixfix ("(_ =?=/ _)", [3, 2], 2)),
   597     ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   598     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
   599     ("TYPE", "'a itself", NoSyn)]
   600   |> add_name "ProtoPure";
   601 
   602 val pure = proto_pure
   603   |> add_syntax Syntax.pure_appl_syntax
   604   |> add_name "Pure";
   605 
   606 val cpure = proto_pure
   607   |> add_syntax Syntax.pure_applC_syntax
   608   |> add_name "CPure";
   609 
   610 end
   611 end;