# HG changeset patch
# User haftmann
# Date 1133535931 -3600
# Node ID 99baddf6b0d01428b68f2693c5d3fe69dfe32129
# Parent  a41ce9c10b738bbcbdeed006a347c138823f8467
various improvements

diff -r a41ce9c10b73 -r 99baddf6b0d0 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Fri Dec 02 16:05:12 2005 +0100
+++ b/src/Pure/Tools/class_package.ML	Fri Dec 02 16:05:31 2005 +0100
@@ -7,10 +7,7 @@
 
 signature CLASS_PACKAGE =
 sig
-  val add_consts: class * xstring list -> theory -> theory
-  val add_consts_i: class * string list -> theory -> theory
-  val add_tycos: class * xstring list -> theory -> theory
-  val add_tycos_i: class * (string * string) list -> theory -> theory
+  val add_classentry: class -> string list -> string list -> theory -> theory
   val the_consts: theory -> class -> string list
   val the_tycos: theory -> class -> (string * string) list
 
@@ -165,7 +162,7 @@
 fun get_const_sign thy tvar const =
   let
     val class = (the o lookup_const_class thy) const;
-    val ty = (Type.unvarifyT o Sign.the_const_constraint thy) const;
+    val (ty, thaw) = (Type.freeze_thaw_type o Sign.the_const_constraint thy) const;
     val tvars_used = Term.add_tfreesT ty [];
     val tvar_rename = hd (Term.invent_names (map fst tvars_used) tvar 1);
   in
@@ -174,8 +171,9 @@
           if Sorts.sort_eq (Sign.classes_of thy) ([class], sort)
           then TFree (tvar, [])
           else if tvar' = tvar
-          then TFree (tvar_rename, sort)
+          then TVar ((tvar_rename, 0), sort)
           else TFree (tvar', sort))
+    |> thaw
   end;
 
 fun get_inst_consts_sign thy (tyco, class) =
@@ -188,7 +186,7 @@
     val vars_new = Term.invent_names vars_used "'a" (length arities);
     val typ_arity = Type (tyco, map2 (curry TFree) vars_new arities);
     val instmem_signs =
-      map (typ_subst_atomic [(TFree ("'a", []), typ_arity)]) const_signs;
+      map (typ_subst_TVars [(("'a", 0), typ_arity)]) const_signs;
   in consts ~~ instmem_signs end;
 
 fun get_classtab thy =
@@ -202,8 +200,8 @@
 
 type sortcontext = (string * sort) list;
 
-fun extract_sortctxt thy typ =
-  (typ_tfrees o Type.unvarifyT) typ
+fun extract_sortctxt thy ty =
+  (typ_tfrees o Type.no_tvars) ty
   |> map (apsnd (filter_class thy))
   |> filter (not o null o snd);
 
@@ -235,7 +233,7 @@
               in Lookup (deriv, (vname, classindex)) end;
           in map mk_look sort_def end;
   in
-    extract_sortctxt thy raw_typ_def
+    extract_sortctxt thy ((fst o Type.freeze_thaw_type) raw_typ_def)
     |> map (tab_lookup o fst)
     |> map (apfst (filter_class thy))
     |> filter (not o null o fst)
@@ -243,18 +241,9 @@
   end;
 
 
-(* outer syntax *)
-
-local
+(* intermediate auxiliary *)
 
-structure P = OuterParse
-and K = OuterKeyword;
-
-in
-
-val classcgK = "codegen_class";
-
-fun classcg raw_class raw_consts raw_tycos thy =
+fun add_classentry raw_class raw_consts raw_tycos thy =
   let
     val class = Sign.intern_class thy raw_class;
   in
@@ -267,22 +256,8 @@
        }
     |> add_consts (class, raw_consts)
     |> add_tycos (class, raw_tycos)
-  end
-
-val classcgP =
-  OuterSyntax.command classcgK "codegen data for classes" K.thy_decl (
-    P.xname
-    -- ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name))
-    -- (Scan.optional ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name)) [])
-    >> (fn ((name, tycos), consts) => (Toplevel.theory (classcg name consts tycos)))
-  )
-
-val _ = OuterSyntax.add_parsers [classcgP];
-
-val _ = OuterSyntax.add_keywords ["\\<Rightarrow>", "=>"];
-
-end; (* local *)
-
+  end;
+  
 
 (* setup *)
 
diff -r a41ce9c10b73 -r 99baddf6b0d0 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Fri Dec 02 16:05:12 2005 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Fri Dec 02 16:05:31 2005 +0100
@@ -12,11 +12,10 @@
 signature CODEGEN_PACKAGE =
 sig
   type deftab;
-  type exprgen_type;
   type exprgen_term;
+  type appgen;
   type defgen;
-  val add_codegen_type: string * exprgen_type -> theory -> theory;
-  val add_codegen_expr: string * exprgen_term -> theory -> theory;
+  val add_appgen: string * appgen -> theory -> theory;
   val add_defgen: string * defgen -> theory -> theory;
   val add_lookup_tyco: string * string -> theory -> theory;
   val add_lookup_const: (string * typ) * CodegenThingol.iexpr -> theory -> theory;
@@ -53,18 +52,23 @@
   val ensure_def_const: theory -> deftab
     -> string -> CodegenThingol.transact -> string * CodegenThingol.transact;
 
-  val codegen_let: (int -> term -> term list * term)
-    -> exprgen_term;
-  val codegen_split: (int -> term -> term list * term)
-    -> exprgen_term;
-  val codegen_number_of: (term -> IntInf.int) -> (term -> term)
-    -> exprgen_term;
-  val codegen_case: (theory -> string -> (string * int) list option)
-    -> exprgen_term;
+  val appgen_let: (int -> term -> term list * term)
+    -> appgen;
+  val appgen_split: (int -> term -> term list * term)
+    -> appgen;
+  val appgen_number_of: (term -> IntInf.int) -> (term -> term)
+    -> appgen;
+  val appgen_case: (theory -> string -> (string * int) list option)
+    -> appgen;
   val defgen_datatype: (theory -> string -> (string 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)
+    -> defgen;
+  val defgen_datatype_eqinst: (theory -> string -> (string list * string list) option)
+    -> defgen;
   val defgen_recfun: (theory -> string * typ -> (term list * term) list * typ)
     -> defgen;
 
@@ -81,7 +85,8 @@
 
 (* auxiliary *)
 
-fun perhaps f x = f x |> the_default x;
+fun devarify_term t = (fst o Type.freeze_thaw) t;
+fun devarify_type ty = (fst o Type.freeze_thaw_type) ty;
 
 
 (* code generator instantiation, part 1 *)
@@ -101,6 +106,7 @@
 type exprgen_sort = theory -> deftab -> (sort, sort) gen_exprgen;
 type exprgen_type = theory -> deftab -> (typ, itype) gen_exprgen;
 type exprgen_term = theory -> deftab -> (term, iexpr) gen_exprgen;
+type appgen = theory -> deftab -> ((string * typ) * term list, iexpr) gen_exprgen;
 type defgen = theory -> deftab -> gen_defgen;
 
 
@@ -140,29 +146,31 @@
   exprgens_sort: (string * (exprgen_sort * stamp)) list,
   exprgens_type: (string * (exprgen_type * stamp)) list,
   exprgens_term: (string * (exprgen_term * stamp)) list,
+  appgens: (string * (appgen * stamp)) list,
   defgens: (string * (defgen * stamp)) list
 };
 
 val empty_gens = {
   exprgens_sort = Symtab.empty, exprgens_type = Symtab.empty,
-  exprgens_term = Symtab.empty, defgens = Symtab.empty
+  exprgens_term = Symtab.empty, defgens = Symtab.empty, appgens = Symtab.empty
 };
 
