# HG changeset patch
# User haftmann
# Date 1141736988 -3600
# Node ID 0b9eb4b0ad98a65267396ef74fd327a0e6a65f08
# Parent  294448903a66ed9d8412b141ab388a82cc446511
substantial improvement in codegen iml

diff -r 294448903a66 -r 0b9eb4b0ad98 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Tue Mar 07 04:06:02 2006 +0100
+++ b/src/HOL/Datatype.thy	Tue Mar 07 14:09:48 2006 +0100
@@ -246,6 +246,9 @@
   fst_conv [code]
   snd_conv [code]
 
+lemma [code unfold]:
+  "1 == Suc 0" by simp
+
 code_generate True False Not "op &" "op |" If
 
 code_syntax_tyco bool
@@ -311,9 +314,4 @@
     ml (target_atom "SOME")
     haskell (target_atom "Just")
 
-code_syntax_const
-  "1 :: nat"
-    ml ("{*Suc 0*}")
-    haskell ("{*Suc 0*}")
-
 end
diff -r 294448903a66 -r 0b9eb4b0ad98 src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Tue Mar 07 04:06:02 2006 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Tue Mar 07 14:09:48 2006 +0100
@@ -9,7 +9,6 @@
 sig
   val add: string option -> attribute
   val del: attribute
-  val get_rec_equations: theory -> string * typ -> (term list * term) list * typ
   val get_thm_equations: theory -> string * typ -> (thm list * typ) option
   val setup: theory -> theory
 end;
@@ -81,19 +80,6 @@
              | SOME thyname => thyname)
        end);
 
