author  wenzelm 
Mon, 24 Jan 1994 12:03:53 +0100  
changeset 247  bc10568855ee 
parent 0  a5a9c433f639 
child 719  e3e1d1a6d408 
permissions  rwrr 
247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

1 
(* Title: Pure/envir.ML 
0  2 
ID: $Id$ 
247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  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 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

14 
signature ENVIR = 
0  15 
sig 
16 
type 'a xolist 

17 
exception ENVIR of string * indexname; 

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

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

19 
iTs: (indexname * typ) list, 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

20 
maxidx: int} 
0  21 
val alist_of : env > (indexname * term) list 
22 
val alist_of_olist : 'a xolist > (indexname * 'a) list 

23 
val empty : int>env 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

24 
val is_empty : env > bool 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

25 
val minidx : env > int option 
0  26 
val genvar : string > env * typ > env * term 
27 
val genvars : string > env * typ list > env * term list 

28 
val lookup : env * indexname > term option 

29 
val norm_term : env > term > term 

30 
val null_olist : 'a xolist 

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

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

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

34 
end; 

35 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

36 
functor EnvirFun () : ENVIR = 
0  37 
struct 
38 

39 

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

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

42 

43 

44 
exception ENVIR of string * indexname; 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

45 

bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

46 
(*look up key in ordered list*) 
0  47 
fun xsearch (Olist[], key) = None 
48 
 xsearch (Olist ((keyi,xi)::pairs), key) = 

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

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

50 
else if key=keyi then Some xi 
0  51 
else None; 
52 

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

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

55 
let fun insert [] = [newpr] 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

56 
 insert ((pair as (keyi,xi)) :: pairs) = 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

57 
if xless(keyi,key) then pair :: insert pairs 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

58 
else if key=keyi then 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

59 
raise ENVIR("xinsert_new: already present",key) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

60 
else newpr::pair::pairs 
0  61 
in Olist (insert al) end; 
62 

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

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

65 
let fun insert [] = [newpr] 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

66 
 insert ((pair as (keyi,xi)) :: pairs) = 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

67 
if xless(keyi,key) then pair :: insert pairs 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

68 
else if key=keyi then newpr::pairs 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

69 
else newpr::pair::pairs 
0  70 
in Olist (insert al) end; 
71 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

72 
(*apply function to the contents part of each pair*) 
0  73 
fun xmap f (Olist pairs) = 
74 
let fun xmp [] = [] 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

75 
 xmp ((key,x)::pairs) = (key, f x) :: xmp pairs 
0  76 
in Olist (xmp pairs) end; 
77 

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

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

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

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

81 
 xmrg (pairsa,[]) = pairsa 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

82 
 xmrg ((keya,x)::pairsa, (keyb,y)::pairsb) = 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

83 
if xless(keya,keyb) then 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

84 
(keya,x) :: xmrg (pairsa, (keyb,y)::pairsb) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

85 
else if xless(keyb,keya) then 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

86 
(keyb,y) :: xmrg ((keya,x)::pairsa, pairsb) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

87 
else (*equal*) (keya, join(x,y)) :: xmrg (pairsa, pairsb) 
0  88 
in Olist (xmrg (pairsa,pairsb)) end; 
89 

90 
val null_olist = Olist[]; 

91 

92 
fun alist_of_olist (Olist pairs) = pairs; 

93 

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

95 

96 

97 

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

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

100 
*) 

101 
datatype env = Envir of 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

102 
{maxidx: int, (*maximum index of vars*) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

103 
asol: term xolist, (*table of assignments to Vars*) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

104 
iTs: (indexname*typ)list} (*table of assignments to TVars*) 
0  105 

106 

107 
(*Generate a list of distinct variables. 

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

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

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

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

112 
 genvs (n, T::Ts) = 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

113 
Var((name ^ radixstring(26,"a",n), maxidx+1), T) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

114 
:: genvs(n+1,Ts) 
0  115 
in (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts)) end; 
116 

117 
(*Generate a variable.*) 

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

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

