substantial improvements for class code generation
authorhaftmann
Fri, 09 Dec 2005 15:25:52 +0100
changeset 18380 9668764224a7
parent 18379 87cb7e641ba5
child 18381 246807ef6dfb
substantial improvements for class code generation
etc/isar-keywords-ZF.el
etc/isar-keywords.el
src/Pure/Tools/class_package.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/codegen_thingol.ML
--- a/etc/isar-keywords-ZF.el	Fri Dec 09 15:25:29 2005 +0100
+++ b/etc/isar-keywords-ZF.el	Fri Dec 09 15:25:52 2005 +0100
@@ -201,6 +201,7 @@
     "case_eqns"
     "con_defs"
     "concl"
+    "constants"
     "constrains"
     "contains"
     "defined_by"
@@ -208,7 +209,6 @@
     "depending_on"
     "domains"
     "elimination"
-    "extracting"
     "file"
     "files"
     "fixes"
--- a/etc/isar-keywords.el	Fri Dec 09 15:25:29 2005 +0100
+++ b/etc/isar-keywords.el	Fri Dec 09 15:25:52 2005 +0100
@@ -216,13 +216,13 @@
     "compose"
     "concl"
     "congs"
+    "constants"
     "constrains"
     "contains"
     "defined_by"
     "defines"
     "depending_on"
     "distinct"
-    "extracting"
     "file"
     "files"
     "fixes"
--- a/src/Pure/Tools/class_package.ML	Fri Dec 09 15:25:29 2005 +0100
+++ b/src/Pure/Tools/class_package.ML	Fri Dec 09 15:25:52 2005 +0100
@@ -227,7 +227,7 @@
       ) subclasses;
     fun mk_class_deriv thy subclasses superclass =
       case get_superclass_derivation (subclasses, superclass)
-      of (subclass::deriv) => (rev deriv, find_index_eq subclass subclasses);
+      of (subclass::deriv) => ((rev o filter (is_class thy)) deriv, find_index_eq subclass subclasses);
     fun mk_lookup (sort_def, (Type (tycon, tys))) =
           let
             val arity_lookup = map2 (curry mk_lookup)
--- a/src/Pure/Tools/codegen_package.ML	Fri Dec 09 15:25:29 2005 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Fri Dec 09 15:25:52 2005 +0100
@@ -60,14 +60,14 @@
     -> appgen;
   val appgen_case: (theory -> string -> (string * int) list option)
     -> appgen;
-  val defgen_datatype: (theory -> string -> (string list * string list) option)
+  val defgen_datatype: (theory -> string -> ((string * sort) list * string list) option)
     -> (theory -> string * string -> typ list option)
     -> defgen;
   val defgen_datacons: (theory -> string * string -> typ list option)
     -> defgen;
-  val defgen_datatype_eq: (theory -> string -> (string list * string list) option)
+  val defgen_datatype_eq: (theory -> string -> ((string * sort) list * string list) option)
     -> defgen;
-  val defgen_datatype_eqinst: (theory -> string -> (string list * string list) option)
+  val defgen_datatype_eqinst: (theory -> string -> ((string * sort) list * string list) option)
     -> defgen;
   val defgen_recfun: (theory -> string * typ -> (term list * term) list * typ)
     -> defgen;
@@ -122,6 +122,7 @@
 val nsp_class = "class";
 val nsp_type = "type";
 val nsp_const = "const";
+val nsp_dtcon = "dtcon"; (*NOT OPERATIONAL YET*)
 val nsp_mem = "mem";
 val nsp_inst = "inst";
 val nsp_eq_class = "eq_class";
@@ -134,7 +135,7 @@
   let
     val name_root = "Generated";
     val nsp_conn = [
-      [nsp_class, nsp_type, nsp_eq_class], [nsp_const, nsp_inst, nsp_mem, nsp_eq]
+      [nsp_class, nsp_type, nsp_eq_class], [nsp_const, nsp_dtcon, nsp_inst, nsp_mem, nsp_eq]
     ];
   in CodegenSerializer.ml_from_thingol nsp_conn name_root end;
 
@@ -142,7 +143,7 @@
   let
     val name_root = "Generated";
     val nsp_conn = [
-      [nsp_class, nsp_eq_class], [nsp_type], [nsp_const, nsp_eq], [nsp_inst], [nsp_mem]
+      [nsp_class, nsp_eq_class], [nsp_type], [nsp_const, nsp_mem, nsp_eq], [nsp_dtcon], [nsp_inst]
     ];
   in CodegenSerializer.haskell_from_thingol nsp_conn name_root end;
 
@@ -756,13 +757,21 @@
 fun defgen_clsdecl thy defs cls trns =
   case name_of_idf thy nsp_class cls
    of SOME cls =>
-        trns
-        |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls)
-        |> fold_map (ensure_def_class thy defs)
-             (map (idf_of_name thy nsp_class) (ClassPackage.get_superclasses thy cls))
-        |-> (fn supcls => succeed (Class (supcls, "a", [], []),
-             map (idf_of_name thy nsp_mem) (ClassPackage.the_consts thy cls)
-             @ map (curry (idf_of_inst thy defs) cls) ((map fst o ClassPackage.the_tycos thy) cls)))
+        let
+          val memnames = ClassPackage.the_consts thy cls;
+          val memtypes = map (devarify_type o ClassPackage.get_const_sign thy "'a") memnames;
+          val memctxt = map (ClassPackage.extract_sortctxt thy) memtypes;
+          val memidfs = map (idf_of_name thy nsp_mem) memnames;
+          val instnames = map (curry (idf_of_inst thy defs) cls) ((map fst o ClassPackage.the_tycos thy) cls);
+        in
+          trns
+          |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls)
+          |> fold_map (ensure_def_class thy defs)
+               (map (idf_of_name thy nsp_class) (ClassPackage.get_superclasses thy cls))
+          ||>> fold_map (invoke_cg_type thy defs) memtypes
+          |-> (fn (supcls, memtypes) => succeed (Class (supcls, "a", memidfs ~~ (memctxt ~~ memtypes), []),
+                 memidfs @ instnames))
+        end
     | _ =>
         trns
         |> fail ("no class definition found for " ^ quote cls);
@@ -773,8 +782,7 @@
         trns
         |> debug 5 (fn _ => "trying defgen class member for " ^ quote f)
         |> ensure_def_class thy defs (idf_of_name thy nsp_class ((the o ClassPackage.lookup_const_class thy) clsmem))
-        ||>> (invoke_cg_type thy defs o devarify_type) (ClassPackage.get_const_sign thy "'a" clsmem)
-        |-> (fn (cls, ty) => succeed (Classmember (cls, "a", ty), []))
+        |-> (fn cls => succeed (Classmember cls, []))
     | _ =>
         trns |> fail ("no class member found for " ^ quote f)
 
@@ -794,9 +802,9 @@
             (ClassPackage.get_inst_consts_sign thy (tyco, cls));
           val _ = debug 10 (fn _ => "(4) CLSINST " ^ cls ^ " - " ^ tyco) ()
           fun add_vars arity clsmems (trns as (_, modl)) =
