--- a/src/Tools/Code/code_ml.ML Mon Mar 20 11:13:01 2023 +0100
+++ b/src/Tools/Code/code_ml.ML Mon Mar 20 22:38:40 2023 +0100
@@ -84,7 +84,7 @@
| print_classrels fxy [classrel] ps = brackify fxy [(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]
- fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
+ 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 ::
@@ -96,7 +96,7 @@
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
(map_index (fn (i, _) => Dict ([],
- Dict_Var { var = v, index = i, length = length sort, class = nth sort i, unique = true })) sort));
+ Dict_Var { var = v, index = i, length = length sort, class = nth sort i, unique = true }, "dummyT" `%% [])) sort));
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) =
@@ -225,7 +225,7 @@
concat [
(str o Long_Name.base_name o deresolve_classrel) (class, super_class),
str "=",
- print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
+ print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x), "dummyT" `%% []))
];
fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
concat [
@@ -409,7 +409,7 @@
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])
- fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
+ 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)) =
@@ -422,7 +422,7 @@
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
(map_index (fn (i, _) => Dict ([],
- Dict_Var { var = v, index = i, length = length sort, class = nth sort i, unique = true })) sort));
+ Dict_Var { var = v, index = i, length = length sort, class = nth sort i, unique = true }, "dummyT" `%% [])) sort));
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) =
@@ -584,7 +584,7 @@
concat [
(str o deresolve_classrel) (class, super_class),
str "=",
- print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
+ print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x), "dummyT" `%% []))
];
fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
concat [
--- a/src/Tools/Code/code_scala.ML Mon Mar 20 11:13:01 2023 +0100
+++ b/src/Tools/Code/code_scala.ML Mon Mar 20 22:38:40 2023 +0100
@@ -73,7 +73,7 @@
fun constraint p1 p2 = Pretty.block [p1, str ":", Pretty.brk 1, p2];
fun print_var vars NONE = str "_"
| print_var vars (SOME v) = (str o lookup_var vars) v;
- fun applify_dict tyvars (Dict (_, d)) = applify_plain_dict tyvars d
+ 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) dss
| applify_plain_dict tyvars (Dict_Var { var, class, ... }) =
--- a/src/Tools/Code/code_thingol.ML Mon Mar 20 11:13:01 2023 +0100
+++ b/src/Tools/Code/code_thingol.ML Mon Mar 20 22:38:40 2023 +0100
@@ -16,14 +16,14 @@
signature BASIC_CODE_THINGOL =
sig
type vname = string;
+ datatype itype =
+ `%% of string * itype list
+ | ITyVar of vname;
datatype dict =
- Dict of (class * class) list * plain_dict
+ Dict of (class * class) list * plain_dict * itype
and plain_dict =
Dict_Const of (string * class) * dict list list
| Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool };
- datatype itype =
- `%% of string * itype list
- | ITyVar of vname;
type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
dom: itype list, range: itype, annotation: itype option };
datatype iterm =
@@ -134,15 +134,16 @@
type vname = string;
+datatype itype =
+ `%% of string * itype list
+ | ITyVar of vname;
+
datatype dict =
- Dict of (class * class) list * plain_dict
+ Dict of (class * class) list * plain_dict * itype
and plain_dict =
Dict_Const of (string * class) * dict list list
| Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool };
-datatype itype =
- `%% of string * itype list
- | ITyVar of vname;
fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
@@ -334,7 +335,7 @@
build (fold_index (fn (i, SOME v) => cons (v, i) | _ => I) vs);
in distill vs_map (map IVar vs) body end;
-fun exists_dict_var f (Dict (_, d)) = exists_plain_dict_var_pred f d
+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 dss
| exists_plain_dict_var_pred f (Dict_Var x) = f x
and exists_dictss_var f dss = (exists o exists) (exists_dict_var f) dss;
@@ -534,7 +535,7 @@
datatype typarg_witness =
Weakening of (class * class) list * plain_typarg_witness
and plain_typarg_witness =
- Global of (string * class) * typarg_witness list list
+ Global of (string * class) * (typarg_witness list * typ) list
| Local of { var: string, index: int, sort: sort, unique: bool };
fun brand_unique unique (w as Global _) = w
@@ -545,8 +546,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, _) dss class =
- Weakening ([], Global ((tyco, class), (map o map) fst dss));
+ fun type_constructor (tyco, ts) dss class =
+ Weakening ([], Global ((tyco, class), map (fn (t,ds) => (map fst ds, t)) (ts ~~ dss)));
fun type_variable (TFree (v, sort)) =
let
val sort' = proj_sort sort;
@@ -647,7 +648,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 (_, dss), _)]) => (super_class, dss));
fun translate_classparam_instance (c, ty) =
let
val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
@@ -810,13 +811,14 @@
#>> (fn sort => (unprefix "'" v, sort))
and translate_dicts ctxt algbr eqngr permissive some_thm (ty, sort) =
let
- fun mk_dict (Weakening (classrels, d)) =
+ fun mk_dict ty (Weakening (classrels, d)) =
fold_map (ensure_classrel ctxt algbr eqngr permissive) classrels
##>> mk_plain_dict d
- #>> Dict
+ ##>> translate_typ ctxt algbr eqngr permissive ty
+ #>> (fn ((c, dss), t) => Dict (c, dss, t))
and mk_plain_dict (Global (inst, dss)) =
ensure_inst ctxt algbr eqngr permissive inst
- ##>> (fold_map o fold_map) mk_dict dss
+ ##>> fold_map (fn (ds, ty) => fold_map (mk_dict ty) ds) dss
#>> Dict_Const
| mk_plain_dict (Local { var, index, sort, unique }) =
ensure_class ctxt algbr eqngr permissive (nth sort index)
@@ -824,7 +826,7 @@
length = length sort, class = class, unique = unique })
in
construct_dictionaries ctxt algbr permissive some_thm (ty, sort)
- #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses)
+ #-> (fn typarg_witnesses => fold_map (mk_dict ty) typarg_witnesses)
end;
--- a/src/Tools/nbe.ML Mon Mar 20 11:13:01 2023 +0100
+++ b/src/Tools/nbe.ML Mon Mar 20 22:38:40 2023 +0100
@@ -311,7 +311,7 @@
end
and assemble_classrels classrels =
fold_rev (fn classrel => assemble_constapp (Class_Relation classrel) [] o single) classrels
- and assemble_dict (Dict (classrels, x)) =
+ and assemble_dict (Dict (classrels, x, _)) =
assemble_classrels classrels (assemble_plain_dict x)
and assemble_plain_dict (Dict_Const (inst, dss)) =
assemble_constapp (Class_Instance inst) dss []