src/Tools/Code/code_scala.ML
author haftmann
Wed Sep 01 16:08:31 2010 +0200 (2010-09-01)
changeset 39022 ac7774a35bcf
parent 38971 5d49165a192e
child 39023 3f70c03e8282
permissions -rw-r--r--
explicit modify_stmt parameter
     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 space_implode "+"
   197       o Long_Name.explode o deresolve_full;
   198     fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
   199           print_def name (vs, ty) (filter (snd o snd) raw_eqs)
   200       | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
   201           let
   202             val tyvars = intro_tyvars vs reserved;
   203             fun print_co ((co, _), []) =
   204                   concat [str "final", str "case", str "object", (str o deresolve) co,
   205                     str "extends", applify "[" "]" I NOBR ((str o deresolve) name)
   206                       (replicate (length vs) (str "Nothing"))]
   207               | print_co ((co, vs_args), tys) =
   208                   concat [applify "(" ")"
   209                     (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) NOBR
   210                     (applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((concat o map str)
   211                       ["final", "case", "class", deresolve co]) vs_args)
   212                     (Name.names (snd reserved) "a" tys),
   213                     str "extends",
   214                     applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
   215                       ((str o deresolve) name) vs
   216                   ];
   217           in
   218             Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars o fst)
   219               NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve name]) vs
   220                 :: map print_co cos)
   221           end
   222       | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
   223           let
   224             val tyvars = intro_tyvars [(v, [name])] reserved;
   225             fun add_typarg s = Pretty.block
   226               [str s, str "[", (str o lookup_tyvar tyvars) v, str "]"];
   227             fun print_super_classes [] = NONE
   228               | print_super_classes classes = SOME (concat (str "extends"
   229                   :: separate (str "with") (map (add_typarg o deresolve o fst) classes)));
   230             fun print_classparam_val (classparam, ty) =
   231               concat [str "val", constraint (print_method classparam)
   232                 ((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)];
   233             fun print_classparam_def (classparam, ty) =
   234               let
   235                 val (tys, ty) = Code_Thingol.unfold_fun ty;
   236                 val [implicit_name] = Name.invents (snd reserved) (lookup_tyvar tyvars v) 1;
   237                 val proto_vars = intro_vars [implicit_name] reserved;
   238                 val auxs = Name.invents (snd proto_vars) "a" (length tys);
   239                 val vars = intro_vars auxs proto_vars;
   240               in
   241                 concat [str "def", constraint (Pretty.block [applify "(" ")"
   242                   (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
   243                   (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
   244                   (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
   245                   add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
   246                   applify "(" ")" (str o lookup_var vars) NOBR
   247                   (Pretty.block [str implicit_name, str ".", print_method classparam]) auxs]
   248               end;
   249           in
   250             Pretty.chunks (
   251               (Pretty.block_enclose
   252                 (concat ([str "trait", (add_typarg o deresolve) name]
   253                   @ the_list (print_super_classes super_classes) @ [str "{"]), str "}")
   254                 (map print_classparam_val classparams))
   255               :: map print_classparam_def classparams
   256             )
   257           end
   258       | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
   259             (super_instances, (classparam_instances, further_classparam_instances)))) =
   260           let
   261             val tyvars = intro_tyvars vs reserved;
   262             val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
   263             fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
   264               let
   265                 val aux_tys = Name.names (snd reserved) "a" tys;
   266                 val auxs = map fst aux_tys;
   267                 val vars = intro_vars auxs reserved;
   268                 val aux_abstr = if null auxs then [] else [enum "," "(" ")"
   269                   (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
   270                   (print_typ tyvars NOBR ty)) aux_tys), str "=>"];
   271               in 
   272                 concat ([str "val", print_method classparam, str "="]
   273                   @ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR
   274                     (const, map (IVar o SOME) auxs))
   275               end;
   276           in
   277             Pretty.block_enclose (concat [str "implicit def",
   278               constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp),
   279               str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
   280                 (map print_classparam_instance (classparam_instances @ further_classparam_instances))
   281           end;
   282   in print_stmt end;
   283 
   284 fun scala_program_of_program labelled_name reserved module_alias program =
   285   let
   286     fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
   287       let
   288         val declare = Name.declare name_fragment;
   289       in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end;
   290     fun namify_class base ((nsp_class, nsp_object), nsp_common) =
   291       let
   292         val (base', nsp_class') = yield_singleton Name.variants base nsp_class
   293       in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
   294     fun namify_object base ((nsp_class, nsp_object), nsp_common) =
   295       let
   296         val (base', nsp_object') = yield_singleton Name.variants base nsp_object
   297       in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
   298     fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
   299       let
   300         val (base', nsp_common') =
   301           yield_singleton Name.variants (if upper then first_upper base else base) nsp_common
   302       in
   303         (base',
   304           ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
   305       end;
   306     fun namify_stmt (Code_Thingol.Fun _) = namify_object
   307       | namify_stmt (Code_Thingol.Datatype _) = namify_class
   308       | namify_stmt (Code_Thingol.Datatypecons _) = namify_common true
   309       | namify_stmt (Code_Thingol.Class _) = namify_class
   310       | namify_stmt (Code_Thingol.Classrel _) = namify_object
   311       | namify_stmt (Code_Thingol.Classparam _) = namify_object
   312       | namify_stmt (Code_Thingol.Classinst _) = namify_common false;
   313     fun memorize_implicits name =
   314       let
   315         fun is_classinst stmt = case stmt
   316          of Code_Thingol.Classinst _ => true
   317           | _ => false;
   318         val implicits = filter (is_classinst o Graph.get_node program)
   319           (Graph.imm_succs program name);
   320       in union (op =) implicits end;
   321     fun modify_stmt (Code_Thingol.Datatypecons _) = NONE
   322       | modify_stmt (Code_Thingol.Classrel _) = NONE
   323       | modify_stmt (Code_Thingol.Classparam _) = NONE
   324       | modify_stmt stmt = SOME stmt;
   325   in
   326     Code_Namespace.hierarchical_program labelled_name { module_alias = module_alias, reserved = reserved,
   327       empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module, namify_stmt = namify_stmt,
   328       cyclic_modules = true, empty_data = [], memorize_data = memorize_implicits, modify_stmt = modify_stmt } program
   329   end;
   330 
   331 fun serialize_scala { labelled_name, reserved_syms, includes,
   332     module_alias, class_syntax, tyco_syntax, const_syntax, program,
   333     names, presentation_names } =
   334   let
   335 
   336     (* build program *)
   337     val reserved = fold (insert (op =) o fst) includes reserved_syms;
   338     val { deresolver, hierarchical_program = sca_program } =
   339       scala_program_of_program labelled_name (Name.make_context reserved) module_alias program;
   340 
   341     (* print statements *)
   342     fun lookup_constr tyco constr = case Graph.get_node program tyco
   343      of Code_Thingol.Datatype (_, (_, constrs)) =>
   344           the (AList.lookup (op = o apsnd fst) constrs constr);
   345     fun classparams_of_class class = case Graph.get_node program class
   346      of Code_Thingol.Class (_, (_, (_, classparams))) => classparams;
   347     fun args_num c = case Graph.get_node program c
   348      of Code_Thingol.Fun (_, (((_, ty), []), _)) =>
   349           (length o fst o Code_Thingol.unfold_fun) ty
   350       | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
   351       | Code_Thingol.Datatypecons (_, tyco) => length (lookup_constr tyco c)
   352       | Code_Thingol.Classparam (_, class) =>
   353           (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =)
   354             (classparams_of_class class)) c;
   355     fun is_singleton_constr c = case Graph.get_node program c
   356      of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
   357       | _ => false;
   358     val print_stmt = print_scala_stmt labelled_name tyco_syntax const_syntax
   359       (make_vars reserved) args_num is_singleton_constr;
   360 
   361     (* print nodes *)
   362     fun print_module base implicit_ps p = Pretty.chunks2
   363       ([str ("object " ^ base ^ " {")]
   364         @ (if null implicit_ps then [] else (single o Pretty.block)
   365             (str "import /*implicits*/" :: Pretty.brk 1 :: commas implicit_ps))
   366         @ [p, str ("} /* object " ^ base ^ " */")]);
   367     fun print_implicit prefix_fragments implicit =
   368       let
   369         val s = deresolver prefix_fragments implicit;
   370       in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
   371     fun print_node _ (_, Dummy) = NONE
   372       | print_node prefix_fragments (name, Code_Namespace.Stmt stmt) =
   373           if null presentation_names
   374           orelse member (op =) presentation_names name
   375           then SOME (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt))
   376           else NONE
   377       | print_node prefix_fragments (name_fragment, Code_Namespace.Module (implicits, nodes)) =
   378           if null presentation_names
   379           then
   380             let
   381               val prefix_fragments' = prefix_fragments @ [name_fragment];
   382             in
   383               Option.map (print_module name_fragment
   384                 (map_filter (print_implicit prefix_fragments') implicits))
   385                   (print_nodes prefix_fragments' nodes)
   386             end
   387           else print_nodes [] nodes
   388     and print_nodes prefix_fragments nodes = let
   389         val ps = map_filter (fn name => print_node prefix_fragments (name,
   390           snd (Graph.get_node nodes name)))
   391             ((rev o flat o Graph.strong_conn) nodes);
   392       in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
   393 
   394     (* serialization *)
   395     val p_includes = if null presentation_names then map snd includes else [];
   396     val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
   397     fun write width NONE = writeln_pretty width
   398       | write width (SOME p) = File.write p o string_of_pretty width;
   399   in
   400     Code_Target.serialization write (rpair [] oo string_of_pretty) p
   401   end;
   402 
   403 val serializer : Code_Target.serializer =
   404   Code_Target.parse_args (Scan.succeed ()) #> K serialize_scala;
   405 
   406 val literals = let
   407   fun char_scala c = if c = "'" then "\\'"
   408     else if c = "\"" then "\\\""
   409     else if c = "\\" then "\\\\"
   410     else let val k = ord c
   411     in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end
   412   fun numeral_scala k = if k < 0
   413     then if k > ~ 2147483647 then "- " ^ string_of_int (~ k)
   414       else quote ("- " ^ string_of_int (~ k))
   415     else if k <= 2147483647 then string_of_int k
   416       else quote (string_of_int k)
   417 in Literals {
   418   literal_char = Library.enclose "'" "'" o char_scala,
   419   literal_string = quote o translate_string char_scala,
   420   literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   421   literal_positive_numeral = fn k => "Nat(" ^ numeral_scala k ^ ")",
   422   literal_alternative_numeral = fn k => "Natural(" ^ numeral_scala k ^ ")",
   423   literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   424   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   425   infix_cons = (6, "::")
   426 } end;
   427 
   428 
   429 (** Isar setup **)
   430 
   431 val setup =
   432   Code_Target.add_target
   433     (target, { serializer = serializer, literals = literals,
   434       check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
   435         make_command = fn scala_home => fn _ =>
   436           "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
   437             ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " ROOT.scala" } })
   438   #> Code_Target.add_tyco_syntax target "fun"
   439      (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   440         brackify_infix (1, R) fxy (
   441           print_typ BR ty1 (*product type vs. tupled arguments!*),
   442           str "=>",
   443           print_typ (INFX (1, R)) ty2
   444         )))
   445   #> fold (Code_Target.add_reserved target) [
   446       "abstract", "case", "catch", "class", "def", "do", "else", "extends", "false",
   447       "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",
   448       "match", "new", "null", "object", "override", "package", "private", "protected",
   449       "requires", "return", "sealed", "super", "this", "throw", "trait", "try",
   450       "true", "type", "val", "var", "while", "with", "yield"
   451     ]
   452   #> fold (Code_Target.add_reserved target) [
   453       "apply", "error", "BigInt", "Nil", "List"
   454     ];
   455 
   456 end; (*struct*)