src/Pure/envir.ML
changeset 247 bc10568855ee
parent 0 a5a9c433f639
child 719 e3e1d1a6d408
--- a/src/Pure/envir.ML	Thu Jan 20 13:35:40 1994 +0100
+++ b/src/Pure/envir.ML	Mon Jan 24 12:03:53 1994 +0100
@@ -1,6 +1,6 @@
-(*  Title: 	envir
+(*  Title:      Pure/envir.ML
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1988  University of Cambridge
 *)
 
@@ -11,16 +11,18 @@
 *)
 
 
-signature ENVIR = 
+signature ENVIR =
 sig
   type 'a xolist
   exception ENVIR of string * indexname;
   datatype env = Envir of {asol: term xolist,
-			   iTs: (indexname * typ) list,
-			   maxidx: int}
+                           iTs: (indexname * typ) list,
+                           maxidx: int}
   val alist_of : env -> (indexname * term) list
   val alist_of_olist : 'a xolist -> (indexname * 'a) list
   val empty : int->env
+  val is_empty : env -> bool
+  val minidx : env -> int option
   val genvar  : string -> env * typ -> env * term
   val genvars : string -> env * typ list -> env * term list
   val lookup : env * indexname -> term option
@@ -31,7 +33,7 @@
   val vupdate : (indexname * term) * env -> env
 end;
 
-functor EnvirFun () : ENVIR = 
+functor EnvirFun () : ENVIR =
 struct
 
 
@@ -40,49 +42,49 @@
 
 
 exception ENVIR of string * indexname;
- 
-(*look up key in ordered list*)  
+
+(*look up key in ordered list*)
 fun xsearch (Olist[], key) = None
   | xsearch (Olist ((keyi,xi)::pairs), key) =
       if xless(keyi,key) then xsearch (Olist pairs, key)
-      else if key=keyi then Some xi  
+      else if key=keyi then Some xi
       else None;
 
 (*insert pair in ordered list, reject if key already present*)
 fun xinsert_new (newpr as (key, x), Olist al) =
   let fun insert [] = [newpr]
-	| insert ((pair as (keyi,xi)) :: pairs) =
-	    if xless(keyi,key) then pair :: insert pairs
-	    else if key=keyi then
-		raise ENVIR("xinsert_new: already present",key)
-	    else newpr::pair::pairs
+        | insert ((pair as (keyi,xi)) :: pairs) =
+            if xless(keyi,key) then pair :: insert pairs
+            else if key=keyi then
+                raise ENVIR("xinsert_new: already present",key)
+            else newpr::pair::pairs
   in  Olist (insert al)  end;
 
 (*insert pair in ordered list, overwrite if key already present*)
 fun xinsert (newpr as (key, x), Olist al) =
   let fun insert [] = [newpr]
-	| insert ((pair as (keyi,xi)) :: pairs) =
-	    if xless(keyi,key) then pair :: insert pairs
-	    else if key=keyi then newpr::pairs
-	    else newpr::pair::pairs
+        | insert ((pair as (keyi,xi)) :: pairs) =
+            if xless(keyi,key) then pair :: insert pairs
+            else if key=keyi then newpr::pairs
+            else newpr::pair::pairs
   in  Olist (insert al)  end;
 
-(*apply function to the contents part of each pair*)   
+(*apply function to the contents part of each pair*)
 fun xmap f (Olist pairs) =
   let fun xmp [] = []
-	| xmp ((key,x)::pairs) = (key, f x) :: xmp pairs
+        | xmp ((key,x)::pairs) = (key, f x) :: xmp pairs
   in Olist (xmp pairs)  end;
 
 (*allows redefinition of a key by "join"ing the contents parts*)
 fun xmerge_olists join (Olist pairsa, Olist pairsb) =
   let fun xmrg ([],pairsb) = pairsb
-	| xmrg (pairsa,[]) = pairsa
-	| xmrg ((keya,x)::pairsa, (keyb,y)::pairsb) =
-	    if xless(keya,keyb) then 
-		(keya,x) :: xmrg (pairsa, (keyb,y)::pairsb)
-	    else if xless(keyb,keya) then
-		(keyb,y) :: xmrg ((keya,x)::pairsa, pairsb)
-	    else (*equal*)  (keya, join(x,y)) :: xmrg (pairsa, pairsb)
+        | xmrg (pairsa,[]) = pairsa
+        | xmrg ((keya,x)::pairsa, (keyb,y)::pairsb) =
+            if xless(keya,keyb) then
+                (keya,x) :: xmrg (pairsa, (keyb,y)::pairsb)
+            else if xless(keyb,keya) then
+                (keyb,y) :: xmrg ((keya,x)::pairsa, pairsb)
+            else (*equal*)  (keya, join(x,y)) :: xmrg (pairsa, pairsb)
   in  Olist (xmrg (pairsa,pairsb))  end;
 
 val null_olist = Olist[];
@@ -97,9 +99,9 @@
    (1) variables out of range   (2) circular assignments
 *)
 datatype env = Envir of
