author  lcp 
Tue, 21 Jun 1994 17:20:34 +0200  
changeset 435  ca5356bd315a 
parent 375  d7ae7ac22d48 
child 728  9a973c3ba350 
permissions  rwrr 
375  1 
(* Title: Pure/term.ML 
0  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright Cambridge University 1992 

5 
*) 

6 

7 

8 
(*Simply typed lambdacalculus: types, terms, and basic operations*) 

9 

10 

11 
(*Indexnames can be quickly renamed by adding an offset to the integer part, 

12 
for resolution.*) 

13 
type indexname = string*int; 

14 

15 
(* Types are classified by classes. *) 

16 
type class = string; 

17 
type sort = class list; 

18 

19 
(* The sorts attached to TFrees and TVars specify the sort of that variable *) 

20 
datatype typ = Type of string * typ list 

21 
 TFree of string * sort 

22 
 TVar of indexname * sort; 

23 

24 
infixr 5 >; 

25 
fun S > T = Type("fun",[S,T]); 

26 

27 
(*handy for multiple args: [T1,...,Tn]>T gives T1>(T2> ... >T)*) 

28 
infixr >; 

29 
val op > = foldr (op >); 

30 

31 

32 
(*terms. Bound variables are indicated by depth number. 

33 
Free variables, (scheme) variables and constants have names. 

34 
An term is "closed" if there every bound variable of level "lev" 

35 
is enclosed by at least "lev" abstractions. 

36 

37 
It is possible to create meaningless terms containing loose bound vars 

38 
or type mismatches. But such terms are not allowed in rules. *) 

39 

40 

41 

42 
infix 9 $; (*application binds tightly!*) 

43 
datatype term = 

44 
Const of string * typ 

45 
 Free of string * typ 

46 
 Var of indexname * typ 

47 
 Bound of int 

48 
 Abs of string*typ*term 

49 
 op $ of term*term; 

50 

51 

52 
(*For errors involving type mismatches*) 

53 
exception TYPE of string * typ list * term list; 

54 

40
3f9f8395519e
added raise_type: string > typ list > term list > 'a;
wenzelm
parents:
0
diff
changeset

55 
fun raise_type msg tys ts = raise TYPE (msg, tys, ts); 
3f9f8395519e
added raise_type: string > typ list > term list > 'a;
wenzelm
parents:
0
diff
changeset

56 

0  57 
(*For system errors involving terms*) 
58 
exception TERM of string * term list; 

59 

40
3f9f8395519e
added raise_type: string > typ list > term list > 'a;
wenzelm
parents:
0
diff
changeset

60 
fun raise_term msg ts = raise TERM (msg, ts); 
3f9f8395519e
added raise_type: string > typ list > term list > 'a;
wenzelm
parents:
0
diff
changeset

61 

0  62 

63 
(*Note variable naming conventions! 

64 
a,b,c: string 

65 
f,g,h: functions (including terms of function type) 

66 
i,j,m,n: int 

67 
t,u: term 

68 
v,w: indexnames 

69 
x,y: any 

70 
A,B,C: term (denoting formulae) 

71 
T,U: typ 

72 
*) 

73 

74 

75 
(** Discriminators **) 

76 

77 
fun is_Const (Const _) = true 

78 
 is_Const _ = false; 

79 

80 
fun is_Free (Free _) = true 

81 
 is_Free _ = false; 

82 

83 
fun is_Var (Var _) = true 

84 
 is_Var _ = false; 

85 

86 
fun is_TVar (TVar _) = true 

87 
 is_TVar _ = false; 

88 

89 
(** Destructors **) 

90 

91 
fun dest_Const (Const x) = x 

92 
 dest_Const t = raise TERM("dest_Const", [t]); 

93 

94 
fun dest_Free (Free x) = x 

95 
 dest_Free t = raise TERM("dest_Free", [t]); 

96 

97 
fun dest_Var (Var x) = x 

98 
 dest_Var t = raise TERM("dest_Var", [t]); 

99 

100 

101 
(* maps [T1,...,Tn]>T to the list [T1,T2,...,Tn]*) 

102 
fun binder_types (Type("fun",[S,T])) = S :: binder_types T 

103 
 binder_types _ = []; 

104 

105 
(* maps [T1,...,Tn]>T to T*) 

106 
fun body_type (Type("fun",[S,T])) = body_type T 

