author  paulson 
Wed, 30 Oct 1996 11:19:09 +0100  
changeset 2138  056dead45ae8 
parent 1460  5a6f2aabd538 
child 2146  6854b692f1fe 
permissions  rwrr 
1460  1 
(* Title: Pure/term.ML 
0  2 
ID: $Id$ 
1460  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright Cambridge University 1992 
1364
8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1029
diff
changeset

5 

8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1029
diff
changeset

6 
Simply typed lambdacalculus: types, terms, and basic operations 
0  7 
*) 
8 

1364
8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1029
diff
changeset

9 
infix 9 $; 
8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1029
diff
changeset

10 
infixr 5 >; 
8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1029
diff
changeset

11 
infixr >; 
8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1029
diff
changeset

12 
infix aconv; 
8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1029
diff
changeset

13 

0  14 

1364
8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1029
diff
changeset

15 
structure Term = 
8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1029
diff
changeset

16 
struct 
0  17 

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

19 
for resolution.*) 

20 
type indexname = string*int; 

21 

22 
(* Types are classified by classes. *) 

23 
type class = string; 

24 
type sort = class list; 

25 

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

27 
datatype typ = Type of string * typ list 

28 
 TFree of string * sort 

1460  29 
 TVar of indexname * sort; 
0  30 

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

32 

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

34 
val op > = foldr (op >); 

35 

36 

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

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

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

40 
is enclosed by at least "lev" abstractions. 

41 

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

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

44 

45 

46 

47 
datatype term = 

48 
Const of string * typ 

49 
 Free of string * typ 

50 
 Var of indexname * typ 

51 
 Bound of int 

52 
 Abs of string*typ*term 

53 
 op $ of term*term; 

54 

55 

56 
(*For errors involving type mismatches*) 

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

58 

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

59 
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

60 

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

63 

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

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

65 

0  66 

67 
(*Note variable naming conventions! 

68 
a,b,c: string 

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

70 
i,j,m,n: int 

71 
t,u: term 

72 
v,w: indexnames 

73 
x,y: any 

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

75 
T,U: typ 

76 
*) 

77 

78 

79 
(** Discriminators **) 

80 

81 
fun is_Const (Const _) = true 

82 
 is_Const _ = false; 

83 

84 
fun is_Free (Free _) = true 

85 
 is_Free _ = false; 

86 

87 
fun is_Var (Var _) = true 

88 
 is_Var _ = false; 

89 

90 
fun is_TVar (TVar _) = true 

91 
 is_TVar _ = false; 

92 

93 
(** Destructors **) 

94 

95 
fun dest_Const (Const x) = x 

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

97 

98 
fun dest_Free (Free x) = x 

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

100 

101 
fun dest_Var (Var x) = x 

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

103 

104 

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

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

107 
 binder_types _ = []; 

108 

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

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

111 
 body_type T = T; 

112 

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

114 
fun strip_type T : typ list * typ = 

115 
(binder_types T, body_type T); 

116 

117 

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

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

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

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

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

1460  123 
handle LIST _ => raise TYPE("type_of: bound variable", [], [Bound i])) 
0  124 
 type_of1 (Ts, Var (_,T)) = T 
125 
 type_of1 (Ts, Abs (_,T,body)) = T > type_of1(T::Ts, body) 

126 
 type_of1 (Ts, f$u) = 

127 
let val U = type_of1(Ts,u) 

128 
and T = type_of1(Ts,f) 

129 
in case T of 

1460  130 
Type("fun",[T1,T2]) => 
131 
if T1=U then T2 else raise TYPE 

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

133 
 _ => raise TYPE 

134 
("type_of: function type is expected in application", 

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

0  136 
end; 
137 

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

139 

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

61  141 
fun fastype_of1 (Ts, f$u) = 
142 
(case fastype_of1 (Ts,f) of 

1460  143 
Type("fun",[_,T]) => T 
144 
 _ => raise TERM("fastype_of: expected function type", [f$u])) 

61  145 
 fastype_of1 (_, Const (_,T)) = T 
146 
 fastype_of1 (_, Free (_,T)) = T 

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

1460  148 
handle LIST _ => raise TERM("fastype_of: Bound", [Bound i])) 
61  149 
 fastype_of1 (_, Var (_,T)) = T 
