1.1 --- a/src/Tools/Code/code_scala.ML Tue Jun 01 13:52:11 2010 +0200
1.2 +++ b/src/Tools/Code/code_scala.ML Tue Jun 01 13:52:11 2010 +0200
1.3 @@ -25,11 +25,12 @@
1.4 fun print_scala_stmt labelled_name syntax_tyco syntax_const reserved args_num is_singleton deresolve =
1.5 let
1.6 val deresolve_base = Long_Name.base_name o deresolve;
1.7 + val lookup_tyvar = first_upper oo lookup_var;
1.8 fun print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
1.9 of NONE => applify "[" "]" fxy
1.10 ((str o deresolve) tyco) (map (print_typ tyvars NOBR) tys)
1.11 | SOME (i, print) => print (print_typ tyvars) fxy tys)
1.12 - | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
1.13 + | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
1.14 fun print_typed tyvars p ty =
1.15 Pretty.block [p, str ":", Pretty.brk 1, print_typ tyvars NOBR ty]
1.16 fun print_var vars NONE = str "_"
1.17 @@ -114,19 +115,20 @@
1.18 fun implicit_arguments tyvars vs vars =
1.19 let
1.20 val implicit_typ_ps = maps (fn (v, sort) => map (fn class => Pretty.block
1.21 - [(str o deresolve) class, str "[", (str o lookup_var tyvars) v, str "]"]) sort) vs;
1.22 - val implicit_names = Name.invents (snd vars) "a" (length implicit_typ_ps);
1.23 + [(str o deresolve) class, str "[", (str o lookup_tyvar tyvars) v, str "]"]) sort) vs;
1.24 + val implicit_names = Name.variant_list [] (maps (fn (v, sort) => map (fn class =>
1.25 + lookup_tyvar tyvars v ^ "_" ^ (Long_Name.base_name o deresolve) class) sort) vs);
1.26 val vars' = intro_vars implicit_names vars;
1.27 val implicit_ps = map2 (fn v => fn p => concat [str (v ^ ":"), p])
1.28 implicit_names implicit_typ_ps;
1.29 in ((implicit_names, implicit_ps), vars') end;
1.30 fun print_defhead tyvars vars p vs params tys implicits ty =
1.31 - concat [str "def", print_typed tyvars (applify "(implicit " ")" NOBR
1.32 + Pretty.block [str "def ", print_typed tyvars (applify "(implicit " ")" NOBR
1.33 (applify "(" ")" NOBR
1.34 - (applify "[" "]" NOBR p (map (str o lookup_var tyvars o fst) vs))
1.35 + (applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs))
1.36 (map2 (fn param => fn ty => print_typed tyvars
1.37 ((str o lookup_var vars) param) ty)
1.38 - params tys)) implicits) ty, str "="]
1.39 + params tys)) implicits) ty, str " ="]
1.40 fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = (case filter (snd o snd) raw_eqs
1.41 of [] =>
1.42 let
1.43 @@ -193,7 +195,7 @@
1.44 val fields = Name.names (snd reserved) "a" tys;
1.45 val vars = intro_vars (map fst fields) reserved;
1.46 fun add_typargs p = applify "[" "]" NOBR p
1.47 - (map (str o lookup_var tyvars o fst) vs);
1.48 + (map (str o lookup_tyvar tyvars o fst) vs);
1.49 in
1.50 concat [
1.51 applify "(" ")" NOBR
1.52 @@ -206,7 +208,7 @@
1.53 in
1.54 Pretty.chunks (
1.55 applify "[" "]" NOBR ((concat o map str) ["sealed", "class", deresolve_base name])
1.56 - (map (str o prefix "+" o lookup_var tyvars o fst) vs)
1.57 + (map (str o prefix "+" o lookup_tyvar tyvars o fst) vs)
1.58 :: map print_co cos
1.59 )
1.60 end
1.61 @@ -214,7 +216,7 @@
1.62 let
1.63 val tyvars = intro_vars [v] reserved;
1.64 val vs = [(v, [name])];
1.65 - fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_var tyvars) v];
1.66 + fun add_typarg p = applify "[" "]" NOBR p [(str o lookup_tyvar tyvars) v];
1.67 fun print_superclasses [] = NONE
1.68 | print_superclasses classes = SOME (concat (str "extends"
1.69 :: separate (str "with") (map (add_typarg o str o deresolve o fst) classes)));
1.70 @@ -255,7 +257,7 @@
1.71 val tyvars = intro_vars (map fst vs) reserved;
1.72 val insttyp = tyco `%% map (ITyVar o fst) vs;
1.73 val p_inst_typ = print_typ tyvars NOBR insttyp;
1.74 - fun add_typ_params p = applify "[" "]" NOBR p (map (str o lookup_var tyvars o fst) vs);
1.75 + fun add_typ_params p = applify "[" "]" NOBR p (map (str o lookup_tyvar tyvars o fst) vs);
1.76 fun add_inst_typ p = Pretty.block [p, str "[", p_inst_typ, str "]"];
1.77 val ((implicit_names, implicit_ps), vars) = implicit_arguments tyvars vs reserved;
1.78 fun print_classparam_inst ((classparam, const as (_, (_, tys))), (thm, _)) =
1.79 @@ -282,10 +284,10 @@
1.80 @ map print_classparam_inst classparam_insts),
1.81 concat [str "implicit", str (if null vs then "val" else "def"),
1.82 applify "(implicit " ")" NOBR (applify "[" "]" NOBR
1.83 - ((str o deresolve_base) name) (map (str o lookup_var tyvars o fst) vs))
1.84 + ((str o deresolve_base) name) (map (str o lookup_tyvar tyvars o fst) vs))
1.85 implicit_ps,
1.86 str "=", str "new", applify "[" "]" NOBR ((str o deresolve_base) name)
1.87 - (map (str o lookup_var tyvars o fst) vs),
1.88 + (map (str o lookup_tyvar tyvars o fst) vs),
1.89 Pretty.enum ";" "{ " " }" (map (str o (fn v => "val arg$" ^ v ^ " = " ^ v) o lookup_var vars)
1.90 implicit_names)]
1.91 ]
1.92 @@ -431,17 +433,17 @@
1.93 val setup =
1.94 Code_Target.add_target (target, (isar_seri_scala, literals))
1.95 #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
1.96 - brackify_infix (1, R) fxy [
1.97 + brackify_infix (1, R) fxy (
1.98 print_typ BR ty1 (*product type vs. tupled arguments!*),
1.99 str "=>",
1.100 print_typ (INFX (1, R)) ty2
1.101 - ]))
1.102 + )))
1.103 #> fold (Code_Target.add_reserved target) [
1.104 "abstract", "case", "catch", "class", "def", "do", "else", "extends", "false",
1.105 "final", "finally", "for", "forSome", "if", "implicit", "import", "lazy",
1.106 "match", "new", "null", "object", "override", "package", "private", "protected",
1.107 "requires", "return", "sealed", "super", "this", "throw", "trait", "try",
1.108 - "true", "type", "val", "var", "while", "with"
1.109 + "true", "type", "val", "var", "while", "with", "yield"
1.110 ]
1.111 #> fold (Code_Target.add_reserved target) [
1.112 "error", "apply", "List", "Nil", "BigInt"