-fun get_rec_equations thy (s, T) =
-  Symtab.lookup (CodegenData.get thy) s
-  |> Option.map (fn thms => 
-       List.filter (fn (thm, _) => is_instance thy T ((snd o const_of o prop_of) thm)) thms
-       |> del_redundant thy [])
-  |> Option.mapPartial (fn thms => if null thms then NONE else SOME thms)
-  |> Option.map (fn thms =>
-       (preprocess thy (map fst thms),
-          (snd o const_of o prop_of o fst o hd) thms))
-  |> the_default ([], dummyT)
-  |> apfst (map prop_of)
-  |> apfst (map (Codegen.rename_term #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> apfst (strip_comb #> snd)))
-
 fun get_thm_equations thy (c, ty) =
   Symtab.lookup (CodegenData.get thy) c
   |> Option.map (fn thms => 
diff -r 294448903a66 -r 0b9eb4b0ad98 src/HOL/ex/nbe.thy
--- a/src/HOL/ex/nbe.thy	Tue Mar 07 04:06:02 2006 +0100
+++ b/src/HOL/ex/nbe.thy	Tue Mar 07 14:09:48 2006 +0100
@@ -6,15 +6,16 @@
 theory nbe
 imports Main
 begin
+
 ML"reset quick_and_dirty"
 
 declare disj_assoc[code]
 
 norm_by_eval "(P | Q) | R"
 
-lemma[code]: "(P \<longrightarrow> P)=True" by blast
+(*lemma[code]: "(P \<longrightarrow> P) = True" by blast
 norm_by_eval "P \<longrightarrow> P"
-norm_by_eval "True \<longrightarrow> P"
+norm_by_eval "True \<longrightarrow> P"*)
 
 
 datatype n = Z | S n
@@ -52,7 +53,6 @@
 "exp m Z = S Z"
 "exp m (S n) = mul (exp m n) m"
 
-
 norm_by_eval "mul2 (S(S(S(S(S(S(S Z))))))) (S(S(S(S(S Z)))))"
 norm_by_eval "mul (S(S(S(S(S(S(S Z))))))) (S(S(S(S(S Z)))))"
 norm_by_eval "exp (S(S(S(S(S(S(S Z))))))) (S(S(S(S(S Z)))))"
@@ -94,16 +94,21 @@
 norm_by_eval "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]"
 norm_by_eval "rev [a, b, c]"
 
-end
-
-(*
-ML"set Toplevel.debug"
 norm_by_eval "case n of None \<Rightarrow> True | Some((x,y),(u,v)) \<Rightarrow> False"
 norm_by_eval "let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)"
 norm_by_eval "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z))"
-*)
-(* to be done
-norm_by_eval "max 0 (0::nat)"
 norm_by_eval "last[a,b,c]"
- Numerals! *)
+
+text {*
+  won't work since it relies on 
+  polymorphically used ad-hoc overloaded function:
+  norm_by_eval "max 0 (0::nat)"
+*}
 
+text {*
+  Numerals still take their time\<dots>
+*}
+
+end
+
+
diff -r 294448903a66 -r 0b9eb4b0ad98 src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Tue Mar 07 04:06:02 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Tue Mar 07 14:09:48 2006 +0100
@@ -138,7 +138,7 @@
   andalso Sign.typ_instance thy (ty2, ty1);
 
 fun is_overloaded thy c = case Defs.specifications_of (Theory.defs_of thy) c
- of [] => false
+ of [] => true
   | [(ty, _)] => not (eq_typ thy (ty, Sign.the_const_type thy c))
   | _ => true;
 
@@ -161,10 +161,17 @@
   fun mk thy ((c, ty), i) =
     let
       val c' = idf_of_name thy nsp_overl c;
-      val prefix = case (AList.lookup (eq_typ thy)
-          (Defs.specifications_of (Theory.defs_of thy) c)) ty
-       of SOME thyname => NameSpace.append thyname nsp_overl
-        | NONE => NameSpace.drop_base c';
+      val prefix = 
+        case (AList.lookup (eq_typ thy)
+            (Defs.specifications_of (Theory.defs_of thy) c)) ty
+         of SOME thyname => NameSpace.append thyname nsp_overl
+          | NONE => if c = "op ="
+              then
+                NameSpace.append
+                  (((fn s => Codegen.thyname_of_type s thy) o fst o dest_Type o hd o fst o strip_type) ty)
+                  nsp_overl
+              else
+                NameSpace.drop_base c';
       val c'' = NameSpace.append prefix (NameSpace.base c');
       fun mangle (Type (tyco, tys)) =
             (NameSpace.base o alias_get thy) tyco :: Library.flat (List.mapPartial mangle tys) |> SOME
@@ -399,13 +406,13 @@
       (c, ty) =
   let
     fun get_overloaded (c, ty) =
-      case Symtab.lookup overltab1 c
+      (case Symtab.lookup overltab1 c
        of SOME tys =>
             (case find_first (curry (Sign.typ_instance thy) ty) tys
              of SOME ty' => ConstNameMangler.get thy overltab2
                   (c, ty') |> SOME
               | _ => NONE)
-        | _ => NONE
+        | _ => NONE)
     fun get_datatypecons (c, ty) =
       case (snd o strip_type) ty
        of Type (tyco, _) =>
@@ -851,12 +858,12 @@
 and appgen_default thy tabs ((c, ty), ts) trns =
   trns
   |> ensure_def_const thy tabs (c, ty)
+  ||>> exprsgen_type thy tabs [ty]
   ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
          (ClassPackage.extract_classlookup thy (c, ty))
-  ||>> exprsgen_type thy tabs [ty]
   ||>> fold_map (exprgen_term thy tabs) ts
-  |-> (fn (((c, ls), [ty]), es) =>
-         pair (IConst ((c, ty), ls) `$$ es))
+  |-> (fn (((c, [ty]), ls), es) =>
+         pair (IConst (c, (ls, ty)) `$$ es))
 and appgen thy tabs ((f, ty), ts) trns =
   case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f
    of SOME ((imin, imax), (ag, _)) =>
@@ -899,43 +906,48 @@
 
 (* parametrized generators, for instantiation in HOL *)
 
-fun appgen_let strip_abs thy tabs (app as ((c, ty), [dt, ct])) trns =
-  let
-    val ([st], bt) = strip_abs 1 ct;
-    val dtyp = (hd o fst o strip_type) ty
-  in
-    trns
-    |> 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 (app as (c as (_, ty), [t])) trns =
+fun appgen_split strip_abs thy tabs (app as (c, [t])) trns =
   case strip_abs 1 (Const c $ t)
-   of ([vt], tb) =>
+   of ([vt], bt) =>
         trns
         |> exprgen_term thy tabs vt
-        ||>> exprgen_type thy tabs (((fn [_, ty] => ty) o fst o strip_type) ty)
-        ||>> exprgen_term thy tabs tb
+        ||>> exprgen_type thy tabs (type_of vt)
+        ||>> exprgen_term thy tabs bt
         ||>> appgen_default thy tabs app
         |-> (fn (((ve, vty), be), e0) => pair (IAbs (((ve, vty), be), e0)))
     | _ =>
         trns
         |> appgen_default thy tabs app;
 
+fun appgen_let strip_abs thy tabs (app as ((c, ty), [dt, ct])) trns =
+  case strip_abs 1 ct
+   of ([st], bt) =>
+        trns
+        |> exprgen_term thy tabs dt
+        ||>> exprgen_type thy tabs (type_of dt)
+        ||>> 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)))
+    | _ =>
+        trns
+        |> 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 =
-    if tyco = tyco_int then
+    if tyco = tyco_nat then
       trns
-      |> exprgen_type thy tabs ty
-      |-> (fn ty => pair (CodegenThingol.IConst (((IntInf.toString o bin_to_int thy) bin, ty), [])))
-    else if tyco = tyco_nat then
-      trns
-      |> exprgen_term thy tabs (mk_int_to_nat bin)
-    else error ("invalid type constructor for numeral: " ^ quote tyco);
+      |> exprgen_term thy tabs (mk_int_to_nat bin) (*should be a preprocessor's work*)
+    else
+      let
+        val i = bin_to_int thy bin;
+        val _ = if i < 0 then error ("negative numeral: " ^ IntInf.toString i) else ();
+          (*should be a preprocessor's work*)
+      in
+        trns
+        |> exprgen_type thy tabs ty
+        |-> (fn ty => pair (CodegenThingol.INum ((i, ty), ())))
+      end;
 
 fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns =
   let
@@ -951,25 +963,7 @@
     ||>> exprsgen_type thy tabs [ty_def]
     ||>> exprgen_term thy tabs tf
     ||>> exprgen_term thy tabs tx
-    |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst ((idf, ty), ls) `$ tf `$ tx))
-  end;
-
-
-fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns =
-  let
-    val ty_def = (op ---> o apfst tl o strip_type o Sign.the_const_type thy) c;
-    val ty' = (op ---> o apfst tl o strip_type) ty;
-    val idf = idf_of_const thy tabs (c, ty);
-  in
-    trns
-    |> ensure_def [("wfrec", (K o succeed) Undef)] ("generating wfrec") idf
-    |> exprgen_type thy tabs ty'
-    ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
-           (ClassPackage.extract_classlookup thy (c, ty))
-    ||>> exprsgen_type thy tabs [ty_def]
-    ||>> exprgen_term thy tabs tf
-    ||>> exprgen_term thy tabs tx
-    |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst ((idf, ty), ls) `$ tf `$ tx))
+    |-> (fn ((((_, ls), [ty]), tf), tx) => pair (IConst (idf, (ls, ty)) `$ tf `$ tx))
   end;
 
 fun eqextr_eq f fals thy tabs ("op =", ty) =
