added haskell serializer
authorhaftmann
Tue, 29 Nov 2005 16:05:10 +0100
changeset 18282 98431741bda3
parent 18281 591e8cdea6f7
child 18283 f8a49f09a202
added haskell serializer
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_package.ML	Tue Nov 29 16:04:57 2005 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Tue Nov 29 16:05:10 2005 +0100
@@ -6,7 +6,7 @@
 intermediate language ("Thin-gol").
 *)
 
-(*NOTE: for simplifying development, this package contains
+(*NOTE: for simplifying developement, this package contains
 some stuff which will finally be moved upwards to HOL*)
 
 signature CODEGEN_PACKAGE =
@@ -120,13 +120,18 @@
 val serializer_ml =
   let
     val name_root = "Generated";
-    val nsp_conn_ml = [
+    val nsp_conn = [
       [nsp_class, nsp_type, nsp_eq_class], [nsp_const, nsp_inst, nsp_mem, nsp_eq]
     ];
-  in CodegenSerializer.ml_from_thingol nsp_conn_ml name_root end;
+  in CodegenSerializer.ml_from_thingol nsp_conn name_root end;
 
-fun serializer_hs _ _ _ _ =
-  error ("haskell serialization not implemented yet");
+val serializer_hs =
+  let
+    val name_root = "Generated";
+    val nsp_conn = [
+      [nsp_class, nsp_eq_class], [nsp_type], [nsp_const], [nsp_inst], [nsp_mem], [nsp_eq]
+    ];
+  in CodegenSerializer.haskell_from_thingol nsp_conn name_root end;
 
 
 (* theory data for codegen *)
@@ -223,7 +228,7 @@
 fun merge_serialize_data
   ({ serializer = serializer, primitives = primitives1,
      syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 },
-   { serializer = _, primitives = primitives2,
+   {serializer = _, primitives = primitives2,
      syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) =
   { serializer = serializer,
     primitives = CodegenSerializer.merge_prims (primitives1, primitives2) : CodegenSerializer.primitives,
@@ -315,7 +320,7 @@
         gens |> map_gens
           (fn (codegens_sort, codegens_type, codegens_expr, defgens) =>
             (codegens_sort, codegens_type,
-             codegens_expr
+        codegens_expr
              |> Output.update_warn (op =) ("overwriting existing expression code generator " ^ name) (name, (cg, stamp ())),
              defgens)),
              lookups, serialize_data, logic_data));
@@ -340,7 +345,7 @@
         lookups |> map_lookups
           (fn (lookups_tyco, lookups_const) =>
             (lookups_tyco |> Symtab.update_new (src, dst),
-             lookups_const)), 
+             lookups_const)),
         serialize_data, logic_data));
 
 fun add_lookup_const ((src, ty), dst) =
@@ -350,7 +355,7 @@
         lookups |> map_lookups
           (fn (lookups_tyco, lookups_const) =>
             (lookups_tyco,
-             lookups_const |> Symtab.update_multi (src, (ty, dst)))), 
+             lookups_const |> Symtab.update_multi (src, (ty, dst)))),
         serialize_data, logic_data));
 
 fun set_is_datatype f =
@@ -436,9 +441,9 @@
 
 fun cname_of_idf thy ((_, overl_rev), _, _) idf =
   case Symtab.lookup overl_rev idf
