src/Tools/Code/code_scala.ML
author haftmann
Fri Jun 18 09:04:00 2010 +0200 (2010-06-18)
changeset 37453 44a307746163
parent 37450 45073611170a
child 37464 9250ad1b98e0
permissions -rw-r--r--
dropped dead code
     1 (*  Author:     Florian Haftmann, TU Muenchen
     2 
     3 Serializer for Scala.
     4 *)
     5 
     6 signature CODE_SCALA =
     7 sig
     8   val setup: theory -> theory
     9 end;
    10 
    11 structure Code_Scala : CODE_SCALA =
    12 struct
    13 
    14 val target = "Scala";
    15 
    16 open Basic_Code_Thingol;
    17 open Code_Printer;
    18 
    19 infixr 5 @@;
    20 infixr 5 @|;
    21 
    22 
    23 (** Scala serializer **)
    24 
    25 fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved args_num is_singleton deresolve =
    26   let
    27     val deresolve_base = Long_Name.base_name o deresolve;
    28     val lookup_tyvar = first_upper oo lookup_var;
    29     fun print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
    30          of NONE => applify "[" "]" fxy
    31               ((str o deresolve) tyco) (map (print_typ tyvars NOBR) tys)
    32           | SOME (i, print) => print (print_typ tyvars) fxy tys)
    33       | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
    34     fun print_typed tyvars p ty =
    35       Pretty.block [p, str ":", Pretty.brk 1, print_typ tyvars NOBR ty]
    36     fun print_var vars NONE = str "_"
    37       | print_var vars (SOME v) = (str o lookup_var vars) v
    38     fun print_term tyvars is_pat some_thm vars fxy (IConst c) =
    39           print_app tyvars is_pat some_thm vars fxy (c, [])
    40       | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
    41           (case Code_Thingol.unfold_const_app t
    42            of SOME app => print_app tyvars is_pat some_thm vars fxy app
    43             | _ => applify "(" ")" fxy
    44                 (print_term tyvars is_pat some_thm vars BR t1)
    45                 [print_term tyvars is_pat some_thm vars NOBR t2])
    46       | print_term tyvars is_pat some_thm vars fxy (IVar v) =
    47           print_var vars v
    48       | print_term tyvars is_pat some_thm vars fxy ((v, ty) `|=> t) =
    49           let
    50             val vars' = intro_vars (the_list v) vars;
    51           in
    52             concat [
    53               Pretty.block [str "(", print_typed tyvars (print_var vars' v) ty, str ")"],
    54               str "=>",
    55               print_term tyvars false some_thm vars' NOBR t
    56             ]
    57           end 
    58       | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
    59           (case Code_Thingol.unfold_const_app t0
    60            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
    61                 then print_case tyvars some_thm vars fxy cases
    62                 else print_app tyvars is_pat some_thm vars fxy c_ts
    63             | NONE => print_case tyvars some_thm vars fxy cases)
    64     and print_app tyvars is_pat some_thm vars fxy (app as ((c, ((arg_typs, _), function_typs)), ts)) =
    65       let
    66         val k = length ts;
    67         val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
    68         val arg_typs' = if is_pat orelse
    69           (is_none (syntax_const c) andalso is_singleton c) then [] else arg_typs;
    70         val (no_syntax, print') = case syntax_const c
    71          of NONE => (true, fn ts => applify "(" ")" fxy
    72               (applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) arg_typs'))
    73                 (map (print_term tyvars is_pat some_thm vars NOBR) ts))
    74           | SOME (_, print) => (false, fn ts =>
    75               print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take l function_typs));
    76       in if k = l then print' ts
    77       else if k < l then
    78         print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
    79       else let
    80         val (ts1, ts23) = chop l ts;
    81       in
    82         Pretty.block (print' ts1 :: map (fn t => Pretty.block
    83           [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23)
    84       end end
    85     and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars true) some_thm fxy p
    86     and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
    87           let
    88             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    89             fun print_match ((pat, ty), t) vars =
    90               vars
    91               |> print_bind tyvars some_thm BR pat
    92               |>> (fn p => semicolon [Pretty.block [str "val", Pretty.brk 1, p,
    93                 str ":", Pretty.brk 1, print_typ tyvars NOBR ty],
    94                   str "=", print_term tyvars false some_thm vars NOBR t])
    95             val (ps, vars') = fold_map print_match binds vars;
    96           in
    97             brackify_block fxy
    98               (str "{")
    99               (ps @| print_term tyvars false some_thm vars' NOBR body)
   100               (str "}")
   101           end
   102       | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
   103           let
   104             fun print_select (pat, body) =
   105               let
   106                 val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
   107               in concat [str "case", p, str "=>", print_term tyvars false some_thm vars' NOBR body] end;
   108           in brackify_block fxy
   109             (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"])
   110             (map print_select clauses)
   111             (str "}") 
   112           end
   113       | print_case tyvars some_thm vars fxy ((_, []), _) =
   114           (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
   115     fun implicit_arguments tyvars vs vars =
   116       let
   117         val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block
   118           [(str o deresolve) class, str "[", (str o lookup_tyvar tyvars) v, str "]"]) sort) vs;
   119         val implicit_names = Name.variant_list [] (maps (fn (v, sort) => map (fn class =>
   120           lookup_tyvar tyvars v ^ "_" ^ (Long_Name.base_name o deresolve) class) sort) vs);
   121         val vars' = intro_vars implicit_names vars;
   122         val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p])
   123           implicit_names implicit_typ_ps;
   124       in ((implicit_names, implicit_ps), vars') end;
   125     fun print_defhead tyvars vars p vs params tys implicits (*FIXME simplify*) ty =
   126       Pretty.block [str "def ", print_typed tyvars (applify "(implicit " ")" NOBR
   127         (applify "(" ")" NOBR
   128           (applify "[" "]" NOBR p (map (fn (v, sort) =>
   129               (str o implode) (lookup_tyvar tyvars v :: map (prefix ": " o deresolve) sort)) vs))
   130             (map2 (fn param => fn ty => print_typed tyvars
   131                 ((str o lookup_var vars) param) ty)
   132               params tys)) implicits) ty, str " ="]
   133     fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) = (case filter (snd o snd) raw_eqs
   134          of [] =>
   135               let
   136                 val (tys, ty') = Code_Thingol.unfold_fun ty;
   137                 val params = Name.invents (snd reserved) "a" (length tys);
   138                 val tyvars = intro_vars (map fst vs) reserved;
   139                 val vars = intro_vars params reserved;
   140               in
   141                 concat [print_defhead tyvars vars ((str o deresolve) name) vs params tys [] ty',
   142                   str ("error(\"" ^ name ^ "\")")]
   143               end
   144           | eqs =>
   145               let
   146                 val tycos = fold (fn ((ts, t), _) =>
   147                   fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
   148                 val tyvars = reserved
   149                   |> intro_base_names
   150                        (is_none o syntax_tyco) deresolve tycos
   151                   |> intro_vars (map fst vs);
   152                 val simple = case eqs
   153                  of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
   154                   | _ => false;
   155                 val consts = fold Code_Thingol.add_constnames
   156                   (map (snd o fst) eqs) [];
   157                 val vars1 = reserved
   158                   |> intro_base_names
   159                        (is_none o syntax_const) deresolve consts
   160                 val ((_, implicit_ps), vars2) = implicit_arguments tyvars vs vars1; (*FIXME drop*)
   161                 val params = if simple then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
   162                   else aux_params vars2 (map (fst o fst) eqs);
   163                 val vars3 = intro_vars params vars2;
   164                 val (tys, ty1) = Code_Thingol.unfold_fun ty;
   165                 val (tys1, tys2) = chop (length params) tys;
   166                 val ty2 = Library.foldr
   167                   (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (tys2, ty1);
   168                 fun print_tuple [p] = p
   169                   | print_tuple ps = enum "," "(" ")" ps;
   170                 fun print_rhs vars' ((_, t), (some_thm, _)) = print_term tyvars false some_thm vars' NOBR t;
   171                 fun print_clause (eq as ((ts, _), (some_thm, _))) =
   172                   let
   173                     val vars' = intro_vars ((fold o Code_Thingol.fold_varnames) (insert (op =)) ts []) vars2;
   174                   in
   175                     concat [str "case", print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
   176                       str "=>", print_rhs vars' eq]
   177                   end;
   178                 val head = print_defhead tyvars vars3 ((str o deresolve) name) vs params tys1 [] ty2;
   179               in if simple then
   180                 concat [head, print_rhs vars3 (hd eqs)]
   181               else
   182                 Pretty.block_enclose
   183                   (concat [head, print_tuple (map (str o lookup_var vars3) params),
   184                     str "match", str "{"], str "}")
   185                   (map print_clause eqs)
   186               end)
   187       | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
   188           let
   189             val tyvars = intro_vars (map fst vs) reserved;
   190             fun print_co ((co, _), []) =
   191                   concat [str "final", str "case", str "object", (str o deresolve_base) co,
   192                     str "extends", applify "[" "]" NOBR ((str o deresolve_base) name)
   193                       (replicate (length vs) (str "Nothing"))]
   194               | print_co ((co, vs_args), tys) =
   195                   let
   196                     val fields = Name.names (snd reserved) "a" tys;
   197                     val vars = intro_vars (map fst fields) reserved;
   198                     fun add_typargs1 p = applify "[" "]" NOBR p
   199                       (map (str o lookup_tyvar tyvars o fst) vs); (*FIXME*)
   200                     fun add_typargs2 p = applify "[" "]" NOBR p
   201                       (map (str o lookup_tyvar tyvars) vs_args); (*FIXME*)
   202                   in
   203                     concat [
   204                       applify "(" ")" NOBR
   205                         (add_typargs2 ((concat o map str) ["final", "case", "class", deresolve_base co]))
   206                         (map (uncurry (print_typed tyvars) o apfst str) fields),
   207                       str "extends",
   208                       add_typargs1 ((str o deresolve_base) name)
   209                     ]
   210                   end
   211           in
   212             Pretty.chunks (
   213               applify "[" "]" NOBR ((concat o map str) ["sealed", "class", deresolve_base name])
   214                 (map (str o prefix "+" o lookup_tyvar tyvars o fst) vs)
   215               :: map print_co cos
   216             )
   217           end
   218       | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
   219           let
   220             val tyvars = intro_vars [v] reserved;
   221             val vs = [(v, [name])];
   222             fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_tyvar tyvars) v];
   223             fun print_super_classes [] = NONE
   224               | print_super_classes classes = SOME (concat (str "extends"
   225                   :: separate (str "with") (map (add_typarg o str o deresolve o fst) classes)));
   226             fun print_tupled_typ ([], ty) =
   227                   print_typ tyvars NOBR ty
   228               | print_tupled_typ ([ty1], ty2) =
   229                   concat [print_typ tyvars BR ty1, str "=>", print_typ tyvars NOBR ty2]
   230               | print_tupled_typ (tys, ty) =
   231                   concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
   232                     str "=>", print_typ tyvars NOBR ty];
   233             fun print_classparam_val (classparam, ty) =
   234               concat [str "val", (str o Library.enclose "`" "+`:" o deresolve_base) classparam,
   235                 (print_tupled_typ o Code_Thingol.unfold_fun) ty]
   236             fun implicit_arguments tyvars vs vars = (*FIXME simplifiy*)
   237               let
   238                 val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block
   239                   [(str o deresolve) class, str "[", (str o lookup_tyvar tyvars) v, str "]"]) sort) vs;
   240                 val implicit_names = Name.variant_list [] (maps (fn (v, sort) => map (fn class =>
   241                   lookup_tyvar tyvars v ^ "_" ^ (Long_Name.base_name o deresolve) class) sort) vs);
   242                 val vars' = intro_vars implicit_names vars;
   243                 val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p])
   244                   implicit_names implicit_typ_ps;
   245               in ((implicit_names, implicit_ps), vars') end;
   246             fun print_classparam_def (classparam, ty) =
   247               let
   248                 val (tys, ty) = Code_Thingol.unfold_fun ty;
   249                 val params = Name.invents (snd reserved) "a" (length tys);
   250                 val vars = intro_vars params reserved;
   251                 val (([implicit], [p_implicit]), vars') = implicit_arguments tyvars vs vars;
   252                 val head = print_defhead tyvars vars' ((str o deresolve) classparam)
   253                   ((map o apsnd) (K []) vs) params tys [p_implicit] ty;
   254               in
   255                 concat [head, applify "(" ")" NOBR
   256                   (Pretty.block [str implicit, str ".", (str o Library.enclose "`" "+`" o deresolve_base) classparam])
   257                   (map (str o lookup_var vars') params)]
   258               end;
   259           in
   260             Pretty.chunks (
   261               (Pretty.block_enclose
   262                 (concat ([str "trait", add_typarg ((str o deresolve_base) name)]
   263                   @ the_list (print_super_classes super_classes) @ [str "{"]), str "}")
   264                 (map print_classparam_val classparams))
   265               :: map print_classparam_def classparams
   266             )
   267           end
   268       | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
   269             (super_instances, (classparam_instances, further_classparam_instances)))) =
   270           let
   271             val tyvars = intro_vars (map fst vs) reserved;
   272             val classtyp = (class, (tyco, map fst vs));
   273             fun print_classtyp' (class, (tyco, vs)) = (*FIXME already exists?*)
   274               applify "[" "]" NOBR(*? FIXME*) ((str o deresolve) class)
   275                 [print_typ tyvars NOBR (tyco `%% map ITyVar vs)]; (*FIXME a mess...*)
   276             fun print_typed' tyvars p classtyp = (*FIXME unify with existing print_typed*)
   277               Pretty.block [p, str ":", Pretty.brk 1, print_classtyp' classtyp];
   278             fun print_defhead' tyvars vars p vs params tys classtyp = (*FIXME unify with existing def_head*)
   279               Pretty.block [str "def ", print_typed' tyvars
   280                 (applify "(" ")" NOBR
   281                   (applify "[" "]" NOBR p (map (fn (v, sort) =>
   282                       (str o implode) (lookup_tyvar tyvars v :: map (prefix ": " o deresolve) sort)) vs))
   283                     (map2 (fn param => fn ty => print_typed tyvars ((str o lookup_var vars) param) ty)
   284                       params tys)) classtyp, str " ="];
   285             fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
   286               let
   287                 val auxs = Name.invents (snd reserved) "a" (length tys);
   288                 val vars = intro_vars auxs reserved;
   289                 val args = if null auxs then [] else
   290                   [concat [enum "," "(" ")" (map2 (fn aux => fn ty => print_typed tyvars ((str o lookup_var vars) aux) ty)
   291                     auxs tys), str "=>"]];
   292               in 
   293                 concat ([str "val", (str o Library.enclose "`" "+`" o deresolve_base) classparam,
   294                   str "="] @ args @ [print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)])
   295               end;
   296             val head = print_defhead' tyvars reserved ((str o deresolve) name) vs [] [] classtyp;
   297             val body = [str "new", print_classtyp' classtyp,
   298               Pretty.enum ";" "{ " " }" (map print_classparam_instance (classparam_instances @ further_classparam_instances))];
   299           in concat (str "implicit" :: head :: body) end;
   300   in print_stmt end;
   301 
   302 fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
   303   let
   304     val the_module_name = the_default "Program" module_name;
   305     val module_alias = K (SOME the_module_name);
   306     val reserved = Name.make_context reserved;
   307     fun prepare_stmt (name, stmt) (nsps, stmts) =
   308       let
   309         val (_, base) = Code_Printer.dest_name name;
   310         val mk_name_stmt = yield_singleton Name.variants;
   311         fun add_class ((nsp_class, nsp_object), nsp_common) =
   312           let
   313             val (base', nsp_class') = mk_name_stmt base nsp_class
   314           in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
   315         fun add_object ((nsp_class, nsp_object), nsp_common) =
   316           let
   317             val (base', nsp_object') = mk_name_stmt base nsp_object
   318           in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
   319         fun add_common upper ((nsp_class, nsp_object), nsp_common) =
   320           let
   321             val (base', nsp_common') =
   322               mk_name_stmt (if upper then first_upper base else base) nsp_common
   323           in (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common')) end;
   324         val add_name = case stmt
   325          of Code_Thingol.Fun _ => add_object
   326           | Code_Thingol.Datatype _ => add_class
   327           | Code_Thingol.Datatypecons _ => add_common true
   328           | Code_Thingol.Class _ => add_class
   329           | Code_Thingol.Classrel _ => add_object
   330           | Code_Thingol.Classparam _ => add_object
   331           | Code_Thingol.Classinst _ => add_common false;
   332         fun add_stmt base' = case stmt
   333          of Code_Thingol.Datatypecons _ => cons (name, (base', NONE))
   334           | Code_Thingol.Classrel _ => cons (name, (base', NONE))
   335           | Code_Thingol.Classparam _ => cons (name, (base', NONE))
   336           | _ => cons (name, (base', SOME stmt));
   337       in
   338         nsps
   339         |> add_name
   340         |-> (fn base' => rpair (add_stmt base' stmts))
   341       end;
   342     val stmts = AList.make (Graph.get_node program) (Graph.strong_conn program |> flat)
   343       |> filter_out (Code_Thingol.is_case o snd);
   344     val (_, sca_program) = fold prepare_stmt stmts (((reserved, reserved), reserved), []);
   345     fun deresolver name = (fst o the o AList.lookup (op =) sca_program) name
   346       handle Option => error ("Unknown statement name: " ^ labelled_name name);
   347   in (deresolver, (the_module_name, sca_program)) end;
   348 
   349 fun serialize_scala raw_module_name labelled_name
   350     raw_reserved includes raw_module_alias
   351     _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
   352   let
   353     val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
   354     val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
   355     val reserved = fold (insert (op =) o fst) includes raw_reserved;
   356     val (deresolver, (the_module_name, sca_program)) = scala_program_of_program labelled_name
   357       module_name reserved raw_module_alias program;
   358     val reserved = make_vars reserved;
   359     fun args_num c = case Graph.get_node program c
   360      of Code_Thingol.Fun (_, (((_, ty), []), _)) => (length o fst o Code_Thingol.unfold_fun) ty
   361       | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
   362       | Code_Thingol.Datatypecons (_, tyco) =>
   363           let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
   364           in (length o the o AList.lookup (eq_fst op =) constrs) (c, []) end (*FIXME simplify lookup*)
   365       | Code_Thingol.Classparam (_, class) =>
   366           let val Code_Thingol.Class (_, (_, (_, classparams))) = Graph.get_node program class
   367           in (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) classparams) c end;
   368     fun is_singleton c = case Graph.get_node program c
   369      of Code_Thingol.Datatypecons (_, tyco) =>
   370           let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
   371           in (null o the o AList.lookup (eq_fst op =) constrs) (c, []) end (*FIXME simplify lookup*)
   372       | _ => false;
   373     val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
   374       reserved args_num is_singleton deresolver;
   375     fun print_module name content =
   376       (name, Pretty.chunks [
   377         str ("object " ^ name ^ " {"),
   378         str "",
   379         content,
   380         str "",
   381         str "}"
   382       ]);
   383     fun serialize_module the_module_name sca_program =
   384       let
   385         val content = Pretty.chunks2 (map_filter
   386           (fn (name, (_, SOME stmt)) => SOME (print_stmt (name, stmt))
   387             | (_, (_, NONE)) => NONE) sca_program);
   388       in print_module the_module_name content end;
   389     fun check_destination destination =
   390       (File.check destination; destination);
   391     fun write_module destination (modlname, content) =
   392       let
   393         val filename = case modlname
   394          of "" => Path.explode "Main.scala"
   395           | _ => (Path.ext "scala" o Path.explode o implode o separate "/"
   396                 o Long_Name.explode) modlname;
   397         val pathname = Path.append destination filename;
   398         val _ = File.mkdir (Path.dir pathname);
   399       in File.write pathname (code_of_pretty content) end
   400   in
   401     Code_Target.mk_serialization target NONE
   402       (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
   403         (write_module (check_destination file)))
   404       (rpair [] o cat_lines o map (code_of_pretty o snd))
   405       (map (uncurry print_module) includes
   406         @| serialize_module the_module_name sca_program)
   407       destination
   408   end;
   409 
   410 val literals = let
   411   fun char_scala c = if c = "'" then "\\'"
   412     else if c = "\"" then "\\\""
   413     else if c = "\\" then "\\\\"
   414     else let val k = ord c
   415     in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end
   416   fun numeral_scala k = if k < 0
   417     then if k <= 2147483647 then "- " ^ string_of_int (~ k)
   418       else quote ("- " ^ string_of_int (~ k))
   419     else if k <= 2147483647 then string_of_int k
   420       else quote (string_of_int k)
   421 in Literals {
   422   literal_char = Library.enclose "'" "'" o char_scala,
   423   literal_string = quote o translate_string char_scala,
   424   literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   425   literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
   426   literal_naive_numeral = fn k => if k >= 0
   427     then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")",
   428   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   429   infix_cons = (6, "::")
   430 } end;
   431 
   432 
   433 (** Isar setup **)
   434 
   435 fun isar_seri_scala module_name =
   436   Code_Target.parse_args (Scan.succeed ())
   437   #> (fn () => serialize_scala module_name);
   438 
   439 val setup =
   440   Code_Target.add_target (target, (isar_seri_scala, literals))
   441   #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   442       brackify_infix (1, R) fxy (
   443         print_typ BR ty1 (*product type vs. tupled arguments!*),
   444         str "=>",
   445         print_typ (INFX (1, R)) ty2
   446       )))
   447   #> fold (Code_Target.add_reserved target) [
   448       "abstract", "case", "catch", "class", "def", "do", "else", "extends", "false",
   449       "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",
   450       "match", "new", "null", "object", "override", "package", "private", "protected",
   451       "requires", "return", "sealed", "super", "this", "throw", "trait", "try",
   452       "true", "type", "val", "var", "while", "with", "yield"
   453     ]
   454   #> fold (Code_Target.add_reserved target) [
   455       "error", "apply", "List", "Nil", "BigInt"
   456     ];
   457 
   458 end; (*struct*)