0

1 
(* Title: envir


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1988 University of Cambridge


5 
*)


6 


7 
(*Environments


8 
Should take account that typ is part of variable name,


9 
otherwise two variables with same name and different types


10 
will cause errors!


11 
*)


12 


13 


14 
signature ENVIR =


15 
sig


16 
type 'a xolist


17 
exception ENVIR of string * indexname;


18 
datatype env = Envir of {asol: term xolist,


19 
iTs: (indexname * typ) list,


20 
maxidx: int}


21 
val alist_of : env > (indexname * term) list


22 
val alist_of_olist : 'a xolist > (indexname * 'a) list


23 
val empty : int>env


24 
val genvar : string > env * typ > env * term


25 
val genvars : string > env * typ list > env * term list


26 
val lookup : env * indexname > term option


27 
val norm_term : env > term > term


28 
val null_olist : 'a xolist


29 
val olist_of_alist: (indexname * 'a) list > 'a xolist


30 
val update : (indexname * term) * env > env


31 
val vupdate : (indexname * term) * env > env


32 
end;


33 


34 
functor EnvirFun () : ENVIR =


35 
struct


36 


37 


38 
(*association lists with keys in ascending order, no repeated keys*)


39 
datatype 'a xolist = Olist of (indexname * 'a) list;


40 


41 


42 
exception ENVIR of string * indexname;


43 


44 
(*look up key in ordered list*)


45 
fun xsearch (Olist[], key) = None


46 
 xsearch (Olist ((keyi,xi)::pairs), key) =


47 
if xless(keyi,key) then xsearch (Olist pairs, key)


48 
else if key=keyi then Some xi


49 
else None;


50 


51 
(*insert pair in ordered list, reject if key already present*)


52 
fun xinsert_new (newpr as (key, x), Olist al) =


53 
let fun insert [] = [newpr]


54 
 insert ((pair as (keyi,xi)) :: pairs) =


55 
if xless(keyi,key) then pair :: insert pairs


56 
else if key=keyi then


57 
raise ENVIR("xinsert_new: already present",key)


58 
else newpr::pair::pairs


59 
in Olist (insert al) end;


60 


61 
(*insert pair in ordered list, overwrite if key already present*)


62 
fun xinsert (newpr as (key, x), Olist al) =


63 
let fun insert [] = [newpr]


64 
 insert ((pair as (keyi,xi)) :: pairs) =


65 
if xless(keyi,key) then pair :: insert pairs


66 
else if key=keyi then newpr::pairs


67 
else newpr::pair::pairs


68 
in Olist (insert al) end;


69 


70 
(*apply function to the contents part of each pair*)


71 
fun xmap f (Olist pairs) =


72 
let fun xmp [] = []


73 
 xmp ((key,x)::pairs) = (key, f x) :: xmp pairs


74 
in Olist (xmp pairs) end;


75 


76 
(*allows redefinition of a key by "join"ing the contents parts*)


77 
fun xmerge_olists join (Olist pairsa, Olist pairsb) =


78 
let fun xmrg ([],pairsb) = pairsb


79 
 xmrg (pairsa,[]) = pairsa


80 
 xmrg ((keya,x)::pairsa, (keyb,y)::pairsb) =


81 
if xless(keya,keyb) then


82 
(keya,x) :: xmrg (pairsa, (keyb,y)::pairsb)


83 
else if xless(keyb,keya) then


84 
(keyb,y) :: xmrg ((keya,x)::pairsa, pairsb)


85 
else (*equal*) (keya, join(x,y)) :: xmrg (pairsa, pairsb)


86 
in Olist (xmrg (pairsa,pairsb)) end;


87 


88 
val null_olist = Olist[];


89 


90 
fun alist_of_olist (Olist pairs) = pairs;


91 


92 
fun olist_of_alist pairs = foldr xinsert (pairs, Olist[]);


93 


94 


95 


96 
(*updating can destroy environment in 2 ways!!


97 
(1) variables out of range (2) circular assignments


98 
*)


99 
datatype env = Envir of


100 
{maxidx: int, (*maximum index of vars*)


101 
asol: term xolist, (*table of assignments to Vars*)


102 
iTs: (indexname*typ)list} (*table of assignments to TVars*)


103 


104 


105 
(*Generate a list of distinct variables.


106 
Increments index to make them distinct from ALL present variables. *)


107 
fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list =


108 
let fun genvs (_, [] : typ list) : term list = []