diff -r 294448903a66 -r 0b9eb4b0ad98 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Tue Mar 07 04:06:02 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Tue Mar 07 14:09:48 2006 +0100
@@ -314,6 +314,19 @@
     |> postprocess_module name
   end;
 
+fun constructive_fun (name, (eqs, ty)) =
+  let
+    fun check_eq (eq as (lhs, rhs)) =
+      if forall CodegenThingol.is_pat lhs
+      then SOME eq
+      else (warning ("in function " ^ quote name ^ ", throwing away one "
+        ^ "non-executable function clause"); NONE)
+  in case List.mapPartial check_eq eqs
+   of [] => error ("in function " ^ quote name ^ ", no"
+        ^ "executable function clauses found")
+    | eqs => (name, (eqs, ty))
+  end;
+
 fun parse_single_file serializer =
   OuterParse.path
   >> (fn path => serializer
@@ -336,7 +349,7 @@
 
 fun pretty_list thingol_nil thingol_cons (target_pred, target_cons) =
   let
-    fun dest_cons (IConst ((c, _), _) `$ e1 `$ e2) =
+    fun dest_cons (IConst (c, _) `$ e1 `$ e2) =
           if c = thingol_cons
           then SOME (e1, e2)
           else NONE
@@ -349,7 +362,7 @@
       ];
     fun pretty_compact fxy pr [e1, e2] =
       case CodegenThingol.unfoldr dest_cons e2
