1 (* Title: Tools/Code/code_scala.ML
2 Author: Florian Haftmann, TU Muenchen
10 val setup: theory -> theory
13 structure Code_Scala : CODE_SCALA =
18 open Basic_Code_Thingol;
25 (** Scala serializer **)
27 fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
28 args_num is_singleton_constr (deresolve, deresolve_full) =
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) =
58 | print_term tyvars is_pat some_thm vars fxy ((v, ty) `|=> t) =
60 val vars' = intro_vars (the_list v) vars;
63 enclose "(" ")" [constraint (print_var vars' v) (print_typ tyvars NOBR ty)],
65 print_term tyvars false some_thm vars' NOBR t
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)) =
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
94 print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
96 val (ts1, ts23) = chop l ts;
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)
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 ((_, [_]), _)) =
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 =
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 "}")
120 | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
122 fun print_select (pat, body) =
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)
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),
143 fun print_def name (vs, ty) [] =
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;
150 concat [print_defhead tyvars vars name vs params tys ty',
151 str ("error(\"" ^ name ^ "\")")]
153 | print_def name (vs, ty) eqs =
155 val tycos = fold (fn ((ts, t), _) =>
156 fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
157 val tyvars = reserved
159 (is_none o syntax_tyco) deresolve tycos
161 val simple = case eqs
162 of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
164 val consts = fold Code_Thingol.add_constnames
165 (map (snd o fst) eqs) [];
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, _))) =
180 val vars' = intro_vars ((fold o Code_Thingol.fold_varnames)
181 (insert (op =)) ts []) vars1;
184 print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
185 str "=>", print_rhs vars' eq]
187 val head = print_defhead tyvars vars2 name vs params tys' ty';
189 concat [head, print_rhs vars2 (hd eqs)]
192 (concat [head, print_tuple (map (str o lookup_var vars2) params),
193 str "match", str "{"], str "}")
194 (map print_clause eqs)
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))) =
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),
214 applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
215 ((str o deresolve) name) vs
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
222 | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
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) =
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;
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]
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
258 | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
259 (super_instances, (classparam_instances, further_classparam_instances)))) =
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, _)) =
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 "=>"];
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))
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))
286 (* hierarchical module name space *)
290 | Stmt of Code_Thingol.stmt
291 | Module of (string list * (string * node) Graph.T);
295 fun scala_program_of_program labelled_name reserved module_alias program =
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);
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)
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;
326 (* distribute statements over hierarchy *)
327 fun add_stmt name stmt =
329 val (name_fragments, base) = dest_name name;
330 fun is_classinst stmt = case stmt
331 of Code_Thingol.Classinst _ => true
333 val implicit_deps = filter (is_classinst o Graph.get_node program)
334 (Graph.imm_succs program name);
336 change_module name_fragments (fn (implicits, nodes) =>
337 (union (op =) implicit_deps implicits, Graph.new_node (name, (base, Stmt stmt)) nodes))
339 fun add_dependency name name' =
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;
351 (* name declarations *)
352 fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
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) =
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) =
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) =
366 val (base', nsp_common') =
367 yield_singleton Name.variants (if upper then first_upper base else base) nsp_common
370 ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
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) =
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) =
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;
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;
404 fun deresolver prefix_fragments name =
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);
414 in (deresolver, sca_program) end;
416 fun serialize_scala labelled_name raw_reserved includes module_alias
417 _ syntax_tyco syntax_const
418 program (stmt_names, presentation_stmt_names) =
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;
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)
443 val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
444 (make_vars reserved) args_num is_singleton_constr;
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 =
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))
462 | print_node prefix_fragments (name_fragment, Module (implicits, nodes)) =
463 if null presentation_stmt_names
466 val prefix_fragments' = prefix_fragments @ [name_fragment];
468 Option.map (print_module name_fragment
469 (map_filter (print_implicit prefix_fragments') implicits))
470 (print_nodes prefix_fragments' nodes)
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;
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 fun write width NONE = writeln_pretty width
484 | write width (SOME p) = File.write p o string_of_pretty width;
486 Code_Target.serialization write (rpair [] oo string_of_pretty) p
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)
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, "::")
516 fun isar_serializer _ =
517 Code_Target.parse_args (Scan.succeed ())
518 #> (fn () => serialize_scala);
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!*),
532 print_typ (INFX (1, R)) ty2
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"
541 #> fold (Code_Target.add_reserved target) [
542 "apply", "error", "BigInt", "Nil", "List"