author  lcp 
Tue, 18 Jan 1994 15:57:40 +0100  
changeset 230  ec8a2b6aa8a7 
parent 61  f8c1922b78e3 
child 375  d7ae7ac22d48 
permissions  rwrr 
0  1 
(* Title: term.ML 
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 

216 
val propT : typ = Type("prop",[]); 

217 

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

219 

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

221 

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

223 

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

225 

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

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

228 
 strip_all_body t = t; 

229 

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

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

232 
(a,T) :: strip_all_vars t 

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

234 

235 
(*increments a term's nonlocal bound variables 

236 
required when moving a term within abstractions 

237 
inc is increment for bound variables 

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

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

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

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

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

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

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

245 

246 
fun incr_boundvars 0 t = t 

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

248 

249 

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

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

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

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

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

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

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

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

258 

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

260 

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

262 
level k or beyond. *) 

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

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

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

266 
 loose_bvar _ = false; 

267 

268 

269 
(*Substitute arguments for loose bound variables. 

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

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

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

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

274 
compensate for the disappearance of lambdas. 

275 
*) 

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

277 
let val n = length args; 

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

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

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

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

282 
 arg::_ => incr_boundvars lev arg) 

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

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

285 
 subst (t,lev) = t 

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

287 

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

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

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

291 

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

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

294 
infix aconv; 

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

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

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

298 
 (Bound i) aconv (Bound j) = i=j 

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

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

301 
 _ aconv _ = false; 

302 

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

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

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

306 
 aconvs _ = false; 

307 

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

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

310 
fun could_unify (t,u) = 

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

312 
 matchrands _ = true 

313 
in case (head_of t , head_of u) of 

314 
(_, Var _) => true 

315 
 (Var _, _) => true 

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

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

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

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

320 
 (_, Abs _) => true 

321 
 _ => false 

322 
end; 

323 

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

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

326 
 subst_free pairs = 

327 
let fun substf u = 

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

329 
Some u' => u' 

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

331 
 t$u' => substf t $ substf u' 

332 
 _ => u) 

333 
in substf end; 

334 

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

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

337 

338 

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

340 
which must contain no loose bound variables. 

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

342 
fun abstract_over (v,body) = 

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

344 
(case u of 

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

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

347 
 _ => u) 

348 
in abst(0,body) end; 

349 

350 

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

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

353 

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

355 
fun list_abs_free ([ ] , t) = t 

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

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

358 

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

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

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

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

363 

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

365 
fun list_all ([], t) = t 

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

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

368 

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

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

371 
fun subst_atomic [] t = t : term 

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

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

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

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

376 
Some u => u  None => t) 

377 
in subst t end; 

378 

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

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

381 
 subst(T as TFree _) = T 

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

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

384 
in subst T end; 

385 

386 
val subst_TVars = map_term_types o typ_subst_TVars; 

387 

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

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

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

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

392 
 subst(f$t) = subst f $ subst t 

393 
 subst(t) = t 

394 
in subst t end; 

395 

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

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

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

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

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

401 
 Some t => t) 

402 
 subst(b as Bound _) = b 

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

404 
 subst(f$t) = subst f $ subst t 

405 
in subst end; 

406 

407 

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

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

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

411 
 maxidx_of_typ(TFree _) = ~1 

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

413 

414 

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

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

417 
 maxidx_of_term (Bound _) = ~1 

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

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

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

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

422 

423 

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

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

426 
 incr_tvar k (T as TFree _) = T 

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

428 

429 

430 
(**** Syntaxrelated declarations ****) 

431 

432 

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

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

435 

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

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

438 
let val zero = ord"0" 

439 
val limit = zero+radix 

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

441 
 scan (num, c::cs) = 

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

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

444 
else (num, c::cs) 

445 
in scan(0,cs) end; 

446 

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

448 

449 

450 
(*** Printing ***) 

451 

452 

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

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

455 
fun variant bs c : string = 

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

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

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

459 

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

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

462 
 variantlist(b::bs, used) = 

463 
let val b' = variant used b 

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

465 

466 
(** TFrees and TVars **) 

467 

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

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

470 

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

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

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

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

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

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

477 
 add_term_names (_, bs) = bs; 

478 

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

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

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

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

483 

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

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

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

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

488 

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

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

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

492 

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

494 
val add_term_tvars = it_term_types add_typ_tvars; 

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

496 

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

498 
val add_term_tfrees = it_term_types add_typ_tfrees; 

499 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

500 

501 
(*Nonlist versions*) 

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

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

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

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

506 

507 
(** Frees and Vars **) 

508 

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

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

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

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

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

514 
 atless _ = false; 

515 

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

517 
fun insert_aterm (t,us) = 

518 
let fun inserta [] = [t] 

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

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

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

522 
else u :: inserta(us') 

523 
in inserta us end; 

524 

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

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

527 
Var _ => insert_aterm(t,vars) 

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

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

530 
 _ => vars; 

531 

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

533 

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

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

536 
Free _ => insert_aterm(t,frees) 

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

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

539 
 _ => frees; 

540 

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

542 

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

544 
having a unique name. *) 

545 
fun variant_abs (a,T,P) = 

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

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

548 

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

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

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

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

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

554 

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