109 
 genvs (n, [T]) = [ Var((name, maxidx+1), T) ]


110 
 genvs (n, T::Ts) =


111 
Var((name ^ radixstring(26,"a",n), maxidx+1), T)


112 
:: genvs(n+1,Ts)


113 
in (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts)) end;


114 


115 
(*Generate a variable.*)


116 
fun genvar name (env,T) : env * term =


117 
let val (env',[v]) = genvars name (env,[T])


118 
in (env',v) end;


119 


120 
fun lookup (Envir{asol,...}, xname) : term option = xsearch (asol,xname);


121 


122 
fun update ((xname, t), Envir{maxidx, asol, iTs}) =


123 
Envir{maxidx=maxidx, asol=xinsert_new ((xname,t), asol), iTs=iTs};


124 


125 
(*The empty environment. New variables will start with the given index.*)


126 
fun empty m = Envir{maxidx=m, asol=null_olist, iTs=[]};


127 


128 
(*Update, checking VarVar assignments: try to suppress higher indexes*)


129 
fun vupdate((a,t), env) = case t of


130 
Var(name',T) =>


131 
if a=name' then env (*cycle!*)


132 
else if xless(a, name') then


133 
(case lookup(env,name') of (*if already assigned, chase*)


134 
None => update((name', Var(a,T)), env)


135 
 Some u => vupdate((a,u), env))


136 
else update((a,t), env)


137 
 _ => update((a,t), env);


138 


139 


140 
(*Convert environment to alist*)


141 
fun alist_of (Envir{maxidx,asol,...}) = alist_of_olist asol;


142 


143 


144 
(*Beta normal form for terms (not eta normal form).


145 
Chases variables in env; Does not exploit sharing of variable bindings


146 
Does not check types, so could loop. *)


147 
local


148 
(*raised when norm has no effect on a term,


149 
to encourage sharing instead of copying*)


150 
exception SAME;


151 


152 
fun norm_term1 (asol,t) : term =


153 
let fun norm (Var (w,T)) =


154 
(case xsearch(asol,w) of


155 
Some u => normh u


156 
 None => raise SAME)


157 
 norm (Abs(a,T,body)) = Abs(a, T, norm body)


158 
 norm (Abs(_,_,body) $ t) = normh(subst_bounds([t], body))


159 
 norm (f $ t) =


160 
((case norm f of


161 
Abs(_,_,body) => normh(subst_bounds([t], body))


162 
 nf => nf $ normh t)


163 
handle SAME => f $ norm t)


164 
 norm _ = raise SAME


165 
and normh t = (norm t) handle SAME => t


166 
in normh t end


167 


168 
and norm_term2(asol,iTs,t) : term =


169 
let fun normT(Type(a,Ts)) = Type(a, normTs Ts)


170 
 normT(TFree _) = raise SAME


171 
 normT(TVar(v,_)) = (case assoc(iTs,v) of


172 
Some(U) => normTh U


173 
 None => raise SAME)


174 
and normTh T = ((normT T) handle SAME => T)


175 
and normTs([]) = raise SAME


176 
 normTs(T::Ts) = ((normT T :: normTsh Ts)


177 
handle SAME => T :: normTs Ts)


178 
and normTsh Ts = ((normTs Ts) handle SAME => Ts)


179 
and norm(Const(a,T)) = Const(a, normT T)


180 
 norm(Free(a,T)) = Free(a, normT T)


181 
 norm(Var (w,T)) =


182 
(case xsearch(asol,w) of


183 
Some u => normh u


184 
 None => Var(w,normT T))


185 
 norm(Abs(a,T,body)) =


186 
(Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body))


187 
 norm(Abs(_,_,body) $ t) = normh(subst_bounds([t], body))


188 
 norm(f $ t) =


189 
((case norm f of


190 
Abs(_,_,body) => normh(subst_bounds([t], body))


191 
 nf => nf $ normh t)


192 
handle SAME => f $ norm t)


193 
 norm _ = raise SAME


194 
and normh t = (norm t) handle SAME => t


195 
in normh t end;


196 


197 
in


198 


199 
(*curried version might be slower in recursive calls*)


200 
fun norm_term (env as Envir{asol,iTs,...}) t : term =


201 
if iTs=[] then norm_term1(asol, t) else norm_term2(asol,iTs, t)


202 


203 
end;


204 


205 
end;


206 


207 