150 
 fastype_of1 (Ts, Abs (_,T,u)) = T > fastype_of1 (T::Ts, u); 

151 

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

0  153 

154 

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

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

157 
 strip_abs_body u = u; 

158 

159 

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

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

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

163 

164 

165 
fun strip_qnt_body qnt = 

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

167 
 strip t = t 

168 
in strip end; 

169 

170 
fun strip_qnt_vars qnt = 

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

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

173 
in strip end; 

174 

175 

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

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

178 

179 

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

181 
fun strip_comb u : term * term list = 

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

183 
 stripc x = x 

184 
in stripc(u,[]) end; 

185 

186 

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

188 
fun head_of (f$t) = head_of f 

189 
 head_of u = u; 

190 

191 

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

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

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

195 
 size_of_term _ = 1; 

196 

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

197 
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

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

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

200 

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

201 
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

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

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

204 

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

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

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

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

210 
 map(t as Bound _) = t 

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

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

213 
in map end; 

214 

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

216 
fun it_term_types f = 

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

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

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

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

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

222 
 iter(Bound _, a) = a 

223 
in iter end 

224 

225 

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

227 

375  228 
val logicC: class = "logic"; 
229 
val logicS: sort = [logicC]; 

230 

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

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

233 

0  234 
val propT : typ = Type("prop",[]); 
235 

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

237 

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

239 

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

241 

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

243 

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

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

246 
 strip_all_body t = t; 

247 

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

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

1460  250 
(a,T) :: strip_all_vars t 
0  251 
 strip_all_vars t = [] : (string*typ) list; 
252 

253 
(*increments a term's nonlocal bound variables 

254 
required when moving a term within abstractions 

255 
inc is increment for bound variables 

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

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

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

1460  259 
Abs(a, T, incr_bv(inc,lev+1,body)) 
0  260 
 incr_bv (inc, lev, f$t) = 
261 
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 

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

263 

264 
fun incr_boundvars 0 t = t 

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

266 

267 

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

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

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

1460  271 
if i<lev then js else (ilev) ins js 
0  272 
 add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js) 
273 
 add_loose_bnos (f$t, lev, js) = 

1460  274 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
0  275 
 add_loose_bnos (_, _, js) = js; 
276 

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

278 

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

280 
level k or beyond. *) 

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

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

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

284 
 loose_bvar _ = false; 

285 

286 

287 
(*Substitute arguments for loose bound variables. 

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

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

1460  290 
and the appropriate call is subst_bounds([b,a], c) . 
0  291 
Loose bound variables >=n are reduced by "n" to 
292 
compensate for the disappearance of lambdas. 

293 
*) 

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

295 
let val n = length args; 

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

1460  297 
if i<lev then t (*var is locally bound*) 
298 
else (case (drop (ilev,args)) of 

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

300 
 arg::_ => incr_boundvars lev arg) 

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

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

303 
 subst (t,lev) = t 

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

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

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

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

309 

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

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

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

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

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

315 
 (Bound i) aconv (Bound j) = i=j 

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

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

318 
 _ aconv _ = false; 

319 

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

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

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

323 
 aconvs _ = false; 

324 

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

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

327 
fun could_unify (t,u) = 

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

1460  329 
 matchrands _ = true 
0  330 
in case (head_of t , head_of u) of 
1460  331 
(_, Var _) => true 
0  332 
 (Var _, _) => true 
333 
 (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u) 

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

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

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

337 
 (_, Abs _) => true 

338 
 _ => false 

339 
end; 

340 

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

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

343 
 subst_free pairs = 

344 
let fun substf u = 

1460  345 
case gen_assoc (op aconv) (pairs, u) of 
346 
Some u' => u' 

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

