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