-       of (es, IConst ((c, _), _)) =>
+       of (es, IConst (c, _)) =>
             if c = thingol_nil
             then Pretty.enum "," "[" "]" (map (pr NOBR) (e1::es))
             else pretty_default fxy pr e1 e2
@@ -445,17 +458,15 @@
           end
       | ml_from_type fxy (ITyVar v) =
           str ("'" ^ v);
-    fun typify trans ty p =
+    fun typify ty p =
       let
         fun needs_type_t (tyco `%% tys) =
             needs_type tyco
-            orelse trans
-              andalso exists needs_type_t tys
+            orelse 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);
+            needs_type_t ty1 orelse needs_type_t ty2;
       in if needs_type_t ty
         then
           Pretty.enclose "(" ")" [
@@ -480,14 +491,20 @@
       | ml_from_expr fxy ((v, ty) `|-> e) =
           brackify BR [
             str "fn",
-            typify true ty (str v),
+            typify ty (str v),
             str "=>",
             ml_from_expr NOBR e
           ]
+      | ml_from_expr fxy (INum ((n, ty), _)) =
+          Pretty.enclose "(" ")" [
+            (str o IntInf.toString) n,
+            str ":",
+            ml_from_type NOBR ty
+          ]
       | ml_from_expr fxy (IAbs (((ve, vty), be), _)) =
           brackify BR [
             str "fn",
-            typify true vty (ml_from_expr NOBR ve),
+            typify vty (ml_from_expr NOBR ve),
             str "=>",
             ml_from_expr NOBR be
           ]
@@ -497,7 +514,7 @@
             fun mk_val ((ve, vty), se) = Pretty.block [
                 (Pretty.block o Pretty.breaks) [
                   str "val",
-                  typify true vty (ml_from_expr NOBR ve),
+                  typify vty (ml_from_expr NOBR ve),
                   str "=",
                   ml_from_expr NOBR se
                 ],
@@ -519,7 +536,7 @@
               ]
           in brackify fxy (
             str "case"
-            :: typify true dty (ml_from_expr NOBR de)
+            :: typify dty (ml_from_expr NOBR de)
             :: mk_clause "of" bse
             :: map (mk_clause "|") bses
           ) end