-            ((Term.invent_names
-              (map ((fn Classmember (_, _, ty) => ty) o get_def modl)
-              clsmems |> tvars_of_itypes) "a" (length arity) ~~ arity, clsmems), trns)
+            case get_def modl (idf_of_name thy nsp_class cls)
+             of Class (_, _, members, _) => ((Term.invent_names
+              (tvars_of_itypes ((map (snd o snd)) members)) "a" (length arity) ~~ arity, clsmems), trns)
           val _ = debug 10 (fn _ => "(5) CLSINST " ^ cls ^ " - " ^ tyco) ()
         in
           trns
@@ -948,25 +956,33 @@
 
 in
 
-fun defgen_datatype get_datatype get_datacons thy defs tyco trns =
-  case tname_of_idf thy tyco
-   of SOME dtname =>
-        (case get_datatype thy dtname
-         of SOME (vs, cnames) =>
-              trns
-              |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtname)
-              |> succeed (Datatype (map (rpair [] o unprefix "'") vs, [], []),
-                   cnames
-                   |> map (idf_of_name thy nsp_const)
-                   |> map (fn "0" => "const.Zero" | c => c)
-                   (* |> add_eqinst get_datacons thy (snd trns) dtname cnames *))
-              (*! VARIABLEN, EQTYPE !*)
+fun defgen_datatype get_datatype get_datacons thy defs idf trns =
+  case tname_of_idf thy idf
+   of SOME dtco =>
+        (case get_datatype thy dtco
+         of SOME (vars, cos) =>
+              let
+                val cotys = map (the o get_datacons thy o rpair dtco) cos;
+                val coidfs = cos
+                  |> map (idf_of_name thy nsp_const)
+                  |> map (fn "0" => "const.Zero" | c => c);
+              in
+                trns
+                |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco)
+                |> fold_map (invoke_cg_sort thy defs) (map snd vars)
+                ||>> (fold_map o fold_map) (invoke_cg_type thy defs o devarify_type) cotys
+                |-> (fn (sorts, tys) => succeed (Datatype
+                     (map2 (fn (v, _) => fn sort => (unprefix "'" v, sort)) vars sorts, coidfs ~~ tys, []),
+                     coidfs
+                     (* |> add_eqinst get_datacons thy (snd trns) dtname cnames *)))
+                (*! VARIABLEN, EQTYPE !*)
+              end
           | NONE =>
               trns
-              |> fail ("no datatype found for " ^ quote tyco))
+              |> fail ("no datatype found for " ^ quote dtco))
     | NONE =>
         trns
-        |> fail ("not a type constructor: " ^ quote tyco)
+        |> fail ("not a type constructor: " ^ quote idf)
   end;
 
 end; (* local *)
@@ -984,12 +1000,11 @@
           (case the_type c
             of SOME dtname =>
                  (case get_datacons thy (c, dtname)
-                   of SOME tyargs =>
+                   of SOME _ =>
                        trns
                        |> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote c)
                        |> ensure_def_tyco thy defs (idf_of_tname thy dtname)
-                       ||>> fold_map (invoke_cg_type thy defs o devarify_type) tyargs
-                       |-> (fn (dtname, tys) => succeed (Datatypecons (dtname, tys), []))
+                       |-> (fn dtname => succeed (Datatypecons dtname, []))
                     | NONE =>
                        trns
                        |> fail ("no datatype constructor found for " ^ quote f))
@@ -1025,11 +1040,12 @@
   case name_of_idf thy nsp_eq_class f
    of SOME dtname =>
         (case get_datatype thy dtname
-         of SOME (vs, _) =>
+         of SOME (vars, _) =>
               trns
               |> debug 5 (fn _ => "trying defgen datatype_eqinst for " ^ quote dtname)
               |> ensure_def_const thy defs (idf_of_name thy nsp_eq dtname)
-              |-> (fn pred_eq => succeed (Classinst (class_eq, (dtname, vs ~~ replicate (length vs) [class_eq]), [(fun_eq, pred_eq)]), []))
+              |-> (fn pred_eq => succeed (Classinst (class_eq, (dtname,
+                    map (fn (v, _) => (v, [class_eq])) vars), [(fun_eq, pred_eq)]), []))
           | NONE =>
               trns
               |> fail ("no datatype found for " ^ quote dtname))
@@ -1348,8 +1364,8 @@
 
 val (classK, generateK, serializeK, syntax_tycoK, syntax_constK, aliasK) =
   ("code_class", "code_generate", "code_serialize", "code_syntax_tyco", "code_syntax_const", "code_alias");
-val (extractingK, definedK, dependingK) =
-  ("extracting", "defined_by", "depending_on");
+val (constantsK, definedK, dependingK) =
+  ("constants", "defined_by", "depending_on");
 
 val classP =
   OuterSyntax.command classK "codegen data for classes" K.thy_decl (
@@ -1371,7 +1387,7 @@
     P.name
     -- P.name
     -- Scan.option (
-         P.$$$ extractingK
+         P.$$$ constantsK
          |-- Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ))
        )
     >> (fn ((serial_name, filename), consts) =>
@@ -1420,7 +1436,7 @@
   );
 
 val _ = OuterSyntax.add_parsers [classP, generateP, serializeP, aliasP, syntax_tycoP, syntax_constP];
-val _ = OuterSyntax.add_keywords ["\\<Rightarrow>", "=>", extractingK, definedK, dependingK];
+val _ = OuterSyntax.add_keywords ["\\<Rightarrow>", "=>", constantsK, definedK, dependingK];
 
 
 (* setup *)
--- a/src/Pure/Tools/codegen_serializer.ML	Fri Dec 09 15:25:29 2005 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Fri Dec 09 15:25:52 2005 +0100
@@ -138,77 +138,6 @@
   in NameSpace.pack (pr @ [String.implode (Char.toLower c :: cs)]) end;
 
 
-(** grouping functions **)
-
-fun group_datatypes one_arg defs =
-  let
-    fun check_typ_dup dtname ts =
-      if AList.defined (op =) ts dtname
-      then error ("double datatype definition: " ^ quote dtname)
-      else ts
-    fun check_typ_miss dtname ts =
-      if AList.defined (op =) ts dtname
-      then ts
-      else error ("missing datatype definition: " ^ quote dtname)
-    fun group (name, Datatype (vs, _, _)) ts =
-          (if one_arg
-           then map (fn (_, []) => () | _ => error "can't serialize sort constrained datatype declaration to ML") vs
-           else [];
-          ts
-          |> apsnd (check_typ_dup name)
-          |> apsnd (AList.update (op =) (name, (vs, []))))
-      | group (name, Datatypecons (dtname, tys as _::_::_)) ts =
-          if one_arg
-          then error ("datatype constructor containing more than one parameter")
-          else
-            ts
-            |> apfst (AList.default (op =) (NameSpace.base dtname, []))
-            |> apfst (AList.map_entry (op =) (NameSpace.base dtname) (cons (name, tys)))
-      | group (name, Datatypecons (dtname, tys)) ts =
-          ts
-          |> apfst (AList.default (op =) (NameSpace.base dtname, []))
-          |> apfst (AList.map_entry (op =) (NameSpace.base dtname) (cons (name, tys)))
-      | group _ _ =
-          error ("Datatype block containing other statements than datatype or constructor definitions")
-    fun group_cons (dtname, co) ts =
-      ts
-      |> check_typ_miss dtname
-      |> AList.map_entry (op =) dtname (rpair co o fst)
-  in
-    ([], [])
-    |> fold group defs
-    |-> (fn cons => fold group_cons cons)
-  end;
-
-fun group_classes defs =
-  let
-    fun check_class_dup clsname ts =
-      if AList.defined (op =) ts clsname
-      then error ("double class definition: " ^ quote clsname)
-      else ts
-    fun check_clsname_miss clsname ts =
-      if AList.defined (op =) ts clsname
-      then ts
-      else error ("missing class definition: " ^ quote clsname)
-    fun group (name, Class (supercls, v, _, _)) ts =
-          ts
-          |> apsnd (check_class_dup name)
-          |> apsnd (AList.update (op =) (name, ((supercls, v), [])))
-      | group (name, Classmember (clsname, _, ty)) ts =
-          ts
-          |> apfst (AList.default (op =) (NameSpace.base clsname, []))
-          |> apfst (AList.map_entry (op =) (NameSpace.base clsname) (cons (name, ty)))
-      | group _ _ =
-          error ("Datatype block containing other statements than datatype or constructor definitions")
-    fun group_members (clsname, member) ts =
-      ts
-      |> check_clsname_miss clsname
-      |> AList.map_entry (op =) clsname (rpair member o fst)
-  in
-    ([], [])
-    |> fold group defs
-    |-> (fn members => fold group_members members)
-  end;
 
 (** ML serializer **)
 
