author  paulson 
Tue, 22 Jul 1997 11:14:18 +0200  
changeset 3538  ed9de44032e0 
parent 2191  58383908f177 
child 5289  41b949f3b8ac 
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 

2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

7 
(*Environments. They don't take account that typ is part of variable name. 
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

8 
Therefore we check elsewhere that two variables with same 
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

9 
names and different types cannot occur. 
0  10 
*) 
11 

12 

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

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

16 
exception ENVIR of string * indexname; 

2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

17 
datatype env = Envir of {asol: term xolist, iTs: typ xolist, maxidx: int} 
1460  18 
val alist_of : env > (indexname * term) list 
19 
val alist_of_olist : 'a xolist > (indexname * 'a) list 

20 
val empty : int>env 

21 
val is_empty : env > bool 

2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

22 
val above : int * env > bool 
1460  23 
val genvar : string > env * typ > env * term 
24 
val genvars : string > env * typ list > env * term list 

25 
val lookup : env * indexname > term option 

26 
val norm_term : env > term > term 

27 
val null_olist : 'a xolist 

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

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

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

0  31 
end; 
32 

1500  33 
structure Envir : ENVIR = 
0  34 
struct 
35 

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

2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

37 
type 'a xolist = (indexname * 'a) list; 
0  38 

39 

40 
exception ENVIR of string * indexname; 

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

41 

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

42 
(*look up key in ordered list*) 
2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

43 
fun xsearch ([], key) = None 
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

44 
 xsearch (((keyi,xi)::pairs), key) = 
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

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

46 
else if key=keyi then Some xi 
0  47 
else None; 
48 

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

2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

50 
fun xinsert_new (newpr as (key, x), al) = 
0  51 
let fun insert [] = [newpr] 
247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

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

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

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

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

56 
else newpr::pair::pairs 
2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

57 
in (insert al) end; 
0  58 

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

2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

60 
fun xinsert (newpr as (key, x), al) = 
0  61 
let fun insert [] = [newpr] 
247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

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

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

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

65 
else newpr::pair::pairs 
2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

66 
in (insert al) end; 
0  67 

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

68 
(*apply function to the contents part of each pair*) 
2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

69 
fun xmap f (pairs) = 
0  70 
let fun xmp [] = [] 
247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

71 
 xmp ((key,x)::pairs) = (key, f x) :: xmp pairs 
2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

72 
in (xmp pairs) end; 
0  73 

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

2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

75 
fun xmerge_olists join (pairsa, pairsb) = 
0  76 
let fun xmrg ([],pairsb) = pairsb 
247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

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

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

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

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

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

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

83 
else (*equal*) (keya, join(x,y)) :: xmrg (pairsa, pairsb) 
2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

84 
in (xmrg (pairsa,pairsb)) end; 
0  85 

2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

86 
val null_olist = []; 
0  87 

2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

88 
fun alist_of_olist (pairs) = pairs; 
0  89 

2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

90 
fun olist_of_alist pairs = foldr xinsert (pairs, []); 
0  91 

92 

93 

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

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

96 
*) 

97 
datatype env = Envir of 

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

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

99 
asol: term xolist, (*table of assignments to Vars*) 
2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

100 
iTs: typ xolist} (*table of assignments to TVars*) 
0  101 

102 

103 
(*Generate a list of distinct variables. 

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

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

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

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

108 
 genvs (n, T::Ts) = 

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

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

110 
:: genvs(n+1,Ts) 
0  111 
in (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts)) end; 
112 

113 
(*Generate a variable.*) 

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

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

115 
let val (env',[v]) = genvars name (env,[T]) 
0  116 
in (env',v) end; 
117 

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

119 

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

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

122 

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

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

125 

2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

126 
(*Test for empty environment*) 
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

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

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

129 

2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

130 
(*Determine if the least index updated exceeds lim*) 
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

131 
fun above (lim, Envir {asol, iTs, ...}) = 
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

132 
let fun upd [] = true 
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

133 
 upd (i::is) = i>lim andalso upd is 
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

134 
in upd (map (#2 o #1) asol @ (map (#2 o #1) iTs)) 
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

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

136 

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

139 
Var(name',T) => 

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

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

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

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

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

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

145 
else update((a,t), env) 
0  146 
 _ => update((a,t), env); 
147 

148 

149 
(*Convert environment to alist*) 

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

151 

152 

1500  153 
(*** Beta normal form for terms (not eta normal form). 
154 
Chases variables in env; Does not exploit sharing of variable bindings 

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

156 

157 
(*raised when norm has no effect on a term, to do sharing instead of copying*) 

158 
exception SAME; 

0  159 

1500  160 
fun norm_term1 (asol,t) : term = 
161 
let fun norm (Var (w,T)) = 

162 
(case xsearch(asol,w) of 

2191  163 
Some u => (norm u handle SAME => u) 
1500  164 
 None => raise SAME) 
165 
 norm (Abs(a,T,body)) = Abs(a, T, norm body) 

2191  166 
 norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body)) 
1500  167 
 norm (f $ t) = 
168 
((case norm f of 

2191  169 
Abs(_,_,body) => normh(subst_bound (t, body)) 
170 
 nf => nf $ (norm t handle SAME => t)) 

1500  171 
handle SAME => f $ norm t) 
172 
 norm _ = raise SAME 

2191  173 
and normh t = norm t handle SAME => t 
1500  174 
in normh t end 
0  175 

1500  176 
and norm_term2(asol,iTs,t) : term = 
177 
let fun normT(Type(a,Ts)) = Type(a, normTs Ts) 

178 
 normT(TFree _) = raise SAME 

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

180 
Some(U) => normTh U 

181 
 None => raise SAME) 

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

183 
and normTs([]) = raise SAME 

2181  184 
 normTs(T::Ts) = ((normT T :: (normTs Ts handle SAME => Ts)) 
1500  185 
handle SAME => T :: normTs Ts) 
186 
and norm(Const(a,T)) = Const(a, normT T) 

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

188 
 norm(Var (w,T)) = 

189 
(case xsearch(asol,w) of 

190 
Some u => normh u 

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

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

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

2191  194 
 norm(Abs(_,_,body) $ t) = normh(subst_bound (t, body)) 
1500  195 
 norm(f $ t) = 
196 
((case norm f of 

2191  197 
Abs(_,_,body) => normh(subst_bound (t, body)) 
1500  198 
 nf => nf $ normh t) 
199 
handle SAME => f $ norm t) 

200 
 norm _ = raise SAME 

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

202 
in normh t end; 

0  203 

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

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

719
e3e1d1a6d408
Pure/envir/norm_term: replaced equality test for [] by null
lcp
parents:
247
diff
changeset

206 
if null iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t) 
e3e1d1a6d408
Pure/envir/norm_term: replaced equality test for [] by null
lcp
parents:
247
diff
changeset

207 

0  208 
end; 
209 