class package and codegen refinements

--- a/src/HOL/Datatype.thy	Mon Feb 27 15:49:56 2006 +0100
+++ b/src/HOL/Datatype.thy	Mon Feb 27 15:51:37 2006 +0100
@@ -286,6 +286,33 @@
     ml (target_atom "(__,/ __)")
     haskell (target_atom "(__,/ __)")
 
+code_generate Unity
+
+code_syntax_tyco
+  unit
+    ml (target_atom "unit")
+    haskell (target_atom "()")
+
+code_syntax_const
+  Unity
+    ml (target_atom "()")
+    haskell (target_atom "()")
+
+code_generate None Some
+
+code_syntax_tyco
+  option
+    ml ("_ option")
+    haskell ("Maybe _")
+
+code_syntax_const
+  None
+    ml (target_atom "NONE")
+    haskell (target_atom "Nothing")
+  Some
+    ml (target_atom "SOME")
+    haskell (target_atom "Just")
+
 code_syntax_const
   "1 :: nat"
     ml ("{*Suc 0*}")

--- a/src/Pure/Tools/class_package.ML	Mon Feb 27 15:49:56 2006 +0100
+++ b/src/Pure/Tools/class_package.ML	Mon Feb 27 15:51:37 2006 +0100
@@ -7,26 +7,22 @@
 
 signature CLASS_PACKAGE =
 sig
-  val add_class: bstring -> class list -> Element.context list -> theory
+  val class: bstring -> class list -> Element.context list -> theory
     -> ProofContext.context * theory
-  val add_class_i: bstring -> class list -> Element.context_i list -> theory
+  val class_i: bstring -> class list -> Element.context_i list -> theory
     -> ProofContext.context * theory
-  val add_instance_arity: (xstring * string list) * string
+  val instance_arity: (xstring * string list) * string
     -> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list
     -> theory -> Proof.state
-  val add_instance_arity_i: (string * sort list) * sort
+  val instance_arity_i: (string * sort list) * sort
     -> bstring * attribute list -> ((bstring * attribute list) * term) list
     -> theory -> Proof.state
-  val prove_instance_arity: tactic -> (xstring * string list) * string
-    -> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list
-    -> theory -> theory
-  val prove_instance_arity_i: tactic -> (string * sort list) * sort
+  val prove_instance_arity: tactic -> (string * sort list) * sort
     -> bstring * attribute list -> ((bstring * attribute list) * term) list
     -> theory -> theory
-  val add_instance_sort: string * string -> theory -> Proof.state
-  val add_instance_sort_i: class * sort -> theory -> Proof.state
-  val prove_instance_sort: tactic -> string * string -> theory -> theory
-  val prove_instance_sort_i: tactic -> class * sort -> theory -> theory
+  val instance_sort: string * string -> theory -> Proof.state
+  val instance_sort_i: class * sort -> theory -> Proof.state
+  val prove_instance_sort: tactic -> class * sort -> theory -> theory
 
   val intern_class: theory -> xstring -> class
   val intern_sort: theory -> sort -> sort
@@ -343,7 +339,7 @@
     |-> (fn _ => I)
   end;
 
-fun gen_add_class add_locale prep_class bname raw_supclasses raw_elems thy =
+fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy =
   let
     val supclasses = map (prep_class thy) raw_supclasses;
     val supsort =
@@ -423,8 +419,8 @@
 
 in
 
-val add_class = gen_add_class (add_locale true) intern_class;
-val add_class_i = gen_add_class (add_locale_i true) certify_class;
+val class = gen_class (add_locale true) intern_class;
+val class_i = gen_class (add_locale_i true) certify_class;
 
 end; (* local *)
 
@@ -538,19 +534,18 @@
     |-> (fn cs => do_proof (after_qed cs) arity)
   end;
 
-fun instance_arity do_proof = gen_instance_arity AxClass.read_arity Attrib.attribute add_defs_overloaded
+fun instance_arity' do_proof = gen_instance_arity AxClass.read_arity Attrib.attribute add_defs_overloaded
   (fn thy => fn t => (snd o read_axm thy) ("", t)) do_proof;
