# HG changeset patch
# User haftmann
# Date 1141217262 -3600
# Node ID f237c0cb3882e0691fc1082c13161b2a43a27136
# Parent  fd8f152cfc76e3a2e7169570e7e388e13708f9c0
refined representation of codegen intermediate language

diff -r fd8f152cfc76 -r f237c0cb3882 src/HOL/ex/nbe.thy
--- a/src/HOL/ex/nbe.thy	Wed Mar 01 10:37:00 2006 +0100
+++ b/src/HOL/ex/nbe.thy	Wed Mar 01 13:47:42 2006 +0100
@@ -7,28 +7,17 @@
 imports Main
 begin
 
-datatype n = Z | S n
-consts
- add :: "n \<Rightarrow> n \<Rightarrow> n"
- mul :: "n \<Rightarrow> n \<Rightarrow> n"
- exp :: "n \<Rightarrow> n \<Rightarrow> n"
-primrec
-"add Z = id"
-"add (S m) = S o add m"
-primrec
-"mul Z = (%n. Z)"
-"mul (S m) = (%n. add (mul m n) n)"
-primrec
-"exp m Z = S Z"
-"exp m (S n) = mul (exp m n) m"
-
 (*ML"set Toplevel.timing"*)
-;norm_by_eval "exp (S(S(S(S(S(S(S Z))))))) (S(S(S(S(S Z)))))";
-norm_by_eval "0 + (n::nat)";
-norm_by_eval "0 + Suc(n)";
-norm_by_eval "Suc(n) + Suc m";
-norm_by_eval "[] @ xs";
-norm_by_eval "(x#xs) @ ys";
-norm_by_eval "[x,y,z] @ [a,b,c]";
+norm_by_eval "exp (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) (Suc (Suc  (Suc (Suc (Suc 0)))))"
+norm_by_eval "0 + (n::nat)"
+norm_by_eval "0 + Suc(n)"
+norm_by_eval "Suc(n) + Suc m"
+norm_by_eval "[] @ xs"
+norm_by_eval "(x#xs) @ ys"
+norm_by_eval "[x,y,z] @ [a,b,c]"
+norm_by_eval "%(xs, ys). xs @ ys"
+norm_by_eval "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f])"
+norm_by_eval "%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True"
+norm_by_eval "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]"
 
 end
diff -r fd8f152cfc76 -r f237c0cb3882 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Wed Mar 01 10:37:00 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Wed Mar 01 13:47:42 2006 +0100
@@ -83,13 +83,6 @@
 struct
 
 open CodegenThingol;
-infix 8 `%%;
-infixr 6 `->;
-infixr 6 `-->;
-infix 4 `$;
-infix 4 `$$;
-infixr 3 `|->;
-infixr 3 `|-->;
 
 (* shallow name spaces *)
 
@@ -661,7 +654,7 @@
   | exprgen_type thy tabs (TFree v_s) trns =
       trns
       |> exprgen_tyvar_sort thy tabs v_s
-      |-> (fn (v, sort) => pair (IVarT v))
+      |-> (fn (v, sort) => pair (ITyVar v))
   | exprgen_type thy tabs (Type ("fun", [t1, t2])) trns =
       trns
       |> exprgen_type thy tabs t1
@@ -815,7 +808,7 @@
   | exprgen_term thy tabs (Free (v, ty)) trns =
       trns
       |> exprgen_type thy tabs ty
-      |-> (fn ty => pair (IVarE (v, ty)))
+      |-> (fn ty => pair (IVar v))
   | exprgen_term thy tabs (Abs (abs as (_, ty, _))) trns =
       let
         val (v, t) = Term.variant_abs abs
@@ -823,7 +816,7 @@
         trns
         |> exprgen_type thy tabs ty
         ||>> exprgen_term thy tabs t
-        |-> (fn (ty, e) => pair (IVarE (v, ty) `|-> e))
+        |-> (fn (ty, e) => pair ((v, ty) `|-> e))
       end
   | exprgen_term thy tabs (t as t1 $ t2) trns =
       let
@@ -867,7 +860,7 @@
             |> debug 10 (fn _ => "eta-expanding")
             |> fold_map (exprgen_type thy tabs) tys
             ||>> ag thy tabs ((f, ty), ts @ map2 (curry Free) vs tys)
-            |-> (fn (tys, e) => pair (map2 (curry IVarE) vs tys `|--> e))
+            |-> (fn (tys, e) => pair (vs ~~ tys `|--> e))
           end
         else if length ts > imax then
           trns
@@ -875,7 +868,7 @@
                ^ string_of_int (length ts) ^ ")")
           |> ag thy tabs ((f, ty), Library.take (imax, ts))
           ||>> fold_map (exprgen_term thy tabs) (Library.drop (imax, ts))
-          |-> (fn es => pair (mk_apps es))
+          |-> (fn (e, es) => pair (e `$$ es))
         else
           trns
           |> debug 10 (fn _ => "keeping arguments")
@@ -896,27 +889,32 @@
 
 (* parametrized generators, for instantiation in HOL *)
 
-fun appgen_let strip_abs thy tabs ((c, ty), [t_val, t_cont]) trns =
+fun appgen_let strip_abs thy tabs (app as ((c, ty), [dt, ct])) trns =
   let
-    val ([t_abs], t_body) = strip_abs 1 t_cont;
+    val ([st], bt) = strip_abs 1 ct;
+    val dtyp = (hd o fst o strip_type) ty
   in
     trns
-    |> exprgen_term thy tabs t_val
-    ||>> exprgen_term thy tabs t_abs
-    ||>> exprgen_term thy tabs t_body
-    |-> (fn ((e, abs), body) => pair (ICase (e, [(abs, body)])))
+    |> exprgen_term thy tabs dt
+    ||>> exprgen_type thy tabs dtyp
+    ||>> exprgen_term thy tabs st
+    ||>> exprgen_term thy tabs bt
+    ||>> appgen_default thy tabs app
+    |-> (fn ((((de, dty), se), be), e0) => pair (ICase (((de, dty), [(se, be)]), e0)))
   end;
 
-fun appgen_split strip_abs thy tabs (c, [t2]) trns =
-  case strip_abs 1 (Const c $ t2)
-   of ([p], body) =>
+fun appgen_split strip_abs thy tabs (app as (c as (_, ty), [t])) trns =
+  case strip_abs 1 (Const c $ t)
+   of ([vt], tb) =>
         trns
