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