-    {maxidx: int, 		(*maximum index of vars*)
-     asol: term xolist,  	(*table of assignments to Vars*)
-     iTs: (indexname*typ)list}	(*table of assignments to TVars*)
+    {maxidx: int,               (*maximum index of vars*)
+     asol: term xolist,         (*table of assignments to Vars*)
+     iTs: (indexname*typ)list}  (*table of assignments to TVars*)
 
 
 (*Generate a list of distinct variables.
@@ -108,13 +110,13 @@
   let fun genvs (_, [] : typ list) : term list = []
         | genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
         | genvs (n, T::Ts) =
-            Var((name ^ radixstring(26,"a",n), maxidx+1), T) 
-            :: genvs(n+1,Ts) 
+            Var((name ^ radixstring(26,"a",n), maxidx+1), T)
+            :: genvs(n+1,Ts)
   in  (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts))  end;
 
 (*Generate a variable.*)
 fun genvar name (env,T) : env * term =
-  let val (env',[v]) = genvars name (env,[T])  
+  let val (env',[v]) = genvars name (env,[T])
   in  (env',v)  end;
 
 fun lookup (Envir{asol,...}, xname) : term option = xsearch (asol,xname);
@@ -125,15 +127,26 @@
 (*The empty environment.  New variables will start with the given index.*)
 fun empty m = Envir{maxidx=m, asol=null_olist, iTs=[]};
 
+(*is_empty*)
+fun is_empty (Envir {asol = Olist [], iTs = [], ...}) = true
+  | is_empty _ = false;
+
+(*minidx*)
+fun minidx (Envir {asol = Olist asns, iTs, ...}) =
+  (case (asns, iTs) of
+    ([], []) => None
+  | (((_, i), _) :: _, _) => Some (min (i :: map (snd o fst) iTs))
+  | _ => Some (min (map (snd o fst) iTs)));
+
 (*Update, checking Var-Var assignments: try to suppress higher indexes*)
 fun vupdate((a,t), env) = case t of
       Var(name',T) =>
-	if a=name' then env	(*cycle!*)
-	else if xless(a, name')  then  
-	   (case lookup(env,name') of  (*if already assigned, chase*)
-		None => update((name', Var(a,T)), env)
-	      | Some u => vupdate((a,u), env))
-	else update((a,t), env)
+        if a=name' then env     (*cycle!*)
+        else if xless(a, name')  then
+           (case lookup(env,name') of  (*if already assigned, chase*)
+                None => update((name', Var(a,T)), env)
+              | Some u => vupdate((a,u), env))
+        else update((a,t), env)
     | _ => update((a,t), env);
 
 
@@ -141,67 +154,66 @@
 fun alist_of (Envir{maxidx,asol,...}) = alist_of_olist asol;
 
 
-(*Beta normal form for terms (not eta normal form). 
+(*Beta normal form for terms (not eta normal form).
   Chases variables in env;  Does not exploit sharing of variable bindings
   Does not check types, so could loop. *)
-local 
-      (*raised when norm has no effect on a term, 
+local
+      (*raised when norm has no effect on a term,
         to encourage sharing instead of copying*)
   exception SAME;
 
   fun norm_term1 (asol,t) : term =
-    let fun norm (Var (w,T)) = 
-	      (case xsearch(asol,w) of
-		  Some u => normh u
-		| None   => raise SAME)
-	  | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
-	  | norm (Abs(_,_,body) $ t) = normh(subst_bounds([t], body))
-	  | norm (f $ t) =
-	      ((case norm f of
-		 Abs(_,_,body) => normh(subst_bounds([t], body))
-	       | nf => nf $ normh t)
-	      handle SAME => f $ norm t)
-	  | norm _ =  raise SAME
-	and normh t = (norm t) handle SAME => t
+    let fun norm (Var (w,T)) =
+              (case xsearch(asol,w) of
+                  Some u => normh u
+                | None   => raise SAME)
+          | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
+          | norm (Abs(_,_,body) $ t) = normh(subst_bounds([t], body))
+          | norm (f $ t) =
+              ((case norm f of
+                 Abs(_,_,body) => normh(subst_bounds([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
 
   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 assoc(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 :: normTsh Ts)
-			     handle SAME => T :: normTs Ts)
-	and normTsh Ts = ((normTs Ts) handle SAME => Ts)
-	and norm(Const(a,T)) = Const(a, normT T)
-	  | norm(Free(a,T)) = Free(a, normT T)
-	  | norm(Var (w,T)) = 
-	      (case xsearch(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_bounds([t], body))
-	  | norm(f $ t) =
-	      ((case norm f of
-		 Abs(_,_,body) => normh(subst_bounds([t], body))
-	       | nf => nf $ normh t)
-	      handle SAME => f $ norm t)
-	  | norm _ =  raise SAME
-	and normh t = (norm t) handle SAME => t
+          | normT(TFree _) = raise SAME
+          | normT(TVar(v,_)) = (case assoc(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 :: normTsh Ts)
+                             handle SAME => T :: normTs Ts)
+        and normTsh Ts = ((normTs Ts) handle SAME => Ts)
+        and norm(Const(a,T)) = Const(a, normT T)
+          | norm(Free(a,T)) = Free(a, normT T)
+          | norm(Var (w,T)) =
+              (case xsearch(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_bounds([t], body))
+          | norm(f $ t) =
+              ((case norm f of
+                 Abs(_,_,body) => normh(subst_bounds([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;
 
 in
 
 (*curried version might be slower in recursive calls*)
 fun norm_term (env as Envir{asol,iTs,...}) t : term =
-	if iTs=[] then norm_term1(asol, t) else norm_term2(asol,iTs, t)
+        if iTs=[] then norm_term1(asol, t) else norm_term2(asol,iTs, t)
 
 end;
 
 end;
 
-