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