348 
 t$u' => substf t $ substf u' 

349 
 _ => u) 

0  350 
in substf end; 
351 

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

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

354 

355 

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

357 
which must contain no loose bound variables. 

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

359 
fun abstract_over (v,body) = 

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

361 
(case u of 

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

1460  363 
 f$rand => abst(lev,f) $ abst(lev,rand) 
364 
 _ => u) 

0  365 
in abst(0,body) end; 
366 

367 

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

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

370 

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

372 
fun list_abs_free ([ ] , t) = t 

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

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

375 

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

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

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

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

380 

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

382 
fun list_all ([], t) = t 

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

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

385 

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

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

388 
fun subst_atomic [] t = t : term 

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

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

1460  391 
 subst (f$t') = subst f $ subst t' 
392 
 subst t = (case assoc(instl,t) of 

393 
Some u => u  None => t) 

0  394 
in subst t end; 
395 

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

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

1460  399 
 subst(T as TFree _) = T 
400 
 subst(T as TVar(ixn,_)) = 

0  401 
(case assoc(iTs,ixn) of None => T  Some(U) => U) 
402 
in subst T end; 

403 

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

404 
(*Substitute for type Vars in a term*) 
0  405 
val subst_TVars = map_term_types o typ_subst_TVars; 
406 

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

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

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

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

412 
 subst(f$t) = subst f $ subst t 

413 
 subst(t) = t 

414 
in subst t end; 

415 

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

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

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

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

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

422 
 Some t => t) 

423 
 subst(b as Bound _) = b 

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

425 
 subst(f$t) = subst f $ subst t 

426 
in subst end; 

427 

428 

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

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

1460  431 
if Ts=[] then ~1 else max(map maxidx_of_typ Ts) 
0  432 
 maxidx_of_typ(TFree _) = ~1 
433 
 maxidx_of_typ(TVar((_,i),_)) = i; 

434 

435 

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

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

438 
 maxidx_of_term (Bound _) = ~1 

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

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

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

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

443 

444 

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

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

448 

449 
(**** Syntaxrelated declarations ****) 

450 

451 

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

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

454 

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

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

457 
let val zero = ord"0" 

458 
val limit = zero+radix 

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

1460  460 
 scan (num, c::cs) = 
461 
if zero <= ord c andalso ord c < limit 

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

463 
else (num, c::cs) 

0  464 
in scan(0,cs) end; 
465 

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

467 

468 

469 
(*** Printing ***) 

470 

471 

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

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

474 
fun variant bs c : string = 

2138
056dead45ae8
Changed some mem calls to mem_string for greater efficiency (not that it could matter)
paulson
parents:
1460
diff
changeset

475 
let fun vary2 c = if (c mem_string bs) then vary2 (bump_string c) else c 
056dead45ae8
Changed some mem calls to mem_string for greater efficiency (not that it could matter)
paulson
parents:
1460
diff
changeset

476 
fun vary1 c = if (c mem_string bs) then vary2 (c ^ "a") else c 
0  477 
in vary1 (if c="" then "u" else c) end; 
478 

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

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

481 
 variantlist(b::bs, used) = 

482 
let val b' = variant used b 

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

484 

485 
(** TFrees and TVars **) 

486 

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

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

489 

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

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

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

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

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

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

496 
 add_term_names (_, bs) = bs; 

497 

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

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

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

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

502 

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

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

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

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

507 

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

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

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

511 

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

512 
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

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

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

515 

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

518 

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

520 
val add_term_tfrees = it_term_types add_typ_tfrees; 

521 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

522 

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

523 
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

524 

0  525 
(*Nonlist versions*) 
526 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

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

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

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

530 

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

531 
(*special code to enforce lefttoright collection of TVarindexnames*) 
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_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

534 
 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

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

536 

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

537 
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

538 
 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

539 
 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

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

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

542 
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

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

544 
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

545 

0  546 
(** Frees and Vars **) 
547 

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

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

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

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

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