107 
 body_type T = T; 

108 

109 
(* maps [T1,...,Tn]>T to ([T1,T2,...,Tn], T) *) 

110 
fun strip_type T : typ list * typ = 

111 
(binder_types T, body_type T); 

112 

113 

114 
(*Compute the type of the term, checking that combinations are welltyped 

115 
Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*) 

116 
fun type_of1 (Ts, Const (_,T)) = T 

117 
 type_of1 (Ts, Free (_,T)) = T 

118 
 type_of1 (Ts, Bound i) = (nth_elem (i,Ts) 

119 
handle LIST _ => raise TYPE("type_of: bound variable", [], [Bound i])) 

120 
 type_of1 (Ts, Var (_,T)) = T 

121 
 type_of1 (Ts, Abs (_,T,body)) = T > type_of1(T::Ts, body) 

122 
 type_of1 (Ts, f$u) = 

123 
let val U = type_of1(Ts,u) 

124 
and T = type_of1(Ts,f) 

125 
in case T of 

126 
Type("fun",[T1,T2]) => 

127 
if T1=U then T2 else raise TYPE 

128 
("type_of: type mismatch in application", [T1,U], [f$u]) 

129 
 _ => raise TYPE ("type_of: Rator must have function type", 

130 
[T,U], [f$u]) 

131 
end; 

132 

133 
fun type_of t : typ = type_of1 ([],t); 

134 

135 
(*Determines the type of a term, with minimal checking*) 

61  136 
fun fastype_of1 (Ts, f$u) = 
137 
(case fastype_of1 (Ts,f) of 

0  138 
Type("fun",[_,T]) => T 
139 
 _ => raise TERM("fastype_of: expected function type", [f$u])) 

61  140 
 fastype_of1 (_, Const (_,T)) = T 
141 
 fastype_of1 (_, Free (_,T)) = T 

142 
 fastype_of1 (Ts, Bound i) = (nth_elem(i,Ts) 

0  143 
handle LIST _ => raise TERM("fastype_of: Bound", [Bound i])) 
61  144 
 fastype_of1 (_, Var (_,T)) = T 
145 
 fastype_of1 (Ts, Abs (_,T,u)) = T > fastype_of1 (T::Ts, u); 

146 

147 
fun fastype_of t : typ = fastype_of1 ([],t); 

0  148 

149 

150 
(* maps (x1,...,xn)t to t *) 

151 
fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t 

152 
 strip_abs_body u = u; 

153 

154 

155 
(* maps (x1,...,xn)t to [x1, ..., xn] *) 

156 
fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t 

157 
 strip_abs_vars u = [] : (string*typ) list; 

158 

159 

160 
fun strip_qnt_body qnt = 

161 
let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm 

162 
 strip t = t 

163 
in strip end; 

164 

165 
fun strip_qnt_vars qnt = 

166 
let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else [] 

167 
 strip t = [] : (string*typ) list 

168 
in strip end; 

169 

170 

171 
(* maps (f, [t1,...,tn]) to f(t1,...,tn) *) 

172 
val list_comb : term * term list > term = foldl (op $); 

173 

174 

175 
(* maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tailrecursive*) 

176 
fun strip_comb u : term * term list = 

177 
let fun stripc (f$t, ts) = stripc (f, t::ts) 

178 
 stripc x = x 

179 
in stripc(u,[]) end; 

180 

181 

182 
(* maps f(t1,...,tn) to f , which is never a combination *) 

183 
fun head_of (f$t) = head_of f 

184 
 head_of u = u; 

185 

186 

187 
(*Number of atoms and abstractions in a term*) 

188 
fun size_of_term (Abs (_,_,body)) = 1 + size_of_term body 

189 
 size_of_term (f$t) = size_of_term f + size_of_term t 

190 
 size_of_term _ = 1; 

191 

192 

193 
(* apply a function to all types in a term *) 

194 
fun map_term_types f = 

195 
let fun map(Const(a,T)) = Const(a, f T) 

196 
 map(Free(a,T)) = Free(a, f T) 

197 
 map(Var(v,T)) = Var(v, f T) 

198 
 map(t as Bound _) = t 

199 
 map(Abs(a,T,t)) = Abs(a, f T, map t) 

200 
 map(f$t) = map f $ map t; 

201 
in map end; 