@@ -222,7 +151,7 @@
       in
         Pretty.chunks (p_init @ [Pretty.block ([p_last, Pretty.str ";"])])
     end;
-    val ml_label_uniq = translate_string (fn "'" => "''" | "." => "'" | c => c);
+    val ml_label_uniq = translate_string (fn "_" => "__" | "." => "_" | c => c);
     fun ml_from_type br (IType ("Pair", [t1, t2])) =
           brackify (eval_br_postfix br (INFX (2, L))) [
             ml_from_type (INFX (2, X)) t1,
@@ -260,7 +189,7 @@
       | ml_from_type _ (IVarT (_, sort)) =
           "cannot serialize sort constrained type variable to ML: " ^ commas sort |> error
       | ml_from_type _ (IDictT fs) =
-          (Pretty.enclose "{" "}" o Pretty.breaks) (
+          Pretty.gen_list "," "{" "}" (
             map (fn (f, ty) =>
               Pretty.block [Pretty.str (ml_label_uniq f ^ ": "), ml_from_type NOBR ty]) fs
           );
@@ -382,18 +311,26 @@
       | ml_from_expr br (IInst _) =
           error "cannot serialize poly instant to ML"
       | ml_from_expr br (IDictE fs) =
-          (Pretty.enclose "{" "}" o Pretty.breaks) (
+          Pretty.gen_list "," "{" "}" (
             map (fn (f, e) =>
               Pretty.block [Pretty.str (ml_label_uniq f ^ " = "), ml_from_expr NOBR e]) fs
           )
+      | ml_from_expr br (ILookup ([], v)) =
+          Pretty.str v
+      | ml_from_expr br (ILookup ([l], v)) =
+          brackify (eval_br br BR) [
+            Pretty.str ("#" ^ (ml_label_uniq l)),
+            Pretty.str v
+          ]
       | ml_from_expr br (ILookup (ls, v)) =
           brackify (eval_br br BR) [
-            Pretty.str "(",
-            ls |> map ((fn s => "#" ^ s) o ml_label_uniq) |> foldr1 (fn (l, e) => l ^ " o " ^ e) |> Pretty.str,
-            Pretty.str ")",
-            Pretty.str " ",
+            Pretty.str ("("
+              ^ (ls |> map ((fn s => "#" ^ s) o ml_label_uniq) |> foldr1 (fn (l, e) => l ^ " o " ^ e))
+              ^ ")"),
             Pretty.str v
           ]
+      | ml_from_expr _ e =
+          error ("dubious expression: " ^ (Pretty.output o pretty_iexpr) e)
     and mk_app_p br p args =
       brackify (eval_br br BR)
         (p :: map (ml_from_expr BR) args)
@@ -504,74 +441,78 @@
         fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (_, ty))) =
           let
             val (pats_hd::pats_tl) = (fst o split_list) eqs;
-            val _ = fold (fn x => fn y => (x ~~ y; y)) pats_tl pats_hd;
-              (*check for equal length of argument lists*)
             val shift = if null eq_tl then I else map (Pretty.block o single);
           in (Pretty.block o Pretty.fbreaks o shift) (
                mk_eq definer f ty eq
                :: map (mk_eq "|" f ty) eq_tl
              )
-          end
+          end;
       in
         chunk_defs (
           mk_fun definer d
           :: map (mk_fun "and") ds_tl
-        )
+        ) |> SOME
       end;
     fun ml_from_datatypes defs =
       let
-        fun mk_datatypes (ds as d::ds_tl) =
-          let
-            fun praetify [] f = [f]
-              | praetify [p] f = [f, Pretty.str " of ", p]
-            fun mk_cons (co, typs) =
-              (Pretty.block oo praetify)
-                (map (ml_from_type NOBR) typs)
-                (Pretty.str (resolv co))
-            fun mk_datatype definer (t, (vs, cs)) =
-              Pretty.block (
-                [Pretty.str definer]
-                @ postify (map (ml_from_type BR o IVarT) vs)
-                    (Pretty.str (resolv t))
-                @ [Pretty.str " =",
-                  Pretty.brk 1]
-                @ separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons cs)
-              )
-          in
+        val defs' = List.mapPartial
+          (fn (name, Datatype info) => SOME (name, info)
+            | (name, Datatypecons _) => NONE
+            | (name, def) => error ("datatype block containing illegal def: " ^ (Pretty.output o pretty_def) def)
+          ) ds
+        fun praetify [] f = [f]
+          | praetify [p] f = [f, Pretty.str " of ", p]
+        fun mk_cons (co, typs) =
+          (Pretty.block oo praetify)
+            (map (ml_from_type NOBR) typs)
+            (Pretty.str (resolv co))
+        fun mk_datatype definer (t, (vs, cs, _)) =
+          Pretty.block (
+            [Pretty.str definer]
+            @ postify (map (ml_from_type BR o IVarT) vs)
+                (Pretty.str (resolv t))
+            @ [Pretty.str " =",
+              Pretty.brk 1]
+            @ separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons cs)
+          )
+      in
+        case defs'
+         of d::ds_tl =>
             chunk_defs (
               mk_datatype "datatype " d
               :: map (mk_datatype "and ") ds_tl
-            )
-          end;
-      in
-        (mk_datatypes o group_datatypes true) defs
+            ) |> SOME
+          | _ => NONE
       end;
-    fun ml_from_def (name, Typesyn (vs, ty)) =
-        (map (fn (vname, []) => () | _ => error "can't serialize sort constrained type declaration to ML") vs;
-         Pretty.block (
-          Pretty.str "type "
-          :: postify (map (Pretty.str o fst) vs) (Pretty.str name)
-          @ [Pretty.str " =",
-          Pretty.brk 1,
-          ml_from_type NOBR ty,
-          Pretty.str ";"
-        ]))
-      | ml_from_def (name, Nop) =
+    fun ml_from_def (name, Nop) =
           if exists (fn query => query name)
             [(fn name => (is_some o tyco_syntax) name),
              (fn name => (is_some o const_syntax) name)]
