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