author  wenzelm 
Sat, 14 Apr 2007 17:36:05 +0200  
changeset 22678  23963361278c 
parent 22174  f2bf6bcd4a98 
child 24670  9aae962b1d56 
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 
21695  42 
val expand_term: (term > (typ * term) option) > term > term 
21795  43 
val expand_term_frees: ((string * typ) * term) list > term > term 
0  44 
end; 
45 

1500  46 
structure Envir : ENVIR = 
0  47 
struct 
48 

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

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

51 
*) 

15797  52 
type tenv = (typ * term) Vartab.table 
53 

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

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

0  58 

12496  59 
fun type_env (Envir {iTs, ...}) = iTs; 
0  60 

61 
(*Generate a list of distinct variables. 

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

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

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

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

66 
 genvs (n, T::Ts) = 

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

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

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

71 
(*Generate a variable.*) 

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

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

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

15797  76 
fun var_clash ixn T T' = raise TYPE ("Variable " ^ 
22678  77 
quote (Term.string_of_vname ixn) ^ " has two distinct types", 
15797  78 
[T', T], []); 
0  79 

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

84 
else var_clash xname T U); 

85 

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

86 
(* 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

87 
(* 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

88 
(* 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

89 
(* and use = instead of eq_type. *) 
15797  90 

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

91 
fun lookup' (asol, p) = gen_lookup op = asol p; 
15797  92 

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

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

94 
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

95 
else gen_lookup (Type.eq_type iTs) asol p; 
15797  96 

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

98 

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

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

5289  102 
(*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

103 
fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty}; 
0  104 

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

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

106 
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

107 

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

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

111 
(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

112 

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

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

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

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

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

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

0  123 

124 

125 
(*Convert environment to alist*) 

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

126 
fun alist_of (Envir{asol,...}) = Vartab.dest asol; 
0  127 

128 

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

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

132 

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

134 
exception SAME; 

0  135 

11513  136 
fun norm_term1 same (asol,t) : term = 
15797  137 
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

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

10485  141 
 norm (Abs(a,T,body)) = Abs(a, T, norm body) 
142 
 norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body)) 

143 
 norm (f $ t) = 

144 
((case norm f of 

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

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

147 
handle SAME => f $ norm t) 

148 
 norm _ = raise SAME 

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

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

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

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

159 
 normTs iTs (T :: Ts) = 

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

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

162 

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

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

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

166 
 norm (Var (w, T)) = 

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

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

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

173 
 norm (f $ t) = 

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

178 
 norm _ = raise SAME 

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

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

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

185 

186 
val norm_term = gen_norm_term false; 

187 
val norm_term_same = gen_norm_term true; 

10485  188 

189 
val beta_norm = norm_term (empty 0); 

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

190 

12496  191 
fun norm_type iTs = normTh iTs; 
192 
fun norm_type_same iTs = 

11513  193 
if Vartab.is_empty iTs then raise SAME else normT iTs; 
194 

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

198 

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

199 
(*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

200 

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

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

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

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

206 
 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

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

208 
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 
 hnorm (f $ t) = (case hnorm f of 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

210 
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

211 
 nf => nf $ t) 
20670  212 
 hnorm _ = raise SAME 
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

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

214 

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

215 

18937  216 
(*Etacontract a term (fully)*) 
217 

22174  218 
local 
219 

220 
fun decr lev (Bound i) = if i >= lev then Bound (i  1) else raise SAME 

221 
 decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body) 

222 
 decr lev (t $ u) = (decr lev t $ decrh lev u handle SAME => t $ decr lev u) 

223 
 decr _ _ = raise SAME 

224 
and decrh lev t = (decr lev t handle SAME => t); 

20670  225 

22174  226 
fun eta (Abs (a, T, body)) = 
227 
((case eta body of 

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

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

230 
else decrh 0 f 

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

232 
(case body of 

233 
f $ Bound 0 => 

234 
if loose_bvar1 (f, 0) then raise SAME 

235 
else decrh 0 f 

236 
 _ => raise SAME)) 

237 
 eta (t $ u) = (eta t $ etah u handle SAME => t $ eta u) 

238 
 eta _ = raise SAME 

239 
and etah t = (eta t handle SAME => t); 

240 

241 
fun has_abs (Abs _) = true 

242 
 has_abs (t $ u) = has_abs t orelse has_abs u 

243 
 has_abs _ = false; 

244 

245 
in 

246 

247 
fun eta_contract t = 

248 
if has_abs t then etah t else t; 

18937  249 

250 
val beta_eta_contract = eta_contract o beta_norm; 

251 

22174  252 
end; 
253 

18937  254 

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

255 
(*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

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

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

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

259 
fun fast Ts (f $ u) = 
20670  260 
(case fast Ts f of 
261 
Type ("fun", [_, T]) => T 

262 
 TVar ixnS => 

263 
(case Type.lookup (iTs, ixnS) of 

264 
SOME (Type ("fun", [_, T])) => T 

265 
 _ => raise TERM (funerr, [f $ u])) 

266 
 _ => raise TERM (funerr, [f $ u])) 

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

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

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

269 
 fast Ts (Bound i) = 
20670  270 
(List.nth (Ts, i) 
271 
handle Subscript => raise TERM ("fastype: Bound", [Bound i])) 

272 
 fast Ts (Var (_, T)) = T 

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

273 
 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

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

275 

15797  276 

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

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

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

280 
 subst(T as TFree _) = T 

281 
 subst(T as TVar ixnS) = 

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

283 
in subst T end; 

284 

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

20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20098
diff
changeset

286 
val subst_TVars = map_types o typ_subst_TVars; 
15797  287 

288 
(*Substitute for Vars in a term *) 

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

18937  290 
let fun subst (v as Var ixnT) = the_default v (lookup' (itms, ixnT)) 
15797  291 
 subst (Abs (a, T, t)) = Abs (a, T, subst t) 
292 
 subst (f $ t) = subst f $ subst t 

293 
 subst t = t 

294 
in subst t end; 

295 

296 
(*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

297 
fun subst_vars (iTs, itms) = 
15797  298 
if Vartab.is_empty iTs then subst_Vars itms else 
299 
let fun subst (Const (a, T)) = Const(a, typ_subst_TVars iTs T) 

300 
 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

301 
 subst (Var (ixn, T)) = (case lookup' (itms, (ixn, T)) of 
15797  302 
NONE => Var (ixn, typ_subst_TVars iTs T) 
303 
 SOME t => t) 

304 
 subst (b as Bound _) = b 

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

306 
 subst (f $ t) = subst f $ subst t 

307 
in subst end; 

308 

18937  309 

21795  310 
(* expand defined atoms  with local beta reduction *) 
18937  311 

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

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

21795  316 
fun expand_term get = 
21695  317 
let 
318 
fun expand tm = 

319 
let 

320 
val (head, args) = Term.strip_comb tm; 

321 
val args' = map expand args; 

322 
fun comb head' = Term.list_comb (head', args'); 

323 
in 

324 
(case head of 

325 
Abs (x, T, t) => comb (Abs (x, T, expand t)) 

326 
 _ => 

21795  327 
(case get head of 
21695  328 
SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args') 
329 
 NONE => comb head) 

330 
 _ => comb head) 

331 
end; 

332 
in expand end; 

333 

21795  334 
fun expand_term_frees defs = 
335 
let 

336 
val eqs = map (fn ((x, U), u) => (x, (U, u))) defs; 

337 
val get = fn Free (x, _) => AList.lookup (op =) eqs x  _ => NONE; 

338 
in expand_term get end; 

339 

0  340 
end; 