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