author  nipkow 
Mon, 13 Mar 1995 09:38:10 +0100  
changeset 949  83c588d6fee9 
parent 728  9a973c3ba350 
child 1029  27808dabf4af 
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 

949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

192 
fun map_type_tvar f (Type(a,Ts)) = Type(a, map (map_type_tvar f) Ts) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

193 
 map_type_tvar f (T as TFree _) = T 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

194 
 map_type_tvar f (TVar x) = f x; 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

195 

83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

196 
fun map_type_tfree f (Type(a,Ts)) = Type(a, map (map_type_tfree f) Ts) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

197 
 map_type_tfree f (TFree x) = f x 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

198 
 map_type_tfree f (T as TVar _) = T; 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

199 

0  200 
(* apply a function to all types in a term *) 
201 
fun map_term_types f = 

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

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

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

205 
 map(t as Bound _) = t 

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

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

208 
in map end; 

209 

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

211 
fun it_term_types f = 

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

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

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

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

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

217 
 iter(Bound _, a) = a 

218 
in iter end 

219 

220 

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

222 

375  223 
val logicC: class = "logic"; 
224 
val logicS: sort = [logicC]; 

225 

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

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

228 

0  229 
val propT : typ = Type("prop",[]); 
230 

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

232 

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

234 

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

236 

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

238 

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

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

241 
 strip_all_body t = t; 

242 

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

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

245 
(a,T) :: strip_all_vars t 

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

247 

248 
(*increments a term's nonlocal bound variables 

249 
required when moving a term within abstractions 

250 
inc is increment for bound variables 

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

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

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

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

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

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

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

258 

259 
fun incr_boundvars 0 t = t 

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

261 

262 

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

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

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

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

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

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

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

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

271 

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

273 

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

275 
level k or beyond. *) 

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

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

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

279 
 loose_bvar _ = false; 

280 

281 

282 
(*Substitute arguments for loose bound variables. 

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

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

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

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

287 
compensate for the disappearance of lambdas. 

288 
*) 

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

290 
let val n = length args; 

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

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

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

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

295 
 arg::_ => incr_boundvars lev arg) 

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

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

298 
 subst (t,lev) = t 

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

300 

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

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

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

304 

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

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

307 
infix aconv; 

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

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

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

311 
 (Bound i) aconv (Bound j) = i=j 

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

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

314 
 _ aconv _ = false; 

315 

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

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

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

319 
 aconvs _ = false; 

320 

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

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

323 
fun could_unify (t,u) = 

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

325 
 matchrands _ = true 

326 
in case (head_of t , head_of u) of 

327 
(_, Var _) => true 

328 
 (Var _, _) => true 

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

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

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

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

333 
 (_, Abs _) => true 

334 
 _ => false 

335 
end; 

336 

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

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

339 
 subst_free pairs = 

340 
let fun substf u = 

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

342 
Some u' => u' 

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

344 
 t$u' => substf t $ substf u' 

345 
 _ => u) 

346 
in substf end; 

347 

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

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

350 

351 

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

353 
which must contain no loose bound variables. 

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

355 
fun abstract_over (v,body) = 

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

357 
(case u of 

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

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

360 
 _ => u) 

361 
in abst(0,body) end; 

362 

363 

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

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

366 

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

368 
fun list_abs_free ([ ] , t) = t 

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

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

371 

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

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

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

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

376 

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

378 
fun list_all ([], t) = t 

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

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

381 

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

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

384 
fun subst_atomic [] t = t : term 

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

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

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

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

389 
Some u => u  None => t) 

390 
in subst t end; 

391 

728
9a973c3ba350
Pure/term: commented typ_subst_TVars, subst_TVars, subst_Vars, subst_vars
lcp
parents:
375
diff
changeset

392 
(*Substitute for type Vars in a type*) 
0  393 
fun typ_subst_TVars iTs T = if null iTs then T else 
394 
let fun subst(Type(a,Ts)) = Type(a, map subst Ts) 

395 
 subst(T as TFree _) = T 

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

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

398 
in subst T end; 

399 

728
9a973c3ba350
Pure/term: commented typ_subst_TVars, subst_TVars, subst_Vars, subst_vars
lcp
parents:
375
diff
changeset

400 
(*Substitute for type Vars in a term*) 
0  401 
val subst_TVars = map_term_types o typ_subst_TVars; 
402 

728
9a973c3ba350
Pure/term: commented typ_subst_TVars, subst_TVars, subst_Vars, subst_vars
lcp
parents:
375
diff
changeset