202 

203 
(* iterate a function over all types in a term *) 

204 
fun it_term_types f = 

205 
let fun iter(Const(_,T), a) = f(T,a) 

206 
 iter(Free(_,T), a) = f(T,a) 

207 
 iter(Var(_,T), a) = f(T,a) 

208 
 iter(Abs(_,T,t), a) = iter(t,f(T,a)) 

209 
 iter(f$u, a) = iter(f, iter(u, a)) 

210 
 iter(Bound _, a) = a 

211 
in iter end 

212 

213 

214 
(** Connectives of higher order logic **) 

215 

375  216 
val logicC: class = "logic"; 
217 
val logicS: sort = [logicC]; 

218 

219 
fun itselfT ty = Type ("itself", [ty]); 

220 
val a_itselfT = itselfT (TFree ("'a", logicS)); 

221 

0  222 
val propT : typ = Type("prop",[]); 
223 

224 
val implies = Const("==>", propT>propT>propT); 

225 

226 
fun all T = Const("all", (T>propT)>propT); 

227 

228 
fun equals T = Const("==", T>T>propT); 

229 

230 
fun flexpair T = Const("=?=", T>T>propT); 

231 

232 
(* maps !!x1...xn. t to t *) 

233 
fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t 

234 
 strip_all_body t = t; 

235 

236 
(* maps !!x1...xn. t to [x1, ..., xn] *) 

237 
fun strip_all_vars (Const("all",_)$Abs(a,T,t)) = 

238 
(a,T) :: strip_all_vars t 

239 
 strip_all_vars t = [] : (string*typ) list; 

240 

241 
(*increments a term's nonlocal bound variables 

242 
required when moving a term within abstractions 

243 
inc is increment for bound variables 

244 
lev is level at which a bound variable is considered 'loose'*) 

245 
fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u 

246 
 incr_bv (inc, lev, Abs(a,T,body)) = 

247 
Abs(a, T, incr_bv(inc,lev+1,body)) 

248 
 incr_bv (inc, lev, f$t) = 

249 
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 

250 
 incr_bv (inc, lev, u) = u; 

251 

252 
fun incr_boundvars 0 t = t 

253 
 incr_boundvars inc t = incr_bv(inc,0,t); 

254 

255 

256 
(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond. 

257 
(Bound 0) is loose at level 0 *) 

258 
fun add_loose_bnos (Bound i, lev, js) = 

259 
if i<lev then js else (ilev) :: js 

260 
 add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js) 

261 
 add_loose_bnos (f$t, lev, js) = 

262 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 

263 
 add_loose_bnos (_, _, js) = js; 

264 

265 
fun loose_bnos t = add_loose_bnos (t, 0, []); 

266 

267 
(* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to 

268 
level k or beyond. *) 

269 
fun loose_bvar(Bound i,k) = i >= k 

270 
 loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k) 

271 
 loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1) 

272 
 loose_bvar _ = false; 

273 

274 

275 
(*Substitute arguments for loose bound variables. 

276 
Betareduction of arg(n1)...arg0 into t replacing (Bound i) with (argi). 

277 
Note that for ((x,y)c)(a,b), the bound vars in c are x=1 and y=0 

278 
and the appropriate call is subst_bounds([b,a], c) . 

279 
Loose bound variables >=n are reduced by "n" to 

280 
compensate for the disappearance of lambdas. 

281 
*) 

282 
fun subst_bounds (args: term list, t) : term = 

283 
let val n = length args; 

284 
fun subst (t as Bound i, lev) = 

285 
if i<lev then t (*var is locally bound*) 

286 
else (case (drop (ilev,args)) of 

287 
[] => Bound(in) (*loose: change it*) 

288 
 arg::_ => incr_boundvars lev arg) 

289 
 subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1)) 

290 
 subst (f$t, lev) = subst(f,lev) $ subst(t,lev) 

291 
 subst (t,lev) = t 

292 
in case args of [] => t  _ => subst (t,0) end; 

293 

294 
(*betareduce if possible, else form application*) 

295 
fun betapply (Abs(_,_,t), u) = subst_bounds([u],t) 

296 
 betapply (f,u) = f$u; 

297 

298 
(*Tests whether 2 terms are alphaconvertible and have same type. 

299 
Note that constants and Vars may have more than one type.*) 