-        |> exprgen_term thy tabs p
-        ||>> exprgen_term thy tabs body
-        |-> (fn (e, body) => pair (e `|-> body))
+        |> exprgen_term thy tabs vt
+        ||>> exprgen_type thy tabs (((fn [_, ty] => ty) o fst o strip_type) ty)
+        ||>> exprgen_term thy tabs tb
+        ||>> appgen_default thy tabs app
+        |-> (fn (((ve, vty), be), e0) => pair (IAbs (((ve, vty), be), e0)))
     | _ =>
         trns
-        |> appgen_default thy tabs (c, [t2]);
+        |> appgen_default thy tabs app;
 
 fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_,
   Type (_, [_, ty as Type (tyco, [])])), [bin]) trns =
@@ -975,7 +973,7 @@
   | eqextr_eq f fals thy tabs _ =
       NONE;
 
-fun appgen_datatype_case cos thy tabs ((_, ty), ts) trns =
+fun appgen_datatype_case cos thy tabs (app as ((_, ty), ts)) trns =
   let
     val (ts', t) = split_last ts;
     val (tys, dty) = (split_last o fst o strip_type) ty;
@@ -997,8 +995,10 @@
   in
     trns
     |> exprgen_term thy tabs t
+    ||>> exprgen_type thy tabs dty
     ||>> fold_map cg_case_d ((cos ~~ tys) ~~ ts')
-    |-> (fn (t, ds) => pair (ICase (t, ds)))
+    ||>> appgen_default thy tabs app
+    |-> (fn (((de, dty), bses), e0) => pair (ICase (((de, dty), bses), e0)))
   end;
 
 fun gen_add_case_const prep_c get_case_const_data raw_c thy =
diff -r fd8f152cfc76 -r f237c0cb3882 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Wed Mar 01 10:37:00 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Wed Mar 01 13:47:42 2006 +0100
@@ -38,15 +38,8 @@
 structure CodegenSerializer: CODEGEN_SERIALIZER =
 struct
 
-open CodegenThingol;
-infix 8 `%%;
-infixr 6 `->;
-infixr 6 `-->;
-infix 4 `$;
-infix 4 `$$;
-infixr 3 `|->;
-infixr 3 `|-->;
-
+open BasicCodegenThingol;
+val debug = CodegenThingol.debug;
 
 (** generic serialization **)
 
@@ -217,7 +210,7 @@
   case Scan.finite Symbol.stopper (Scan.repeat (
          ($$ "`" |-- $$ "`" >> (CodegenThingol.Pretty o str))
       || ($$ "`" |-- Scan.repeat1 (Scan.unless ($$ "`") (Scan.one Symbol.not_eof))
-            --| $$ "`" >> (fn ["_"] => Name | s => error ("malformed antiquote: " ^ implode s)))
+            --| $$ "`" >> (fn ["_"] => CodegenThingol.Name | s => error ("malformed antiquote: " ^ implode s)))
       || Scan.repeat1
            (Scan.unless ($$ "`") (Scan.one Symbol.not_eof)) >> (CodegenThingol.Pretty o str o implode)
     )) ((Symbol.explode o Symbol.strip_blanks) s)
@@ -234,7 +227,7 @@
       * (string -> itype pretty_syntax option)
       * (string -> iexpr pretty_syntax option)
     -> string list option
-    -> module -> unit)
+    -> CodegenThingol.module -> unit)
     * OuterParse.token list;
 
 fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator, postproc)
@@ -244,7 +237,7 @@
     fun pretty_of_prim resolv (name, primdef) =
       let
         fun pr (CodegenThingol.Pretty p) = p
-          | pr Name = (str o resolv) name;
+          | pr CodegenThingol.Name = (str o resolv) name;
       in case AList.lookup (op = : string * string -> bool) primdef target
        of NONE => error ("no primitive definition for " ^ quote name)
         | SOME ps => (case map pr ps
@@ -256,11 +249,11 @@
   in
     module
     |> debug 3 (fn _ => "selecting submodule...")
-    |> (if is_some select then (partof o the) select else I)
+    |> (if is_some select then (CodegenThingol.partof o the) select else I)
     |> debug 3 (fn _ => "preprocessing...")
     |> preprocess
     |> debug 3 (fn _ => "serializing...")
-    |> serialize (from_defs (pretty_of_prim, (class_syntax : string -> string option, tyco_syntax, const_syntax)))
+    |> CodegenThingol.serialize (from_defs (pretty_of_prim, (class_syntax : string -> string option, tyco_syntax, const_syntax)))
          from_module' validator postproc nspgrp name_root
     |> K ()
   end;
@@ -343,7 +336,7 @@
 
 fun pretty_list thingol_nil thingol_cons (target_pred, target_cons) =
   let
-    fun dest_cons (IApp (IApp (IConst ((c, _), _), e1), e2)) =
+    fun dest_cons (IConst ((c, _), _) `$ e1 `$ e2) =
           if c = thingol_cons
           then SOME (e1, e2)
           else NONE
@@ -355,7 +348,7 @@
         pr (INFX (target_pred, R)) e2
       ];
     fun pretty_compact fxy pr [e1, e2] =
-      case unfoldr dest_cons e2
+      case CodegenThingol.unfoldr dest_cons e2
        of (es, IConst ((c, _), _)) =>
             if c = thingol_nil
             then Pretty.enum "," "[" "]" (map (pr NOBR) (e1::es))
