1 (* Title: Tools/Code/code_scala.ML
2 Author: Florian Haftmann, TU Muenchen
10 val check: theory -> Path.T -> unit
11 val setup: theory -> theory
14 structure Code_Scala : CODE_SCALA =
19 open Basic_Code_Thingol;
26 (** Scala serializer **)
28 fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved
29 args_num is_singleton_constr deresolve =
31 val deresolve_base = Long_Name.base_name o deresolve;
32 fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
33 fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
34 fun print_tyco_expr tyvars fxy (tyco, tys) = applify "[" "]"
35 (print_typ tyvars NOBR) fxy ((str o deresolve) tyco) tys
36 and print_typ tyvars fxy (tyco `%% tys) = (case syntax_tyco tyco
37 of NONE => print_tyco_expr tyvars fxy (tyco, tys)
38 | SOME (i, print) => print (print_typ tyvars) fxy tys)
39 | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
40 fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (class, [ty]);
41 fun print_tupled_typ tyvars ([], ty) =
42 print_typ tyvars NOBR ty
43 | print_tupled_typ tyvars ([ty1], ty2) =
44 concat [print_typ tyvars BR ty1, str "=>", print_typ tyvars NOBR ty2]
45 | print_tupled_typ tyvars (tys, ty) =
46 concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
47 str "=>", print_typ tyvars NOBR ty];
48 fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2];
49 fun print_var vars NONE = str "_"
50 | print_var vars (SOME v) = (str o lookup_var vars) v
51 fun print_term tyvars is_pat some_thm vars fxy (IConst c) =
52 print_app tyvars is_pat some_thm vars fxy (c, [])
53 | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
54 (case Code_Thingol.unfold_const_app t
55 of SOME app => print_app tyvars is_pat some_thm vars fxy app
56 | _ => applify "(" ")" (print_term tyvars is_pat some_thm vars NOBR) fxy
57 (print_term tyvars is_pat some_thm vars BR t1) [t2])
58 | print_term tyvars is_pat some_thm vars fxy (IVar v) =
60 | print_term tyvars is_pat some_thm vars fxy ((v, ty) `|=> t) =
62 val vars' = intro_vars (the_list v) vars;
65 enclose "(" ")" [constraint (print_var vars' v) (print_typ tyvars NOBR ty)],
67 print_term tyvars false some_thm vars' NOBR t
70 | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
71 (case Code_Thingol.unfold_const_app t0
72 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
73 then print_case tyvars some_thm vars fxy cases
74 else print_app tyvars is_pat some_thm vars fxy c_ts
75 | NONE => print_case tyvars some_thm vars fxy cases)
76 and print_app tyvars is_pat some_thm vars fxy
77 (app as ((c, ((arg_typs, _), function_typs)), ts)) =
80 val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
81 val arg_typs' = if is_pat orelse
82 (is_none (syntax_const c) andalso is_singleton_constr c) then [] else arg_typs;
83 val (no_syntax, print') = case syntax_const c
84 of NONE => (true, fn ts => applify "(" ")"
85 (print_term tyvars is_pat some_thm vars NOBR) fxy
86 (applify "[" "]" (print_typ tyvars NOBR)
87 NOBR ((str o deresolve) c) arg_typs') ts)
88 | SOME (_, print) => (false, fn ts =>
89 print (print_term tyvars is_pat some_thm) some_thm vars fxy
90 (ts ~~ take l function_typs));
91 in if k = l then print' ts
93 print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
95 val (ts1, ts23) = chop l ts;
97 Pretty.block (print' ts1 :: map (fn t => Pretty.block
98 [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23)
100 and print_bind tyvars some_thm fxy p =
101 gen_print_bind (print_term tyvars true) some_thm fxy p
102 and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
104 val (binds, body) = Code_Thingol.unfold_let (ICase cases);
105 fun print_match ((pat, ty), t) vars =
107 |> print_bind tyvars some_thm BR pat
108 |>> (fn p => concat [str "val", constraint p (print_typ tyvars NOBR ty),
109 str "=", print_term tyvars false some_thm vars NOBR t])
110 val (all_ps, vars') = fold_map print_match binds vars;
111 val (ps, p) = split_last all_ps;
112 in brackify_block fxy
114 (ps @ Pretty.block [p, str ";"] @@ print_term tyvars false some_thm vars' NOBR body)
117 | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
119 fun print_select (pat, body) =
121 val (p_pat, vars') = print_bind tyvars some_thm NOBR pat vars;
122 val p_body = print_term tyvars false some_thm vars' NOBR body
123 in concat [str "case", p_pat, str "=>", p_body] end;
124 in brackify_block fxy
125 (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"])
126 (map print_select clauses)
129 | print_case tyvars some_thm vars fxy ((_, []), _) =
130 (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
131 fun print_context tyvars vs name = applify "[" "]"
132 (fn (v, sort) => (Pretty.block o map str)
133 (lookup_tyvar tyvars v :: maps (fn sort => [": ", deresolve sort]) sort))
134 NOBR ((str o deresolve) name) vs;
135 fun print_defhead tyvars vars name vs params tys ty =
136 Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
137 constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
138 NOBR (print_context tyvars vs name) (params ~~ tys)) (print_typ tyvars NOBR ty),
140 fun print_def name (vs, ty) [] =
142 val (tys, ty') = Code_Thingol.unfold_fun ty;
143 val params = Name.invents (snd reserved) "a" (length tys);
144 val tyvars = intro_tyvars vs reserved;
145 val vars = intro_vars params reserved;
147 concat [print_defhead tyvars vars name vs params tys ty',
148 str ("error(\"" ^ name ^ "\")")]
150 | print_def name (vs, ty) eqs =
152 val tycos = fold (fn ((ts, t), _) =>
153 fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
154 val tyvars = reserved
156 (is_none o syntax_tyco) deresolve tycos
158 val simple = case eqs
159 of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
161 val consts = fold Code_Thingol.add_constnames
162 (map (snd o fst) eqs) [];
165 (is_none o syntax_const) deresolve consts
166 val params = if simple
167 then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
168 else aux_params vars1 (map (fst o fst) eqs);
169 val vars2 = intro_vars params vars1;
170 val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty;
171 fun print_tuple [p] = p
172 | print_tuple ps = enum "," "(" ")" ps;
173 fun print_rhs vars' ((_, t), (some_thm, _)) =
174 print_term tyvars false some_thm vars' NOBR t;
175 fun print_clause (eq as ((ts, _), (some_thm, _))) =
177 val vars' = intro_vars ((fold o Code_Thingol.fold_varnames)
178 (insert (op =)) ts []) vars1;
181 print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
182 str "=>", print_rhs vars' eq]
184 val head = print_defhead tyvars vars2 name vs params tys' ty';
186 concat [head, print_rhs vars2 (hd eqs)]
189 (concat [head, print_tuple (map (str o lookup_var vars2) params),
190 str "match", str "{"], str "}")
191 (map print_clause eqs)
193 val print_method = (str o Library.enclose "`" "+`" o deresolve_base);
194 fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
195 print_def name (vs, ty) (filter (snd o snd) raw_eqs)
196 | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
198 val tyvars = intro_tyvars vs reserved;
199 fun print_co ((co, _), []) =
200 concat [str "final", str "case", str "object", (str o deresolve_base) co,
201 str "extends", applify "[" "]" I NOBR ((str o deresolve_base) name)
202 (replicate (length vs) (str "Nothing"))]
203 | print_co ((co, vs_args), tys) =
204 concat [applify "(" ")"
205 (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) NOBR
206 (applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((concat o map str)
207 ["final", "case", "class", deresolve_base co]) vs_args)
208 (Name.names (snd reserved) "a" tys),
210 applify "[" "]" (str o lookup_tyvar tyvars o fst) NOBR
211 ((str o deresolve_base) name) vs
214 Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars o fst)
215 NOBR ((concat o map str) ["sealed", "class", deresolve_base name]) vs
218 | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
220 val tyvars = intro_tyvars [(v, [name])] reserved;
221 fun add_typarg s = Pretty.block
222 [str s, str "[", (str o lookup_tyvar tyvars) v, str "]"];
223 fun print_super_classes [] = NONE
224 | print_super_classes classes = SOME (concat (str "extends"
225 :: separate (str "with") (map (add_typarg o deresolve o fst) classes)));
226 fun print_classparam_val (classparam, ty) =
227 concat [str "val", constraint (print_method classparam)
228 ((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)];
229 fun print_classparam_def (classparam, ty) =
231 val (tys, ty) = Code_Thingol.unfold_fun ty;
232 val [implicit_name] = Name.invents (snd reserved) (lookup_tyvar tyvars v) 1;
233 val proto_vars = intro_vars [implicit_name] reserved;
234 val auxs = Name.invents (snd proto_vars) "a" (length tys);
235 val vars = intro_vars auxs proto_vars;
237 concat [str "def", constraint (Pretty.block [applify "(" ")"
238 (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
239 (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve classparam))
240 (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
241 add_typarg (deresolve name), str ")"]) (print_typ tyvars NOBR ty), str "=",
242 applify "(" ")" (str o lookup_var vars) NOBR
243 (Pretty.block [str implicit_name, str ".", print_method classparam]) auxs]
247 (Pretty.block_enclose
248 (concat ([str "trait", (add_typarg o deresolve_base) name]
249 @ the_list (print_super_classes super_classes) @ [str "{"]), str "}")
250 (map print_classparam_val classparams))
251 :: map print_classparam_def classparams
254 | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
255 (super_instances, (classparam_instances, further_classparam_instances)))) =
257 val tyvars = intro_tyvars vs reserved;
258 val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
259 fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
261 val aux_tys = Name.names (snd reserved) "a" tys;
262 val auxs = map fst aux_tys;
263 val vars = intro_vars auxs reserved;
264 val aux_abstr = if null auxs then [] else [enum "," "(" ")"
265 (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
266 (print_typ tyvars NOBR ty)) aux_tys), str "=>"];
268 concat ([str "val", print_method classparam, str "="]
269 @ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR
270 (const, map (IVar o SOME) auxs))
273 Pretty.block_enclose (concat [str "implicit def",
274 constraint (print_context tyvars vs name) (print_dicttyp tyvars classtyp),
275 str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
276 (map print_classparam_instance (classparam_instances @ further_classparam_instances))
280 fun scala_program_of_program labelled_name module_name reserved raw_module_alias program =
282 val the_module_name = the_default "Program" module_name;
283 val module_alias = K (SOME the_module_name);
284 val reserved = Name.make_context reserved;
285 fun prepare_stmt (name, stmt) (nsps, stmts) =
287 val (_, base) = Code_Printer.dest_name name;
288 val mk_name_stmt = yield_singleton Name.variants;
289 fun add_class ((nsp_class, nsp_object), nsp_common) =
291 val (base', nsp_class') = mk_name_stmt base nsp_class
292 in (base', ((nsp_class', nsp_object), Name.declare base' nsp_common)) end;
293 fun add_object ((nsp_class, nsp_object), nsp_common) =
295 val (base', nsp_object') = mk_name_stmt base nsp_object
296 in (base', ((nsp_class, nsp_object'), Name.declare base' nsp_common)) end;
297 fun add_common upper ((nsp_class, nsp_object), nsp_common) =
299 val (base', nsp_common') =
300 mk_name_stmt (if upper then first_upper base else base) nsp_common
303 ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
305 val add_name = case stmt
306 of Code_Thingol.Fun _ => add_object
307 | Code_Thingol.Datatype _ => add_class
308 | Code_Thingol.Datatypecons _ => add_common true
309 | Code_Thingol.Class _ => add_class
310 | Code_Thingol.Classrel _ => add_object
311 | Code_Thingol.Classparam _ => add_object
312 | Code_Thingol.Classinst _ => add_common false;
313 fun add_stmt base' = case stmt
314 of Code_Thingol.Datatypecons _ => cons (name, (base', NONE))
315 | Code_Thingol.Classrel _ => cons (name, (base', NONE))
316 | Code_Thingol.Classparam _ => cons (name, (base', NONE))
317 | _ => cons (name, (base', SOME stmt));
321 |-> (fn base' => rpair (add_stmt base' stmts))
323 val stmts = AList.make (Graph.get_node program) (Graph.strong_conn program |> flat)
324 |> filter_out (Code_Thingol.is_case o snd);
325 val (_, sca_program) = fold prepare_stmt stmts (((reserved, reserved), reserved), []);
326 fun deresolver name = (fst o the o AList.lookup (op =) sca_program) name
327 handle Option => error ("Unknown statement name: " ^ labelled_name name);
328 in (deresolver, (the_module_name, sca_program)) end;
330 fun serialize_scala raw_module_name labelled_name
331 raw_reserved includes raw_module_alias
332 _ syntax_tyco syntax_const (code_of_pretty, code_writeln)
333 program stmt_names destination =
335 val presentation_stmt_names = Code_Target.stmt_names_of_destination destination;
336 val module_name = if null presentation_stmt_names then raw_module_name else SOME "Code";
337 val reserved = fold (insert (op =) o fst) includes raw_reserved;
338 val (deresolver, (the_module_name, sca_program)) = scala_program_of_program labelled_name
339 module_name reserved raw_module_alias program;
340 val reserved = make_vars reserved;
341 fun lookup_constr tyco constr = case Graph.get_node program tyco
342 of Code_Thingol.Datatype (_, (_, constrs)) =>
343 the (AList.lookup (op = o apsnd fst) constrs constr);
344 fun classparams_of_class class = case Graph.get_node program class
345 of Code_Thingol.Class (_, (_, (_, classparams))) => classparams;
346 fun args_num c = case Graph.get_node program c
347 of Code_Thingol.Fun (_, (((_, ty), []), _)) =>
348 (length o fst o Code_Thingol.unfold_fun) ty
349 | Code_Thingol.Fun (_, ((_, ((ts, _), _) :: _), _)) => length ts
350 | Code_Thingol.Datatypecons (_, tyco) => length (lookup_constr tyco c)
351 | Code_Thingol.Classparam (_, class) =>
352 (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =)
353 (classparams_of_class class)) c;
354 fun is_singleton_constr c = case Graph.get_node program c
355 of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
357 val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
358 reserved args_num is_singleton_constr deresolver;
359 fun print_module name content =
360 (name, Pretty.chunks [
361 str ("object " ^ name ^ " {"),
367 fun serialize_module the_module_name sca_program =
369 val content = Pretty.chunks2 (map_filter
370 (fn (name, (_, SOME stmt)) => SOME (print_stmt (name, stmt))
371 | (_, (_, NONE)) => NONE) sca_program);
372 in print_module the_module_name content end;
373 fun check_destination destination =
374 (File.check destination; destination);
375 fun write_module destination (modlname, content) =
377 val filename = case modlname
378 of "" => Path.explode "Main.scala"
379 | _ => (Path.ext "scala" o Path.explode o implode o separate "/"
380 o Long_Name.explode) modlname;
381 val pathname = Path.append destination filename;
382 val _ = File.mkdir_leaf (Path.dir pathname);
383 in File.write pathname (code_of_pretty content) end
385 Code_Target.mk_serialization target
386 (fn NONE => K () o map (code_writeln o snd) | SOME file => K () o map
387 (write_module (check_destination file)))
388 (rpair [] o cat_lines o map (code_of_pretty o snd))
389 (map (uncurry print_module) includes
390 @| serialize_module the_module_name sca_program)
395 fun char_scala c = if c = "'" then "\\'"
396 else if c = "\"" then "\\\""
397 else if c = "\\" then "\\\\"
398 else let val k = ord c
399 in if k < 32 orelse k > 126 then "\\" ^ radixstring (8, "0", k) else c end
400 fun numeral_scala k = if k < 0
401 then if k <= 2147483647 then "- " ^ string_of_int (~ k)
402 else quote ("- " ^ string_of_int (~ k))
403 else if k <= 2147483647 then string_of_int k
404 else quote (string_of_int k)
406 literal_char = Library.enclose "'" "'" o char_scala,
407 literal_string = quote o translate_string char_scala,
408 literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
409 literal_positive_numeral = fn k => "Nat.Nat(" ^ numeral_scala k ^ ")",
410 literal_naive_numeral = fn k => if k >= 0
411 then string_of_int k else "(- " ^ string_of_int (~ k) ^ ")",
412 literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
413 infix_cons = (6, "::")
417 (** formal checking of compiled code **)
419 fun check thy = Code_Target.external_check thy target
420 "SCALA_HOME" I (fn scala_home => fn p => fn _ =>
421 Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala");
427 fun isar_seri_scala module_name =
428 Code_Target.parse_args (Scan.succeed ())
429 #> (fn () => serialize_scala module_name);
432 Code_Target.add_target (target, (isar_seri_scala, literals))
433 #> Code_Target.add_syntax_tyco target "fun"
434 (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
435 brackify_infix (1, R) fxy (
436 print_typ BR ty1 (*product type vs. tupled arguments!*),
438 print_typ (INFX (1, R)) ty2
440 #> fold (Code_Target.add_reserved target) [
441 "abstract", "case", "catch", "class", "def", "do", "else", "extends", "false",
442 "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",
443 "match", "new", "null", "object", "override", "package", "private", "protected",
444 "requires", "return", "sealed", "super", "this", "throw", "trait", "try",
445 "true", "type", "val", "var", "while", "with", "yield"
447 #> fold (Code_Target.add_reserved target) [
448 "apply", "error", "BigInt", "Nil", "List"