# HG changeset patch
# User wenzelm
# Date 974483369 -3600
# Node ID f1576723371f699f4ba2ed757583b5ffb516d77b
# Parent  1f7c944443fc372e6d12bfcb64035e217bb13fa7
added beta_norm;
tuned;

diff -r 1f7c944443fc -r f1576723371f src/Pure/envir.ML
--- a/src/Pure/envir.ML	Fri Nov 17 18:49:09 2000 +0100
+++ b/src/Pure/envir.ML	Fri Nov 17 18:49:29 2000 +0100
@@ -2,27 +2,26 @@
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1988  University of Cambridge
+
+Environments.  They don't take account that typ is part of variable
+name.  Therefore we check elsewhere that two variables with same names
+and different types cannot occur.
 *)
 
-(*Environments.  They don't take account that typ is part of variable name.
-                 Therefore we check elsewhere that  two variables with same
-		 names and different types cannot occur.
-*)
-
-
 signature ENVIR =
 sig
   datatype env = Envir of {asol: term Vartab.table, iTs: typ Vartab.table, maxidx: int}
-  val alist_of		: env -> (indexname * term) list
-  val empty		: int->env
-  val is_empty		: env -> bool
-  val above		: int * env -> bool
-  val genvar		: string -> env * typ -> env * term
-  val genvars		: string -> env * typ list -> env * term list
-  val lookup		: env * indexname -> term option
-  val norm_term		: env -> term -> term
-  val update		: (indexname * term) * env -> env
-  val vupdate		: (indexname * term) * env -> env
+  val genvars: string -> env * typ list -> env * term list
+  val genvar: string -> env * typ -> env * term
+  val lookup: env * indexname -> term option
+  val update: (indexname * term) * env -> env
+  val empty: int -> env
+  val is_empty: env -> bool
+  val above: int * env -> bool
+  val vupdate: (indexname * term) * env -> env
+  val alist_of: env -> (indexname * term) list
+  val norm_term: env -> term -> term
+  val beta_norm: term -> term
 end;
 
 structure Envir : ENVIR =
@@ -96,51 +95,51 @@
 
 fun norm_term1 (asol,t) : term =
   let fun norm (Var (w,T)) =
-	    (case Vartab.lookup (asol, w) of
-		Some u => (norm u handle SAME => u)
-	      | None   => raise SAME)
-	| norm (Abs(a,T,body)) =  Abs(a, T, norm body)
-	| norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
-	| norm (f $ t) =
-	    ((case norm f of
-	       Abs(_,_,body) => normh(subst_bound (t, body))
-	     | nf => nf $ (norm t handle SAME => t))
-	    handle SAME => f $ norm t)
-	| norm _ =  raise SAME
+            (case Vartab.lookup (asol, w) of
+                Some u => (norm u handle SAME => u)
+              | None   => raise SAME)
+        | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
+        | norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body))
+        | norm (f $ t) =
+            ((case norm f of
+               Abs(_,_,body) => normh(subst_bound (t, body))
+             | nf => nf $ (norm t handle SAME => t))
+            handle SAME => f $ norm t)
+        | norm _ =  raise SAME
       and normh t = norm t handle SAME => t
   in normh t end
 
 and norm_term2(asol,iTs,t) : term =
   let fun normT(Type(a,Ts)) = Type(a, normTs Ts)
-	| normT(TFree _) = raise SAME
-	| normT(TVar(v,_)) = (case Vartab.lookup (iTs, v) of
-		Some(U) => normTh U
-	      | None => raise SAME)
+        | normT(TFree _) = raise SAME
+        | normT(TVar(v,_)) = (case Vartab.lookup (iTs, v) of
+                Some(U) => normTh U
+              | None => raise SAME)
       and normTh T = ((normT T) handle SAME => T)
       and normTs([]) = raise SAME
-	| normTs(T::Ts) = ((normT T :: (normTs Ts handle SAME => Ts))
-			   handle SAME => T :: normTs Ts)
+        | normTs(T::Ts) = ((normT T :: (normTs Ts handle SAME => Ts))
+                           handle SAME => T :: normTs Ts)
       and norm(Const(a,T)) = Const(a, normT T)
-	| norm(Free(a,T)) = Free(a, normT T)
-	| norm(Var (w,T)) =
-	    (case Vartab.lookup (asol, w) of
-		Some u => normh u
-	      | None   => Var(w,normT T))
-	| norm(Abs(a,T,body)) =
-	      (Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body))
-	| norm(Abs(_,_,body) $ t) = normh(subst_bound (t, body))
-	| norm(f $ t) =
-	    ((case norm f of
-	       Abs(_,_,body) => normh(subst_bound (t, body))
-	     | nf => nf $ normh t)
-	    handle SAME => f $ norm t)
-	| norm _ =  raise SAME
+        | norm(Free(a,T)) = Free(a, normT T)
+        | norm(Var (w,T)) =
+            (case Vartab.lookup (asol, w) of
+                Some u => normh u
+              | None   => Var(w,normT T))
+        | norm(Abs(a,T,body)) =
+              (Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body))
+        | norm(Abs(_,_,body) $ t) = normh(subst_bound (t, body))
+        | norm(f $ t) =
+            ((case norm f of
+               Abs(_,_,body) => normh(subst_bound (t, body))
+             | nf => nf $ normh t)
+            handle SAME => f $ norm t)
+        | norm _ =  raise SAME
       and normh t = (norm t) handle SAME => t
   in normh t end;
 
-(*curried version might be slower in recursive calls*)
 fun norm_term (env as Envir{asol,iTs,...}) t : term =
-        if Vartab.is_empty iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t)
+  if Vartab.is_empty iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t)
+
+val beta_norm = norm_term (empty 0);
 
 end;
-