@@ -427,7 +420,7 @@
         | [p] => Pretty.block [p, Pretty.brk 1, tyco']
         | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
       end
-    and ml_from_type fxy (IType (tycoexpr as (tyco, tys))) =
+    and ml_from_type fxy (tycoexpr as tyco `%% tys) =
           (case tyco_syntax tyco
            of NONE => ml_from_tycoexpr fxy (tyco, tys)
             | SOME ((i, k), pr) =>
@@ -437,7 +430,7 @@
                   ^ string_of_int i ^ " to " ^ string_of_int k
                   ^ " expected")
                 else pr fxy ml_from_type tys)
-      | ml_from_type fxy (IFun (t1, t2)) =
+      | ml_from_type fxy (t1 `-> t2) =
           let
             val brackify = gen_brackify
               (case fxy
@@ -450,102 +443,109 @@
               ml_from_type (INFX (1, R)) t2
             ]
           end
-      | ml_from_type fxy (IVarT v) =
+      | ml_from_type fxy (ITyVar v) =
           str ("'" ^ v);
-    fun ml_from_expr fxy (e as IApp (e1, e2)) =
-          (case unfold_const_app e
+    fun typify trans ty p =
+      let
+        fun needs_type_t (tyco `%% tys) =
+            needs_type tyco
+            orelse trans
+              andalso exists needs_type_t tys
+        | needs_type_t (ITyVar _) =
+            false
+        | needs_type_t (ty1 `-> ty2) =
+            trans
+            andalso (needs_type_t ty1 orelse needs_type_t ty2);
+      in if needs_type_t ty
+        then
+          Pretty.enclose "(" ")" [
+            p,
+            str ":",
+            ml_from_type NOBR ty
+          ]
+        else p
+      end;
+    fun ml_from_expr fxy (e as IConst x) =
+          ml_from_app fxy (x, [])
+      | ml_from_expr fxy (IVar v) =
+          str v
+      | ml_from_expr fxy (e as e1 `$ e2) =
+          (case CodegenThingol.unfold_const_app e
            of SOME x => ml_from_app fxy x
             | NONE =>
                 brackify fxy [
                   ml_from_expr NOBR e1,
                   ml_from_expr BR e2
                 ])
-      | ml_from_expr fxy (e as IConst x) =
-          ml_from_app fxy (x, [])
-      | ml_from_expr fxy (IVarE (v, ty)) =
-          if needs_type ty
-            then
-              Pretty.enclose "(" ")" [
-                str v,
-                str ":",
-                ml_from_type NOBR ty
-              ]
-            else
-              str v
-      | ml_from_expr fxy (IAbs (e1, e2)) =
+      | ml_from_expr fxy ((v, ty) `|-> e) =
+          brackify BR [
+            str "fn",
+            typify true ty (str v),
+            str "=>",
+            ml_from_expr NOBR e
+          ]
+      | ml_from_expr fxy (IAbs (((ve, vty), be), _)) =
           brackify BR [
             str "fn",
-            ml_from_expr NOBR e1,
+            typify true vty (ml_from_expr NOBR ve),
             str "=>",
-            ml_from_expr NOBR e2
+            ml_from_expr NOBR be
           ]
-      | ml_from_expr fxy (e as ICase (_, [_])) =
+      | ml_from_expr fxy (e as ICase ((_, [_]), _)) =
           let
-            val (ps, e) = unfold_let e;
-            fun mk_val (p, e) = Pretty.block [
-                str "val ",
-                ml_from_expr fxy p,
-                str " =",
-                Pretty.brk 1,
-                ml_from_expr NOBR e,
+            val (ves, be) = CodegenThingol.unfold_let e;
+            fun mk_val ((ve, vty), se) = Pretty.block [
+                (Pretty.block o Pretty.breaks) [
+                  str "val",
+                  typify true vty (ml_from_expr NOBR ve),
+                  str "=",
+                  ml_from_expr NOBR se
+                ],
                 str ";"
-              ]
+              ];
           in Pretty.chunks [
-            [str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block,
-            [str ("in"), Pretty.fbrk, ml_from_expr NOBR e] |> Pretty.block,
+            [str ("let"), Pretty.fbrk, map mk_val ves |> Pretty.chunks] |> Pretty.block,
+            [str ("in"), Pretty.fbrk, ml_from_expr NOBR be] |> Pretty.block,
             str ("end")
           ] end
-      | ml_from_expr fxy (ICase (e, c::cs)) =
+      | ml_from_expr fxy (ICase (((de, dty), bse::bses), _)) =
           let
-            fun mk_clause definer (p, e) =
-              Pretty.block [
+            fun mk_clause definer (se, be) =
+              (Pretty.block o Pretty.breaks) [
                 str definer,
-                ml_from_expr NOBR p,
-                str " =>",
-                Pretty.brk 1,
-                ml_from_expr NOBR e
+                ml_from_expr NOBR se,
+                str "=>",
+                ml_from_expr NOBR be
               ]
           in brackify fxy (
             str "case"
-            :: ml_from_expr NOBR e
-            :: mk_clause "of " c
-            :: map (mk_clause "| ") cs
+            :: typify true dty (ml_from_expr NOBR de)
+            :: mk_clause "of" bse
+            :: map (mk_clause "|") bses
           ) end
       | ml_from_expr _ e =
-          error ("dubious expression: " ^ (Pretty.output o pretty_iexpr) e)
+          error ("dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iexpr) e)
     and ml_mk_app f es =
       if is_cons f andalso length es > 1 then
         [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
-      else if has_nsp f "mem" then 
-        Pretty.block [str "#", ml_from_label f] :: map (ml_from_expr BR) es
       else
         (str o resolv) f :: map (ml_from_expr BR) es
     and ml_from_app fxy (((c, ty), lss), es) =
       case map (ml_from_sortlookup BR) lss
        of [] =>
-            let
-              val p = from_app ml_mk_app ml_from_expr const_syntax fxy ((c, ty), es)
-            in if needs_type ty
-              then
-                Pretty.enclose "(" ")" [
-                  p,
-                  str ":",
-                  ml_from_type NOBR ty
-                ]
-              else
-                p
-            end
+            from_app ml_mk_app ml_from_expr const_syntax fxy ((c, ty), es)
+            |> typify false ty
         | lss =>
             brackify fxy (
               (str o resolv) c
               :: (lss
               @ map (ml_from_expr BR) es)
             );
-  in (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) end;
+  in (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) end;
 
 fun ml_fun_datatyp (is_cons, needs_type) (tyco_syntax, const_syntax) resolv =
   let
-    val (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
+    val (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) =
       ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv;
     fun chunk_defs ps =
       let
@@ -579,12 +579,18 @@
           let
             val shift = if null eq_tl then I else
               map (Pretty.block o single o Pretty.block o single);
+            fun mk_arg e ty =
+              ml_from_expr BR e
+              |> typify true ty
             fun mk_eq definer (pats, expr) =
               (Pretty.block o Pretty.breaks) (
                 [str definer, (str o resolv) name]
                 @ (if null pats
                    then [str ":", ml_from_type NOBR ty]
-                   else map from_tyvar sortctxt @ map (ml_from_expr BR) pats)
+                   else
+                     map from_tyvar sortctxt
+                     @ map2 mk_arg pats
+                         ((curry Library.take (length pats) o fst o CodegenThingol.unfold_fun) ty))
                 @ [str "=", ml_from_expr NOBR expr]
               )
           in
@@ -613,7 +619,7 @@
         fun mk_datatype definer (t, (vs, cs)) =
           (Pretty.block o Pretty.breaks) (
             str definer
-            :: ml_from_tycoexpr NOBR (t, map (IVarT o fst) vs)
+            :: ml_from_tycoexpr NOBR (t, map (ITyVar o fst) vs)
             :: str "="
             :: separate (str "|") (map mk_cons cs)
           )
@@ -629,22 +635,22 @@
     (from_prim, (_, tyco_syntax, const_syntax)) resolver prefix defs =
   let
     val resolv = resolver prefix;
-    val (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
+    val (ml_from_label, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) =
       ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv;
     val (ml_from_funs, ml_from_datatypes) =
       ml_fun_datatyp (is_cons, needs_type) (tyco_syntax, const_syntax) resolv;
     val filter_datatype =
       List.mapPartial
-        (fn (name, Datatype info) => SOME (name, info)
-          | (name, Datatypecons _) => NONE
+        (fn (name, CodegenThingol.Datatype info) => SOME (name, info)
+          | (name, CodegenThingol.Datatypecons _) => NONE
           | (name, def) => error ("datatype block containing illegal def: "
-                ^ (Pretty.output o pretty_def) def));
+                ^ (Pretty.output o CodegenThingol.pretty_def) def));
     fun filter_class defs = 
       case List.mapPartial
-        (fn (name, Class info) => SOME (name, info)
-          | (name, Classmember _) => NONE
+        (fn (name, CodegenThingol.Class info) => SOME (name, info)
+          | (name, CodegenThingol.Classmember _) => NONE
           | (name, def) => error ("class block containing illegal def: "
-                ^ (Pretty.output o pretty_def) def)) defs
+                ^ (Pretty.output o CodegenThingol.pretty_def) def)) defs
        of [class] => class
         | _ => error ("class block without class: " ^ (commas o map (quote o fst)) defs)
     fun ml_from_class (name, (supclasses, (v, membrs))) =
@@ -687,23 +693,23 @@
           ]
         :: map from_membr_fun membrs)
       end
-    fun ml_from_def (name, Undef) =
+    fun ml_from_def (name, CodegenThingol.Undef) =
           error ("empty definition during serialization: " ^ quote name)
-      | ml_from_def (name, Prim prim) =
+      | ml_from_def (name, CodegenThingol.Prim prim) =
           from_prim resolv (name, prim)
-      | ml_from_def (name, Typesyn (vs, ty)) =
+      | ml_from_def (name, CodegenThingol.Typesyn (vs, ty)) =
         (map (fn (vname, []) => () | _ =>
             error "can't serialize sort constrained type declaration to ML") vs;
           Pretty.block [
             str "type ",
-            ml_from_tycoexpr NOBR (name, map (IVarT o fst) vs),
+            ml_from_tycoexpr NOBR (name, map (ITyVar o fst) vs),
             str " =",
             Pretty.brk 1,
             ml_from_type NOBR ty,
             str ";"
             ]
           ) |> SOME
-      | ml_from_def (name, Classinst (((class, (tyco, arity)), suparities), memdefs)) =
+      | ml_from_def (name, CodegenThingol.Classinst (((class, (tyco, arity)), suparities), memdefs)) =
           let
             val definer = if null arity then "val" else "fun"
             fun from_supclass (supclass, (supinst, lss)) =
@@ -749,23 +755,21 @@
             ] |> SOME
           end;
   in case defs
-   of (_, Fun _)::_ => (SOME o ml_from_funs o map (fn (name, Fun info) => (name, info))) defs
-    | (_, Datatypecons _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
-    | (_, Datatype _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
-    | (_, Class _)::_ => (SOME o ml_from_class o filter_class) defs
-    | (_, Classmember _)::_ => (SOME o ml_from_class o filter_class) defs
+   of (_, CodegenThingol.Fun _)::_ => (SOME o ml_from_funs o map (fn (name, CodegenThingol.Fun info) => (name, info))) defs
+    | (_, CodegenThingol.Datatypecons _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
+    | (_, CodegenThingol.Datatype _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs
+    | (_, CodegenThingol.Class _)::_ => (SOME o ml_from_class o filter_class) defs
+    | (_, CodegenThingol.Classmember _)::_ => (SOME o ml_from_class o filter_class) defs
     | [def] => ml_from_def def
     | defs => error ("illegal mutual dependencies: " ^ (commas o map fst) defs)
   end;
 
 fun ml_annotators (nsp_dtcon, nsp_class, is_int_tyco) =
   let
-    fun needs_type (IType (tyco, _)) =
-          has_nsp tyco nsp_class
-          orelse is_int_tyco tyco
-      | needs_type _ =
-          false;
-    fun is_cons c = has_nsp c nsp_dtcon;
+    fun needs_type tyco =
+      CodegenThingol.has_nsp tyco nsp_class
+      orelse is_int_tyco tyco;
+    fun is_cons c = CodegenThingol.has_nsp c nsp_dtcon;
   in (is_cons, needs_type) end;
 
 in
@@ -788,21 +792,22 @@
     fun eta_expander module const_syntax s =
       case const_syntax s
        of SOME ((i, _), _) => i
-        | _ => if has_nsp s nsp_dtcon
-               then case get_def module s
-                of Datatypecons dtname => case get_def module dtname
-                of Datatype (_, cs) =>
+        | _ => if CodegenThingol.has_nsp s nsp_dtcon
+               then case CodegenThingol.get_def module s
+                of CodegenThingol.Datatypecons dtname =>
+                  case CodegenThingol.get_def module dtname
+                of CodegenThingol.Datatype (_, cs) =>
                   let val l = AList.lookup (op =) cs s |> the |> length
                   in if l >= 2 then l else 0 end
                 else 0;
     fun preprocess const_syntax module =
       module
       |> debug 3 (fn _ => "eta-expanding...")
-      |> eta_expand (eta_expander module const_syntax)
+      |> CodegenThingol.eta_expand (eta_expander module const_syntax)
       |> debug 3 (fn _ => "eta-expanding polydefs...")
-      |> eta_expand_poly
+      |> CodegenThingol.eta_expand_poly
       |> debug 3 (fn _ => "unclashing expression/type variables...")
-      |> unclash_vars_tvars;
+      |> CodegenThingol.unclash_vars_tvars;
     val parse_multi =
       OuterParse.name
       #-> (fn "dir" => 
@@ -861,10 +866,10 @@
       end;
     fun hs_from_tycoexpr fxy (tyco, tys) =
       brackify fxy ((str o resolv) tyco :: map (hs_from_type BR) tys)
-    and hs_from_type fxy (IType (tycoexpr as (tyco, tys))) =
+    and hs_from_type fxy (tycoexpr as tyco `%% tys) =
           (case tyco_syntax tyco
            of NONE =>
-                hs_from_tycoexpr fxy tycoexpr
+                hs_from_tycoexpr fxy (tyco, tys)
             | SOME ((i, k), pr) =>
                 if not (i <= length tys andalso length tys <= k)
                 then error ("number of argument mismatch in customary serialization: "
@@ -872,71 +877,80 @@
                   ^ string_of_int i ^ " to " ^ string_of_int k
                   ^ " expected")
                 else pr fxy hs_from_type tys)
-      | hs_from_type fxy (IFun (t1, t2)) =
+      | hs_from_type fxy (t1 `-> t2) =
           brackify_infix (1, R) fxy [
             hs_from_type (INFX (1, X)) t1,
             str "->",
             hs_from_type (INFX (1, R)) t2
           ]
-      | hs_from_type fxy (IVarT v) =
+      | hs_from_type fxy (ITyVar v) =
           str v;
     fun hs_from_sctxt_tycoexpr (sctxt, tycoexpr) =
       Pretty.block [hs_from_sctxt sctxt, hs_from_tycoexpr NOBR tycoexpr]
     fun hs_from_sctxt_type (sctxt, ty) =
       Pretty.block [hs_from_sctxt sctxt, hs_from_type NOBR ty]
-    fun hs_from_expr fxy (e as IApp (e1, e2)) =
-          (case unfold_const_app e
+    fun hs_from_expr fxy (e as IConst x) =
+          hs_from_app fxy (x, [])
+      | hs_from_expr fxy (e as (e1 `$ e2)) =
+          (case CodegenThingol.unfold_const_app e
            of SOME x => hs_from_app fxy x
             | _ =>
                 brackify fxy [
                   hs_from_expr NOBR e1,
                   hs_from_expr BR e2
                 ])
-      | hs_from_expr fxy (e as IConst x) =
-          hs_from_app fxy (x, [])
-      | hs_from_expr fxy (IVarE (v, _)) =
-          str v
-      | hs_from_expr fxy (e as IAbs _) =
+      | hs_from_expr fxy (IVar v) =
+          (str o String.implode o nth_map 0 Char.toLower o String.explode) v
+      | hs_from_expr fxy (e as _ `|-> _) =
           let
-            val (es, e) = unfold_abs e
+            val (es, e) = CodegenThingol.unfold_abs e
           in
             brackify BR (
               str "\\"
-              :: map (hs_from_expr BR) es @ [
+              :: map (hs_from_expr BR o fst) es @ [
               str "->",
               hs_from_expr NOBR e
             ])
           end
-      | hs_from_expr fxy (e as ICase (_, [_])) =
+      | hs_from_expr fxy (e as IAbs _) =
           let
-            val (ps, body) = unfold_let e;
-            fun mk_bind (p, e) = Pretty.block [
+            val (es, e) = CodegenThingol.unfold_abs e
+          in
+            brackify BR (
+              str "\\"
+              :: map (hs_from_expr BR o fst) es @ [
+              str "->",
+              hs_from_expr NOBR e
+            ])
+          end
+      | hs_from_expr fxy (e as ICase ((_, [_]), _)) =
+          let
+            val (ps, body) = CodegenThingol.unfold_let e;
+            fun mk_bind ((p, _), e) = (Pretty.block o Pretty.breaks) [
                 hs_from_expr BR p,
-                str " =",
-                Pretty.brk 1,
+                str "=",
                 hs_from_expr NOBR e
               ];
           in Pretty.chunks [
             [str ("let"), Pretty.fbrk, map mk_bind ps |> Pretty.chunks] |> Pretty.block,
             [str ("in "), hs_from_expr NOBR body] |> Pretty.block
           ] end
-      | hs_from_expr fxy (ICase (e, cs)) =
+      | hs_from_expr fxy (ICase (((de, _), bses), _)) =
           let
-            fun mk_clause (p, e) =
-              Pretty.block [
-                hs_from_expr NOBR p,
-                str " ->",
-                Pretty.brk 1,
-                hs_from_expr NOBR e
+            fun mk_clause (se, be) =
+              (Pretty.block o Pretty.breaks) [
+                hs_from_expr NOBR se,
+                str "->",
+                hs_from_expr NOBR be
               ]
           in Pretty.block [
             str "case",
             Pretty.brk 1,
-            hs_from_expr NOBR e,
+            hs_from_expr NOBR de,
             Pretty.brk 1,
             str "of",
             Pretty.fbrk,
-            (Pretty.chunks o map mk_clause) cs
+            (Pretty.chunks o map mk_clause) bses
           ] end
     and hs_mk_app c es =
       (str o resolv) c :: map (hs_from_expr BR) es
@@ -954,11 +968,11 @@
             hs_from_expr NOBR rhs
           ]
       in Pretty.chunks (map (from_eq name) eqs) end;
-    fun hs_from_def (name, Undef) =
+    fun hs_from_def (name, CodegenThingol.Undef) =
           error ("empty statement during serialization: " ^ quote name)
-      | hs_from_def (name, Prim prim) =
+      | hs_from_def (name, CodegenThingol.Prim prim) =
           from_prim resolv_here (name, prim)
-      | hs_from_def (name, Fun (eqs, (sctxt, ty))) =
+      | hs_from_def (name, CodegenThingol.Fun (eqs, (sctxt, ty))) =
           let
             val body = hs_from_funeqs (name, eqs);
           in if with_typs then
@@ -971,15 +985,15 @@
               body
             ] |> SOME
           else SOME body end
-      | hs_from_def (name, Typesyn (vs, ty)) =
+      | hs_from_def (name, CodegenThingol.Typesyn (sctxt, ty)) =
           Pretty.block [
             str "type ",
-            hs_from_sctxt_tycoexpr (vs, (resolv_here name, map (IVarT o fst) vs)),
+            hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt)),
             str " =",
             Pretty.brk 1,
             hs_from_sctxt_type ([], ty)
           ] |> SOME
-      | hs_from_def (name, Datatype (vs, constrs)) =
+      | hs_from_def (name, CodegenThingol.Datatype (sctxt, constrs)) =
           let
             fun mk_cons (co, tys) =
               (Pretty.block o Pretty.breaks) (
@@ -989,7 +1003,7 @@
           in
             Pretty.block ((
               str "data "
-              :: hs_from_sctxt_type (vs, IType (resolv_here name, map (IVarT o fst) vs))
+              :: hs_from_sctxt_tycoexpr (sctxt, (resolv_here name, map (ITyVar o fst) sctxt))
               :: str " ="
               :: Pretty.brk 1
               :: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs)
@@ -998,9 +1012,9 @@
               str "deriving Show"
             ])
           end |> SOME
-      | hs_from_def (_, Datatypecons _) =
+      | hs_from_def (_, CodegenThingol.Datatypecons _) =
           NONE
-      | hs_from_def (name, Class (supclasss, (v, membrs))) =
+      | hs_from_def (name, CodegenThingol.Class (supclasss, (v, membrs))) =
           let
             fun mk_member (m, (sctxt, ty)) =
               Pretty.block [
@@ -1018,14 +1032,14 @@
               Pretty.chunks (map mk_member membrs)
             ] |> SOME
           end
-      | hs_from_def (name, Classmember _) =
+      | hs_from_def (name, CodegenThingol.Classmember _) =
           NONE
-      | hs_from_def (_, Classinst (((clsname, (tyco, arity)), _), memdefs)) = 
+      | hs_from_def (_, CodegenThingol.Classinst (((clsname, (tyco, arity)), _), memdefs)) = 
           Pretty.block [
             str "instance ",
-            hs_from_sctxt_tycoexpr (arity, (clsname, map (IVarT o fst) arity)),
+            hs_from_sctxt_tycoexpr (arity, (clsname, map (ITyVar o fst) arity)),
             str " ",
-            hs_from_sctxt_tycoexpr (arity, (tyco, map (IVarT o fst) arity)),
+            hs_from_sctxt_tycoexpr (arity, (tyco, map (ITyVar o fst) arity)),
             str " where",
             Pretty.fbrk,
             Pretty.chunks (map (fn (m, (_, (eqs, _))) => hs_from_funeqs (m, eqs)) memdefs)
@@ -1045,7 +1059,7 @@
       "import", "default", "forall", "let", "in", "class", "qualified", "data",
       "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
     ] @ [
-      "Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "negate"
+      "Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "not", "negate"
     ];
     fun hs_from_module imps ((_, name), ps) =
       (Pretty.chunks) (
@@ -1070,7 +1084,7 @@
     fun preprocess const_syntax module =
       module
       |> debug 3 (fn _ => "eta-expanding...")
-      |> eta_expand (eta_expander const_syntax)
+      |> CodegenThingol.eta_expand (eta_expander const_syntax)
   in
     (Scan.optional (OuterParse.name >> (fn "no_typs" => false | s => Scan.fail_with (fn _ => "illegal flag: " ^ quote s) true)) true
     #-> (fn with_typs => parse_multi_file ((K o K) NONE) "hs" (serializer with_typs)))
diff -r fd8f152cfc76 -r f237c0cb3882 src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Wed Mar 01 10:37:00 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Wed Mar 01 13:47:42 2006 +0100
@@ -5,53 +5,58 @@
 Intermediate language ("Thin-gol") for code extraction.
 *)
 
+infix 8 `%%;
+infixr 6 `->;
+infixr 6 `-->;
+infix 4 `$;
+infix 4 `$$;
+infixr 3 `|->;
+infixr 3 `|-->;
+
 signature BASIC_CODEGEN_THINGOL =
 sig
   type vname = string;
-  datatype classlookup = Instance of string * classlookup list list
-                       | Lookup of class list * (string * int);
+  type sortcontext = ClassPackage.sortcontext;
+  datatype iclasslookup = Instance of string * iclasslookup list list
+                        | Lookup of class list * (string * int);
   datatype itype =
-      IType of string * itype list
-    | IFun of itype * itype
-    | IVarT of vname;
-  type ityp = ClassPackage.sortcontext * itype;
+      `%% of string * itype list
+    | `-> of itype * itype
+    | ITyVar of vname;
   datatype iexpr =
-      IConst of (string * itype) * classlookup list list
-    | IVarE of vname * itype
-    | IApp of iexpr * iexpr
-    | IAbs of iexpr * iexpr
-    | ICase of iexpr * (iexpr * iexpr) list;
+      IConst of (string * itype) * iclasslookup list list
+    | IVar of vname
+    | `$ of iexpr * iexpr
+    | `|-> of (vname * itype) * iexpr
+    | IAbs of ((iexpr * itype) * iexpr) * iexpr
+        (* (((binding expression (ve), binding type (vty)),
+                body expression (be)), native expression (e0)) *)
+    | ICase of ((iexpr * itype) * (iexpr * iexpr) list) * iexpr;
+        (* ((discrimendum expression (de), discrimendum type (dty)),
+                [(selector expression (se), body expression (be))]),
+                native expression (e0)) *)
 end;
 
 signature CODEGEN_THINGOL =
 sig
   include BASIC_CODEGEN_THINGOL;
-  val mk_funs: itype list * itype -> itype;
-  val mk_apps: iexpr * iexpr list -> iexpr;
-  val mk_abss: iexpr list * iexpr -> iexpr;
+  val `--> : itype list * itype -> itype;
+  val `$$ : iexpr * iexpr list -> iexpr;
+  val `|--> : (vname * itype) list * iexpr -> iexpr;
   val pretty_itype: itype -> Pretty.T;
   val pretty_iexpr: iexpr -> Pretty.T;
   val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list;
   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 -> iexpr list * iexpr;
-  val unfold_let: iexpr -> (iexpr * iexpr) list * iexpr;
+  val unfold_abs: iexpr -> (iexpr * itype) list * iexpr;
+  val unfold_let: iexpr -> ((iexpr * itype) * iexpr) list * iexpr;
   val unfold_const_app: iexpr ->
-    (((string * itype) * classlookup list list) * iexpr list) option;
+    (((string * itype) * iclasslookup list list) * iexpr list) option;
   val ensure_pat: iexpr -> iexpr;
-  val itype_of_iexpr: iexpr -> itype;
 
-  val `%% : string * itype list -> itype;
-  val `-> : itype * itype -> itype;
-  val `--> : itype list * itype -> itype;
-  val `$ : iexpr * iexpr -> iexpr;
-  val `$$ : iexpr * iexpr list -> iexpr;
-  val `|-> : iexpr * iexpr -> iexpr;
-  val `|--> : iexpr list * iexpr -> iexpr;
-
-  type funn = (iexpr list * iexpr) list * ityp;
-  type datatyp = ClassPackage.sortcontext * (string * itype list) list;
+  type funn = (iexpr list * iexpr) list * (sortcontext * itype);
+  type datatyp = sortcontext * (string * itype list) list;
   datatype prim =
       Pretty of Pretty.T
     | Name;
@@ -62,10 +67,10 @@
     | Typesyn of (vname * sort) list * itype
     | Datatype of datatyp
     | Datatypecons of string
-    | Class of class list * (vname * (string * ityp) list)
+    | Class of class list * (vname * (string * (sortcontext * itype)) list)
     | Classmember of class
     | Classinst of ((class * (string * (vname * sort) list))
-          * (class * (string * classlookup list list)) list)
+          * (class * (string * iclasslookup list list)) list)
         * (string * (string * funn)) list;
   type module;
   type transact;
@@ -144,31 +149,25 @@
 
 (* language representation *)
 
-infix 8 `%%;
-infixr 6 `->;
-infixr 6 `-->;
-infix 4 `$;
-infix 4 `$$;
-infixr 3 `|->;
-infixr 3 `|-->;
-
 type vname = string;
 
-datatype classlookup = Instance of string * classlookup list list
-                     | Lookup of class list * (string * int);
+type sortcontext = ClassPackage.sortcontext;
+datatype iclasslookup = Instance of string * iclasslookup list list
+                      | Lookup of class list * (string * int);
 
 datatype itype =
-    IType of string * itype list
-  | IFun of itype * itype
-  | IVarT of vname;
-type ityp = ClassPackage.sortcontext * itype;
+    `%% of string * itype list
+  | `-> of itype * itype
+  | ITyVar of vname;
 
 datatype iexpr =
-    IConst of (string * itype) * classlookup list list
-  | IVarE of vname * itype
-  | IApp of iexpr * iexpr
-  | IAbs of iexpr * iexpr
-  | ICase of iexpr * (iexpr * iexpr) list;
+    IConst of (string * itype) * iclasslookup list list
+  | IVar of vname
+  | `$ of iexpr * iexpr
+  | `|-> of (vname * itype) * iexpr
+  | IAbs of ((iexpr * itype) * iexpr) * iexpr
+  | ICase of ((iexpr * itype) * (iexpr * iexpr) list) * iexpr;
+    (*see also signature*)
 
 (*
   variable naming conventions
@@ -194,64 +193,62 @@
     constructors (co, tys)  constr
  *)
 
-val mk_funs = Library.foldr IFun;
-val mk_apps = Library.foldl IApp;
-val mk_abss = Library.foldr IAbs;
-
-val op `%% = IType;
-val op `-> = IFun;
-val op `$ = IApp;
-val op `|-> = IAbs;
-val op `--> = mk_funs;
-val op `$$ = mk_apps;
-val op `|--> = mk_abss;
+val op `--> = Library.foldr (op `->);
+val op `$$ = Library.foldl (op `$);
+val op `|--> = Library.foldr (op `|->);
 
 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)) =
+fun pretty_itype (tyco `%% tys) =
+      Pretty.block (Pretty.str tyco :: map pretty_itype tys)
+  | pretty_itype (ty1 `-> ty2) =
       Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
-  | pretty_itype (IVarT v) =
+  | pretty_itype (ITyVar v) =
       Pretty.str v;
 
-fun pretty_iexpr (IConst ((c, ty), _)) =
-      Pretty.block [Pretty.str (c ^ "::"), pretty_itype ty]
-  | pretty_iexpr (IVarE (v, ty)) =
-      Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty]
-  | pretty_iexpr (IApp (e1, e2)) =
-      Pretty.enclose "(" ")" [pretty_iexpr e1, Pretty.brk 1, pretty_iexpr e2]
-  | pretty_iexpr (IAbs (e1, e2)) =
-      Pretty.enclose "(" ")" [pretty_iexpr e1, Pretty.brk 1, Pretty.str "|->", Pretty.brk 1, pretty_iexpr e2]
-  | pretty_iexpr (ICase (e, cs)) =
-      Pretty.enclose "(" ")" [
-        Pretty.str "case ",
+fun pretty_iexpr (IConst ((c, _), _)) =
+      Pretty.str c
+  | pretty_iexpr (IVar v) =
+      Pretty.str ("?" ^ v)
+  | pretty_iexpr (e1 `$ e2) =
+      (Pretty.enclose "(" ")" o Pretty.breaks)
+        [pretty_iexpr e1, pretty_iexpr e2]
+  | pretty_iexpr ((v, ty) `|-> e) =
+      (Pretty.enclose "(" ")" o Pretty.breaks)
+        [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iexpr e]
+  | pretty_iexpr (IAbs (((e1, _), e2), _)) =
+      (Pretty.enclose "(" ")" o Pretty.breaks)
+        [pretty_iexpr e1, Pretty.str "|->", pretty_iexpr e2]
+  | pretty_iexpr (ICase (((e, _), cs), _)) =
+      (Pretty.enclose "(" ")" o Pretty.breaks) [
+        Pretty.str "case",
         pretty_iexpr e,
         Pretty.enclose "(" ")" (map (fn (p, e) =>
-          Pretty.block [
+          (Pretty.block o Pretty.breaks) [
             pretty_iexpr p,
-            Pretty.str " => ",
+            Pretty.str "=>",
             pretty_iexpr e
           ]
         ) cs)
       ];
 
 val unfold_fun = unfoldr
-  (fn IFun t => SOME t
+  (fn op `-> t => SOME t
     | _ => NONE);
 
 val unfold_app = unfoldl
-  (fn IApp e => SOME e
+  (fn op `$ e => SOME e
     | _ => NONE);
 
 val unfold_abs = unfoldr
-  (fn IAbs b => SOME b
+  (fn (v, ty) `|-> e => SOME ((IVar v, ty), e)
+    | IAbs (((e1, ty), e2), _) => SOME ((e1, ty), e2)
     | _ => NONE)
 
 val unfold_let = unfoldr
-  (fn ICase (e, [(p, e')]) => SOME ((p, e), e')
+  (fn ICase (((de, dty), [(se, be)]), _) => SOME (((se, dty), de), be)
     | _ => NONE);
 
 fun unfold_const_app e = 
@@ -259,59 +256,36 @@
   of (IConst x, es) => SOME (x, es)
    | _ => NONE;
 
-fun map_itype f_itype (IType (tyco, tys)) =
-      tyco `%% map f_itype tys
-  | map_itype f_itype (IFun (t1, t2)) =
-      f_itype t1 `-> f_itype t2
-  | map_itype _ (ty as IVarT _) =
-      ty;
+fun map_itype _ (ty as ITyVar _) =
+      ty
+  | map_itype f (tyco `%% tys) =
+      tyco `%% map f tys
+  | map_itype f (t1 `-> t2) =
+      f t1 `-> f t2;
 
-fun map_iexpr f (IApp (e1, e2)) =
-      f e1 `$ f e2
-  | map_iexpr f (IAbs (v, e)) =
-      v `|-> f e
-  | map_iexpr f (ICase (e, ps)) =
-      ICase (f e, map (fn (p, e) => (f p, f e)) ps)
-  | map_iexpr _ (e as IConst _) =
+fun map_iexpr _ (e as IConst _) =
       e
-  | map_iexpr _ (e as IVarE _) =
-      e;
-
-fun map_atype f (ty as IVarT _) =
-      f ty
-  | map_atype f ty =
-      map_itype (map_atype f) ty;
-
-fun map_aexpr f (e as IConst _) = 
-      f e
-  | map_aexpr f (e as IVarE _) =
-      f e
-  | map_aexpr f e =
-      map_iexpr (map_aexpr f) e;
+  | map_iexpr _ (e as IVar _) =
+      e
+  | map_iexpr f (e1 `$ e2) =
+      f e1 `$ f e2
+  | map_iexpr f ((v, ty) `|-> e) =
+      (v, ty) `|-> f e
+  | map_iexpr f (IAbs (((ve, vty), be), e0)) =
+      IAbs (((f ve, vty), f be), e0)
+  | map_iexpr f (ICase (((de, dty), bses), e0)) =
+      ICase (((f de, dty), map (fn (se, be) => (f se, f be)) bses), e0);
 
 fun map_iexpr_itype f =
   let
-    fun mapp (IConst ((c, ty), ctxt)) = IConst ((c, f ty), ctxt)
-      | mapp (IVarE (v, ty)) = IVarE (v, f ty)
-  in map_aexpr mapp end;
-
-fun fold_atype f (IFun (ty1, ty2)) =
-      fold_atype f ty1 #> fold_atype f ty2
-  | fold_atype f (ty as IType _) =
-      f ty
-  | fold_atype f (ty as IVarT _) =
-      f ty;
-
-fun fold_aexpr f (IApp (e1, e2)) =
-      fold_aexpr f e1 #> fold_aexpr f e2
-  | fold_aexpr f (IAbs (v, e)) =
-      fold_aexpr f e
-  | fold_aexpr f (ICase (e, ps)) =
-      fold_aexpr f e #> fold (fn (p, e) => fold_aexpr f p #> fold_aexpr f e) ps
-  | fold_aexpr f (e as IConst _) =
-      f e
-  | fold_aexpr f (e as IVarE _) =
-      f e;
+    fun mapp (IConst ((c, ty), sctxt)) = IConst ((c, f ty), sctxt)
+      | mapp ((v, ty) `|-> e) = (v, f ty) `|-> mapp e
+      | mapp (IAbs (((ve, vty), be), e0)) =
+          IAbs (((mapp ve, f vty), mapp be), e0)
+      | mapp (ICase (((de, dty), bses), e0)) =
+          ICase (((mapp de, f dty), map (fn (se, be) => (mapp se, mapp be)) bses), e0)
+      | mapp e = map_iexpr mapp e;
+  in mapp end;
 
 fun eq_ityp ((sctxt1, ty1), (sctxt2, ty2)) =
   let
@@ -322,18 +296,18 @@
         | 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 =
+    fun eq (ITyVar v1) (ITyVar 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 =
+      | eq (tyco1 `%% tys1) (tyco2 `%% tys2) subs =
           if tyco1 <> tyco2
           then raise NO_MATCH
           else subs |> fold2 eq tys1 tys2
-      | eq (IFun (ty11, ty12)) (IFun (ty21, ty22)) subs =
+      | eq (ty11 `-> ty12) (ty21 `-> ty22) subs =
           subs |> eq ty11 ty21 |> eq ty12 ty22
       | eq _ _ _ = raise NO_MATCH;
   in
@@ -343,44 +317,36 @@
 
 fun instant_itype f =
   let
-    fun instant (IVarT x) = f x
+    fun instant (ITyVar x) = f x
       | instant y = map_itype instant y;
   in map_itype instant end;
 
-fun itype_of_iexpr (IConst ((_, ty), s)) = ty
-  | itype_of_iexpr (IVarE (_, ty)) = ty
-  | itype_of_iexpr (e as IApp (e1, e2)) = (case itype_of_iexpr e1
-      of (IFun (ty2, ty')) =>
-            if ty2 = itype_of_iexpr e2
-            then ty'
-            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 (IAbs (e1, e2)) = itype_of_iexpr e1 `-> itype_of_iexpr e2
-  | itype_of_iexpr (ICase ((_, [(_, e)]))) = itype_of_iexpr e;
-
 fun ensure_pat (e as IConst (_, [])) = e
-  | ensure_pat (e as IVarE _) = e
-  | ensure_pat (e as IApp (e1, e2)) =
-      (ensure_pat e1 `$ ensure_pat e2; e)
+  | ensure_pat (e as IVar _) = e
+  | ensure_pat (e as (e1 `$ e2)) =
+      (ensure_pat e1; ensure_pat e2; e)
   | ensure_pat e =
       error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e);
 
-fun type_vnames ty = 
-  let
-    fun extr (IVarT v) =
-          insert (op =) v
-      | extr _ = I;
-  in fold_atype extr ty end;
+fun has_tyvars (_ `%% tys) =
+      exists has_tyvars tys
+  | has_tyvars (ITyVar _) =
+      true
+  | has_tyvars (ty1 `-> ty2) =
+      has_tyvars ty1 orelse has_tyvars ty2;
 
-fun expr_names e =
-  let
-    fun extr (IConst ((c, _), _)) =
-          insert (op =) c
-      | extr (IVarE (v, _)) =
-          insert (op =) v
-  in fold_aexpr extr e end;
+fun varnames_of (IConst ((c, _), _)) =
+      I
+  | varnames_of (IVar v) =
+      insert (op =) v
+  | varnames_of (e1 `$ e2) =
+      varnames_of e1 #> varnames_of e2
+  | varnames_of ((v, _) `|-> e) =
+      insert (op =) v #> varnames_of e
+  | varnames_of (IAbs (((ve, _), be), _)) =
+      varnames_of ve #> varnames_of be
+  | varnames_of (ICase (((de, _), bses), _)) =
+      varnames_of de #> fold (fn (be, se) => varnames_of be #> varnames_of se) bses;
 
 fun invent seed used =
   let
@@ -393,8 +359,8 @@
 
 (* type definitions *)
 
-type funn = (iexpr list * iexpr) list * ityp;
-type datatyp = ClassPackage.sortcontext * (string * itype list) list;
+type funn = (iexpr list * iexpr) list * (sortcontext * itype);
+type datatyp = sortcontext * (string * itype list) list;
 
 datatype prim =
     Pretty of Pretty.T
@@ -407,10 +373,10 @@
   | Typesyn of (vname * sort) list * itype
   | Datatype of datatyp
   | Datatypecons of string
-  | Class of class list * (vname * (string * ityp) list)
+  | Class of class list * (vname * (string * (sortcontext * itype)) list)
   | Classmember of class
   | Classinst of ((class * (string * (vname * sort) list))
-        * (class * (string * classlookup list list)) list)
+        * (class * (string * iclasslookup list list)) list)
       * (string * (string * funn)) list;
 
 datatype node = Def of def | Module of node Graph.T;
@@ -784,14 +750,14 @@
           then error "too many member definitions given"
           else ();
         fun instant (w, ty) v =
-          if v = w then ty else IVarT v;
+          if v = w then ty else ITyVar 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, (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),
+                     instant_itype (instant (v, tyco `%% map (ITyVar o fst) arity)) ty),
                   (sortctxt', ty'))
                 then (m, (m', (check_funeqs eqs, (sortctxt', ty'))))
                 else error ("inconsistent type for member definition " ^ quote m)
@@ -926,28 +892,25 @@
               (fst o unfold_fun) ty
               |> curry Library.drop (length es)
               |> curry Library.take add_n
-            val add_vars =
-              map2 (curry IVarE) (Term.invent_names (fold expr_names es []) "x" add_n) tys;
+            val vs = (Term.invent_names (fold varnames_of es []) "x" add_n)
           in
-            add_vars `|--> IConst ((f, ty), ls) `$$ map eta es `$$ add_vars
+            vs ~~ tys `|--> IConst ((f, ty), ls) `$$ map eta es `$$ map IVar vs
           end
        | NONE => map_iexpr eta e;
   in (map_defs o map_def_fun o map_def_fun_expr) eta end;
 
 val eta_expand_poly =
   let
-    fun eta (funn as ([([], e)], cty as (sortctxt, (ty as IFun (ty1, ty2))))) =
-          if (not o null) sortctxt
-            orelse null (type_vnames ty [])
+    fun eta (funn as ([([], e)], cty as (sctxt, (ty as (ty1 `-> ty2))))) =
+          if (not o null) sctxt
+            orelse (not o has_tyvars) ty
           then funn
-          else
-            (case unfold_abs e
-             of ([], e) =>
-                  let
-                    val add_var = IVarE (hd (Term.invent_names (expr_names e []) "x" 1), ty1)
-                  in (([([add_var], e `$ add_var)], cty)) end
-              | eq => 
-                  (([eq], cty)))
+          else (case unfold_abs e
+           of ([], e) =>
+              let
+                val add_var = IVar (hd (Term.invent_names (varnames_of e []) "x" 1))
+              in (([([add_var], e `$ add_var)], cty)) end
+            | _ =>  funn)
       | eta funn = funn;
   in (map_defs o map_def_fun) eta end;
 
@@ -956,13 +919,13 @@
     fun unclash (eqs, (sortctxt, ty)) =
       let
         val used_expr =
-          fold (fn (pats, rhs) => fold expr_names pats #> expr_names rhs) eqs [];
+          fold (fn (pats, rhs) => fold varnames_of pats #> varnames_of rhs) eqs [];
         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;
         val rename =
           perhaps (AList.lookup (op =) rename_map);
-        val rename_typ = instant_itype (IVarT o rename);
+        val rename_typ = instant_itype (ITyVar o rename);
         val rename_expr = map_iexpr_itype rename_typ;
         fun rename_eq (args, rhs) = (map rename_expr args, rename_expr rhs)
       in
diff -r fd8f152cfc76 -r f237c0cb3882 src/Pure/Tools/nbe.ML
--- a/src/Pure/Tools/nbe.ML	Wed Mar 01 10:37:00 2006 +0100
+++ b/src/Pure/Tools/nbe.ML	Wed Mar 01 13:47:42 2006 +0100
@@ -44,8 +44,9 @@
     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 modl_new = CodegenPackage.get_root_module thy';
+    val diff = CodegenThingol.diff_module (modl_new, modl_old);
+    val _ = writeln ("new definitions: " ^ (commas o map fst) diff);
     val _ = (tab := nbe_tab;
              Library.seq (use_show o NBE_Codegen.generate defined) diff)
     val thy'' = NBE_Data.put (!tab) thy'
diff -r fd8f152cfc76 -r f237c0cb3882 src/Pure/Tools/nbe_codegen.ML
--- a/src/Pure/Tools/nbe_codegen.ML	Wed Mar 01 10:37:00 2006 +0100
+++ b/src/Pure/Tools/nbe_codegen.ML	Wed Mar 01 13:47:42 2006 +0100
@@ -10,7 +10,6 @@
 fun MLname
 val quote = quote;
 
-FIXME CodegenThingol names!
 *)
 
 signature NBE_CODEGEN =
@@ -86,46 +85,53 @@
 		   S.abs (S.tup []) (S.app Eval_C
 	(S.quote nm))]);
 
+open BasicCodegenThingol;
 
 fun mk_rexpr defined nm ar =
   let fun mk args t = case t of
-    CodegenThingol.IConst((s,_),_) => 
+    IConst((s,_),_) => 
     if s=nm then selfcall nm ar args
     else if defined s then S.nbe_apps (MLname s) args
     else S.app Eval_Constr (S.tup [S.quote s,S.list args ])
-  | CodegenThingol.IVarE(s,_) => S.nbe_apps (MLvname s) args
-  | CodegenThingol.IApp(e1,e2) => mk (args @ [mk [] e2]) e1
-  | CodegenThingol.IAbs(CodegenThingol.IVarE(nm,_), e) =>
+  | IVar s => S.nbe_apps (MLvname s) args
+  | e1 `$ e2 => mk (args @ [mk [] e2]) e1
+  | (nm, _) `|-> e =>
       S.nbe_apps (mk_nbeFUN(nm, mk [] e)) args
+  | IAbs (_, e) => mk args e
+  | ICase (_, e) => mk args e
   | _ => sys_error "NBE mkexpr"
   in mk [] end;
 
 val mk_lexpr =
   let fun mk args t = case t of
-    CodegenThingol.IConst((s,_),_) =>
+    IConst((s,_),_) =>
       S.app Eval_Constr (S.tup [S.quote s, S.list args])
-  | CodegenThingol.IVarE(s,_) => if args = [] then MLvname s else 
+  | IVar s => if args = [] then MLvname s else 
       sys_error "NBE mk_lexpr illegal higher order pattern"
-  | CodegenThingol.IApp(e1,e2) => mk (args @ [mk [] e2]) e1
+  | e1 `$ e2 => mk (args @ [mk [] e2]) e1
+  | IAbs (_, e) => mk args e
+  | ICase (_, e) => mk args e
   | _ => sys_error "NBE mk_lexpr illegal pattern"
   in mk [] end;
 
 fun mk_eqn defined nm ar (lhs,e) =
   ([S.list(map mk_lexpr (rev lhs))], mk_rexpr defined nm ar e);
 
-fun funs_of_expr(CodegenThingol.IConst((s,_),_),fs) = s::fs
-  | funs_of_expr(CodegenThingol.IApp(e1,e2),fs) =
-      funs_of_expr(e1, funs_of_expr(e2, fs))
-  | funs_of_expr(CodegenThingol.IAbs(_, e),fs) = funs_of_expr(e,fs)
-  | funs_of_expr(_,fs) = fs;
+fun funs_of_expr (IConst ((s, _), _)) = insert (op =) s
+  | funs_of_expr (e1 `$ e2) =
+      funs_of_expr e1 #> funs_of_expr e2
+  | funs_of_expr (_ `|-> e) = funs_of_expr e
+  | funs_of_expr (IAbs (_, e)) = funs_of_expr e
+  | funs_of_expr (ICase (_, e)) = funs_of_expr e
+  | funs_of_expr _ = I;
 
 fun lookup nm = S.Val (MLname nm) (tab_lookup (S.quote nm));
 
-fun generate defined (nm,CodegenThingol.Fun(eqns,_)) =
+fun generate defined (nm, CodegenThingol.Fun (eqns, _)) =
   let
     val ar = length(fst(hd eqns));
     val params = S.list (rev (MLparams ar));
-    val funs = Library.flat(map (fn (_,e) => funs_of_expr(e,[])) eqns) \ nm;
+    val funs = Library.flat(map (fn (_,e) => funs_of_expr e []) eqns) \ nm;
     val globals = map lookup (filter defined funs);
     val default_eqn = ([params], S.app Eval_Constr (S.tup[S.quote nm,params]));
     val code = S.eqns (MLname nm)
diff -r fd8f152cfc76 -r f237c0cb3882 src/Pure/Tools/nbe_eval.ML
--- a/src/Pure/Tools/nbe_eval.ML	Wed Mar 01 10:37:00 2006 +0100
+++ b/src/Pure/Tools/nbe_eval.ML	Wed Mar 01 13:47:42 2006 +0100
@@ -127,21 +127,24 @@
 
 (* greetings to Tarski *)
 
-structure IL = CodegenThingol
+open BasicCodegenThingol;
 
-fun eval(IL.IConst((f,_),_)) xs = lookup f
-  | eval(IL.IVarE(n,_)) xs =
-      (case AList.lookup (op =) xs n of NONE => Var(n,[])
-       | SOME v => v)
-  | eval(IL.IApp(s,t)) xs = apply (eval s xs) (eval t xs)
-  | eval(IL.IAbs(IL.IVarE(n,_), t)) xs =
-      Fun (fn [x] => eval t ((n,x)::xs), [], 1,
-           fn () => let val var = new_name() in
-                 AbsN(var, to_term (eval t ((n,BVar(var,[])) :: xs))) end);
+fun eval xs (IConst ((f, _), _)) = lookup f
+  | eval xs (IVar n) =
+      AList.lookup (op =) xs n
+      |> the_default (Var (n, []))
+  | eval xs (s `$ t) = apply (eval xs s) (eval xs t)
+  | eval xs ((n, _) `|-> t) =
+      Fun (fn [x] => eval (AList.update (op =) (n, x) xs) t,
+             [], 1,
+             fn () => let val var = new_name() in
+                 AbsN (var, to_term (eval (AList.update (op =) (n, BVar (var, [])) xs) t)) end)
+  | eval xs (IAbs (_, t)) = eval xs t
+  | eval xs (ICase (_, t)) = eval xs t;
 
 
 (* finally... *)
 
-fun nbe tab t = (counter :=0; xfun_tab := tab; to_term(eval t []));
+fun nbe tab t = (counter :=0; xfun_tab := tab; to_term(eval [] t));
 
 end;