403 
(*Substitute for Vars in a term; see also envir/norm_term*) 
0  404 
fun subst_Vars itms t = if null itms then t else 
405 
let fun subst(v as Var(ixn,_)) = 

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

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

408 
 subst(f$t) = subst f $ subst t 

409 
 subst(t) = t 

410 
in subst t end; 

411 

728
9a973c3ba350
Pure/term: commented typ_subst_TVars, subst_TVars, subst_Vars, subst_vars
lcp
parents:
375
diff
changeset

412 
(*Substitute for type/term Vars in a term; see also envir/norm_term*) 
0  413 
fun subst_vars(iTs,itms) = if null iTs then subst_Vars itms else 
414 
let fun subst(Const(a,T)) = Const(a,typ_subst_TVars iTs T) 

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

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

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

418 
 Some t => t) 

419 
 subst(b as Bound _) = b 

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

421 
 subst(f$t) = subst f $ subst t 

422 
in subst end; 

423 

424 

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

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

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

428 
 maxidx_of_typ(TFree _) = ~1 

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

430 

431 

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

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

434 
 maxidx_of_term (Bound _) = ~1 

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

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

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

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

439 

440 

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

949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

442 
fun incr_tvar k = map_type_tvar (fn ((a,i),S) => TVar((a,i+k),S)); 
0  443 

444 

445 
(**** Syntaxrelated declarations ****) 

446 

447 

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

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

450 

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

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

453 
let val zero = ord"0" 

454 
val limit = zero+radix 

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

456 
 scan (num, c::cs) = 

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

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

459 
else (num, c::cs) 

460 
in scan(0,cs) end; 

461 

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

463 

464 

465 
(*** Printing ***) 

466 

467 

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

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

470 
fun variant bs c : string = 

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

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

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

474 

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

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

477 
 variantlist(b::bs, used) = 

478 
let val b' = variant used b 

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

480 

481 
(** TFrees and TVars **) 

482 

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

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

485 

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

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

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

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

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

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

492 
 add_term_names (_, bs) = bs; 

493 

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

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

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

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

498 

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

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

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

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

503 

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

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

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

507 

949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

508 
fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames (Ts,nms) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

509 
 add_typ_varnames(TFree(nm,_),nms) = nm ins nms 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

510 
 add_typ_varnames(TVar((nm,_),_),nms) = nm ins nms; 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

511 

0  512 
(*Accumulates the TVars in a term, suppressing duplicates. *) 
513 
val add_term_tvars = it_term_types add_typ_tvars; 

514 

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

516 
val add_term_tfrees = it_term_types add_typ_tfrees; 

517 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

518 

949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

519 
val add_term_tvarnames = it_term_types add_typ_varnames; 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

520 

0  521 
(*Nonlist versions*) 
522 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

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

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

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

526 

949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

527 
(*special code to enforce lefttoright collection of TVarindexnames*) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

528 

83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

529 
fun add_typ_ixns(ixns,Type(_,Ts)) = foldl add_typ_ixns (ixns,Ts) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

530 
 add_typ_ixns(ixns,TVar(ixn,_)) = if ixn mem ixns then ixns else ixns@[ixn] 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

531 
 add_typ_ixns(ixns,TFree(_)) = ixns; 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

532 

83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

533 
fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

534 
 add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

535 
 add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

536 
 add_term_tvar_ixns(Bound _,ixns) = ixns 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

537 
 add_term_tvar_ixns(Abs(_,T,t),ixns) = 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

538 
add_term_tvar_ixns(t,add_typ_ixns(ixns,T)) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

539 
 add_term_tvar_ixns(f$t,ixns) = 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

540 
add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns)); 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

541 

0  542 
(** Frees and Vars **) 
543 

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

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

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

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

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

549 
 atless _ = false; 

550 

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

552 
fun insert_aterm (t,us) = 

553 
let fun inserta [] = [t] 

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

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

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

557 
else u :: inserta(us') 

558 
in inserta us end; 

559 

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

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

562 
Var _ => insert_aterm(t,vars) 

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

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

565 
 _ => vars; 

566 

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

568 

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

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

571 
Free _ => insert_aterm(t,frees) 

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

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

574 
 _ => frees; 

575 

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

577 

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

579 
having a unique name. *) 

580 
fun variant_abs (a,T,P) = 

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

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

583 

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

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

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

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

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

589 

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