cleaned up some mess

--- a/src/Pure/Tools/nbe.ML	Wed Oct 04 14:17:46 2006 +0200
+++ b/src/Pure/Tools/nbe.ML	Wed Oct 04 14:17:47 2006 +0200
@@ -1,12 +1,13 @@
-(*  ID:         $Id$
+(*  Title:      Pure/nbe.ML
+    ID:         $Id$
     Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
 
 Toplevel theory interface for "normalization by evaluation"
-Preconditions: no Vars
 *)
 
 signature NBE =
 sig
+  (*preconditions: no Vars/TVars in term*)
   val norm_term: theory -> term -> term
   val normalization_conv: cterm -> thm
   val lookup: string -> NBE_Eval.Univ
@@ -89,7 +90,7 @@
       (fn c => (CodegenNames.const thy c, CodegenFuncgr.get_funcs funcgr c)) all_consts;
     val _ = tracing (fn () => "new definitions: " ^ (commas o maps (map fst)) funs);
     val _ = generate thy funs;
-    val nt = NBE_Eval.nbe thy (!tab) t';
+    val nt = NBE_Eval.eval thy (!tab) t';
   in nt end;
 
 fun subst_Frees [] = I

--- a/src/Pure/Tools/nbe_codegen.ML	Wed Oct 04 14:17:46 2006 +0200
+++ b/src/Pure/Tools/nbe_codegen.ML	Wed Oct 04 14:17:47 2006 +0200
@@ -1,4 +1,5 @@
-(*  ID:         $Id$
+(*  Title:      Pure/nbe_codegen.ML
+    ID:         $Id$
     Author:     Klaus Aehlig, LMU Muenchen; Tobias Nipkow, TU Muenchen
 
 Code generator for "normalization by evaluation".
@@ -145,21 +146,25 @@
 
 open NBE_Eval;
 
-val tcount = ref 0;
-
-fun varifyT ty =
-  let val ty' = map_type_tvar (fn ((s,i),S) => TypeInfer.param (!tcount + i) (s,S)) ty;
-      val _ = (tcount := !tcount + maxidx_of_typ ty + 1);
-  in tcount := !tcount+1; ty' end;
-
 fun nterm_to_term thy t =
   let
-   fun to_term bounds (C s) = Const ((apsnd varifyT o CodegenPackage.const_of_idf thy) s)
-     | to_term bounds (V s) = Free (s, dummyT)
-     | to_term bounds (B i) = Bound (find_index (fn j => i = j) bounds)
-     | to_term bounds (A (t1, t2)) = to_term bounds t1 $ to_term bounds t2
-     | to_term bounds (AbsN (i, t)) =
-          Abs("u", dummyT, to_term (i::bounds) t);
-  in tcount := 0; to_term [] t end;
+    fun to_term bounds (C s) tcount =
+          let
+            val (c, ty) = CodegenPackage.const_of_idf thy s;
+            val ty' = map_type_tvar (fn ((s,i),S) => TypeInfer.param (tcount + i) (s,S)) ty;
+            val tcount' = tcount + maxidx_of_typ ty + 1;
+          in (Const (c, ty'), tcount') end
+      | to_term bounds (V s) tcount = (Free (s, dummyT), tcount)
+      | to_term bounds (B i) tcount = (Bound (find_index (fn j => i = j) bounds), tcount)
+      | to_term bounds (A (t1, t2)) tcount =
+          tcount
+          |> to_term bounds t1
+          ||>> to_term bounds t2
+          |-> (fn (t1', t2') => pair (t1' $ t2'))
+      | to_term bounds (AbsN (i, t)) tcount =
+          tcount
+          |> to_term (i :: bounds) t
+          |-> (fn t' => pair (Abs ("u", dummyT, t')));
+  in fst (to_term [] t 0) end;
 
 end;

--- a/src/Pure/Tools/nbe_eval.ML	Wed Oct 04 14:17:46 2006 +0200
+++ b/src/Pure/Tools/nbe_eval.ML	Wed Oct 04 14:17:47 2006 +0200
@@ -1,4 +1,5 @@
-(*  ID:         $Id$
+(*  Title:      Pure/nbe_eval.ML
+    ID:         $Id$
     Author:     Klaus Aehlig, LMU Muenchen; Tobias Nipkow, TU Muenchen
 
 Evaluator infrastructure for "normalization by evaluation".
@@ -25,7 +26,7 @@
     | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm)
                                          (*functions*);
 
-  val nbe: theory -> Univ Symtab.table -> term -> nterm
+  val eval: theory -> Univ Symtab.table -> term -> nterm
   val apply: Univ -> Univ -> Univ
   val prep_term: theory -> term -> term
 
@@ -123,33 +124,23 @@
 (* generation of fresh names *)
 
 val counter = ref 0;
+fun new_name () = (counter := !counter +1; !counter);
 
-fun new_name () = (counter := !counter +1; !counter);
 
 (* greetings to Tarski *)
 
-fun eval lookup =
+fun eval thy tab t =
   let
-    fun evl vars (Const (s, _)) = lookup s
-      | evl vars (Free (v, _)) = 
-          AList.lookup (op =) vars v
-          |> the_default (Var (v, []))
-      | evl vars (s $ t) = apply (evl vars s) (evl vars t)
+    fun evl vars (Const (s, _)) =
+          the_default (Constr (s, [])) (Symtab.lookup tab s)
+      | evl vars (Free (v, _)) =
+          the_default (Var (v, [])) (AList.lookup (op =) vars v)
+      | evl vars (s $ t) =
+          apply (evl vars s) (evl vars t)
       | evl vars (Abs (v, _, t)) =
-          Fun (fn [x] => evl (AList.update (op =) (v, x) vars) t,
-            [], 1,
+          Fun (fn [x] => evl (AList.update (op =) (v, x) vars) t, [], 1,
             fn () => let val var = new_name() in
               AbsN (var, to_term (evl (AList.update (op =) (v, BVar (var, [])) vars) t)) end)
-  in evl end;
-
-
-(* finally... *)
-
-fun nbe thy tab t =
-  let
-    fun lookup s = case Symtab.lookup tab s
-       of SOME x => x
-        | NONE   => Constr (s, []);
-  in (counter := 0; to_term (eval lookup [] (prep_term thy t))) end;
+  in (counter := 0; to_term (evl [] (prep_term thy t))) end;
 
 end;