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