author  wenzelm 
Tue, 11 Jul 2006 23:00:35 +0200  
changeset 20098  19871ee094b1 
parent 19861  620d90091788 
child 20548  8ef25fe585a8 
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 
10485  5 

15797  6 
Environments. The type of a term variable / sort of a type variable is 
7 
part of its name. The lookup function must apply type substitutions, 

8 
since they may change the identity of a variable. 

0  9 
*) 
10 

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

11 
signature ENVIR = 
0  12 
sig 
15797  13 
type tenv 
14 
datatype env = Envir of {asol: tenv, iTs: Type.tyenv, maxidx: int} 

15 
val type_env: env > Type.tyenv 

11513  16 
exception SAME 
10485  17 
val genvars: string > env * typ list > env * term list 
18 
val genvar: string > env * typ > env * term 

15797  19 
val lookup: env * (indexname * typ) > term option 
16652
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset

20 
val lookup': tenv * (indexname * typ) > term option 
15797  21 
val update: ((indexname * typ) * term) * env > env 
10485  22 
val empty: int > env 
23 
val is_empty: env > bool 

19861  24 
val above: env > int > bool 
15797  25 
val vupdate: ((indexname * typ) * term) * env > env 
26 
val alist_of: env > (indexname * (typ * term)) list 

10485  27 
val norm_term: env > term > term 
11513  28 
val norm_term_same: env > term > term 
15797  29 
val norm_type: Type.tyenv > typ > typ 
30 
val norm_type_same: Type.tyenv > typ > typ 

31 
val norm_types_same: Type.tyenv > typ list > typ list 

10485  32 
val beta_norm: term > term 
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

33 
val head_norm: env > term > term 
18937  34 
val eta_contract: term > term 
35 
val beta_eta_contract: term > term 

12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

36 
val fastype: env > typ list > term > typ 
15797  37 
val typ_subst_TVars: Type.tyenv > typ > typ 
38 
val subst_TVars: Type.tyenv > term > term 

39 
val subst_Vars: tenv > term > term 

40 
val subst_vars: Type.tyenv * tenv > term > term 

19422  41 
val expand_atom: typ > typ * term > term 
0  42 
end; 
43 

1500  44 
structure Envir : ENVIR = 
0  45 
struct 
46 

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

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

49 
*) 

15797  50 
type tenv = (typ * term) Vartab.table 
51 

0  52 
datatype env = Envir of 
15797  53 
{maxidx: int, (*maximum index of vars*) 
54 
asol: tenv, (*table of assignments to Vars*) 

55 
iTs: Type.tyenv} (*table of assignments to TVars*) 

0  56 

12496  57 
fun type_env (Envir {iTs, ...}) = iTs; 
0  58 

59 
(*Generate a list of distinct variables. 

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

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

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

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

64 
 genvs (n, T::Ts) = 

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

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

66 
:: genvs(n+1,Ts) 
0  67 
in (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts)) end; 
68 

69 
(*Generate a variable.*) 

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

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