300 
infix aconv; 

301 
fun (Const(a,T)) aconv (Const(b,U)) = a=b andalso T=U 

302 
 (Free(a,T)) aconv (Free(b,U)) = a=b andalso T=U 

303 
 (Var(v,T)) aconv (Var(w,U)) = v=w andalso T=U 

304 
 (Bound i) aconv (Bound j) = i=j 

305 
 (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u andalso T=U 

306 
 (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u) 

307 
 _ aconv _ = false; 

308 

309 
(*are two term lists alphaconvertible in corresponding elements?*) 

310 
fun aconvs ([],[]) = true 

311 
 aconvs (t::ts, u::us) = t aconv u andalso aconvs(ts,us) 

312 
 aconvs _ = false; 

313 

314 
(*A fast unification filter: true unless the two terms cannot be unified. 

315 
Terms must be NORMAL. Treats all Vars as distinct. *) 

316 
fun could_unify (t,u) = 

317 
let fun matchrands (f$t, g$u) = could_unify(t,u) andalso matchrands(f,g) 

318 
 matchrands _ = true 

319 
in case (head_of t , head_of u) of 

320 
(_, Var _) => true 

321 
 (Var _, _) => true 

322 
 (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u) 

323 
 (Free(a,_), Free(b,_)) => a=b andalso matchrands(t,u) 

324 
 (Bound i, Bound j) => i=j andalso matchrands(t,u) 

325 
 (Abs _, _) => true (*because of possible eta equality*) 

326 
 (_, Abs _) => true 

327 
 _ => false 

328 
end; 

329 

330 
(*Substitute new for free occurrences of old in a term*) 

331 
fun subst_free [] = (fn t=>t) 

332 
 subst_free pairs = 

333 
let fun substf u = 

334 
case gen_assoc (op aconv) (pairs, u) of 

335 
Some u' => u' 

336 
 None => (case u of Abs(a,T,t) => Abs(a, T, substf t) 

337 
 t$u' => substf t $ substf u' 

338 
 _ => u) 

339 
in substf end; 

340 

341 
(*a total, irreflexive ordering on index names*) 

342 
fun xless ((a,i), (b,j): indexname) = i<j orelse (i=j andalso a<b); 

343 

344 

345 
(*Abstraction of the term "body" over its occurrences of v, 

346 
which must contain no loose bound variables. 

347 
The resulting term is ready to become the body of an Abs.*) 

348 
fun abstract_over (v,body) = 

349 
let fun abst (lev,u) = if (v aconv u) then (Bound lev) else 

350 
(case u of 

351 
Abs(a,T,t) => Abs(a, T, abst(lev+1, t)) 

352 
 f$rand => abst(lev,f) $ abst(lev,rand) 

353 
 _ => u) 

354 
in abst(0,body) end; 

355 

356 

357 
(*Form an abstraction over a free variable.*) 

358 
fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body)); 

359 

360 
(*Abstraction over a list of free variables*) 

361 
fun list_abs_free ([ ] , t) = t 

362 
 list_abs_free ((a,T)::vars, t) = 

363 
absfree(a, T, list_abs_free(vars,t)); 

364 

365 
(*Quantification over a list of free variables*) 

366 
fun list_all_free ([], t: term) = t 

367 
 list_all_free ((a,T)::vars, t) = 

368 
(all T) $ (absfree(a, T, list_all_free(vars,t))); 

369 

370 
(*Quantification over a list of variables (already bound in body) *) 

371 
fun list_all ([], t) = t 

372 
 list_all ((a,T)::vars, t) = 

373 
(all T) $ (Abs(a, T, list_all(vars,t))); 

374 

375 
(*Replace the ATOMIC term ti by ui; instl = [(t1,u1), ..., (tn,un)]. 

376 
A simultaneous substitution: [ (a,b), (b,a) ] swaps a and b. *) 

377 
fun subst_atomic [] t = t : term 

378 
 subst_atomic (instl: (term*term) list) t = 

379 
let fun subst (Abs(a,T,body)) = Abs(a, T, subst body) 

