# HG changeset patch
# User haftmann
# Date 1679682617 0
# Node ID a6a81f848135c27c210d4650579c47f781382e2c
# Parent  596452389ad052c4286b321fcf96601cb80a450d
More explicit type information in dictionary arguments.

diff -r 596452389ad0 -r a6a81f848135 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Tools/Code/code_ml.ML	Fri Mar 24 18:30:17 2023 +0000
@@ -29,7 +29,7 @@
 datatype ml_binding =
     ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
   | ML_Instance of (string * class) * { class: class, tyco: string, vs: (vname * sort) list,
-        superinsts: (class * dict list list) list,
+        superinsts: (class * (itype * dict list) list) list,
         inst_params: ((string * (const * int)) * (thm * bool)) list,
         superinst_params: ((string * (const * int)) * (thm * bool)) list };
 
@@ -89,7 +89,7 @@
     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 "()"]
-            else map_filter (print_dicts is_pseudo_fun BR) dss))
+            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 ^ "_"
             else Name.enforce_case true var ^ string_of_int (index + 1) ^ "_")]
@@ -415,7 +415,7 @@
     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 "()"]
-            else map_filter (print_dicts is_pseudo_fun BR) dss))
+            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
             else "_" ^ Name.enforce_case true var ^ string_of_int (index + 1))
@@ -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, x) =
+            fun print_super_instance (super_class, dss) =
               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), dss)))
               ];
             fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
               concat [
diff -r 596452389ad0 -r a6a81f848135 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Tools/Code/code_scala.ML	Fri Mar 24 18:30:17 2023 +0000
@@ -75,7 +75,7 @@
       | print_var vars (SOME v) = (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) dss
+          applify_dictss tyvars ((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,
diff -r 596452389ad0 -r a6a81f848135 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Tools/Code/code_thingol.ML	Fri Mar 24 18:30:17 2023 +0000
@@ -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
   and plain_dict = 
-      Dict_Const of (string * class) * dict list list
+      Dict_Const of (string * class) * (itype * 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 =
@@ -78,7 +78,7 @@
     | Classrel of class * class
     | Classparam of class
     | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
-        superinsts: (class * dict list list) list,
+        superinsts: (class * (itype * dict list) list) list,
         inst_params: ((string * (const * int)) * (thm * bool)) list,
         superinst_params: ((string * (const * int)) * (thm * bool)) list };
   type program = stmt Code_Symbol.Graph.T
@@ -136,16 +136,16 @@
 
 type vname = string;
 
+datatype itype =
+    `%% of string * itype list
+  | ITyVar of vname;
+
 datatype dict =
     Dict of (class * class) list * plain_dict
 and plain_dict = 
-    Dict_Const of (string * class) * dict list list
+    Dict_Const of (string * class) * (itype * 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];
 
 val op `--> = Library.foldr (op `->);
@@ -353,9 +353,9 @@
   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 dss
+and exists_plain_dict_var_pred f (Dict_Const (_, dss)) = exists_dictss_var f (map snd 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;
+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
   | contains_dict_var (IVar _) = false
@@ -378,7 +378,7 @@
   | Classrel of class * class
   | Classparam of class
   | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
-      superinsts: (class * dict list list) list,
+      superinsts: (class * (itype * dict list) list) list,
       inst_params: ((string * (const * int)) * (thm * bool)) list,
       superinst_params: ((string * (const * int)) * (thm * bool)) list };
 
@@ -552,7 +552,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) * (typ * typarg_witness list) list
   | Local of { var: string, index: int, sort: sort, unique: bool };
 
 fun brand_unique unique (w as Global _) = w
@@ -563,8 +563,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, typs) dss class =
+      Weakening ([], Global ((tyco, class), typs ~~ (map o map) fst dss));
     fun type_variable (TFree (v, sort)) =
       let
         val sort' = proj_sort sort;
@@ -832,21 +832,23 @@
   #>> (fn sort => (unprefix "'" v, sort))
 and translate_dicts ctxt algbr eqngr permissive some_thm (ty, sort) =
   let
-    fun mk_dict (Weakening (classrels, d)) =
+    fun translate_dict (Weakening (classrels, d)) =
           fold_map (ensure_classrel ctxt algbr eqngr permissive) classrels
-          ##>> mk_plain_dict d
+          ##>> translate_plain_dict d
           #>> Dict 
-    and mk_plain_dict (Global (inst, dss)) =
+    and translate_plain_dict (Global (inst, dss)) =
           ensure_inst ctxt algbr eqngr permissive inst
-          ##>> (fold_map o fold_map) mk_dict dss
+          ##>> fold_map (fn (ty, ds) =>
+            translate_typ ctxt algbr eqngr permissive ty
+            ##>> fold_map translate_dict ds) dss
           #>> Dict_Const
-      | mk_plain_dict (Local { var, index, sort, unique }) =
+      | translate_plain_dict (Local { var, index, sort, unique }) =
           ensure_class ctxt algbr eqngr permissive (nth sort index)
           #>> (fn class => Dict_Var { var = unprefix "'" var, index = index,
             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 translate_dict typarg_witnesses)
   end;
 
 
diff -r 596452389ad0 -r a6a81f848135 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Tools/nbe.ML	Fri Mar 24 18:30:17 2023 +0000
@@ -314,7 +314,7 @@
     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 []
+          assemble_constapp (Class_Instance inst) (map snd dss) []
       | assemble_plain_dict (Dict_Var { var, index, ... }) =
           nbe_dict var index
 
@@ -448,7 +448,7 @@
       []
   | 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, dss) => dummy_const (Class_Instance (tyco, class)) dss) superinsts
+        map (fn (class, dss) => dummy_const (Class_Instance (tyco, class)) (map snd dss)) superinsts
         @ map (IConst o fst o snd o fst) inst_params)]))];