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