# HG changeset patch
# User haftmann
# Date 1291911943 -3600
# Node ID 6c0940392fb4271b2f416480a1e1e84144412f3b
# Parent  5cf62cefbbb4d9a9716b1825bbbee1ee2ae924f8
dictionary constants must permit explicit weakening of classes;
tuned names

diff -r 5cf62cefbbb4 -r 6c0940392fb4 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Thu Dec 09 09:58:33 2010 +0100
+++ b/src/Tools/Code/code_ml.ML	Thu Dec 09 17:25:43 2010 +0100
@@ -76,23 +76,20 @@
         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
-    fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) =
-          brackify fxy ((str o deresolve) inst ::
+    fun print_classrels fxy [] ps = brackify fxy ps
+      | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve) classrel, brackify BR ps]
+      | print_classrels fxy classrels ps =
+          brackify fxy [enum " o" "(" ")" (map (str o deresolve) classrels), brackify BR ps]
+    fun print_dict is_pseudo_fun fxy (Dict_Const (classrels, (inst, dss))) =
+          print_classrels fxy classrels ((str o deresolve) inst ::
             (if is_pseudo_fun inst then [str "()"]
             else map_filter (print_dicts is_pseudo_fun BR) dss))
-      | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) =
-          let
-            val v_p = str (if k = 1 then first_upper v ^ "_"
-              else first_upper v ^ string_of_int (i+1) ^ "_");
-          in case classrels
-           of [] => v_p
-            | [classrel] => brackets [(str o deresolve) classrel, v_p]
-            | classrels => brackets
-                [enum " o" "(" ")" (map (str o deresolve) classrels), v_p]
-          end
+      | print_dict is_pseudo_fun fxy (Dict_Var (classrels, (v, (i, k)))) =
+          print_classrels fxy classrels [str (if k = 1 then first_upper v ^ "_"
+            else first_upper v ^ string_of_int (i+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, _) => DictVar ([], (v, (i, length sort)))) sort));
+      (map_index (fn (i, _) => Dict_Var ([], (v, (i, length sort)))) sort));
     fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
           print_app is_pseudo_fun some_thm vars fxy (c, [])
       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
@@ -218,11 +215,11 @@
       | print_def is_pseudo_fun _ definer
           (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
           let
-            fun print_super_instance (_, (classrel, dss)) =
+            fun print_super_instance (_, (classrel, x)) =
               concat [
                 (str o Long_Name.base_name o deresolve) classrel,
                 str "=",
-                print_dict is_pseudo_fun NOBR (DictConst dss)
+                print_dict is_pseudo_fun NOBR (Dict_Const ([], x))
               ];
             fun print_classparam_instance ((classparam, const), (thm, _)) =
               concat [
@@ -381,18 +378,20 @@
         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
-    fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) =
-          brackify fxy ((str o deresolve) inst ::
+    val print_classrels =
+      fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve) classrel])
+    fun print_dict is_pseudo_fun fxy (Dict_Const (classrels, (inst, dss))) =
+          brackify BR ((str o deresolve) inst ::
             (if is_pseudo_fun inst then [str "()"]
             else map_filter (print_dicts is_pseudo_fun BR) dss))
-      | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) =
+          |> print_classrels classrels
+      | print_dict is_pseudo_fun fxy (Dict_Var (classrels, (v, (i, k)))) =
           str (if k = 1 then "_" ^ first_upper v
             else "_" ^ first_upper v ^ string_of_int (i+1))
-          |> fold_rev (fn classrel => fn p =>
-               Pretty.block [p, str ".", (str o deresolve) classrel]) classrels
+          |> print_classrels classrels
     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, _) => DictVar ([], (v, (i, length sort)))) sort));
+      (map_index (fn (i, _) => Dict_Var ([], (v, (i, length sort)))) sort));
     fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
           print_app is_pseudo_fun some_thm vars fxy (c, [])
       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