-          then Pretty.str ""
+          then NONE
           else error ("empty statement during serialization: " ^ quote name)
+      | ml_from_def (name, Typesyn (vs, ty)) =
+        (map (fn (vname, []) => () | _ => error "can't serialize sort constrained type declaration to ML") vs;
+          Pretty.block (
+            Pretty.str "type "
+            :: postify (map (ml_from_type BR o IVarT) vs) (Pretty.str name)
+            @ [Pretty.str " =",
+            Pretty.brk 1,
+            ml_from_type NOBR ty,
+            Pretty.str ";"
+            ]
+          )) |> SOME
       | ml_from_def (name, Class _) =
           error ("can't serialize class declaration " ^ quote name ^ " to ML")
+      | ml_from_def (_, Classmember _) =
+          NONE
       | ml_from_def (name, Classinst _) =
           error ("can't serialize instance declaration " ^ quote name ^ " to ML")
-  in (debug 10 (fn _ => "******************") (); (*map (writeln o Pretty.o)*)
-  case (snd o hd) ds
-   of Fun _ => ml_from_funs ds
-    | Datatypecons _ => ml_from_datatypes ds
-    | Datatype _ => ml_from_datatypes ds
-    | _ => (case ds of [d] => ml_from_def d))
+  in (debug 10 (fn _ => "*** defs " ^ commas (map fst ds)) ();
+  case ds
+   of (_, Fun _)::_ => ml_from_funs ds
+    | (_, Datatypecons _)::_ => ml_from_datatypes ds
+    | (_, Datatype _)::_ => ml_from_datatypes ds
+    | [d] => ml_from_def d)
   end;
 
 in
@@ -619,8 +560,11 @@
       | eta_expander s =
           if NameSpace.is_qualified s
           then case get_def module s
-            of Datatypecons (_ , tys) =>
-                if length tys >= 2 then length tys else 0
+            of Datatypecons dtname =>
+                (case get_def module dtname
+                  of Datatype (_, cs, _) =>
+                    let val l = AList.lookup (op =) cs s |> the |> length
+                    in if l >= 2 then l else 0 end)
              | _ =>
                 const_syntax s
                 |> Option.map fst
@@ -629,19 +573,17 @@
   in
     module
     |> debug 12 (Pretty.output o pretty_module)
-    |> debug 3 (fn _ => "connecting datatypes and classdecls...")
-    |> connect_datatypes_clsdecls
     |> debug 3 (fn _ => "selecting submodule...")
     |> (if is_some select then (partof o the) select else I)
     |> debug 3 (fn _ => "eta-expanding...")
     |> eta_expand eta_expander
     |> debug 3 (fn _ => "eta-expanding polydefs...")
     |> eta_expand_poly
-    |> debug 12 (Pretty.output o pretty_module)
     |> debug 3 (fn _ => "tupelizing datatypes...")
     |> tupelize_cons
     |> debug 3 (fn _ => "eliminating classes...")
     |> eliminate_classes
+    |> debug 12 (Pretty.output o pretty_module)
     |> debug 3 (fn _ => "generating...")
     |> serialize (ml_from_defs tyco_syntax const_syntax) ml_from_module ml_validator nspgrp name_root
     |> (fn p => Pretty.chunks [setmp print_mode [] (Pretty.str o mk_prims) prims, p])
@@ -934,51 +876,11 @@
           ]
       | haskell_from_binop br pr ass f args =
           mk_app_p br (Pretty.str ("(" ^ f ^ ")")) args
-    fun haskell_from_datatypes defs =
-      let
-        fun mk_cons (co, typs) =
-            (Pretty.block o Pretty.breaks) (
-              Pretty.str ((upper_first o resolv) co)
-              :: map (haskell_from_type NOBR) typs
-            )
-        fun mk_datatype (t, (vs, cs)) =
-          Pretty.block (
-            Pretty.str "data "
-            :: haskell_from_sctxt vs
-            :: Pretty.str (upper_first t)
-            :: Pretty.block (map (fn (v, _) => Pretty.str (" " ^ (lower_first) v)) vs)
-            :: Pretty.str " ="
-            :: Pretty.brk 1
-            :: separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons cs)
-          )
-      in
-        Pretty.chunks ((separate (Pretty.str "") o map mk_datatype o group_datatypes false) defs)
-      end;
-    fun haskell_from_classes defs =
-      let
-        fun mk_member (f, ty) =
-          Pretty.block [
-            Pretty.str (f ^ " ::"),
-            Pretty.brk 1,
-            haskell_from_type NOBR ty
-          ];
-        fun mk_class (clsname, ((supclsnames, v), members)) =
-          Pretty.block [
-            Pretty.str "class ",
-            haskell_from_sctxt (map (fn class => (v, [class])) supclsnames),
-            Pretty.str ((upper_first clsname) ^ " " ^ v),
-            Pretty.str " where",
-            Pretty.fbrk,
-            Pretty.chunks (map mk_member members)
-          ];
-      in
-        Pretty.chunks ((separate (Pretty.str "") o map mk_class o group_classes) defs)
-      end;
     fun haskell_from_def (name, Nop) =
           if exists (fn query => query name)
             [(fn name => (is_some o tyco_syntax) name),
              (fn name => (is_some o const_syntax) name)]
-          then Pretty.str ""
+          then NONE
           else error ("empty statement during serialization: " ^ quote name)
       | haskell_from_def (name, Fun (eqs, (_, ty))) =
           let
@@ -999,7 +901,7 @@
                 haskell_from_type NOBR ty
               ],
               Pretty.chunks (map (from_eq name) eqs)
-            ]
+            ] |> SOME
           end
       | haskell_from_def (name, Typesyn (vs, ty)) =
           Pretty.block [
@@ -1010,7 +912,47 @@
             Pretty.str " =",
             Pretty.brk 1,
             haskell_from_type NOBR ty
-          ]
+          ] |> SOME
+      | haskell_from_def (name, Datatype (vars, constrs, _)) =
+          let
+            fun mk_cons (co, tys) =
+              (Pretty.block o Pretty.breaks) (
+                Pretty.str ((upper_first o resolv) co)
+                :: map (haskell_from_type NOBR) tys
+              )
+          in
+            Pretty.block (
+              Pretty.str "data "
+              :: haskell_from_sctxt vars
+              :: Pretty.str (upper_first name)
+              :: Pretty.block (map (fn (v, _) => Pretty.str (" " ^ (lower_first) v)) vars)
+              :: Pretty.str " ="
+              :: Pretty.brk 1
+              :: separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons constrs)
+            )
+          end |> SOME
+      | haskell_from_def (_, Datatypecons _) =
+          NONE
+      | haskell_from_def (name, Class (supclasss, v, membrs, _)) =
+          let
+            fun mk_member (m, (_, ty)) =
+              Pretty.block [
+                Pretty.str (resolv m ^ " ::"),
+                Pretty.brk 1,
+                haskell_from_type NOBR ty
+              ]
+          in
+            Pretty.block [
+              Pretty.str "class ",
+              haskell_from_sctxt (map (fn class => (v, [class])) supclasss),
+              Pretty.str ((upper_first name) ^ " " ^ v),
+              Pretty.str " where",
+              Pretty.fbrk,
+              Pretty.chunks (map mk_member membrs)
+            ] |> SOME
+          end
+      | haskell_from_def (name, Classmember _) =
+          NONE
       | haskell_from_def (_, Classinst (clsname, (tyco, arity), instmems)) = 
           Pretty.block [
             Pretty.str "instance ",
@@ -1023,13 +965,11 @@
             Pretty.chunks (map (fn (member, const) =>
               Pretty.str ((lower_first o resolv) member ^ " = " ^ (lower_first o resolv) const)
             ) instmems)
-          ];
-  in case (snd o hd) defs
-   of Datatypecons _ => haskell_from_datatypes defs
-    | Datatype _ => haskell_from_datatypes defs
-    | Class _ => haskell_from_classes defs
-    | Classmember _ => haskell_from_classes defs
-    | _ => Pretty.block (map haskell_from_def defs |> separate (Pretty.str ""))
+          ] |> SOME
+  in
+    case List.mapPartial (fn (name, def) => haskell_from_def (name, def)) defs
+     of [] => NONE
+      | l => (SOME o Pretty.block) l
   end;
 
 in