-fun instance_arity_i do_proof = gen_instance_arity AxClass.cert_arity (K I) add_defs_overloaded_i
+fun instance_arity_i' do_proof = gen_instance_arity AxClass.cert_arity (K I) add_defs_overloaded_i
   (K I) do_proof;
 val setup_proof = AxClass.instance_arity_i;
 fun tactic_proof tac after_qed arity = AxClass.add_inst_arity_i arity tac #> after_qed;
 
 in
 
-val add_instance_arity = instance_arity setup_proof;
-val add_instance_arity_i = instance_arity_i setup_proof;
-val prove_instance_arity = instance_arity o tactic_proof;
-val prove_instance_arity_i = instance_arity_i o tactic_proof;
+val instance_arity = instance_arity' setup_proof;
+val instance_arity_i = instance_arity_i' setup_proof;
+val prove_instance_arity = instance_arity_i' o tactic_proof;
 
 end; (* local *)
 
@@ -585,7 +580,7 @@
   |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
   |-> (fn _ => I);
 
-fun gen_add_instance_sort prep_class prep_sort do_proof (raw_class, raw_sort) theory =
+fun gen_instance_sort prep_class prep_sort do_proof (raw_class, raw_sort) theory =
   let
     val class = prep_class theory raw_class;
     val sort = prep_sort theory raw_sort;
@@ -605,18 +600,16 @@
     |> do_proof after_qed (loc_name, loc_expr)
   end;
 
-fun instance_sort do_proof = gen_add_instance_sort intern_class read_sort do_proof;
-fun instance_sort_i do_proof = gen_add_instance_sort certify_class certify_sort do_proof;
-
+fun instance_sort' do_proof = gen_instance_sort intern_class read_sort do_proof;
+fun instance_sort_i' do_proof = gen_instance_sort certify_class certify_sort do_proof;
 val setup_proof = add_interpretation_in;
 val tactic_proof = prove_interpretation_in;
 
 in
 
-val add_instance_sort = instance_sort setup_proof;
-val add_instance_sort_i = instance_sort_i setup_proof;
-val prove_instance_sort = instance_sort o tactic_proof;
-val prove_instance_sort_i = instance_sort_i o tactic_proof;
+val instance_sort = instance_sort' setup_proof;
+val instance_sort_i = instance_sort_i' setup_proof;
+val prove_instance_sort = instance_sort_i' o tactic_proof;
 
 end; (* local *)
 
@@ -727,10 +720,10 @@
       if (is_some o lookup_class_data thy o Sign.intern_class thy) class
         andalso (is_some o lookup_class_data thy o Sign.intern_class thy) class'
       then
-        add_instance_sort (class, sort) thy
+        instance_sort (class, sort) thy
       else
         AxClass.instance_subclass (class, sort) thy
-    | _ => add_instance_sort (class, sort) thy;
+    | _ => instance_sort (class, sort) thy;
 
 val parse_inst =
   (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 P.sort --| P.$$$ ")")) [] -- P.xname --| P.$$$ "::" -- P.sort)
@@ -749,14 +742,14 @@
     -- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) []
     -- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) []
       >> (Toplevel.theory_context
-          o (fn ((bname, supclasses), elems) => add_class bname supclasses elems)));
+          o (fn ((bname, supclasses), elems) => class bname supclasses elems)));
 
 val instanceP =
   OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
       P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> wrap_add_instance_subclass
       || P.opt_thm_name ":" -- (parse_inst -- Scan.repeat (P.opt_thm_name ":" -- P.prop))
            >> (fn (("", []), (((tyco, asorts), sort), [])) => AxClass.instance_arity I (tyco, asorts, sort)
-                | (natts, (inst, defs)) => add_instance_arity inst natts defs)
+                | (natts, (inst, defs)) => instance_arity inst natts defs)
     ) >> (Toplevel.print oo Toplevel.theory_to_proof));
 
 val _ = OuterSyntax.add_parsers [classP, instanceP];

--- a/src/Pure/Tools/codegen_package.ML	Mon Feb 27 15:49:56 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Mon Feb 27 15:51:37 2006 +0100
@@ -38,10 +38,11 @@
     -> theory -> theory;
   val set_int_tyco: string -> theory -> theory;
 
-  val codegen_incr: term -> theory -> (CodegenThingol.iexpr * (string * CodegenThingol.def) list) * theory;
+  val codegen_term: term -> theory -> CodegenThingol.iexpr * theory;
   val is_dtcon: string -> bool;