@@ -553,11 +552,11 @@
       | print_def is_pseudo_fun _ definer
             (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
           let
-            fun print_super_instance (_, (classrel, dss)) =
+            fun print_super_instance (_, (classrel, x)) =
               concat [
                 (str o deresolve) classrel,
                 str "=",
-                print_dict is_pseudo_fun NOBR (DictConst dss)
+                print_dict is_pseudo_fun NOBR (Dict_Const ([], x))
               ];
             fun print_classparam_instance ((classparam, const), (thm, _)) =
               concat [
diff -r 5cf62cefbbb4 -r 6c0940392fb4 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Dec 09 09:58:33 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML	Thu Dec 09 17:25:43 2010 +0100
@@ -15,8 +15,8 @@
 sig
   type vname = string;
   datatype dict =
-      DictConst of string * dict list list
-    | DictVar of string list * (vname * (int * int));
+      Dict_Const of string list * (string * dict list list)
+    | Dict_Var of string list * (vname * (int * int));
   datatype itype =
       `%% of string * itype list
     | ITyVar of vname;
@@ -50,7 +50,7 @@
   val unfold_const_app: iterm -> (const * iterm list) option
   val is_IVar: iterm -> bool
   val eta_expand: int -> const * iterm list -> iterm
-  val contains_dictvar: iterm -> bool
+  val contains_dict_var: iterm -> bool
   val locally_monomorphic: iterm -> bool
   val add_constnames: iterm -> string list -> string list
   val add_tyconames: iterm -> string list -> string list
@@ -132,8 +132,8 @@
 type vname = string;
 
 datatype dict =
-    DictConst of string * dict list list
-  | DictVar of string list * (vname * (int * int));
+    Dict_Const of string list * (string * dict list list)
+  | Dict_Var of string list * (vname * (int * int));
 
 datatype itype =
     `%% of string * itype list
@@ -242,10 +242,10 @@
       (Name.names ctxt "a" ((take l o drop j) tys));
   in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
 
-fun contains_dictvar t =
+fun contains_dict_var t =
   let
-    fun cont_dict (DictConst (_, dss)) = (exists o exists) cont_dict dss
-      | cont_dict (DictVar _) = true;
+    fun cont_dict (Dict_Const (_, (_, dss))) = (exists o exists) cont_dict dss
+      | cont_dict (Dict_Var _) = true;
     fun cont_term (IConst (_, ((_, dss), _))) = (exists o exists) cont_dict dss
       | cont_term (IVar _) = false
       | cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
@@ -641,7 +641,7 @@
       ensure_class thy algbr eqngr permissive super_class
       ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)
       ##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class])
-      #>> (fn ((super_class, classrel), [DictConst (inst, dss)]) =>
+      #>> (fn ((super_class, classrel), [Dict_Const ([], (inst, dss))]) =>
             (super_class, (classrel, (inst, dss))));
     fun translate_classparam_instance (c, ty) =
       let
@@ -801,32 +801,35 @@
   #>> (fn sort => (unprefix "'" v, sort))
 and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr permissive some_thm (ty, sort) =
   let
-    datatype typarg =
-        Global of (class * string) * typarg list list
+    datatype typarg_witness =
+        Global of (class * class) list * ((class * string) * typarg_witness list list)
       | Local of (class * class) list * (string * (int * sort));
-    fun class_relation (Global ((_, tyco), yss), _) class =
-          Global ((class, tyco), yss)
-      | class_relation (Local (classrels, v), sub_class) super_class =
-          Local ((sub_class, super_class) :: classrels, v);
-    fun type_constructor (tyco, _) yss class =
-      Global ((class, tyco), (map o map) fst yss);
+    fun add_classrel classrel (Global (classrels, x)) =
+          Global (classrel :: classrels, x)
+      | add_classrel classrel (Local (classrels, x)) =
+          Local (classrel :: classrels, x)
+    fun class_relation (d, sub_class) super_class =
+      add_classrel (sub_class, super_class) d;
+    fun type_constructor (tyco, _) dss class =
+      Global ([], ((class, tyco), (map o map) fst dss));
     fun type_variable (TFree (v, sort)) =
       let
         val sort' = proj_sort sort;
       in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
-    val typargs = Sorts.of_sort_derivation algebra
+    val typarg_witnesses = Sorts.of_sort_derivation algebra
       {class_relation = K (Sorts.classrel_derivation algebra class_relation),
        type_constructor = type_constructor,
        type_variable = type_variable} (ty, proj_sort sort)
       handle Sorts.CLASS_ERROR e => not_wellsorted thy permissive some_thm ty sort e;
-    fun mk_dict (Global (inst, yss)) =
-          ensure_inst thy algbr eqngr permissive inst
-          ##>> (fold_map o fold_map) mk_dict yss
-          #>> (fn (inst, dss) => DictConst (inst, dss))
+    fun mk_dict (Global (classrels, (inst, dss))) =
+          fold_map (ensure_classrel thy algbr eqngr permissive) classrels
+          ##>> ensure_inst thy algbr eqngr permissive inst
+          ##>> (fold_map o fold_map) mk_dict dss
+          #>> (fn ((classrels, inst), dss) => Dict_Const (classrels, (inst, dss)))
       | mk_dict (Local (classrels, (v, (n, sort)))) =
           fold_map (ensure_classrel thy algbr eqngr permissive) classrels
-          #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (n, length sort))))
-  in fold_map mk_dict typargs end;
+          #>> (fn classrels => Dict_Var (classrels, (unprefix "'" v, (n, length sort))))
+  in fold_map mk_dict typarg_witnesses end;
 
 
 (* store *)
diff -r 5cf62cefbbb4 -r 6c0940392fb4 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu Dec 09 09:58:33 2010 +0100
+++ b/src/Tools/nbe.ML	Thu Dec 09 17:25:43 2010 +0100
@@ -297,10 +297,12 @@
             then nbe_apps (nbe_fun 0 c) ts'
             else nbe_apps_constr idx_of c ts'
       end
-    and assemble_idict (DictConst (inst, dss)) =
-          assemble_constapp inst dss []
-      | assemble_idict (DictVar (supers, (v, (n, _)))) =
-          fold_rev (fn super => assemble_constapp super [] o single) supers (nbe_dict v n);
+    and assemble_classrels classrels =
+      fold_rev (fn classrel => assemble_constapp classrel [] o single) classrels
+    and assemble_idict (Dict_Const (classrels, (inst, dss))) =
+          assemble_classrels classrels (assemble_constapp inst dss [])
+      | assemble_idict (Dict_Var (classrels, (v, (n, _)))) =
+          assemble_classrels classrels (nbe_dict v n);
 
     fun assemble_iterm constapp =
       let