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