diff -r 3f875966c3e1 -r ceb4f33d3073 src/Tools/Code/code_scala.ML --- 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) [