-fun map_gens f { exprgens_sort, exprgens_type, exprgens_term, defgens } =
+fun map_gens f { exprgens_sort, exprgens_type, exprgens_term, appgens, defgens } =
   let
-    val (exprgens_sort, exprgens_type, exprgens_term, defgens) =
-      f (exprgens_sort, exprgens_type, exprgens_term, defgens)
+    val (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) =
+      f (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens)
   in { exprgens_sort = exprgens_sort, exprgens_type = exprgens_type,
-       exprgens_term = exprgens_term, defgens = defgens } end;
+       exprgens_term = exprgens_term, appgens = appgens, defgens = defgens } end;
 
 fun merge_gens
   ({ exprgens_sort = exprgens_sort1, exprgens_type = exprgens_type1,
-     exprgens_term = exprgens_term1, defgens = defgens1 },
+     exprgens_term = exprgens_term1, appgens = appgens1, defgens = defgens1 },
    { exprgens_sort = exprgens_sort2, exprgens_type = exprgens_type2,
-     exprgens_term = exprgens_term2, defgens = defgens2 }) =
+     exprgens_term = exprgens_term2, appgens = appgens2, defgens = defgens2 }) =
   { exprgens_sort = AList.merge (op =) (eq_snd (op =)) (exprgens_sort1, exprgens_sort2),
     exprgens_type = AList.merge (op =) (eq_snd (op =)) (exprgens_type1, exprgens_type2),
     exprgens_term = AList.merge (op =) (eq_snd (op =)) (exprgens_term1, exprgens_term2),
+    appgens = AList.merge (op =) (eq_snd (op =)) (appgens1, appgens2),
     defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2) } : gens;
 
 type lookups = {
@@ -247,7 +255,7 @@
   };
   val empty = {
     modl = empty_module,
-    gens = { exprgens_sort = [], exprgens_type = [], exprgens_term = [], defgens = [] } : gens,
+    gens = { exprgens_sort = [], exprgens_type = [], exprgens_term = [], appgens = [], defgens = [] } : gens,
     lookups = { lookups_tyco = Symtab.empty, lookups_const = Symtab.empty } : lookups,
     logic_data = { is_datatype = NONE, alias = (Symtab.empty, Symtab.empty) } : logic_data,
     serialize_data =
@@ -261,7 +269,10 @@
               |> CodegenSerializer.add_prim ("wfrec", ("fun wfrec f x = f (wfrec f) x;", [])),
             syntax_tyco = Symtab.empty, syntax_const = Symtab.empty })
       |> Symtab.update ("haskell",
-          { serializer = serializer_hs : CodegenSerializer.serializer, primitives = CodegenSerializer.empty_prims,
+          { serializer = serializer_hs : CodegenSerializer.serializer,
+            primitives =
+              CodegenSerializer.empty_prims
+              |> CodegenSerializer.add_prim ("wfrec", ("wfrec f x = f (wfrec f) x", [])),
             syntax_tyco = Symtab.empty, syntax_const = Symtab.empty })
   } : T;
   val copy = I;
@@ -297,43 +308,54 @@
     (fn (modl, gens, lookups, serialize_data, logic_data) =>
        (modl,
         gens |> map_gens
-          (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) =>
+          (fn (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) =>
             (exprgens_sort
              |> Output.update_warn (op =) ("overwriting existing class code generator " ^ name) (name, (cg, stamp ())),
-             exprgens_type, exprgens_term, defgens)), lookups, serialize_data, logic_data));
+             exprgens_type, exprgens_term, appgens, defgens)), lookups, serialize_data, logic_data));
 
 fun add_codegen_type (name, cg) =
   map_codegen_data
     (fn (modl, gens, lookups, serialize_data, logic_data) =>
        (modl,
         gens |> map_gens
-          (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) =>
+          (fn (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) =>
             (exprgens_sort,
              exprgens_type
              |> Output.update_warn (op =) ("overwriting existing type code generator " ^ name) (name, (cg, stamp ())),
-             exprgens_term, defgens)), lookups, serialize_data, logic_data));
+             exprgens_term, appgens, defgens)), lookups, serialize_data, logic_data));
 
 fun add_codegen_expr (name, cg) =
   map_codegen_data
     (fn (modl, gens, lookups, serialize_data, logic_data) =>
        (modl,
         gens |> map_gens
-          (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) =>
+          (fn (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) =>
             (exprgens_sort, exprgens_type,
         exprgens_term
              |> Output.update_warn (op =) ("overwriting existing expression code generator " ^ name) (name, (cg, stamp ())),
-             defgens)),
+             appgens, defgens)),
              lookups, serialize_data, logic_data));
 
+fun add_appgen (name, ag) =
+  map_codegen_data
+    (fn (modl, gens, lookups, serialize_data, logic_data) =>
+       (modl,
+        gens |> map_gens
+          (fn (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) =>
+            (exprgens_sort, exprgens_type, exprgens_term,
+             appgens
+             |> Output.update_warn (op =) ("overwriting existing definition application generator " ^ name) (name, (ag, stamp ())),
+             defgens)), lookups, serialize_data, logic_data));
+
 fun add_defgen (name, dg) =
   map_codegen_data
     (fn (modl, gens, lookups, serialize_data, logic_data) =>
        (modl,
         gens |> map_gens
-          (fn (exprgens_sort, exprgens_type, exprgens_term, defgens) =>
+          (fn (exprgens_sort, exprgens_type, exprgens_term, appgens, defgens) =>
             (exprgens_sort, exprgens_type, exprgens_term,
-             defgens
-             |> Output.update_warn (op =) ("overwriting existing definition code generator " ^ name) (name, (dg, stamp ())))),
+             appgens, defgens
+             |> Output.update_warn (op =) ("overwriting existing definition definition generator " ^ name) (name, (dg, stamp ())))),
              lookups, serialize_data, logic_data));
 
 val get_lookups_tyco = #lookups_tyco o #lookups o CodegenData.get;
@@ -450,17 +472,6 @@
     | s => s;
 
 