-   of NONE => 
+   of NONE =>
         (case name_of_idf thy nsp_const idf
-         of NONE => (case name_of_idf thy nsp_mem idf
+    of NONE => (case name_of_idf thy nsp_mem idf
          of NONE => NONE
           | SOME n => SOME (n, Sign.the_const_constraint thy n))
           | SOME n => SOME (n, Sign.the_const_constraint thy n))
@@ -509,7 +514,7 @@
         |> pair f
   else (f, trns);
 
-fun mk_fun thy defs eqs ty trns = 
+fun mk_fun thy defs eqs ty trns =
   let
     val sortctxt = ClassPackage.extract_sortctxt thy ty;
     fun mk_sortvar (v, sort) trns =
@@ -561,7 +566,7 @@
        (sort |> filter (ClassPackage.is_class thy) |> map (idf_of_name thy nsp_class))
   |-> (fn sort => succeed sort)
 
-fun codegen_type_default thy defs (v as TVar (_, sort)) trns =
+fun codegen_type_default thy defs(v as TVar (_, sort)) trns =
       trns
       |> invoke_cg_sort thy defs sort
       |-> (fn sort => succeed (IVarT (name_of_tvar v, sort)))
@@ -598,7 +603,7 @@
         val _ = debug 10 (fn _ => "making application (3)") ();
         fun mk_itapp e [] = e
           | mk_itapp e lookup = IInst (e, lookup);
-      in 
+      in
         trns
         |> debug 10 (fn _ => "making application (4): " ^ f ^ "::" ^ Sign.string_of_typ thy ty ^ " <~> " ^ Sign.string_of_typ thy ty_def)
         |> ensure_def_const thy defs (idf_of_cname thy defs (f, ty))
@@ -662,7 +667,7 @@
 
 fun defgen_tyco_fallback thy defs tyco trns =
   if Symtab.fold (fn (_, { syntax_tyco, ... }) => fn b => b orelse Symtab.defined syntax_tyco tyco)
-    ((#serialize_data o CodegenData.get) thy) false 
+    ((#serialize_data o CodegenData.get) thy) false
   then
     trns
     |> debug 5 (fn _ => "trying defgen tyco fallback for " ^ quote tyco)
@@ -673,7 +678,7 @@
 
 fun defgen_const_fallback thy defs f trns =
   if Symtab.fold (fn (_, { syntax_const, ... }) => fn b => b orelse Symtab.defined syntax_const f)
-    ((#serialize_data o CodegenData.get) thy) false 
+    ((#serialize_data o CodegenData.get) thy) false
   then
     trns
     |> debug 5 (fn _ => "trying defgen const fallback for " ^ quote f)
@@ -709,6 +714,8 @@
   case name_of_idf thy nsp_mem f
    of SOME clsmem =>
         let
+          val _ = debug 10 (fn _ => "CLSMEM " ^ quote clsmem) ();
+          val _ = debug 10 (fn _ => (the o ClassPackage.lookup_const_class thy) clsmem) ();
           val cls = idf_of_name thy nsp_class ((the o ClassPackage.lookup_const_class thy) clsmem);
           val (tvar, ty) = ClassPackage.get_const_sign thy clsmem;
         in
@@ -725,20 +732,25 @@
    of SOME (cls, tyco) =>
         let
           val arity = (map o map) (idf_of_name thy nsp_class)
-            (ClassPackage.get_arities thy [cls] tyco)
+            (ClassPackage.get_arities thy [cls] tyco);
           val clsmems = map (idf_of_name thy nsp_mem)
             (ClassPackage.the_consts thy cls);
           val instmem_idfs = map (idf_of_cname thy defs)
             (ClassPackage.get_inst_consts_sign thy (tyco, cls));
+          fun add_vars arity clsmems (trns as (_, univ)) =
+            ((invent_var_t_names
+              (map ((fn Classmember (_, _, ty) => ty) o get_def univ)
+              clsmems) (length arity) [] "a" ~~ arity, clsmems), trns)
         in
           trns
           |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")")
-          |> ensure_def_class thy defs (idf_of_name thy nsp_class cls)
+          |> (fold_map o fold_map) (ensure_def_class thy defs) arity
+          ||>> fold_map (ensure_def_const thy defs) clsmems
+          |-> (fn (arity, clsmems) => add_vars arity clsmems)
+          ||>> ensure_def_class thy defs (idf_of_name thy nsp_class cls)
           ||>> ensure_def_tyco thy defs (idf_of_tname thy tyco)
-          ||>> (fold_map o fold_map) (ensure_def_class thy defs) arity
-          ||>> fold_map (ensure_def_const thy defs) clsmems
           ||>> fold_map (ensure_def_const thy defs) instmem_idfs
-          |-> (fn ((((cls, tyco), arity), clsmems), instmem_idfs) =>
+          |-> (fn ((((arity, clsmems), cls), tyco), instmem_idfs) =>
                  succeed (Classinst (cls, (tyco, arity), clsmems ~~ instmem_idfs), []))
         end
     | _ =>
@@ -859,7 +871,7 @@
         )
     | _ =>
         trns
-        |> fail ("not a case constant expression: " ^ Sign.string_of_term thy t)
+        |> fail ("not a caseconstant expression: " ^ Sign.string_of_term thy t)
   end;
 
 fun defgen_datatype get_datatype thy defs tyco trns =
@@ -952,29 +964,7 @@
         |> null ? K ["x"]
         |> space_implode "_"
       end;
-    fun add_def (name, [(ty, (_, (args, rhs)))]) (overl, defs, clstab) =
-          (overl,
-           defs |> Symtab.update_new (idf_of_name thy nsp_const name, (args, rhs, ty)),
-           clstab)
-      | add_def (name, ds) ((overl, overl_rev), defs, clstab) =
-          let
-            val ty_decl = Sign.the_const_constraint thy name;
-            fun mk_idf ("0", Type ("nat", [])) = "const.Zero"
-              | mk_idf ("1", Type ("nat", [])) = "."
-              | mk_idf (nm, ty) =
-                  if is_number nm
-                  then nm
-                  else idf_of_name thy nsp_const nm
-                     ^ "_" ^ mangle_tyname (ty_decl, ty)
-            val overl_lookups = map
-              (fn (ty, (_, (args, rhs))) => (ty, mk_idf (name, ty), args, rhs)) ds;
-          in
-            ((overl |> Symtab.update_new (name, map (fn (ty, idf, _, _) => (ty, idf)) overl_lookups),
-              overl_rev |> fold Symtab.update_new (map (fn (ty, idf, _, _) => (idf, (name, ty))) overl_lookups)),
-             defs |> fold Symtab.update_new (map (fn (ty, idf, args, rhs) => (idf, (args, rhs, ty))) overl_lookups),
-             clstab)
-          end;
-    fun mk_instname thyname (cls, tyco) =
+    fun mangle_instname thyname (cls, tyco) =
       idf_of_name thy nsp_inst
         (NameSpace.append thyname (NameSpace.base cls ^ "_" ^ NameSpace.base tyco))
     fun add_clsmems classtab ((overl, overl_rev), defs, (clstab, clstab_rev, clsmems)) =
@@ -1001,19 +991,43 @@
        (clstab
         |> Symtab.fold
              (fn (cls, (_, clsinsts)) => fold
-                (fn (tyco, thyname) => Insttab.update ((cls, tyco), mk_instname thyname (cls, tyco))) clsinsts)
+                (fn (tyco, thyname) => Insttab.update ((cls, tyco), mangle_instname thyname (cls, tyco))) clsinsts)
              classtab,
         clstab_rev
         |> Symtab.fold
              (fn (cls, (_, clsinsts)) => fold
-                (fn (tyco, thyname) => Symtab.update (mk_instname thyname (cls, tyco), (cls, tyco))) clsinsts)
+                (fn (tyco, thyname) => Symtab.update (mangle_instname thyname (cls, tyco), (cls, tyco))) clsinsts)
              classtab,
         clsmems
         |> Symtab.fold
              (fn (class, (clsmems, _)) => fold
                 (fn clsmem => Symtab.update (clsmem, class)) clsmems)
              classtab))
-  in 
+    fun add_def (name, [(ty, (_, (args, rhs)))]) (overl, defs, clstab) =
+          (overl,
+           defs |> Symtab.update_new (idf_of_name thy nsp_const name, (args, rhs, ty)),
+           clstab)
+      | add_def (name, ds) ((overl, overl_rev), defs, clstab) =
+          let
+            val ty_decl = Sign.the_const_constraint thy name;
+            fun mk_idf ("0", Type ("nat", [])) = "const.Zero"
+              | mk_idf ("1", Type ("nat", [])) = "."
+              | mk_idf (nm, ty) =
+                  if is_number nm
+                  then nm
+                  else idf_of_name thy nsp_const nm
+                     ^ "_" ^ mangle_tyname (ty_decl, ty)
+            val overl_lookups = map
+              (fn (ty, (_, (args, rhs))) => (ty, mk_idf (name, ty), args, rhs)) ds;
+          in
+            ((overl
+              |> Symtab.default (name, [])
+              |> Symtab.map_entry name (append (map (fn (ty, idf, _, _) => (ty, idf)) overl_lookups)),
+              overl_rev
+              |> fold Symtab.update_new (map (fn (ty, idf, _, _) => (idf, (name, ty))) overl_lookups)),
+             defs
+             |> fold Symtab.update_new (map (fn (ty, idf, args, rhs) => (idf, (args, rhs, ty))) overl_lookups), clstab)
+          end;  in
     ((Symtab.empty, Symtab.empty), Symtab.empty, (Insttab.empty, Symtab.empty, Symtab.empty))
     |> add_clsmems (ClassPackage.get_classtab thy)
     |> fold add_def (Codegen.mk_deftab thy |> Symtab.dest)
@@ -1174,9 +1188,13 @@
 
 fun serialize_code serial_name filename consts thy =
   let
-    fun mk_sfun tab name args f =
-      Symtab.lookup tab name
-      |> Option.map (fn ms => Codegen.fillin_mixfix ms args (f : 'a -> Pretty.T))
+    fun mk_sfun tab =
+      let
+        fun na name =
+          Option.map Codegen.num_args_of (Symtab.lookup tab name)
+        fun stx name =
+          Codegen.fillin_mixfix ((the o Symtab.lookup tab) name)
+      in (na, stx) end;
     val serialize_data =
       thy
       |> CodegenData.get
@@ -1188,7 +1206,7 @@
       (#primitives serialize_data);
     val _ = serializer' : string list option -> module -> Pretty.T;
     val compile_it = serial_name = "ml" andalso filename = "-";
-    fun use_code code = 
+    fun use_code code =
       if compile_it
       then use_text Context.ml_output false code
       else File.write (Path.unpack filename) (code ^ "\n");
@@ -1197,7 +1215,7 @@
     |> (if is_some consts then generate_code (the consts) else pair [])
     |-> (fn [] => `(serializer' NONE o #modl o CodegenData.get)
           | consts => `(serializer' (SOME consts) o #modl o CodegenData.get))
-    |-> (fn code => ((use_code o Pretty.output) code; I))
+    |-> (fn code => (setmp print_mode [] (use_code o Pretty.output) code; I))
   end;
 
 
@@ -1214,14 +1232,14 @@
   ("code_generate", "code_serialize", "extracting", "defined_by", "depending_on", "code_alias", "code_syntax_tyco", "code_syntax_const");
 
 val generateP =
-  OuterSyntax.command generateK "generate executable code for constants" K.thy_decl ( 
+  OuterSyntax.command generateK "generate executable code for constants" K.thy_decl (
     Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ))
     >> (fn consts =>
           Toplevel.theory (generate_code consts #> snd))
   );
 
 val serializeP =
-  OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl ( 
+  OuterSyntax.command serializeK "serialize executable code for constants" K.thy_decl (
     P.name
     -- P.name
     -- Scan.option (
@@ -1233,7 +1251,7 @@
   );
 
 val aliasP =
-  OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl ( 
+  OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl (
     P.name
     -- P.name
       >> (fn (src, dst) => Toplevel.theory (add_alias (src, dst)))
@@ -1300,15 +1318,15 @@
     add_defgen ("defs", defgen_defs),
     add_defgen ("clsmem", defgen_clsmem),
     add_defgen ("clsinst", defgen_clsinst),
-    add_alias ("op <>", "neq"),
-    add_alias ("op >=", "ge"),
-    add_alias ("op >", "gt"),
-    add_alias ("op <=", "le"),
-    add_alias ("op <", "lt"),
-    add_alias ("op +", "add"),
-    add_alias ("op -", "minus"),
-    add_alias ("op *", "times"),
-    add_alias ("op @", "append"),
+    add_alias ("op <>", "op_neq"),
+    add_alias ("op >=", "op_ge"),
+    add_alias ("op >", "op_gt"),
+    add_alias ("op <=", "op_le"),
+    add_alias ("op <", "op_lt"),
+    add_alias ("op +", "op_add"),
+    add_alias ("op -", "op_minus"),
+    add_alias ("op *", "op_times"),
+    add_alias ("op @", "op_append"),
     add_lookup_tyco ("bool", type_bool),
     add_lookup_tyco ("IntDef.int", type_integer),
     add_lookup_tyco ("List.list", type_list),
--- a/src/Pure/Tools/codegen_serializer.ML	Tue Nov 29 16:04:57 2005 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Tue Nov 29 16:05:10 2005 +0100
@@ -15,13 +15,16 @@
   val has_prim: primitives -> string -> bool;
   val mk_prims: primitives -> string;
 
+  type num_args_syntax = string -> int option;
   type 'a pretty_syntax = string -> Pretty.T list -> ('a -> Pretty.T)
-    -> (string list * Pretty.T) option;
-  type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax
+    -> Pretty.T;
+  type serializer = num_args_syntax * CodegenThingol.itype pretty_syntax
+    -> num_args_syntax * CodegenThingol.iexpr pretty_syntax
     -> primitives -> string list option -> CodegenThingol.module -> Pretty.T;
   type parm_serializer = OuterParse.token list -> serializer * OuterParse.token list;
 
   val ml_from_thingol: string list list -> string -> serializer;
+  val haskell_from_thingol: string list list -> string -> serializer;
 end;
 
 structure CodegenSerializer: CODEGEN_SERIALIZER =
@@ -64,9 +67,11 @@
 
 (** generic serialization **)
 
+type num_args_syntax = string -> int option;
 type 'a pretty_syntax = string -> Pretty.T list -> ('a -> Pretty.T)
-  -> (string list * Pretty.T) option;
-type serializer = CodegenThingol.itype pretty_syntax -> CodegenThingol.iexpr pretty_syntax
+  -> Pretty.T;
+type serializer = num_args_syntax * CodegenThingol.itype pretty_syntax
+  -> num_args_syntax * CodegenThingol.iexpr pretty_syntax
   -> primitives -> string list option -> CodegenThingol.module -> Pretty.T;
 type parm_serializer = OuterParse.token list -> serializer * OuterParse.token list;
 
@@ -105,94 +110,121 @@
   | postify [p] f = [p, Pretty.brk 1, f]
   | postify (ps as _::_) f = [Pretty.list "(" ")" ps, Pretty.brk 1, f];
 
-fun praetify [] f = [f]
-  | praetify [p] f = [f, Pretty.str " of ", p]
+fun upper_first s =
+  let val (c :: cs) = String.explode s
+  in String.implode (Char.toUpper c :: cs) end;
+
+fun lower_first s =
+  let val (c :: cs) = String.explode s
+  in String.implode (Char.toLower c :: cs) end;
+
+
+(** grouping functions **)
+
+fun group_datatypes one_arg defs =
+  let
+    fun check_typ_dup dtname xs =
+      if AList.defined (op =) xs dtname
+      then error ("double datatype definition: " ^ quote dtname)
+      else xs
+    fun check_typ_miss dtname xs =
+      if AList.defined (op =) xs dtname
+      then xs
+      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;
 
 
 (** ML serializer **)
 
 local
 
-fun ml_validator prims name =
+fun ml_from_defs (tyco_na, tyco_stx) (const_na, const_stx) resolv ds =
   let
-    fun replace_invalid c =
-      if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
-      andalso not (NameSpace.separator = c)
-      then c
-      else "_"
-    fun suffix_it name =
-      name
-      |> member (op =) ThmDatabase.ml_reserved ? suffix "'"
-      |> member (op =) CodegenThingol.prims ? suffix "'"
-      |> has_prim prims ? suffix "'"
-      |> (fn name' => if name = name' then name else suffix_it name')
-  in
-    name
-    |> translate_string replace_invalid
-    |> suffix_it
-    |> (fn name' => if name = name' then NONE else SOME name')
-  end;
-
-val ml_label_uniq = translate_string (fn "'" => "''" | "." => "'" | c => c);
-
-fun ml_from_defs styco sconst resolv ds =
-  let
-    fun chunk_defs ps = 
+    fun chunk_defs ps =
       let
         val (p_init, p_last) = split_last ps
       in
         Pretty.chunks (p_init @ [Pretty.block ([p_last, Pretty.str ";"])])
     end;
-    fun ml_from_typ br (IType ("Pair", [t1, t2])) =
+    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_typ (INFX (2, X)) t1,
+            ml_from_type (INFX (2, X)) t1,
             Pretty.str "*",
-            ml_from_typ (INFX (2, X)) t2
+            ml_from_type (INFX (2, X)) t2
           ]
-      | ml_from_typ br (IType ("Bool", [])) =
+      | ml_from_type br (IType ("Bool", [])) =
           Pretty.str "bool"
-      | ml_from_typ br (IType ("Integer", [])) =
+      | ml_from_type br (IType ("Integer", [])) =
           Pretty.str "IntInf.int"
-      | ml_from_typ br (IType ("List", [ty])) =
-          postify ([ml_from_typ BR ty]) (Pretty.str "list")
+      | ml_from_type br (IType ("List", [ty])) =
+          postify ([ml_from_type BR ty]) (Pretty.str "list")
           |> Pretty.block
-      | ml_from_typ br (IType (tyco, typs)) =
+      | ml_from_type br (IType (tyco, typs)) =
           let
-            val tyargs = (map (ml_from_typ BR) typs)
+            val tyargs = (map (ml_from_type BR) typs)
           in
-            case styco tyco tyargs (ml_from_typ BR)
+            case tyco_na tyco
              of NONE =>
                   postify tyargs ((Pretty.str o resolv) tyco)
                   |> Pretty.block
-              | SOME ([], p) =>
-                  p
-              | SOME (_, p) =>
-                  error ("cannot serialize partial type application to ML, while serializing "
-                    ^ quote (tyco ^ " " ^ Pretty.output (Pretty.list "(" ")" tyargs)))
+              | SOME i =>
+                  if i <> length (typs)
+                  then error "can only serialize strictly complete type applications to ML"
+                  else tyco_stx tyco tyargs (ml_from_type BR)
           end
-      | ml_from_typ br (IFun (t1, t2)) =
+      | ml_from_type br (IFun (t1, t2)) =
           brackify (eval_br_postfix br (INFX (1, R))) [
-            ml_from_typ (INFX (1, X)) t1,
+            ml_from_type (INFX (1, X)) t1,
             Pretty.str "->",
-            ml_from_typ (INFX (1, R)) t2
+            ml_from_type (INFX (1, R)) t2
           ]
-      | ml_from_typ _ (IVarT (v, [])) =
+      | ml_from_type _ (IVarT (v, [])) =
           Pretty.str ("'" ^ v)
-      | ml_from_typ _ (IVarT (_, sort)) =
+      | ml_from_type _ (IVarT (_, sort)) =
           "cannot serialize sort constrained type variable to ML: " ^ commas sort |> error
-      | ml_from_typ _ (IDictT fs) =
+      | ml_from_type _ (IDictT fs) =
           (Pretty.enclose "{" "}" o Pretty.breaks) (
             map (fn (f, ty) =>
-              Pretty.block [Pretty.str (ml_label_uniq f ^ ": "), ml_from_typ NOBR ty]) fs
+              Pretty.block [Pretty.str (ml_label_uniq f ^ ": "), ml_from_type NOBR ty]) fs
           );
     fun ml_from_pat br (ICons (("True", []), _)) =
           Pretty.str "true"
       | ml_from_pat br (ICons (("False", []), _)) =
           Pretty.str "false"
-      | ml_from_pat br (ICons (("Pair", ps), _)) =
-          ps
-          |> map (ml_from_pat NOBR)
-          |> Pretty.list "(" ")"
+      | ml_from_pat br (ICons (("Pair", [p1, p2]), _)) =
+          Pretty.list "(" ")" [
+            ml_from_pat NOBR p1,
+            ml_from_pat NOBR p2
+          ]
       | ml_from_pat br (ICons (("Nil", []), _)) =
           Pretty.str "[]"
       | ml_from_pat br (p as ICons (("Cons", _), _)) =
@@ -217,10 +249,14 @@
           |> cons ((Pretty.str o resolv) f)
           |> brackify (eval_br br BR)
       | ml_from_pat br (IVarP (v, IType ("Integer", []))) =
-          Pretty.str ("(" ^ v ^ ":IntInf.int)")
+          brackify (eval_br br BR) [
+            Pretty.str v,
+            Pretty.str ":",
+            Pretty.str "IntInf.int"
+          ]
       | ml_from_pat br (IVarP (v, _)) =
           Pretty.str v;
-    fun ml_from_iexpr br (e as (IApp (IConst ("Cons", _), _))) =
+    fun ml_from_expr br (e as (IApp (IConst ("Cons", _), _))) =
           let
             fun dest_cons (IApp (IConst ("Cons", _),
                   IApp (IApp (IConst ("Pair", _), e1), e2))) = SOME (e1, e2)
@@ -229,33 +265,33 @@
             case unfoldr dest_cons e
              of (es, (IConst ("Nil", _))) =>
                   es
-                  |> map (ml_from_iexpr NOBR) 
+                  |> map (ml_from_expr NOBR)
                   |> Pretty.list "[" "]"
               | (es, e) =>
                   (es @ [e])
-                  |> map (ml_from_iexpr (INFX (5, X)))
+                  |> map (ml_from_expr (INFX (5, X)))
                   |> separate (Pretty.str "::")
                   |> brackify (eval_br br (INFX (5, R)))
           end
-      | ml_from_iexpr br (e as IApp (e1, e2)) =
+      | ml_from_expr br (e as IApp (e1, e2)) =
           (case (unfold_app e)
            of (e as (IConst (f, _)), es) =>
                 ml_from_app br (f, es)
-            | _ => 
+            | _ =>
                 brackify (eval_br br BR) [
-                  ml_from_iexpr NOBR e1,
-                  ml_from_iexpr BR e2
+                  ml_from_expr NOBR e1,
+                  ml_from_expr BR e2
                 ])
-      | ml_from_iexpr br (e as IConst (f, _)) =
+      | ml_from_expr br (e as IConst (f, _)) =
           ml_from_app br (f, [])
-      | ml_from_iexpr br (IVarE (v, _)) =
+      | ml_from_expr br (IVarE (v, _)) =
           Pretty.str v
-      | ml_from_iexpr br (IAbs ((v, _), e)) =
+      | ml_from_expr br (IAbs ((v, _), e)) =
           brackify (eval_br br BR) [
             Pretty.str ("fn " ^ v ^ " =>"),
-            ml_from_iexpr BR e
+            ml_from_expr NOBR e
           ]
-      | ml_from_iexpr br (e as ICase (_, [_])) =
+      | ml_from_expr br (e as ICase (_, [_])) =
           let
             val (ps, e) = unfold_let e;
             fun mk_val (p, e) = Pretty.block [
@@ -263,15 +299,15 @@
                 ml_from_pat BR p,
                 Pretty.str " =",
                 Pretty.brk 1,
-                ml_from_iexpr NOBR e,
+                ml_from_expr NOBR e,
                 Pretty.str ";"
               ]
           in Pretty.chunks [
             [Pretty.str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block,
-            [Pretty.str ("in"), Pretty.fbrk, ml_from_iexpr NOBR e] |> Pretty.block,
+            [Pretty.str ("in"), Pretty.fbrk, ml_from_expr NOBR e] |> Pretty.block,
             Pretty.str ("end")
           ] end
-      | ml_from_iexpr br (ICase (e, c::cs)) =
+      | ml_from_expr br (ICase (e, c::cs)) =
           let
             fun mk_clause definer (p, e) =
               Pretty.block [
@@ -279,22 +315,22 @@
                 ml_from_pat NOBR p,
                 Pretty.str " =>",
                 Pretty.brk 1,
-                ml_from_iexpr NOBR e
+                ml_from_expr NOBR e
               ]
           in brackify (eval_br br BR) (
             Pretty.str "case"
-            :: ml_from_iexpr NOBR e
+            :: ml_from_expr NOBR e
             :: mk_clause "of " c
             :: map (mk_clause "| ") cs
           ) end
-      | ml_from_iexpr br (IInst _) =
+      | ml_from_expr br (IInst _) =
           error "cannot serialize poly instant to ML"
-      | ml_from_iexpr br (IDictE fs) =
+      | ml_from_expr br (IDictE fs) =
           (Pretty.enclose "{" "}" o Pretty.breaks) (
             map (fn (f, e) =>
-              Pretty.block [Pretty.str (ml_label_uniq f ^ " = "), ml_from_iexpr NOBR e]) fs
+              Pretty.block [Pretty.str (ml_label_uniq f ^ " = "), ml_from_expr NOBR e]) fs
           )
-      | ml_from_iexpr br (ILookup (ls, 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,
@@ -304,7 +340,7 @@
           ]
     and mk_app_p br p args =
       brackify (eval_br br BR)
-        (p :: map (ml_from_iexpr BR) args)
+        (p :: map (ml_from_expr BR) args)
     and ml_from_app br ("Nil", []) =
           Pretty.str "[]"
       | ml_from_app br ("True", []) =
@@ -313,75 +349,76 @@
           Pretty.str "false"
       | ml_from_app br ("primeq", [e1, e2]) =
           brackify (eval_br br (INFX (4, L))) [
-            ml_from_iexpr (INFX (4, L)) e1,
+            ml_from_expr (INFX (4, L)) e1,
             Pretty.str "=",
-            ml_from_iexpr (INFX (4, X)) e2
+            ml_from_expr (INFX (4, X)) e2
           ]
       | ml_from_app br ("Pair", [e1, e2]) =
           Pretty.list "(" ")" [
-            ml_from_iexpr NOBR e1,
-            ml_from_iexpr NOBR e2
+            ml_from_expr NOBR e1,
+            ml_from_expr NOBR e2
           ]
       | ml_from_app br ("and", [e1, e2]) =
           brackify (eval_br br (INFX (~1, L))) [
-            ml_from_iexpr (INFX (~1, L)) e1,
+            ml_from_expr (INFX (~1, L)) e1,
             Pretty.str "andalso",
-            ml_from_iexpr (INFX (~1, X)) e2
+            ml_from_expr (INFX (~1, X)) e2
           ]
       | ml_from_app br ("or", [e1, e2]) =
           brackify (eval_br br (INFX (~2, L))) [
-            ml_from_iexpr (INFX (~2, L)) e1,
+            ml_from_expr (INFX (~2, L)) e1,
             Pretty.str "orelse",
-            ml_from_iexpr (INFX (~2, X)) e2
+            ml_from_expr (INFX (~2, X)) e2
           ]
       | ml_from_app br ("if", [b, e1, e2]) =
           brackify (eval_br br BR) [
             Pretty.str "if",
-            ml_from_iexpr BR b,
+            ml_from_expr NOBR b,
             Pretty.str "then",
-            ml_from_iexpr BR e1,
+            ml_from_expr NOBR e1,
             Pretty.str "else",
-            ml_from_iexpr BR e2
+            ml_from_expr NOBR e2
           ]
       | ml_from_app br ("add", [e1, e2]) =
           brackify (eval_br br (INFX (6, L))) [
-            ml_from_iexpr (INFX (6, L)) e1,
+            ml_from_expr (INFX (6, L)) e1,
             Pretty.str "+",
-            ml_from_iexpr (INFX (6, X)) e2
+            ml_from_expr (INFX (6, X)) e2
           ]
       | ml_from_app br ("mult", [e1, e2]) =
           brackify (eval_br br (INFX (7, L))) [
-            ml_from_iexpr (INFX (7, L)) e1,
+            ml_from_expr (INFX (7, L)) e1,
             Pretty.str "+",
-            ml_from_iexpr (INFX (7, X)) e2
+            ml_from_expr (INFX (7, X)) e2
           ]
       | ml_from_app br ("lt", [e1, e2]) =
           brackify (eval_br br (INFX (4, L))) [
-            ml_from_iexpr (INFX (4, L)) e1,
+            ml_from_expr (INFX (4, L)) e1,
             Pretty.str "<",
-            ml_from_iexpr (INFX (4, X)) e2
+            ml_from_expr (INFX (4, X)) e2
           ]
       | ml_from_app br ("le", [e1, e2]) =
           brackify (eval_br br (INFX (7, L))) [
-            ml_from_iexpr (INFX (4, L)) e1,
+            ml_from_expr (INFX (4, L)) e1,
             Pretty.str "<=",
-            ml_from_iexpr (INFX (4, X)) e2
+            ml_from_expr (INFX (4, X)) e2
           ]
       | ml_from_app br ("minus", es) =
           mk_app_p br (Pretty.str "~") es
       | ml_from_app br ("wfrec", es) =
           mk_app_p br (Pretty.str "wfrec") es
+      | ml_from_app br (f, []) =
+          Pretty.str (resolv f)
       | ml_from_app br (f, es) =
-          let
-            val args = map (ml_from_iexpr BR) es
-            val brackify' = K (eval_br br BR) ? (single #> Pretty.enclose "(" ")")
-          in
-            case sconst f args (ml_from_iexpr BR)
-             of NONE =>
-                  brackify (eval_br br BR) (Pretty.str (resolv f) :: args)
-              | SOME (_, p) =>
-                  brackify' p
-          end;
+          case const_na f
+           of NONE =>
+                let
+                  val (es', e) = split_last es;
+                in mk_app_p br (ml_from_app NOBR (f, es')) [e] end
+            | SOME i =>
+                let
+                  val (es1, es2) = splitAt (i, es);
+                in mk_app_p br (const_stx f (map (ml_from_expr BR) es1) (ml_from_expr BR)) es2 end;
     fun ml_from_funs (ds as d::ds_tl) =
       let
         fun mk_definer [] = "val"
@@ -399,9 +436,9 @@
           let
             val lhs = [Pretty.str (definer ^ " " ^ f)]
                        @ (if null pats
-                          then [Pretty.str ":", ml_from_typ NOBR ty]
+                          then [Pretty.str ":", ml_from_type NOBR ty]
                           else map (ml_from_pat BR) pats)
-            val rhs = [Pretty.str "=", ml_from_iexpr NOBR expr]
+            val rhs = [Pretty.str "=", ml_from_expr NOBR expr]
           in
             Pretty.block (separate (Pretty.brk 1) (lhs @ rhs))
           end
@@ -422,44 +459,21 @@
           :: map (mk_fun "and") ds_tl
         )
       end;
-    fun ml_from_datatypes ds =
+    fun ml_from_datatypes defs =
       let
-        fun check_typ_dup ty xs =
-          if AList.defined (op =) xs ty
-          then error ("double datatype definition: " ^ quote ty)
-          else xs
-        fun check_typ_miss ty xs =
-          if AList.defined (op =) xs ty
-          then xs
-          else error ("missing datatype definition: " ^ quote ty)
-        fun group (name, Datatype (vs, _, _)) ts =
-              (map (fn (_, []) => () | _ => error "can't serialize sort constrained datatype declaration to ML") vs;
-              ts
-              |> apsnd (check_typ_dup name)
-              |> apsnd (AList.update (op =) (name, (vs, []))))
-          | group (_, Datatypecons (_, _::_::_)) _ =
-              error ("Datatype constructor containing more than one parameter")
-          | group (name, Datatypecons (ty, tys)) ts =
-              ts
-              |> apfst (AList.default (op =) (resolv ty, []))
-              |> apfst (AList.map_entry (op =) (resolv ty) (cons (name, tys)))
-          | group _ _ =
-              error ("Datatype block containing other statements than datatype or constructor definitions")
-        fun group_cons (ty, co) ts =
-          ts
-          |> check_typ_miss ty
-          |> AList.map_entry (op =) ty (rpair co o fst)
         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_typ NOBR) typs)
+                (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_typ BR o IVarT) vs)
-                    (Pretty.str t)
+                @ 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)
@@ -471,10 +485,7 @@
             )
           end;
       in
-        ([], [])
-        |> fold group ds
-        |-> (fn cons => fold group_cons cons)
-        |> mk_datatypes
+        (mk_datatypes o group_datatypes true) defs
       end;
     fun ml_from_def (name, Typesyn (vs, ty)) =
         (map (fn (vname, []) => () | _ => error "can't serialize sort constrained type declaration to ML") vs;
@@ -483,30 +494,50 @@
           :: postify (map (Pretty.str o fst) vs) (Pretty.str name)
           @ [Pretty.str " =",
           Pretty.brk 1,
-          ml_from_typ NOBR ty,
+          ml_from_type NOBR ty,
           Pretty.str ";"
         ]))
       | ml_from_def (name, Nop) =
           if exists (fn query => (is_some o query) name)
-            [(fn name => styco name [] (ml_from_typ NOBR)),
-             (fn name => sconst name [] (ml_from_iexpr NOBR))]
+            [(fn name => tyco_na name),
+             (fn name => const_na name)]
           then Pretty.str ""
           else error ("empty statement during serialization: " ^ quote name)
       | ml_from_def (name, Class _) =
           error ("can't serialize class declaration " ^ quote name ^ " to ML")
       | ml_from_def (name, Classinst _) =
           error ("can't serialize instance declaration " ^ quote name ^ " to ML")
-  in case (snd o hd) ds
+  in (writeln "******************"; (*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)
+    | _ => (case ds of [d] => ml_from_def d))
   end;
 
 in
 
-fun ml_from_thingol nspgrp name_root styco sconst prims select module =
+fun ml_from_thingol nspgrp name_root (tyco_syntax) (const_syntax as (const_na, _)) prims select module =
   let
+    fun ml_validator name =
+      let
+        fun replace_invalid c =
+          if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
+          andalso not (NameSpace.separator = c)
+          then c
+          else "_"
+        fun suffix_it name =
+          name
+          |> member (op =) ThmDatabase.ml_reserved ? suffix "'"
+          |> member (op =) CodegenThingol.prims ? suffix "'"
+          |> has_prim prims ? suffix "'"
+          |> (fn name' => if name = name' then name else suffix_it name')
+      in
+        name
+        |> translate_string replace_invalid
+        |> suffix_it
+        |> (fn name' => if name = name' then NONE else SOME name')
+    end;
     fun ml_from_module (name, ps) =
       Pretty.chunks ([
         Pretty.str ("structure " ^ name ^ " = "),
@@ -532,11 +563,10 @@
             of Datatypecons (_ , tys) =>
                 if length tys >= 2 then length tys else 0
              | _ =>
-              (case sconst s [] (K (Pretty.str ""))
-               of NONE => 0
-                | SOME (xs, _) => length xs)
+                const_na s
+                |> the_default 0
           else 0
-  in 
+  in
     module
     |> debug 12 (Pretty.output o pretty_module)
     |> debug 3 (fn _ => "connecting datatypes and classdecls...")
@@ -553,7 +583,7 @@
     |> debug 3 (fn _ => "eliminating classes...")
     |> eliminate_classes
     |> debug 3 (fn _ => "generating...")
-    |> serialize (ml_from_defs styco sconst) ml_from_module (ml_validator prims) nspgrp name_root
+    |> serialize (ml_from_defs tyco_syntax const_syntax) ml_from_module ml_validator nspgrp name_root
   end;
 
 fun ml_from_thingol' nspgrp name_root =
@@ -571,5 +601,396 @@
 
 end; (* local *)
 
+local
+
+val bslash = "\\";
+
+fun haskell_from_defs (tyco_na, tyco_stx) (const_na, const_stx) is_cons resolv defs =
+  let
+    val resolv = fn s =>
+      let
+        val (prfix, base) = (split_last o NameSpace.unpack o resolv) s
+      in
+        NameSpace.pack (map upper_first prfix @ [base])
+      end;
+    fun resolv_const f =
+      if is_cons f
+      then (upper_first o resolv) f
+      else (lower_first o resolv) f
+    fun haskell_from_sctxt vs =
+      let
+        fun from_sctxt [] = Pretty.str ""
+          | from_sctxt vs =
+              vs
+              |> map (fn (v, cls) => Pretty.str ((upper_first o resolv) cls ^ " " ^ lower_first v))
+              |> Pretty.gen_list "," "(" ")"
+              |> (fn p => Pretty.block [p, Pretty.str " => "])
+      in 
+        vs
+        |> map (fn (v, sort) => map (pair v) sort)
+        |> Library.flat
+        |> from_sctxt
+      end;
+    fun haskell_from_type br ty =
+      let
+        fun from_itype br (IType ("Pair", [t1, t2])) sctxt =
+              sctxt
+              |> from_itype NOBR t1
+              ||>> from_itype NOBR t2
+              |-> (fn (p1, p2) => pair (Pretty.gen_list "," "(" ")" [p1, p2]))
+          | from_itype br (IType ("List", [ty])) sctxt =
+              sctxt
+              |> from_itype NOBR ty
+              |-> (fn p => pair (Pretty.enclose "[" "]" [p]))
+          | from_itype br (IType (tyco, tys)) sctxt =
+              let
+                fun mk_itype NONE tyargs sctxt =
+                      sctxt
+                      |> pair (brackify (eval_br br BR) ((Pretty.str o upper_first o resolv) tyco :: tyargs))
+                  | mk_itype (SOME i) tyargs sctxt =
+                      if i <> length (tys)
+                      then error "can only serialize strictly complete type applications to haskell"
+                      else
+                        sctxt
+                        |> pair (tyco_stx tyco tyargs (haskell_from_type BR))
+              in
+                sctxt
+                |> fold_map (from_itype BR) tys
+                |-> mk_itype (tyco_na tyco)
+              end
+          | from_itype br (IFun (t1, t2)) sctxt =
+              sctxt
+              |> from_itype (INFX (1, X)) t1
+              ||>> from_itype (INFX (1, R)) t2
+              |-> (fn (p1, p2) => pair (
+                    brackify (eval_br br (INFX (1, R))) [
+                      p1,
+                      Pretty.str "->",
+                      p2
+                    ]
+                  ))
+          | from_itype br (IVarT (v, [])) sctxt =
+              sctxt
+              |> pair ((Pretty.str o lower_first) v)
+          | from_itype br (IVarT (v, sort)) sctxt =
+              sctxt
+              |> AList.default (op =) (v, [])
+              |> AList.map_entry (op =) v (fold (insert (op =)) sort)
+              |> pair ((Pretty.str o lower_first) v)
+          | from_itype br (IDictT _) _ =
+              error "cannot serialize dictionary type to haskell"
+      in
+        []
+        |> from_itype br ty
+        ||> haskell_from_sctxt
+        |> (fn (pty, pctxt) => Pretty.block [pctxt, pty])
+      end;
+    fun haskell_from_pat br (ICons (("Pair", [p1, p2]), _)) =
+          Pretty.list "(" ")" [
+            haskell_from_pat NOBR p1,
+            haskell_from_pat NOBR p2
+          ]
+      | haskell_from_pat br (ICons (("Nil", []), _)) =
+          Pretty.str "[]"
+      | haskell_from_pat br (p as ICons (("Cons", _), _)) =
+          let
+            fun dest_cons (ICons (("Cons", [p1, p2]), ty)) = SOME (p1, p2)
+              | dest_cons p = NONE
+          in
+            case unfoldr dest_cons p
+             of (ps, (ICons (("Nil", []), _))) =>
+                  ps
+                  |> map (haskell_from_pat NOBR)
+                  |> Pretty.list "[" "]"
+              | (ps, p) =>
+                  (ps @ [p])
+                  |> map (haskell_from_pat (INFX (5, X)))
+                  |> separate (Pretty.str ":")
+                  |> brackify (eval_br br (INFX (5, R)))
+          end
+      | haskell_from_pat br (ICons ((f, ps), _)) =
+          ps
+          |> map (haskell_from_pat BR)
+          |> cons ((Pretty.str o upper_first o resolv) f)
+          |> brackify (eval_br br BR)
+      | haskell_from_pat br (IVarP (v, _)) =
+          (Pretty.str o lower_first) v;
+    fun haskell_from_expr br (e as (IApp (IApp (IConst ("Cons", _), _), _))) =
+          let
+            fun dest_cons (IApp (IApp (IConst ("Cons", _), e1), e2)) = SOME (e1, e2)
+              | dest_cons p = NONE
+          in
+            case unfoldr dest_cons e
+             of (es, (IConst ("Nil", _))) =>
+                  es
+                  |> map (haskell_from_expr NOBR)
+                  |> Pretty.list "[" "]"
+              | (es, e) =>
+                  (es @ [e])
+                  |> map (haskell_from_expr (INFX (5, X)))
+                  |> separate (Pretty.str ":")
+                  |> brackify (eval_br br (INFX (5, R)))
+          end
+      | haskell_from_expr br (e as IApp (e1, e2)) =
+          (case (unfold_app e)
+           of (e as (IConst (f, _)), es) =>
+                haskell_from_app br (f, es)
+            | _ =>
+                brackify (eval_br br BR) [
+                  haskell_from_expr NOBR e1,
+                  haskell_from_expr BR e2
+                ])
+      | haskell_from_expr br (e as IConst (f, _)) =
+          haskell_from_app br (f, [])
+      | haskell_from_expr br (IVarE (v, _)) =
+          (Pretty.str o lower_first) v
+      | haskell_from_expr br (e as IAbs _) =
+          let
+            val (vs, body) = unfold_abs e
+          in
+            brackify (eval_br br BR) (
+              Pretty.str bslash
+              :: map (Pretty.str o lower_first o fst) vs @ [
+              Pretty.str "->",
+              haskell_from_expr NOBR body
+            ])
+          end
+      | haskell_from_expr br (e as ICase (_, [_])) =
+          let
+            val (ps, body) = unfold_let e;
+            fun mk_bind (p, e) = Pretty.block [
+                haskell_from_pat BR p,
+                Pretty.str " =",
+                Pretty.brk 1,
+                haskell_from_expr NOBR e
+              ];
+          in Pretty.chunks [
+            [Pretty.str ("let"), Pretty.fbrk, map mk_bind ps |> Pretty.chunks] |> Pretty.block,
+            [Pretty.str ("in "), haskell_from_expr NOBR body] |> Pretty.block
+          ] end
+      | haskell_from_expr br (ICase (e, c::cs)) =
+          let
+            fun mk_clause (p, e) =
+              Pretty.block [
+                haskell_from_pat NOBR p,
+                Pretty.str " ->",
+                Pretty.brk 1,
+                haskell_from_expr NOBR e
+              ]
+          in (Pretty.block o Pretty.fbreaks) (
+            Pretty.block [Pretty.str "case ", haskell_from_expr NOBR e, Pretty.str " of"]
+            :: map (mk_clause) cs
+          )end
+      | haskell_from_expr br (IInst (e, _)) =
+          haskell_from_expr br e
+      | haskell_from_expr br (IDictE _) =
+          error "cannot serialize dictionary expression to haskell"
+      | haskell_from_expr br (ILookup _) =
+          error "cannot serialize lookup expression to haskell"
+    and mk_app_p br p args =
+      brackify (eval_br br BR)
+        (p :: map (haskell_from_expr BR) args)
+    and haskell_from_app br ("Nil", []) =
+          Pretty.str "[]"
+      | haskell_from_app br ("Cons", es) =
+          mk_app_p br (Pretty.str "(:)") es
+      | haskell_from_app br ("primeq", [e1, e2]) =
+          brackify (eval_br br (INFX (4, L))) [
+            haskell_from_expr (INFX (4, L)) e1,
+            Pretty.str "==",
+            haskell_from_expr (INFX (4, X)) e2
+          ]
+      | haskell_from_app br ("Pair", [e1, e2]) =
+          Pretty.list "(" ")" [
+            haskell_from_expr NOBR e1,
+            haskell_from_expr NOBR e2
+          ]
+      | haskell_from_app br ("and", [e1, e2]) =
+          brackify (eval_br br (INFX (3, R))) [
+            haskell_from_expr (INFX (3, X)) e1,
+            Pretty.str "&&",
+            haskell_from_expr (INFX (3, R)) e2
+          ]
+      | haskell_from_app br ("or", [e1, e2]) =
+          brackify (eval_br br (INFX (2, L))) [
+            haskell_from_expr (INFX (2, L)) e1,
+            Pretty.str "||",
+            haskell_from_expr (INFX (2, X)) e2
+          ]
+      | haskell_from_app br ("if", [b, e1, e2]) =
+          brackify (eval_br br BR) [
+            Pretty.str "if",
+            haskell_from_expr NOBR b,
+            Pretty.str "then",
+            haskell_from_expr NOBR e1,
+            Pretty.str "else",
+            haskell_from_expr NOBR e2
+          ]
+      | haskell_from_app br ("add", [e1, e2]) =
+          brackify (eval_br br (INFX (6, L))) [
+            haskell_from_expr (INFX (6, L)) e1,
+            Pretty.str "+",
+            haskell_from_expr (INFX (6, X)) e2
+          ]
+      | haskell_from_app br ("mult", [e1, e2]) =
+          brackify (eval_br br (INFX (7, L))) [
+            haskell_from_expr (INFX (7, L)) e1,
+            Pretty.str "*",
+            haskell_from_expr (INFX (7, X)) e2
+          ]
+      | haskell_from_app br ("lt", [e1, e2]) =
+          brackify (eval_br br (INFX (4, L))) [
+            haskell_from_expr (INFX (4, L)) e1,
+            Pretty.str "<",
+            haskell_from_expr (INFX (4, X)) e2
+          ]
+      | haskell_from_app br ("le", [e1, e2]) =
+          brackify (eval_br br (INFX (7, L))) [
+            haskell_from_expr (INFX (4, L)) e1,
+            Pretty.str "<=",
+            haskell_from_expr (INFX (4, X)) e2
+          ]
+      | haskell_from_app br ("minus", es) =
+          mk_app_p br (Pretty.str "negate") es
+      | haskell_from_app br ("wfrec", es) =
+          mk_app_p br (Pretty.str "wfrec") es
+      | haskell_from_app br (f, []) =
+          Pretty.str (resolv_const f)
+      | haskell_from_app br (f, es) =
+          case const_na f
+           of NONE =>
+                let
+                  val (es', e) = split_last es;
+                in mk_app_p br (haskell_from_app NOBR (f, es')) [e] end
+            | SOME i =>
+                let
+                  val (es1, es2) = splitAt (i, es);
+                in mk_app_p br (const_stx f (map (haskell_from_expr BR) es1) (haskell_from_expr BR)) es2 end;
+    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 = Pretty.str "";
+(*
+      | haskell_from_def (name, Class (supclsnames, members, insts)) = Pretty.str ""
+      | haskell_from_def (name, Classmember (clsname, v, ty)) = Pretty.str ""
+*)
+    fun haskell_from_def (name, Nop) =
+          if exists (fn query => (is_some o query) name)
+            [(fn name => tyco_na name),
+             (fn name => const_na name)]
+          then Pretty.str ""
+          else error ("empty statement during serialization: " ^ quote name)
+      | haskell_from_def (name, Fun (eqs, (_, ty))) =
+          let
+            fun from_eq name (args, rhs) =
+              Pretty.block [
+                Pretty.str (lower_first name),
+                Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, haskell_from_pat BR p]) args),
+                Pretty.brk 1,
+                Pretty.str ("="),
+                Pretty.brk 1,
+                haskell_from_expr NOBR rhs
+              ]
+          in
+            Pretty.chunks [
+              Pretty.block [
+                Pretty.str (name ^ " ::"),
+                Pretty.brk 1,
+                haskell_from_type NOBR ty
+              ],
+              Pretty.chunks (map (from_eq name) eqs)
+            ]
+          end
+      | haskell_from_def (name, Typesyn (vs, ty)) =
+          Pretty.block [
+            Pretty.str "type ",
+            haskell_from_sctxt vs,
+            Pretty.str (upper_first name),
+            Pretty.block (map (fn (v, _) => Pretty.str (" " ^ (lower_first) v)) vs),
+            Pretty.str " =",
+            Pretty.brk 1,
+            haskell_from_type NOBR ty
+          ]
+      | haskell_from_def (_, Classinst (clsname, (tyco, arity), instmems)) = 
+          Pretty.block [
+            Pretty.str "instance ",
+            haskell_from_sctxt arity,
+            Pretty.str ((upper_first o resolv) clsname),
+            Pretty.str " ",
+            Pretty.str ((upper_first o resolv) tyco),
+            Pretty.str " where",
+            Pretty.fbrk,
+            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 ""))
+  end;
+
+in
+
+fun haskell_from_thingol nspgrp name_root tyco_syntax (const_syntax as (const_na, _)) prims select module =
+  let
+    fun haskell_from_module (name, ps) =
+      Pretty.block [
+          Pretty.str ("module " ^ (upper_first name) ^ " where"),
+          Pretty.fbrk,
+          Pretty.fbrk,
+          Pretty.chunks (separate (Pretty.str "") ps)
+        ];
+    fun haskell_validator s = NONE;
+    fun eta_expander "Pair" = 2
+      | eta_expander "if" = 3
+      | 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
+             | _ =>
+                const_na s
+                |> the_default 0
+          else 0;
+    fun is_cons f =
+      NameSpace.is_qualified f
+      andalso case get_def module f
+       of Datatypecons _ => true
+        | _ => false;
+  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 _ => "generating...")
+    |> serialize (haskell_from_defs tyco_syntax const_syntax is_cons) haskell_from_module haskell_validator nspgrp name_root
+  end;
+
+end; (* local *)
+
 end; (* struct *)
 
--- a/src/Pure/Tools/codegen_thingol.ML	Tue Nov 29 16:04:57 2005 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Tue Nov 29 16:05:10 2005 +0100
@@ -25,9 +25,6 @@
     | ICase of iexpr * (ipat * iexpr) list
     | IDictE of (string * iexpr) list
     | ILookup of (string list * vname);
-  val eq_itype: itype * itype -> bool
-  val eq_ipat: ipat * ipat -> bool
-  val eq_iexpr: iexpr * iexpr -> bool
   val mk_funs: itype list * itype -> itype;
   val mk_apps: iexpr * iexpr list -> iexpr;
   val mk_abss: (vname * itype) list * iexpr -> iexpr;
@@ -38,9 +35,11 @@
   val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
   val unfold_fun: itype -> itype list * itype;
   val unfold_app: iexpr -> iexpr * iexpr list;
+  val unfold_abs: iexpr -> (vname * itype) list * iexpr;
   val unfold_let: iexpr -> (ipat * iexpr) list * iexpr;
   val itype_of_iexpr: iexpr -> itype;
   val ipat_of_iexpr: iexpr -> ipat;
+  val eq_itype: itype * itype -> bool;
   val invent_var_t_names: itype list -> int -> vname list -> vname -> vname list;
   val invent_var_e_names: iexpr list -> int -> vname list -> vname -> vname list;
 
@@ -52,15 +51,14 @@
     | Datatypecons of string * itype list
     | Class of string list * string list * string list
     | Classmember of string * vname * itype
-    | Classinst of string * (string * string list list) * (string * string) list;
+    | Classinst of string * (string * (vname * string list) list) * (string * string) list;
   type module;
   type transact;
   type 'dst transact_fin;
   type ('src, 'dst) gen_codegen = 'src -> transact -> 'dst transact_fin;
   type gen_defgen = string -> transact -> (def * string list) transact_fin;
-  val eq_def: def * def -> bool;
   val pretty_def: def -> Pretty.T;
-  val pretty_module: module -> Pretty.T;  
+  val pretty_module: module -> Pretty.T; 
   val empty_module: module;
   val get_def: module -> string -> def;
   val merge_module: module * module -> module;
@@ -222,10 +220,6 @@
   | IDictE of (string * iexpr) list
   | ILookup of (string list * vname);
 
-val eq_itype = (op =);
-val eq_ipat = (op =);
-val eq_iexpr = (op =);
-
 val mk_funs = Library.foldr IFun;
 val mk_apps = Library.foldl IApp;
 val mk_abss = Library.foldr IAbs;
@@ -246,6 +240,10 @@
   (fn IApp e => SOME e
     | _ => NONE);
 
+val unfold_abs = unfoldr
+  (fn IAbs b => SOME b
+    | _ => NONE)
+
 val unfold_let = unfoldr
   (fn ICase (e, [(p, e')]) => SOME ((p, e), e')
     | _ => NONE);
@@ -273,7 +271,10 @@
   | map_iexpr _ _ _ (e as IConst _) =
       e
   | map_iexpr _ _ _ (e as IVarE _) =
-      e;
+      e
+  | map_iexpr f_itype f_ipat f_iexpr (IDictE ms) =
+      IDictE (map (apsnd f_iexpr) ms)
+  | map_iexpr _ _ _ (ILookup _) = error "ILOOKUP";
 
 fun fold_itype f_itype (IFun (t1, t2)) =
       f_itype t1 #> f_itype t2
@@ -294,13 +295,41 @@
   | fold_iexpr f_itype f_ipat f_iexpr (IAbs (v, e)) =
       f_iexpr e
   | fold_iexpr f_itype f_ipat f_iexpr (ICase (e, ps)) =
-      f_iexpr e #> fold (fn (p, e) => f_ipat p #> f_iexpr e) ps 
+      f_iexpr e #> fold (fn (p, e) => f_ipat p #> f_iexpr e) ps
   | fold_iexpr _ _ _ (e as IConst _) =
       I
   | fold_iexpr _ _ _ (e as IVarE _) =
       I;
 
 
+(* simple type matching *)
+
+fun eq_itype (ty1, ty2) =
+  let
+    exception NO_MATCH;
+    fun eq (IVarT (v1, sort1)) (IVarT (v2, sort2)) subs =
+          if sort1 <> sort2
+          then raise NO_MATCH
+          else
+            (case AList.lookup (op =) subs v1
+             of NONE => subs |> AList.update (op =) (v1, v2)
+              | (SOME v1') =>
+                  if v1' <> v2
+                  then raise NO_MATCH
+                  else subs)
+      | eq (IType (tyco1, tys1)) (IType (tyco2, tys2)) subs =
+          if tyco1 <> tyco2
+          then raise NO_MATCH
+          else subs |> fold2 eq tys1 tys2
+      | eq (IFun (ty11, ty12)) (IFun (ty21, ty22)) subs =
+          subs |> eq ty11 ty21 |> eq ty12 ty22
+      | eq _ _ _ = raise NO_MATCH;
+  in
+    (eq ty1 ty2 []; true)
+    handle NO_MATCH => false
+  end;
+
+
 (* simple diagnosis *)
 
 fun pretty_itype (IType (tyco, tys)) =
@@ -309,12 +338,14 @@
       Pretty.gen_list "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
   | pretty_itype (IVarT (v, sort)) =
       Pretty.str (v ^ enclose "|" "|" (space_implode "|" sort))
+  | pretty_itype (IDictT _) =
+      Pretty.str "<DictT>";
 
 fun pretty_ipat (ICons ((cons, ps), ty)) =
       Pretty.gen_list " " "(" ")"
         (Pretty.str cons :: map pretty_ipat ps @ [Pretty.str ":: ", pretty_itype ty])
   | pretty_ipat (IVarP (v, ty)) =
-      Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty]
+      Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty];
 
 fun pretty_iexpr (IConst (f, ty)) =
       Pretty.block [Pretty.str (f ^ "::"), pretty_itype ty]
@@ -338,6 +369,10 @@
           ]
         ) cs)
       ]
+  | pretty_iexpr (IDictE _) =
+      Pretty.str "<DictE>"
+  | pretty_iexpr (ILookup _) =
+      Pretty.str "<Lookup>";
 
 
 (* language auxiliary *)
@@ -351,7 +386,7 @@
             else error ("inconsistent application: in " ^ Pretty.output (pretty_iexpr e)
               ^ ", " ^ (Pretty.output o pretty_itype) ty2 ^ " vs. " ^ (Pretty.output o pretty_itype o itype_of_iexpr) e2)
        | _ => error ("expression is not a function: " ^ Pretty.output (pretty_iexpr e1)))
-  | itype_of_iexpr (IInst (e, cs)) = error ""
+  | itype_of_iexpr (IInst (e, cs)) = itype_of_iexpr e
   | itype_of_iexpr (IAbs ((_, ty1), e2)) = ty1 `-> itype_of_iexpr e2
   | itype_of_iexpr (ICase ((_, [(_, e)]))) = itype_of_iexpr e;
 
@@ -402,22 +437,25 @@
     fun invent (IConst (f, _)) =
           I
       | invent (IVarE (v, _)) =
-          cons v
+          insert (op =) v
       | invent (IApp (e1, e2)) =
           invent e1 #> invent e2
       | invent (IAbs ((v, _), e)) =
-          cons v #> invent e
+          insert (op =) v #> invent e
       | invent (ICase (e, cs)) =
           invent e
-          #>
-          fold (fn (p, e) => append (vars_of_ipats [p]) #> invent e) cs
+          #> fold (fn (p, e) => fold (insert (op =)) (vars_of_ipats [p]) #> invent e) cs
+      | invent (IInst (e, lookup)) =
+          invent e
+      | invent (IDictE ms) =
+          fold (invent o snd) ms
+      | invent (ILookup (ls, v)) = error "ILOOKUP"
   in Term.invent_names (fold invent es used) a n end;
 
 
+
 (** language module system - definitions, modules, transactions **)
 
-
-
 (* type definitions *)
 
 datatype def =
@@ -428,7 +466,7 @@
   | Datatypecons of string * itype list
   | Class of string list * string list * string list
   | Classmember of string * string * itype
-  | Classinst of string * (string * string list list) * (string * string) list;
+  | Classinst of string * (string * (vname * string list) list) * (string * string) list;
 
 datatype node = Def of def | Module of node Graph.T;
 type module = node Graph.T;
@@ -478,26 +516,26 @@
       ]
   | pretty_def (Class (supcls, mems, insts)) =
       Pretty.block [
-        Pretty.str "class extending",
+        Pretty.str "class extending ",
         Pretty.gen_list "," "[" "]" (map Pretty.str supcls),
-        Pretty.str "with ",
+        Pretty.str " with ",
         Pretty.gen_list "," "[" "]" (map Pretty.str mems),
-        Pretty.str "instances ",
+        Pretty.str " instances ",
         Pretty.gen_list "," "[" "]" (map Pretty.str insts)
       ]
-  | pretty_def (Classmember (cls, v, ty)) =
+  | pretty_def (Classmember (clsname, v, ty)) =
       Pretty.block [
         Pretty.str "class member belonging to ",
-        Pretty.str cls
+        Pretty.str clsname
       ]
-  | pretty_def (Classinst (cls, (tyco, arity), mems)) =
+  | pretty_def (Classinst (clsname, (tyco, arity), mems)) =
       Pretty.block [
         Pretty.str "class instance (",
-        Pretty.str cls,
+        Pretty.str clsname,
         Pretty.str ", (",
         Pretty.str tyco,
         Pretty.str ", ",
-        Pretty.gen_list "," "[" "]" (map (Pretty.gen_list "," "{" "}" o map Pretty.str) arity),
+        Pretty.gen_list "," "[" "]" (map (Pretty.gen_list "," "{" "}" o map Pretty.str o snd) arity),
         Pretty.str "))"
       ];
 
@@ -658,7 +696,8 @@
       (debug 7 (fn _ => "transformation for datatype constructor " ^ quote name
         ^ " of datatype " ^ quote dtname) ();
       ([([dtname],
-          fn [Datatype (_, _, [])] => NONE | _ => "attempted to add constructor to already instantiating datatype" |> SOME)],
+          fn [Datatype (_, _, [])] => NONE
+            | _ => "attempted to add constructor to already instantiating datatype" |> SOME)],
        [(dtname,
           fn Datatype (vs, cs, clss) => Datatype (vs, name::cs, clss)
            | def => "attempted to add datatype constructor to non-datatype: "
@@ -692,20 +731,16 @@
   | add_check_transform (name, Classinst (clsname, (tyco, arity), memdefs)) =
       let
         val _ = debug 7 (fn _ => "transformation for class instance " ^ quote tyco
-        ^ " of class " ^ quote clsname) ();
+          ^ " of class " ^ quote clsname) ();
         fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] =
               let
-                val _ = writeln "CHECK RUNNING (1)";
-                val mtyp_i' = instant_itype (v, tyco `%%
-                  map2 IVarT ((invent_var_t_names [mtyp_c] (length arity) [] "a"), arity)) mtyp_c;
-                val _ = writeln "CHECK RUNNING (2)";
-              in let val XXX = (
-                 if eq_itype (mtyp_i', mtyp_i) (*! PERHAPS TOO STRICT !*)
-              then NONE
-              else "wrong type signature for class member: "
-                ^ (Pretty.output o pretty_itype) mtyp_i' ^ " expected,"
-                ^ (Pretty.output o pretty_itype) mtyp_i ^ " given" |> SOME
-              ) in (writeln "CHECK RUNNING (3)"; XXX) end end
+                val mtyp_i' = instant_itype (v, tyco `%% map IVarT arity) mtyp_c;
+              in if eq_itype (mtyp_i', mtyp_i)
+                then NONE
+                else "wrong type signature for class member: "
+                  ^ (Pretty.output o pretty_itype) mtyp_i' ^ " expected, "
+                  ^ (Pretty.output o pretty_itype) mtyp_i ^ " given" |> SOME
+              end
           | check defs =
               "non-well-formed definitions encountered for classmembers: "
               ^ (commas o map (quote o Pretty.output o pretty_def)) defs |> SOME
@@ -735,16 +770,15 @@
       let
         fun handle_fail msgs f =
           let
-            fun handl trns =
-              trns |> f
-              handle FAIL exc => (Fail exc, ([], modl))
             in
               if ! soft_exc
               then
-                ([], modl) |> handl
-                handle e => (Fail (msgs, SOME e), ([], modl))
+                ([], modl) |> f
+                handle FAIL exc => (Fail exc, ([], modl))
+                     | e => (Fail (msgs, SOME e), ([], modl))
               else
-                ([], modl) |> handl
+                ([], modl) |> f
+                handle FAIL exc => (Fail exc, ([], modl))
             end;
         fun select msgs [(gname, gen)] =
           handle_fail (msgs @ [mk_msg gname]) (gen src)
@@ -773,7 +807,6 @@
         val (checks, trans) = add_check_transform (name, def);
         fun check (check_defs, checker) modl =
           let
-            val _ = writeln ("CHECK (1): " ^ commas check_defs)
             fun get_def' s =
               if NameSpace.is_qualified s
               then get_def modl s
@@ -781,12 +814,10 @@
             val defs =
               check_defs
               |> map get_def';
-            val _ = writeln ("CHECK (2): " ^ commas check_defs)
           in
-            let val XXX = case checker defs
+            case checker defs
              of NONE => modl
-              | SOME e => raise FAIL ([e], NONE)
-            in (writeln "CHECK (3)"; XXX) end
+              | SOME msg => raise FAIL ([msg], NONE)
           end;
         fun transform (name, f) modl =
           modl
@@ -957,8 +988,12 @@
       let
         val delta = query f - length es;
         val add_n = if delta < 0 then 0 else delta;
+        val tys =
+          (fst o unfold_fun) ty
+          |> curry Library.drop (length es)
+          |> curry Library.take add_n
         val add_vars =
-          invent_var_e_names es add_n [] "x" ~~ Library.drop (length es, (fst o unfold_fun) ty);
+          invent_var_e_names es add_n [] "x" ~~ tys;
       in
         Library.foldr IAbs (add_vars, IConst (f, ty) `$$ es `$$ (map IVarE add_vars))
       end;
@@ -988,7 +1023,7 @@
 
 fun connect_datatypes_clsdecls module =
   let
-    fun extract_dep (name, Datatypecons (dtname, _)) = 
+    fun extract_dep (name, Datatypecons (dtname, _)) =
           [(dtname, name)]
       | extract_dep (name, Classmember (cls, _, _)) =
           [(cls, name)]
@@ -1033,7 +1068,7 @@
     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, members, insts)) =
+    fun transform_dicts (Class (supcls, members, _)) =
           let
             val memberdecls = AList.make
               ((fn Classmember (_, v, ty) => (v, ty)) o get_def module) members;
@@ -1041,13 +1076,12 @@
           in
             Typesyn ([(varname_cls, [])], IDictT (mk_cls_typ_map memberdecls (IVarT (varname_cls, []))))
           end
-      | transform_dicts (Classinst (tyco, (cls, arity), memdefs)) =
+      | transform_dicts (Classinst (clsname, (tyco, arity), memdefs)) =
           let
-            val Class (_, members, _) = get_def module cls;
+            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 (invent_var_t_names (map (snd o snd) memberdecls)
-              (length arity) [] "a" ~~ arity);
+            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;
@@ -1059,45 +1093,57 @@
     fun transform_defs (Fun (ds, (sortctxt, ty))) =
           let
             fun reduce f xs = foldl' f (NONE, xs);
+            val _ = writeln ("class 1");
             val varnames_ctxt =
               sortctxt
               |> length o Library.flat o map snd
               |> (fn used => invent_var_e_names (map snd ds) used ((vars_of_ipats o fst o hd) ds) "d")
               |> unflat (map snd sortctxt);
+            val _ = writeln ("class 2");
             val vname_alist = map2 (fn ((vt, sort), vs) => (vt, vs ~~ sort)) (sortctxt, varnames_ctxt);
+            val _ = writeln ("class 3");
             fun add_typarms ty =
               map (reduce (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 (reduce (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;
-            fun transform_lookup (ClassPackage.Instance ((cdict, idict), ls)) = 
+            val _ = writeln ("class 7");
+            fun transform_lookup (ClassPackage.Instance ((cdict, idict), ls)) =
                   ls
                   |> transform_lookups
-                  |-> (fn ty =>
-                        curry mk_apps (IConst (idict, cdict `%% ty))
-                        #> pair (cdict `%% ty))
+                  |-> (fn tys =>
+                        curry mk_apps (IConst (idict, cdict `%% tys))
+                        #> pair (cdict `%% tys))
               | transform_lookup (ClassPackage.Lookup (deriv, (v, i))) =
                   let
                     val (v', cls) =
                       (nth o the oo AList.lookup (op =)) vname_alist v i;
                     fun mk_parm tyco = tyco `%% [IVarT (v, [])];
-                  in (mk_parm (hd (deriv)), ILookup (rev deriv, v')) end
+                  in (mk_parm cls, ILookup (rev deriv, v')) end
             and transform_lookups lss =
                   map_yield (map_yield transform_lookup
                        #> apfst (reduce (op xx))
                        #> apsnd (reduce (op **))) lss;
+            val _ = writeln ("class 8");
             fun transform_iexpr (IInst (e, ls)) =
-                  transform_iexpr e `$$ (snd o transform_lookups) ls
-              | transform_iexpr e = 
-                  map_iexpr transform_itype transform_ipat transform_iexpr e;
-            fun transform_rhs (ps, rhs) = (add_parms ps, transform_iexpr rhs)
+                  (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
   in
@@ -1174,7 +1220,7 @@
     |> fill_in [] [] module
   end;
 
-fun mk_resolv tab = 
+fun mk_resolv tab =
   let
     fun resolver modl name =
       if NameSpace.is_qualified name then