380 
 subst (f$t') = subst f $ subst t' 

381 
 subst t = (case assoc(instl,t) of 

382 
Some u => u  None => t) 

383 
in subst t end; 

384 

385 
fun typ_subst_TVars iTs T = if null iTs then T else 

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

387 
 subst(T as TFree _) = T 

388 
 subst(T as TVar(ixn,_)) = 

389 
(case assoc(iTs,ixn) of None => T  Some(U) => U) 

390 
in subst T end; 

391 

392 
val subst_TVars = map_term_types o typ_subst_TVars; 

393 

394 
fun subst_Vars itms t = if null itms then t else 

395 
let fun subst(v as Var(ixn,_)) = 

396 
(case assoc(itms,ixn) of None => v  Some t => t) 

397 
 subst(Abs(a,T,t)) = Abs(a,T,subst t) 

398 
 subst(f$t) = subst f $ subst t 

399 
 subst(t) = t 

400 
in subst t end; 

401 

402 
fun subst_vars(iTs,itms) = if null iTs then subst_Vars itms else 

403 
let fun subst(Const(a,T)) = Const(a,typ_subst_TVars iTs T) 

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

405 
 subst(v as Var(ixn,T)) = (case assoc(itms,ixn) of 

406 
None => Var(ixn,typ_subst_TVars iTs T) 

407 
 Some t => t) 

408 
 subst(b as Bound _) = b 

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

410 
 subst(f$t) = subst f $ subst t 

411 
in subst end; 

412 

413 

414 
(*Computing the maximum index of a typ*) 

415 
fun maxidx_of_typ(Type(_,Ts)) = 

416 
if Ts=[] then ~1 else max(map maxidx_of_typ Ts) 

417 
 maxidx_of_typ(TFree _) = ~1 

418 
 maxidx_of_typ(TVar((_,i),_)) = i; 

419 

420 

421 
(*Computing the maximum index of a term*) 

422 
fun maxidx_of_term (Const(_,T)) = maxidx_of_typ T 

423 
 maxidx_of_term (Bound _) = ~1 

424 
 maxidx_of_term (Free(_,T)) = maxidx_of_typ T 

425 
 maxidx_of_term (Var ((_,i), T)) = max[i, maxidx_of_typ T] 

426 
 maxidx_of_term (Abs (_,T,body)) = max[maxidx_of_term body, maxidx_of_typ T] 

427 
 maxidx_of_term (f$t) = max [maxidx_of_term f, maxidx_of_term t]; 

428 

429 

430 
(* Increment the index of all Poly's in T by k *) 

431 
fun incr_tvar k (Type(a,Ts)) = Type(a, map (incr_tvar k) Ts) 

432 
 incr_tvar k (T as TFree _) = T 

433 
 incr_tvar k (TVar((a,i),rs)) = TVar((a,i+k),rs); 

434 

435 

436 
(**** Syntaxrelated declarations ****) 

437 

438 

439 
(*Dummy type for parsing. Will be replaced during type inference. *) 

440 
val dummyT = Type("dummy",[]); 

441 

442 
(*scan a numeral of the given radix, normally 10*) 

443 
fun scan_radixint (radix: int, cs) : int * string list = 

444 
let val zero = ord"0" 

445 
val limit = zero+radix 

446 
fun scan (num,[]) = (num,[]) 

447 
 scan (num, c::cs) = 

448 
if zero <= ord c andalso ord c < limit 

449 
then scan(radix*num + ord c  zero, cs) 

450 
else (num, c::cs) 

451 
in scan(0,cs) end; 

452 

453 
fun scan_int cs = scan_radixint(10,cs); 

454 

455 

456 
(*** Printing ***) 

457 

458 

459 
(*Makes a variant of the name c distinct from the names in bs. 

460 
First attaches the suffix "a" and then increments this. *) 

461 
fun variant bs c : string = 

462 
let fun vary2 c = if (c mem bs) then vary2 (bump_string c) else c 

463 
fun vary1 c = if (c mem bs) then vary2 (c ^ "a") else c 

464 
in vary1 (if c="" then "u" else c) end; 

465 

466 
(*Create variants of the list of names, with priority to the first ones*) 

467 
fun variantlist ([], used) = [] 

468 
 variantlist(b::bs, used) = 

469 
let val b' = variant used b 

470 
in b' :: variantlist (bs, b'::used) end; 

471 

472 
(** TFrees and TVars **) 

473 

474 
(*maps (bs,v) to v'::bs this reverses the identifiers bs*) 

475 
fun add_new_id (bs, c) : string list = variant bs c :: bs; 

476 

477 
(*Accumulates the names in the term, suppressing duplicates. 

478 
Includes Frees and Consts. For choosing unambiguous bound var names.*) 

479 
fun add_term_names (Const(a,_), bs) = a ins bs 

480 
 add_term_names (Free(a,_), bs) = a ins bs 

481 
 add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) 

482 
 add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) 