553 
 atless _ = false; 

554 

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

556 
fun insert_aterm (t,us) = 

557 
let fun inserta [] = [t] 

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

1460  559 
if atless(t,u) then t::us 
560 
else if t=u then us (*duplicate*) 

561 
else u :: inserta(us') 

0  562 
in inserta us end; 
563 

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

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

566 
Var _ => insert_aterm(t,vars) 

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

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

569 
 _ => vars; 

570 

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

572 

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

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

575 
Free _ => insert_aterm(t,frees) 

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

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

578 
 _ => frees; 

579 

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

581 

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

583 
having a unique name. *) 

584 
fun variant_abs (a,T,P) = 

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

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

587 

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

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

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

1460  591 
(variant (map #1 vars @ names) a, T) :: vars 
0  592 
in foldl rename_aT ([],vars) end; 
593 

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

1364
8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1029
diff
changeset

595 

1417  596 

597 

1426  598 
(*** Compression of terms and types by sharing common subtrees. 
599 
Saves 5075% on storage requirements. As it is fairly slow, 

600 
it is called only for axioms, stored theorems, etc. ***) 

1417  601 

602 
(** Sharing of types **) 

603 

604 
fun atomic_tag (Type (a,_)) = if a<>"fun" then a else raise Match 

605 
 atomic_tag (TFree (a,_)) = a 

606 
 atomic_tag (TVar ((a,_),_)) = a; 

607 

608 
fun type_tag (Type("fun",[S,T])) = atomic_tag S ^ type_tag T 

609 
 type_tag T = atomic_tag T; 

610 

611 
val memo_types = ref (Symtab.null : typ list Symtab.table); 

612 

613 
fun find_type (T, []: typ list) = None 

614 
 find_type (T, T'::Ts) = 

615 
if T=T' then Some T' 

616 
else find_type (T, Ts); 

617 

618 
fun compress_type T = 

619 
let val tag = type_tag T 

620 
val tylist = the (Symtab.lookup (!memo_types, tag)) 

1460  621 
handle _ => [] 
1417  622 
in 
623 
case find_type (T,tylist) of 

1460  624 
Some T' => T' 
1417  625 
 None => 
1460  626 
let val T' = 
627 
case T of 

628 
Type (a,Ts) => Type (a, map compress_type Ts) 

629 
 _ => T 

630 
in memo_types := Symtab.update ((tag, T'::tylist), !memo_types); 

631 
T 

632 
end 

1417  633 
end 
634 
handle Match => 

635 
let val Type (a,Ts) = T 

636 
in Type (a, map compress_type Ts) end; 

637 

638 
(** Sharing of atomic terms **) 

639 

640 
val memo_terms = ref (Symtab.null : term list Symtab.table); 

641 

642 
fun find_term (t, []: term list) = None 

643 
 find_term (t, t'::ts) = 

644 
if t=t' then Some t' 

645 
else find_term (t, ts); 

646 

647 
fun const_tag (Const (a,_)) = a 

648 
 const_tag (Free (a,_)) = a 

649 
 const_tag (Var ((a,i),_)) = a 

650 
 const_tag (t as Bound _) = ".B."; 

651 

652 
fun share_term (t $ u) = share_term t $ share_term u 

653 
 share_term (Abs (a,T,u)) = Abs (a, T, share_term u) 

654 
 share_term t = 

655 
let val tag = const_tag t 

1460  656 
val ts = the (Symtab.lookup (!memo_terms, tag)) 
657 
handle _ => [] 

1417  658 
in 
1460  659 
case find_term (t,ts) of 
660 
Some t' => t' 

661 
 None => (memo_terms := Symtab.update ((tag, t::ts), !memo_terms); 

662 
t) 

1417  663 
end; 
664 

665 
val compress_term = share_term o map_term_types compress_type; 

666 

1364
8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1029
diff
changeset

667 
end; 
8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1029
diff
changeset

668 

8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1029
diff
changeset

669 
open Term; 