src/Pure/sign.ML
author wenzelm
Thu May 19 16:20:52 1994 +0200 (1994-05-19)
changeset 386 e9ba9f7e2542
parent 277 4abe17e92130
child 402 16a8fe4f2250
permissions -rw-r--r--
added const_type: sg -> typ option;
stamps now stored in REVERSE order;
now supports 'draft signatures' and incremental extension: is_draft,
add_classes (supports axclasses), add_defsort, add_types, add_tyabbrs,
add_tyabbrs_i, add_arities, add_consts, add_consts_i, add_syntax,
add_syntax_i, add_trfuns, add_trrules, add_name, make_draft;
added const_of_class, class_of_const (for axclasses);
changed the pure signature to support axclasses (added itself, TYPE);
various major internal changes;
     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 TODO:
     8   pure sign: elim Syntax.constrainC
     9 *)
    10 
    11 signature SIGN =
    12 sig
    13   structure Symtab: SYMTAB
    14   structure Syntax: SYNTAX
    15   structure Type: TYPE
    16   sharing Symtab = Type.Symtab
    17   local open Type Syntax Syntax.Mixfix in
    18     type sg
    19     val rep_sg: sg ->
    20       {tsig: type_sig,
    21        const_tab: typ Symtab.table,
    22        syn: syntax,
    23        stamps: string ref list}
    24     val subsig: sg * sg -> bool
    25     val eq_sg: sg * sg -> bool
    26     val is_draft: sg -> bool
    27     val const_type: sg -> string -> typ option
    28     val print_sg: sg -> unit
    29     val pprint_sg: sg -> pprint_args -> unit
    30     val pretty_term: sg -> term -> Pretty.T
    31     val pretty_typ: sg -> typ -> 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 add_classes: (class list * class * class list) list -> sg -> sg
    40     val add_defsort: sort -> sg -> sg
    41     val add_types: (string * int * mixfix) list -> sg -> sg
    42     val add_tyabbrs: (string * string list * string * mixfix) list -> sg -> sg
    43     val add_tyabbrs_i: (string * string list * typ * mixfix) list -> sg -> sg
    44     val add_arities: (string * sort list * sort) list -> sg -> sg
    45     val add_consts: (string * string * mixfix) list -> sg -> sg
    46     val add_consts_i: (string * typ * mixfix) list -> sg -> sg
    47     val add_syntax: (string * string * mixfix) list -> sg -> sg
    48     val add_syntax_i: (string * typ * mixfix) list -> sg -> sg
    49     val add_trfuns:
    50       (string * (ast list -> ast)) list *
    51       (string * (term list -> term)) list *
    52       (string * (term list -> term)) list *
    53       (string * (ast list -> ast)) list -> sg -> sg
    54     val add_trrules: xrule list -> sg -> sg
    55     val add_name: string -> sg -> sg
    56     val make_draft: sg -> sg
    57     val extend: sg -> string ->
    58       (class * class list) list * class list *
    59       (string list * int) list *
    60       (string * string list * string) list *
    61       (string list * (sort list * class)) list *
    62       (string list * string) list * sext option -> sg
    63     val merge: sg * sg -> sg
    64     val pure: sg
    65     val const_of_class: class -> string
    66     val class_of_const: string -> class
    67   end
    68 end;
    69 
    70 functor SignFun(structure Syntax: SYNTAX and Type: TYPE): SIGN =
    71 struct
    72 
    73 structure Symtab = Type.Symtab;
    74 structure Syntax = Syntax;
    75 structure BasicSyntax: BASIC_SYNTAX = Syntax;
    76 structure Pretty = Syntax.Pretty;
    77 structure Type = Type;
    78 open BasicSyntax Type;
    79 open Syntax.Mixfix;   (* FIXME *)
    80 
    81 
    82 (** datatype sg **)
    83 
    84 (*the "ref" in stamps ensures that no two signatures are identical -- it is
    85   impossible to forge a signature*)
    86 
    87 datatype sg =
    88   Sg of {
    89     tsig: type_sig,                 (*order-sorted signature of types*)
    90     const_tab: typ Symtab.table,    (*types of constants*)
    91     syn: Syntax.syntax,             (*syntax for parsing and printing*)
    92     stamps: string ref list};       (*unique theory indentifier*)
    93 
    94 fun rep_sg (Sg args) = args;
    95 
    96 
    97 fun is_draft (Sg {stamps = ref "#" :: _, ...}) = true
    98   | is_draft _ = false;
    99 
   100 fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = s1 subset s2;
   101 
   102 fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2);
   103 
   104 
   105 fun const_type (Sg {const_tab, ...}) c =
   106   Symtab.lookup (const_tab, c);
   107 
   108 
   109 
   110 (** print signature **)
   111 
   112 val stamp_names = rev o map !;
   113 
   114 fun print_sg sg =
   115   let
   116     fun prt_typ syn ty = Pretty.quote (Syntax.pretty_typ syn ty);
   117 
   118     fun pretty_sort [cl] = Pretty.str cl
   119       | pretty_sort cls = Pretty.str_list "{" "}" cls;
   120 
   121     fun pretty_subclass (cl, cls) = Pretty.block
   122       [Pretty.str (cl ^ " <"), Pretty.brk 1, pretty_sort cls];
   123 
   124     fun pretty_default cls = Pretty.block
   125       [Pretty.str "default:", Pretty.brk 1, pretty_sort cls];
   126 
   127     fun pretty_arg (ty, n) = Pretty.str (ty ^ " " ^ string_of_int n);
   128 
   129     fun pretty_abbr syn (ty, (vs, rhs)) = Pretty.block
   130       [prt_typ syn (Type (ty, map (fn v => TVar (v, [])) vs)),
   131         Pretty.str " =", Pretty.brk 1, prt_typ syn rhs];
   132 
   133     fun pretty_arity ty (cl, []) = Pretty.block
   134           [Pretty.str (ty ^ " ::"), Pretty.brk 1, Pretty.str cl]
   135       | pretty_arity ty (cl, srts) = Pretty.block
   136           [Pretty.str (ty ^ " ::"), Pretty.brk 1,
   137             Pretty.list "(" ")" (map pretty_sort srts),
   138             Pretty.brk 1, Pretty.str cl];
   139 
   140     fun pretty_coreg (ty, ars) = map (pretty_arity ty) ars;
   141 
   142     fun pretty_const syn (c, ty) = Pretty.block
   143       [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ syn ty];
   144 
   145 
   146     val Sg {tsig, const_tab, syn, stamps} = sg;
   147     val {classes, subclass, default, args, abbrs, coreg} = rep_tsig tsig;
   148   in
   149     Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps));
   150     Pretty.writeln (Pretty.strs ("classes:" :: classes));
   151     Pretty.writeln (Pretty.big_list "subclass:" (map pretty_subclass subclass));
   152     Pretty.writeln (pretty_default default);
   153     Pretty.writeln (Pretty.big_list "types:" (map pretty_arg args));
   154     Pretty.writeln (Pretty.big_list "abbrs:" (map (pretty_abbr syn) abbrs));
   155     Pretty.writeln (Pretty.big_list "coreg:" (flat (map pretty_coreg coreg)));
   156     Pretty.writeln (Pretty.big_list "consts:"
   157       (map (pretty_const syn) (Symtab.dest const_tab)))
   158   end;
   159 
   160 
   161 fun pprint_sg (Sg {stamps, ...}) =
   162   Pretty.pprint (Pretty.str_list "{" "}" (stamp_names stamps));
   163 
   164 
   165 
   166 (** pretty printing of terms and types **)
   167 
   168 fun pretty_term (Sg {syn, ...}) = Syntax.pretty_term syn;
   169 fun pretty_typ (Sg {syn, ...}) = Syntax.pretty_typ syn;
   170 
   171 fun string_of_term (Sg {syn, ...}) = Syntax.string_of_term syn;
   172 fun string_of_typ (Sg {syn, ...}) = Syntax.string_of_typ syn;
   173 
   174 fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg);
   175 fun pprint_typ sg = Pretty.pprint o Pretty.quote o (pretty_typ sg);
   176 
   177 
   178 
   179 (** certify types and terms **)   (*exception TYPE*)
   180 
   181 fun certify_typ (Sg {tsig, ...}) ty = cert_typ tsig ty;
   182 
   183 
   184 fun mapfilt_atoms f (Abs (_, _, t)) = mapfilt_atoms f t
   185   | mapfilt_atoms f (t $ u) = mapfilt_atoms f t @ mapfilt_atoms f u
   186   | mapfilt_atoms f a = (case f a of Some y => [y] | None => []);
   187 
   188 fun certify_term (sg as Sg {tsig, ...}) tm =
   189   let
   190     fun valid_const a T =
   191       (case const_type sg a of
   192         Some U => typ_instance (tsig, T, U)
   193       | _ => false);
   194 
   195     fun atom_err (Const (a, T)) =
   196           if valid_const a T then None
   197           else Some ("Illegal type for constant " ^ quote a ^ " :: " ^
   198             quote (string_of_typ sg T))
   199       | atom_err (Var ((x, i), _)) =
   200           if i < 0 then Some ("Negative index for Var " ^ quote x) else None
   201       | atom_err _ = None;
   202 
   203     val norm_tm =
   204       (case it_term_types (typ_errors tsig) (tm, []) of
   205         [] => map_term_types (norm_typ tsig) tm
   206       | errs => raise_type (cat_lines errs) [] [tm]);
   207   in
   208     (case mapfilt_atoms atom_err norm_tm of
   209       [] => (norm_tm, type_of norm_tm, maxidx_of_term norm_tm)
   210     | errs => raise_type (cat_lines errs) [] [norm_tm])
   211   end;
   212 
   213 
   214 
   215 (** read types **)    (*exception ERROR*)
   216 
   217 (* FIXME rd_typ vs. read_raw_typ (?) *)
   218 
   219 fun rd_typ tsig syn sort_of s =
   220   let
   221     val def_sort = defaultS tsig;
   222     val raw_ty =        (*this may raise ERROR, too!*)
   223       Syntax.read_typ syn (fn x => if_none (sort_of x) def_sort) s;
   224   in
   225     cert_typ tsig raw_ty
   226       handle TYPE (msg, _, _) => error msg
   227   end
   228   handle ERROR => error ("The error(s) above occurred in type " ^ quote s);
   229 
   230 fun read_typ (Sg {tsig, syn, ...}, sort_of) s = rd_typ tsig syn sort_of s;
   231 
   232 
   233 
   234 (** extend signature **)    (*exception ERROR*)
   235 
   236 (* FIXME -> type.ML *)
   237 
   238 (* FIXME replace? *)
   239 fun varify_typ (Type (t, tys)) = Type (t, map varify_typ tys)
   240   | varify_typ (TFree (a, s)) = TVar ((a, 0), s)
   241   | varify_typ (ty as TVar _) =
   242       raise_type "Illegal schematic type variable" [ty] [];
   243 
   244 
   245 (* fake newstyle interfaces *) (* FIXME -> type.ML *)
   246 
   247 fun ext_tsig_classes tsig classes =
   248   if exists (fn ([], _, _) => false | _ => true) classes then
   249     sys_error "FIXME ext_tsig_classes"
   250   else
   251     extend_tsig tsig (map (fn (_, c, cs) => (c, cs)) classes, [], [], []);
   252 
   253 fun ext_tsig_defsort tsig defsort =
   254   extend_tsig tsig ([], defsort, [], []);
   255 
   256 fun ext_tsig_types tsig types =
   257   extend_tsig tsig ([], [], map (fn (t, n) => ([t], n)) types, []);
   258 
   259 (* FIXME varify_typ, rem_sorts; norm_typ (?) *)
   260 fun ext_tsig_abbrs tsig abbrs = Type.ext_tsig_abbrs tsig
   261   (map (fn (t, vs, rhs) => (t, (map (rpair 0) vs, varifyT rhs))) abbrs);
   262 
   263 fun ext_tsig_arities tsig arities = extend_tsig tsig
   264   ([], [], [], flat (map (fn (t, ss, cs) => map (fn c => ([t], (ss, c))) cs) arities));
   265 
   266 
   267 
   268 (** read types **)  (*exception ERROR*)
   269 
   270 fun err_in_type s =
   271   error ("The error(s) above occurred in type " ^ quote s);
   272 
   273 fun read_raw_typ syn tsig sort_of str =
   274   Syntax.read_typ syn (fn x => if_none (sort_of x) (defaultS tsig)) str
   275     handle ERROR => err_in_type str;
   276 
   277 (*read and certify typ wrt a signature*)
   278 fun read_typ (Sg {tsig, syn, ...}, sort_of) str =
   279   cert_typ tsig (read_raw_typ syn tsig sort_of str)
   280     handle TYPE (msg, _, _) => (writeln msg; err_in_type str);
   281 
   282 
   283 
   284 (** extension functions **)  (*exception ERROR*)
   285 
   286 fun decls_of name_of mfixs =
   287   map (fn (x, y, mx) => (name_of x mx, y)) mfixs;
   288 
   289 
   290 (* add default sort *)
   291 
   292 fun ext_defsort (syn, tsig, ctab) defsort =
   293   (syn, ext_tsig_defsort tsig defsort, ctab);
   294 
   295 
   296 (* add type constructors *)
   297 
   298 fun ext_types (syn, tsig, ctab) types =
   299   (Syntax.extend_type_gram syn types,
   300     ext_tsig_types tsig (decls_of type_name types),
   301     ctab);
   302 
   303 
   304 (* add type abbreviations *)
   305 
   306 fun read_abbr syn tsig (t, vs, rhs_src) =
   307   (t, vs, read_raw_typ syn tsig (K None) rhs_src)
   308     handle ERROR => error ("in type abbreviation " ^ t);
   309 
   310 fun ext_abbrs rd_abbr (syn, tsig, ctab) abbrs =
   311   let
   312     fun mfix_of (t, vs, _, mx) = (t, length vs, mx);
   313     val syn1 = Syntax.extend_type_gram syn (map mfix_of abbrs);
   314 
   315     fun decl_of (t, vs, rhs, mx) =
   316       rd_abbr syn1 tsig (type_name t mx, vs, rhs);
   317   in
   318     (syn1, ext_tsig_abbrs tsig (map decl_of abbrs), ctab)
   319   end;
   320 
   321 val ext_tyabbrs_i = ext_abbrs (K (K I));
   322 val ext_tyabbrs = ext_abbrs read_abbr;
   323 
   324 
   325 (* add type arities *)
   326 
   327 fun ext_arities (syn, tsig, ctab) arities =
   328   let
   329     val tsig1 = ext_tsig_arities tsig arities;
   330     val log_types = logical_types tsig1;
   331   in
   332     (Syntax.extend_log_types syn log_types, tsig1, ctab)
   333   end;
   334 
   335 
   336 (* add term constants and syntax *)
   337 
   338 fun err_in_const c =
   339   error ("in declaration of constant " ^ quote c);
   340 
   341 fun err_dup_consts cs =
   342   error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
   343 
   344 
   345 fun read_const syn tsig (c, ty_src, mx) =
   346   (c, read_raw_typ syn tsig (K None) ty_src, mx)
   347     handle ERROR => err_in_const (const_name c mx);
   348 
   349 fun ext_cnsts rd_const syn_only (syn, tsig, ctab) raw_consts =
   350   let
   351     fun prep_const (c, ty, mx) = (c, cert_typ tsig (varify_typ ty), mx)
   352       handle TYPE (msg, _, _) => (writeln msg; err_in_const (const_name c mx));
   353 
   354     val consts = map (prep_const o rd_const syn tsig) raw_consts;
   355     val decls =
   356       if syn_only then []
   357       else filter_out (equal "" o fst) (decls_of const_name consts);
   358   in
   359     (Syntax.extend_const_gram syn consts, tsig,
   360       Symtab.extend_new (ctab, decls)
   361         handle Symtab.DUPS cs => err_dup_consts cs)
   362   end;
   363 
   364 val ext_consts_i = ext_cnsts (K (K I)) false;
   365 val ext_consts = ext_cnsts read_const false;
   366 val ext_syntax_i = ext_cnsts (K (K I)) true;
   367 val ext_syntax = ext_cnsts read_const true;
   368 
   369 
   370 (* add type classes *)
   371 
   372 fun const_of_class c = c ^ "_class";
   373 
   374 fun class_of_const c_class =
   375   let
   376     val c = implode (take (size c_class - 6, explode c_class));
   377   in
   378     if const_of_class c = c_class then c
   379     else raise_term ("class_of_const: bad name " ^ quote c_class) []
   380   end;
   381 
   382 
   383 fun ext_classes (syn, tsig, ctab) classes =
   384   let
   385     val names = map (fn (_, c, _) => c) classes;
   386     val consts =
   387       map (fn c => (const_of_class c, a_itselfT --> propT, NoSyn)) names;
   388   in
   389     ext_consts_i
   390       (Syntax.extend_consts syn names, ext_tsig_classes tsig classes, ctab)
   391       consts
   392   end;
   393 
   394 
   395 (* add syntactic translations *)
   396 
   397 fun ext_trfuns (syn, tsig, ctab) trfuns =
   398   (Syntax.extend_trfuns syn trfuns, tsig, ctab);
   399 
   400 fun ext_trrules (syn, tsig, ctab) xrules =
   401   (Syntax.extend_trrules syn xrules, tsig, ctab);
   402 
   403 
   404 (* build signature *)
   405 
   406 (* FIXME debug *)
   407 fun assert_stamps_ok stamps =
   408   let val names = map ! stamps;
   409   in
   410     if not (null (duplicates stamps)) then
   411       error "DEBUG dup stamps"
   412     else if not (null (duplicates names)) then
   413       error "DEBUG dup stamp names"
   414     else if not (null names) andalso exists (equal "#") (tl names) then
   415       error "DEBUG misplaced draft stamp name"
   416     else stamps
   417   end;
   418 
   419 fun ext_stamps stamps name =
   420   let
   421     val stmps = (case stamps of ref "#" :: ss => ss | ss => ss);
   422   in
   423     if exists (equal name o !) stmps then
   424       error ("Theory already contains a " ^ quote name ^ " component")
   425     else assert_stamps_ok (ref name :: stmps)
   426   end;
   427 
   428 
   429 fun make_sign (syn, tsig, ctab) stamps name =
   430   Sg {tsig = tsig, const_tab = ctab, syn = syn,
   431     stamps = ext_stamps stamps name};
   432 
   433 fun extend_sign extfun name decls (Sg {tsig, const_tab, syn, stamps}) =
   434   make_sign (extfun (syn, tsig, const_tab) decls) stamps name;
   435 
   436 
   437 (* the external interfaces *)
   438 
   439 val add_classes   = extend_sign ext_classes "#";
   440 val add_defsort   = extend_sign ext_defsort "#";
   441 val add_types     = extend_sign ext_types "#";
   442 val add_tyabbrs   = extend_sign ext_tyabbrs "#";
   443 val add_tyabbrs_i = extend_sign ext_tyabbrs_i "#";
   444 val add_arities   = extend_sign ext_arities "#";
   445 val add_consts    = extend_sign ext_consts "#";
   446 val add_consts_i  = extend_sign ext_consts_i "#";
   447 val add_syntax    = extend_sign ext_syntax "#";
   448 val add_syntax_i  = extend_sign ext_syntax_i "#";
   449 val add_trfuns    = extend_sign ext_trfuns "#";
   450 val add_trrules   = extend_sign ext_trrules "#";
   451 
   452 fun add_name name sg = extend_sign K name () sg;
   453 val make_draft = add_name "#";
   454 
   455 
   456 
   457 (** extend signature (old) **)      (* FIXME remove *)
   458 
   459 fun extend sg name (classes, default, types, abbrs, arities, consts, opt_sext) =
   460   let
   461     fun read_abbr syn (c, vs, rhs_src) =
   462       (c, (map (rpair 0) vs, varifyT (Syntax.read_typ syn (K []) rhs_src)))
   463         handle ERROR => error ("The error(s) above occurred in the rhs " ^
   464           quote rhs_src ^ "\nof type abbreviation " ^ quote c);
   465 
   466     (*reset TVar indices to 0, renaming to preserve distinctness*)
   467     fun zero_tvar_idxs T =
   468       let
   469         val inxSs = typ_tvars T;
   470         val nms' = variantlist (map (#1 o #1) inxSs, []);
   471         val tye = map2 (fn ((v, S), a) => (v, TVar ((a, 0), S))) (inxSs, nms');
   472       in
   473         typ_subst_TVars tye T
   474       end;
   475 
   476     (*read and check the type mentioned in a const declaration; zero type var
   477       indices because type inference requires it*)
   478     fun read_const tsig syn (c, s) =
   479       (c, zero_tvar_idxs (varifyT (rd_typ tsig syn (K None) s)))
   480         handle ERROR => error ("in declaration of constant " ^ quote c);
   481 
   482 
   483     val Sg {tsig, const_tab, syn, stamps} = sg;
   484     val xconsts = map #1 classes @ flat (map #1 types) @ map #1 abbrs @
   485       flat (map #1 consts);
   486     val sext = if_none opt_sext Syntax.empty_sext;
   487 
   488     val tsig' = extend_tsig tsig (classes, default, types, arities);
   489     val tsig1 = Type.ext_tsig_abbrs tsig' (map (read_abbr syn) abbrs);
   490 
   491     val syn1 = Syntax.extend syn (rd_typ tsig1 syn (K None))
   492       (logical_types tsig1, xconsts, sext);
   493 
   494     val all_consts = flat (map (fn (cs, s) => map (rpair s) cs)
   495       (Syntax.constants sext @ consts));
   496 
   497     val const_tab1 =
   498       Symtab.extend_new (const_tab, map (read_const tsig1 syn) all_consts)
   499         handle Symtab.DUPS cs => err_dup_consts cs;
   500 
   501     val stamps1 = ext_stamps stamps name;
   502   in
   503     Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1, stamps = stamps1}
   504   end;
   505 
   506 
   507 
   508 (** merge signatures **)    (*exception TERM*)
   509 
   510 fun merge (sg1, sg2) =
   511   if subsig (sg2, sg1) then sg1
   512   else if subsig (sg1, sg2) then sg2
   513   else if is_draft sg1 orelse is_draft sg2 then
   514     raise_term "Illegal merge of draft signatures" []
   515   else
   516     (*neither is union already; must form union*)
   517     let
   518       val Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1,
   519         stamps = stamps1} = sg1;
   520       val Sg {tsig = tsig2, const_tab = const_tab2, syn = syn2,
   521         stamps = stamps2} = sg2;
   522 
   523 
   524       val tsig = merge_tsigs (tsig1, tsig2);
   525 
   526       val const_tab = Symtab.merge (op =) (const_tab1, const_tab2)
   527         handle Symtab.DUPS cs =>
   528           raise_term ("Incompatible types for constant(s) " ^ commas_quote cs) [];
   529 
   530       val syn = Syntax.merge_syntaxes syn1 syn2;
   531 
   532       val stamps = merge_rev_lists stamps1 stamps2;
   533       val dups = duplicates (stamp_names stamps);
   534     in
   535       if null dups then assert_stamps_ok stamps    (* FIXME debug *)
   536       else raise_term ("Attempt to merge different versions of theories " ^
   537         commas_quote dups) [];
   538       Sg {tsig = tsig, const_tab = const_tab, syn = syn, stamps = stamps}
   539     end;
   540 
   541 
   542 
   543 (** the Pure signature **)
   544 
   545 val pure =
   546   make_sign (Syntax.type_syn, tsig0, Symtab.null) [] "#"
   547   also add_types
   548    (("fun", 2, NoSyn) ::
   549     ("prop", 0, NoSyn) ::
   550     ("itself", 1, NoSyn) ::
   551     Syntax.Mixfix.pure_types)
   552   also add_classes [([], logicC, [])]
   553   also add_defsort logicS
   554   also add_arities
   555    [("fun", [logicS, logicS], logicS),
   556     ("prop", [], logicS),
   557     ("itself", [logicS], logicS)]
   558   also add_syntax Syntax.Mixfix.pure_syntax
   559   also add_trfuns Syntax.pure_trfuns
   560   also add_consts
   561    [("==", "['a::{}, 'a] => prop", Mixfix ("(_ ==/ _)", [3, 2], 2)),
   562     ("=?=", "['a::{}, 'a] => prop", Mixfix ("(_ =?=/ _)", [3, 2], 2)),
   563     ("==>", "[prop, prop] => prop", Mixfix ("(_ ==>/ _)", [2, 1], 1)),
   564     ("all", "('a => prop) => prop", Binder ("!!", 0)),
   565     ("TYPE", "'a itself", NoSyn),
   566     (Syntax.constrainC, "'a::{} => 'a", NoSyn)]
   567   also add_name "Pure";
   568 
   569 
   570 end;
   571