@@ -1066,8 +1006,11 @@
       | eta_expander s =
           if NameSpace.is_qualified s
           then case get_def module s
-            of Datatypecons (_ , tys) =>
-                if length tys >= 2 then length tys else 0
+            of Datatypecons dtname =>
+                (case get_def module dtname
+                  of Datatype (_, cs, _) =>
+                    let val l = AList.lookup (op =) cs s |> the |> length
+                    in if l >= 2 then l else 0 end)
              | _ =>
                 const_syntax s
                 |> Option.map fst
@@ -1081,8 +1024,6 @@
   in
     module
     |> debug 12 (Pretty.output o pretty_module)
-    |> debug 3 (fn _ => "connecting datatypes and classdecls...")
-    |> connect_datatypes_clsdecls
     |> debug 3 (fn _ => "selecting submodule...")
     |> (if is_some select then (partof o the) select else I)
     |> debug 3 (fn _ => "eta-expanding...")
--- a/src/Pure/Tools/codegen_thingol.ML	Fri Dec 09 15:25:29 2005 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Fri Dec 09 15:25:52 2005 +0100
@@ -1,4 +1,4 @@
- (*  Title:      Pure/Tools/codegen_thingol.ML
+(*  Title:      Pure/Tools/codegen_thingol.ML
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
@@ -48,10 +48,10 @@
       Nop
     | Fun of (ipat list * iexpr) list * (ClassPackage.sortcontext * itype)
     | Typesyn of (vname * string list) list * itype
-    | Datatype of (vname * string list) list * string list * string list
-    | Datatypecons of string * itype list
-    | Class of class list * vname * string list * string list
-    | Classmember of class * vname * itype
+    | Datatype of (vname * string list) list * (string * itype list) list * string list
+    | Datatypecons of string
+    | Class of class list * vname * (string * (ClassPackage.sortcontext * itype)) list * string list
+    | Classmember of class
     | Classinst of class * (string * (vname * string list) list) * (string * string) list;
   type module;
   type transact;
@@ -111,7 +111,6 @@
   val extract_defs: iexpr -> string list;
   val eta_expand: (string -> int) -> module -> module;
   val eta_expand_poly: module -> module;
-  val connect_datatypes_clsdecls: module -> module;
   val tupelize_cons: module -> module;
   val eliminate_classes: module -> module;
 
@@ -120,7 +119,7 @@
   val soft_exc: bool ref;
 
   val serialize:
-    ((string -> string) -> (string * def) list -> Pretty.T)
+    ((string -> string) -> (string * def) list -> Pretty.T option)
     -> (string * Pretty.T list -> Pretty.T)
     -> (string -> string option)
     -> string list list -> string -> module -> Pretty.T
@@ -212,6 +211,30 @@
   | IDictE of (string * iexpr) list
   | ILookup of (string list * vname);
 
+(*
+  variable naming conventions
+
+  bare names:
+    variable names          v
+    class names             cls
+    type constructor names  tyco
+    datatype names          dtco
+    const names (general)   c
+    constructor names       co
+    class member names      m
+    arbitrary name          s
+
+  constructs:
+    sort                    sort
+    type                    ty
+    expression              e
+    pattern                 p
+    instance (cls, tyco)    inst
+    variable (v, ty)        var
+    class member (m, ty)    membr
+    constructors (co, tys)  constr
+ *)
+
 val mk_funs = Library.foldr IFun;
 val mk_apps = Library.foldl IApp;
 val mk_abss = Library.foldr IAbs;
@@ -266,7 +289,8 @@
       e
   | map_iexpr f_itype f_ipat f_iexpr (IDictE ms) =
       IDictE (map (apsnd f_iexpr) ms)
-  | map_iexpr _ _ _ (ILookup _) = error "ILOOKUP";
+  | map_iexpr _ _ _ (e as ILookup _) =
+      e ;
 
 fun fold_itype f_itype (IFun (t1, t2)) =
       f_itype t1 #> f_itype t2
@@ -363,8 +387,8 @@
       ]
   | pretty_iexpr (IDictE _) =
       Pretty.str "<DictE>"
-  | pretty_iexpr (ILookup _) =
-      Pretty.str "<Lookup>";
+  | pretty_iexpr (ILookup (ls, v)) =
+      Pretty.str ("<Lookup: " ^ commas ls ^ " in " ^ v ^ ">");
 
 
 (* language auxiliary *)
@@ -383,13 +407,19 @@
   | itype_of_iexpr (ICase ((_, [(_, e)]))) = itype_of_iexpr e;
 
 fun itype_of_ipat (ICons (_, ty)) = ty
-  | itype_of_ipat (IVarP (_, ty)) = ty
+  | itype_of_ipat (IVarP (_, ty)) = ty;
 
 fun ipat_of_iexpr (IConst (f, ty)) = ICons ((f, []), ty)
   | ipat_of_iexpr (IVarE v) = IVarP v
   | ipat_of_iexpr (e as IApp _) =
-      case unfold_app e of (IConst (f, ty), es) =>
-        ICons ((f, map ipat_of_iexpr es), (snd o unfold_fun) ty);
+      (case unfold_app e
+        of (IConst (f, ty), es) =>
+              ICons ((f, map ipat_of_iexpr es), (snd o unfold_fun) ty)
+         | (IInst (IConst (f, ty), _), es) =>
+              ICons ((f, map ipat_of_iexpr es), (snd o unfold_fun) ty)
+         | _ => error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e))
+  | ipat_of_iexpr e =
+      error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e);
 
 fun tvars_of_itypes tys =
   let
@@ -427,6 +457,8 @@
           vars e
       | vars (IDictE ms) =
           fold (vars o snd) ms
+      | vars (ILookup (_, v)) =
+          cons v
   in fold vars es [] end;
 
 fun instant_itype (v, sty) ty =
@@ -449,10 +481,10 @@
     Nop
   | Fun of (ipat list * iexpr) list * (ClassPackage.sortcontext * itype)
   | Typesyn of (vname * string list) list * itype
