--- a/src/Tools/Code/code_scala.ML Sun Mar 30 13:50:06 2025 +0200
+++ b/src/Tools/Code/code_scala.ML Sun Mar 30 13:50:06 2025 +0200
@@ -57,29 +57,29 @@
fun lookup_tyvar tyvars = lookup_var tyvars o Name.enforce_case true;
fun intro_tyvars vs = intro_vars (map (Name.enforce_case true o fst) vs);
fun print_tyco_expr tyvars fxy (sym, tys) = applify "[" "]"
- (print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys
+ (print_typ tyvars NOBR) fxy ((Pretty.str o deresolve) sym) tys
and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
of NONE => print_tyco_expr tyvars fxy (Type_Constructor tyco, tys)
| SOME (_, print) => print (print_typ tyvars) fxy tys)
- | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
+ | print_typ tyvars fxy (ITyVar v) = (Pretty.str o lookup_tyvar tyvars) v;
fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Type_Class class, [ty]);
fun print_tupled_typ tyvars ([], ty) =
print_typ tyvars NOBR ty
| print_tupled_typ tyvars ([ty1], ty2) =
- concat [print_typ tyvars BR ty1, str "=>", print_typ tyvars NOBR ty2]
+ concat [print_typ tyvars BR ty1, Pretty.str "=>", print_typ tyvars NOBR ty2]
| print_tupled_typ tyvars (tys, ty) =
- concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
- str "=>", print_typ tyvars NOBR ty];
- fun constraint p1 p2 = Pretty.block [p1, str " : ", p2];
- fun print_var vars NONE = str "_"
- | print_var vars (SOME v) = (str o lookup_var vars) v;
+ concat [Pretty.enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
+ Pretty.str "=>", print_typ tyvars NOBR ty];
+ fun constraint p1 p2 = Pretty.block [p1, Pretty.str " : ", p2];
+ fun print_var vars NONE = Pretty.str "_"
+ | print_var vars (SOME v) = (Pretty.str o lookup_var vars) v;
fun applify_dict tyvars (Dict (_, d)) = applify_plain_dict tyvars d
and applify_plain_dict tyvars (Dict_Const (inst, dss)) =
- applify_dictss tyvars ((str o deresolve o Class_Instance) inst) (map snd dss)
+ applify_dictss tyvars ((Pretty.str o deresolve o Class_Instance) inst) (map snd dss)
| applify_plain_dict tyvars (Dict_Var { var, class, ... }) =
- Pretty.block [str "implicitly",
- enclose "[" "]" [Pretty.block [(str o deresolve_class) class,
- enclose "[" "]" [(str o lookup_tyvar tyvars) var]]]]
+ Pretty.block [Pretty.str "implicitly",
+ Pretty.enclose "[" "]" [Pretty.block [(Pretty.str o deresolve_class) class,
+ Pretty.enclose "[" "]" [(Pretty.str o lookup_tyvar tyvars) var]]]]
and applify_dictss tyvars p dss =
applify "(" ")" (applify_dict tyvars) NOBR p (flat dss)
fun print_term tyvars is_pat some_thm vars fxy (IConst const) =
@@ -110,8 +110,8 @@
val vars' = intro_vars (the_list some_v) vars;
in
(concat [
- enclose "(" ")" [constraint (print_var vars' some_v) (print_typ tyvars NOBR ty)],
- str "=>"
+ Pretty.enclose "(" ")" [constraint (print_var vars' some_v) (print_typ tyvars NOBR ty)],
+ Pretty.str "=>"
], vars')
end
and print_app tyvars is_pat some_thm vars fxy
@@ -131,12 +131,12 @@
(gen_applify (is_constr sym) "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
(applify "[" "]" (print_typ tyvars NOBR)
- NOBR ((str o deresolve) sym) typargs') ts) dicts)
+ NOBR ((Pretty.str o deresolve) sym) typargs') ts) dicts)
| SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify_dicts
(applify "(" ")"
(print_term tyvars is_pat some_thm vars NOBR) fxy
(applify "[" "]" (print_typ tyvars NOBR)
- NOBR (str s) typargs') ts) dicts)
+ NOBR (Pretty.str s) typargs') ts) dicts)
| SOME (k, Complex_printer print) =>
(k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
(ts ~~ take k dom))
@@ -148,21 +148,21 @@
print' fxy ts
else
Pretty.block (print' BR ts1 :: map (fn t => Pretty.block
- [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts2)
+ [Pretty.str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, Pretty.str ")"]) ts2)
else
print_term tyvars is_pat some_thm vars fxy (vs_tys `|==> (IConst const `$$ ts1, rty))
end
and print_bind tyvars some_thm fxy p =
gen_print_bind (print_term tyvars true) some_thm fxy p
and print_case tyvars some_thm vars fxy { clauses = [], ... } =
- (brackify fxy o Pretty.breaks o map str) ["sys.error(\"empty case\")"]
+ (brackify fxy o Pretty.breaks o map Pretty.str) ["sys.error(\"empty case\")"]
| print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
let
val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr);
fun print_match_val ((pat, ty), t) vars =
vars
|> print_bind tyvars some_thm BR pat
- |>> (fn p => (false, concat [str "val", p, str "=",
+ |>> (fn p => (false, concat [Pretty.str "val", p, Pretty.str "=",
constraint (print_term tyvars false some_thm vars NOBR t) (print_typ tyvars BR ty)]));
fun print_match_seq t vars =
((true, print_term tyvars false some_thm vars NOBR t), vars);
@@ -177,30 +177,30 @@
val all_seps_ps = seps_ps @ [(true, print_term tyvars false some_thm vars' NOBR body)];
fun insert_seps [(_, p)] = [p]
| insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) =
- (if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps
- in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}") end
+ (if sep then Pretty.block [p, Pretty.str ";"] else p) :: insert_seps seps_ps
+ in brackify_block fxy (Pretty.str "{") (insert_seps all_seps_ps) (Pretty.str "}") end
| print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
let
fun print_select (pat, body) =
let
val (p_pat, vars') = print_bind tyvars some_thm NOBR pat vars;
val p_body = print_term tyvars false some_thm vars' NOBR body
- in concat [str "case", p_pat, str "=>", p_body] end;
+ in concat [Pretty.str "case", p_pat, Pretty.str "=>", p_body] end;
in
map print_select clauses
- |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match {"], str "}")
+ |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, Pretty.str "match {"], Pretty.str "}")
|> single
- |> enclose "(" ")"
+ |> Pretty.enclose "(" ")"
end;
fun print_context tyvars vs s = applify "[" "]"
- (fn (v, sort) => (Pretty.block o map str)
+ (fn (v, sort) => (Pretty.block o map Pretty.str)
(lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort))
- NOBR (str s) vs;
+ NOBR (Pretty.str s) vs;
fun print_defhead tyvars vars const vs params tys ty =
- concat [str "def", constraint (applify "(" ")" (fn (param, ty) =>
- constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
+ concat [Pretty.str "def", constraint (applify "(" ")" (fn (param, ty) =>
+ constraint ((Pretty.str o lookup_var vars) param) (print_typ tyvars NOBR ty))
NOBR (print_context tyvars vs (deresolve_const const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
- str "="];
+ Pretty.str "="];
fun print_def const (vs, ty) [] =
let
val (tys, ty') = Code_Thingol.unfold_fun ty;
@@ -209,7 +209,7 @@
val vars = intro_vars params reserved;
in
concat [print_defhead tyvars vars const vs params tys ty',
- str ("sys.error(" ^ print_scala_string const ^ ")")]
+ Pretty.str ("sys.error(" ^ print_scala_string const ^ ")")]
end
| print_def const (vs, ty) eqs =
let
@@ -231,7 +231,7 @@
val vars2 = intro_vars params vars1;
val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty;
fun tuplify [p] = p
- | tuplify ps = enum "," "(" ")" ps;
+ | tuplify ps = Pretty.enum "," "(" ")" ps;
fun print_rhs vars' ((_, t), (some_thm, _)) =
print_term tyvars false some_thm vars' NOBR t;
fun print_clause (eq as ((ts, _), (some_thm, _))) =
@@ -239,20 +239,20 @@
val vars' =
intro_vars (build (fold Code_Thingol.add_varnames ts)) vars1;
in
- concat [str "case",
+ concat [Pretty.str "case",
tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
- str "=>", print_rhs vars' eq]
+ Pretty.str "=>", print_rhs vars' eq]
end;
val head = print_defhead tyvars vars2 const vs params tys' ty';
in if simple then
concat [head, print_rhs vars2 (hd eqs)]
else
Pretty.block_enclose
- (concat [head, tuplify (map (str o lookup_var vars2) params),
- str "match {"], str "}")
+ (concat [head, tuplify (map (Pretty.str o lookup_var vars2) params),
+ Pretty.str "match {"], Pretty.str "}")
(map print_clause eqs)
end;
- val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant;
+ val print_method = Pretty.str o enclose "`" "`" o deresolve_full o Constant;
fun print_inst class (tyco, { vs, inst_params, superinst_params }) =
let
val tyvars = intro_tyvars vs reserved;
@@ -264,22 +264,22 @@
val vars = intro_vars auxs reserved;
val (aux_dom1, aux_dom2) = chop dom_length aux_dom;
fun abstract_using [] = []
- | abstract_using aux_dom = [enum "," "(" ")"
- (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
- (print_typ tyvars NOBR ty)) aux_dom), str "=>"];
+ | abstract_using aux_dom = [Pretty.enum "," "(" ")"
+ (map (fn (aux, ty) => constraint ((Pretty.str o lookup_var vars) aux)
+ (print_typ tyvars NOBR ty)) aux_dom), Pretty.str "=>"];
val aux_abstr1 = abstract_using aux_dom1;
val aux_abstr2 = abstract_using aux_dom2;
in
- concat ([str "val", print_method classparam, str "="]
+ concat ([Pretty.str "val", print_method classparam, Pretty.str "="]
@ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR
(const, map (IVar o SOME) auxs))
end;
in
- Pretty.block_enclose (concat [str "implicit def",
+ Pretty.block_enclose (concat [Pretty.str "implicit def",
constraint (print_context tyvars vs
((Library.enclose "`" "`" o deresolve_full o Class_Instance) (tyco, class)))
(print_dicttyp tyvars classtyp),
- str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
+ Pretty.str "=", Pretty.str "new", print_dicttyp tyvars classtyp, Pretty.str "{"], Pretty.str "}")
(map print_classparam_instance (inst_params @ superinst_params))
end;
fun print_stmt (Constant const, (_, Fun ((vs, ty), raw_eqs))) =
@@ -288,29 +288,29 @@
let
val tyvars = intro_tyvars (map (rpair []) vs) reserved;
fun print_co ((co, vs_args), tys) =
- concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR
- (str ("final case class " ^ deresolve_const co)) vs_args)
- @@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg))
+ concat [Pretty.block ((applify "[" "]" (Pretty.str o lookup_tyvar tyvars) NOBR
+ (Pretty.str ("final case class " ^ deresolve_const co)) vs_args)
+ @@ Pretty.enum "," "(" ")" (map (fn (v, arg) => constraint (Pretty.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_tyco) tyco) vs
+ Pretty.str "extends",
+ applify "[" "]" (Pretty.str o lookup_tyvar tyvars) NOBR
+ ((Pretty.str o deresolve_tyco) tyco) vs
];
in
- Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
- NOBR (str ("abstract sealed class " ^ deresolve_tyco tyco)) vs
+ Pretty.chunks (applify "[" "]" (Pretty.str o lookup_tyvar tyvars)
+ NOBR (Pretty.str ("abstract sealed class " ^ deresolve_tyco tyco)) vs
:: map print_co cos)
end
| print_stmt (Type_Class class, (_, Class ((v, (classrels, classparams)), insts))) =
let
val tyvars = intro_tyvars [(v, [class])] reserved;
fun add_typarg s = Pretty.block
- [str s, str "[", (str o lookup_tyvar tyvars) v, str "]"];
+ [Pretty.str s, Pretty.str "[", (Pretty.str o lookup_tyvar tyvars) v, Pretty.str "]"];
fun print_super_classes [] = NONE
- | print_super_classes classrels = SOME (concat (str "extends"
- :: separate (str "with") (map (add_typarg o deresolve_class o snd) classrels)));
+ | print_super_classes classrels = SOME (concat (Pretty.str "extends"
+ :: separate (Pretty.str "with") (map (add_typarg o deresolve_class o snd) classrels)));
fun print_classparam_val (classparam, ty) =
- concat [str "val", constraint (print_method classparam)
+ concat [Pretty.str "val", constraint (print_method classparam)
((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)];
fun print_classparam_def (classparam, ty) =
let
@@ -320,23 +320,23 @@
val auxs = Name.invent (snd proto_vars) "a" (length tys);
val vars = intro_vars auxs proto_vars;
in
- concat [str "def", constraint (Pretty.block [applify "(" ")"
- (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
+ concat [Pretty.str "def", constraint (Pretty.block [applify "(" ")"
+ (fn (aux, ty) => constraint ((Pretty.str o lookup_var vars) aux)
(print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam))
- (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
- add_typarg (deresolve_class class), str ")"]) (print_typ tyvars NOBR ty), str "=",
- applify "(" ")" (str o lookup_var vars) NOBR
- (Pretty.block [str implicit_name, str ".", print_method classparam]) auxs]
+ (auxs ~~ tys), Pretty.str "(implicit ", Pretty.str implicit_name, Pretty.str ": ",
+ add_typarg (deresolve_class class), Pretty.str ")"]) (print_typ tyvars NOBR ty), Pretty.str "=",
+ applify "(" ")" (Pretty.str o lookup_var vars) NOBR
+ (Pretty.block [Pretty.str implicit_name, Pretty.str ".", print_method classparam]) auxs]
end;
in
Pretty.chunks (
(Pretty.block_enclose
- (concat ([str "trait", (add_typarg o deresolve_class) class]
- @ the_list (print_super_classes classrels) @ [str "{"]), str "}")
+ (concat ([Pretty.str "trait", (add_typarg o deresolve_class) class]
+ @ the_list (print_super_classes classrels) @ [Pretty.str "{"]), Pretty.str "}")
(map print_classparam_val classparams))
:: map print_classparam_def classparams
@| Pretty.block_enclose
- (str ("object " ^ deresolve_class class ^ " {"), str "}")
+ (Pretty.str ("object " ^ deresolve_class class ^ " {"), Pretty.str "}")
(map (print_inst class) insts)
)
end;
@@ -432,8 +432,8 @@
(* print modules *)
fun print_module _ base _ ps = Pretty.chunks2
- (str ("object " ^ base ^ " {")
- :: ps @| str ("} /* object " ^ base ^ " */"));
+ (Pretty.str ("object " ^ base ^ " {")
+ :: ps @| Pretty.str ("} /* object " ^ base ^ " */"));
(* serialization *)
val p = Pretty.chunks2 (map snd includes
@@ -456,7 +456,7 @@
in Literals {
literal_string = print_scala_string,
literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
- literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
+ literal_list = fn [] => Pretty.str "Nil" | ps => Pretty.block [Pretty.str "List", Pretty.enum "," "(" ")" ps],
infix_cons = (6, "::")
} end;
@@ -475,7 +475,7 @@
[(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ BR ty1 (*product type vs. tupled arguments!*),
- str "=>",
+ Pretty.str "=>",
print_typ (INFX (1, R)) ty2
)))]))
#> fold (Code_Target.add_reserved target) [