-  val consts_of_idfs: theory -> string list -> (string * (string * typ)) list
-
+  val consts_of_idfs: theory -> string list -> (string * typ) list;
+  val idfs_of_consts: theory -> (string * typ) list -> string list;
+  val get_root_module: theory -> CodegenThingol.module;
   val get_ml_fun_datatype: theory -> (string -> string)
     -> ((string * CodegenThingol.funn) list -> Pretty.T)
         * ((string * CodegenThingol.datatyp) list -> Pretty.T);
@@ -188,7 +189,7 @@
       |> curry (op ^ o swap) ((implode oo replicate) i "'")
     end;
   fun is_valid _ _ = true;
-  fun maybe_unique thy (c, ty) = 
+  fun maybe_unique thy (c, ty) =
     if is_overloaded thy c
       then NONE
       else (SOME o idf_of_name thy nsp_const) c;
@@ -475,7 +476,7 @@
         gens |> map_gens
           (fn (appconst, eqextrs) =>
             (appconst, eqextrs
-             |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name)
+    |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name)
                  (name, (eqx, stamp ())))),
              target_data, logic_data));
 
@@ -660,7 +661,7 @@
   | exprgen_type thy tabs (TFree v_s) trns =
       trns
       |> exprgen_tyvar_sort thy tabs v_s
-      |-> (fn v_s => pair (IVarT v_s))
+      |-> (fn (v, sort) => pair (IVarT v))
   | exprgen_type thy tabs (Type ("fun", [t1, t2])) trns =
       trns
       |> exprgen_type thy tabs t1
@@ -907,14 +908,15 @@
   end;
 
 fun appgen_split strip_abs thy tabs (c, [t2]) trns =
-  let
-    val ([p], body) = strip_abs 1 (Const c $ t2)
-  in
-    trns
-    |> exprgen_term thy tabs p
-    ||>> exprgen_term thy tabs body
-    |-> (fn (e, body) => pair (e `|-> body))
-  end;
+  case strip_abs 1 (Const c $ t2)
+   of ([p], body) =>
+        trns
+        |> exprgen_term thy tabs p
+        ||>> exprgen_term thy tabs body
+        |-> (fn (e, body) => pair (e `|-> body))
+    | _ =>
+        trns
+        |> appgen_default thy tabs (c, [t2]);
 
 fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_,
   Type (_, [_, ty as Type (tyco, [])])), [bin]) trns =
@@ -1074,7 +1076,7 @@
             let
               val c = "op =";
               val ty = Sign.the_const_type thy c;
-              fun inst dtco = 
+              fun inst dtco =
                 map_atyps (fn _ => Type (dtco,
                   (map (fn (v, sort) => TVar ((v, 0), sort)) o fst o the o get_datatype thy) dtco)) ty
               val dtcos = fold (insert (op =) o snd) (get_all_datatype_cons thy) [];
@@ -1096,7 +1098,7 @@
             ) (get_all_datatype_cons thy) [])
       |-> (fn _ => I);
     fun mk_clsmemtab thy =
-      Symtab.empty
+   Symtab.empty
       |> Symtab.fold
           (fn (class, (clsmems, _)) => fold
             (fn clsmem => Symtab.update (clsmem, class)) clsmems)
@@ -1159,25 +1161,24 @@
     fold ensure (get_datatype_case_consts thy) thy
   end;
 
-fun codegen_incr t thy =
+fun codegen_term t thy =
   thy