-  | Datatype of (vname * string list) list * string list * string list
-  | Datatypecons of string * itype list
-  | Class of class list * vname * string list * string list
-  | Classmember of class * vname * itype
+  | Datatype of (vname * string list) list * (string * itype list) list * string list
+  | Datatypecons of string
+  | Class of class list * vname * (string * (ClassPackage.sortcontext * itype)) list * string list
+  | Classmember of class
   | Classinst of class * (string * (vname * string list) list) * (string * string) list;
 
 datatype node = Def of def | Module of node Graph.T;
@@ -492,25 +524,24 @@
       Pretty.block [
         Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
         Pretty.str " |=> ",
-        Pretty.gen_list " |" "" "" (map Pretty.str cs),
+        Pretty.gen_list " |" "" ""
+          (map (fn (c, tys) => (Pretty.block o Pretty.breaks) (Pretty.str c :: map pretty_itype tys)) cs),
         Pretty.str ", instances ",
         Pretty.gen_list "," "[" "]" (map Pretty.str insts)
       ]
-  | pretty_def (Datatypecons (dtname, tys)) =
+  | pretty_def (Datatypecons dtname) =
+      Pretty.str ("cons " ^ dtname)
+  | pretty_def (Class (supcls, v, mems, insts)) =
       Pretty.block [
-        Pretty.str "cons ",
-        Pretty.gen_list " ->" "" "" (map pretty_itype tys @ [Pretty.str dtname])
-      ]
-  | pretty_def (Class (supcls, _, mems, insts)) =
-      Pretty.block [
-        Pretty.str "class extending ",
+        Pretty.str ("class var " ^ v ^ "extending "),
         Pretty.gen_list "," "[" "]" (map Pretty.str supcls),
         Pretty.str " with ",
-        Pretty.gen_list "," "[" "]" (map Pretty.str mems),
+        Pretty.gen_list "," "[" "]"
+          (map (fn (m, (_, ty)) => Pretty.block [Pretty.str (m ^ "::"), pretty_itype ty]) mems),
         Pretty.str " instances ",
         Pretty.gen_list "," "[" "]" (map Pretty.str insts)
       ]
-  | pretty_def (Classmember (clsname, v, ty)) =
+  | pretty_def (Classmember clsname) =
       Pretty.block [
         Pretty.str "class member belonging to ",
         Pretty.str clsname
@@ -543,12 +574,21 @@
 fun pretty_deps modl =
   let
     fun one_node key =
-      (Pretty.block o Pretty.fbreaks) (
-        Pretty.str key
-        :: (map (fn s => Pretty.str ("<- " ^ s)) o Graph.imm_preds modl) key
-        @ (map (fn s => Pretty.str ("-> " ^ s)) o Graph.imm_succs modl) key
-        @ (the_list oo Option.mapPartial) ((fn Module modl' => SOME (pretty_deps modl') | _ => NONE) o Graph.get_node modl) (SOME key)
-      );
+      let
+        val preds_ = Graph.imm_preds modl key;
+        val succs_ = Graph.imm_succs modl key;
+        val mutbs = gen_inter (op =) (preds_, succs_);
+        val preds = fold (remove (op =)) mutbs preds_;
+        val succs = fold (remove (op =)) mutbs succs_;
+      in
+        (Pretty.block o Pretty.fbreaks) (
+          Pretty.str key
+          :: map (fn s => Pretty.str ("<-> " ^ s)) mutbs
+          @ map (fn s => Pretty.str ("<-- " ^ s)) preds
+          @ map (fn s => Pretty.str ("--> " ^ s)) succs
+          @ (the_list oo Option.mapPartial) ((fn Module modl' => SOME (pretty_deps modl') | _ => NONE) o Graph.get_node modl) (SOME key)
+        )
+      end
   in
     modl
     |> Graph.strong_conn
@@ -697,7 +737,7 @@
     |> dest_modl
   end;
 
-fun add_check_transform (name, (Datatypecons (dtname, _))) =
+fun (*add_check_transform (name, (Datatypecons dtname)) =
       (debug 7 (fn _ => "transformation for datatype constructor " ^ quote name
         ^ " of datatype " ^ quote dtname) ();
       ([([dtname],
@@ -733,11 +773,11 @@
               | def => "attempted to add class member to non-class"
                  ^ (Pretty.output o pretty_def) def |> error)])
       end
-  | add_check_transform (name, Classinst (clsname, (tyco, arity), memdefs)) =
+  | *) add_check_transform (name, Classinst (clsname, (tyco, arity), memdefs)) =
       let
         val _ = debug 7 (fn _ => "transformation for class instance " ^ quote tyco
           ^ " of class " ^ quote clsname) ();
-        fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] =
+        (* fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] =
               let
                 val mtyp_i' = instant_itype (v, tyco `%% map IVarT arity) mtyp_c;
               in if eq_itype (mtyp_i', mtyp_i)
@@ -748,9 +788,9 @@
               end
           | check defs =
               "non-well-formed definitions encountered for classmembers: "
-              ^ (commas o map (quote o Pretty.output o pretty_def)) defs |> SOME
+              ^ (commas o map (quote o Pretty.output o pretty_def)) defs |> SOME *)
       in
