295 end; |
295 end; |
296 val head = print_defhead' tyvars reserved ((str o deresolve) name) vs [] [] classtyp; |
296 val head = print_defhead' tyvars reserved ((str o deresolve) name) vs [] [] classtyp; |
297 val body = [str "new", print_classtyp' classtyp, |
297 val body = [str "new", print_classtyp' classtyp, |
298 Pretty.enum ";" "{ " " }" (map print_classparam_instance (classparam_instances @ further_classparam_instances))]; |
298 Pretty.enum ";" "{ " " }" (map print_classparam_instance (classparam_instances @ further_classparam_instances))]; |
299 in concat (str "implicit" :: head :: body) end; |
299 in concat (str "implicit" :: head :: body) end; |
300 (*let |
|
301 val tyvars = intro_vars (map fst vs) reserved; |
|
302 val insttyp = tyco `%% map (ITyVar o fst) vs; |
|
303 val p_inst_typ = print_typ tyvars NOBR insttyp; |
|
304 fun add_typ_params p = applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs); |
|
305 fun add_inst_typ p = Pretty.block [p, str "[", p_inst_typ, str "]"]; |
|
306 val ((implicit_names, implicit_ps), vars) = implicit_arguments tyvars vs reserved; |
|
307 fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) = |
|
308 let |
|
309 val auxs = Name.invents (snd reserved) "a" (length tys); |
|
310 val vars = intro_vars auxs reserved; |
|
311 val args = if null auxs then [] else |
|
312 [concat [enum "," "(" ")" (map2 (fn aux => fn ty => print_typed tyvars ((str o lookup_var vars) aux) ty) |
|
313 auxs tys), str "=>"]]; |
|
314 in |
|
315 concat ([str "val", (str o Library.enclose "`" "+`" o deresolve_base) classparam, |
|
316 str "="] @ args @ [print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)]) |
|
317 end; |
|
318 in |
|
319 Pretty.chunks [ |
|
320 Pretty.block_enclose |
|
321 (concat ([str "trait", |
|
322 add_typ_params ((str o deresolve_base) name), |
|
323 str "extends", |
|
324 Pretty.block [(str o deresolve) class, str "[", p_inst_typ, str "]"]] |
|
325 @ map (fn (_, (_, (super_instance, _))) => add_typ_params (str ("with " ^ deresolve super_instance))) |
|
326 super_instances @| str "{"), str "}") |
|
327 (map (fn p => Pretty.block [str "implicit val arg$", p]) implicit_ps |
|
328 @ map print_classparam_instance classparam_instances), |
|
329 concat [str "implicit", str (if null vs then "val" else "def"), |
|
330 applify "(implicit " ")" NOBR (applify "[" "]" NOBR |
|
331 ((str o deresolve_base) name) (map (str o lookup_tyvar tyvars o fst) vs)) |
|
332 implicit_ps, |
|
333 str "=", str "new", applify "[" "]" NOBR ((str o deresolve_base) name) |
|
334 (map (str o lookup_tyvar tyvars o fst) vs), |
|
335 Pretty.enum ";" "{ " " }" (map (str o (fn v => "val arg$" ^ v ^ " = " ^ v) o lookup_var vars) |
|
336 implicit_names)] |
|
337 ] |
|
338 end;*) |
|
339 in print_stmt end; |
300 in print_stmt end; |
340 |
301 |
341 fun scala_program_of_program labelled_name module_name reserved raw_module_alias program = |
302 fun scala_program_of_program labelled_name module_name reserved raw_module_alias program = |
342 let |
303 let |
343 val the_module_name = the_default "Program" module_name; |
304 val the_module_name = the_default "Program" module_name; |