119 
let val (env',[v]) = genvars name (env,[T]) 
0  120 
in (env',v) end; 
121 

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

123 

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

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

126 

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

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

129 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

130 
(*is_empty*) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

131 
fun is_empty (Envir {asol = Olist [], iTs = [], ...}) = true 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

132 
 is_empty _ = false; 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

133 

bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

134 
(*minidx*) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

135 
fun minidx (Envir {asol = Olist asns, iTs, ...}) = 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

136 
(case (asns, iTs) of 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

137 
([], []) => None 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

138 
 (((_, i), _) :: _, _) => Some (min (i :: map (snd o fst) iTs)) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

139 
 _ => Some (min (map (snd o fst) iTs))); 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

140 

0  141 
(*Update, checking VarVar assignments: try to suppress higher indexes*) 
142 
fun vupdate((a,t), env) = case t of 

143 
Var(name',T) => 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

144 
if a=name' then env (*cycle!*) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

145 
else if xless(a, name') then 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

146 
(case lookup(env,name') of (*if already assigned, chase*) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

147 
None => update((name', Var(a,T)), env) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

148 
 Some u => vupdate((a,u), env)) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

149 
else update((a,t), env) 
0  150 
 _ => update((a,t), env); 
151 

152 

153 
(*Convert environment to alist*) 

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

155 

156 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

157 
(*Beta normal form for terms (not eta normal form). 
0  158 
Chases variables in env; Does not exploit sharing of variable bindings 
159 
Does not check types, so could loop. *) 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

160 
local 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

161 
(*raised when norm has no effect on a term, 
0  162 
to encourage sharing instead of copying*) 
163 
exception SAME; 

164 

165 
fun norm_term1 (asol,t) : term = 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

166 
let fun norm (Var (w,T)) = 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

167 
(case xsearch(asol,w) of 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

168 
Some u => normh u 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

169 
 None => raise SAME) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

170 
 norm (Abs(a,T,body)) = Abs(a, T, norm body) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

171 
 norm (Abs(_,_,body) $ t) = normh(subst_bounds([t], body)) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

172 
 norm (f $ t) = 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

173 
((case norm f of 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

174 
Abs(_,_,body) => normh(subst_bounds([t], body)) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

175 
 nf => nf $ normh t) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

176 
handle SAME => f $ norm t) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

177 
 norm _ = raise SAME 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

178 
and normh t = (norm t) handle SAME => t 
0  179 
in normh t end 
180 

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

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

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

183 
 normT(TFree _) = raise SAME 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

184 
 normT(TVar(v,_)) = (case assoc(iTs,v) of 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

185 
Some(U) => normTh U 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

186 
 None => raise SAME) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

187 
and normTh T = ((normT T) handle SAME => T) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

188 
and normTs([]) = raise SAME 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

189 
 normTs(T::Ts) = ((normT T :: normTsh Ts) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

190 
handle SAME => T :: normTs Ts) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

191 
and normTsh Ts = ((normTs Ts) handle SAME => Ts) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

192 
and norm(Const(a,T)) = Const(a, normT T) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

193 
 norm(Free(a,T)) = Free(a, normT T) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

194 
 norm(Var (w,T)) = 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

195 
(case xsearch(asol,w) of 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

196 
Some u => normh u 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

197 
 None => Var(w,normT T)) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

198 
 norm(Abs(a,T,body)) = 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

199 
(Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body)) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

200 
 norm(Abs(_,_,body) $ t) = normh(subst_bounds([t], body)) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

201 
 norm(f $ t) = 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

202 
((case norm f of 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

203 
Abs(_,_,body) => normh(subst_bounds([t], body)) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

204 
 nf => nf $ normh t) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

205 
handle SAME => f $ norm t) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

206 
 norm _ = raise SAME 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

207 
and normh t = (norm t) handle SAME => t 
0  208 
in normh t end; 
209 

210 
in 

211 

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

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

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

214 
if iTs=[] then norm_term1(asol, t) else norm_term2(asol,iTs, t) 
0  215 

216 
end; 

217 

218 
end; 

219 