-        (map (fn (memname, memprim) => ([memname, memprim], check)) memdefs,
+        ((* map (fn (memname, memprim) => ([memname, memprim], check)) memdefs*) [],
           [(clsname,
               fn Class (supcs, v, mems, insts) => Class (supcs, v, mems, name::insts)
                | def => "attempted to add class instance to non-class"
@@ -763,6 +803,13 @@
       end
   | add_check_transform _ = ([], []);
 
+(* checks to be implemented here lateron:
+    - well-formedness of function equations
+    - only possible to add defined constructors and class members
+    - right type abstraction with class members
+    - correct typing of instance definitions
+*)
+
 fun succeed some = pair (Succeed some);
 fun fail msg = pair (Fail ([msg], NONE));
 
@@ -945,21 +992,19 @@
 val Fun_le = IConst (fun_le, Type_integer `-> Type_integer `-> Type_bool);
 val Fun_wfrec = IConst (fun_wfrec, ((A `-> B) `-> A `-> B) `-> A `-> B);
 
-infix 7 xx;
-infix 5 **;
-infix 5 &&;
-
-fun a xx b = Type_pair a b;
-fun a ** b =
+fun foldl1 f (x::xs) =
+  Library.foldl f (x, xs);
+val ** = foldl1 (uncurry Type_pair);
+val XXp = foldl1 (fn (a, b) =>
+  let
+    val ty_a = itype_of_ipat a;
+    val ty_b = itype_of_ipat b;
+  in ICons ((cons_pair, [a, b]), Type_pair ty_a ty_b) end);
+val XXe = foldl1 (fn (a, b) =>
   let
     val ty_a = itype_of_iexpr a;
     val ty_b = itype_of_iexpr b;
-  in IConst (cons_pair, ty_a `-> ty_b `-> ty_a xx ty_b) `$ a `$ b end;
-fun a && b =
-  let
-    val ty_a = itype_of_ipat a;
-    val ty_b = itype_of_ipat b;
-  in ICons ((cons_pair, [a, b]), ty_a xx ty_b) end;
+  in IConst (cons_pair, ty_a `-> ty_b `-> Type_pair ty_a ty_b) `$ a `$ b end);
 
 end; (* local *)
 
@@ -1000,12 +1045,8 @@
 
 fun build_eqpred modl dtname =
   let
-    val cons =
-      map ((fn Datatypecons c => c) o get_def modl)
-        (case get_def modl dtname of Datatype (_, cs, _) => cs);
-    val sortctxt =
-      map (rpair [class_eq])
-        (case get_def modl dtname of Datatype (_, vs, _) => vs);
+    val (vs, cons, _) = case get_def modl dtname of Datatype info => info;
+    val sortctxt = map (rpair [class_eq] o fst) vs
     val ty = IType (dtname, map IVarT sortctxt);
     fun mk_eq (c, []) =
           ([ICons ((c, []), ty), ICons ((c, []), ty)], Cons_true)
@@ -1085,31 +1126,26 @@
       | map_def_fun def = def;
   in map_defs map_def_fun end;
 
-fun connect_datatypes_clsdecls module =
-  let
-    fun extract_dep (name, Datatypecons (dtname, _)) =
-          [(dtname, name)]
-      | extract_dep (name, Classmember (cls, _, _)) =
-          [(cls, name)]
-      | extract_dep (name, def) = []
-  in add_deps extract_dep module end;
-
 fun tupelize_cons module =
   let
-    fun replace_def (_, (def as Datatypecons (_, []))) acc =
-          (def, acc)
-      | replace_def (_, (def as Datatypecons (_, [_]))) acc =
-          (def, acc)
-      | replace_def (name, (Datatypecons (tyco, tys))) acc =
-          (Datatypecons (tyco,
-            [foldr1 (op xx) tys]), name::acc)
-      | replace_def (_, def) acc = (def, acc);
+    fun replace_cons (cons as (_, [])) =
+          pair cons
+      | replace_cons (cons as (_, [_])) =
+          pair cons
+      | replace_cons (con, tys) =
+          cons con
+          #> pair (con, [** tys])
+    fun replace_def (_, (def as Datatype (vs, cs, insts))) =
+          fold_map replace_cons cs
+          #-> (fn cs => pair (Datatype (vs, cs, insts)))
+      | replace_def (_, def) =
+          pair def
     fun replace_app cs ((f, ty), es) =
       if member (op =) cs f
       then
         let
           val (tys, ty') = unfold_fun ty
-        in IConst (f, foldr1 (op xx) tys `-> ty') `$ foldr1 (op **) es end
+        in IConst (f, ** tys `-> ty') `$ XXe es end
       else IConst (f, ty) `$$ es;
     fun replace_iexpr cs (IConst (f, ty)) =
           replace_app cs ((f, ty), [])
@@ -1120,7 +1156,7 @@
       | replace_iexpr cs e = map_iexpr I I (replace_iexpr cs) e;
     fun replace_ipat cs (p as ICons ((c, ps), ty)) =
           if member (op =) cs c then
-            ICons ((c, [(foldr1 (op &&) (map (replace_ipat cs) ps))]), ty)
+            ICons ((c, [XXp (map (replace_ipat cs) ps)]), ty)
           else map_ipat I (replace_ipat cs) p
       | replace_ipat cs p = map_ipat I (replace_ipat cs) p;
   in
@@ -1129,57 +1165,16 @@
 
 fun eliminate_classes module =
   let
-    fun mk_cls_typ_map memberdecls ty_inst =
-      map (fn (memname, (v, ty)) =>
-        (memname, ty |> instant_itype (v, ty_inst))) memberdecls;
-    fun transform_dicts (Class (supcls, v, members, _)) =
-          let
-            val memberdecls = AList.make
-              ((fn Classmember (_, v, ty) => (v, ty)) o get_def module) members;
-            val varname_cls = Term.invent_names (tvars_of_itypes (map (snd o snd) memberdecls)) "a" 1 |> hd
-          in
-            Typesyn ([(varname_cls, [])], IDictT (mk_cls_typ_map memberdecls (IVarT (varname_cls, []))))
-          end
-      | transform_dicts (Classinst (clsname, (tyco, arity), memdefs)) =
+    fun transform_itype (IVarT (v, s)) =
+          IVarT (v, [])
+      | transform_itype (ty as IDictT _) =
+          ty
+      | transform_itype ty =
+          map_itype transform_itype ty;
+    fun transform_ipat p =
+          map_ipat transform_itype transform_ipat p;
+    fun transform_iexpr vname_alist (IInst (e, ls)) =
           let
-            val Class (_, _, members, _) = get_def module clsname;
-            val memberdecls = AList.make
-              ((fn Classmember (_, v, ty) => (v, ty)) o get_def module) members;
-            val ty_arity = tyco `%% map IVarT arity;
-            val inst_typ_map = mk_cls_typ_map memberdecls ty_arity;
-            val memdefs_ty = map (fn (memname, memprim) =>
-              (memname, (memprim, (the o AList.lookup (op =) inst_typ_map) memname))) memdefs;
-          in
-            Fun ([([], IDictE (map (apsnd IConst) memdefs_ty))],
-              ([], IDictT inst_typ_map))
-          end
-      | transform_dicts d = d
-    fun transform_defs (Fun (ds, (sortctxt, ty))) =
-          let
-            val _ = writeln ("class 1");
-            val varnames_ctxt =
-              dig
-                (Term.invent_names ((vars_of_iexprs o map snd) ds @ (vars_of_ipats o Library.flat o map fst) ds) "d" o length)
-                (map snd sortctxt);
-            val _ = writeln ("class 2");
-            val vname_alist = map2 (fn (vt, sort) => fn vs => (vt, vs ~~ sort)) sortctxt varnames_ctxt;
-            val _ = writeln ("class 3");
-            fun add_typarms ty =
-              map (foldr1 (op xx) o (fn (vt, vss) => map (fn (_, cls) => cls `%% [IVarT (vt, [])]) vss)) vname_alist
-                `--> ty;
-            val _ = writeln ("class 4");
-            fun add_parms ps =
-              map (foldr1 (op &&) o (fn (vt, vss) => map (fn (v, cls) => IVarP (v, cls `%% [IVarT (vt, [])])) vss)) vname_alist
-                @ ps;
-            val _ = writeln ("class 5");
-            fun transform_itype (IVarT (v, s)) =
-                  IVarT (v, [])
-              | transform_itype ty =
-                  map_itype transform_itype ty;
-            val _ = writeln ("class 6");
-            fun transform_ipat p =
-                  map_ipat transform_itype transform_ipat p;
-            val _ = writeln ("class 7");
             fun transform_lookup (ClassPackage.Instance ((cdict, idict), ls)) =
                   ls
                   |> transform_lookups
@@ -1191,27 +1186,87 @@
                     val (v', cls) =
                       (nth o the oo AList.lookup (op =)) vname_alist v i;
                     fun mk_parm tyco = tyco `%% [IVarT (v, [])];
-                  in (mk_parm cls, ILookup (rev deriv, v')) end
+                  in (mk_parm cls, ILookup (deriv, v')) end
             and transform_lookups lss =
                   map_yield (map_yield transform_lookup
-                       #> apfst (foldr1 (op xx))
-                       #> apsnd (foldr1 (op **))) lss;
-            val _ = writeln ("class 8");
-            fun transform_iexpr (IInst (e, ls)) =
-                  (writeln "A"; transform_iexpr e `$$ (snd o transform_lookups) ls)
-              | transform_iexpr e =
-                  (writeln "B"; map_iexpr transform_itype transform_ipat transform_iexpr e);
-            fun transform_rhs (ps, rhs) =
-              (writeln ("LHS: " ^ (commas o map (Pretty.output o pretty_ipat)) ps);
-               writeln ("RHS: " ^ ((Pretty.output o pretty_iexpr) rhs));
-              (add_parms ps, writeln "---", transform_iexpr rhs) |> (fn (a, _, b) => (writeln "***"; (a, b))))
-            val _ = writeln ("class 9");
-          in Fun (map transform_rhs ds, ([], add_typarms ty)) end
-      | transform_defs d = d
+                       #> apfst **
+                       #> apsnd XXe) lss
+          in transform_iexpr vname_alist e `$$ (snd o transform_lookups) ls end
+      | transform_iexpr vname_alist e =
+          map_iexpr transform_itype transform_ipat (transform_iexpr vname_alist) e;
+    fun mk_cls_typ_map v membrs ty_inst =
+      map (fn (m, (mctxt, ty)) =>
+        (m, ty |> instant_itype (v, ty_inst))) membrs;
+    fun extract_members (cls, Class (supclss, v, membrs, _)) =
+          let
+            val ty_cls = cls `%% [IVarT (v, [])];
+            val w = "d";
+            val add_supclss = if null supclss then I else cons (v, supclss);
+            fun mk_fun (m, (mctxt, ty)) = (m, Fun ([([IVarP (w, ty_cls)], ILookup ([m], w))],
+              (add_supclss mctxt, ty `-> ty_cls)));
+          in fold (cons o mk_fun) membrs end
+      | extract_members _ = I;
+    fun introduce_dicts (Class (supcls, v, membrs, insts)) =
+          let
+            val _ = writeln "TRANSFORMING CLASS";
+            val _ = PolyML.print (Class (supcls, v, membrs, insts));
+            val varname_cls = Term.invent_names (tvars_of_itypes (map (snd o snd) membrs)) "a" 1 |> hd
+          in
+            Typesyn ([(varname_cls, supcls)], IDictT (mk_cls_typ_map v membrs (IVarT (varname_cls, []))))
+          end
+      | introduce_dicts (Classinst (clsname, (tyco, arity), memdefs)) =
+          let
+            val _ = writeln "TRANSFORMING CLASSINST";
+            val _ = PolyML.print (Classinst (clsname, (tyco, arity), memdefs));
+            val Class (_, v, members, _) = get_def module clsname;
+            val ty = tyco `%% map IVarT arity;
+            val inst_typ_map = mk_cls_typ_map v members ty;
+            val memdefs_ty = map (fn (memname, memprim) =>
+              (memname, (memprim, (the o AList.lookup (op =) inst_typ_map) memname))) memdefs;
+          in
+            Fun ([([], IDictE (map (apsnd IConst) memdefs_ty))],
+              ([], IType (clsname, [ty])))
+          end
+      | introduce_dicts d = d;
+    fun elim_sorts (Fun (eqs, ([], ty))) =
+          (writeln "TRANSFORMING FUN ()";
+          Fun (map (fn (ps, rhs) => (map transform_ipat ps, transform_iexpr [] rhs)) eqs,
+            ([], transform_itype ty)))
+      | elim_sorts (Fun (eqs, (sortctxt, ty))) =
+          let
+            val _ = writeln "TRANSFORMING FUN (1)";
+            val varnames_ctxt =
+              dig
+                (Term.invent_names ((vars_of_iexprs o map snd) eqs @
+                  (vars_of_ipats o Library.flat o map fst) eqs) "d" o length)
+                (map snd sortctxt);
+            val _ = writeln "TRANSFORMING FUN (2)";
+            val vname_alist = map2 (fn (vt, sort) => fn vs => (vt, vs ~~ sort))
+              sortctxt varnames_ctxt |> PolyML.print;
+            val _ = writeln "TRANSFORMING FUN (3)";
+            val ty' = map (op ** o (fn (vt, vss) => map (fn (_, cls) =>
+              cls `%% [IVarT (vt, [])]) vss)) vname_alist
+              `--> transform_itype ty;
+            val _ = writeln "TRANSFORMING FUN (4)";
+            val ps_add = map (XXp o (fn (vt, vss) => map (fn (v, cls) =>
+              IVarP (v, cls `%% [IVarT (vt, [])])) vss)) vname_alist;
+            val _ = writeln "TRANSFORMING FUN (5)";
+          in Fun (map (fn (ps, rhs) => (ps_add @ map transform_ipat ps, transform_iexpr vname_alist rhs)) eqs, ([], ty')) before writeln "TRANSFORMING FUN (6)" end
+      | elim_sorts (Datatype (vars, constrs, insts)) =
+          (writeln "TRANSFORMING DATATYPE (1)";
+          Datatype (map (fn (v, _) => (v, [])) vars, map (apsnd (map transform_itype)) constrs, insts)
+          before writeln "TRANSFORMING DATATYPE (2)")
+      | elim_sorts (Typesyn (vars, ty)) =
+          (writeln "TRANSFORMING TYPESYN (1)";
+          Typesyn (map (fn (v, _) => (v, [])) vars, transform_itype ty)
+          before writeln "TRANSFORMING TYPESYN (2)")
+      | elim_sorts d = d;
   in
     module
-    |> map_defs transform_dicts
-    |> map_defs transform_defs
+    |> `(fn module => fold_defs extract_members module [])
+    |-> (fn membrs => fold (fn (name, f) => map_def name (K f)) membrs)
+    |> map_defs introduce_dicts
+    |> map_defs elim_sorts
   end;
 
 
@@ -1302,16 +1357,23 @@
 
 fun serialize s_def s_module validate nspgrp name_root module =
   let
+    val _ = debug 15 (fn _ => "serialize 1") ();
     val resolvtab = mk_resolvtab nspgrp validate module;
+    val _ = debug 15 (fn _ => "serialize 2") ();
     val resolver = mk_resolv resolvtab;
+    val _ = debug 15 (fn _ => "serialize 3") ();
     fun seri prfx ([(name, Module module)]) =
+          (debug 15 (fn _ => "serializing module " ^ quote name) ();
           s_module (resolver prfx (prfx @ [name] |> NameSpace.pack),
-            (map (seri (prfx @ [name]))
-               ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)))
+            List.mapPartial (seri (prfx @ [name]))
+              ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module))
+          |> SOME)
       | seri prfx ds =
-          s_def (resolver prfx) (map (fn (name, Def def) => (resolver prfx (prfx @ [name] |> NameSpace.pack), def)) ds)
+          (debug 15 (fn _ => "serializing definitions " ^ (commas o map fst) ds) ();
+          s_def (resolver prfx) (map
+            (fn (name, Def def) => (resolver prfx (prfx @ [name] |> NameSpace.pack), def)) ds))
   in
-    setmp print_mode [] (fn _ => s_module (name_root, (map (seri [])
+    setmp print_mode [] (fn _ => s_module (name_root, (List.mapPartial (seri [])
       ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)))) ()
   end;