src/Pure/sign.ML
author wenzelm
Wed Apr 16 18:23:25 1997 +0200 (1997-04-16)
changeset 2963 f3b5af1c5a67
parent 2693 8300bba275e3
child 2979 db6941221197
permissions -rw-r--r--
renamed subclass to classrel;
tune type checking error msgs;
     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_classrel (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, classrel, 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 "classrel:"
   197                       (map pretty_classrel classrel));
   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
   322     val show_typ = string_of_typ sg;
   323     val show_term = set_ap Syntax.show_brackets true (string_of_term sg);
   324 
   325     fun term_err [] = ""
   326       | term_err [t] = "\n\nInvolving this term:\n" ^ show_term t
   327       | term_err ts =
   328           "\n\nInvolving these terms:\n" ^ cat_lines (map show_term ts);
   329   in
   330     "\nType checking error: " ^ msg ^ "\n" ^
   331       cat_lines (map show_typ Ts) ^ term_err ts ^ "\n"
   332   end;
   333 
   334 
   335 
   336 (** infer_types **)         (*exception ERROR*)
   337 
   338 (*ts is the list of alternative parses; only one is hoped to be type-correct.
   339   T is the expected type for the correct term.
   340   Other standard arguments:
   341     types is a partial map from indexnames to types (constrains Free, Var).
   342     sorts is a partial map from indexnames to sorts (constrains TFree, TVar).
   343     used is the list of already used type variables.
   344     If freeze then internal TVars are turned into TFrees, else TVars.*)
   345 fun infer_types sg types sorts used freeze (ts, T) =
   346   let
   347     val Sg {tsig, ...} = sg;
   348 
   349     val T' = certify_typ sg T handle TYPE arg => error (exn_type_msg sg arg);
   350 
   351     val ct = const_type sg;
   352 
   353     fun warn() =
   354       if length ts > 1 andalso length ts <= !Syntax.ambiguity_level
   355       then (*no warning shown yet*)
   356            warning "Currently parsed input \
   357                    \produces more than one parse tree.\n\
   358                    \For more information lower Syntax.ambiguity_level."
   359       else ();
   360 
   361     datatype result = One of int * term * (indexname * typ) list
   362                     | Errs of (string * typ list * term list)list
   363                     | Ambigs of term list;
   364 
   365     fun process_term(res,(t,i)) =
   366        let val ([u],tye) = 
   367 	       Type.infer_types(tsig,ct,types,sorts,used,freeze,[T'],[t])
   368        in case res of
   369             One(_,t0,_) => Ambigs([u,t0])
   370           | Errs _ => One(i,u,tye)
   371           | Ambigs(us) => Ambigs(u::us)
   372        end
   373        handle TYPE arg => (case res of Errs(errs) => Errs(arg::errs)
   374                                      | _ => res);
   375 
   376   in case foldl process_term (Errs[], ts ~~ (0 upto (length ts - 1))) of
   377        One(res) =>
   378          (if length ts > !Syntax.ambiguity_level
   379           then writeln "Fortunately, only one parse tree is type correct.\n\
   380             \It helps (speed!) if you disambiguate your grammar or your input."
   381           else ();
   382           res)
   383      | Errs(errs) => (warn(); error(cat_lines(map (exn_type_msg sg) errs)))
   384      | Ambigs(us) =>
   385          (warn();
   386           let val old_show_brackets = !show_brackets
   387               val dummy = show_brackets := true;
   388               val errs = cat_lines(map (string_of_term sg) us)
   389           in show_brackets := old_show_brackets;
   390              error("Error: More than one term is type correct:\n" ^ errs)
   391           end)
   392   end;
   393 
   394 
   395 (** extend signature **)    (*exception ERROR*)
   396 
   397 (** signature extension functions **)  (*exception ERROR*)
   398 
   399 fun decls_of name_of mfixs =
   400   map (fn (x, y, mx) => (name_of x mx, y)) mfixs;
   401 
   402 
   403 (* add default sort *)
   404 
   405 fun ext_defsort (syn, tsig, ctab) defsort =
   406   (syn, Type.ext_tsig_defsort tsig defsort, ctab);
   407 
   408 
   409 (* add type constructors *)
   410 
   411 fun ext_types (syn, tsig, ctab) types =
   412   (Syntax.extend_type_gram syn types,
   413     Type.ext_tsig_types tsig (decls_of Syntax.type_name types),
   414     ctab);
   415 
   416 
   417 (* add type abbreviations *)
   418 
   419 fun read_abbr syn tsig (t, vs, rhs_src) =
   420   (t, vs, read_raw_typ syn tsig (K None) rhs_src)
   421     handle ERROR => error ("in type abbreviation " ^ t);
   422 
   423 fun ext_abbrs rd_abbr (syn, tsig, ctab) abbrs =
   424   let
   425     fun mfix_of (t, vs, _, mx) = (t, length vs, mx);
   426     val syn1 = Syntax.extend_type_gram syn (map mfix_of abbrs);
   427 
   428     fun decl_of (t, vs, rhs, mx) =
   429       rd_abbr syn1 tsig (Syntax.type_name t mx, vs, rhs);
   430   in
   431     (syn1, Type.ext_tsig_abbrs tsig (map decl_of abbrs), ctab)
   432   end;
   433 
   434 fun ext_tyabbrs_i arg = ext_abbrs (K (K I)) arg;
   435 fun ext_tyabbrs   arg = ext_abbrs read_abbr arg;
   436 
   437 
   438 (* add type arities *)
   439 
   440 fun ext_arities (syn, tsig, ctab) arities =
   441   let
   442     val tsig1 = Type.ext_tsig_arities tsig arities;
   443     val log_types = Type.logical_types tsig1;
   444   in
   445     (Syntax.extend_log_types syn log_types, tsig1, ctab)
   446   end;
   447 
   448 
   449 (* add term constants and syntax *)
   450 
   451 fun err_in_const c =
   452   error ("in declaration of constant " ^ quote c);
   453 
   454 fun err_dup_consts cs =
   455   error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
   456 
   457 
   458 fun read_const syn tsig (c, ty_src, mx) =
   459   (c, read_raw_typ syn tsig (K None) ty_src, mx)
   460     handle ERROR => err_in_const (Syntax.const_name c mx);
   461 
   462 fun ext_cnsts rd_const syn_only prmode (syn, tsig, ctab) raw_consts =
   463   let
   464     fun prep_const (c, ty, mx) = 
   465      (c, compress_type (Type.varifyT (Type.cert_typ tsig (Type.no_tvars ty))), mx)
   466        handle TYPE (msg, _, _)
   467          => (writeln msg; err_in_const (Syntax.const_name c mx));
   468 
   469     val consts = map (prep_const o rd_const syn tsig) raw_consts;
   470     val decls =
   471       if syn_only then []
   472       else filter_out (equal "" o fst) (decls_of Syntax.const_name consts);
   473   in
   474     (Syntax.extend_const_gram syn prmode consts, tsig,
   475       Symtab.extend_new (ctab, decls)
   476         handle Symtab.DUPS cs => err_dup_consts cs)
   477   end;
   478 
   479 val ext_consts_i = ext_cnsts (K (K I)) false ("", true);
   480 val ext_consts = ext_cnsts read_const false ("", true);
   481 val ext_syntax_i = ext_cnsts (K (K I)) true ("", true);
   482 val ext_syntax = ext_cnsts read_const true ("", true);
   483 fun ext_modesyntax_i sg (prmode, consts) = ext_cnsts (K (K I)) true prmode sg consts;
   484 fun ext_modesyntax sg (prmode, consts) = ext_cnsts read_const true prmode sg consts;
   485 
   486 
   487 (* add type classes *)
   488 
   489 fun const_of_class c = c ^ "_class";
   490 
   491 fun class_of_const c_class =
   492   let
   493     val c = implode (take (size c_class - 6, explode c_class));
   494   in
   495     if const_of_class c = c_class then c
   496     else raise_term ("class_of_const: bad name " ^ quote c_class) []
   497   end;
   498 
   499 
   500 fun ext_classes (syn, tsig, ctab) classes =
   501   let
   502     val names = map fst classes;
   503     val consts =
   504       map (fn c => (const_of_class c, a_itselfT --> propT, NoSyn)) names;
   505   in
   506     ext_consts_i
   507       (Syntax.extend_consts syn names, Type.ext_tsig_classes tsig classes, ctab)
   508       consts
   509   end;
   510 
   511 
   512 (* add to classrel *)
   513 
   514 fun ext_classrel (syn, tsig, ctab) pairs =
   515   (syn, Type.ext_tsig_classrel tsig pairs, ctab);
   516 
   517 
   518 (* add to syntax *)
   519 
   520 fun ext_syn extfun (syn, tsig, ctab) args =
   521   (extfun syn args, tsig, ctab);
   522 
   523 
   524 (* build signature *)
   525 
   526 fun ext_stamps stamps name =
   527   let
   528     val stmps = (case stamps of ref "#" :: ss => ss | ss => ss);
   529   in
   530     if exists (equal name o !) stmps then
   531       error ("Theory already contains a " ^ quote name ^ " component")
   532     else ref name :: stmps
   533   end;
   534 
   535 fun make_sign (syn, tsig, ctab) stamps name =
   536   Sg {tsig = tsig, const_tab = ctab, syn = syn,
   537     stamps = ext_stamps stamps name};
   538 
   539 fun extend_sign extfun name decls (Sg {tsig, const_tab, syn, stamps}) =
   540   make_sign (extfun (syn, tsig, const_tab) decls) stamps name;
   541 
   542 
   543 (* the external interfaces *)
   544 
   545 val add_classes      = extend_sign ext_classes "#";
   546 val add_classrel     = extend_sign ext_classrel "#";
   547 val add_defsort      = extend_sign ext_defsort "#";
   548 val add_types        = extend_sign ext_types "#";
   549 val add_tyabbrs      = extend_sign ext_tyabbrs "#";
   550 val add_tyabbrs_i    = extend_sign ext_tyabbrs_i "#";
   551 val add_arities      = extend_sign ext_arities "#";
   552 val add_consts       = extend_sign ext_consts "#";
   553 val add_consts_i     = extend_sign ext_consts_i "#";
   554 val add_syntax       = extend_sign ext_syntax "#";
   555 val add_syntax_i     = extend_sign ext_syntax_i "#";
   556 val add_modesyntax   = extend_sign ext_modesyntax "#";
   557 val add_modesyntax_i = extend_sign ext_modesyntax_i "#";
   558 val add_trfuns       = extend_sign (ext_syn Syntax.extend_trfuns) "#";
   559 val add_trfunsT      = extend_sign (ext_syn Syntax.extend_trfunsT) "#";
   560 val add_tokentrfuns  = extend_sign (ext_syn Syntax.extend_tokentrfuns) "#";
   561 val add_trrules      = extend_sign (ext_syn Syntax.extend_trrules) "#";
   562 val add_trrules_i    = extend_sign (ext_syn Syntax.extend_trrules_i) "#";
   563 
   564 fun add_name name sg = extend_sign K name () sg;
   565 val make_draft = add_name "#";
   566 
   567 
   568 
   569 (** merge signatures **)    (*exception TERM*) (*exception ERROR (* FIXME *)*)
   570 
   571 fun merge (sg1, sg2) =
   572   if fast_subsig (sg2, sg1) then sg1
   573   else if fast_subsig (sg1, sg2) then sg2
   574   else if subsig (sg2, sg1) then sg1
   575   else if subsig (sg1, sg2) then sg2
   576   else if is_draft sg1 orelse is_draft sg2 then
   577     raise_term "Illegal merge of draft signatures" []
   578   else
   579     (*neither is union already; must form union*)
   580     let
   581       val Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1,
   582         stamps = stamps1} = sg1;
   583       val Sg {tsig = tsig2, const_tab = const_tab2, syn = syn2,
   584         stamps = stamps2} = sg2;
   585 
   586 
   587       val stamps = merge_rev_lists stamps1 stamps2;
   588       val _ =
   589         (case duplicates (stamp_names stamps) of
   590           [] => ()
   591         | dups => raise_term ("Attempt to merge different versions of theories "
   592             ^ commas_quote dups) []);
   593 
   594       val tsig = Type.merge_tsigs (tsig1, tsig2);
   595 
   596       val const_tab = Symtab.merge (op =) (const_tab1, const_tab2)
   597         handle Symtab.DUPS cs =>
   598           raise_term ("Incompatible types for constant(s) " ^ commas_quote cs) [];
   599 
   600       val syn = Syntax.merge_syntaxes syn1 syn2;
   601     in
   602       Sg {tsig = tsig, const_tab = const_tab, syn = syn, stamps = stamps}
   603     end;
   604 
   605 
   606 
   607 (** the Pure signature **)
   608 
   609 val proto_pure =
   610   make_sign (Syntax.pure_syn, Type.tsig0, Symtab.null) [] "#"
   611   |> add_types
   612    (("fun", 2, NoSyn) ::
   613     ("prop", 0, NoSyn) ::
   614     ("itself", 1, NoSyn) ::
   615     Syntax.pure_types)
   616   |> add_classes [(logicC, [])]
   617   |> add_defsort logicS
   618   |> add_arities
   619    [("fun", [logicS, logicS], logicS),
   620     ("prop", [], logicS),
   621     ("itself", [logicS], logicS)]
   622   |> add_syntax Syntax.pure_syntax
   623   |> add_modesyntax (("symbols", true), Syntax.pure_sym_syntax)
   624   |> add_trfuns Syntax.pure_trfuns
   625   |> add_trfunsT Syntax.pure_trfunsT
   626   |> add_consts
   627    [("==", "['a::{}, 'a] => prop", InfixrName ("==", 2)),
   628     ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
   629     ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
   630     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
   631     ("TYPE", "'a itself", NoSyn)]
   632   |> add_syntax
   633    [("==>", "[prop, prop] => prop", Delimfix "op ==>")]
   634   |> add_name "ProtoPure";
   635 
   636 val pure = proto_pure
   637   |> add_syntax Syntax.pure_appl_syntax
   638   |> add_name "Pure";
   639 
   640 val cpure = proto_pure
   641   |> add_syntax Syntax.pure_applC_syntax
   642   |> add_name "CPure";
   643 
   644 end;