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 Var-Var 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 |
|