src/Tools/Code/code_scala.ML
author haftmann
Thu Sep 02 10:29:50 2010 +0200 (2010-09-02)
changeset 39030 2bb34f36db80
parent 39024 30d5dd2f30b6
child 39034 ebeb48fd653b
permissions -rw-r--r--
include names need not be considered as reserved any longer
     1 (*  Title:      Tools/Code/code_scala.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Serializer for Scala.
     5 *)
     6 
     7 signature CODE_SCALA =
     8 sig
     9   val target: string
    10   val setup: theory -> theory
    11 end;
    12 
    13 structure Code_Scala : CODE_SCALA =
    14 struct
    15 
    16 val target = "Scala";
    17 
    18 open Basic_Code_Thingol;
    19 open Code_Printer;
    20 
    21 infixr 5 @@;
    22 infixr 5 @|;
    23 
    24 
    25 (** Scala serializer **)
    26 
    27 fun print_scala_stmt labelled_name tyco_syntax const_syntax reserved
    28     args_num is_singleton_constr (deresolve, deresolve_full) =
    29   let
    30     fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
    31     fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
    32     fun print_tyco_expr tyvars fxy (tyco, tys) = applify "[" "]"
    33           (print_typ tyvars NOBR) fxy ((str o deresolve) tyco) tys
    34     and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
    35          of NONE => print_tyco_expr tyvars fxy (tyco, tys)
    36           | SOME (i, print) => print (print_typ tyvars) fxy tys)
    37       | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
    38     fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (class, [ty]);
    39     fun print_tupled_typ tyvars ([], ty) =
    40           print_typ tyvars NOBR ty
    41       | print_tupled_typ tyvars ([ty1], ty2) =
    42           concat [print_typ tyvars BR ty1, str "=>", print_typ tyvars NOBR ty2]
    43       | print_tupled_typ tyvars (tys, ty) =
    44           concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
    45             str "=>", print_typ tyvars NOBR ty];
    46     fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2];
    47     fun print_var vars NONE = str "_"
    48       | print_var vars (SOME v) = (str o lookup_var vars) v
    49     fun print_term tyvars is_pat some_thm vars fxy (IConst c) =
    50           print_app tyvars is_pat some_thm vars fxy (c, [])
    51       | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
    52           (case Code_Thingol.unfold_const_app t
    53            of SOME app => print_app tyvars is_pat some_thm vars fxy app
    54             | _ => applify "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy
    55                 (print_term tyvars is_pat some_thm vars BR t1) [t2])
    56       | print_term tyvars is_pat some_thm vars fxy (IVar v) =
    57           print_var vars v
    58       | print_term tyvars is_pat some_thm vars fxy ((v, ty) `|=> t) =
    59           let
    60             val vars' = intro_vars (the_list v) vars;
    61           in
    62             concat [
    63               enclose "(" ")" [constraint (print_var vars' v) (print_typ tyvars NOBR ty)],
    64               str "=>",
    65               print_term tyvars false some_thm vars' NOBR t
    66             ]
    67           end 
    68       | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
    69           (case Code_Thingol.unfold_const_app t0
    70            of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
    71                 then print_case tyvars some_thm vars fxy cases
    72                 else print_app tyvars is_pat some_thm vars fxy c_ts
    73             | NONE => print_case tyvars some_thm vars fxy cases)
    74     and print_app tyvars is_pat some_thm vars fxy
    75         (app as ((c, ((arg_typs, _), function_typs)), ts)) =
    76       let
    77         val k = length ts;
    78         val arg_typs' = if is_pat orelse
    79           (is_none (const_syntax c) andalso is_singleton_constr c) then [] else arg_typs;
    80         val (l, print') = case const_syntax c
    81          of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
    82               (print_term tyvars is_pat some_thm vars NOBR) fxy
    83                 (applify "[" "]" (print_typ tyvars NOBR)
    84                   NOBR ((str o deresolve) c) arg_typs') ts)
    85           | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
    86               (print_term tyvars is_pat some_thm vars NOBR) fxy
    87                 (applify "[" "]" (print_typ tyvars NOBR)
    88                   NOBR (str s) arg_typs') ts)
    89           | SOME (Complex_const_syntax (k, print)) =>
    90               (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
    91                 (ts ~~ take k function_typs))
    92       in if k = l then print' fxy ts
    93       else if k < l then
    94         print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
    95       else let
    96         val (ts1, ts23) = chop l ts;
    97       in
    98         Pretty.block (print' BR ts1 :: map (fn t => Pretty.block
    99           [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23)
   100       end end
   101     and print_bind tyvars some_thm fxy p =
   102       gen_print_bind (print_term tyvars true) some_thm fxy p
   103     and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
   104           let
   105             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
   106             fun print_match ((IVar NONE, _), t) vars =
   107                   ((true, print_term tyvars false some_thm vars NOBR t), vars)
   108               | print_match ((pat, ty), t) vars =
   109                   vars
   110                   |> print_bind tyvars some_thm BR pat
   111                   |>> (fn p => (false, concat [str "val", constraint p (print_typ tyvars NOBR ty),
   112                       str "=", print_term tyvars false some_thm vars NOBR t]))
   113             val (seps_ps, vars') = fold_map print_match binds vars;
   114             val all_seps_ps = seps_ps @ [(true, print_term tyvars false some_thm vars' NOBR body)];
   115             fun insert_seps [(_, p)] = [p]
   116               | insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) =
   117                   (if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps
   118           in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}")
   119           end
   120       | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
   121           let
   122             fun print_select (pat, body) =
   123               let
   124                 val (p_pat, vars') = print_bind tyvars some_thm NOBR pat vars;
   125                 val p_body = print_term tyvars false some_thm vars' NOBR body
   126               in concat [str "case", p_pat, str "=>", p_body] end;
   127           in brackify_block fxy
   128             (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"])
   129             (map print_select clauses)
   130             (str "}") 
   131           end
   132       | print_case tyvars some_thm vars fxy ((_, []), _) =
   133           (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
   134     fun print_context tyvars vs name = applify "[" "]"
   135       (fn (v, sort) => (Pretty.block o map str)
   136         (lookup_tyvar tyvars v :: maps (fn sort => [": ", deresolve sort]) sort))
   137           NOBR ((str o deresolve) name) vs;
   138     fun print_defhead tyvars vars name vs params tys ty =
   139       Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
   140         constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
   141           NOBR (print_context tyvars vs name) (params ~~ tys)) (print_typ tyvars NOBR ty),
   142             str " ="];
   143     fun print_def name (vs, ty) [] =
   144           let
   145             val (tys, ty') = Code_Thingol.unfold_fun ty;
   146             val params = Name.invents (snd reserved) "a" (length tys);
   147             val tyvars = intro_tyvars vs reserved;
   148             val vars = intro_vars params reserved;
   149           in
   150             concat [print_defhead tyvars vars name vs params tys ty',
   151               str ("error(\"" ^ name ^ "\")")]
   152           end
   153       | print_def name (vs, ty) eqs =
   154           let
   155             val tycos = fold (fn ((ts, t), _) =>
   156               fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
   157             val tyvars = reserved
   158               |> intro_base_names
   159                    (is_none o tyco_syntax) deresolve tycos
   160               |> intro_tyvars vs;
   161             val simple = case eqs
   162              of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
   163               | _ => false;
   164             val consts = fold Code_Thingol.add_constnames
   165               (map (snd o fst) eqs) [];
   166             val vars1 = reserved
   167               |> intro_base_names
   168                    (is_none o const_syntax) deresolve consts
   169             val params = if simple
   170               then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
   171               else aux_params vars1 (map (fst o fst) eqs);
   172             val vars2 = intro_vars params vars1;
   173             val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty;
   174             fun tuplify [p] = p
   175               | tuplify ps = enum "," "(" ")" ps;
   176             fun print_rhs vars' ((_, t), (some_thm, _)) =
   177               print_term tyvars false some_thm vars' NOBR t;
   178             fun print_clause (eq as ((ts, _), (some_thm, _))) =
   179               let
   180                 val vars' = intro_vars ((fold o Code_Thingol.fold_varnames)
   181                   (insert (op =)) ts []) vars1;
   182               in
   183                 concat [str "case",
   184                   tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
   185                   str "=>", print_rhs vars' eq]
   186               end;
   187             val head = print_defhead tyvars vars2 name vs params tys' ty';
   188           in if simple then
   189             concat [head, print_rhs vars2 (hd eqs)]
   190           else
   191             Pretty.block_enclose
   192               (concat [head, tuplify (map (str o lookup_var vars2) params),
   193                 str "match", str "{"], str "}")
   194               (map print_clause eqs)
   195           end;
   196     val print_method = str o Library.enclose "`" "`" o deresolve_full;
   197     fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
   198           print_def name (vs, ty) (filter (snd o snd) raw_eqs)
   199       | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
   200           let
   201             val tyvars = intro_tyvars vs reserved;
   202             fun print_co ((co, _), []) =
   203                   concat [str "final", str "case", str "object", (str o deresolve) co,
   204                     str "extends", applify "[" "]" I NOBR ((str o deresolve) name)
   205                       (replicate (length vs) (str "Nothing"))]
   206               | print_co ((co, vs_args), tys) =
   207                   concat [applify "(" ")"
   208                     (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) NOBR
   209                     (applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((concat o map str)
   210                       ["final", "case", "class", deresolve co]) vs_args)
   211                     (Name.names (snd reserved) "a" tys),
   212                     str "extends",
   213                     applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
   214                       ((str o deresolve) name) vs
   215                   ];
   216           in
   217             Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars o fst)
   218               NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve name]) vs
   219                 :: map print_co cos)
   220           end
   221       | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
   222           let
   223             val tyvars = intro_tyvars [(v, [name])] reserved;
   224             fun add_typarg s = Pretty.block
   225               [str s, str "[", (str o lookup_tyvar tyvars) v, str "]"];
   226             fun print_super_classes [] = NONE
   227               | print_super_classes classes = SOME (concat (str "extends"
   228                   :: separate (str "with") (map (add_typarg o deresolve o fst) classes)));
   229             fun print_classparam_val (classparam, ty) =
   230               concat [str "val", constraint (print_method classparam)
   231                 ((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)];
   232             fun print_classparam_def (classparam, ty) =
   233               let
   234                 val (tys, ty) = Code_Thingol.unfold_fun ty;
   235                 val [implicit_name] = Name.invents (snd reserved) (lookup_tyvar tyvars v) 1;
   236                 val proto_vars = intro_vars [implicit_name] reserved;
   237                 val auxs = Name.invents (snd proto_vars) "a" (length tys);
   238                 val vars = intro_vars auxs proto_vars;
   239               in
   240                 concat [str "def", constraint (Pretty.block [applify "(" ")"
   241                   (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
   242                   (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
   243                   (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
   244                   add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
   245                   applify "(" ")" (str o lookup_var vars) NOBR
   246                   (Pretty.block [str implicit_name, str ".", print_method classparam]) auxs]
   247               end;
   248           in
   249             Pretty.chunks (
   250               (Pretty.block_enclose
   251                 (concat ([str "trait", (add_typarg o deresolve) name]
   252                   @ the_list (print_super_classes super_classes) @ [str "{"]), str "}")
   253                 (map print_classparam_val classparams))
   254               :: map print_classparam_def classparams
   255             )
   256           end
   257       | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
   258             (super_instances, (classparam_instances, further_classparam_instances)))) =
   259           let
   260             val tyvars = intro_tyvars vs reserved;
   261             val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
   262             fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
   263               let
   264                 val aux_tys = Name.names (snd reserved) "a" tys;
   265                 val auxs = map fst aux_tys;
   266                 val vars = intro_vars auxs reserved;
   267                 val aux_abstr = if null auxs then [] else [enum "," "(" ")"
   268                   (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
   269                   (print_typ tyvars NOBR ty)) aux_tys), str "=>"];
   270               in 
   271                 concat ([str "val", print_method classparam, str "="]
   272                   @ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR
   273                     (const, map (IVar o SOME) auxs))
   274               end;
   275           in
   276             Pretty.block_enclose (concat [str "implicit def",
   277               constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp),
   278               str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
   279                 (map print_classparam_instance (classparam_instances @ further_classparam_instances))
   280           end;
   281   in print_stmt end;
   282 
   283 fun scala_program_of_program labelled_name reserved module_alias program =
   284   let
   285     fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
   286       let
   287         val declare = Name.declare name_fragment;
   288       in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end;
   289     fun namify_class base ((nsp_class, nsp_object), nsp_common) =
   290       let
   291         val (base', nsp_class') = yield_singleton Name.variants base nsp_class
   292       in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
   293     fun namify_object base ((nsp_class, nsp_object), nsp_common) =
   294       let
   295         val (base', nsp_object') = yield_singleton Name.variants base nsp_object
   296       in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
   297     fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
   298       let
   299         val (base', nsp_common') =
   300           yield_singleton Name.variants (if upper then first_upper base else base) nsp_common
   301       in
   302         (base',
   303           ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
   304       end;
   305     fun namify_stmt (Code_Thingol.Fun _) = namify_object
   306       | namify_stmt (Code_Thingol.Datatype _) = namify_class
   307       | namify_stmt (Code_Thingol.Datatypecons _) = namify_common true
   308       | namify_stmt (Code_Thingol.Class _) = namify_class
   309       | namify_stmt (Code_Thingol.Classrel _) = namify_object
   310       | namify_stmt (Code_Thingol.Classparam _) = namify_object
   311       | namify_stmt (Code_Thingol.Classinst _) = namify_common false;
   312     fun memorize_implicits name =
   313       let
   314         fun is_classinst stmt = case stmt
   315          of Code_Thingol.Classinst _ => true
   316           | _ => false;
   317         val implicits = filter (is_classinst o Graph.get_node program)
   318           (Graph.imm_succs program name);
   319       in union (op =) implicits end;
   320     fun modify_stmt (_, Code_Thingol.Datatypecons _) = NONE
   321       | modify_stmt (_, Code_Thingol.Classrel _) = NONE
   322       | modify_stmt (_, Code_Thingol.Classparam _) = NONE
   323       | modify_stmt (_, stmt) = SOME stmt;
   324   in
   325     Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
   326       empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module, namify_stmt = namify_stmt,
   327       cyclic_modules = true, empty_data = [], memorize_data = memorize_implicits, modify_stmts = map modify_stmt } program
   328   end;
   329 
   330 fun serialize_scala { labelled_name, reserved_syms, includes,
   331     module_alias, class_syntax, tyco_syntax, const_syntax, program,
   332     names, presentation_names } =
   333   let
   334 
   335     (* build program *)
   336     val { deresolver, hierarchical_program = sca_program } =
   337       scala_program_of_program labelled_name (Name.make_context reserved_syms) module_alias program;
   338 
   339     (* print statements *)
   340     fun lookup_constr tyco constr = case Graph.get_node program tyco
   341      of Code_Thingol.Datatype (_, (_, constrs)) =>
   342           the (AList.lookup (op = o apsnd fst) constrs constr);
   343     fun classparams_of_class class = case Graph.get_node program class
   344      of Code_Thingol.Class (_, (_, (_, classparams))) => classparams;
   345     fun args_num c = case Graph.get_node program c
   346      of Code_Thingol.Fun (_, (((_, ty), []), _)) =>
   347           (length o fst o Code_Thingol.unfold_fun) ty
   348       | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
   349       | Code_Thingol.Datatypecons (_, tyco) => length (lookup_constr tyco c)
   350       | Code_Thingol.Classparam (_, class) =>
   351           (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =)
   352             (classparams_of_class class)) c;
   353     fun is_singleton_constr c = case Graph.get_node program c
   354      of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
   355       | _ => false;
   356     val print_stmt = print_scala_stmt labelled_name tyco_syntax const_syntax
   357       (make_vars reserved_syms) args_num is_singleton_constr;
   358 
   359     (* print nodes *)
   360     fun print_module base implicit_ps p = Pretty.chunks2
   361       ([str ("object " ^ base ^ " {")]
   362         @ (if null implicit_ps then [] else (single o Pretty.block)
   363             (str "import /*implicits*/" :: Pretty.brk 1 :: commas implicit_ps))
   364         @ [p, str ("} /* object " ^ base ^ " */")]);
   365     fun print_implicit prefix_fragments implicit =
   366       let
   367         val s = deresolver prefix_fragments implicit;
   368       in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
   369     fun print_node _ (_, Code_Namespace.Dummy) = NONE
   370       | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
   371           if null presentation_names
   372           orelse member (op =) presentation_names name
   373           then SOME (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt))
   374           else NONE
   375       | print_node prefix_fragments (name_fragment, Code_Namespace.Module (implicits, nodes)) =
   376           if null presentation_names
   377           then
   378             let
   379               val prefix_fragments' = prefix_fragments @ [name_fragment];
   380             in
   381               Option.map (print_module name_fragment
   382                 (map_filter (print_implicit prefix_fragments') implicits))
   383                   (print_nodes prefix_fragments' nodes)
   384             end
   385           else print_nodes [] nodes
   386     and print_nodes prefix_fragments nodes = let
   387         val ps = map_filter (fn name => print_node prefix_fragments (name,
   388           snd (Graph.get_node nodes name)))
   389             ((rev o flat o Graph.strong_conn) nodes);
   390       in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
   391 
   392     (* serialization *)
   393     val p_includes = if null presentation_names then map snd includes else [];
   394     val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
   395     fun write width NONE = writeln_pretty width
   396       | write width (SOME p) = File.write p o string_of_pretty width;
   397   in
   398     Code_Target.serialization write (rpair [] oo string_of_pretty) p
   399   end;
   400 
   401 val serializer : Code_Target.serializer =
   402   Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
   403 
   404 val literals = let
   405   fun char_scala c = if c = "'" then "\\'"
   406     else if c = "\"" then "\\\""
   407     else if c = "\\" then "\\\\"
   408     else let val k = ord c
   409     in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end
   410   fun numeral_scala k = if k < 0
   411     then if k > ~ 2147483647 then "- " ^ string_of_int (~ k)
   412       else quote ("- " ^ string_of_int (~ k))
   413     else if k <= 2147483647 then string_of_int k
   414       else quote (string_of_int k)
   415 in Literals {
   416   literal_char = Library.enclose "'" "'" o char_scala,
   417   literal_string = quote o translate_string char_scala,
   418   literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   419   literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
   420   literal_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
   421   literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   422   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   423   infix_cons = (6, "::")
   424 } end;
   425 
   426 
   427 (** Isar setup **)
   428 
   429 val setup =
   430   Code_Target.add_target
   431     (target, { serializer = serializer, literals = literals,
   432       check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
   433         make_command = fn scala_home => fn _ =>
   434           "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
   435             ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " ROOT.scala" } })
   436   #> Code_Target.add_tyco_syntax target "fun"
   437      (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   438         brackify_infix (1, R) fxy (
   439           print_typ BR ty1 (*product type vs. tupled arguments!*),
   440           str "=>",
   441           print_typ (INFX (1, R)) ty2
   442         )))
   443   #> fold (Code_Target.add_reserved target) [
   444       "abstract", "case", "catch", "class", "def", "do", "else", "extends", "false",
   445       "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",
   446       "match", "new", "null", "object", "override", "package", "private", "protected",
   447       "requires", "return", "sealed", "super", "this", "throw", "trait", "try",
   448       "true", "type", "val", "var", "while", "with", "yield"
   449     ]
   450   #> fold (Code_Target.add_reserved target) [
   451       "apply", "error", "BigInt", "Nil", "List"
   452     ];
   453 
   454 end; (*struct*)