src/Tools/Code/code_scala.ML
author haftmann
Mon Aug 30 16:00:41 2010 +0200 (2010-08-30)
changeset 38910 6af1d8673cbf
parent 38863 9070a7c356c9
child 38912 c79c1e4e1111
permissions -rw-r--r--
width is a formal parameter of serialization
     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, 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 syntax_tyco 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 (syntax_const 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 (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
    80         val (l, print') = case syntax_const 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 syntax_tyco) 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 syntax_const) 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 print_tuple [p] = p
   175               | print_tuple 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                   print_tuple (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, print_tuple (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 local
   285 
   286 (* hierarchical module name space *)
   287 
   288 datatype node =
   289     Dummy
   290   | Stmt of Code_Thingol.stmt
   291   | Module of (string list * (string * node) Graph.T);
   292 
   293 in
   294 
   295 fun scala_program_of_program labelled_name reserved module_alias program =
   296   let
   297 
   298     (* building module name hierarchy *)
   299     fun alias_fragments name = case module_alias name
   300      of SOME name' => Long_Name.explode name'
   301       | NONE => map (fn name => fst (yield_singleton Name.variants name reserved))
   302           (Long_Name.explode name);
   303     val module_names = Graph.fold (insert (op =) o fst o dest_name o fst) program [];
   304     val fragments_tab = fold (fn name => Symtab.update
   305       (name, alias_fragments name)) module_names Symtab.empty;
   306     val dest_name = Code_Printer.dest_name #>> (the o Symtab.lookup fragments_tab);
   307 
   308     (* building empty module hierarchy *)
   309     val empty_module = ([], Graph.empty);
   310     fun map_module f (Module content) = Module (f content);
   311     fun change_module [] = I
   312       | change_module (name_fragment :: name_fragments) =
   313           apsnd o Graph.map_node name_fragment o apsnd o map_module
   314             o change_module name_fragments;
   315     fun ensure_module name_fragment (implicits, nodes) =
   316       if can (Graph.get_node nodes) name_fragment then (implicits, nodes)
   317       else (implicits,
   318         nodes |> Graph.new_node (name_fragment, (name_fragment, Module empty_module)));
   319     fun allocate_module [] = I
   320       | allocate_module (name_fragment :: name_fragments) =
   321           ensure_module name_fragment
   322           #> (apsnd o Graph.map_node name_fragment o apsnd o map_module o allocate_module) name_fragments;
   323     val empty_program = Symtab.fold (fn (_, fragments) => allocate_module fragments)
   324       fragments_tab empty_module;
   325 
   326     (* distribute statements over hierarchy *)
   327     fun add_stmt name stmt =
   328       let
   329         val (name_fragments, base) = dest_name name;
   330         fun is_classinst stmt = case stmt
   331          of Code_Thingol.Classinst _ => true
   332           | _ => false;
   333         val implicit_deps = filter (is_classinst o Graph.get_node program)
   334           (Graph.imm_succs program name);
   335       in
   336         change_module name_fragments (fn (implicits, nodes) =>
   337           (union (op =) implicit_deps implicits, Graph.new_node (name, (base, Stmt stmt)) nodes))
   338       end;
   339     fun add_dependency name name' =
   340       let
   341         val (name_fragments, base) = dest_name name;
   342         val (name_fragments', base') = dest_name name';
   343         val (name_fragments_common, (diff, diff')) =
   344           chop_prefix (op =) (name_fragments, name_fragments');
   345         val dep = if null diff then (name, name') else (hd diff, hd diff')
   346       in (change_module name_fragments_common o apsnd) (Graph.add_edge dep) end;
   347     val proto_program = empty_program
   348       |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
   349       |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
   350 
   351     (* name declarations *)
   352     fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
   353       let
   354         val declare = Name.declare name_fragment;
   355       in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end;
   356     fun namify_class base ((nsp_class, nsp_object), nsp_common) =
   357       let
   358         val (base', nsp_class') = yield_singleton Name.variants base nsp_class
   359       in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
   360     fun namify_object base ((nsp_class, nsp_object), nsp_common) =
   361       let
   362         val (base', nsp_object') = yield_singleton Name.variants base nsp_object
   363       in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
   364     fun namify_common upper base ((nsp_class, nsp_object), nsp_common) =
   365       let
   366         val (base', nsp_common') =
   367           yield_singleton Name.variants (if upper then first_upper base else base) nsp_common
   368       in
   369         (base',
   370           ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
   371       end;
   372     fun namify_stmt (Code_Thingol.Fun _) = namify_object
   373       | namify_stmt (Code_Thingol.Datatype _) = namify_class
   374       | namify_stmt (Code_Thingol.Datatypecons _) = namify_common true
   375       | namify_stmt (Code_Thingol.Class _) = namify_class
   376       | namify_stmt (Code_Thingol.Classrel _) = namify_object
   377       | namify_stmt (Code_Thingol.Classparam _) = namify_object
   378       | namify_stmt (Code_Thingol.Classinst _) = namify_common false;
   379     fun make_declarations nsps (implicits, nodes) =
   380       let
   381         val (module_fragments, stmt_names) = List.partition
   382           (fn name_fragment => case Graph.get_node nodes name_fragment
   383             of (_, Module _) => true | _ => false) (Graph.keys nodes);
   384         fun modify_stmt (Stmt (Code_Thingol.Datatypecons _)) = Dummy
   385           | modify_stmt (Stmt (Code_Thingol.Classrel _)) = Dummy
   386           | modify_stmt (Stmt (Code_Thingol.Classparam _)) = Dummy
   387           | modify_stmt stmt = stmt;
   388         fun declare namify modify name (nsps, nodes) =
   389           let
   390             val (base, node) = Graph.get_node nodes name;
   391             val (base', nsps') = namify node base nsps;
   392             val nodes' = Graph.map_node name (K (base', modify node)) nodes;
   393           in (nsps', nodes') end;
   394         val (nsps', nodes') = (nsps, nodes)
   395           |> fold (declare (K namify_module) I) module_fragments
   396           |> fold (declare (namify_stmt o (fn Stmt stmt => stmt)) modify_stmt) stmt_names;
   397         val nodes'' = nodes'
   398           |> fold (fn name_fragment => (Graph.map_node name_fragment
   399               o apsnd o map_module) (make_declarations nsps')) module_fragments;
   400       in (implicits, nodes'') end;
   401     val (_, sca_program) = make_declarations ((reserved, reserved), reserved) proto_program;
   402 
   403     (* deresolving *)
   404     fun deresolver prefix_fragments name =
   405       let
   406         val (name_fragments, _) = dest_name name;
   407         val (_, (_, remainder)) = chop_prefix (op =) (prefix_fragments, name_fragments);
   408         val nodes = fold (fn name_fragment => fn nodes => case Graph.get_node nodes name_fragment
   409          of (_, Module (_, nodes)) => nodes) name_fragments sca_program;
   410         val (base', _) = Graph.get_node nodes name;
   411       in Long_Name.implode (remainder @ [base']) end
   412         handle Graph.UNDEF _ => error ("Unknown statement name: " ^ labelled_name name);
   413 
   414   in (deresolver, sca_program) end;
   415 
   416 fun serialize_scala labelled_name raw_reserved includes module_alias
   417     _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
   418     program (stmt_names, presentation_stmt_names) width =
   419   let
   420 
   421     (* build program *)
   422     val reserved = fold (insert (op =) o fst) includes raw_reserved;
   423     val (deresolver, sca_program) = scala_program_of_program labelled_name
   424       (Name.make_context reserved) module_alias program;
   425 
   426     (* print statements *)
   427     fun lookup_constr tyco constr = case Graph.get_node program tyco
   428      of Code_Thingol.Datatype (_, (_, constrs)) =>
   429           the (AList.lookup (op = o apsnd fst) constrs constr);
   430     fun classparams_of_class class = case Graph.get_node program class
   431      of Code_Thingol.Class (_, (_, (_, classparams))) => classparams;
   432     fun args_num c = case Graph.get_node program c
   433      of Code_Thingol.Fun (_, (((_, ty), []), _)) =>
   434           (length o fst o Code_Thingol.unfold_fun) ty
   435       | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
   436       | Code_Thingol.Datatypecons (_, tyco) => length (lookup_constr tyco c)
   437       | Code_Thingol.Classparam (_, class) =>
   438           (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =)
   439             (classparams_of_class class)) c;
   440     fun is_singleton_constr c = case Graph.get_node program c
   441      of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
   442       | _ => false;
   443     val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
   444       (make_vars reserved) args_num is_singleton_constr;
   445 
   446     (* print nodes *)
   447     fun print_module base implicit_ps p = Pretty.chunks2
   448       ([str ("object " ^ base ^ " {")]
   449         @ (if null implicit_ps then [] else (single o Pretty.block)
   450             (str "import /*implicits*/" :: Pretty.brk 1 :: commas implicit_ps))
   451         @ [p, str ("} /* object " ^ base ^ " */")]);
   452     fun print_implicit prefix_fragments implicit =
   453       let
   454         val s = deresolver prefix_fragments implicit;
   455       in if length (Long_Name.explode s) = 1 then NONE else SOME (str s) end;
   456     fun print_node _ (_, Dummy) = NONE
   457       | print_node prefix_fragments (name, Stmt stmt) =
   458           if null presentation_stmt_names
   459           orelse member (op =) presentation_stmt_names name
   460           then SOME (print_stmt (deresolver prefix_fragments, deresolver []) (name, stmt))
   461           else NONE
   462       | print_node prefix_fragments (name_fragment, Module (implicits, nodes)) =
   463           if null presentation_stmt_names
   464           then
   465             let
   466               val prefix_fragments' = prefix_fragments @ [name_fragment];
   467             in
   468               Option.map (print_module name_fragment
   469                 (map_filter (print_implicit prefix_fragments') implicits))
   470                   (print_nodes prefix_fragments' nodes)
   471             end
   472           else print_nodes [] nodes
   473     and print_nodes prefix_fragments nodes = let
   474         val ps = map_filter (fn name => print_node prefix_fragments (name,
   475           snd (Graph.get_node nodes name)))
   476             ((rev o flat o Graph.strong_conn) nodes);
   477       in if null ps then NONE else SOME (Pretty.chunks2 ps) end;
   478 
   479     (* serialization *)
   480     val p_includes = if null presentation_stmt_names
   481       then map (fn (base, p) => print_module base [] p) includes else [];
   482     val p = Pretty.chunks2 (p_includes @ the_list (print_nodes [] sca_program));
   483   in
   484     Code_Target.mk_serialization
   485       (fn width => (fn NONE => code_writeln | SOME file => File.write file o code_of_pretty))
   486       (fn width => (rpair [] o code_of_pretty)) p width
   487   end;
   488 
   489 end; (*local*)
   490 
   491 val literals = let
   492   fun char_scala c = if c = "'" then "\\'"
   493     else if c = "\"" then "\\\""
   494     else if c = "\\" then "\\\\"
   495     else let val k = ord c
   496     in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end
   497   fun numeral_scala k = if k < 0
   498     then if k > ~ 2147483647 then "- " ^ string_of_int (~ k)
   499       else quote ("- " ^ string_of_int (~ k))
   500     else if k <= 2147483647 then string_of_int k
   501       else quote (string_of_int k)
   502 in Literals {
   503   literal_char = Library.enclose "'" "'" o char_scala,
   504   literal_string = quote o translate_string char_scala,
   505   literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   506   literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
   507   literal_alternative_numeral = fn k => "Natural.Nat(" ^ numeral_scala k ^ ")",
   508   literal_naive_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
   509   literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
   510   infix_cons = (6, "::")
   511 } end;
   512 
   513 
   514 (** Isar setup **)
   515 
   516 fun isar_serializer _ =
   517   Code_Target.parse_args (Scan.succeed ())
   518   #> (fn () => serialize_scala);
   519 
   520 val setup =
   521   Code_Target.add_target
   522     (target, { serializer = isar_serializer, literals = literals,
   523       check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
   524         make_command = fn scala_home => fn _ =>
   525           "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
   526             ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " ROOT.scala" } })
   527   #> Code_Target.add_syntax_tyco target "fun"
   528      (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
   529         brackify_infix (1, R) fxy (
   530           print_typ BR ty1 (*product type vs. tupled arguments!*),
   531           str "=>",
   532           print_typ (INFX (1, R)) ty2
   533         )))
   534   #> fold (Code_Target.add_reserved target) [
   535       "abstract", "case", "catch", "class", "def", "do", "else", "extends", "false",
   536       "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",
   537       "match", "new", "null", "object", "override", "package", "private", "protected",
   538       "requires", "return", "sealed", "super", "this", "throw", "trait", "try",
   539       "true", "type", "val", "var", "while", "with", "yield"
   540     ]
   541   #> fold (Code_Target.add_reserved target) [
   542       "apply", "error", "BigInt", "Nil", "List"
   543     ];
   544 
   545 end; (*struct*)