--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Sun Apr 06 15:50:56 2025 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Sun Apr 06 16:05:35 2025 +0200
@@ -645,7 +645,7 @@
(*assumption: dummy values are not relevant for serialization*)
val unitT = \<^type_name>\<open>unit\<close> `%% [];
val unitt =
- IConst { sym = Code_Symbol.Constant \<^const_name>\<open>Unity\<close>, typargs = [], dicts = [], dom = [],
+ IConst { sym = Code_Symbol.Constant \<^const_name>\<open>Unity\<close>, typargs = [], dictss = [], dom = [],
annotation = NONE, range = unitT };
fun dest_abs ((v, ty) `|=> (t, _), _) = ((v, ty), t)
| dest_abs (t, ty) =
--- a/src/Tools/Code/code_haskell.ML Sun Apr 06 15:50:56 2025 +0200
+++ b/src/Tools/Code/code_haskell.ML Sun Apr 06 16:05:35 2025 +0200
@@ -252,7 +252,7 @@
val vars = reserved
|> intro_vars (map_filter I (s :: vs));
val lhs = IConst { sym = Constant classparam, typargs = [],
- dicts = [], dom = dom, range = range, annotation = NONE } `$$ map IVar vs;
+ dictss = [], dom = dom, range = range, annotation = NONE } `$$ map IVar vs;
(*dictionaries are not relevant in Haskell,
and these consts never need type annotations for disambiguation *)
in
--- a/src/Tools/Code/code_ml.ML Sun Apr 06 15:50:56 2025 +0200
+++ b/src/Tools/Code/code_ml.ML Sun Apr 06 16:05:35 2025 +0200
@@ -86,10 +86,10 @@
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)) =
+ and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dictss)) =
((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))
+ else map_filter (print_dicts is_pseudo_fun BR o snd) dictss))
| print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) =
[Pretty.str (if length = 1 then Name.enforce_case true var ^ "_"
else Name.enforce_case true var ^ string_of_int (index + 1) ^ "_")]
@@ -123,7 +123,7 @@
then print_case is_pseudo_fun some_thm vars fxy case_expr
else print_app is_pseudo_fun some_thm vars fxy app
| NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
- and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts, dom, ... }, ts)) =
+ and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dictss, dom, ... }, ts)) =
if is_constr sym then
let val wanted = length dom in
if wanted < 2 orelse length ts = wanted
@@ -133,7 +133,7 @@
end
else if is_pseudo_fun sym
then (Pretty.str o deresolve) sym @@ Pretty.str "()"
- else (Pretty.str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
+ else (Pretty.str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dictss
@ 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
@@ -412,10 +412,10 @@
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)) =
+ and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dictss)) =
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))
+ else map_filter (print_dicts is_pseudo_fun BR o snd) dictss))
| print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) =
Pretty.str (if length = 1 then "_" ^ Name.enforce_case true var
else "_" ^ Name.enforce_case true var ^ string_of_int (index + 1))
@@ -446,7 +446,7 @@
then print_case is_pseudo_fun some_thm vars fxy case_expr
else print_app is_pseudo_fun some_thm vars fxy app
| NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
- and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dicts, dom, ... }, ts)) =
+ and print_app_expr is_pseudo_fun some_thm vars (app as ({ sym, dictss, dom, ... }, ts)) =
if is_constr sym then
let val wanted = length dom in
if length ts = wanted
@@ -456,7 +456,7 @@
end
else if is_pseudo_fun sym
then (Pretty.str o deresolve) sym @@ Pretty.str "()"
- else (Pretty.str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
+ else (Pretty.str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dictss
@ 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
@@ -580,11 +580,11 @@
| print_def is_pseudo_fun _ definer
(ML_Instance (inst as (tyco, class), { vs, superinsts, inst_params, ... })) =
let
- fun print_super_instance (super_class, dss) =
+ fun print_super_instance (super_class, dictss) =
concat [
(Pretty.str o deresolve_classrel) (class, super_class),
Pretty.str "=",
- print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), dss)))
+ print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), dictss)))
];
fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
concat [
--- a/src/Tools/Code/code_preproc.ML Sun Apr 06 15:50:56 2025 +0200
+++ b/src/Tools/Code/code_preproc.ML Sun Apr 06 16:05:35 2025 +0200
@@ -511,7 +511,7 @@
(* applying instantiations *)
-fun dicts_of ctxt (proj_sort, algebra) (T, sort) =
+fun dictss_of ctxt (proj_sort, algebra) (T, sort) =
let
val thy = Proof_Context.theory_of ctxt;
fun class_relation _ (x, _) _ = x;
@@ -558,7 +558,7 @@
val algebra = Sorts.subalgebra (Context.Theory thy) (is_proper_class thy)
(AList.lookup (op =) arities') (Sign.classes_of thy);
val (rhss, eqngr') = Symtab.fold (add_cert ctxt vardeps) eqntab ([], eqngr);
- fun deps_of (c, rhs) = c :: maps (dicts_of ctxt algebra)
+ fun deps_of (c, rhs) = c :: maps (dictss_of ctxt algebra)
(rhs ~~ sortargs eqngr' c);
val eqngr'' = fold (fn (c, rhs) => fold
(curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
--- a/src/Tools/Code/code_scala.ML Sun Apr 06 15:50:56 2025 +0200
+++ b/src/Tools/Code/code_scala.ML Sun Apr 06 16:05:35 2025 +0200
@@ -74,14 +74,14 @@
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 ((Pretty.str o deresolve o Class_Instance) inst) (map snd dss)
+ and applify_plain_dict tyvars (Dict_Const (inst, dictss)) =
+ applify_dictss tyvars ((Pretty.str o deresolve o Class_Instance) inst) (map snd dictss)
| applify_plain_dict tyvars (Dict_Var { var, class, ... }) =
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)
+ and applify_dictss tyvars p dictss =
+ applify "(" ")" (applify_dict tyvars) NOBR p (flat dictss)
fun print_term tyvars is_pat some_thm vars fxy (IConst const) =
print_app tyvars is_pat some_thm vars fxy (const, [])
| print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
@@ -115,7 +115,7 @@
], vars')
end
and print_app tyvars is_pat some_thm vars fxy
- (app as (const as { sym, typargs, dom, dicts, ... }, ts)) =
+ (app as (const as { sym, typargs, dom, dictss, ... }, ts)) =
let
val typargs' = if is_pat then [] else typargs;
val syntax = case sym of
@@ -123,7 +123,7 @@
| _ => NONE;
val applify_dicts =
if is_pat orelse is_some syntax orelse is_constr sym
- orelse Code_Thingol.unambiguous_dictss dicts
+ orelse Code_Thingol.unambiguous_dictss dictss
then fn p => K p
else applify_dictss tyvars;
val (wanted, print') = case syntax of
@@ -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 ((Pretty.str o deresolve) sym) typargs') ts) dicts)
+ NOBR ((Pretty.str o deresolve) sym) typargs') ts) dictss)
| 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 (Pretty.str s) typargs') ts) dicts)
+ NOBR (Pretty.str s) typargs') ts) dictss)
| 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))
--- a/src/Tools/Code/code_thingol.ML Sun Apr 06 15:50:56 2025 +0200
+++ b/src/Tools/Code/code_thingol.ML Sun Apr 06 16:05:35 2025 +0200
@@ -24,7 +24,7 @@
and plain_dict =
Dict_Const of (string * class) * (itype * dict list) list
| Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool }
- type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
+ type const = { sym: Code_Symbol.T, typargs: itype list, dictss: dict list list,
dom: itype list, range: itype, annotation: itype option }
datatype iterm =
IConst of const
@@ -160,7 +160,7 @@
val (tys3, tys2) = chop n tys1;
in (tys3, tys2 `--> ty1) end;
-type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
+type const = { sym: Code_Symbol.T, typargs: itype list, dictss: dict list list,
dom: itype list, range: itype, annotation: itype option };
datatype iterm =
@@ -350,11 +350,11 @@
in distill vs_map (map IVar vs) body end;
fun exists_dict_var f (Dict (_, d)) = exists_plain_dict_var_pred f d
-and exists_plain_dict_var_pred f (Dict_Const (_, dss)) = exists_dictss_var f (map snd dss)
+and exists_plain_dict_var_pred f (Dict_Const (_, dictss)) = exists_dictss_var f (map snd dictss)
| exists_plain_dict_var_pred f (Dict_Var x) = f x
and exists_dictss_var f = (exists o exists) (exists_dict_var f);
-fun contains_dict_var (IConst { dicts = dss, ... }) = exists_dictss_var (K true) dss
+fun contains_dict_var (IConst { dictss = dictss, ... }) = exists_dictss_var (K true) dictss
| contains_dict_var (IVar _) = false
| contains_dict_var (t1 `$ t2) = contains_dict_var t1 orelse contains_dict_var t2
| contains_dict_var (_ `|=> (t, _)) = contains_dict_var t
@@ -560,8 +560,8 @@
let
fun class_relation unique (Weakening (classrels, x), sub_class) super_class =
Weakening ((sub_class, super_class) :: classrels, brand_unique unique x);
- fun type_constructor (tyco, typs) dss class =
- Weakening ([], Global ((tyco, class), typs ~~ (map o map) fst dss));
+ fun type_constructor (tyco, typs) dictss class =
+ Weakening ([], Global ((tyco, class), typs ~~ (map o map) fst dictss));
fun type_variable (TFree (v, sort)) =
let
val sort' = proj_sort sort;
@@ -662,7 +662,7 @@
fun translate_super_instance super_class =
ensure_class ctxt algbr eqngr permissive super_class
##>> translate_dicts ctxt algbr eqngr permissive NONE (arity_typ, [super_class])
- #>> (fn (super_class, [Dict ([], Dict_Const (_, dss))]) => (super_class, dss));
+ #>> (fn (super_class, [Dict ([], Dict_Const (_, dictss))]) => (super_class, dictss));
fun translate_classparam_instance (c, ty) =
let
val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
@@ -739,8 +739,8 @@
||>> fold_map (translate_typ ctxt algbr eqngr permissive) typargs
||>> fold_map (translate_dicts ctxt algbr eqngr permissive some_thm) (typargs ~~ sorts)
||>> fold_map (translate_typ ctxt algbr eqngr permissive) (range :: dom)
- |>> (fn (((c, typargs), dss), range :: dom) =>
- { sym = Constant c, typargs = typargs, dicts = dss,
+ |>> (fn (((c, typargs), dictss), range :: dom) =>
+ { sym = Constant c, typargs = typargs, dictss = dictss,
dom = dom, range = range, annotation =
if annotate then SOME (dom `--> range) else NONE })
end
@@ -806,11 +806,11 @@
fold_map (ensure_classrel ctxt algbr eqngr permissive) classrels
##>> translate_plain_dict d
#>> Dict
- and translate_plain_dict (Global (inst, dss)) =
+ and translate_plain_dict (Global (inst, dictss)) =
ensure_inst ctxt algbr eqngr permissive inst
- ##>> fold_map (fn (ty, ds) =>
+ ##>> fold_map (fn (ty, dicts) =>
translate_typ ctxt algbr eqngr permissive ty
- ##>> fold_map translate_dict ds) dss
+ ##>> fold_map translate_dict dicts) dictss
#>> Dict_Const
| translate_plain_dict (Local { var, index, sort, unique }) =
ensure_class ctxt algbr eqngr permissive (nth sort index)
--- a/src/Tools/nbe.ML Sun Apr 06 15:50:56 2025 +0200
+++ b/src/Tools/nbe.ML Sun Apr 06 16:05:35 2025 +0200
@@ -344,10 +344,10 @@
fun apply_constr sym = nbe_apps_constr (constr_fun_ident sym);
fun apply_constmatch sym = nbe_apps_constmatch (constr_fun_ident sym);
- fun assemble_constapp sym tys dicts ts =
+ fun assemble_constapp sym tys dictss ts =
let
val s_tys = map (assemble_type) tys;
- val ts' = (maps o map) assemble_dict (map2 (fn ty => map (fn dict => (ty, dict))) tys dicts) @ ts;
+ val ts' = (maps o map) assemble_dict (map2 (fn ty => map (fn dict => (ty, dict))) tys dictss) @ ts;
in case AList.lookup (op =) eqnss sym
of SOME (num_args, _) => if num_args <= length ts'
then let val (ts1, ts2) = chop num_args ts'
@@ -361,13 +361,13 @@
fold_rev (fn classrel => assemble_constapp (Class_Relation classrel) [] [] o single) classrels
and assemble_dict (ty, Dict (classrels, x)) =
assemble_classrels classrels (assemble_plain_dict ty x)
- and assemble_plain_dict (_ `%% tys) (Dict_Const (inst, dicts)) =
- assemble_constapp (Class_Instance inst) tys (map snd dicts) []
+ and assemble_plain_dict (_ `%% tys) (Dict_Const (inst, dictss)) =
+ assemble_constapp (Class_Instance inst) tys (map snd dictss) []
| assemble_plain_dict _ (Dict_Var { var, index, ... }) =
nbe_dict var index
- fun assemble_constmatch sym _ dicts ts =
- apply_constmatch sym ((maps o map) (K "_") dicts @ ts);
+ fun assemble_constmatch sym _ dictss ts =
+ apply_constmatch sym ((maps o map) (K "_") dictss @ ts);
fun assemble_iterm constapp =
let
@@ -375,7 +375,7 @@
let
val (t', ts) = Code_Thingol.unfold_app t
in of_iapp match_continuation t' (fold_rev (cons o of_iterm NONE) ts []) end
- and of_iapp match_continuation (IConst { sym, typargs = tys, dicts, ... }) ts = constapp sym tys dicts ts
+ and of_iapp match_continuation (IConst { sym, typargs = tys, dictss, ... }) ts = constapp sym tys dictss ts
| of_iapp match_continuation (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
| of_iapp match_continuation ((v, _) `|=> (t, _)) ts =
nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
@@ -446,8 +446,8 @@
(* extraction of equations from statements *)
-fun dummy_const sym tys dicts =
- IConst { sym = sym, typargs = tys, dicts = dicts,
+fun dummy_const sym tys dictss =
+ IConst { sym = sym, typargs = tys, dictss = dictss,
dom = [], annotation = NONE, range = ITyVar "" };
fun eqns_of_stmt (_, Code_Thingol.NoStmt) =
@@ -475,8 +475,8 @@
[]
| eqns_of_stmt (sym_inst, Code_Thingol.Classinst { class, tyco, vs, superinsts, inst_params, ... }) =
[(sym_inst, (vs, [([], dummy_const (Type_Class class) [] [] `$$
- map (fn (class, dicts) =>
- dummy_const (Class_Instance (tyco, class)) (map (ITyVar o fst) vs) (map snd dicts)) superinsts
+ map (fn (class, dictss) =>
+ dummy_const (Class_Instance (tyco, class)) (map (ITyVar o fst) vs) (map snd dictss)) superinsts
@ map (IConst o fst o snd o fst) inst_params)]))];