483 
 add_term_names (_, bs) = bs; 

484 

485 
(*Accumulates the TVars in a type, suppressing duplicates. *) 

486 
fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars (Ts,vs) 

487 
 add_typ_tvars(TFree(_),vs) = vs 

488 
 add_typ_tvars(TVar(v),vs) = v ins vs; 

489 

490 
(*Accumulates the TFrees in a type, suppressing duplicates. *) 

491 
fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names (Ts,fs) 

492 
 add_typ_tfree_names(TFree(f,_),fs) = f ins fs 

493 
 add_typ_tfree_names(TVar(_),fs) = fs; 

494 

495 
fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees (Ts,fs) 

496 
 add_typ_tfrees(TFree(f),fs) = f ins fs 

497 
 add_typ_tfrees(TVar(_),fs) = fs; 

498 

499 
(*Accumulates the TVars in a term, suppressing duplicates. *) 

500 
val add_term_tvars = it_term_types add_typ_tvars; 

501 
val add_term_tvar_ixns = (map #1) o (it_term_types add_typ_tvars); 

502 

503 
(*Accumulates the TFrees in a term, suppressing duplicates. *) 

504 
val add_term_tfrees = it_term_types add_typ_tfrees; 

505 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

506 

507 
(*Nonlist versions*) 

508 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

509 
fun typ_tvars T = add_typ_tvars(T,[]); 

510 
fun term_tfrees t = add_term_tfrees(t,[]); 

511 
fun term_tvars t = add_term_tvars(t,[]); 

512 

513 
(** Frees and Vars **) 

514 

515 
(*a partial ordering (not reflexive) for atomic terms*) 

516 
fun atless (Const (a,_), Const (b,_)) = a<b 

517 
 atless (Free (a,_), Free (b,_)) = a<b 

518 
 atless (Var(v,_), Var(w,_)) = xless(v,w) 

519 
 atless (Bound i, Bound j) = i<j 

520 
 atless _ = false; 

521 

522 
(*insert atomic term into partially sorted list, suppressing duplicates (?)*) 

523 
fun insert_aterm (t,us) = 

524 
let fun inserta [] = [t] 

525 
 inserta (us as u::us') = 

526 
if atless(t,u) then t::us 

527 
else if t=u then us (*duplicate*) 

528 
else u :: inserta(us') 

529 
in inserta us end; 

530 

531 
(*Accumulates the Vars in the term, suppressing duplicates*) 

532 
fun add_term_vars (t, vars: term list) = case t of 

533 
Var _ => insert_aterm(t,vars) 

534 
 Abs (_,_,body) => add_term_vars(body,vars) 

535 
 f$t => add_term_vars (f, add_term_vars(t, vars)) 

536 
 _ => vars; 

537 

538 
fun term_vars t = add_term_vars(t,[]); 

539 

540 
(*Accumulates the Frees in the term, suppressing duplicates*) 

541 
fun add_term_frees (t, frees: term list) = case t of 

542 
Free _ => insert_aterm(t,frees) 

543 
 Abs (_,_,body) => add_term_frees(body,frees) 

544 
 f$t => add_term_frees (f, add_term_frees(t, frees)) 

545 
 _ => frees; 

546 

547 
fun term_frees t = add_term_frees(t,[]); 

548 

549 
(*Given an abstraction over P, replaces the bound variable by a Free variable 

550 
having a unique name. *) 

551 
fun variant_abs (a,T,P) = 

552 
let val b = variant (add_term_names(P,[])) a 

553 
in (b, subst_bounds ([Free(b,T)], P)) end; 

554 

555 
(* renames and reverses the strings in vars away from names *) 

556 
fun rename_aTs names vars : (string*typ)list = 

557 
let fun rename_aT (vars,(a,T)) = 

558 
(variant (map #1 vars @ names) a, T) :: vars 

559 
in foldl rename_aT ([],vars) end; 

560 

561 
fun rename_wrt_term t = rename_aTs (add_term_names(t,[])); 