--- a/src/HOL/List.thy Sun Mar 30 13:50:06 2025 +0200
+++ b/src/HOL/List.thy Sun Mar 30 13:50:06 2025 +0200
@@ -8156,7 +8156,7 @@
fun print_list (target_fxy, target_cons) pr fxy t1 t2 =
Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
- Code_Printer.str target_cons,
+ Pretty.str target_cons,
pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
);
--- a/src/HOL/Tools/literal.ML Sun Mar 30 13:50:06 2025 +0200
+++ b/src/HOL/Tools/literal.ML Sun Mar 30 13:50:06 2025 +0200
@@ -103,7 +103,7 @@
let
fun pretty literals _ thm _ _ [(b0, _), (b1, _), (b2, _), (b3, _), (b4, _), (b5, _), (b6, _), (t, _)] =
case implode_literal b0 b1 b2 b3 b4 b5 b6 t of
- SOME s => (Code_Printer.str o Code_Printer.literal_string literals) s
+ SOME s => (Pretty.str o Code_Printer.literal_string literals) s
| NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression";
in
thy
--- a/src/HOL/Tools/numeral.ML Sun Mar 30 13:50:06 2025 +0200
+++ b/src/HOL/Tools/numeral.ML Sun Mar 30 13:50:06 2025 +0200
@@ -104,7 +104,7 @@
let
fun pretty literals _ thm _ _ [(t, _)] =
case dest_num_code t of
- SOME n => (Code_Printer.str o print literals o preproc) n
+ SOME n => (Pretty.str o print literals o preproc) n
| NONE => Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term";
in
thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,
--- a/src/Tools/Code/code_haskell.ML Sun Mar 30 13:50:06 2025 +0200
+++ b/src/Tools/Code/code_haskell.ML Sun Mar 30 13:50:06 2025 +0200
@@ -51,20 +51,20 @@
| SOME class => class;
fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
of [] => []
- | constraints => enum "," "(" ")" (
+ | constraints => Pretty.enum "," "(" ")" (
map (fn (v, class) =>
- str (class_name class ^ " " ^ lookup_var tyvars v)) constraints)
- @@ str " => ";
+ Pretty.str (class_name class ^ " " ^ lookup_var tyvars v)) constraints)
+ @@ Pretty.str " => ";
fun print_typforall tyvars vs = case map fst vs
of [] => []
- | vnames => str "forall " :: Pretty.breaks
- (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
+ | vnames => Pretty.str "forall " :: Pretty.breaks
+ (map (Pretty.str o lookup_var tyvars) vnames) @ Pretty.str "." @@ Pretty.brk 1;
fun print_tyco_expr tyvars fxy (tyco, tys) =
- brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
+ brackify fxy (Pretty.str tyco :: map (print_typ tyvars BR) tys)
and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
of NONE => print_tyco_expr tyvars fxy (deresolve_tyco tyco, tys)
| SOME (_, print) => print (print_typ tyvars) fxy tys)
- | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
+ | print_typ tyvars fxy (ITyVar v) = (Pretty.str o lookup_var tyvars) v;
fun print_typdecl tyvars (tyco, vs) =
print_tyco_expr tyvars NOBR (tyco, map ITyVar vs);
fun print_typscheme tyvars (vs, ty) =
@@ -80,14 +80,14 @@
print_term tyvars some_thm vars BR t2
])
| print_term tyvars some_thm vars fxy (IVar NONE) =
- str "_"
+ Pretty.str "_"
| print_term tyvars some_thm vars fxy (IVar (SOME v)) =
- (str o lookup_var vars) v
+ (Pretty.str o lookup_var vars) v
| print_term tyvars some_thm vars fxy (t as _ `|=> _) =
let
val (binds, t') = Code_Thingol.unfold_pat_abs t;
val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
- in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
+ in brackets (Pretty.str "\\" :: ps @ Pretty.str "->" @@ print_term tyvars some_thm vars' NOBR t') end
| print_term tyvars some_thm vars fxy (ICase case_expr) =
(case Code_Thingol.unfold_const_app (#primitive case_expr)
of SOME (app as ({ sym = Constant const, ... }, _)) =>
@@ -99,42 +99,42 @@
let
val printed_const =
case annotation of
- SOME ty => brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty]
- | NONE => (str o deresolve) sym
+ SOME ty => brackets [(Pretty.str o deresolve) sym, Pretty.str "::", print_typ tyvars NOBR ty]
+ | NONE => (Pretty.str o deresolve) sym
in
printed_const :: map (print_term tyvars some_thm vars BR) ts
end
and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
and print_case tyvars some_thm vars fxy { clauses = [], ... } =
- (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]
+ (brackify fxy o Pretty.breaks o map Pretty.str) ["error", "\"empty case\""]
| print_case tyvars some_thm vars fxy (case_expr as { clauses = [(IVar _, _)], ... }) =
let
val (vs, body) = Code_Thingol.unfold_let_no_pat (ICase case_expr);
fun print_assignment ((some_v, _), t) vars =
vars
|> print_bind tyvars some_thm BR (IVar some_v)
- |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t])
+ |>> (fn p => semicolon [p, Pretty.str "=", print_term tyvars some_thm vars NOBR t])
val (ps, vars') = fold_map print_assignment vs vars;
- in brackify_block fxy (str "let {")
+ in brackify_block fxy (Pretty.str "let {")
ps
- (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
+ (concat [Pretty.str "}", Pretty.str "in", print_term tyvars some_thm vars' NOBR body])
end
| print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
let
fun print_select (pat, body) =
let
val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
- in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end;
+ in semicolon [p, Pretty.str "->", print_term tyvars some_thm vars' NOBR body] end;
in Pretty.block_enclose
- (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
+ (concat [Pretty.str "(case", print_term tyvars some_thm vars NOBR t, Pretty.str "of", Pretty.str "{"], Pretty.str "})")
(map print_select clauses)
end;
fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
let
val tyvars = intro_vars (map fst vs) reserved;
fun print_err n =
- (semicolon o map str) (
+ (semicolon o map Pretty.str) (
deresolve_const const
:: replicate n "_"
@ "="
@@ -149,16 +149,16 @@
|> intro_vars (build (fold Code_Thingol.add_varnames ts));
in
semicolon (
- (str o deresolve_const) const
+ (Pretty.str o deresolve_const) const
:: map (print_term tyvars some_thm vars BR) ts
- @ str "="
+ @ Pretty.str "="
@@ print_term tyvars some_thm vars NOBR t
)
end;
in
Pretty.chunks (
semicolon [
- (str o suffix " ::" o deresolve_const) const,
+ (Pretty.str o suffix " ::" o deresolve_const) const,
print_typscheme tyvars (vs, ty)
]
:: (case filter (snd o snd) raw_eqs
@@ -171,7 +171,7 @@
val tyvars = intro_vars vs reserved;
in
semicolon [
- str "data",
+ Pretty.str "data",
print_typdecl tyvars (deresolve_tyco tyco, vs)
]
end
@@ -180,12 +180,12 @@
val tyvars = intro_vars vs reserved;
in
semicolon (
- str "newtype"
+ Pretty.str "newtype"
:: print_typdecl tyvars (deresolve_tyco tyco, vs)
- :: str "="
- :: (str o deresolve_const) co
+ :: Pretty.str "="
+ :: (Pretty.str o deresolve_const) co
:: print_typ tyvars BR ty
- :: (if deriving_show tyco then [str "deriving (Prelude.Read, Prelude.Show)"] else [])
+ :: (if deriving_show tyco then [Pretty.str "deriving (Prelude.Read, Prelude.Show)"] else [])
)
end
| print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
@@ -193,17 +193,17 @@
val tyvars = intro_vars vs reserved;
fun print_co ((co, _), tys) =
concat (
- (str o deresolve_const) co
+ (Pretty.str o deresolve_const) co
:: map (print_typ tyvars BR) tys
)
in
semicolon (
- str "data"
+ Pretty.str "data"
:: print_typdecl tyvars (deresolve_tyco tyco, vs)
- :: str "="
+ :: Pretty.str "="
:: print_co co
- :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
- @ (if deriving_show tyco then [str "deriving (Prelude.Read, Prelude.Show)"] else [])
+ :: map ((fn p => Pretty.block [Pretty.str "| ", p]) o print_co) cos
+ @ (if deriving_show tyco then [Pretty.str "deriving (Prelude.Read, Prelude.Show)"] else [])
)
end
| print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
@@ -211,19 +211,19 @@
val tyvars = intro_vars [v] reserved;
fun print_classparam (classparam, ty) =
semicolon [
- (str o deresolve_const) classparam,
- str "::",
+ (Pretty.str o deresolve_const) classparam,
+ Pretty.str "::",
print_typ tyvars NOBR ty
]
in
Pretty.block_enclose (
Pretty.block [
- str "class ",
+ Pretty.str "class ",
Pretty.block (print_typcontext tyvars [(v, map snd classrels)]),
- str (deresolve_class class ^ " " ^ lookup_var tyvars v),
- str " where {"
+ Pretty.str (deresolve_class class ^ " " ^ lookup_var tyvars v),
+ Pretty.str " where {"
],
- str "};"
+ Pretty.str "};"
) (map print_classparam classparams)
end
| print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) =
@@ -232,13 +232,13 @@
fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
case const_syntax classparam of
NONE => semicolon [
- (str o Long_Name.base_name o deresolve_const) classparam,
- str "=",
+ (Pretty.str o Long_Name.base_name o deresolve_const) classparam,
+ Pretty.str "=",
print_app tyvars (SOME thm) reserved NOBR (const, [])
]
| SOME (_, Code_Printer.Plain_printer s) => semicolon [
- (str o Long_Name.base_name) s,
- str "=",
+ (Pretty.str o Long_Name.base_name) s,
+ Pretty.str "=",
print_app tyvars (SOME thm) reserved NOBR (const, [])
]
| SOME (wanted, Code_Printer.Complex_printer _) =>
@@ -258,20 +258,20 @@
in
semicolon [
print_term tyvars (SOME thm) vars NOBR lhs,
- str "=",
+ Pretty.str "=",
print_term tyvars (SOME thm) vars NOBR rhs
]
end;
in
Pretty.block_enclose (
Pretty.block [
- str "instance ",
+ Pretty.str "instance ",
Pretty.block (print_typcontext tyvars vs),
- str (class_name class ^ " "),
+ Pretty.str (class_name class ^ " "),
print_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
- str " where {"
+ Pretty.str " where {"
],
- str "};"
+ Pretty.str "};"
) (map print_classparam_instance inst_params)
end;
in print_stmt end;
@@ -368,31 +368,31 @@
fun print_module_frame module_name header exports ps =
(module_names module_name, Pretty.chunks2 (
header
- @ concat [str "module",
+ @ concat [Pretty.str "module",
case exports of
- SOME ps => Pretty.block [str module_name, enclose "(" ")" (commas ps)]
- | NONE => str module_name,
- str "where {"
+ SOME ps => Pretty.block [Pretty.str module_name, Pretty.enclose "(" ")" (Pretty.commas ps)]
+ | NONE => Pretty.str module_name,
+ Pretty.str "where {"
]
:: ps
- @| str "}"
+ @| Pretty.str "}"
));
fun print_qualified_import module_name =
- semicolon [str "import qualified", str module_name];
+ semicolon [Pretty.str "import qualified", Pretty.str module_name];
val import_common_ps =
- enclose "import Prelude (" ");" (commas (map str
- (map (Library.enclose "(" ")") prelude_import_operators @ prelude_import_unqualified)
- @ map (fn (tyco, constrs) => (enclose (tyco ^ "(") ")" o commas o map str) constrs) prelude_import_unqualified_constr))
- :: enclose "import Data.Bits (" ");" (commas
- (map (str o Library.enclose "(" ")") data_bits_import_operators))
+ Pretty.enclose "import Prelude (" ");" (Pretty.commas (map Pretty.str
+ (map (enclose "(" ")") prelude_import_operators @ prelude_import_unqualified)
+ @ map (fn (tyco, constrs) => (Pretty.enclose (tyco ^ "(") ")" o Pretty.commas o map Pretty.str) constrs) prelude_import_unqualified_constr))
+ :: Pretty.enclose "import Data.Bits (" ");" (Pretty.commas
+ (map (Pretty.str o enclose "(" ")") data_bits_import_operators))
:: print_qualified_import "Prelude"
:: print_qualified_import "Data.Bits"
:: map (print_qualified_import o fst) includes;
fun print_module module_name (gr, imports) =
let
val deresolve = deresolver module_name;
- val deresolve_import = SOME o str o deresolve;
- val deresolve_import_attached = SOME o str o suffix "(..)" o deresolve;
+ val deresolve_import = SOME o Pretty.str o deresolve;
+ val deresolve_import_attached = SOME o Pretty.str o suffix "(..)" o deresolve;
fun print_import (sym, (_, Code_Thingol.Fun _)) = deresolve_import sym
| print_import (sym, (Code_Namespace.Public, Code_Thingol.Datatype _)) = deresolve_import_attached sym
| print_import (sym, (Code_Namespace.Opaque, Code_Thingol.Datatype _)) = deresolve_import sym
@@ -409,7 +409,7 @@
|> split_list
|> apfst (map_filter I);
in
- print_module_frame module_name [str language_pragma] (SOME export_ps)
+ print_module_frame module_name [Pretty.str language_pragma] (SOME export_ps)
((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
end;
@@ -430,7 +430,7 @@
val literals = Literals {
literal_string = print_haskell_string,
literal_numeral = print_numeral "Integer",
- literal_list = enum "," "[" "]",
+ literal_list = Pretty.enum "," "[" "]",
infix_cons = (5, ":")
};
@@ -455,22 +455,22 @@
(semicolon [print_term vars NOBR t], vars)
| print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars
|> print_bind NOBR bind
- |>> (fn p => semicolon [p, str "<-", print_term vars NOBR t])
+ |>> (fn p => semicolon [p, Pretty.str "<-", print_term vars NOBR t])
| print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars
|> print_bind NOBR bind
- |>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]);
+ |>> (fn p => semicolon [Pretty.str "let", Pretty.str "{", p, Pretty.str "=", print_term vars NOBR t, Pretty.str "}"]);
fun pretty _ print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
of SOME (bind, t') => let
val (binds, t'') = implode_monad t'
val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
(bind :: binds) vars;
in
- brackify_block fxy (str "do { ")
+ brackify_block fxy (Pretty.str "do { ")
(ps @| print_term vars' NOBR t'')
- (str " }")
+ (Pretty.str " }")
end
| NONE => brackify_infix (1, L) fxy
- (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
+ (print_term vars (INFX (1, L)) t1, Pretty.str ">>=", print_term vars (INFX (1, X)) t2)
in (2, pretty) end;
fun add_monad target' raw_c_bind thy =
@@ -499,7 +499,7 @@
[(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
- str "->",
+ Pretty.str "->",
print_typ (INFX (1, R)) ty2
)))]))
#> fold (Code_Target.add_reserved target) [
--- a/src/Tools/Code/code_ml.ML Sun Mar 30 13:50:06 2025 +0200
+++ b/src/Tools/Code/code_ml.ML Sun Mar 30 13:50:06 2025 +0200
@@ -42,11 +42,11 @@
fun print_product _ [] = NONE
| print_product print [x] = SOME (print x)
- | print_product print xs = (SOME o enum " *" "" "") (map print xs);
+ | print_product print xs = (SOME o Pretty.enum " *" "" "") (map print xs);
fun tuplify _ _ [] = NONE
| tuplify print fxy [x] = SOME (print fxy x)
- | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
+ | tuplify print _ xs = SOME (Pretty.enum "," "(" ")" (map (print NOBR) xs));
(** SML serializer **)
@@ -65,33 +65,33 @@
val deresolve_const = deresolve o Constant;
val deresolve_classrel = deresolve o Class_Relation;
val deresolve_inst = deresolve o Class_Instance;
- fun print_tyco_expr (sym, []) = (str o deresolve) sym
+ fun print_tyco_expr (sym, []) = (Pretty.str o deresolve) sym
| print_tyco_expr (sym, [ty]) =
- concat [print_typ BR ty, (str o deresolve) sym]
+ concat [print_typ BR ty, (Pretty.str o deresolve) sym]
| print_tyco_expr (sym, tys) =
- concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
+ concat [Pretty.enum "," "(" ")" (map (print_typ BR) tys), (Pretty.str o deresolve) sym]
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
of NONE => print_tyco_expr (Type_Constructor tyco, tys)
| SOME (_, print) => print print_typ fxy tys)
- | print_typ fxy (ITyVar v) = str ("'" ^ v);
+ | print_typ fxy (ITyVar v) = Pretty.str ("'" ^ v);
fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
- fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
+ fun print_typscheme_prefix (vs, p) = Pretty.enum " ->" "" ""
(map_filter (fn (v, sort) =>
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
fun print_classrels fxy [] ps = brackify fxy ps
- | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve_classrel) classrel, brackify BR ps]
+ | print_classrels fxy [classrel] ps = brackify fxy [(Pretty.str o deresolve_classrel) classrel, brackify BR ps]
| print_classrels fxy classrels ps =
- brackify fxy [enum " o" "(" ")" (map (str o deresolve_classrel) classrels), brackify BR ps]
+ brackify fxy [Pretty.enum " o" "(" ")" (map (Pretty.str o deresolve_classrel) classrels), brackify BR ps]
fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)
and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
- ((str o deresolve_inst) inst ::
- (if is_pseudo_fun (Class_Instance inst) then [str "()"]
+ ((Pretty.str o deresolve_inst) inst ::
+ (if is_pseudo_fun (Class_Instance inst) then [Pretty.str "()"]
else map_filter (print_dicts is_pseudo_fun BR o snd) dss))
| print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) =
- [str (if length = 1 then Name.enforce_case true var ^ "_"
+ [Pretty.str (if length = 1 then Name.enforce_case true var ^ "_"
else Name.enforce_case true var ^ string_of_int (index + 1) ^ "_")]
and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
@@ -100,9 +100,9 @@
fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
print_app is_pseudo_fun some_thm vars fxy (const, [])
| print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
- str "_"
+ Pretty.str "_"
| print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
- str (lookup_var vars v)
+ Pretty.str (lookup_var vars v)
| print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
of SOME app => print_app is_pseudo_fun some_thm vars fxy app
@@ -113,7 +113,7 @@
val (binds, t') = Code_Thingol.unfold_pat_abs t;
fun print_abs (pat, ty) =
print_bind is_pseudo_fun some_thm NOBR pat
- #>> (fn p => concat [str "fn", p, str "=>"]);
+ #>> (fn p => concat [Pretty.str "fn", p, Pretty.str "=>"]);
val (ps, vars') = fold_map print_abs binds vars;
in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
| print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
@@ -127,33 +127,33 @@
if is_constr sym then
let val wanted = length dom in
if wanted < 2 orelse length ts = wanted
- then (str o deresolve) sym
+ then (Pretty.str o deresolve) sym
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.saturated_application wanted app)]
end
else if is_pseudo_fun sym
- then (str o deresolve) sym @@ str "()"
- else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
+ then (Pretty.str o deresolve) sym @@ Pretty.str "()"
+ else (Pretty.str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
@ map (print_term is_pseudo_fun some_thm vars BR) ts
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
(print_term is_pseudo_fun) const_syntax some_thm vars
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
- (concat o map str) ["raise", "Fail", "\"empty case\""]
+ (concat o map Pretty.str) ["raise", "Fail", "\"empty case\""]
| print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
let
val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
fun print_match ((pat, _), t) vars =
vars
|> print_bind is_pseudo_fun some_thm NOBR pat
- |>> (fn p => semicolon [str "val", p, str "=",
+ |>> (fn p => semicolon [Pretty.str "val", p, Pretty.str "=",
print_term is_pseudo_fun some_thm vars NOBR t])
val (ps, vars') = fold_map print_match binds vars;
in
Pretty.chunks [
- Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps],
- Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun some_thm vars' NOBR body],
- str "end"
+ Pretty.block [Pretty.str "let", Pretty.fbrk, Pretty.chunks ps],
+ Pretty.block [Pretty.str "in", Pretty.fbrk, print_term is_pseudo_fun some_thm vars' NOBR body],
+ Pretty.str "end"
]
end
| print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
@@ -162,29 +162,29 @@
let
val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
in
- concat [str delim, p, str "=>", print_term is_pseudo_fun some_thm vars' NOBR body]
+ concat [Pretty.str delim, p, Pretty.str "=>", print_term is_pseudo_fun some_thm vars' NOBR body]
end;
in
brackets (
- str "case"
+ Pretty.str "case"
:: print_term is_pseudo_fun some_thm vars NOBR t
:: print_select "of" clause
:: map (print_select "|") clauses
)
end;
fun print_val_decl print_typscheme (sym, typscheme) = concat
- [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
+ [Pretty.str "val", Pretty.str (deresolve sym), Pretty.str ":", print_typscheme typscheme];
fun print_datatype_decl definer (tyco, (vs, cos)) =
let
- fun print_co ((co, _), []) = str (deresolve_const co)
- | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
- enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
+ fun print_co ((co, _), []) = Pretty.str (deresolve_const co)
+ | print_co ((co, _), tys) = concat [Pretty.str (deresolve_const co), Pretty.str "of",
+ Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
in
concat (
- str definer
+ Pretty.str definer
:: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
- :: str "="
- :: separate (str "|") (map print_co cos)
+ :: Pretty.str "="
+ :: separate (Pretty.str "|") (map print_co cos)
)
end;
fun print_def is_pseudo_fun needs_typ definer
@@ -197,15 +197,15 @@
deresolve (t :: ts)
|> intro_vars (build (fold Code_Thingol.add_varnames ts));
val prolog = if needs_typ then
- concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
- else (concat o map str) [definer, deresolve_const const];
+ concat [Pretty.str definer, (Pretty.str o deresolve_const) const, Pretty.str ":", print_typ NOBR ty]
+ else (concat o map Pretty.str) [definer, deresolve_const const];
in
concat (
prolog
- :: (if is_pseudo_fun (Constant const) then [str "()"]
+ :: (if is_pseudo_fun (Constant const) then [Pretty.str "()"]
else print_dict_args vs
@ map (print_term is_pseudo_fun some_thm vars BR) ts)
- @ str "="
+ @ Pretty.str "="
@@ print_term is_pseudo_fun some_thm vars NOBR t
)
end
@@ -223,35 +223,35 @@
let
fun print_super_instance (super_class, x) =
concat [
- (str o Long_Name.base_name o deresolve_classrel) (class, super_class),
- str "=",
+ (Pretty.str o Long_Name.base_name o deresolve_classrel) (class, super_class),
+ Pretty.str "=",
print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
];
fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
concat [
- (str o Long_Name.base_name o deresolve_const) classparam,
- str "=",
+ (Pretty.str o Long_Name.base_name o deresolve_const) classparam,
+ Pretty.str "=",
print_app (K false) (SOME thm) reserved NOBR (const, [])
];
in pair
(print_val_decl print_dicttypscheme
(Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
(concat (
- str definer
- :: (str o deresolve_inst) inst
- :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
+ Pretty.str definer
+ :: (Pretty.str o deresolve_inst) inst
+ :: (if is_pseudo_fun (Class_Instance inst) then [Pretty.str "()"]
else print_dict_args vs)
- @ str "="
- :: enum "," "{" "}"
+ @ Pretty.str "="
+ :: Pretty.enum "," "{" "}"
(map print_super_instance superinsts
@ map print_classparam_instance inst_params)
- :: str ":"
+ :: Pretty.str ":"
@@ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
))
end;
fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair
[print_val_decl print_typscheme (Constant const, vs_ty)]
- ((semicolon o map str) (
+ ((semicolon o map Pretty.str) (
(if n = 0 then "val" else "fun")
:: deresolve_const const
:: replicate n "_"
@@ -271,11 +271,11 @@
let
val print_def' = print_def (member (op =) pseudo_funs) false;
fun print_pseudo_fun sym = concat [
- str "val",
- (str o deresolve) sym,
- str "=",
- (str o deresolve) sym,
- str "();"
+ Pretty.str "val",
+ (Pretty.str o deresolve) sym,
+ Pretty.str "=",
+ (Pretty.str o deresolve) sym,
+ Pretty.str "();"
];
val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
(print_def' "fun" binding :: map (print_def' "and" o snd) exports_bindings);
@@ -290,8 +290,8 @@
val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
in
pair
- [concat [str "type", ty_p]]
- (semicolon [str "datatype", ty_p, str "=", str "EMPTY__"])
+ [concat [Pretty.str "type", ty_p]]
+ (semicolon [Pretty.str "datatype", ty_p, Pretty.str "=", Pretty.str "EMPTY__"])
end
| print_stmt export (ML_Datas (data :: datas)) =
let
@@ -302,15 +302,15 @@
(if Code_Namespace.is_public export
then decl_ps
else map (fn (tyco, (vs, _)) =>
- concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)])
+ concat [Pretty.str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)])
(data :: datas))
(Pretty.chunks (ps @| semicolon [p]))
end
| print_stmt export (ML_Class (class, (v, (classrels, classparams)))) =
let
- fun print_field s p = concat [str s, str ":", p];
+ fun print_field s p = concat [Pretty.str s, Pretty.str ":", p];
fun print_proj s p = semicolon
- (map str ["val", s, "=", "#" ^ s, ":"] @| p);
+ (map Pretty.str ["val", s, "=", "#" ^ s, ":"] @| p);
fun print_super_class_decl (classrel as (_, super_class)) =
print_val_decl print_dicttypscheme
(Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
@@ -328,17 +328,17 @@
print_proj (deresolve_const classparam)
(print_typscheme ([(v, [class])], ty));
in pair
- (concat [str "type", print_dicttyp (class, ITyVar v)]
+ (concat [Pretty.str "type", print_dicttyp (class, ITyVar v)]
:: (if Code_Namespace.is_public export
then map print_super_class_decl classrels
@ map print_classparam_decl classparams
else []))
(Pretty.chunks (
concat [
- str "type",
+ Pretty.str "type",
print_dicttyp (class, ITyVar v),
- str "=",
- enum "," "{" "};" (
+ Pretty.str "=",
+ Pretty.enum "," "{" "};" (
map print_super_class_field classrels
@ map print_classparam_field classparams
)
@@ -352,18 +352,18 @@
fun print_sml_module name decls body =
Pretty.chunks2 (
Pretty.chunks [
- str ("structure " ^ name ^ " : sig"),
- (indent 2 o Pretty.chunks) decls,
- str "end = struct"
+ Pretty.str ("structure " ^ name ^ " : sig"),
+ (Pretty.indent 2 o Pretty.chunks) decls,
+ Pretty.str "end = struct"
]
:: body
- @| str ("end; (*struct " ^ name ^ "*)")
+ @| Pretty.str ("end; (*struct " ^ name ^ "*)")
);
val literals_sml = Literals {
literal_string = print_sml_string,
literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
- literal_list = enum "," "[" "]",
+ literal_list = Pretty.enum "," "[" "]",
infix_cons = (7, "::")
};
@@ -392,32 +392,32 @@
val deresolve_const = deresolve o Constant;
val deresolve_classrel = deresolve o Class_Relation;
val deresolve_inst = deresolve o Class_Instance;
- fun print_tyco_expr (sym, []) = (str o deresolve) sym
+ fun print_tyco_expr (sym, []) = (Pretty.str o deresolve) sym
| print_tyco_expr (sym, [ty]) =
- concat [print_typ BR ty, (str o deresolve) sym]
+ concat [print_typ BR ty, (Pretty.str o deresolve) sym]
| print_tyco_expr (sym, tys) =
- concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
+ concat [Pretty.enum "," "(" ")" (map (print_typ BR) tys), (Pretty.str o deresolve) sym]
and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
of NONE => print_tyco_expr (Type_Constructor tyco, tys)
| SOME (_, print) => print print_typ fxy tys)
- | print_typ fxy (ITyVar v) = str ("'" ^ v);
+ | print_typ fxy (ITyVar v) = Pretty.str ("'" ^ v);
fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
- fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
+ fun print_typscheme_prefix (vs, p) = Pretty.enum " ->" "" ""
(map_filter (fn (v, sort) =>
(print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
val print_classrels =
- fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve_classrel) classrel])
+ fold_rev (fn classrel => fn p => Pretty.block [p, Pretty.str ".", (Pretty.str o deresolve_classrel) classrel])
fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
print_plain_dict is_pseudo_fun fxy x
|> print_classrels classrels
and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
- brackify BR ((str o deresolve_inst) inst ::
- (if is_pseudo_fun (Class_Instance inst) then [str "()"]
+ brackify BR ((Pretty.str o deresolve_inst) inst ::
+ (if is_pseudo_fun (Class_Instance inst) then [Pretty.str "()"]
else map_filter (print_dicts is_pseudo_fun BR o snd) dss))
| print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) =
- str (if length = 1 then "_" ^ Name.enforce_case true var
+ Pretty.str (if length = 1 then "_" ^ Name.enforce_case true var
else "_" ^ Name.enforce_case true var ^ string_of_int (index + 1))
and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
@@ -426,9 +426,9 @@
fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
print_app is_pseudo_fun some_thm vars fxy (const, [])
| print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
- str "_"
+ Pretty.str "_"
| print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
- str (lookup_var vars v)
+ Pretty.str (lookup_var vars v)
| print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
of SOME app => print_app is_pseudo_fun some_thm vars fxy app
@@ -438,7 +438,7 @@
let
val (binds, t') = Code_Thingol.unfold_pat_abs t;
val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
- in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
+ in brackets (Pretty.str "fun" :: ps @ Pretty.str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
| print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
(case Code_Thingol.unfold_const_app (#primitive case_expr)
of SOME (app as ({ sym = Constant const, ... }, _)) =>
@@ -450,19 +450,19 @@
if is_constr sym then
let val wanted = length dom in
if length ts = wanted
- then (str o deresolve) sym
+ then (Pretty.str o deresolve) sym
:: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.saturated_application wanted app)]
end
else if is_pseudo_fun sym
- then (str o deresolve) sym @@ str "()"
- else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
+ then (Pretty.str o deresolve) sym @@ Pretty.str "()"
+ else (Pretty.str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
@ map (print_term is_pseudo_fun some_thm vars BR) ts
and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
(print_term is_pseudo_fun) const_syntax some_thm vars
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
- (concat o map str) ["failwith", "\"empty case\""]
+ (concat o map Pretty.str) ["failwith", "\"empty case\""]
| print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
let
val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
@@ -470,7 +470,7 @@
vars
|> print_bind is_pseudo_fun some_thm NOBR pat
|>> (fn p => concat
- [str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"])
+ [Pretty.str "let", p, Pretty.str "=", print_term is_pseudo_fun some_thm vars NOBR t, Pretty.str "in"])
val (ps, vars') = fold_map print_let binds vars;
in
brackets [Pretty.chunks ps, print_term is_pseudo_fun some_thm vars' NOBR body]
@@ -480,28 +480,28 @@
fun print_select delim (pat, body) =
let
val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
- in concat [str delim, p, str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end;
+ in concat [Pretty.str delim, p, Pretty.str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end;
in
brackets (
- str "match"
+ Pretty.str "match"
:: print_term is_pseudo_fun some_thm vars NOBR t
:: print_select "with" clause
:: map (print_select "|") clauses
)
end;
fun print_val_decl print_typscheme (sym, typscheme) = concat
- [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
+ [Pretty.str "val", Pretty.str (deresolve sym), Pretty.str ":", print_typscheme typscheme];
fun print_datatype_decl definer (tyco, (vs, cos)) =
let
- fun print_co ((co, _), []) = str (deresolve_const co)
- | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
- enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
+ fun print_co ((co, _), []) = Pretty.str (deresolve_const co)
+ | print_co ((co, _), tys) = concat [Pretty.str (deresolve_const co), Pretty.str "of",
+ Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
in
concat (
- str definer
+ Pretty.str definer
:: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
- :: str "="
- :: separate (str "|") (map print_co cos)
+ :: Pretty.str "="
+ :: separate (Pretty.str "|") (map print_co cos)
)
end;
fun print_def is_pseudo_fun needs_typ definer
@@ -514,9 +514,9 @@
deresolve (t :: ts)
|> intro_vars (build (fold Code_Thingol.add_varnames ts));
in concat [
- (Pretty.block o commas)
+ (Pretty.block o Pretty.commas)
(map (print_term is_pseudo_fun some_thm vars NOBR) ts),
- str "->",
+ Pretty.str "->",
print_term is_pseudo_fun some_thm vars NOBR t
] end;
fun print_eqns is_pseudo [((ts, t), (some_thm, _))] =
@@ -527,20 +527,20 @@
|> intro_vars (build (fold Code_Thingol.add_varnames ts));
in
concat (
- (if is_pseudo then [str "()"]
+ (if is_pseudo then [Pretty.str "()"]
else map (print_term is_pseudo_fun some_thm vars BR) ts)
- @ str "="
+ @ Pretty.str "="
@@ print_term is_pseudo_fun some_thm vars NOBR t
)
end
| print_eqns _ ((eq as (([_], _), _)) :: eqs) =
Pretty.block (
- str "="
+ Pretty.str "="
:: Pretty.brk 1
- :: str "function"
+ :: Pretty.str "function"
:: Pretty.brk 1
:: print_eqn eq
- :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
+ :: maps (append [Pretty.fbrk, Pretty.str "|", Pretty.brk 1]
o single o print_eqn) eqs
)
| print_eqns _ (eqs as eq :: eqs') =
@@ -548,27 +548,27 @@
val vars = reserved
|> intro_base_names_for (is_none o const_syntax)
deresolve (map (snd o fst) eqs)
- val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
+ val dummy_parms = (map Pretty.str o aux_params vars o map (fst o fst)) eqs;
in
Pretty.block (
Pretty.breaks dummy_parms
@ Pretty.brk 1
- :: str "="
+ :: Pretty.str "="
:: Pretty.brk 1
- :: str "match"
+ :: Pretty.str "match"
:: Pretty.brk 1
- :: (Pretty.block o commas) dummy_parms
+ :: (Pretty.block o Pretty.commas) dummy_parms
:: Pretty.brk 1
- :: str "with"
+ :: Pretty.str "with"
:: Pretty.brk 1
:: print_eqn eq
- :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
+ :: maps (append [Pretty.fbrk, Pretty.str "|", Pretty.brk 1]
o single o print_eqn) eqs'
)
end;
val prolog = if needs_typ then
- concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
- else (concat o map str) [definer, deresolve_const const];
+ concat [Pretty.str definer, (Pretty.str o deresolve_const) const, Pretty.str ":", print_typ NOBR ty]
+ else (concat o map Pretty.str) [definer, deresolve_const const];
in pair
(print_val_decl print_typscheme (Constant const, vs_ty))
(concat (
@@ -582,36 +582,36 @@
let
fun print_super_instance (super_class, dss) =
concat [
- (str o deresolve_classrel) (class, super_class),
- str "=",
+ (Pretty.str o deresolve_classrel) (class, super_class),
+ Pretty.str "=",
print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), dss)))
];
fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
concat [
- (str o deresolve_const) classparam,
- str "=",
+ (Pretty.str o deresolve_const) classparam,
+ Pretty.str "=",
print_app (K false) (SOME thm) reserved NOBR (const, [])
];
in pair
(print_val_decl print_dicttypscheme
(Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
(concat (
- str definer
- :: (str o deresolve_inst) inst
- :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
+ Pretty.str definer
+ :: (Pretty.str o deresolve_inst) inst
+ :: (if is_pseudo_fun (Class_Instance inst) then [Pretty.str "()"]
else print_dict_args vs)
- @ str "="
+ @ Pretty.str "="
@@ brackets [
enum_default "()" ";" "{" "}" (map print_super_instance superinsts
@ map print_classparam_instance inst_params),
- str ":",
+ Pretty.str ":",
print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
]
))
end;
fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair
[print_val_decl print_typscheme (Constant const, vs_ty)]
- ((doublesemicolon o map str) (
+ ((doublesemicolon o map Pretty.str) (
"let"
:: deresolve_const const
:: replicate n "_"
@@ -630,11 +630,11 @@
let
val print_def' = print_def (member (op =) pseudo_funs) false;
fun print_pseudo_fun sym = concat [
- str "let",
- (str o deresolve) sym,
- str "=",
- (str o deresolve) sym,
- str "();;"
+ Pretty.str "let",
+ (Pretty.str o deresolve) sym,
+ Pretty.str "=",
+ (Pretty.str o deresolve) sym,
+ Pretty.str "();;"
];
val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
(print_def' "let rec" binding :: map (print_def' "and" o snd) exports_bindings);
@@ -649,8 +649,8 @@
val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
in
pair
- [concat [str "type", ty_p]]
- (doublesemicolon [str "type", ty_p, str "=", str "EMPTY__"])
+ [concat [Pretty.str "type", ty_p]]
+ (doublesemicolon [Pretty.str "type", ty_p, Pretty.str "=", Pretty.str "EMPTY__"])
end
| print_stmt export (ML_Datas (data :: datas)) =
let
@@ -661,13 +661,13 @@
(if Code_Namespace.is_public export
then decl_ps
else map (fn (tyco, (vs, _)) =>
- concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)])
+ concat [Pretty.str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)])
(data :: datas))
(Pretty.chunks (ps @| doublesemicolon [p]))
end
| print_stmt export (ML_Class (class, (v, (classrels, classparams)))) =
let
- fun print_field s p = concat [str s, str ":", p];
+ fun print_field s p = concat [Pretty.str s, Pretty.str ":", p];
fun print_super_class_field (classrel as (_, super_class)) =
print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
fun print_classparam_decl (classparam, ty) =
@@ -677,12 +677,12 @@
print_field (deresolve_const classparam) (print_typ NOBR ty);
val w = "_" ^ Name.enforce_case true v;
fun print_classparam_proj (classparam, _) =
- (concat o map str) ["let", deresolve_const classparam, w, "=",
+ (concat o map Pretty.str) ["let", deresolve_const classparam, w, "=",
w ^ "." ^ deresolve_const classparam ^ ";;"];
val type_decl_p = concat [
- str "type",
+ Pretty.str "type",
print_dicttyp (class, ITyVar v),
- str "=",
+ Pretty.str "=",
enum_default "unit" ";" "{" "}" (
map print_super_class_field classrels
@ map print_classparam_field classparams
@@ -693,7 +693,7 @@
then type_decl_p :: map print_classparam_decl classparams
else if null classrels andalso null classparams
then [type_decl_p] (*work around weakness in export calculation*)
- else [concat [str "type", print_dicttyp (class, ITyVar v)]])
+ else [concat [Pretty.str "type", print_dicttyp (class, ITyVar v)]])
(Pretty.chunks (
doublesemicolon [type_decl_p]
:: map print_classparam_proj classparams
@@ -704,12 +704,12 @@
fun print_ocaml_module name decls body =
Pretty.chunks2 (
Pretty.chunks [
- str ("module " ^ name ^ " : sig"),
- (indent 2 o Pretty.chunks) decls,
- str "end = struct"
+ Pretty.str ("module " ^ name ^ " : sig"),
+ (Pretty.indent 2 o Pretty.chunks) decls,
+ Pretty.str "end = struct"
]
:: body
- @| str ("end;; (*struct " ^ name ^ "*)")
+ @| Pretty.str ("end;; (*struct " ^ name ^ "*)")
);
val literals_ocaml = let
@@ -721,7 +721,7 @@
in Literals {
literal_string = print_ocaml_string,
literal_numeral = numeral_ocaml,
- literal_list = enum ";" "[" "]",
+ literal_list = Pretty.enum ";" "[" "]",
infix_cons = (6, "::")
} end;
@@ -868,7 +868,7 @@
fun fun_syntax print_typ fxy [ty1, ty2] =
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
- str "->",
+ Pretty.str "->",
print_typ (INFX (1, R)) ty2
);
--- a/src/Tools/Code/code_printer.ML Sun Mar 30 13:50:06 2025 +0200
+++ b/src/Tools/Code/code_printer.ML Sun Mar 30 13:50:06 2025 +0200
@@ -15,16 +15,11 @@
val @@ : 'a * 'a -> 'a list
val @| : 'a list * 'a -> 'a list
- val str: string -> Pretty.T
val concat: Pretty.T list -> Pretty.T
val brackets: Pretty.T list -> Pretty.T
- val enclose: string -> string -> Pretty.T list -> Pretty.T
- val commas: Pretty.T list -> Pretty.T list
- val enum: string -> string -> string -> Pretty.T list -> Pretty.T
val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
val semicolon: Pretty.T list -> Pretty.T
val doublesemicolon: Pretty.T list -> Pretty.T
- val indent: int -> Pretty.T -> Pretty.T
val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T
val format: Code_Symbol.T list -> int -> Pretty.T -> Bytes.T
@@ -121,17 +116,13 @@
infixr 5 @|;
fun x @@ y = [x, y];
fun xs @| y = xs @ [y];
-val str = Pretty.str;
val concat = Pretty.block o Pretty.breaks;
val commas = Pretty.commas;
-val enclose = Pretty.enclose;
-val brackets = enclose "(" ")" o Pretty.breaks;
-val enum = Pretty.enum;
-fun enum_default default sep l r [] = str default
- | enum_default default sep l r xs = enum sep l r xs;
-fun semicolon ps = Pretty.block [concat ps, str ";"];
-fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
-val indent = Pretty.indent;
+val brackets = Pretty.enclose "(" ")" o Pretty.breaks;
+fun enum_default default sep l r [] = Pretty.str default
+ | enum_default default sep l r xs = Pretty.enum sep l r xs;
+fun semicolon ps = Pretty.block [concat ps, Pretty.str ";"];
+fun doublesemicolon ps = Pretty.block [concat ps, Pretty.str ";;"];
fun markup_stmt sym =
Pretty.mark (Markup.code_presentationN, [(Markup.stmt_nameN, Code_Symbol.marker sym)]);
@@ -251,34 +242,34 @@
| fixity _ _ = true;
fun gen_brackify _ [p] = p
- | gen_brackify true (ps as _::_) = enclose "(" ")" ps
+ | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps
| gen_brackify false (ps as _::_) = Pretty.block ps;
fun brackify fxy_ctxt =
gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
fun brackify_infix infx fxy_ctxt (l, m, r) =
- gen_brackify (fixity (INFX infx) fxy_ctxt) [l, str " ", m, Pretty.brk 1, r];
+ gen_brackify (fixity (INFX infx) fxy_ctxt) [l, Pretty.str " ", m, Pretty.brk 1, r];
fun brackify_block fxy_ctxt p1 ps p2 =
let val p = Pretty.block_enclose (p1, p2) ps
in if fixity BR fxy_ctxt
- then enclose "(" ")" [p]
+ then Pretty.enclose "(" ")" [p]
else p
end;
fun gen_applify strict opn cls f fxy_ctxt p [] =
if strict
- then gen_brackify (fixity BR fxy_ctxt) [p, str (opn ^ cls)]
+ then gen_brackify (fixity BR fxy_ctxt) [p, Pretty.str (opn ^ cls)]
else p
| gen_applify strict opn cls f fxy_ctxt p ps =
- gen_brackify (fixity BR fxy_ctxt) (p @@ enum "," opn cls (map f ps));
+ gen_brackify (fixity BR fxy_ctxt) (p @@ Pretty.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));
+ | tuplify print _ xs = SOME (Pretty.enum "," "(" ")" (map (print NOBR) xs));
(* generic syntax *)
@@ -337,7 +328,7 @@
Constant name => (case const_syntax name of
NONE => brackify fxy (print_app_expr some_thm vars app)
| SOME (_, Plain_printer s) =>
- brackify fxy (str s :: map (print_term some_thm vars BR) ts)
+ brackify fxy (Pretty.str s :: map (print_term some_thm vars BR) ts)
| SOME (wanted, Complex_printer print) =>
let
val ((vs_tys, (ts1, rty)), ts2) =
@@ -382,7 +373,7 @@
| fillin print (Arg fxy :: mfx) (a :: args) =
(print fxy o prep_arg) a :: fillin print mfx args
| fillin print (String s :: mfx) args =
- str s :: fillin print mfx args
+ Pretty.str s :: fillin print mfx args
| fillin print (Break :: mfx) args =
Pretty.brk 1 :: fillin print mfx args;
in
@@ -430,7 +421,7 @@
of_printer (printer_of_mixfix prep_arg (fixity, mfx));
fun parse_tyco_syntax x =
- (parse_mixfix >> syntax_of_mixfix (fn s => (0, (K o K o K o str) s)) I I) x;
+ (parse_mixfix >> syntax_of_mixfix (fn s => (0, (K o K o K o Pretty.str) s)) I I) x;
val parse_const_syntax =
parse_mixfix >> syntax_of_mixfix plain_const_syntax simple_const_syntax fst;
--- a/src/Tools/Code/code_runtime.ML Sun Mar 30 13:50:06 2025 +0200
+++ b/src/Tools/Code/code_runtime.ML Sun Mar 30 13:50:06 2025 +0200
@@ -55,7 +55,7 @@
val _ = Theory.setup
(Code_Target.add_derived_target (target, [(Code_ML.target_SML, I)])
#> Code_Target.set_printings (Type_Constructor (\<^type_name>\<open>prop\<close>,
- [(target, SOME (0, (K o K o K) (Code_Printer.str truthN)))]))
+ [(target, SOME (0, (K o K o K) (Pretty.str truthN)))]))
#> Code_Target.set_printings (Constant (\<^const_name>\<open>Code_Generator.holds\<close>,
[(target, SOME (Code_Printer.plain_const_syntax HoldsN))]))
#> Code_Target.add_reserved target thisN
@@ -685,7 +685,7 @@
| pr pr' _ [ty] =
Code_Printer.concat [pr' Code_Printer.BR ty, tyco']
| pr pr' _ tys =
- Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
+ Code_Printer.concat [Pretty.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
in
thy
|> Code_Target.set_printings (Type_Constructor (tyco, [(target, SOME (k, pr))]))
@@ -709,9 +709,9 @@
thy
|> Code_Target.add_reserved target module_name
|> Context.theory_map (compile_ML true code)
- |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
- |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
- |> fold (add_eval_const o apsnd Code_Printer.str) const_map
+ |> fold (add_eval_tyco o apsnd Pretty.str) tyco_map
+ |> fold (add_eval_constr o apsnd Pretty.str) constr_map
+ |> fold (add_eval_const o apsnd Pretty.str) const_map
| process_reflection (code, _) _ (SOME binding) thy =
let
val code_binding = Path.map_binding Code_Target.code_path binding;
@@ -856,7 +856,7 @@
|> Specification.axiomatization [(b, SOME T, NoSyn)] [] [] []
|-> (fn ([Const (const, _)], _) =>
Code_Target.set_printings (Constant (const,
- [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
+ [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Pretty.str) ml_name)))]))
#> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target Code_Target.generatedN NONE []));
fun process_file filepath (definienda, thy) =
--- 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) [
--- a/src/Tools/Code/code_target.ML Sun Mar 30 13:50:06 2025 +0200
+++ b/src/Tools/Code/code_target.ML Sun Mar 30 13:50:06 2025 +0200
@@ -656,7 +656,7 @@
local
-val format_source = Pretty.block0 o Pretty.fbreaks o map Code_Printer.str o split_lines;
+val format_source = Pretty.block0 o Pretty.fbreaks o map Pretty.str o split_lines;
fun eval_source (Literal s) = s
| eval_source (File p) = File.read p;