src/Pure/envir.ML
changeset 247 bc10568855ee
parent 0 a5a9c433f639
child 719 e3e1d1a6d408
     1.1 --- a/src/Pure/envir.ML	Thu Jan 20 13:35:40 1994 +0100
     1.2 +++ b/src/Pure/envir.ML	Mon Jan 24 12:03:53 1994 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	envir
     1.5 +(*  Title:      Pure/envir.ML
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1988  University of Cambridge
    1.10  *)
    1.11  
    1.12 @@ -11,16 +11,18 @@
    1.13  *)
    1.14  
    1.15  
    1.16 -signature ENVIR = 
    1.17 +signature ENVIR =
    1.18  sig
    1.19    type 'a xolist
    1.20    exception ENVIR of string * indexname;
    1.21    datatype env = Envir of {asol: term xolist,
    1.22 -			   iTs: (indexname * typ) list,
    1.23 -			   maxidx: int}
    1.24 +                           iTs: (indexname * typ) list,
    1.25 +                           maxidx: int}
    1.26    val alist_of : env -> (indexname * term) list
    1.27    val alist_of_olist : 'a xolist -> (indexname * 'a) list
    1.28    val empty : int->env
    1.29 +  val is_empty : env -> bool
    1.30 +  val minidx : env -> int option
    1.31    val genvar  : string -> env * typ -> env * term
    1.32    val genvars : string -> env * typ list -> env * term list
    1.33    val lookup : env * indexname -> term option
    1.34 @@ -31,7 +33,7 @@
    1.35    val vupdate : (indexname * term) * env -> env
    1.36  end;
    1.37  
    1.38 -functor EnvirFun () : ENVIR = 
    1.39 +functor EnvirFun () : ENVIR =
    1.40  struct
    1.41  
    1.42  
    1.43 @@ -40,49 +42,49 @@
    1.44  
    1.45  
    1.46  exception ENVIR of string * indexname;
    1.47 - 
    1.48 -(*look up key in ordered list*)  
    1.49 +
    1.50 +(*look up key in ordered list*)
    1.51  fun xsearch (Olist[], key) = None
    1.52    | xsearch (Olist ((keyi,xi)::pairs), key) =
    1.53        if xless(keyi,key) then xsearch (Olist pairs, key)
    1.54 -      else if key=keyi then Some xi  
    1.55 +      else if key=keyi then Some xi
    1.56        else None;
    1.57  
    1.58  (*insert pair in ordered list, reject if key already present*)
    1.59  fun xinsert_new (newpr as (key, x), Olist al) =
    1.60    let fun insert [] = [newpr]
    1.61 -	| insert ((pair as (keyi,xi)) :: pairs) =
    1.62 -	    if xless(keyi,key) then pair :: insert pairs
    1.63 -	    else if key=keyi then
    1.64 -		raise ENVIR("xinsert_new: already present",key)
    1.65 -	    else newpr::pair::pairs
    1.66 +        | insert ((pair as (keyi,xi)) :: pairs) =
    1.67 +            if xless(keyi,key) then pair :: insert pairs
    1.68 +            else if key=keyi then
    1.69 +                raise ENVIR("xinsert_new: already present",key)
    1.70 +            else newpr::pair::pairs
    1.71    in  Olist (insert al)  end;
    1.72  
    1.73  (*insert pair in ordered list, overwrite if key already present*)
    1.74  fun xinsert (newpr as (key, x), Olist al) =
    1.75    let fun insert [] = [newpr]
    1.76 -	| insert ((pair as (keyi,xi)) :: pairs) =
    1.77 -	    if xless(keyi,key) then pair :: insert pairs
    1.78 -	    else if key=keyi then newpr::pairs
    1.79 -	    else newpr::pair::pairs
    1.80 +        | insert ((pair as (keyi,xi)) :: pairs) =
    1.81 +            if xless(keyi,key) then pair :: insert pairs
    1.82 +            else if key=keyi then newpr::pairs
    1.83 +            else newpr::pair::pairs
    1.84    in  Olist (insert al)  end;
    1.85  
    1.86 -(*apply function to the contents part of each pair*)   
    1.87 +(*apply function to the contents part of each pair*)
    1.88  fun xmap f (Olist pairs) =
    1.89    let fun xmp [] = []
    1.90 -	| xmp ((key,x)::pairs) = (key, f x) :: xmp pairs
    1.91 +        | xmp ((key,x)::pairs) = (key, f x) :: xmp pairs
    1.92    in Olist (xmp pairs)  end;
    1.93  
    1.94  (*allows redefinition of a key by "join"ing the contents parts*)
    1.95  fun xmerge_olists join (Olist pairsa, Olist pairsb) =
    1.96    let fun xmrg ([],pairsb) = pairsb
    1.97 -	| xmrg (pairsa,[]) = pairsa
    1.98 -	| xmrg ((keya,x)::pairsa, (keyb,y)::pairsb) =
    1.99 -	    if xless(keya,keyb) then 
   1.100 -		(keya,x) :: xmrg (pairsa, (keyb,y)::pairsb)
   1.101 -	    else if xless(keyb,keya) then
   1.102 -		(keyb,y) :: xmrg ((keya,x)::pairsa, pairsb)
   1.103 -	    else (*equal*)  (keya, join(x,y)) :: xmrg (pairsa, pairsb)
   1.104 +        | xmrg (pairsa,[]) = pairsa
   1.105 +        | xmrg ((keya,x)::pairsa, (keyb,y)::pairsb) =
   1.106 +            if xless(keya,keyb) then
   1.107 +                (keya,x) :: xmrg (pairsa, (keyb,y)::pairsb)
   1.108 +            else if xless(keyb,keya) then
   1.109 +                (keyb,y) :: xmrg ((keya,x)::pairsa, pairsb)
   1.110 +            else (*equal*)  (keya, join(x,y)) :: xmrg (pairsa, pairsb)
   1.111    in  Olist (xmrg (pairsa,pairsb))  end;
   1.112  
   1.113  val null_olist = Olist[];
   1.114 @@ -97,9 +99,9 @@
   1.115     (1) variables out of range   (2) circular assignments
   1.116  *)
   1.117  datatype env = Envir of
   1.118 -    {maxidx: int, 		(*maximum index of vars*)
   1.119 -     asol: term xolist,  	(*table of assignments to Vars*)
   1.120 -     iTs: (indexname*typ)list}	(*table of assignments to TVars*)
   1.121 +    {maxidx: int,               (*maximum index of vars*)
   1.122 +     asol: term xolist,         (*table of assignments to Vars*)
   1.123 +     iTs: (indexname*typ)list}  (*table of assignments to TVars*)
   1.124  
   1.125  
   1.126  (*Generate a list of distinct variables.
   1.127 @@ -108,13 +110,13 @@
   1.128    let fun genvs (_, [] : typ list) : term list = []
   1.129          | genvs (n, [T]) = [ Var((name, maxidx+1), T) ]
   1.130          | genvs (n, T::Ts) =
   1.131 -            Var((name ^ radixstring(26,"a",n), maxidx+1), T) 
   1.132 -            :: genvs(n+1,Ts) 
   1.133 +            Var((name ^ radixstring(26,"a",n), maxidx+1), T)
   1.134 +            :: genvs(n+1,Ts)
   1.135    in  (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts))  end;
   1.136  
   1.137  (*Generate a variable.*)
   1.138  fun genvar name (env,T) : env * term =
   1.139 -  let val (env',[v]) = genvars name (env,[T])  
   1.140 +  let val (env',[v]) = genvars name (env,[T])
   1.141    in  (env',v)  end;
   1.142  
   1.143  fun lookup (Envir{asol,...}, xname) : term option = xsearch (asol,xname);
   1.144 @@ -125,15 +127,26 @@
   1.145  (*The empty environment.  New variables will start with the given index.*)
   1.146  fun empty m = Envir{maxidx=m, asol=null_olist, iTs=[]};
   1.147  
   1.148 +(*is_empty*)
   1.149 +fun is_empty (Envir {asol = Olist [], iTs = [], ...}) = true
   1.150 +  | is_empty _ = false;
   1.151 +
   1.152 +(*minidx*)
   1.153 +fun minidx (Envir {asol = Olist asns, iTs, ...}) =
   1.154 +  (case (asns, iTs) of
   1.155 +    ([], []) => None
   1.156 +  | (((_, i), _) :: _, _) => Some (min (i :: map (snd o fst) iTs))
   1.157 +  | _ => Some (min (map (snd o fst) iTs)));
   1.158 +
   1.159  (*Update, checking Var-Var assignments: try to suppress higher indexes*)
   1.160  fun vupdate((a,t), env) = case t of
   1.161        Var(name',T) =>
   1.162 -	if a=name' then env	(*cycle!*)
   1.163 -	else if xless(a, name')  then  
   1.164 -	   (case lookup(env,name') of  (*if already assigned, chase*)
   1.165 -		None => update((name', Var(a,T)), env)
   1.166 -	      | Some u => vupdate((a,u), env))
   1.167 -	else update((a,t), env)
   1.168 +        if a=name' then env     (*cycle!*)
   1.169 +        else if xless(a, name')  then
   1.170 +           (case lookup(env,name') of  (*if already assigned, chase*)
   1.171 +                None => update((name', Var(a,T)), env)
   1.172 +              | Some u => vupdate((a,u), env))
   1.173 +        else update((a,t), env)
   1.174      | _ => update((a,t), env);
   1.175  
   1.176  
   1.177 @@ -141,67 +154,66 @@
   1.178  fun alist_of (Envir{maxidx,asol,...}) = alist_of_olist asol;
   1.179  
   1.180  
   1.181 -(*Beta normal form for terms (not eta normal form). 
   1.182 +(*Beta normal form for terms (not eta normal form).
   1.183    Chases variables in env;  Does not exploit sharing of variable bindings
   1.184    Does not check types, so could loop. *)
   1.185 -local 
   1.186 -      (*raised when norm has no effect on a term, 
   1.187 +local
   1.188 +      (*raised when norm has no effect on a term,
   1.189          to encourage sharing instead of copying*)
   1.190    exception SAME;
   1.191  
   1.192    fun norm_term1 (asol,t) : term =
   1.193 -    let fun norm (Var (w,T)) = 
   1.194 -	      (case xsearch(asol,w) of
   1.195 -		  Some u => normh u
   1.196 -		| None   => raise SAME)
   1.197 -	  | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
   1.198 -	  | norm (Abs(_,_,body) $ t) = normh(subst_bounds([t], body))
   1.199 -	  | norm (f $ t) =
   1.200 -	      ((case norm f of
   1.201 -		 Abs(_,_,body) => normh(subst_bounds([t], body))
   1.202 -	       | nf => nf $ normh t)
   1.203 -	      handle SAME => f $ norm t)
   1.204 -	  | norm _ =  raise SAME
   1.205 -	and normh t = (norm t) handle SAME => t
   1.206 +    let fun norm (Var (w,T)) =
   1.207 +              (case xsearch(asol,w) of
   1.208 +                  Some u => normh u
   1.209 +                | None   => raise SAME)
   1.210 +          | norm (Abs(a,T,body)) =  Abs(a, T, norm body)
   1.211 +          | norm (Abs(_,_,body) $ t) = normh(subst_bounds([t], body))
   1.212 +          | norm (f $ t) =
   1.213 +              ((case norm f of
   1.214 +                 Abs(_,_,body) => normh(subst_bounds([t], body))
   1.215 +               | nf => nf $ normh t)
   1.216 +              handle SAME => f $ norm t)
   1.217 +          | norm _ =  raise SAME
   1.218 +        and normh t = (norm t) handle SAME => t
   1.219      in normh t end
   1.220  
   1.221    and norm_term2(asol,iTs,t) : term =
   1.222      let fun normT(Type(a,Ts)) = Type(a, normTs Ts)
   1.223 -	  | normT(TFree _) = raise SAME
   1.224 -	  | normT(TVar(v,_)) = (case assoc(iTs,v) of
   1.225 -		  Some(U) => normTh U
   1.226 -		| None => raise SAME)
   1.227 -	and normTh T = ((normT T) handle SAME => T)
   1.228 -	and normTs([]) = raise SAME
   1.229 -	  | normTs(T::Ts) = ((normT T :: normTsh Ts)
   1.230 -			     handle SAME => T :: normTs Ts)
   1.231 -	and normTsh Ts = ((normTs Ts) handle SAME => Ts)
   1.232 -	and norm(Const(a,T)) = Const(a, normT T)
   1.233 -	  | norm(Free(a,T)) = Free(a, normT T)
   1.234 -	  | norm(Var (w,T)) = 
   1.235 -	      (case xsearch(asol,w) of
   1.236 -		  Some u => normh u
   1.237 -		| None   => Var(w,normT T))
   1.238 -	  | norm(Abs(a,T,body)) =
   1.239 -		(Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body))
   1.240 -	  | norm(Abs(_,_,body) $ t) = normh(subst_bounds([t], body))
   1.241 -	  | norm(f $ t) =
   1.242 -	      ((case norm f of
   1.243 -		 Abs(_,_,body) => normh(subst_bounds([t], body))
   1.244 -	       | nf => nf $ normh t)
   1.245 -	      handle SAME => f $ norm t)
   1.246 -	  | norm _ =  raise SAME
   1.247 -	and normh t = (norm t) handle SAME => t
   1.248 +          | normT(TFree _) = raise SAME
   1.249 +          | normT(TVar(v,_)) = (case assoc(iTs,v) of
   1.250 +                  Some(U) => normTh U
   1.251 +                | None => raise SAME)
   1.252 +        and normTh T = ((normT T) handle SAME => T)
   1.253 +        and normTs([]) = raise SAME
   1.254 +          | normTs(T::Ts) = ((normT T :: normTsh Ts)
   1.255 +                             handle SAME => T :: normTs Ts)
   1.256 +        and normTsh Ts = ((normTs Ts) handle SAME => Ts)
   1.257 +        and norm(Const(a,T)) = Const(a, normT T)
   1.258 +          | norm(Free(a,T)) = Free(a, normT T)
   1.259 +          | norm(Var (w,T)) =
   1.260 +              (case xsearch(asol,w) of
   1.261 +                  Some u => normh u
   1.262 +                | None   => Var(w,normT T))
   1.263 +          | norm(Abs(a,T,body)) =
   1.264 +                (Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body))
   1.265 +          | norm(Abs(_,_,body) $ t) = normh(subst_bounds([t], body))
   1.266 +          | norm(f $ t) =
   1.267 +              ((case norm f of
   1.268 +                 Abs(_,_,body) => normh(subst_bounds([t], body))
   1.269 +               | nf => nf $ normh t)
   1.270 +              handle SAME => f $ norm t)
   1.271 +          | norm _ =  raise SAME
   1.272 +        and normh t = (norm t) handle SAME => t
   1.273      in normh t end;
   1.274  
   1.275  in
   1.276  
   1.277  (*curried version might be slower in recursive calls*)
   1.278  fun norm_term (env as Envir{asol,iTs,...}) t : term =
   1.279 -	if iTs=[] then norm_term1(asol, t) else norm_term2(asol,iTs, t)
   1.280 +        if iTs=[] then norm_term1(asol, t) else norm_term2(asol,iTs, t)
   1.281  
   1.282  end;
   1.283  
   1.284  end;
   1.285  
   1.286 -