@@ -530,11 +547,10 @@
         [(str o resolv) f, Pretty.enum "," "(" ")" (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) =
+    and ml_from_app fxy ((c, (lss, ty)), es) =
       case map (ml_from_sortlookup BR) lss
        of [] =>
             from_app ml_mk_app ml_from_expr const_syntax fxy ((c, ty), es)
-            |> typify false ty
         | lss =>
             brackify fxy (
               (str o resolv) c
@@ -581,7 +597,7 @@
               map (Pretty.block o single o Pretty.block o single);
             fun mk_arg e ty =
               ml_from_expr BR e
-              |> typify true ty
+              |> typify ty
             fun mk_eq definer (pats, expr) =
               (Pretty.block o Pretty.breaks) (
                 [str definer, (str o resolv) name]
@@ -601,8 +617,8 @@
           end;
       in
         chunk_defs (
-          mk_fun (the (fold check_args defs NONE)) def
-          :: map (mk_fun "and") defs_tl
+          (mk_fun (the (fold check_args defs NONE)) o constructive_fun) def
+          :: map (mk_fun "and" o constructive_fun) defs_tl
         )
       end;
     fun ml_from_datatypes (defs as (def::defs_tl)) =
@@ -912,6 +928,8 @@
               hs_from_expr NOBR e
             ])
           end
+      | hs_from_expr fxy (INum ((n, _), _)) =
+          (str o IntInf.toString) n
       | hs_from_expr fxy (e as IAbs _) =
           let
             val (es, e) = CodegenThingol.unfold_abs e
@@ -954,11 +972,11 @@
           ] end
     and hs_mk_app c es =
       (str o resolv) c :: map (hs_from_expr BR) es
-    and hs_from_app fxy (((c, ty), ls), es) =
+    and hs_from_app fxy ((c, (ty, ls)), es) =
       from_app hs_mk_app hs_from_expr const_syntax fxy ((c, ty), es);
-    fun hs_from_funeqs (name, eqs) =
+    fun hs_from_funeqs (def as (name, _)) =
       let
-        fun from_eq name (args, rhs) =
+        fun from_eq (args, rhs) =
           Pretty.block [
             (str o resolv_here) name,
             Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, hs_from_expr BR p]) args),
@@ -967,14 +985,14 @@
             Pretty.brk 1,
             hs_from_expr NOBR rhs
           ]
-      in Pretty.chunks (map (from_eq name) eqs) end;
+      in Pretty.chunks ((map from_eq o fst o snd o constructive_fun) def) end;
     fun hs_from_def (name, CodegenThingol.Undef) =
           error ("empty statement during serialization: " ^ quote name)
       | hs_from_def (name, CodegenThingol.Prim prim) =
           from_prim resolv_here (name, prim)
-      | hs_from_def (name, CodegenThingol.Fun (eqs, (sctxt, ty))) =
+      | hs_from_def (name, CodegenThingol.Fun (def as (_, (sctxt, ty)))) =
           let
-            val body = hs_from_funeqs (name, eqs);
+            val body = hs_from_funeqs (name, def);
           in if with_typs then
             Pretty.chunks [
               Pretty.block [
@@ -1042,7 +1060,7 @@
             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)
+            Pretty.chunks (map (fn (m, (_, (eqs, ty))) => hs_from_funeqs (m, (eqs, ty))) memdefs)
           ] |> SOME
   in
     case List.mapPartial (fn (name, def) => hs_from_def (name, def)) defs
