src/Tools/Code/code_scala.ML
author haftmann
Thu Aug 26 10:16:22 2010 +0200 (2010-08-26)
changeset 38771 f9cd27cbe8a4
parent 38769 317e64c886d2
child 38772 eb7bc47f062b
permissions -rw-r--r--
code_include Scala: qualify module nmae
     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 syntax_tyco syntax_const reserved
    28     args_num is_singleton_constr deresolve =
    29   let
    30     val deresolve_base = Long_Name.base_name o deresolve;
    31     fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
    32     fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
    33     fun print_tyco_expr tyvars fxy (tyco, tys) = applify "[" "]"
    34           (print_typ tyvars NOBR) fxy ((str o deresolve) tyco) tys
    35     and print_typ tyvars fxy (tyco `%% tys) = (case syntax_tyco tyco
    36          of NONE => print_tyco_expr tyvars fxy (tyco, tys)
    37           | SOME (i, print) => print (print_typ tyvars) fxy tys)
    38       | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
    39     fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (class, [ty]);
    40     fun print_tupled_typ tyvars ([], ty) =
    41           print_typ tyvars NOBR ty
    42       | print_tupled_typ tyvars ([ty1], ty2) =
    43           concat [print_typ tyvars BR ty1, str "=>", print_typ tyvars NOBR ty2]
    44       | print_tupled_typ tyvars (tys, ty) =
    45           concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
    46             str "=>", print_typ tyvars NOBR ty];
    47     fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2];
    48     fun print_var vars NONE = str "_"
    49       | print_var vars (SOME v) = (str o lookup_var vars) v
    50     fun print_term tyvars is_pat some_thm vars fxy (IConst c) =
    51           print_app tyvars is_pat some_thm vars fxy (c, [])
    52       | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
    53           (case Code_Thingol.unfold_const_app t
    54            of SOME app => print_app tyvars is_pat some_thm vars fxy app
    55             | _ => applify "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy
    56                 (print_term tyvars is_pat some_thm vars BR t1) [t2])
    57       | print_term tyvars is_pat some_thm vars fxy (IVar v) =
    58           print_var vars v
    59       | print_term tyvars is_pat some_thm vars fxy ((v, ty) `|=> t) =
    60           let
    61             val vars' = intro_vars (the_list v) vars;
    62           in
    63             concat [
    64               enclose "(" ")" [constraint (print_var vars' v) (print_typ tyvars NOBR ty)],
    65               str "=>",
    66               print_term tyvars false some_thm vars' NOBR t
    67             ]
    68           end 
    69       | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
    70           (case Code_Thingol.unfold_const_app t0
    71            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
    72                 then print_case tyvars some_thm vars fxy cases
    73                 else print_app tyvars is_pat some_thm vars fxy c_ts
    74             | NONE => print_case tyvars some_thm vars fxy cases)
    75     and print_app tyvars is_pat some_thm vars fxy
    76         (app as ((c, ((arg_typs, _), function_typs)), ts)) =
    77       let
    78         val k = length ts;
    79         val arg_typs' = if is_pat orelse
    80           (is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
    81         val (l, print') = case syntax_const c
    82          of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
    83               (print_term tyvars is_pat some_thm vars NOBR) fxy
    84                 (applify "[" "]" (print_typ tyvars NOBR)
    85                   NOBR ((str o deresolve) c) arg_typs') ts)
    86           | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
    87               (print_term tyvars is_pat some_thm vars NOBR) fxy
    88                 (applify "[" "]" (print_typ tyvars NOBR)
    89                   NOBR (str s) arg_typs') ts)
    90           | SOME (Complex_const_syntax (k, print)) =>
    91               (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
    92                 (ts ~~ take k function_typs))
    93       in if k = l then print' fxy ts
    94       else if k < l then
    95         print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
    96       else let
    97         val (ts1, ts23) = chop l ts;
    98       in
    99         Pretty.block (print' BR ts1 :: map (fn t => Pretty.block
   100           [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23)
   101       end end
   102     and print_bind tyvars some_thm fxy p =
   103       gen_print_bind (print_term tyvars true) some_thm fxy p
   104     and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
   105           let
   106             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
   107             fun print_match ((IVar NONE, _), t) vars =
   108                   ((true, print_term tyvars false some_thm vars NOBR t), vars)
   109               | print_match ((pat, ty), t) vars =
   110                   vars
   111                   |> print_bind tyvars some_thm BR pat
   112                   |>> (fn p => (false, concat [str "val", constraint p (print_typ tyvars NOBR ty),
   113                       str "=", print_term tyvars false some_thm vars NOBR t]))
   114             val (seps_ps, vars') = fold_map print_match binds vars;
   115             val all_seps_ps = seps_ps @ [(true, print_term tyvars false some_thm vars' NOBR body)];
   116             fun insert_seps [(_, p)] = [p]
   117               | insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) =
   118                   (if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps
   119           in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}")
   120           end
   121       | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
   122           let
   123             fun print_select (pat, body) =
   124               let
   125                 val (p_pat, vars') = print_bind tyvars some_thm NOBR pat vars;
   126                 val p_body = print_term tyvars false some_thm vars' NOBR body
   127               in concat [str "case", p_pat, str "=>", p_body] end;
   128           in brackify_block fxy
   129             (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"])
   130             (map print_select clauses)
   131             (str "}") 
   132           end
   133       | print_case tyvars some_thm vars fxy ((_, []), _) =
   134           (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
   135     fun print_context tyvars vs name = applify "[" "]"
   136       (fn (v, sort) => (Pretty.block o map str)
   137         (lookup_tyvar tyvars v :: maps (fn sort => [": ", deresolve sort]) sort))
   138           NOBR ((str o deresolve_base) name) vs;
   139     fun print_defhead tyvars vars name vs params tys ty =
   140       Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
   141         constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
   142           NOBR (print_context tyvars vs name) (params ~~ tys)) (print_typ tyvars NOBR ty),
   143             str " ="];
   144     fun print_def name (vs, ty) [] =
   145           let
   146             val (tys, ty') = Code_Thingol.unfold_fun ty;
   147             val params = Name.invents (snd reserved) "a" (length tys);
   148             val tyvars = intro_tyvars vs reserved;
   149             val vars = intro_vars params reserved;
   150           in
   151             concat [print_defhead tyvars vars name vs params tys ty',
   152               str ("error(\"" ^ name ^ "\")")]
   153           end
   154       | print_def name (vs, ty) eqs =
   155           let
   156             val tycos = fold (fn ((ts, t), _) =>
   157               fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
   158             val tyvars = reserved
   159               |> intro_base_names
   160                    (is_none o syntax_tyco) deresolve tycos
   161               |> intro_tyvars vs;
   162             val simple = case eqs
   163              of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
   164               | _ => false;
   165             val consts = fold Code_Thingol.add_constnames
   166               (map (snd o fst) eqs) [];
   167             val vars1 = reserved
   168               |> intro_base_names
   169                    (is_none o syntax_const) deresolve consts
   170             val params = if simple
   171               then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
   172               else aux_params vars1 (map (fst o fst) eqs);
   173             val vars2 = intro_vars params vars1;
   174             val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty;
   175             fun print_tuple [p] = p
   176               | print_tuple ps = enum "," "(" ")" ps;
   177             fun print_rhs vars' ((_, t), (some_thm, _)) =
   178               print_term tyvars false some_thm vars' NOBR t;
   179             fun print_clause (eq as ((ts, _), (some_thm, _))) =
   180               let
   181                 val vars' = intro_vars ((fold o Code_Thingol.fold_varnames)
   182                   (insert (op =)) ts []) vars1;
   183               in
   184                 concat [str "case",
   185                   print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
   186                   str "=>", print_rhs vars' eq]
   187               end;
   188             val head = print_defhead tyvars vars2 name vs params tys' ty';
   189           in if simple then
   190             concat [head, print_rhs vars2 (hd eqs)]
   191           else
   192             Pretty.block_enclose
   193               (concat [head, print_tuple (map (str o lookup_var vars2) params),
   194                 str "match", str "{"], str "}")
   195               (map print_clause eqs)
   196           end;
   197     val print_method = str o Library.enclose "`" "`" o space_implode "+"
   198       o fst o split_last o Long_Name.explode;
   199     fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
   200           print_def name (vs, ty) (filter (snd o snd) raw_eqs)
   201       | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
   202           let
   203             val tyvars = intro_tyvars vs reserved;
   204             fun print_co ((co, _), []) =
   205                   concat [str "final", str "case", str "object", (str o deresolve_base) co,
   206                     str "extends", applify "[" "]" I NOBR ((str o deresolve_base) name)
   207                       (replicate (length vs) (str "Nothing"))]
   208               | print_co ((co, vs_args), tys) =
   209                   concat [applify "(" ")"
   210                     (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) NOBR
   211                     (applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((concat o map str)
   212                       ["final", "case", "class", deresolve_base co]) vs_args)
   213                     (Name.names (snd reserved) "a" tys),
   214                     str "extends",
   215                     applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
   216                       ((str o deresolve_base) name) vs
   217                   ];
   218           in
   219             Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars o fst)
   220               NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_base name]) vs
   221                 :: map print_co cos)
   222           end
   223       | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
   224           let
   225             val tyvars = intro_tyvars [(v, [name])] reserved;
   226             fun add_typarg s = Pretty.block
   227               [str s, str "[", (str o lookup_tyvar tyvars) v, str "]"];
   228             fun print_super_classes [] = NONE
   229               | print_super_classes classes = SOME (concat (str "extends"
   230                   :: separate (str "with") (map (add_typarg o deresolve o fst) classes)));
   231             fun print_classparam_val (classparam, ty) =
   232               concat [str "val", constraint (print_method classparam)
   233                 ((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)];
   234             fun print_classparam_def (classparam, ty) =
   235               let
   236                 val (tys, ty) = Code_Thingol.unfold_fun ty;
   237                 val [implicit_name] = Name.invents (snd reserved) (lookup_tyvar tyvars v) 1;
   238                 val proto_vars = intro_vars [implicit_name] reserved;
   239                 val auxs = Name.invents (snd proto_vars) "a" (length tys);
   240                 val vars = intro_vars auxs proto_vars;
   241               in
   242                 concat [str "def", constraint (Pretty.block [applify "(" ")"
   243                   (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
   244                   (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_base classparam))
   245                   (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
   246                   add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
   247                   applify "(" ")" (str o lookup_var vars) NOBR
   248                   (Pretty.block [str implicit_name, str ".", print_method classparam]) auxs]
   249               end;
   250           in
   251             Pretty.chunks (
   252               (Pretty.block_enclose
   253                 (concat ([str "trait", (add_typarg o deresolve_base) name]
   254                   @ the_list (print_super_classes super_classes) @ [str "{"]), str "}")
   255                 (map print_classparam_val classparams))
   256               :: map print_classparam_def classparams
   257             )
   258           end
   259       | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
   260             (super_instances, (classparam_instances, further_classparam_instances)))) =
   261           let
   262             val tyvars = intro_tyvars vs reserved;
   263             val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
   264             fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
   265               let
   266                 val aux_tys = Name.names (snd reserved) "a" tys;
   267                 val auxs = map fst aux_tys;
   268                 val vars = intro_vars auxs reserved;
   269                 val aux_abstr = if null auxs then [] else [enum "," "(" ")"
   270                   (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
   271                   (print_typ tyvars NOBR ty)) aux_tys), str "=>"];
   272               in 
   273                 concat ([str "val", print_method classparam, str "="]
   274                   @ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR
   275                     (const, map (IVar o SOME) auxs))
   276               end;
   277           in
   278             Pretty.block_enclose (concat [str "implicit def",
   279               constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp),
   280               str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
   281                 (map print_classparam_instance (classparam_instances @ further_classparam_instances))
   282           end;
   283   in print_stmt end;
   284 
   285 local
   286 
   287 (* hierarchical module name space *)
   288 
   289 datatype node =
   290     Dummy
   291   | Stmt of Code_Thingol.stmt
   292   | Module of ((Name.context * Name.context) * Name.context) * (string list * (string * node) Graph.T);
   293 
   294 in
   295 
   296 fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
   297   let
   298 
   299     (* building module name hierarchy *)
   300     val module_alias = if is_some module_name then K module_name else raw_module_alias;
   301     fun alias_fragments name = case module_alias name
   302      of SOME name' => Long_Name.explode name'
   303       | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
   304           (Long_Name.explode name);
   305     val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
   306     val fragments_tab = fold (fn name => Symtab.update
   307       (name, alias_fragments name)) module_names Symtab.empty;
   308     val dest_name = Code_Printer.dest_name #>> (the o Symtab.lookup fragments_tab);
   309 
   310     (* building empty module hierarchy *)
   311     val empty_module = (((reserved, reserved), reserved), ([], Graph.empty));
   312     fun map_module f (Module content) = Module (f content);
   313     fun declare_module name_fragement ((nsp_class, nsp_object), nsp_common) =
   314       let
   315         val declare = Name.declare name_fragement;
   316       in ((declare nsp_class, declare nsp_object), declare nsp_common) end;
   317     fun ensure_module name_fragement (nsps, (implicits, nodes)) =
   318       if can (Graph.get_node nodes) name_fragement then (nsps, (implicits, nodes))
   319       else
   320         (nsps |> declare_module name_fragement, (implicits,
   321           nodes |> Graph.new_node (name_fragement, (name_fragement, Module empty_module))));
   322     fun allocate_module [] = I
   323       | allocate_module (name_fragment :: name_fragments) =
   324           ensure_module name_fragment
   325           #> (apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module o allocate_module) name_fragments;
   326     val empty_program = Symtab.fold (fn (_, fragments) => allocate_module fragments)
   327       fragments_tab empty_module;
   328     fun change_module [] = I
   329       | change_module (name_fragment :: name_fragments) =
   330           apsnd o apsnd o Graph.map_node name_fragment o apsnd o map_module
   331             o change_module name_fragments;
   332 
   333     (* statement declaration *)
   334     fun namify_class base ((nsp_class, nsp_object), nsp_common) =
   335       let
   336         val (base', nsp_class') = yield_singleton Name.variants base nsp_class
   337       in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
   338     fun namify_object base ((nsp_class, nsp_object), nsp_common) =
   339       let
   340         val (base', nsp_object') = yield_singleton Name.variants base nsp_object
   341       in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
   342     fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
   343       let
   344         val (base', nsp_common') =
   345           yield_singleton Name.variants (if upper then first_upper base else base) nsp_common
   346       in
   347         (base',
   348           ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
   349       end;
   350     fun declare_stmt name stmt =
   351       let
   352         val (name_fragments, base) = dest_name name;
   353         val namify = case stmt
   354          of Code_Thingol.Fun _ => namify_object
   355           | Code_Thingol.Datatype _ => namify_class
   356           | Code_Thingol.Datatypecons _ => namify_common true
   357           | Code_Thingol.Class _ => namify_class
   358           | Code_Thingol.Classrel _ => namify_object
   359           | Code_Thingol.Classparam _ => namify_object
   360           | Code_Thingol.Classinst _ => namify_common false;
   361         val stmt' = case stmt
   362          of Code_Thingol.Datatypecons _ => Dummy
   363           | Code_Thingol.Classrel _ => Dummy
   364           | Code_Thingol.Classparam _ => Dummy
   365           | _ => Stmt stmt;
   366         fun is_classinst stmt = case stmt
   367          of Code_Thingol.Classinst _ => true
   368           | _ => false;
   369         val implicit_deps = filter (is_classinst o Graph.get_node program)
   370           (Graph.imm_succs program name);
   371         fun declaration (nsps, (implicits, nodes)) =
   372           let
   373             val (base', nsps') = namify base nsps;
   374             val implicits' = union (op =) implicit_deps implicits;
   375             val nodes' = Graph.new_node (name, (base', stmt')) nodes;
   376           in (nsps', (implicits', nodes')) end;
   377       in change_module name_fragments declaration end;
   378 
   379     (* dependencies *)
   380     fun add_dependency name name' =
   381       let
   382         val (name_fragments, base) = dest_name name;
   383         val (name_fragments', base') = dest_name name';
   384         val (name_fragments_common, (diff, diff')) =
   385           chop_prefix (op =) (name_fragments, name_fragments');
   386         val dep = if null diff then (name, name') else (hd diff, hd diff')
   387       in (change_module name_fragments_common o apsnd o apsnd) (Graph.add_edge dep) end;
   388 
   389     (* producing program *)
   390     val (_, (_, sca_program)) = empty_program
   391       |> Graph.fold (fn (name, (stmt, _)) => declare_stmt name stmt) program
   392       |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
   393 
   394     (* deresolving *)
   395     fun deresolve name =
   396       let
   397         val (name_fragments, _) = dest_name name;
   398         val nodes = fold (fn name_fragement => fn nodes => case Graph.get_node nodes name_fragement
   399          of (_, Module (_, (_, nodes))) => nodes) name_fragments sca_program;
   400         val (base', _) = Graph.get_node nodes name;
   401       in Long_Name.implode (name_fragments @ [base']) end
   402         handle Graph.UNDEF _ => error ("Unknown statement name: " ^ labelled_name name);
   403 
   404   in (deresolve, sca_program) end;
   405 
   406 fun serialize_scala raw_module_name labelled_name
   407     raw_reserved includes raw_module_alias
   408     _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
   409     program stmt_names destination =
   410   let
   411 
   412     (* generic nonsense *)
   413     val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
   414     val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
   415 
   416     (* preprocess program *)
   417     val reserved = fold (insert (op =) o fst) includes raw_reserved;
   418     val (deresolve, sca_program) = scala_program_of_program labelled_name
   419       module_name (Name.make_context reserved) raw_module_alias program;
   420 
   421     (* print statements *)
   422     fun lookup_constr tyco constr = case Graph.get_node program tyco
   423      of Code_Thingol.Datatype (_, (_, constrs)) =>
   424           the (AList.lookup (op = o apsnd fst) constrs constr);
   425     fun classparams_of_class class = case Graph.get_node program class
   426      of Code_Thingol.Class (_, (_, (_, classparams))) => classparams;
   427     fun args_num c = case Graph.get_node program c
   428      of Code_Thingol.Fun (_, (((_, ty), []), _)) =>
   429           (length o fst o Code_Thingol.unfold_fun) ty
   430       | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
   431       | Code_Thingol.Datatypecons (_, tyco) => length (lookup_constr tyco c)
   432       | Code_Thingol.Classparam (_, class) =>
   433           (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =)
   434             (classparams_of_class class)) c;
   435     fun is_singleton_constr c = case Graph.get_node program c
   436      of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
   437       | _ => false;
   438     val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
   439       (make_vars reserved) args_num is_singleton_constr deresolve;
   440 
   441     (* print nodes *)
   442     fun print_implicits [] = NONE
   443       | print_implicits implicits = (SOME o Pretty.block)
   444           (str "import /*implicits*/" :: Pretty.brk 1 :: Pretty.commas (map (str o deresolve) implicits));
   445     fun print_module base implicits p = Pretty.chunks2
   446       ([str ("object " ^ base ^ " {")] @ the_list (print_implicits implicits)
   447         @ [p, str ("} /* object " ^ base ^ " */")]);
   448     fun print_node (_, Dummy) = NONE
   449       | print_node (name, Stmt stmt) = if not (not (null presentation_stmt_names)
   450           andalso member (op =) presentation_stmt_names name)
   451           then SOME (print_stmt (name, stmt))
   452           else NONE
   453       | print_node (name, Module (_, (implicits, nodes))) = if null presentation_stmt_names
   454           then case print_nodes nodes
   455            of NONE => NONE
   456             | SOME p => SOME (print_module (Long_Name.base_name name) implicits p)
   457           else print_nodes nodes
   458     and print_nodes nodes = let
   459         val ps = map_filter (fn name => print_node (name,
   460           snd (Graph.get_node nodes name)))
   461             ((rev o flat o Graph.strong_conn) nodes);
   462       in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
   463 
   464     (* serialization *)
   465     val p = Pretty.chunks2 (map (fn (base, p) => print_module base [] p) includes
   466       @ the_list (print_nodes sca_program));
   467   in
   468     Code_Target.mk_serialization target
   469       (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty)
   470       (rpair [] o code_of_pretty) p destination
   471   end;
   472 
   473 end; (*local*)
   474 
   475 val literals = let
   476   fun char_scala c = if c = "'" then "\\'"
   477     else if c = "\"" then "\\\""
   478     else if c = "\\" then "\\\\"
   479     else let val k = ord c
   480     in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end
   481   fun numeral_scala k = if k < 0
   482     then if k > ~ 2147483647 then "- " ^ string_of_int (~ k)
   483       else quote ("- " ^ string_of_int (~ k))
   484     else if k <= 2147483647 then string_of_int k
   485       else quote (string_of_int k)
   486 in Literals {
   487   literal_char = Library.enclose "'" "'" o char_scala,
   488   literal_string = quote o translate_string char_scala,
   489   literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   490   literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
   491   literal_alternative_numeral = fn k => "Natural.Nat(" ^ numeral_scala k ^ ")",
   492   literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   493   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   494   infix_cons = (6, "::")
   495 } end;
   496 
   497 
   498 (** Isar setup **)
   499 
   500 fun isar_serializer module_name =
   501   Code_Target.parse_args (Scan.succeed ())
   502   #> (fn () => serialize_scala module_name);
   503 
   504 val setup =
   505   Code_Target.add_target
   506     (target, { serializer = isar_serializer, literals = literals,
   507       check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
   508         make_command = fn scala_home => fn p => fn _ =>
   509           "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
   510             ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " " ^ File.shell_path p } })
   511   #> Code_Target.add_syntax_tyco target "fun"
   512      (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   513         brackify_infix (1, R) fxy (
   514           print_typ BR ty1 (*product type vs. tupled arguments!*),
   515           str "=>",
   516           print_typ (INFX (1, R)) ty2
   517         )))
   518   #> fold (Code_Target.add_reserved target) [
   519       "abstract", "case", "catch", "class", "def", "do", "else", "extends", "false",
   520       "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",
   521       "match", "new", "null", "object", "override", "package", "private", "protected",
   522       "requires", "return", "sealed", "super", "this", "throw", "trait", "try",
   523       "true", "type", "val", "var", "while", "with", "yield"
   524     ]
   525   #> fold (Code_Target.add_reserved target) [
   526       "apply", "error", "BigInt", "Nil", "List"
   527     ];
   528 
   529 end; (*struct*)