71 
let val (env',[v]) = genvars name (env,[T]) 
0  72 
in (env',v) end; 
73 

15797  74 
fun var_clash ixn T T' = raise TYPE ("Variable " ^ 
75 
quote (Syntax.string_of_vname ixn) ^ " has two distinct types", 

76 
[T', T], []); 

0  77 

15797  78 
fun gen_lookup f asol (xname, T) = 
17412  79 
(case Vartab.lookup asol xname of 
15797  80 
NONE => NONE 
81 
 SOME (U, t) => if f (T, U) then SOME t 

82 
else var_clash xname T U); 

83 

16652
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset

84 
(* When dealing with environments produced by matching instead *) 
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset

85 
(* of unification, there is no need to chase assigned TVars. *) 
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset

86 
(* In this case, we can simply ignore the type substitution *) 
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset

87 
(* and use = instead of eq_type. *) 
15797  88 

16652
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset

89 
fun lookup' (asol, p) = gen_lookup op = asol p; 
15797  90 

16652
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset

91 
fun lookup2 (iTs, asol) p = 
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset

92 
if Vartab.is_empty iTs then lookup' (asol, p) 
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset

93 
else gen_lookup (Type.eq_type iTs) asol p; 
15797  94 

95 
fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p; 

96 

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

17412  98 
Envir{maxidx=maxidx, asol=Vartab.update_new (xname, (T, t)) asol, iTs=iTs}; 
0  99 

5289  100 
(*The empty environment. New variables will start with the given index+1.*) 
8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset

101 
fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty}; 
0  102 

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

103 
(*Test for empty environment*) 
8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset

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

105 

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

106 
(*Determine if the least index updated exceeds lim*) 
19861  107 
fun above (Envir {asol, iTs, ...}) lim = 
108 
(case Vartab.min_key asol of SOME (_, i) => i > lim  NONE => true) andalso 

109 
(case Vartab.min_key iTs of SOME (_, i) => i > lim  NONE => true); 

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

110 

0  111 
(*Update, checking VarVar assignments: try to suppress higher indexes*) 
15797  112 
fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of 
113 
Var (nT as (name', T)) => 

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

20098  115 
else if Term.indexname_ord (a, name') = LESS then 
15797  116 
(case lookup (env, nT) of (*if already assigned, chase*) 
117 
NONE => update ((nT, Var (a, T)), env) 

118 
 SOME u => vupdate ((aU, u), env)) 

119 
else update ((aU, t), env) 

120 
 _ => update ((aU, t), env); 

0  121 

122 

123 
(*Convert environment to alist*) 

8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset

124 
fun alist_of (Envir{asol,...}) = Vartab.dest asol; 
0  125 

126 

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

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

130 

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

132 
exception SAME; 

0  133 

11513  134 
fun norm_term1 same (asol,t) : term = 
15797  135 
let fun norm (Var wT) = 
16652
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset

136 
(case lookup' (asol, wT) of 
15531  137 
SOME u => (norm u handle SAME => u) 
138 
 NONE => raise SAME) 

10485  139 
 norm (Abs(a,T,body)) = Abs(a, T, norm body) 
140 
 norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body)) 

141 
 norm (f $ t) = 

142 
((case norm f of 

143 
Abs(_,_,body) => normh(subst_bound (t, body)) 

144 
 nf => nf $ (norm t handle SAME => t)) 

145 
handle SAME => f $ norm t) 

146 
 norm _ = raise SAME 

2191  147 
and normh t = norm t handle SAME => t 
11513  148 
in (if same then norm else normh) t end 
0  149 

11513  150 
fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts) 
151 
 normT iTs (TFree _) = raise SAME 

15797  152 
 normT iTs (TVar vS) = (case Type.lookup (iTs, vS) of 
15531  153 
SOME U => normTh iTs U 
154 
 NONE => raise SAME) 

11513  155 
and normTh iTs T = ((normT iTs T) handle SAME => T) 
156 
and normTs iTs [] = raise SAME 

157 
 normTs iTs (T :: Ts) = 

158 
((normT iTs T :: (normTs iTs Ts handle SAME => Ts)) 

159 
handle SAME => T :: normTs iTs Ts); 

160 

161 
fun norm_term2 same (asol, iTs, t) : term = 

162 
let fun norm (Const (a, T)) = Const(a, normT iTs T) 

163 
 norm (Free (a, T)) = Free(a, normT iTs T) 

164 
 norm (Var (w, T)) = 

15797  165 
(case lookup2 (iTs, asol) (w, T) of 
15531  166 
SOME u => normh u 
167 
 NONE => Var(w, normT iTs T)) 

11513  168 
 norm (Abs (a, T, body)) = 
169 
(Abs (a, normT iTs T, normh body) handle SAME => Abs (a, T, norm body)) 

170 
 norm (Abs(_, _, body) $ t) = normh (subst_bound (t, body)) 

171 
 norm (f $ t) = 

10485  172 
((case norm f of 
11513  173 
Abs(_, _, body) => normh (subst_bound (t, body)) 
10485  174 
 nf => nf $ normh t) 
175 
handle SAME => f $ norm t) 

176 
 norm _ = raise SAME 

1500  177 
and normh t = (norm t) handle SAME => t 
11513  178 
in (if same then norm else normh) t end; 
0  179 

11513  180 
fun gen_norm_term same (env as Envir{asol,iTs,...}) t : term = 
181 
if Vartab.is_empty iTs then norm_term1 same (asol, t) 

182 
else norm_term2 same (asol, iTs, t); 

183 

184 
val norm_term = gen_norm_term false; 

185 
val norm_term_same = gen_norm_term true; 

10485  186 

187 
val beta_norm = norm_term (empty 0); 

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

188 

12496  189 
fun norm_type iTs = normTh iTs; 
190 
fun norm_type_same iTs = 

11513  191 
if Vartab.is_empty iTs then raise SAME else normT iTs; 
192 

12496  193 
fun norm_types_same iTs = 
11513  194 
if Vartab.is_empty iTs then raise SAME else normTs iTs; 
195 

196 

12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

197 
(*Put a term into head normal form for unification.*) 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

198 

4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

199 
fun head_norm env t = 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

200 
let 
15797  201 
fun hnorm (Var vT) = (case lookup (env, vT) of 
15531  202 
SOME u => head_norm env u 
203 
 NONE => raise SAME) 

12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

204 
 hnorm (Abs (a, T, body)) = Abs (a, T, hnorm body) 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

205 
 hnorm (Abs (_, _, body) $ t) = 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

206 
head_norm env (subst_bound (t, body)) 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

207 
 hnorm (f $ t) = (case hnorm f of 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

208 
Abs (_, _, body) => head_norm env (subst_bound (t, body)) 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

209 
 nf => nf $ t) 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

210 
 hnorm _ = raise SAME 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

211 
in hnorm t handle SAME => t end; 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

212 

4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

213 

18937  214 
(*Etacontract a term (fully)*) 
215 

216 
fun eta_contract t = 

217 
let 

218 
exception SAME; 

219 
fun eta (Abs (a, T, body)) = 

220 
((case eta body of 

221 
body' as (f $ Bound 0) => 

222 
if loose_bvar1 (f, 0) then Abs(a, T, body') 

223 
else incr_boundvars ~1 f 

224 
 body' => Abs (a, T, body')) handle SAME => 

225 
(case body of 

226 
(f $ Bound 0) => 

227 
if loose_bvar1 (f, 0) then raise SAME 

228 
else incr_boundvars ~1 f 

229 
 _ => raise SAME)) 

230 
 eta (f $ t) = 

231 
(let val f' = eta f 

232 
in f' $ etah t end handle SAME => f $ eta t) 

233 
 eta _ = raise SAME 

234 
and etah t = (eta t handle SAME => t) 

235 
in etah t end; 

236 

237 
val beta_eta_contract = eta_contract o beta_norm; 

238 

239 

12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

240 
(*finds type of term without checking that combinations are consistent 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

241 
Ts holds types of bound variables*) 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

242 
fun fastype (Envir {iTs, ...}) = 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

243 
let val funerr = "fastype: expected function type"; 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

244 
fun fast Ts (f $ u) = 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

245 
(case fast Ts f of 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

246 
Type ("fun", [_, T]) => T 
15797  247 
 TVar ixnS => 
248 
(case Type.lookup (iTs, ixnS) of 

15531  249 
SOME (Type ("fun", [_, T])) => T 
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

250 
 _ => raise TERM (funerr, [f $ u])) 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

251 
 _ => raise TERM (funerr, [f $ u])) 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

252 
 fast Ts (Const (_, T)) = T 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

253 
 fast Ts (Free (_, T)) = T 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

254 
 fast Ts (Bound i) = 
15570  255 
(List.nth (Ts, i) 
256 
handle Subscript => raise TERM ("fastype: Bound", [Bound i])) 

12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

257 
 fast Ts (Var (_, T)) = T 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

258 
 fast Ts (Abs (_, T, u)) = T > fast (T :: Ts) u 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

259 
in fast end; 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

260 

15797  261 

262 
(*Substitute for type Vars in a type*) 

263 
fun typ_subst_TVars iTs T = if Vartab.is_empty iTs then T else 

264 
let fun subst(Type(a, Ts)) = Type(a, map subst Ts) 

265 
 subst(T as TFree _) = T 

266 
 subst(T as TVar ixnS) = 

267 
(case Type.lookup (iTs, ixnS) of NONE => T  SOME(U) => U) 

268 
in subst T end; 

269 

270 
(*Substitute for type Vars in a term*) 

271 
val subst_TVars = map_term_types o typ_subst_TVars; 

272 

273 
(*Substitute for Vars in a term *) 

274 
fun subst_Vars itms t = if Vartab.is_empty itms then t else 

18937  275 
let fun subst (v as Var ixnT) = the_default v (lookup' (itms, ixnT)) 
15797  276 
 subst (Abs (a, T, t)) = Abs (a, T, subst t) 
277 
 subst (f $ t) = subst f $ subst t 

278 
 subst t = t 

279 
in subst t end; 

280 

281 
(*Substitute for type/term Vars in a term *) 

16652
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset

282 
fun subst_vars (iTs, itms) = 
15797  283 
if Vartab.is_empty iTs then subst_Vars itms else 
284 
let fun subst (Const (a, T)) = Const(a, typ_subst_TVars iTs T) 

285 
 subst (Free (a, T)) = Free (a, typ_subst_TVars iTs T) 

16652
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset

286 
 subst (Var (ixn, T)) = (case lookup' (itms, (ixn, T)) of 
15797  287 
NONE => Var (ixn, typ_subst_TVars iTs T) 
288 
 SOME t => t) 

289 
 subst (b as Bound _) = b 

290 
 subst (Abs (a, T, t)) = Abs(a, typ_subst_TVars iTs T, subst t) 

291 
 subst (f $ t) = subst f $ subst t 

292 
in subst end; 

293 

18937  294 

295 
(* expand_atom *) 

296 

19422  297 
fun expand_atom T (U, u) = 
298 
subst_TVars (Type.raw_match (U, T) Vartab.empty) u 

18937  299 
handle Type.TYPE_MATCH => raise TYPE ("expand_atom: illtyped replacement", [T, U], [u]); 
300 

0  301 
end; 