diff -r 294448903a66 -r 0b9eb4b0ad98 src/Pure/Tools/codegen_thingol.ML
--- a/src/Pure/Tools/codegen_thingol.ML	Tue Mar 07 04:06:02 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Tue Mar 07 14:09:48 2006 +0100
@@ -24,10 +24,11 @@
     | `-> of itype * itype
     | ITyVar of vname;
   datatype iexpr =
-      IConst of (string * itype) * iclasslookup list list
+      IConst of string * (iclasslookup list list * itype)
     | IVar of vname
     | `$ of iexpr * iexpr
     | `|-> of (vname * itype) * iexpr
+    | INum of (IntInf.int (*positive!*) * itype) * unit
     | IAbs of ((iexpr * itype) * iexpr) * iexpr
         (* (((binding expression (ve), binding type (vty)),
                 body expression (be)), native expression (e0)) *)
@@ -52,8 +53,11 @@
   val unfold_abs: iexpr -> (iexpr * itype) list * iexpr;
   val unfold_let: iexpr -> ((iexpr * itype) * iexpr) list * iexpr;
   val unfold_const_app: iexpr ->
-    (((string * itype) * iclasslookup list list) * iexpr list) option;
-  val ensure_pat: iexpr -> iexpr;
+    ((string * (iclasslookup list list * itype)) * iexpr list) option;
+  val add_constnames: iexpr -> string list -> string list;
+  val add_varnames: iexpr -> string list -> string list;
+  val is_pat: iexpr -> bool;
+  val map_pure: (iexpr -> 'a) -> iexpr -> 'a;
 
   type funn = (iexpr list * iexpr) list * (sortcontext * itype);
   type datatyp = sortcontext * (string * itype list) list;
@@ -161,10 +165,11 @@
   | ITyVar of vname;
 
 datatype iexpr =
-    IConst of (string * itype) * iclasslookup list list
+    IConst of string * (iclasslookup list list * itype)
   | IVar of vname
   | `$ of iexpr * iexpr
   | `|-> of (vname * itype) * iexpr
+  | INum of (IntInf.int (*positive!*) * itype) * unit
   | IAbs of ((iexpr * itype) * iexpr) * iexpr
   | ICase of ((iexpr * itype) * (iexpr * iexpr) list) * iexpr;
     (*see also signature*)
@@ -208,7 +213,7 @@
   | pretty_itype (ITyVar v) =
       Pretty.str v;
 
-fun pretty_iexpr (IConst ((c, _), _)) =
+fun pretty_iexpr (IConst (c, _)) =
       Pretty.str c
   | pretty_iexpr (IVar v) =
       Pretty.str ("?" ^ v)
@@ -218,6 +223,8 @@
   | 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 (INum ((n, _), _)) =
+      (Pretty.str o IntInf.toString) n
   | pretty_iexpr (IAbs (((e1, _), e2), _)) =
       (Pretty.enclose "(" ")" o Pretty.breaks)
         [pretty_iexpr e1, Pretty.str "|->", pretty_iexpr e2]
@@ -271,6 +278,8 @@
       f e1 `$ f e2
   | map_iexpr f ((v, ty) `|-> e) =
       (v, ty) `|-> f e
+  | map_iexpr _ (e as INum _) =
+      e
   | map_iexpr f (IAbs (((ve, vty), be), e0)) =
       IAbs (((f ve, vty), f be), e0)
   | map_iexpr f (ICase (((de, dty), bses), e0)) =
@@ -278,8 +287,8 @@
 
 fun map_iexpr_itype f =
   let
-    fun mapp (IConst ((c, ty), sctxt)) = IConst ((c, f ty), sctxt)
-      | mapp ((v, ty) `|-> e) = (v, f ty) `|-> mapp e
+    fun mapp ((v, ty) `|-> e) = (v, f ty) `|-> mapp e
+      | mapp (INum ((n, ty), e)) = INum ((n, f ty), e)
       | mapp (IAbs (((ve, vty), be), e0)) =
           IAbs (((mapp ve, f vty), mapp be), e0)
       | mapp (ICase (((de, dty), bses), e0)) =
@@ -321,12 +330,27 @@
       | instant y = map_itype instant y;
   in map_itype instant end;
 
-fun ensure_pat (e as IConst (_, [])) = 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 is_pat (e as IConst (_, ([], _))) = true
+  | is_pat (e as IVar _) = true
+  | is_pat (e as (e1 `$ e2)) =
+      is_pat e1 andalso is_pat e2
+  | is_pat (e as INum _) = true
+  | is_pat e = false;
+
+fun map_pure f (e as IConst _) =
+      f e
+  | map_pure f (e as IVar _) =
+      f e
+  | map_pure f (e as _ `$ _) =
+      f e
+  | map_pure f (e as _ `|-> _) =
+      f e
+  | map_pure _ (INum _) =
+      error ("sorry, no pure representation of numerals so far")
+  | map_pure f (IAbs (_, e0)) =
+      f e0
+  | map_pure f (ICase (_, e0)) =
+      f e0;
 
 fun has_tyvars (_ `%% tys) =
       exists has_tyvars tys
@@ -335,18 +359,35 @@
   | has_tyvars (ty1 `-> ty2) =
       has_tyvars ty1 orelse has_tyvars ty2;
 
-fun varnames_of (IConst ((c, _), _)) =
+fun add_constnames (IConst (c, _)) =
+      insert (op =) c
+  | add_constnames (IVar _) =
       I
-  | varnames_of (IVar v) =
+  | add_constnames (e1 `$ e2) =
+      add_constnames e1 #> add_constnames e2
+  | add_constnames (_ `|-> e) =
+      add_constnames e
+  | add_constnames (INum _) =
+      I
+  | add_constnames (IAbs (_, e)) =
+      add_constnames e
+  | add_constnames (ICase (_, e)) =
+      add_constnames e;
+
+fun add_varnames (IConst _) =
+      I
+  | add_varnames (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;
+  | add_varnames (e1 `$ e2) =
+      add_varnames e1 #> add_varnames e2
+  | add_varnames ((v, _) `|-> e) =
+      insert (op =) v #> add_varnames e
+  | add_varnames (INum _) =
+      I
+  | add_varnames (IAbs (((ve, _), be), _)) =
+      add_varnames ve #> add_varnames be
+  | add_varnames (ICase (((de, _), bses), _)) =
+      add_varnames de #> fold (fn (be, se) => add_varnames be #> add_varnames se) bses;
 
 fun invent seed used =
   let
@@ -884,17 +925,17 @@
   let
     fun eta e =
      case unfold_const_app e
-      of SOME (((f, ty), ls), es) =>
+      of SOME (const as (c, (_, ty)), es) =>
           let
-            val delta = query f - length es;
+            val delta = query c - length es;
             val add_n = if delta < 0 then 0 else delta;
             val tys =
               (fst o unfold_fun) ty
               |> curry Library.drop (length es)
               |> curry Library.take add_n
-            val vs = (Term.invent_names (fold varnames_of es []) "x" add_n)
+            val vs = (Term.invent_names (fold add_varnames es []) "x" add_n)
           in
-            vs ~~ tys `|--> IConst ((f, ty), ls) `$$ map eta es `$$ map IVar vs
+            vs ~~ tys `|--> IConst const `$$ 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;
@@ -908,7 +949,7 @@
           else (case unfold_abs e
            of ([], e) =>
               let
-                val add_var = IVar (hd (Term.invent_names (varnames_of e []) "x" 1))
+                val add_var = IVar (hd (Term.invent_names (add_varnames e []) "x" 1))
               in (([([add_var], e `$ add_var)], cty)) end
             | _ =>  funn)
       | eta funn = funn;
@@ -919,7 +960,7 @@
     fun unclash (eqs, (sortctxt, ty)) =
       let
         val used_expr =
-          fold (fn (pats, rhs) => fold varnames_of pats #> varnames_of rhs) eqs [];
+          fold (fn (pats, rhs) => fold add_varnames pats #> add_varnames 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;
diff -r 294448903a66 -r 0b9eb4b0ad98 src/Pure/Tools/nbe_codegen.ML
--- a/src/Pure/Tools/nbe_codegen.ML	Tue Mar 07 04:06:02 2006 +0100
+++ b/src/Pure/Tools/nbe_codegen.ML	Tue Mar 07 14:09:48 2006 +0100
@@ -91,55 +91,43 @@
 open BasicCodegenThingol;
 
 fun mk_rexpr defined nm ar =
-  let fun mk args t = case t of
-    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 ])
-  | 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
+  let
+    fun mk args = CodegenThingol.map_pure (mk' args)
+    and mk' args (IConst (c, _)) =
+          if c = nm then selfcall nm ar args
+          else if defined c then S.nbe_apps (MLname c) args
+          else S.app Eval_Constr (S.tup [S.quote c, S.list args])
+      | mk' args (IVar s) = S.nbe_apps (MLvname s) args
+      | mk' args (e1 `$ e2) = mk (args @ [mk [] e2]) e1
+      | mk' args ((nm, _) `|-> e) = S.nbe_apps (mk_nbeFUN (nm, mk [] e)) args;
   in mk [] end;
 
 val mk_lexpr =
-  let fun mk args t = case t of
-    IConst((s,_),_) =>
-      S.app Eval_Constr (S.tup [S.quote s, S.list args])
-  | IVar s => if args = [] then MLvname s else 
-      sys_error "NBE mk_lexpr illegal higher order pattern"
-  | e1 `$ e2 => mk (args @ [mk [] e2]) e1
-  | IAbs (_, e) => mk args e
-  | ICase (_, e) => mk args e
-  | _ => sys_error "NBE mk_lexpr illegal pattern"
+  let
+    fun mk args = CodegenThingol.map_pure (mk' args)
+    and mk' args (IConst (c, _)) =
+          S.app Eval_Constr (S.tup [S.quote c, S.list args])
+      | mk' args (IVar s) = if args = [] then MLvname s else 
+          sys_error "NBE mk_lexpr illegal higher order pattern"
+      | mk' args (e1 `$ e2) = mk (args @ [mk [] e2]) e1
+      | mk' args (_ `|-> _) =
+          sys_error "NBE mk_lexpr illegal pattern";
   in mk [] end;
 
-fun vars (IVar s) = [s]
-  | vars (e1 `$ e2) = (vars e1) @ (vars e2)
-  | vars (IAbs(_,e)) = vars e
-  | vars (ICase(_,e)) = vars e
-  | vars _ = [] (* note that a lambda won't occur here anyway *)
-
 fun mk_eqn defined nm ar (lhs,e) =
-  if has_duplicates (op =) (Library.flat (map vars lhs)) then [] else
+  if has_duplicates (op =) (fold CodegenThingol.add_varnames lhs []) then [] else
   [([S.list(map mk_lexpr (rev lhs))], mk_rexpr defined nm ar e)];
 
-fun consts_of (IConst ((s, _), _)) = insert (op =) s
-  | consts_of (e1 `$ e2) =
-      consts_of e1 #> consts_of e2
-  | consts_of (_ `|-> e) = consts_of e
-  | consts_of (IAbs (_, e)) = consts_of e
-  | consts_of (ICase (_, e)) = consts_of e
-  | consts_of _ = I;
-
 fun lookup nm = S.Val (MLname nm) (tab_lookup (S.quote nm));
 
 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) => consts_of e []) eqns) \ nm;
+        val ar = (length o fst o hd) eqns;
+        val params = (S.list o rev o MLparams) ar;
+        val funs =
+          []
+          |> fold (fn (_, e) => CodegenThingol.add_constnames e) eqns
+          |> remove (op =) 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 294448903a66 -r 0b9eb4b0ad98 src/Pure/Tools/nbe_eval.ML
--- a/src/Pure/Tools/nbe_eval.ML	Tue Mar 07 04:06:02 2006 +0100
+++ b/src/Pure/Tools/nbe_eval.ML	Tue Mar 07 14:09:48 2006 +0100
@@ -121,18 +121,19 @@
 
 open BasicCodegenThingol;
 
-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,
+fun eval xs =
+  let
+    fun evl (IConst (c, _)) = lookup c
+      | evl (IVar n) =
+          AList.lookup (op =) xs n
+          |> the_default (Var (n, []))
+      | evl (s `$ t) = apply (eval xs s) (eval xs t)
+      | evl ((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;
+  in CodegenThingol.map_pure evl end;
 
 (* finally... *)