src/Pure/Syntax/sextension.ML
author paulson
Thu Sep 25 12:09:41 1997 +0200 (1997-09-25)
changeset 3706 e57b5902822f
parent 473 fdacecc688a1
permissions -rw-r--r--
Generalized and exported biresolution_from_nets_tac to allow the declaration
of Clarify_tac
     1 (*  Title:      Pure/Syntax/sextension.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 
     5 Syntax extensions (external interface): mixfix declarations, infixes,
     6 binders, translation rules / functions and the Pure syntax.
     7 
     8 TODO:
     9   move ast_to_term, pt_to_ast (?)
    10 *)
    11 
    12 infix |-> <-| <->;
    13 
    14 signature SEXTENSION0 =
    15 sig
    16   structure Parser: PARSER
    17   local open Parser.SynExt.Ast in
    18     datatype mixfix =
    19       Mixfix of string * string * string * int list * int |
    20       Delimfix of string * string * string |
    21       Infixl of string * string * int |
    22       Infixr of string * string * int |
    23       Binder of string * string * string * int * int |
    24       TInfixl of string * string * int |
    25       TInfixr of string * string * int
    26     datatype xrule =
    27       op |-> of (string * string) * (string * string) |
    28       op <-| of (string * string) * (string * string) |
    29       op <-> of (string * string) * (string * string)
    30     datatype sext =
    31       Sext of {
    32         mixfix: mixfix list,
    33         parse_translation: (string * (term list -> term)) list,
    34         print_translation: (string * (term list -> term)) list} |
    35       NewSext of {
    36         mixfix: mixfix list,
    37         xrules: xrule list,
    38         parse_ast_translation: (string * (ast list -> ast)) list,
    39         parse_translation: (string * (term list -> term)) list,
    40         print_translation: (string * (term list -> term)) list,
    41         print_ast_translation: (string * (ast list -> ast)) list}
    42     val eta_contract: bool ref
    43     val mk_binder_tr: string * string -> string * (term list -> term)
    44     val mk_binder_tr': string * string -> string * (term list -> term)
    45     val dependent_tr': string * string -> term list -> term
    46     val max_pri: int
    47   end
    48 end;
    49 
    50 signature SEXTENSION1 =
    51 sig
    52   include SEXTENSION0
    53   local open Parser.SynExt.Ast in
    54     val empty_sext: sext
    55     val simple_sext: mixfix list -> sext
    56     val constants: sext -> (string list * string) list
    57     val pure_sext: sext
    58     val syntax_types: string list
    59     val syntax_consts: (string list * string) list
    60     val constrainAbsC: string
    61     val pure_trfuns:
    62       (string * (ast list -> ast)) list *
    63       (string * (term list -> term)) list *
    64       (string * (term list -> term)) list *
    65       (string * (ast list -> ast)) list
    66   end
    67 end;
    68 
    69 signature SEXTENSION =
    70 sig
    71   include SEXTENSION1
    72   local open Parser Parser.SynExt Parser.SynExt.Ast in
    73     val xrules_of: sext -> xrule list
    74     val abs_tr': term -> term
    75     val prop_tr': bool -> term -> term
    76     val appl_ast_tr': ast * ast list -> ast
    77     val syn_ext_of_sext: string list -> string list -> string list -> (string -> typ) -> sext -> syn_ext
    78     val pt_to_ast: (string -> (ast list -> ast) option) -> parsetree -> ast
    79     val ast_to_term: (string -> (term list -> term) option) -> ast -> term
    80   end
    81 end;
    82 
    83 functor SExtensionFun(structure TypeExt: TYPE_EXT and Parser: PARSER
    84   sharing TypeExt.SynExt = Parser.SynExt): SEXTENSION =
    85 struct
    86 
    87 structure Parser = Parser;
    88 open TypeExt Parser.Lexicon Parser.SynExt.Ast Parser.SynExt Parser;
    89 
    90 
    91 (** datatype sext **)   (* FIXME remove *)
    92 
    93 datatype mixfix =
    94   Mixfix of string * string * string * int list * int |
    95   Delimfix of string * string * string |
    96   Infixl of string * string * int |
    97   Infixr of string * string * int |
    98   Binder of string * string * string * int * int |
    99   TInfixl of string * string * int |
   100   TInfixr of string * string * int;
   101 
   102 
   103 (* FIXME -> syntax.ML, BASIC_SYNTAX, SYNTAX *)
   104 datatype xrule =
   105   op |-> of (string * string) * (string * string) |
   106   op <-| of (string * string) * (string * string) |
   107   op <-> of (string * string) * (string * string);
   108 
   109 datatype sext =
   110   Sext of {
   111     mixfix: mixfix list,
   112     parse_translation: (string * (term list -> term)) list,
   113     print_translation: (string * (term list -> term)) list} |
   114   NewSext of {
   115     mixfix: mixfix list,
   116     xrules: xrule list,
   117     parse_ast_translation: (string * (ast list -> ast)) list,
   118     parse_translation: (string * (term list -> term)) list,
   119     print_translation: (string * (term list -> term)) list,
   120     print_ast_translation: (string * (ast list -> ast)) list};
   121 
   122 
   123 (* simple_sext *)
   124 
   125 fun simple_sext mixfix =
   126   Sext {mixfix = mixfix, parse_translation = [], print_translation = []};
   127 
   128 
   129 (* empty_sext *)
   130 
   131 val empty_sext = simple_sext [];
   132 
   133 
   134 (* sext_components *)
   135 
   136 fun sext_components (Sext {mixfix, parse_translation, print_translation}) =
   137       {mixfix = mixfix,
   138         xrules = [],
   139         parse_ast_translation = [],
   140         parse_translation = parse_translation,
   141         print_translation = print_translation,
   142         print_ast_translation = []}
   143   | sext_components (NewSext cmps) = cmps;
   144 
   145 
   146 (* mixfix_of *)
   147 
   148 fun mixfix_of (Sext {mixfix, ...}) = mixfix
   149   | mixfix_of (NewSext {mixfix, ...}) = mixfix;
   150 
   151 
   152 (* xrules_of *)
   153 
   154 fun xrules_of (Sext _) = []
   155   | xrules_of (NewSext {xrules, ...}) = xrules;
   156 
   157 
   158 
   159 (*** translation functions ***) (* FIXME -> trans.ML *)
   160 
   161 fun const c = Const (c, dummyT);
   162 
   163 
   164 (** parse (ast) translations **)
   165 
   166 (* application *)
   167 
   168 fun appl_ast_tr (*"_appl"*) [f, args] = Appl (f :: unfold_ast "_args" args)
   169   | appl_ast_tr (*"_appl"*) asts = raise_ast "appl_ast_tr" asts;
   170 
   171 
   172 (* abstraction *)
   173 
   174 fun idtyp_ast_tr (*"_idtyp"*) [x, ty] = Appl [Constant constrainC, x, ty]
   175   | idtyp_ast_tr (*"_idtyp"*) asts = raise_ast "idtyp_ast_tr" asts;
   176 
   177 fun lambda_ast_tr (*"_lambda"*) [idts, body] =
   178       fold_ast_p "_abs" (unfold_ast "_idts" idts, body)
   179   | lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts;
   180 
   181 fun abs_tr (*"_abs"*) [Free (x, T), body] = absfree (x, T, body)
   182   | abs_tr (*"_abs"*) (ts as [Const (c, _) $ Free (x, T) $ tT, body]) =
   183       if c = constrainC then
   184         const "_constrainAbs" $ absfree (x, T, body) $ tT
   185       else raise_term "abs_tr" ts
   186   | abs_tr (*"_abs"*) ts = raise_term "abs_tr" ts;
   187 
   188 
   189 (* nondependent abstraction *)
   190 
   191 fun k_tr (*"_K"*) [t] = Abs ("uu", dummyT, incr_boundvars 1 t)
   192   | k_tr (*"_K"*) ts = raise_term "k_tr" ts;
   193 
   194 
   195 (* binder *)
   196 
   197 fun mk_binder_tr (sy, name) =
   198   let
   199     fun tr (Free (x, T), t) = const name $ absfree (x, T, t)
   200       | tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t))
   201       | tr (t1 as Const (c, _) $ Free (x, T) $ tT, t) =
   202           if c = constrainC then
   203             const name $ (const "_constrainAbs" $ absfree (x, T, t) $ tT)
   204           else raise_term "binder_tr" [t1, t]
   205       | tr (t1, t2) = raise_term "binder_tr" [t1, t2];
   206 
   207     fun binder_tr (*sy*) [idts, body] = tr (idts, body)
   208       | binder_tr (*sy*) ts = raise_term "binder_tr" ts;
   209   in
   210     (sy, binder_tr)
   211   end;
   212 
   213 
   214 (* meta propositions *)
   215 
   216 fun aprop_tr (*"_aprop"*) [t] = const constrainC $ t $ const "prop"
   217   | aprop_tr (*"_aprop"*) ts = raise_term "aprop_tr" ts;
   218 
   219 fun ofclass_tr (*"_ofclass"*) [ty, cls] =
   220       cls $ (const constrainC $ const "TYPE" $ (const "itself" $ ty))
   221   | ofclass_tr (*"_ofclass"*) ts = raise_term "ofclass_tr" ts;
   222 
   223 
   224 (* meta implication *)
   225 
   226 fun bigimpl_ast_tr (*"_bigimpl"*) [asms, concl] =
   227       fold_ast_p "==>" (unfold_ast "_asms" asms, concl)
   228   | bigimpl_ast_tr (*"_bigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
   229 
   230 
   231 (* explode atoms *)
   232 
   233 fun explode_tr (*"_explode"*) (ts as [consC, nilC, bit0, bit1, txt]) =
   234       let
   235         fun mk_list [] = nilC
   236           | mk_list (t :: ts) = consC $ t $ mk_list ts;
   237 
   238         fun encode_bit 0 = bit0
   239           | encode_bit 1 = bit1
   240           | encode_bit _ = sys_error "encode_bit";
   241 
   242         fun encode_char c =   (* FIXME leading 0s (?) *)
   243           mk_list (map encode_bit (radixpand (2, (ord c))));
   244 
   245         val str =
   246           (case txt of
   247             Free (s, _) => s
   248           | Const (s, _) => s
   249           | _ => raise_term "explode_tr" ts);
   250       in
   251         mk_list (map encode_char (explode str))
   252       end
   253   | explode_tr (*"_explode"*) ts = raise_term "explode_tr" ts;
   254 
   255 
   256 
   257 (** print (ast) translations **)
   258 
   259 (* application *)
   260 
   261 fun appl_ast_tr' (f, []) = raise_ast "appl_ast_tr'" [f]
   262   | appl_ast_tr' (f, args) = Appl [Constant "_appl", f, fold_ast "_args" args];
   263 
   264 
   265 (* abstraction *)
   266 
   267 fun strip_abss vars_of body_of tm =
   268   let
   269     fun free (x, _) = Free (x, dummyT);
   270 
   271     val vars = vars_of tm;
   272     val body = body_of tm;
   273     val rev_new_vars = rename_wrt_term body vars;
   274   in
   275     (map Free (rev rev_new_vars), subst_bounds (map free rev_new_vars, body))
   276   end;
   277 
   278 (*do (partial) eta-contraction before printing*)
   279 
   280 val eta_contract = ref false;
   281 
   282 fun eta_contr tm =
   283   let
   284     fun eta_abs (Abs (a, T, t)) =
   285           (case eta_abs t of
   286             t' as f $ u =>
   287               (case eta_abs u of
   288                 Bound 0 =>
   289                   if not (0 mem loose_bnos f) then incr_boundvars ~1 f
   290                   else Abs (a, T, t')
   291               | _ => Abs (a, T, t'))
   292           | t' => Abs (a, T, t'))
   293       | eta_abs t = t;
   294   in
   295     if ! eta_contract then eta_abs tm else tm
   296   end;
   297 
   298 
   299 fun abs_tr' tm =
   300   foldr (fn (x, t) => const "_abs" $ x $ t)
   301     (strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
   302 
   303 
   304 fun abs_ast_tr' (*"_abs"*) asts =
   305   (case unfold_ast_p "_abs" (Appl (Constant "_abs" :: asts)) of
   306     ([], _) => raise_ast "abs_ast_tr'" asts
   307   | (xs, body) => Appl [Constant "_lambda", fold_ast "_idts" xs, body]);
   308 
   309 
   310 (* binder *)
   311 
   312 fun mk_binder_tr' (name, sy) =
   313   let
   314     fun mk_idts [] = raise Match    (*abort translation*)
   315       | mk_idts [idt] = idt
   316       | mk_idts (idt :: idts) = const "_idts" $ idt $ mk_idts idts;
   317 
   318     fun tr' t =
   319       let
   320         val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
   321       in
   322         const sy $ mk_idts xs $ bd
   323       end;
   324 
   325     fun binder_tr' (*name*) (t :: ts) =
   326           list_comb (tr' (const name $ t), ts)
   327       | binder_tr' (*name*) [] = raise Match;
   328   in
   329     (name, binder_tr')
   330   end;
   331 
   332 
   333 (* idts *)
   334 
   335 fun idts_ast_tr' (*"_idts"*) [Appl [Constant c, x, ty], xs] =
   336       if c = constrainC then
   337         Appl [Constant "_idts", Appl [Constant "_idtyp", x, ty], xs]
   338       else raise Match
   339   | idts_ast_tr' (*"_idts"*) _ = raise Match;
   340 
   341 
   342 (* meta propositions *)
   343 
   344 fun prop_tr' show_sorts tm =
   345   let
   346     fun aprop t = const "_aprop" $ t;
   347 
   348     fun is_prop tys t =
   349       fastype_of1 (tys, t) = propT handle TERM _ => false;
   350 
   351     fun tr' _ (t as Const _) = t
   352       | tr' _ (t as Free (x, ty)) =
   353           if ty = propT then aprop (Free (x, dummyT)) else t
   354       | tr' _ (t as Var (xi, ty)) =
   355           if ty = propT then aprop (Var (xi, dummyT)) else t
   356       | tr' tys (t as Bound _) =
   357           if is_prop tys t then aprop t else t
   358       | tr' tys (Abs (x, ty, t)) = Abs (x, ty, tr' (ty :: tys) t)
   359       | tr' tys (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [ty])))) =
   360           if is_prop tys t then
   361             const "_ofclass" $ term_of_typ show_sorts ty $ tr' tys t1
   362           else tr' tys t1 $ tr' tys t2
   363       | tr' tys (t as t1 $ t2) =
   364           (if is_Const (head_of t) orelse not (is_prop tys t)
   365             then I else aprop) (tr' tys t1 $ tr' tys t2);
   366   in
   367     tr' [] tm
   368   end;
   369 
   370 
   371 (* meta implication *)
   372 
   373 fun impl_ast_tr' (*"==>"*) asts =
   374   (case unfold_ast_p "==>" (Appl (Constant "==>" :: asts)) of
   375     (asms as _ :: _ :: _, concl)
   376       => Appl [Constant "_bigimpl", fold_ast "_asms" asms, concl]
   377   | _ => raise Match);
   378 
   379 
   380 (* dependent / nondependent quantifiers *)
   381 
   382 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
   383       if 0 mem (loose_bnos B) then
   384         let val (x', B') = variant_abs (x, dummyT, B);
   385         in list_comb (const q $ Free (x', T) $ A $ B', ts) end
   386       else list_comb (const r $ A $ B, ts)
   387   | dependent_tr' _ _ = raise Match;
   388 
   389 
   390 (* implode atoms *)
   391 
   392 fun implode_ast_tr' (*"_implode"*) (asts as [Constant cons_name, nilC,
   393     bit0, bit1, bitss]) =
   394       let
   395         fun err () = raise_ast "implode_ast_tr'" asts;
   396 
   397         fun strip_list lst =
   398           let val (xs, y) = unfold_ast_p cons_name lst
   399           in if y = nilC then xs else err ()
   400           end;
   401 
   402         fun decode_bit bit =
   403           if bit = bit0 then "0"
   404           else if bit = bit1 then "1"
   405           else err ();
   406 
   407         fun decode_char bits =
   408           chr (#1 (scan_radixint (2, map decode_bit (strip_list bits))));
   409       in
   410         Variable (implode (map decode_char (strip_list bitss)))
   411       end
   412   | implode_ast_tr' (*"_implode"*) asts = raise_ast "implode_ast_tr'" asts;
   413 
   414 
   415 
   416 
   417 (** syn_ext_of_sext **)   (* FIXME remove *)
   418 
   419 fun strip_esc str =
   420   let
   421     fun strip ("'" :: c :: cs) = c :: strip cs
   422       | strip ["'"] = []
   423       | strip (c :: cs) = c :: strip cs
   424       | strip [] = [];
   425   in
   426     implode (strip (explode str))
   427   end;
   428 
   429 fun infix_name sy = "op " ^ strip_esc sy;
   430 
   431 
   432 fun syn_ext_of_sext all_roots new_roots xconsts read_typ sext =
   433   let
   434     val {mixfix, parse_ast_translation, parse_translation, print_translation,
   435       print_ast_translation, ...} = sext_components sext;
   436 
   437     val tinfixT = [typeT, typeT] ---> typeT;
   438 
   439     fun binder (Binder (sy, _, name, _, _)) = Some (sy, name)
   440       | binder _ = None;
   441 
   442     fun binder_typ ty =
   443       (case read_typ ty of
   444         Type ("fun", [Type ("fun", [_, T2]), T3]) =>
   445           [Type ("idts", []), T2] ---> T3
   446       | _ => error ("Illegal binder type " ^ quote ty));
   447 
   448     fun mk_infix sy ty c p1 p2 p3 =
   449       [Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3),
   450        Mfix ("op " ^ sy, ty, c, [], max_pri)];
   451 
   452     fun mfix_of (Mixfix (sy, ty, c, ps, p)) = [Mfix (sy, read_typ ty, c, ps, p)]
   453       | mfix_of (Delimfix (sy, ty, c)) = [Mfix (sy, read_typ ty, c, [], max_pri)]
   454       | mfix_of (Infixl (sy, ty, p)) =
   455           mk_infix sy (read_typ ty) (infix_name sy) p (p + 1) p
   456       | mfix_of (Infixr (sy, ty, p)) =
   457           mk_infix sy (read_typ ty) (infix_name sy) (p + 1) p p
   458       | mfix_of (Binder (sy, ty, _, p, q)) =
   459           [Mfix ("(3" ^ sy ^ "_./ _)", binder_typ ty, sy, [0, p], q)]
   460       | mfix_of (TInfixl (s, c, p)) =
   461           [Mfix ("(_ " ^ s ^ "/ _)", tinfixT, c, [p, p + 1], p)]
   462       | mfix_of (TInfixr (s, c, p)) =
   463           [Mfix ("(_ " ^ s ^ "/ _)", tinfixT, c, [p + 1, p], p)];
   464 
   465     val mfix = flat (map mfix_of mixfix);
   466     val binders = mapfilter binder mixfix;
   467     val bparses = map mk_binder_tr binders;
   468     val bprints = map (mk_binder_tr' o swap) binders;
   469   in
   470     syn_ext all_roots new_roots mfix (distinct (filter is_xid xconsts))
   471       (parse_ast_translation,
   472         bparses @ parse_translation,
   473         bprints @ print_translation,
   474         print_ast_translation)
   475       ([], [])
   476   end;
   477 
   478 
   479 
   480 (** constants **)     (* FIXME remove *)
   481 
   482 fun constants sext =
   483   let
   484     fun consts (Delimfix (_, ty, c)) = ([c], ty)
   485       | consts (Mixfix (_, ty, c, _, _)) = ([c], ty)
   486       | consts (Infixl (c, ty, _)) = ([infix_name c], ty)
   487       | consts (Infixr (c, ty, _)) = ([infix_name c], ty)
   488       | consts (Binder (_, ty, c, _, _)) = ([c], ty)
   489       | consts _ = ([""], "");    (*is filtered out below*)
   490   in
   491     distinct (filter_out (fn (l, _) => l = [""]) (map consts (mixfix_of sext)))
   492   end;
   493 
   494 
   495 
   496 (** pt_to_ast **)
   497 
   498 fun pt_to_ast trf pt =
   499   let
   500     fun trans a args =
   501       (case trf a of
   502         None => mk_appl (Constant a) args
   503       | Some f => f args handle exn
   504           => (writeln ("Error in parse ast translation for " ^ quote a); raise exn));
   505 
   506     fun ast_of (Node (a, pts)) = trans a (map ast_of pts)
   507       | ast_of (Tip tok) = Variable (str_of_token tok);
   508   in
   509     ast_of pt
   510   end;
   511 
   512 
   513 
   514 (** ast_to_term **)
   515 
   516 fun ast_to_term trf ast =
   517   let
   518     fun trans a args =
   519       (case trf a of
   520         None => list_comb (const a, args)
   521       | Some f => f args handle exn
   522           => (writeln ("Error in parse translation for " ^ quote a); raise exn));
   523 
   524     fun term_of (Constant a) = trans a []
   525       | term_of (Variable x) = scan_var x
   526       | term_of (Appl (Constant a :: (asts as _ :: _))) =
   527           trans a (map term_of asts)
   528       | term_of (Appl (ast :: (asts as _ :: _))) =
   529           list_comb (term_of ast, map term_of asts)
   530       | term_of (ast as Appl _) = raise_ast "ast_to_term: malformed ast" [ast];
   531   in
   532     term_of ast
   533   end;
   534 
   535 
   536 
   537 (** pure_trfuns **)
   538 
   539 val pure_trfuns =
   540  ([(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr),
   541     ("_bigimpl", bigimpl_ast_tr)],
   542   [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
   543     ("_K", k_tr), ("_explode", explode_tr)],
   544   [],
   545   [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'), ("==>", impl_ast_tr'),
   546     ("_implode", implode_ast_tr')]);
   547 
   548 val constrainAbsC = "_constrainAbs";
   549 
   550 
   551 (** the Pure syntax **)   (* FIXME remove *)
   552 
   553 val pure_sext =
   554   NewSext {
   555     mixfix = [
   556       Mixfix   ("(3%_./ _)",  "[idts, 'a] => ('b => 'a)",      "_lambda", [0], 0),
   557       Delimfix ("_",          "'a => " ^ args,                 ""),
   558       Delimfix ("_,/ _",      "['a, " ^ args ^ "] => " ^ args, "_args"),
   559       Delimfix ("_",          "id => idt",                     ""),
   560       Mixfix   ("_::_",       "[id, type] => idt",             "_idtyp", [0, 0], 0),
   561       Delimfix ("'(_')",      "idt => idt",                    ""),
   562       Delimfix ("_",          "idt => idts",                   ""),
   563       Mixfix   ("_/ _",       "[idt, idts] => idts",           "_idts", [1, 0], 0),
   564       Delimfix ("_",          "id => aprop",                   ""),
   565       Delimfix ("_",          "var => aprop",                  ""),
   566       Mixfix   ("(1_/(1'(_')))", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], max_pri),
   567       Delimfix ("PROP _",     "aprop => prop",                 "_aprop"),
   568       Delimfix ("_",          "prop => asms",                  ""),
   569       Delimfix ("_;/ _",      "[prop, asms] => asms",          "_asms"),
   570       Mixfix   ("((3[| _ |]) ==>/ _)", "[asms, prop] => prop", "_bigimpl", [0, 1], 1),
   571       Mixfix   ("(_ ==/ _)",  "['a::{}, 'a] => prop",          "==", [3, 2], 2),
   572       Mixfix   ("(_ =?=/ _)", "['a::{}, 'a] => prop",          "=?=", [3, 2], 2),
   573       Mixfix   ("(_ ==>/ _)", "[prop, prop] => prop",          "==>", [2, 1], 1),
   574       Binder   ("!!",         "('a::logic => prop) => prop",   "all", 0, 0)],
   575     xrules = [],
   576     parse_ast_translation = [(applC, appl_ast_tr), ("_lambda", lambda_ast_tr),
   577       ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr)],
   578     parse_translation = [("_abs", abs_tr), ("_aprop", aprop_tr), ("_K", k_tr),
   579       ("_explode", explode_tr)],
   580     print_translation = [],
   581     print_ast_translation = [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'),
   582       ("==>", impl_ast_tr'), ("_implode", implode_ast_tr')]};
   583 
   584 val syntax_types = terminals @ ["syntax", logic, "type", "types", "sort",
   585   "classes", args, "idt", "idts", "aprop", "asms"];
   586 
   587 val syntax_consts = [(["_K", "_explode", "_implode"], "syntax")];
   588 
   589 
   590 end;
   591