src/Tools/Code/code_scala.ML
author haftmann
Thu Jun 17 15:59:48 2010 +0200 (2010-06-17)
changeset 37450 45073611170a
parent 37447 ad3e04f289b6
child 37453 44a307746163
permissions -rw-r--r--
first serious draft of a scala code generator
     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           (*let
   301             val tyvars = intro_vars (map fst vs) reserved;
   302             val insttyp = tyco `%% map (ITyVar o fst) vs;
   303             val p_inst_typ = print_typ tyvars NOBR insttyp;
   304             fun add_typ_params p = applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs);
   305             fun add_inst_typ p = Pretty.block [p, str "[", p_inst_typ, str "]"];
   306             val ((implicit_names, implicit_ps), vars) = implicit_arguments tyvars vs reserved;
   307             fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
   308               let
   309                 val auxs = Name.invents (snd reserved) "a" (length tys);
   310                 val vars = intro_vars auxs reserved;
   311                 val args = if null auxs then [] else
   312                   [concat [enum "," "(" ")" (map2 (fn aux => fn ty => print_typed tyvars ((str o lookup_var vars) aux) ty)
   313                     auxs tys), str "=>"]];
   314               in 
   315                 concat ([str "val", (str o Library.enclose "`" "+`" o deresolve_base) classparam,
   316                   str "="] @ args @ [print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)])
   317               end;
   318           in
   319             Pretty.chunks [
   320               Pretty.block_enclose
   321                 (concat ([str "trait",
   322                     add_typ_params ((str o deresolve_base) name),
   323                     str "extends",
   324                     Pretty.block [(str o deresolve) class, str "[", p_inst_typ, str "]"]]
   325                     @ map (fn (_, (_, (super_instance, _))) => add_typ_params (str ("with " ^ deresolve super_instance)))
   326                       super_instances @| str "{"), str "}")
   327                 (map (fn p => Pretty.block [str "implicit val arg$", p]) implicit_ps
   328                   @ map print_classparam_instance classparam_instances),
   329               concat [str "implicit", str (if null vs then "val" else "def"),
   330                 applify "(implicit " ")" NOBR (applify "[" "]" NOBR
   331                   ((str o deresolve_base) name) (map (str o lookup_tyvar tyvars o fst) vs))
   332                     implicit_ps,
   333                   str "=", str "new", applify "[" "]" NOBR ((str o deresolve_base) name)
   334                       (map (str o lookup_tyvar tyvars o fst) vs),
   335                     Pretty.enum ";" "{ " " }" (map (str o (fn v => "val arg$" ^ v ^ " = " ^ v) o lookup_var vars)
   336                       implicit_names)]
   337             ]
   338           end;*)
   339   in print_stmt end;
   340 
   341 fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
   342   let
   343     val the_module_name = the_default "Program" module_name;
   344     val module_alias = K (SOME the_module_name);
   345     val reserved = Name.make_context reserved;
   346     fun prepare_stmt (name, stmt) (nsps, stmts) =
   347       let
   348         val (_, base) = Code_Printer.dest_name name;
   349         val mk_name_stmt = yield_singleton Name.variants;
   350         fun add_class ((nsp_class, nsp_object), nsp_common) =
   351           let
   352             val (base', nsp_class') = mk_name_stmt base nsp_class
   353           in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
   354         fun add_object ((nsp_class, nsp_object), nsp_common) =
   355           let
   356             val (base', nsp_object') = mk_name_stmt base nsp_object
   357           in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
   358         fun add_common upper ((nsp_class, nsp_object), nsp_common) =
   359           let
   360             val (base', nsp_common') =
   361               mk_name_stmt (if upper then first_upper base else base) nsp_common
   362           in (base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common')) end;
   363         val add_name = case stmt
   364          of Code_Thingol.Fun _ => add_object
   365           | Code_Thingol.Datatype _ => add_class
   366           | Code_Thingol.Datatypecons _ => add_common true
   367           | Code_Thingol.Class _ => add_class
   368           | Code_Thingol.Classrel _ => add_object
   369           | Code_Thingol.Classparam _ => add_object
   370           | Code_Thingol.Classinst _ => add_common false;
   371         fun add_stmt base' = case stmt
   372          of Code_Thingol.Datatypecons _ => cons (name, (base', NONE))
   373           | Code_Thingol.Classrel _ => cons (name, (base', NONE))
   374           | Code_Thingol.Classparam _ => cons (name, (base', NONE))
   375           | _ => cons (name, (base', SOME stmt));
   376       in
   377         nsps
   378         |> add_name
   379         |-> (fn base' => rpair (add_stmt base' stmts))
   380       end;
   381     val stmts = AList.make (Graph.get_node program) (Graph.strong_conn program |> flat)
   382       |> filter_out (Code_Thingol.is_case o snd);
   383     val (_, sca_program) = fold prepare_stmt stmts (((reserved, reserved), reserved), []);
   384     fun deresolver name = (fst o the o AList.lookup (op =) sca_program) name
   385       handle Option => error ("Unknown statement name: " ^ labelled_name name);
   386   in (deresolver, (the_module_name, sca_program)) end;
   387 
   388 fun serialize_scala raw_module_name labelled_name
   389     raw_reserved includes raw_module_alias
   390     _ syntax_tyco syntax_const (code_of_pretty, code_writeln) program stmt_names destination =
   391   let
   392     val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
   393     val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
   394     val reserved = fold (insert (op =) o fst) includes raw_reserved;
   395     val (deresolver, (the_module_name, sca_program)) = scala_program_of_program labelled_name
   396       module_name reserved raw_module_alias program;
   397     val reserved = make_vars reserved;
   398     fun args_num c = case Graph.get_node program c
   399      of Code_Thingol.Fun (_, (((_, ty), []), _)) => (length o fst o Code_Thingol.unfold_fun) ty
   400       | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
   401       | Code_Thingol.Datatypecons (_, tyco) =>
   402           let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
   403           in (length o the o AList.lookup (eq_fst op =) constrs) (c, []) end (*FIXME simplify lookup*)
   404       | Code_Thingol.Classparam (_, class) =>
   405           let val Code_Thingol.Class (_, (_, (_, classparams))) = Graph.get_node program class
   406           in (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) classparams) c end;
   407     fun is_singleton c = case Graph.get_node program c
   408      of Code_Thingol.Datatypecons (_, tyco) =>
   409           let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
   410           in (null o the o AList.lookup (eq_fst op =) constrs) (c, []) end (*FIXME simplify lookup*)
   411       | _ => false;
   412     val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
   413       reserved args_num is_singleton deresolver;
   414     fun print_module name content =
   415       (name, Pretty.chunks [
   416         str ("object " ^ name ^ " {"),
   417         str "",
   418         content,
   419         str "",
   420         str "}"
   421       ]);
   422     fun serialize_module the_module_name sca_program =
   423       let
   424         val content = Pretty.chunks2 (map_filter
   425           (fn (name, (_, SOME stmt)) => SOME (print_stmt (name, stmt))
   426             | (_, (_, NONE)) => NONE) sca_program);
   427       in print_module the_module_name content end;
   428     fun check_destination destination =
   429       (File.check destination; destination);
   430     fun write_module destination (modlname, content) =
   431       let
   432         val filename = case modlname
   433          of "" => Path.explode "Main.scala"
   434           | _ => (Path.ext "scala" o Path.explode o implode o separate "/"
   435                 o Long_Name.explode) modlname;
   436         val pathname = Path.append destination filename;
   437         val _ = File.mkdir (Path.dir pathname);
   438       in File.write pathname (code_of_pretty content) end
   439   in
   440     Code_Target.mk_serialization target NONE
   441       (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
   442         (write_module (check_destination file)))
   443       (rpair [] o cat_lines o map (code_of_pretty o snd))
   444       (map (uncurry print_module) includes
   445         @| serialize_module the_module_name sca_program)
   446       destination
   447   end;
   448 
   449 val literals = let
   450   fun char_scala c = if c = "'" then "\\'"
   451     else if c = "\"" then "\\\""
   452     else if c = "\\" then "\\\\"
   453     else let val k = ord c
   454     in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end
   455   fun numeral_scala k = if k < 0
   456     then if k <= 2147483647 then "- " ^ string_of_int (~ k)
   457       else quote ("- " ^ string_of_int (~ k))
   458     else if k <= 2147483647 then string_of_int k
   459       else quote (string_of_int k)
   460 in Literals {
   461   literal_char = Library.enclose "'" "'" o char_scala,
   462   literal_string = quote o translate_string char_scala,
   463   literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   464   literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
   465   literal_naive_numeral = fn k => if k >= 0
   466     then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")",
   467   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   468   infix_cons = (6, "::")
   469 } end;
   470 
   471 
   472 (** Isar setup **)
   473 
   474 fun isar_seri_scala module_name =
   475   Code_Target.parse_args (Scan.succeed ())
   476   #> (fn () => serialize_scala module_name);
   477 
   478 val setup =
   479   Code_Target.add_target (target, (isar_seri_scala, literals))
   480   #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   481       brackify_infix (1, R) fxy (
   482         print_typ BR ty1 (*product type vs. tupled arguments!*),
   483         str "=>",
   484         print_typ (INFX (1, R)) ty2
   485       )))
   486   #> fold (Code_Target.add_reserved target) [
   487       "abstract", "case", "catch", "class", "def", "do", "else", "extends", "false",
   488       "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",
   489       "match", "new", "null", "object", "override", "package", "private", "protected",
   490       "requires", "return", "sealed", "super", "this", "throw", "trait", "try",
   491       "true", "type", "val", "var", "while", "with", "yield"
   492     ]
   493   #> fold (Code_Target.add_reserved target) [
   494       "error", "apply", "List", "Nil", "BigInt"
   495     ];
   496 
   497 end; (*struct*)