--- a/src/Tools/Code/code_printer.ML Thu Dec 27 21:01:08 2012 +0100
+++ b/src/Tools/Code/code_printer.ML Thu Dec 27 21:01:08 2012 +0100
@@ -67,6 +67,7 @@
val brackify: fixity -> Pretty.T list -> Pretty.T
val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
+ val gen_applify: bool -> string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
@@ -270,11 +271,16 @@
else p
end;
-fun applify opn cls f fxy_ctxt p [] = p
- | applify opn cls f fxy_ctxt p ps =
+fun gen_applify strict opn cls f fxy_ctxt p [] =
+ if strict
+ then (if fixity BR fxy_ctxt then enclose "(" ")" else Pretty.block) [p, str "()"]
+ else p
+ | gen_applify strict opn cls f fxy_ctxt p ps =
(if fixity BR fxy_ctxt then enclose "(" ")" else Pretty.block)
(p @@ enum "," opn cls (map f ps));
+fun applify opn = gen_applify false opn;
+
fun tuplify _ _ [] = NONE
| tuplify print fxy [x] = SOME (print fxy x)
| tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
--- a/src/Tools/Code/code_scala.ML Thu Dec 27 21:01:08 2012 +0100
+++ b/src/Tools/Code/code_scala.ML Thu Dec 27 21:01:08 2012 +0100
@@ -25,7 +25,7 @@
(** Scala serializer **)
fun print_scala_stmt tyco_syntax const_syntax reserved
- args_num is_singleton_constr (deresolve, deresolve_full) =
+ args_num is_constr (deresolve, deresolve_full) =
let
fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
@@ -75,10 +75,9 @@
(app as ({ name = c, typargs, dom, ... }, ts)) =
let
val k = length ts;
- val typargs' = if is_pat orelse
- (is_none (const_syntax c) andalso is_singleton_constr c) then [] else typargs;
+ val typargs' = if is_pat then [] else typargs;
val (l, print') = case const_syntax c
- of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
+ of NONE => (args_num c, fn fxy => fn ts => gen_applify (is_constr c ) "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
(applify "[" "]" (print_typ tyvars NOBR)
NOBR ((str o deresolve) c) typargs') ts)
@@ -206,22 +205,17 @@
| print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
let
val tyvars = intro_tyvars (map (rpair []) vs) reserved;
- fun print_co ((co, _), []) =
- concat [str "final", str "case", str "object", (str o deresolve) co,
- str "extends", applify "[" "]" I NOBR ((str o deresolve) name)
- (replicate (length vs) (str "Nothing"))]
- | print_co ((co, vs_args), tys) =
- concat [applify "(" ")"
- (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) NOBR
- (applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((concat o map str)
- ["final", "case", "class", deresolve co]) vs_args)
- (Name.invent_names (snd reserved) "a" tys),
- str "extends",
- applify "[" "]" (str o lookup_tyvar tyvars) NOBR
- ((str o deresolve) name) vs
- ];
+ fun print_co ((co, vs_args), tys) =
+ concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR
+ ((concat o map str) ["final", "case", "class", deresolve co]) vs_args)
+ @@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg))
+ (Name.invent_names (snd reserved) "a" tys))),
+ str "extends",
+ applify "[" "]" (str o lookup_tyvar tyvars) NOBR
+ ((str o deresolve) name) vs
+ ];
in
- Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars)
+ Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve name]) vs
:: map print_co cos)
end
@@ -359,12 +353,9 @@
| Code_Thingol.Classparam (_, class) =>
(length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =)
(classparams_of_class class)) c;
- fun is_singleton_constr c = case Graph.get_node program c
- of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
- | _ => false;
fun print_stmt prefix_fragments = print_scala_stmt
tyco_syntax const_syntax (make_vars reserved_syms) args_num
- is_singleton_constr (deresolver prefix_fragments, deresolver []);
+ (Code_Thingol.is_constr program) (deresolver prefix_fragments, deresolver []);
(* print modules *)
fun print_implicit prefix_fragments implicit =