# HG changeset patch
# User haftmann
# Date 1457467668 -3600
# Node ID 00f8bca4aba0d9ca0c1565e08e31ae42ea0586c3
# Parent  85ebb645b1a347bd39a29ef775e632df19acc496
explicit record values for dictionary variables

diff -r 85ebb645b1a3 -r 00f8bca4aba0 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Tue Mar 08 21:07:47 2016 +0100
+++ b/src/Tools/Code/code_ml.ML	Tue Mar 08 21:07:48 2016 +0100
@@ -87,12 +87,13 @@
           ((str o deresolve_inst) inst ::
             (if is_pseudo_fun (Class_Instance inst) then [str "()"]
             else map_filter (print_dicts is_pseudo_fun BR) dss))
-      | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
-          [str (if k = 1 then Name.enforce_case true v ^ "_"
-            else Name.enforce_case true v ^ string_of_int (i+1) ^ "_")]
+      | 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) ^ "_")]
     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 (v, (i, length sort)))) sort));
+      (map_index (fn (i, _) =>
+        Dict ([], Dict_Var { var = v, index = i, length = length sort })) 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) =
@@ -398,12 +399,13 @@
           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))
-      | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
-          str (if k = 1 then "_" ^ Name.enforce_case true v
-            else "_" ^ Name.enforce_case true v ^ string_of_int (i+1))
+      | 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))
     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 (v, (i, length sort)))) sort));
+      (map_index (fn (i, _) =>
+        Dict ([], Dict_Var { var = v, index = i, length = length sort })) 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) =
diff -r 85ebb645b1a3 -r 00f8bca4aba0 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Tue Mar 08 21:07:47 2016 +0100
+++ b/src/Tools/Code/code_thingol.ML	Tue Mar 08 21:07:48 2016 +0100
@@ -19,7 +19,7 @@
       Dict of (class * class) list * plain_dict
   and plain_dict = 
       Dict_Const of (string * class) * dict list list
-    | Dict_Var of vname * (int * int);
+    | Dict_Var of { var: vname, index: int, length: int };
   datatype itype =
       `%% of string * itype list
     | ITyVar of vname;
@@ -132,7 +132,7 @@
     Dict of (class * class) list * plain_dict
 and plain_dict = 
     Dict_Const of (string * class) * dict list list
-  | Dict_Var of vname * (int * int);
+  | Dict_Var of { var: vname, index: int, length: int };
 
 datatype itype =
     `%% of string * itype list
@@ -760,8 +760,8 @@
           ensure_inst ctxt algbr eqngr permissive inst
           ##>> (fold_map o fold_map) mk_dict dss
           #>> (fn (inst, dss) => Dict_Const (inst, dss))
-      | mk_plain_dict (Local (v, (n, sort))) =
-          pair (Dict_Var (unprefix "'" v, (n, length sort)))
+      | mk_plain_dict (Local (v, (index, sort))) =
+          pair (Dict_Var { var = unprefix "'" v, index = index, length = length sort })
   in
     construct_dictionaries ctxt algbr permissive some_thm (ty, sort)
     #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses)
diff -r 85ebb645b1a3 -r 00f8bca4aba0 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Tue Mar 08 21:07:47 2016 +0100
+++ b/src/Tools/nbe.ML	Tue Mar 08 21:07:48 2016 +0100
@@ -311,8 +311,8 @@
           assemble_classrels classrels (assemble_plain_dict x)
     and assemble_plain_dict (Dict_Const (inst, dss)) =
           assemble_constapp (Class_Instance inst) dss []
-      | assemble_plain_dict (Dict_Var (v, (n, _))) =
-          nbe_dict v n
+      | assemble_plain_dict (Dict_Var { var, index, ... }) =
+          nbe_dict var index
 
     fun assemble_iterm constapp =
       let