# HG changeset patch
# User nipkow
# Date 1181891406 -7200
# Node ID 2cc3352f6c3c89442eeaa83d5427b898a653e047
# Parent  6d72ababc58fe76179633a061c07c7863b84d624
Removed thunk from Fun

diff -r 6d72ababc58f -r 2cc3352f6c3c src/Pure/Tools/nbe_codegen.ML
--- a/src/Pure/Tools/nbe_codegen.ML	Fri Jun 15 09:09:06 2007 +0200
+++ b/src/Pure/Tools/nbe_codegen.ML	Fri Jun 15 09:10:06 2007 +0200
@@ -74,11 +74,11 @@
 val tab_update = S.app "NBE.update";
 
 fun mk_nbeFUN(nm,e) =
-  S.app Eval_Fun (S.tup [S.abs(S.list [MLvname nm])e,S.list [],"1",
+  S.app Eval_Fun (S.tup [S.abs(S.list [MLvname nm])e,S.list [],"1" (*,
       S.abs(S.tup [])(S.Let 
         [S.Val (MLintern "var") (S.app Eval_new_name (S.tup [])),
          S.Val (MLvname nm) (S.app Eval_BVar (S.tup [(MLintern "var"), S.list []]))]
-	(S.app Eval_AbsN(S.tup[MLintern "var",(S.app Eval_to_term e)])))]);
+	(S.app Eval_AbsN(S.tup[MLintern "var",(S.app Eval_to_term e)])))*)]);
 
 fun take_last n xs = rev (Library.take(n, rev xs));
 fun drop_last n xs = rev (Library.drop(n, rev xs));
@@ -87,10 +87,9 @@
 	if (ar <= length args) then 
 	  S.nbe_apps (S.app (MLname nm) (S.list (take_last ar args)))
 	             (drop_last ar args)
-        else S.app Eval_Fun (S.tup [MLname nm,S.list args,
+        else S.app Eval_Fun (S.tup [MLname nm,S.list args(*,
 	           string_of_int(ar - (length args)),
-		   S.abs (S.tup []) (S.app Eval_C
-	(S.quote nm))]);
+		   S.abs (S.tup []) (S.app Eval_C (S.quote nm))*)]);
 
 fun mk_rexpr defined names ar =
   let
diff -r 6d72ababc58f -r 2cc3352f6c3c src/Pure/Tools/nbe_eval.ML
--- a/src/Pure/Tools/nbe_eval.ML	Fri Jun 15 09:09:06 2007 +0200
+++ b/src/Pure/Tools/nbe_eval.ML	Fri Jun 15 09:10:06 2007 +0200
@@ -23,7 +23,7 @@
       Constr of string*(Univ list)       (*named constructors*)
     | Var of string*(Univ list)          (*free variables*)
     | BVar of int*(Univ list)            (*bound named variables*)
-    | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm)
+    | Fun of (Univ list -> Univ) * (Univ list) * int
                                          (*functions*);
 
   val eval: theory -> Univ Symtab.table -> term -> nterm
@@ -87,12 +87,7 @@
     Constr of string*(Univ list)       (* Named Constructors *)
   | Var of string*(Univ list)          (* Free variables *)
   | BVar of int*(Univ list)         (* Bound named variables *)
-  | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
-
-fun to_term (Constr(name, args))    = apps (C name) (map to_term args)
-  | to_term (Var   (name, args))    = apps (V name) (map to_term args)
-  | to_term (BVar  (name, args))    = apps (B name) (map to_term args)
-  | to_term (Fun(_,args,_,name_thunk)) = apps (name_thunk ()) (map to_term args);
+  | Fun of (Univ list -> Univ) * (Univ list) * int;
 
 (*
    A typical operation, why functions might be good for, is
@@ -100,14 +95,14 @@
    reasonably we applied in a semantical way.
 *)
 
-fun apply (Fun(f,xs,1,name))  x = f (x::xs)
-  | apply (Fun(f,xs,n,name))  x = Fun(f,x::xs,n-1,name)
+fun apply (Fun(f,xs,1))  x = f (x::xs)
+  | apply (Fun(f,xs,n))  x = Fun(f,x::xs,n-1)
   | apply (Constr(name,args)) x = Constr(name,x::args)
   | apply (Var(name,args))    x = Var(name,x::args)
   | apply (BVar(name,args))   x = BVar(name,x::args);
 
 fun mk_Fun(name,v,0) = (name,v [])
-  | mk_Fun(name,v,n) = (name,Fun(v,[],n, fn () => C name));
+  | mk_Fun(name,v,n) = (name,Fun(v,[],n));
 
 
 (* ------------------ evaluation with greetings to Tarski ------------------ *)
@@ -117,8 +112,7 @@
   | prep_term thy (Free v_ty) = Free v_ty
   | prep_term thy (s $ t) = prep_term thy s $ prep_term thy t
   | prep_term thy (Abs (raw_v, ty, raw_t)) =
-      let
-        val (v, t) = Syntax.variant_abs (raw_v, ty, raw_t);
+      let val (v,t) = Syntax.variant_abs (raw_v, ty, raw_t);
       in Abs (v, ty, prep_term thy t) end;
 
 
@@ -127,6 +121,13 @@
 val counter = ref 0;
 fun new_name () = (counter := !counter +1; !counter);
 
+fun to_term (Constr(name, args))    = apps (C name) (map to_term args)
+  | to_term (Var   (name, args))    = apps (V name) (map to_term args)
+  | to_term (BVar  (name, args))    = apps (B name) (map to_term args)
+  | to_term (F as Fun _) =
+      let val var = new_name()
+      in AbsN(var, to_term (apply F (BVar(var,[])))) end;
+
 
 (* greetings to Tarski *)
 
@@ -139,9 +140,7 @@
       | 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,
-            fn () => let val var = new_name() in
-              AbsN (var, to_term (evl (AList.update (op =) (v, BVar (var, [])) vars) t)) end)
+          Fun (fn [x] => evl (AList.update (op =) (v, x) vars) t, [], 1)
   in (counter := 0; to_term (evl [] (prep_term thy t))) end;
 
 end;