-(* auxiliary *)
-
-fun find_lookup_expr thy (f, ty) =
-  Symtab.lookup_multi ((#lookups_const o #lookups o CodegenData.get) thy) f
-  |> (fn tab => AList.lookup (Sign.typ_instance thy) tab ty)
-
-fun name_of_tvar (TFree (v, _)) = v |> unprefix "'"
-  | name_of_tvar (TVar ((v, i), _)) =
-      (if i=0 then v else v ^ string_of_int i) |> unprefix "'"
-
-
 (* code generator instantiation, part 2 *)
 
 fun invoke_cg_sort thy defs sort trns =
@@ -478,14 +489,30 @@
     ((map (apsnd (fn (cg, _) => cg thy defs)) o #exprgens_term o #gens o CodegenData.get) thy)
     ("generating expression " ^ (quote o Sign.string_of_term thy) t) t trns;
 
+fun invoke_appgen thy defs (app as ((f, ty), ts)) trns =
+  gen_invoke
+    ((map (apsnd (fn (ag, _) => ag thy defs)) o #appgens o #gens o CodegenData.get) thy)
+    ("generating application " ^ f ^ "::" ^ (Sign.string_of_typ thy) ty
+     ^ " " ^ enclose "(" ")" (commas (map (Sign.string_of_term thy) ts))) app trns;
+
+fun find_lookup_expr thy (f, ty) =
+  Symtab.lookup_multi ((#lookups_const o #lookups o CodegenData.get) thy) f
+  |> (fn tab => AList.lookup (Sign.typ_instance thy) tab ty);
+
 fun get_defgens thy defs =
   (map (apsnd (fn (dg, _) => dg thy defs)) o #defgens o #gens o CodegenData.get) thy;
 
-fun ensure_def_class thy defs cls_or_inst trns =
+fun ensure_def_class thy defs cls trns =
   trns
-  |> debug 4 (fn _ => "generating class or instance " ^ quote cls_or_inst)
-  |> gen_ensure_def (get_defgens thy defs) ("generating class/instance " ^ quote cls_or_inst) cls_or_inst
-  |> pair cls_or_inst;
+  |> debug 4 (fn _ => "generating class " ^ quote cls)
+  |> gen_ensure_def (get_defgens thy defs) ("generating class " ^ quote cls) cls
+  |> pair cls;
+
+fun ensure_def_instance thy defs inst trns =
+  trns
+  |> debug 4 (fn _ => "generating instance " ^ quote inst)
+  |> gen_ensure_def (get_defgens thy defs) ("generating instance " ^ quote inst) inst
+  |> pair inst;
 
 fun ensure_def_tyco thy defs tyco trns =
   if NameSpace.is_qualified tyco
@@ -506,9 +533,9 @@
    of NONE =>
         trns
         |> debug 4 (fn _ => "generating constant " ^ quote f)
-        |> invoke_cg_type thy defs (cname_of_idf thy defs f |> the |> snd)
+        |> invoke_cg_type thy defs (cname_of_idf thy defs f |> the |> snd |> devarify_type)
         ||> gen_ensure_def (get_defgens thy defs) ("generating constant " ^ quote f) f
-        |-> (fn ty' => pair f)
+        |-> (fn _ => pair f)
     | SOME (IConst (f, ty)) =>
         trns
         |> pair f
@@ -523,29 +550,34 @@
       |-> (fn sort => pair (unprefix "'" v, sort))
     fun mk_eq (args, rhs) trns =
       trns
-      |> fold_map (invoke_cg_expr thy defs) args
-      ||>> invoke_cg_expr thy defs rhs
+      |> fold_map (invoke_cg_expr thy defs o devarify_term) args
+      ||>> (invoke_cg_expr thy defs o devarify_term) rhs
       |-> (fn (args, rhs) => pair (map ipat_of_iexpr args, rhs))
   in
     trns
     |> fold_map mk_eq eqs
-    ||>> invoke_cg_type thy defs ty
+    ||>> invoke_cg_type thy defs (devarify_type ty)
     ||>> fold_map mk_sortvar sortctxt
     |-> (fn ((eqs, ty), sortctxt) => pair (Fun (eqs, (sortctxt, ty))))
   end;
 
-fun fix_nargs thy defs gen i (t, ts) trns =
-  if length ts < i
-  then
+fun fix_nargs thy defs gen (imin, imax) (t, ts) trns =
+  if length ts < imin then
     trns
     |> debug 10 (fn _ => "eta-expanding")
-    |> gen (strip_comb (Codegen.eta_expand t ts i))
+    |> gen (strip_comb (Codegen.eta_expand t ts imin))
+    |-> succeed
+  else if length ts > imax then
+    trns
+    |> debug 10 (fn _ => "splitting arguments (" ^ string_of_int imax ^ ", " ^ string_of_int (length ts) ^ ")")
+    |> gen (t, Library.take (imax, ts))
+    ||>> fold_map (invoke_cg_expr thy defs) (Library.drop (imax, ts))
+    |-> succeed o mk_apps
   else
     trns
-    |> debug 10 (fn _ => "splitting arguments (" ^ string_of_int i ^ ", " ^ string_of_int (length ts) ^ ")")
-    |> gen (t, Library.take (i, ts))
-    ||>> fold_map (invoke_cg_expr thy defs) (Library.drop (i, ts))
-    |-> pair o mk_apps;
+    |> debug 10 (fn _ => "keeping arguments")
+    |> gen (t, ts)
+    |-> succeed;
 
 local
   open CodegenThingolOp;
@@ -566,14 +598,12 @@
        (sort |> filter (ClassPackage.is_class thy) |> map (idf_of_name thy nsp_class))
   |-> (fn sort => succeed sort)
 
-fun exprgen_type_default thy defs(v as TVar (_, sort)) trns =
+fun exprgen_type_default thy defs (TVar _) trns =
+      error "TVar encountered during code generation"
+  | exprgen_type_default thy defs (TFree (v, sort)) trns =
       trns
       |> invoke_cg_sort thy defs sort
-      |-> (fn sort => succeed (IVarT (name_of_tvar v, sort)))
-  | exprgen_type_default thy defs (v as TFree (_, sort)) trns =
-      trns
-      |> invoke_cg_sort thy defs sort
-      |-> (fn sort => succeed (IVarT (name_of_tvar v, sort)))
+      |-> (fn sort => succeed (IVarT (v |> unprefix "'", sort)))
   | exprgen_type_default thy defs (Type ("fun", [t1, t2])) trns =
       trns
       |> invoke_cg_type thy defs t1
@@ -586,53 +616,85 @@
       |-> (fn (tyco, tys) => succeed (tyco `%% tys))
 
 fun exprgen_term_default thy defs (Const (f, ty)) trns =
-      let
-        val _ = debug 5 (fn _ => "making application of " ^ quote f) ();
-        val ty_def = Sign.the_const_constraint thy f;
-        val _ = debug 10 (fn _ => "making application (2)") ();
-        fun mk_lookup (ClassPackage.Instance (i, ls)) trns =
-              trns
-              |> ensure_def_class thy defs ((idf_of_name thy nsp_class o fst) i)
-              ||>> ensure_def_class thy defs (idf_of_inst thy defs i)
-              ||>> (fold_map o fold_map) mk_lookup ls
-              |-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls)))
-          | mk_lookup (ClassPackage.Lookup (clss, (v, i))) trns =
-              trns
-              |> fold_map (ensure_def_class thy defs) (map (idf_of_name thy nsp_class) clss)
-              |-> (fn clss => pair (ClassPackage.Lookup (clss, (name_of_tvar (TFree (v, [])), i))));
-        val _ = debug 10 (fn _ => "making application (3)") ();
-        fun mk_itapp e [] = e
-          | mk_itapp e lookup = IInst (e, lookup);
-      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))
-        |> debug 10 (fn _ => "making application (5)")
-        ||>> (fold_map o fold_map) mk_lookup (ClassPackage.extract_sortlookup thy (ty_def, ty))
-        |> debug 10 (fn _ => "making application (6)")
-        ||>> invoke_cg_type thy defs ty
-        |> debug 10 (fn _ => "making application (7)")
-        |-> (fn ((f, lookup), ty) =>
-               succeed (mk_itapp (IConst (f, ty)) lookup))
-      end
+      trns
+      |> invoke_appgen thy defs ((f, ty), [])
+      |-> (fn e => succeed e)
+  | exprgen_term_default thy defs (Var ((v, i), ty)) trns =
+      trns
+      |> invoke_cg_type thy defs ty
+      |-> (fn ty => succeed (IVarE (if i = 0 then v else v ^ "_" ^ string_of_int i, ty)))
   | exprgen_term_default thy defs (Free (v, ty)) trns =
       trns
       |> invoke_cg_type thy defs ty
       |-> (fn ty => succeed (IVarE (v, ty)))
-  | exprgen_term_default thy defs (Var ((v, i), ty)) trns =
-      trns
-      |> invoke_cg_type thy defs ty
-      |-> (fn ty => succeed (IVarE (if i=0 then v else v ^ string_of_int i, ty)))
   | exprgen_term_default thy defs (Abs (v, ty, t)) trns =
       trns
       |> invoke_cg_type thy defs ty
       ||>> invoke_cg_expr thy defs (subst_bound (Free (v, ty), t))
       |-> (fn (ty, e) => succeed ((v, ty) `|-> e))
-  | exprgen_term_default thy defs (t1 $ t2) trns =
+  | exprgen_term_default thy defs (t as t1 $ t2) trns =
+      let
+        val (t', ts) = strip_comb t
+      in case t'
+       of Const (f, ty) =>
+            trns
+            |> invoke_appgen thy defs ((f, ty), ts)
+            |-> (fn e => succeed e)
+        | _ =>
+            trns
+            |> invoke_cg_expr thy defs t'
+            ||>> fold_map (invoke_cg_expr thy defs) ts
+            |-> (fn (e, es) => succeed (e `$$ es))
+      end;
+
+fun appgen_default thy defs ((f, ty), ts) trns =
+  let
+    val _ = debug 5 (fn _ => "making application of " ^ quote f) ();
+    val ty_def = Sign.the_const_constraint thy f;
+    val _ = debug 10 (fn _ => "making application (2)") ();
+    fun mk_lookup (ClassPackage.Instance (i, ls)) trns =
+          trns
+          |> ensure_def_class thy defs ((idf_of_name thy nsp_class o fst) i)
+          ||>> ensure_def_instance thy defs (idf_of_inst thy defs i)
+          ||>> (fold_map o fold_map) mk_lookup ls
+          |-> (fn ((cls, i), ls) => pair (ClassPackage.Instance ((cls, i), ls)))
+      | mk_lookup (ClassPackage.Lookup (clss, (v, i))) trns =
+          trns
+          |> fold_map (ensure_def_class thy defs) (map (idf_of_name thy nsp_class) clss)
+          |-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i))));
+    val _ = debug 10 (fn _ => "making application (3)") ();
+    fun mk_itapp e [] = e
+      | mk_itapp e lookup = IInst (e, lookup);
+  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))
+    ||> debug 10 (fn _ => "making application (5)")
+    ||>> (fold_map o fold_map) mk_lookup (ClassPackage.extract_sortlookup thy (ty_def, ty))
+    ||> debug 10 (fn _ => "making application (6)")
+    ||>> invoke_cg_type thy defs ty
+    ||> debug 10 (fn _ => "making application (7)")
+    ||>> fold_map (invoke_cg_expr thy defs) ts
+    ||> debug 10 (fn _ => "making application (8)")
+    |-> (fn (((f, lookup), ty), es) =>
+           succeed (mk_itapp (IConst (f, ty)) lookup `$$ es))
+  end
+
+fun appgen_neg thy defs (f as ("neg", Type ("fun", [ty, _])), ts) trns =
+      let
+        fun gen_neg _ trns =
+          trns
+          |> invoke_cg_expr thy defs (Const ("op >", ty --> ty --> Type ("bool", [])) $ Const ("0", ty))
+      in
+        trns
+        |> fix_nargs thy defs gen_neg (0, 0) (Const f, ts)
+      end
+  | appgen_neg thy defs ((f, _), _) trns =
       trns
-      |> invoke_cg_expr thy defs t1
-      ||>> invoke_cg_expr thy defs t2
-      |-> (fn (e1, e2) => succeed (e1 `$ e2));
+      |> fail ("not a negation: " ^ quote f);
+
+fun exprgen_term_eq thy defs (Const ("op =", Type ("fun", [ty, _]))) trns =
+  trns
 
 (*fun codegen_eq thy defs t trns =
  let
@@ -650,18 +712,6 @@
          |> fail ("no equality: " ^ Sign.string_of_term thy t)
   in cg_eq (strip_comb t) end;*)
 
-fun codegen_neg thy defs t trns =
-  let
-    val (u, ts) = strip_comb t;
-    fun cg_neg (Const ("neg", _)) =
-         trns
-         |> invoke_cg_expr thy defs (hd ts)
-         |-> (fn e => succeed (Fun_lt `$ e `$ IConst ("0", Type_integer)))
-      | cg_neg _ =
-         trns
-         |> fail ("no negation: " ^ Sign.string_of_term thy t)
-  in cg_neg u end;
-
 
 (* definition generators *)
 
@@ -692,7 +742,7 @@
    of SOME (args, rhs, ty) =>
         trns
         |> debug 5 (fn _ => "trying defgen def for " ^ quote f)
-        |> mk_fun thy defs [(args, rhs)] ty
+        |> mk_fun thy defs [(args, rhs)] (devarify_type ty)
         |-> (fn def => succeed (def, []))
       | _ => trns |> fail ("no definition found for " ^ quote f);
 
@@ -721,7 +771,7 @@
         in
           trns
           |> debug 5 (fn _ => "trying defgen class member for " ^ quote f)
-          |> invoke_cg_type thy defs ty
+          |> (invoke_cg_type thy defs o devarify_type) ty
           |-> (fn ty => succeed (Classmember (cls, "a", ty), []))
         end
     | _ =>
@@ -731,16 +781,22 @@
   case inst_of_idf thy defs clsinst
    of SOME (cls, tyco) =>
         let
+          val _ = debug 10 (fn _ => "(1) CLSINST " ^ cls ^ " - " ^ tyco) ()
           val arity = (map o map) (idf_of_name thy nsp_class)
             (ClassPackage.get_arities thy [cls] tyco);
+          val _ = debug 10 (fn _ => "(2) CLSINST " ^ cls ^ " - " ^ tyco) ()
           val clsmems = map (idf_of_name thy nsp_mem)
             (ClassPackage.the_consts thy cls);
+          val _ = debug 10 (fn _ => "(3) CLSINST " ^ cls ^ " - " ^ tyco) ()
+          val _ = debug 10 (fn _ => AList.string_of_alist I (Sign.string_of_typ thy) (ClassPackage.get_inst_consts_sign thy (tyco, 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)) =
+          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 univ)
+              (map ((fn Classmember (_, _, ty) => ty) o get_def modl)
               clsmems |> tvars_of_itypes) "a" (length arity) ~~ arity, clsmems), trns)
+          val _ = debug 10 (fn _ => "(5) CLSINST " ^ cls ^ " - " ^ tyco) ()
         in
           trns
           |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")")
@@ -759,69 +815,82 @@
 
 (* parametrized generators, for instantiation in HOL *)
 
-fun codegen_let strip_abs thy defs t trns =
-  let
-    fun dest_let (l as Const ("Let", _) $ t $ u) =
-          (case strip_abs 1 u
-           of ([p], u') => apfst (cons (p, t)) (dest_let u')
-            | _ => ([], l))
-      | dest_let t = ([], t);
-    fun mk_let (l, r) trns =
-      trns
-      |> invoke_cg_expr thy defs l
-      ||>> invoke_cg_expr thy defs r
-      |-> (fn (l, r) => pair (r, ipat_of_iexpr l));
-    fun cg_let' ([], _) _ =
+fun appgen_let strip_abs thy defs (f as ("Let", _), ts) trns =
+      let
+        fun dest_let (l as Const ("Let", _) $ t $ u) =
+              (case strip_abs 1 u
+               of ([p], u') => apfst (cons (p, t)) (dest_let u')
+                | _ => ([], l))
+          | dest_let t = ([], t);
+        fun mk_let (l, r) trns =
           trns
-          |> fail ("no let expression: " ^ Sign.string_of_term thy t)
-      | cg_let' (lets, body) args =
-          trns
-          |> fold_map mk_let lets
-          ||>> invoke_cg_expr thy defs body
-          ||>> fold_map (invoke_cg_expr thy defs) args
-          |-> (fn ((lets, body), args) =>
-               succeed (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body) `$$ args))
-    fun cg_let (t1 as Const ("Let", _), t2 :: t3 :: ts) =
-          cg_let' (dest_let (t1 $ t2 $ t3)) ts
-      | cg_let _ =
-          trns
-          |> fail ("no let expression: " ^ Sign.string_of_term thy t);
-  in cg_let (strip_comb t) end;
+          |> invoke_cg_expr thy defs l
+          ||>> invoke_cg_expr thy defs r
+          |-> (fn (l, r) => pair (r, ipat_of_iexpr l));
+        fun gen_let (t1, [t2, t3]) trns =
+          let
+            val (lets, body) = dest_let (t1 $ t2 $ t3)
+          in
+            trns
+            |> fold_map mk_let lets
+            ||>> invoke_cg_expr thy defs body
+            |-> (fn (lets, body) =>
+                 pair (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body)))
+          end;
+      in
+        trns
+        |> fix_nargs thy defs gen_let (2, 2) (Const f, ts)
+      end
+  | appgen_let strip_abs thy defs ((f, _), _) trns =
+      trns
+      |> fail ("not a let: " ^ quote f);
 
-fun codegen_split strip_abs thy defs t trns =
-  let
-    fun cg_split' ([p], body) args =
-          trns
-          |> invoke_cg_expr thy defs p
-          ||>> invoke_cg_expr thy defs body
-          ||>> fold_map (invoke_cg_expr thy defs) args
-          |-> (fn (((IVarE v), body), args) => succeed (IAbs (v, body) `$$ args))
-      | cg_split' _ _ =
-          trns
-          |> fail ("no split expression: " ^ Sign.string_of_term thy t);
-    fun cg_split (t1 as Const ("split", _), t2 :: ts) =
-          cg_split' (strip_abs 1 (t1 $ t2)) ts
-      | cg_split _ =
+fun appgen_split strip_abs thy defs (f as ("split", _), ts) trns =
+      let
+        fun gen_split (t1, [t2]) trns =
+          let
+            val ([p], body) = strip_abs 1 (t1 $ t2)
+          in
+            trns
+            |> invoke_cg_expr thy defs p
+            ||>> invoke_cg_expr thy defs body
+            |-> (fn (IVarE v, body) => pair (IAbs (v, body)))
+          end
+      in
+        trns
+        |> fix_nargs thy defs gen_split (1, 1) (Const f, ts)
+      end
+  | appgen_split strip_abs thy defs ((f, _), _) trns =
+      trns
+      |> fail ("not a split: " ^ quote f);
+
+fun appgen_number_of dest_binum mk_int_to_nat thy defs (f as ("Numeral.number_of",
+      Type ("fun", [_, Type ("IntDef.int", [])])), ts) trns =
+      let
+        fun gen_num (_, [bin]) trns =
           trns
-          |> fail ("no split expression: " ^ Sign.string_of_term thy t);
-  in cg_split (strip_comb t) end;
-
-fun codegen_number_of dest_binum mk_int_to_nat thy defs (Const ("Numeral.number_of",
-      Type ("fun", [_, Type ("IntDef.int", [])])) $ bin) trns =
+          |> (pair (IConst ((IntInf.toString o dest_binum) bin, Type_integer))
+              handle TERM _
+              => error ("not a number: " ^ Sign.string_of_term thy bin))
+      in
+        trns
+        |> fix_nargs thy defs gen_num (1, 1) (Const f, ts)
+      end
+  | appgen_number_of dest_binum mk_int_to_nat thy defs (f as ("Numeral.number_of",
+      Type ("fun", [_, Type ("nat", [])])), ts) trns =
+      let
+        fun gen_num (_, [bin]) trns =
+          trns
+          |> invoke_cg_expr thy defs (mk_int_to_nat bin)
+      in
+        trns
+        |> fix_nargs thy defs gen_num (1, 1) (Const f, ts)
+      end
+  | appgen_number_of dest_binum mk_int_to_nat thy defs ((f, _), _) trns =
       trns
-      |> (succeed (IConst ((IntInf.toString o dest_binum) bin, Type_integer))
-          handle TERM _
-          => fail ("not a number: " ^ Sign.string_of_term thy bin))
-  | codegen_number_of dest_binum mk_int_to_nat thy defs (Const ("Numeral.number_of",
-      Type ("fun", [_, Type ("nat", [])])) $ bin) trns =
-      trns
-      |> invoke_cg_expr thy defs (mk_int_to_nat bin)
-      |-> (fn expr => succeed expr)
-  | codegen_number_of dest_binum mk_int_to_nat thy defs t trns =
-      trns
-      |> fail ("not a number: " ^ Sign.string_of_term thy t);
+      |> fail ("not a number_of: " ^ quote f);
 
-fun codegen_case get_case_const_data thy defs t trns =
+fun appgen_case get_case_const_data thy defs ((f, ty), ts) trns =
   let
     fun cg_case_d gen_names dty (((cname, i), ty), t) trns =
       let
@@ -849,42 +918,47 @@
         ||>> fold_map (cg_case_d gen_names dty) (cs ~~ ts')
         |-> (fn (t, ds) => pair (ICase (t, ds)))
       end;
-  in case strip_comb t
-   of (t as Const (f, ty), ts) =>
-        (case get_case_const_data thy f
-         of NONE =>
-              trns
-              |> fail ("not a case constant: " ^ quote f)
-          | SOME cs =>
-              let
-                val (tys, dty) = (split_last o fst o strip_type) ty;
-              in
-                trns
-                |> debug 9 (fn _ => "for case const " ^ f ^ "::"
-                     ^ Sign.string_of_typ thy ty ^ ",\n  with " ^ AList.string_of_alist I string_of_int cs
-                     ^ ",\n  given as args " ^ (commas o map (Sign.string_of_term thy)) ts
-                     ^ ",\n  with significant length " ^ string_of_int (length cs + 1))
-                |> fix_nargs thy defs (cg_case dty (cs ~~ tys))
-                     (length cs + 1) (t, ts)
-                |-> succeed
-              end
-        )
-    | _ =>
-        trns
-        |> fail ("not a caseconstant expression: " ^ Sign.string_of_term thy t)
+  in 
+    case get_case_const_data thy f
+     of NONE =>
+          trns
+          |> fail ("not a case constant: " ^ quote f)
+      | SOME cs =>
+          let
+            val (tys, dty) = (split_last o fst o strip_type) ty;
+          in
+            trns
+            |> debug 9 (fn _ => "for case const " ^ f ^ "::"
+                 ^ Sign.string_of_typ thy ty ^ ",\n  with " ^ AList.string_of_alist I string_of_int cs
+                 ^ ",\n  given as args " ^ (commas o map (Sign.string_of_term thy)) ts
+                 ^ ",\n  with significant length " ^ string_of_int (length cs + 1))
+            |> fix_nargs thy defs (cg_case dty (cs ~~ tys))
+                 (length cs + 1, length cs + 1) (Const (f, ty), ts)
+          end
   end;
 
-fun defgen_datatype get_datatype thy defs tyco trns =
+local
+
+fun add_eqinst get_datacons thy modl dtname cnames =
+  if forall (is_eqtype modl)
+    (Library.flat (map (fn cname => get_datacons thy (cname, dtname)) cnames))
+  then append [idf_of_name thy nsp_eq_class dtname]
+  else I
+
+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 tyco
+        (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))
+                   |> map (fn "0" => "const.Zero" | c => c)
+                   (* |> add_eqinst get_datacons thy (snd trns) dtname cnames *))
               (*! VARIABLEN, EQTYPE !*)
           | NONE =>
               trns
@@ -894,6 +968,8 @@
         |> fail ("not a type constructor: " ^ quote tyco)
   end;
 
+end; (* local *)
+
 fun defgen_datacons get_datacons thy defs f trns =
   let
     fun the_type "0" = SOME "nat"
@@ -911,7 +987,7 @@
                        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) tyargs
+                       ||>> fold_map (invoke_cg_type thy defs o devarify_type) tyargs
                        |-> (fn (dtname, tys) => succeed (Datatypecons (dtname, tys), []))
                     | NONE =>
                        trns
@@ -924,6 +1000,42 @@
           |> fail ("not a constant: " ^ quote f)
   end;
 
+fun defgen_datatype_eq get_datatype thy defs f trns =
+  case name_of_idf thy nsp_eq f
+   of SOME dtname =>
+        (case get_datatype thy dtname
+         of SOME (_, cnames) =>
+              trns
+              |> debug 5 (fn _ => "trying defgen datatype_eq for " ^ quote dtname)
+              |> ensure_def_tyco thy defs (idf_of_tname thy dtname)
+              ||>> fold_map (ensure_def_const thy defs) (cnames
+                   |> map (idf_of_name thy nsp_const)
+                   |> map (fn "0" => "const.Zero" | c => c))
+              ||>> `(fn (_, modl) => build_eqpred modl dtname)
+              |-> (fn (_, eqpred) => succeed (eqpred, []))
+          | NONE =>
+              trns
+              |> fail ("no datatype found for " ^ quote dtname))
+    | NONE =>
+        trns
+        |> fail ("not an equality predicate: " ^ quote f)
+
+fun defgen_datatype_eqinst get_datatype thy defs f trns =
+  case name_of_idf thy nsp_eq_class f
+   of SOME dtname =>
+        (case get_datatype thy dtname
+         of SOME (vs, _) =>
+              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)]), []))
+          | NONE =>
+              trns
+              |> fail ("no datatype found for " ^ quote dtname))
+    | NONE =>
+        trns
+        |> fail ("not an equality instance: " ^ quote f)
+
 fun defgen_recfun get_equations thy defs f trns =
   case cname_of_idf thy defs f
    of SOME (f, ty) =>
@@ -934,7 +1046,7 @@
            of (_::_) =>
                 trns
                 |> debug 5 (fn _ => "trying defgen recfun for " ^ quote f)
-                |> mk_fun thy defs eqs ty
+                |> mk_fun thy defs eqs (devarify_type ty)
                 |-> (fn def => succeed (def, []))
             | _ =>
                 trns
@@ -1033,6 +1145,11 @@
     |> fold add_def (Codegen.mk_deftab thy |> Symtab.dest)
   end;
 
+fun check_for_serializer serial_name serialize_data =
+  if Symtab.defined serialize_data serial_name
+  then serialize_data
+  else error ("unknown code serializer: " ^ quote serial_name);
+
 fun expand_module defs gen thy =
   let
     fun put_module modl =
@@ -1063,7 +1180,7 @@
     |-> (fn mfx => map_codegen_data
       (fn (modl, gens, lookups, serialize_data, logic_data) =>
          (modl, gens, lookups,
-          serialize_data |> Symtab.map_entry serial_name
+          serialize_data |> check_for_serializer serial_name |> Symtab.map_entry serial_name
             (map_serialize_data
               (fn (primitives, syntax_tyco, syntax_const) =>
                (primitives |> add_primdef primdef,
@@ -1088,7 +1205,7 @@
       let
         val proto_mfx = Codegen.parse_mixfix
           (typ_of o read_ctyp thy) mfx;
-        fun generate thy defs = fold_map (invoke_cg_type thy defs)
+        fun generate thy defs = fold_map (invoke_cg_type thy defs o devarify_type)
           (Codegen.quotes_of proto_mfx);
       in
         thy
@@ -1115,7 +1232,7 @@
     |-> (fn mfx => map_codegen_data
       (fn (modl, gens, lookups, serialize_data, logic_data) =>
          (modl, gens, lookups,
-          serialize_data |> Symtab.map_entry serial_name
+          serialize_data |> check_for_serializer serial_name |> Symtab.map_entry serial_name
             (map_serialize_data
               (fn (primitives, syntax_tyco, syntax_const) =>
                (primitives |> add_primdef primdef,
@@ -1149,7 +1266,7 @@
       let
         val proto_mfx = Codegen.parse_mixfix
           (term_of o read_cterm thy o rpair TypeInfer.logicT) mfx;
-        fun generate thy defs = fold_map (invoke_cg_expr thy defs)
+        fun generate thy defs = fold_map (invoke_cg_expr thy defs o devarify_term)
           (Codegen.quotes_of proto_mfx);
       in
         thy
@@ -1198,6 +1315,7 @@
       thy
       |> CodegenData.get
       |> #serialize_data
+      |> check_for_serializer serial_name
       |> (fn data => (the oo Symtab.lookup) data serial_name)
     val serializer' = (get_serializer thy serial_name)
       ((mk_sfun o #syntax_tyco) serialize_data)
@@ -1227,8 +1345,18 @@
 
 in
 
-val (generateK, serializeK, extractingK, aliasK, definedK, dependingK, syntax_tycoK, syntax_constK) =
-  ("code_generate", "code_serialize", "extracting", "defined_by", "depending_on", "code_alias", "code_syntax_tyco", "code_syntax_const");
+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 classP =
+  OuterSyntax.command classK "codegen data for classes" K.thy_decl (
+    P.xname
+    -- ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name))
+    -- (Scan.optional ((P.$$$ "\\<Rightarrow>" || P.$$$ "=>") |-- (P.list1 P.name)) [])
+    >> (fn ((name, tycos), consts) => (Toplevel.theory (ClassPackage.add_classentry name consts tycos)))
+  )
 
 val generateP =
   OuterSyntax.command generateK "generate executable code for constants" K.thy_decl (
@@ -1258,13 +1386,13 @@
 
 val syntax_tycoP =
   OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl (
-    P.string
+    P.name
     -- Scan.repeat1 (
          P.xname -- (P.$$$ "(" |-- P.string --| P.$$$ ")")
          -- Scan.option (
               P.$$$ definedK
               |-- Scan.option (P.$$$ "(" |-- P.string --| P.$$$ ")")
-              -- (P.string -- Scan.optional (P.$$$ dependingK |-- P.list1 P.string) [])
+              -- (P.text -- Scan.optional (P.$$$ dependingK |-- P.list1 P.string) [])
             )
        )
     >> (fn (serial_name, xs) =>
@@ -1275,13 +1403,13 @@
 
 val syntax_constP =
   OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl (
-    P.string
+    P.name
     -- Scan.repeat1 (
          (P.xname -- Scan.option (P.$$$ "::" |-- P.typ)) -- (P.$$$ "(" |-- P.string --| P.$$$ ")")
          -- Scan.option (
               P.$$$ definedK
               |-- Scan.option (P.$$$ "(" |-- P.string --| P.$$$ ")")
-              -- (P.string -- Scan.optional (P.$$$ dependingK |-- P.list1 P.string) [])
+              -- (P.text -- Scan.optional (P.$$$ dependingK |-- P.list1 P.string) [])
             )
        )
     >> (fn (serial_name, xs) =>
@@ -1290,8 +1418,8 @@
               add_syntax_const serial_name ((f, raw_mfx), raw_def)) xs)
   );
 
-val _ = OuterSyntax.add_parsers [generateP, serializeP, aliasP, syntax_tycoP, syntax_constP];
-val _ = OuterSyntax.add_keywords [extractingK, definedK, dependingK];
+val _ = OuterSyntax.add_parsers [classP, generateP, serializeP, aliasP, syntax_tycoP, syntax_constP];
+val _ = OuterSyntax.add_keywords ["\\<Rightarrow>", "=>", extractingK, definedK, dependingK];
 
 
 (* setup *)
@@ -1309,8 +1437,9 @@
     add_codegen_sort ("default", exprgen_sort_default),
     add_codegen_type ("default", exprgen_type_default),
     add_codegen_expr ("default", exprgen_term_default),
+    add_appgen ("default", appgen_default),
 (*     add_codegen_expr ("eq", codegen_eq),  *)
-    add_codegen_expr ("neg", codegen_neg),
+    add_appgen ("neg", appgen_neg),
     add_defgen ("clsdecl", defgen_clsdecl),
     add_defgen ("tyco_fallback", defgen_tyco_fallback),
     add_defgen ("const_fallback", defgen_const_fallback),
diff -r a41ce9c10b73 -r 99baddf6b0d0 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Fri Dec 02 16:05:12 2005 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Fri Dec 02 16:05:31 2005 +0100
@@ -13,7 +13,6 @@
   val add_prim: string * (string * string list) -> primitives -> primitives;
   val merge_prims: primitives * primitives -> primitives;
   val has_prim: primitives -> string -> bool;
-  val mk_prims: primitives -> string;
 
   type 'a pretty_syntax = string
     -> (int * (Pretty.T list -> ('a -> Pretty.T) -> Pretty.T)) option;
@@ -127,12 +126,16 @@
   | postify (ps as _::_) f = [Pretty.list "(" ")" ps, Pretty.brk 1, f];
 
 fun upper_first s =
-  let val (c :: cs) = String.explode s
-  in String.implode (Char.toUpper c :: cs) end;
+  let
+    val (pr, b) = split_last (NameSpace.unpack s);
+    val (c::cs) = String.explode b;
+  in NameSpace.pack (pr @ [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;
+  let
+    val (pr, b) = split_last (NameSpace.unpack s);
+    val (c::cs) = String.explode b;
+  in NameSpace.pack (pr @ [String.implode (Char.toLower c :: cs)]) end;
 
 
 (** grouping functions **)
@@ -289,10 +292,18 @@
                   |> brackify (eval_br br (INFX (5, R)))
           end
       | ml_from_pat br (ICons ((f, ps), ty)) =
-          ps
-          |> map (ml_from_pat BR)
-          |> cons ((Pretty.str o resolv) f)
-          |> brackify (eval_br br BR)
+          (case const_syntax f
+           of NONE =>
+              ps
+              |> map (ml_from_pat BR)
+              |> cons ((Pretty.str o resolv) f)
+              |> brackify (eval_br br BR)
+            | SOME (i, pr) =>
+              if i = length ps
+              then
+                pr (map (ml_from_pat BR) ps) (ml_from_expr BR)
+              else
+                error "number of argument mismatch in customary serialization")
       | ml_from_pat br (IVarP (v, IType ("Integer", []))) =
           brackify (eval_br br BR) [
             Pretty.str v,
@@ -300,8 +311,8 @@
             Pretty.str "IntInf.int"
           ]
       | ml_from_pat br (IVarP (v, _)) =
-          Pretty.str v;
-    fun ml_from_expr br (e as (IApp (IConst ("Cons", _), _))) =
+          Pretty.str v
+    and 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)
@@ -396,7 +407,9 @@
           brackify (eval_br br (INFX (4, L))) [
             ml_from_expr (INFX (4, L)) e1,
             Pretty.str "=",
-            ml_from_expr (INFX (4, X)) e2
+            ml_from_expr (INFX (4, X)) e2,
+            Pretty.str ":",
+            ml_from_type NOBR (itype_of_iexpr e2)
           ]
       | ml_from_app br ("Pair", [e1, e2]) =
           Pretty.list "(" ")" [
@@ -452,14 +465,15 @@
           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) =
           case const_syntax f
            of NONE =>
-                let
-                  val (es', e) = split_last es;
-                in mk_app_p br (ml_from_app NOBR (f, es')) [e] end
+                (case es
+                 of [] => Pretty.str (resolv f)
+                  | es =>
+                      let
+                        val (es', e) = split_last es;
+                      in mk_app_p br (ml_from_app NOBR (f, es')) [e] end)
             | SOME (i, pr) =>
                 let
                   val (es1, es2) = splitAt (i, es);
@@ -552,7 +566,7 @@
           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 (writeln "******************"; (*map (writeln o Pretty.o)*)
+  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
@@ -630,6 +644,7 @@
     |> eliminate_classes
     |> debug 3 (fn _ => "generating...")
     |> serialize (ml_from_defs tyco_syntax const_syntax) ml_from_module ml_validator nspgrp name_root
+    |> (fn p => Pretty.chunks [(Pretty.str o mk_prims) prims, p])
   end;
 
 fun ml_from_thingol' nspgrp name_root =
@@ -660,9 +675,13 @@
         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
+      if NameSpace.is_qualified f
+      then
+        if is_cons f
+        then (upper_first o resolv) f
+        else (lower_first o resolv) f
+      else
+        f;
     fun haskell_from_sctxt vs =
       let
         fun from_sctxt [] = Pretty.str ""
@@ -755,13 +774,21 @@
                   |> 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)
+          (case const_syntax f
+           of NONE =>
+              ps
+              |> map (haskell_from_pat BR)
+              |> cons ((Pretty.str o resolv_const) f)
+              |> brackify (eval_br br BR)
+            | SOME (i, pr) =>
+              if i = length ps
+              then
+                pr (map (haskell_from_pat BR) ps) (haskell_from_expr BR)
+              else
+                error "number of argument mismatch in customary serialization")
       | haskell_from_pat br (IVarP (v, _)) =
-          (Pretty.str o lower_first) v;
-    fun haskell_from_expr br (e as (IApp (IApp (IConst ("Cons", _), _), _))) =
+          (Pretty.str o lower_first) v
+    and 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
@@ -846,23 +873,17 @@
             Pretty.str "==",
             haskell_from_expr (INFX (4, X)) e2
           ]
+      | haskell_from_app br ("eq", [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",
@@ -872,46 +893,49 @@
             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 ("and", es) =
+          haskell_from_binop br 3 R "&&" es
+      | haskell_from_app br ("or", es) =
+          haskell_from_binop br 2 R "||" es
+      | haskell_from_app br ("add", es) =
+          haskell_from_binop br 6 L "+" es
+      | haskell_from_app br ("mult", es) =
+          haskell_from_binop br 7 L "*" es
+      | haskell_from_app br ("lt", es) =
+          haskell_from_binop br 4 L "<" es
+      | haskell_from_app br ("le", es) =
+          haskell_from_binop br 4 L "<=" es
       | 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_syntax f
            of NONE =>
-                let
-                  val (es', e) = split_last es;
-                in mk_app_p br (haskell_from_app NOBR (f, es')) [e] end
+                (case es
+                 of [] => Pretty.str (resolv_const f)
+                  | es =>
+                      let
+                        val (es', e) = split_last es;
+                      in mk_app_p br (haskell_from_app NOBR (f, es')) [e] end)
             | SOME (i, pr) =>
                 let
                   val (es1, es2) = splitAt (i, es);
-                in mk_app_p br (pr (map (haskell_from_expr BR) es1) (haskell_from_expr BR)) es2 end;
+                in mk_app_p br (pr (map (haskell_from_expr BR) es1) (haskell_from_expr BR)) es2 end
+    and haskell_from_binop br pr L f [e1, e2] =
+          brackify (eval_br br (INFX (pr, L))) [
+            haskell_from_expr (INFX (pr, L)) e1,
+            Pretty.str f,
+            haskell_from_expr (INFX (pr, X)) e2
+          ]
+      | haskell_from_binop br pr R f [e1, e2] =
+          brackify (eval_br br (INFX (pr, R))) [
+            haskell_from_expr (INFX (pr, X)) e1,
+            Pretty.str f,
+            haskell_from_expr (INFX (pr, R)) e2
+          ]
+      | 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) =
@@ -1050,6 +1074,7 @@
     |> 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
+    |> (fn p => Pretty.chunks [(Pretty.str o mk_prims) prims, p])
   end;
 
 end; (* local *)
diff -r a41ce9c10b73 -r 99baddf6b0d0 src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Fri Dec 02 16:05:12 2005 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Fri Dec 02 16:05:31 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,7 +48,7 @@
       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 * class list
+    | 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
@@ -78,6 +78,7 @@
   val type_list: string;
   val type_integer: string;
   val cons_pair: string;
+  val fun_eq: string;
   val fun_fst: string;
   val fun_snd: string;
   val Type_integer: itype;
@@ -103,7 +104,9 @@
   val Fun_wfrec: iexpr;
 
   val prims: string list;
+  val get_eqpred: module -> string -> string option;
   val is_eqtype: module -> itype -> bool;
+  val build_eqpred: module -> string -> def;
   val extract_defs: iexpr -> string list;
   val eta_expand: (string -> int) -> module -> module;
   val eta_expand_poly: module -> module;
@@ -484,13 +487,13 @@
         Pretty.str " |=> ",
         pretty_itype ty
       ]
-  | pretty_def (Datatype (vs, cs, clss)) =
+  | pretty_def (Datatype (vs, cs, insts)) =
       Pretty.block [
         Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
         Pretty.str " |=> ",
         Pretty.gen_list " |" "" "" (map Pretty.str cs),
-        Pretty.str ", instance of ",
-        Pretty.gen_list "," "[" "]" (map Pretty.str clss)
+        Pretty.str ", instances ",
+        Pretty.gen_list "," "[" "]" (map Pretty.str insts)
       ]
   | pretty_def (Datatypecons (dtname, tys)) =
       Pretty.block [
@@ -655,25 +658,25 @@
   in Graph.join (K join_module) modl12 end;
 
 fun partof names modl =
-      let
-        datatype pathnode = PN of (string list * (string * pathnode) list);
-        fun mk_ipath ([], base) (PN (defs, modls)) =
-              PN (base :: defs, modls)
-          | mk_ipath (n::ns, base) (PN (defs, modls)) =
-              modls
-              |> AList.default (op =) (n, PN ([], []))
-              |> AList.map_entry (op =) n (mk_ipath (ns, base))
-              |> (pair defs #> PN);
-        fun select (PN (defs, modls)) (Module module) =
-          module
-          |> Graph.subgraph (Graph.all_succs module (defs @ map fst modls))
-          |> fold (fn (name, modls) => Graph.map_node name (select modls)) modls
-          |> Module;
-      in
-        Module modl
-        |> select (fold (mk_ipath o dest_name) (filter NameSpace.is_qualified names) (PN ([], [])))
-        |> dest_modl
-      end;
+  let
+    datatype pathnode = PN of (string list * (string * pathnode) list);
+    fun mk_ipath ([], base) (PN (defs, modls)) =
+          PN (base :: defs, modls)
+      | mk_ipath (n::ns, base) (PN (defs, modls)) =
+          modls
+          |> AList.default (op =) (n, PN ([], []))
+          |> AList.map_entry (op =) n (mk_ipath (ns, base))
+          |> (pair defs #> PN);
+    fun select (PN (defs, modls)) (Module module) =
+      module
+      |> Graph.subgraph (Graph.all_succs module (defs @ map fst modls))
+      |> fold (fn (name, modls) => Graph.map_node name (select modls)) modls
+      |> Module;
+  in
+    Module modl
+    |> select (fold (mk_ipath o dest_name) (filter NameSpace.is_qualified names) (PN ([], [])))
+    |> dest_modl
+  end;
 
 fun add_check_transform (name, (Datatypecons (dtname, _))) =
       (debug 7 (fn _ => "transformation for datatype constructor " ^ quote name
@@ -682,7 +685,7 @@
           fn [Datatype (_, _, [])] => NONE
             | _ => "attempted to add constructor to already instantiating datatype" |> SOME)],
        [(dtname,
-          fn Datatype (vs, cs, clss) => Datatype (vs, name::cs, clss)
+          fn Datatype (vs, cs, insts) => Datatype (vs, name::cs, insts)
            | def => "attempted to add datatype constructor to non-datatype: "
               ^ (Pretty.output o pretty_def) def |> error)])
       )
@@ -734,7 +737,7 @@
                | def => "attempted to add class instance to non-class"
                   ^ (Pretty.output o pretty_def) def |> error),
            (tyco,
-              fn Datatype (vs, cs, clss) => Datatype (vs, cs, clsname::clss)
+              fn Datatype (vs, cs, insts) => Datatype (vs, cs, name::insts)
                | Nop => Nop
                | def => "attempted to instantiate non-type to class instance"
                   ^ (Pretty.output o pretty_def) def |> error)])
@@ -945,32 +948,68 @@
   cons_true, cons_false, cons_pair, cons_nil, cons_cons, fun_primeq, fun_eq, fun_not, fun_and,
   fun_or, fun_if, fun_fst, fun_snd, fun_add, fun_mult, fun_minus, fun_lt, fun_le, fun_wfrec];
 
-fun is_superclass_of modl class_sub class_sup =
-  if class_sub = class_sup
-  then true
-  else
-    if NameSpace.is_qualified class_sub
-    then
-      case get_def modl class_sub
-       of Class (supclsnames, _, _, _)
-            => exists (fn class => is_superclass_of modl class class_sup) supclsnames
-    else
-      false;
+
+(** equality handling **)
+
+fun get_eqpred modl tyco =
+  if NameSpace.is_qualified tyco
+  then
+    case get_def modl tyco
+     of Datatype (_, _, insts) =>
+          get_first (fn inst =>
+            case get_def modl inst
+             of Classinst (cls, _, memdefs) =>
+                if cls = class_eq
+                then (SOME o snd o hd) memdefs
+                else NONE) insts
+  else SOME fun_primeq;
 
 fun is_eqtype modl (IType (tyco, tys)) =
       forall (is_eqtype modl) tys
-      andalso
-        if NameSpace.is_qualified tyco
-        then
+      andalso (
+        NameSpace.is_qualified tyco
+        orelse
           case get_def modl tyco
            of Typesyn (vs, ty) => is_eqtype modl ty
-            | Datatype (_, _, classes) => exists (is_superclass_of modl class_eq) classes
-        else
-          true
+            | Datatype (_, _, insts) =>
+                exists (fn inst => case get_def modl inst of Classinst (cls, _, _) => cls = class_eq) insts
+      )
   | is_eqtype modl (IFun _) =
       false
   | is_eqtype modl (IVarT (_, sort)) =
-      exists (is_superclass_of modl class_eq) sort
+      member (op =) sort class_eq;
+
+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 ty = IType (dtname, map IVarT sortctxt);
+    fun mk_eq (c, []) =
+          ([ICons ((c, []), ty), ICons ((c, []), ty)], Cons_true)
+      | mk_eq (c, tys) =
+          let
+            val vars1 = Term.invent_names [] "a" (length tys);
+            val vars2 = Term.invent_names vars1 "b" (length tys);
+            fun mk_eq_cons ty' (v1, v2) =
+              IConst (fun_eq, ty' `-> ty' `-> Type_bool) `$ IVarE (v1, ty) `$ IVarE (v2, ty)
+            fun mk_conj (e1, e2) =
+              Fun_and `$ e1 `$ e2;
+          in
+            ([ICons ((c, map2 (curry IVarP) vars1 tys), ty),
+              ICons ((c, map2 (curry IVarP) vars2 tys), ty)],
+              foldr1 mk_conj (map2 mk_eq_cons tys (vars1 ~~ vars2)))
+          end;
+    val eqs = map mk_eq cons @ [([IVarP ("_", ty), IVarP ("_", ty)], Cons_false)];
+  in
+    Fun (eqs, (sortctxt, ty `-> ty `-> Type_bool))
+  end;
+
+
+(** generic transformation **)
 
 fun extract_defs e =
   let
@@ -988,10 +1027,6 @@
           fold_iexpr extr_itype extr_ipat extr_iexpr e
   in extr_iexpr e [] end;
 
-
-
-(** generic transformation **)
-
 fun eta_expand query =
   let
     fun eta_app ((f, ty), es) =