-  |> `(#modl o CodegenData.get)
-  ||>> expand_module NONE exprsgen_term [t]
-  ||>> `(#modl o CodegenData.get)
-  |-> (fn ((modl_old, [t]), modl_new) => pair (t, CodegenThingol.diff_module (modl_new, modl_old)));
+  |> expand_module NONE exprsgen_term [t]
+  |-> (fn [t] => pair t);
 
 val is_dtcon = has_nsp nsp_dtcon;
 
 fun consts_of_idfs thy =
-  let
-    val tabs = mk_tabs thy;
-  in
-    map (fn idf => (idf, (the o recconst_of_idf thy tabs) idf))
-  end;
+  map (the o recconst_of_idf thy (mk_tabs thy));
+
+fun idfs_of_consts thy =
+  map (idf_of_const thy (mk_tabs thy));
+
+val get_root_module = (#modl o CodegenData.get);
 
 fun get_ml_fun_datatype thy resolv =
   let
-    val target_data = 
+    val target_data =
       ((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy;
   in
     CodegenSerializer.ml_fun_datatype (nsp_dtcon, nsp_class, K false)
@@ -1342,9 +1343,9 @@
 (** toplevel interface **)
 
 local
- 
+
 fun generate_code (SOME raw_consts) thy =
-      let
+   let
         val consts = map (read_const thy) raw_consts;
       in
         thy

--- a/src/Pure/Tools/codegen_serializer.ML	Mon Feb 27 15:49:56 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Mon Feb 27 15:51:37 2006 +0100
@@ -26,6 +26,7 @@
     ml: string * (string * string * (string -> bool) -> serializer),
     haskell: string * (string list -> serializer)
   };
+  val mk_flat_ml_resolver: string list -> string -> string;
   val ml_fun_datatype: string * string * (string -> bool)
     -> ((string -> CodegenThingol.itype pretty_syntax option)
         * (string -> CodegenThingol.iexpr pretty_syntax option))
@@ -264,6 +265,23 @@
     |> K ()
   end;
 
+fun replace_invalid s =
+  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 contract "_" (acc as "_" :: _) = acc
+      | contract c acc = c :: acc;
+    fun contract_underscores s =
+      implode (fold_rev contract (explode s) []);
+  in
+    s
+    |> translate_string replace_invalid
+    |> contract_underscores
+  end;
+
 fun abstract_validator keywords name =
   let
     fun replace_invalid c =
@@ -351,6 +369,23 @@
 
 local
 
+val reserved_ml = ThmDatabase.ml_reserved @ [
+  "bool", "int", "list", "unit", "option", "true", "false", "not", "None", "Some", "o"
+];
+
+structure NameMangler = NameManglerFun (
+  type ctxt = string list;
+  type src = string;
+  val ord = string_ord;
+  fun mk reserved_ml (name, 0) =
+        (replace_invalid o NameSpace.base) name
+    | mk reserved_ml (name, i) =
+        (replace_invalid o NameSpace.base) name ^ replicate_string i "'";
+  fun is_valid reserved_ml = not o member (op =) reserved_ml;
+  fun maybe_unique _ _ = NONE;
+  fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
+);
+
 fun ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv =
   let
     val ml_from_label =
@@ -415,7 +450,7 @@
               ml_from_type (INFX (1, R)) t2
             ]
           end
-      | ml_from_type fxy (IVarT (v, _)) =
+      | ml_from_type fxy (IVarT v) =
           str ("'" ^ v);
     fun ml_from_expr fxy (e as IApp (e1, e2)) =
           (case unfold_const_app e
@@ -578,7 +613,7 @@
         fun mk_datatype definer (t, (vs, cs)) =
           (Pretty.block o Pretty.breaks) (
             str definer
-            :: ml_from_tycoexpr NOBR (t, map IVarT vs)
+            :: ml_from_tycoexpr NOBR (t, map (IVarT o fst) vs)
             :: str "="
             :: separate (str "|") (map mk_cons cs)
           )
@@ -661,7 +696,7 @@
             error "can't serialize sort constrained type declaration to ML") vs;
           Pretty.block [
             str "type ",
-            ml_from_tycoexpr NOBR (name, map IVarT vs),
+            ml_from_tycoexpr NOBR (name, map (IVarT o fst) vs),
             str " =",
             Pretty.brk 1,
             ml_from_type NOBR ty,
@@ -737,9 +772,6 @@
 
 fun ml_from_thingol target (nsp_dtcon, nsp_class, is_int_tyco) nspgrp =
   let
-    val reserved_ml = ThmDatabase.ml_reserved @ [
-      "bool", "int", "list", "true", "false", "not", "o"
-    ];
     fun ml_from_module _ ((_, name), ps) =
       Pretty.chunks ([
         str ("structure " ^ name ^ " = "),
@@ -786,6 +818,14 @@
          (preprocess const_syntax) (class_syntax, tyco_syntax, const_syntax))
   end;
 
+fun mk_flat_ml_resolver names =
+  let
+    val mangler =
+      NameMangler.empty
+      |> fold_map (NameMangler.declare reserved_ml) names
+      |-> (fn _ => I)
+  in NameMangler.get reserved_ml mangler end;
+
 fun ml_fun_datatype (nsp_dtcon, nsp_class, is_int_tyco) =
   ml_fun_datatyp (ml_annotators (nsp_dtcon, nsp_class, is_int_tyco));
 
@@ -838,7 +878,7 @@
             str "->",
             hs_from_type (INFX (1, R)) t2
           ]
-      | hs_from_type fxy (IVarT (v, _)) =
+      | hs_from_type fxy (IVarT v) =
           str v;
     fun hs_from_sctxt_tycoexpr (sctxt, tycoexpr) =
       Pretty.block [hs_from_sctxt sctxt, hs_from_tycoexpr NOBR tycoexpr]
@@ -934,7 +974,7 @@
       | hs_from_def (name, Typesyn (vs, ty)) =
           Pretty.block [
             str "type ",
-            hs_from_sctxt_tycoexpr (vs, (resolv_here name, map IVarT vs)),
+            hs_from_sctxt_tycoexpr (vs, (resolv_here name, map (IVarT o fst) vs)),
             str " =",
             Pretty.brk 1,
             hs_from_sctxt_type ([], ty)
@@ -949,7 +989,7 @@
           in
             Pretty.block ((
               str "data "
-              :: hs_from_sctxt_type (vs, IType (resolv_here name, map IVarT vs))
+              :: hs_from_sctxt_type (vs, IType (resolv_here name, map (IVarT o fst) vs))
               :: str " ="
               :: Pretty.brk 1
               :: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs)
@@ -983,9 +1023,9 @@
       | hs_from_def (_, Classinst (((clsname, (tyco, arity)), _), memdefs)) = 
           Pretty.block [
             str "instance ",
-            hs_from_sctxt_tycoexpr (arity, (clsname, map (IVarT o rpair [] o fst) arity)),
+            hs_from_sctxt_tycoexpr (arity, (clsname, map (IVarT o fst) arity)),
             str " ",
-            hs_from_sctxt_tycoexpr (arity, (tyco, map (IVarT o rpair [] o fst) arity)),
+            hs_from_sctxt_tycoexpr (arity, (tyco, map (IVarT o fst) arity)),
             str " where",
             Pretty.fbrk,
             Pretty.chunks (map (fn (m, (_, (eqs, _))) => hs_from_funeqs (m, eqs)) memdefs)
@@ -1005,7 +1045,7 @@
       "import", "default", "forall", "let", "in", "class", "qualified", "data",
       "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
     ] @ [
-      "Bool", "Integer", "True", "False", "negate"
+      "Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "negate"
     ];
     fun hs_from_module imps ((_, name), ps) =
       (Pretty.chunks) (

--- a/src/Pure/Tools/codegen_thingol.ML	Mon Feb 27 15:49:56 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Mon Feb 27 15:51:37 2006 +0100
@@ -13,7 +13,8 @@
   datatype itype =
       IType of string * itype list
     | IFun of itype * itype
-    | IVarT of vname * sort;
+    | IVarT of vname;
+  type ityp = ClassPackage.sortcontext * itype;
   datatype iexpr =
       IConst of (string * itype) * classlookup list list
     | IVarE of vname * itype
@@ -49,8 +50,8 @@
   val `|-> : iexpr * iexpr -> iexpr;
   val `|--> : iexpr list * iexpr -> iexpr;
 
-  type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype);
-  type datatyp = (vname * sort) list * (string * itype list) list;
+  type funn = (iexpr list * iexpr) list * ityp;
+  type datatyp = ClassPackage.sortcontext * (string * itype list) list;
   datatype prim =
       Pretty of Pretty.T
     | Name;
@@ -61,7 +62,7 @@
     | Typesyn of (vname * sort) list * itype
     | Datatype of datatyp
     | Datatypecons of string
-    | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)
+    | Class of class list * (vname * (string * ityp) list)
     | Classmember of class
     | Classinst of ((class * (string * (vname * sort) list))
           * (class * (string * classlookup list list)) list)
@@ -159,7 +160,8 @@
 datatype itype =
     IType of string * itype list
   | IFun of itype * itype
-  | IVarT of vname * sort;
+  | IVarT of vname;
+type ityp = ClassPackage.sortcontext * itype;
 
 datatype iexpr =
     IConst of (string * itype) * classlookup list list
@@ -204,12 +206,16 @@
 val op `$$ = mk_apps;
 val op `|--> = mk_abss;
 
+val pretty_sortcontext =
+  Pretty.commas o map (fn (v, sort) => (Pretty.block o Pretty.breaks)
+    [Pretty.str v, Pretty.str "::", Pretty.enum "&" "" "" (map Pretty.str sort)]);
+
 fun pretty_itype (IType (tyco, tys)) =
       Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
   | pretty_itype (IFun (ty1, ty2)) =
       Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
-  | pretty_itype (IVarT (v, sort)) =
-      Pretty.str (v ^ enclose "|" "|" (space_implode "|" sort));
+  | pretty_itype (IVarT v) =
+      Pretty.str v;
 
 fun pretty_iexpr (IConst ((c, ty), _)) =
       Pretty.block [Pretty.str (c ^ "::"), pretty_itype ty]
@@ -307,19 +313,22 @@
   | fold_aexpr f (e as IVarE _) =
       f e;
 
-fun eq_itype (ty1, ty2) =
+fun eq_ityp ((sctxt1, ty1), (sctxt2, 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)
+    fun eq_sctxt subs sctxt1 sctxt2 =
+      map (fn (v, sort) => case AList.lookup (op =) subs v
+       of NONE => raise NO_MATCH
+        | SOME v' => case AList.lookup (op =) sctxt2 v'
+           of NONE => raise NO_MATCH
+            | SOME sort' => if sort <> sort' then raise NO_MATCH else ()) sctxt1
+    fun eq (IVarT v1) (IVarT v2) subs =
+          (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
@@ -360,7 +369,7 @@
 
 fun type_vnames ty = 
   let
-    fun extr (IVarT (v, _)) =
+    fun extr (IVarT v) =
           insert (op =) v
       | extr _ = I;
   in fold_atype extr ty end;
@@ -384,8 +393,8 @@
 
 (* type definitions *)
 
-type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype);
-type datatyp = (vname * sort) list * (string * itype list) list;
+type funn = (iexpr list * iexpr) list * ityp;
+type datatyp = ClassPackage.sortcontext * (string * itype list) list;
 
 datatype prim =
     Pretty of Pretty.T
@@ -398,7 +407,7 @@
   | Typesyn of (vname * sort) list * itype
   | Datatype of datatyp
   | Datatypecons of string
-  | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)
+  | Class of class list * (vname * (string * ityp) list)
   | Classmember of class
   | Classinst of ((class * (string * (vname * sort) list))
         * (class * (string * classlookup list list)) list)
@@ -433,13 +442,13 @@
         )
   | pretty_def (Typesyn (vs, ty)) =
       Pretty.block [
-        Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
+        Pretty.list "(" ")" (pretty_sortcontext vs),
         Pretty.str " |=> ",
         pretty_itype ty
       ]
   | pretty_def (Datatype (vs, cs)) =
       Pretty.block [
-        Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
+        Pretty.list "(" ")" (pretty_sortcontext vs),
         Pretty.str " |=> ",
         Pretty.enum " |" "" ""
           (map (fn (c, tys) => (Pretty.block o Pretty.breaks)
@@ -774,14 +783,17 @@
         val _ = if length memdefs > length memdefs
           then error "too many member definitions given"
           else ();
-        fun instant (w, ty) (var as (v, _)) =
-          if v = w then ty else IVarT var;
-        fun mk_memdef (m, (ctxt, ty)) =
+        fun instant (w, ty) v =
+          if v = w then ty else IVarT v;
+        fun mk_memdef (m, (sortctxt, ty)) =
           case AList.lookup (op =) memdefs m
            of NONE => error ("missing definition for member " ^ quote m)
-            | SOME (m', (eqs, (ctxt', ty'))) =>
-                if eq_itype (instant_itype (instant (v, tyco `%% map IVarT arity)) ty, ty')
-                then (m, (m', (check_funeqs eqs, (ctxt', ty'))))
+            | SOME (m', (eqs, (sortctxt', ty'))) =>
+                if eq_ityp
+                  ((sortctxt |> fold (fn v_sort => AList.update (op =) v_sort) arity,
+                     instant_itype (instant (v, tyco `%% map (IVarT o fst) arity)) ty),
+                  (sortctxt', ty'))
+                then (m, (m', (check_funeqs eqs, (sortctxt', ty'))))
                 else error ("inconsistent type for member definition " ^ quote m)
       in Classinst (d, map mk_memdef membrs) end;
 
@@ -933,7 +945,7 @@
              of ([], e) =>
                   let
                     val add_var = IVarE (hd (Term.invent_names (expr_names e []) "x" 1), ty1)
-                  in (([([add_var], add_var `|-> e)], cty)) end
+                  in (([([add_var], e `$ add_var)], cty)) end
               | eq => 
                   (([eq], cty)))
       | eta funn = funn;
@@ -948,13 +960,13 @@
         val used_type = map fst sortctxt;
         val clash = gen_union (op =) (used_expr, used_type);
         val rename_map = fold_map (fn c => invent c #-> (fn c' => pair (c, c'))) clash [] |> fst;
-        fun rename (v, sort) =
-          (perhaps (AList.lookup (op =) rename_map) v, sort);
+        val rename =
+          perhaps (AList.lookup (op =) rename_map);
         val rename_typ = instant_itype (IVarT o rename);
         val rename_expr = map_iexpr_itype rename_typ;
         fun rename_eq (args, rhs) = (map rename_expr args, rename_expr rhs)
       in
-        (map rename_eq eqs, (map rename sortctxt, rename_typ ty))
+        (map rename_eq eqs, (map (apfst rename) sortctxt, rename_typ ty))
       end;
   in (map_defs o map_def_fun) unclash end;
 
@@ -975,10 +987,13 @@
           | _ => mk (postprocess, validate) ((shallow, name), 1)
         end
     | mk (postprocess, validate) (("", name), i) =
-        postprocess ("", name ^ "_" ^ string_of_int (i+1))
+        postprocess ("", name ^ replicate_string i "'")
+        |> perhaps validate
+    | mk (postprocess, validate) ((shallow, name), 1) =
+        postprocess (shallow, shallow ^ "_" ^ name)
         |> perhaps validate
     | mk (postprocess, validate) ((shallow, name), i) =
-        postprocess (shallow, shallow ^ "_" ^ name ^ "_" ^ string_of_int (i+1))
+        postprocess (shallow, name ^ replicate_string i "'")
         |> perhaps validate;
   fun is_valid _ _ = true;
   fun maybe_unique _ _ = NONE;

--- a/src/Pure/Tools/nbe.ML	Mon Feb 27 15:49:56 2006 +0100
+++ b/src/Pure/Tools/nbe.ML	Mon Feb 27 15:51:37 2006 +0100
@@ -32,22 +32,28 @@
                                 "\n---\n")
       true s);
 
-val tab = ref Symtab.empty
-fun lookup s = the(Symtab.lookup (!tab) s)
-fun update sx = (tab := Symtab.update sx (!tab))
+val tab : NBE_Eval.Univ Symtab.table ref = ref Symtab.empty;
+fun lookup s = the(Symtab.lookup (!tab) s);
+fun update sx = (tab := Symtab.update sx (!tab));
 fun defined s = Symtab.defined (!tab) s;
 
 fun top_nbe st thy =
-let val t = Sign.read_term thy st
-    val ((t',diff),thy') = CodegenPackage.codegen_incr t thy
-    val _ = (tab := NBE_Data.get thy;
+  let
+    val t = Sign.read_term thy st;
+    val nbe_tab = NBE_Data.get thy;
+    val modl_old = CodegenThingol.partof (Symtab.keys nbe_tab)
+      (CodegenPackage.get_root_module thy);
+    val (t', thy') = CodegenPackage.codegen_term t thy
+    val modl_new = CodegenPackage.get_root_module thy;
+    val diff = CodegenThingol.diff_module (modl_old, modl_new);
+    val _ = (tab := nbe_tab;
              Library.seq (use_show o NBE_Codegen.generate defined) diff)
     val thy'' = NBE_Data.put (!tab) thy'
     val nt' = NBE_Eval.nbe (!tab) t'
     val _ = print nt'
-in
-  thy''
-end
+  in
+    thy''
+  end;
 
 structure P = OuterParse and K = OuterKeyword;