author  wenzelm 
Fri, 19 Dec 1997 10:16:16 +0100  
changeset 4444  fa05a79b3e97 
parent 4286  a09e3e6da2de 
child 4464  7a8150506746 
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 

4444  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 >; 
4444  11 
infixr >; 
12 
infix aconv; 

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

13 

4444  14 
signature BASIC_TERM = 
15 
sig 

16 
type indexname 

17 
type class 

18 
type sort 

19 
datatype typ = 

20 
Type of string * typ list  

21 
TFree of string * sort  

22 
TVar of indexname * sort 

23 
val > : typ * typ > typ 

24 
val > : typ list * typ > typ 

25 
val is_TVar: typ > bool 

26 
val domain_type: typ > typ 

27 
val binder_types: typ > typ list 

28 
val body_type: typ > typ 

29 
val strip_type: typ > typ list * typ 

30 
datatype term = 

31 
Const of string * typ  

32 
Free of string * typ  

33 
Var of indexname * typ  

34 
Bound of int  

35 
Abs of string * typ * term  

36 
op $ of term * term 

37 
exception TYPE of string * typ list * term list 

38 
exception TERM of string * term list 

39 
val is_Const: term > bool 

40 
val is_Free: term > bool 

41 
val is_Var: term > bool 

42 
val dest_Const: term > string * typ 

43 
val dest_Free: term > string * typ 

44 
val dest_Var: term > indexname * typ 

45 
val type_of: term > typ 

46 
val type_of1: typ list * term > typ 

47 
val fastype_of: term > typ 

48 
val fastype_of1: typ list * term > typ 

49 
val strip_abs_body: term > term 

50 
val strip_abs_vars: term > (string * typ) list 

51 
val strip_qnt_body: string > term > term 

52 
val strip_qnt_vars: string > term > (string * typ) list 

53 
val list_comb: term * term list > term 

54 
val strip_comb: term > term * term list 

55 
val head_of: term > term 

56 
val size_of_term: term > int 

57 
val map_type_tvar: (indexname * sort > typ) > typ > typ 

58 
val map_type_tfree: (string * sort > typ) > typ > typ 

59 
val map_term_types: (typ > typ) > term > term 

60 
val it_term_types: (typ * 'a > 'a) > term * 'a > 'a 

61 
val map_typ: (class > class) > (string > string) > typ > typ 

62 
val map_term: 

63 
(class > class) > 

64 
(string > string) > (string > string) > term > term 

65 
val foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a 

66 
val foldl_types: ('a * typ > 'a) > 'a * term > 'a 

67 
val foldl_aterms: ('a * term > 'a) > 'a * term > 'a 

68 
val dummyT: typ 

69 
val logicC: class 

70 
val logicS: sort 

71 
val itselfT: typ > typ 

72 
val a_itselfT: typ 

73 
val propT: typ 

74 
val implies: term 

75 
val all: typ > term 

76 
val equals: typ > term 

77 
val flexpair: typ > term 

78 
val strip_all_body: term > term 

79 
val strip_all_vars: term > (string * typ) list 

80 
val incr_bv: int * int * term > term 

81 
val incr_boundvars: int > term > term 

82 
val add_loose_bnos: term * int * int list > int list 

83 
val loose_bnos: term > int list 

84 
val loose_bvar: term * int > bool 

85 
val loose_bvar1: term * int > bool 

86 
val subst_bounds: term list * term > term 

87 
val subst_bound: term * term > term 

88 
val subst_TVars: (indexname * typ) list > term > term 

89 
val betapply: term * term > term 

90 
val eq_ix: indexname * indexname > bool 

91 
val ins_ix: indexname * indexname list > indexname list 

92 
val mem_ix: indexname * indexname list > bool 

93 
val eq_sort: sort * class list > bool 

94 
val mem_sort: sort * class list list > bool 

95 
val subset_sort: sort list * class list list > bool 

96 
val eq_set_sort: sort list * sort list > bool 

97 
val ins_sort: sort * class list list > class list list 

98 
val union_sort: sort list * sort list > sort list 

99 
val aconv: term * term > bool 

100 
val aconvs: term list * term list > bool 

101 
val mem_term: term * term list > bool 

102 
val subset_term: term list * term list > bool 

103 
val eq_set_term: term list * term list > bool 

104 
val ins_term: term * term list > term list 

105 
val union_term: term list * term list > term list 

106 
val could_unify: term * term > bool 

107 
val subst_free: (term * term) list > term > term 

108 
val subst_atomic: (term * term) list > term > term 

109 
val subst_vars: (indexname * typ) list * (indexname * term) list > term > term 

110 
val typ_subst_TVars: (indexname * typ) list > typ > typ 

111 
val subst_Vars: (indexname * term) list > term > term 

112 
val incr_tvar: int > typ > typ 

113 
val xless: (string * int) * indexname > bool 

114 
val atless: term * term > bool 

115 
val insert_aterm: term * term list > term list 

116 
val abstract_over: term * term > term 

117 
val absfree: string * typ * term > term 

118 
val list_abs_free: (string * typ) list * term > term 

119 
val list_all_free: (string * typ) list * term > term 

120 
val list_all: (string * typ) list * term > term 

121 
val maxidx_of_typ: typ > int 

122 
val maxidx_of_typs: typ list > int 

123 
val maxidx_of_term: term > int 

124 
val scan_radixint: int * string list > int * string list 

125 
val scan_int: string list > int * string list 

126 
val variant: string list > string > string 

127 
val variantlist: string list * string list > string list 

128 
val variant_abs: string * typ * term > string * term 

129 
val rename_wrt_term: term > (string * typ) list > (string * typ) list 

130 
val add_new_id: string list * string > string list 

131 
val add_typ_classes: typ * class list > class list 

132 
val add_typ_ixns: indexname list * typ > indexname list 

133 
val add_typ_tfree_names: typ * string list > string list 

134 
val add_typ_tfrees: typ * (string * sort) list > (string * sort) list 

135 
val typ_tfrees: typ > (string * sort) list 

136 
val add_typ_tvars: typ * (indexname * sort) list > (indexname * sort) list 

137 
val typ_tvars: typ > (indexname * sort) list 

138 
val add_typ_tycons: typ * string list > string list 

139 
val add_typ_varnames: typ * string list > string list 

140 
val add_term_classes: term * class list > class list 

141 
val add_term_consts: term * string list > string list 

142 
val add_term_frees: term * term list > term list 

143 
val term_frees: term > term list 

144 
val add_term_names: term * string list > string list 

145 
val add_term_tfree_names: term * string list > string list 

146 
val add_term_tfrees: term * (string * sort) list > (string * sort) list 

147 
val term_tfrees: term > (string * sort) list 

148 
val add_term_tvar_ixns: term * indexname list > indexname list 

149 
val add_term_tvarnames: term * string list > string list 

150 
val add_term_tvars: term * (indexname * sort) list > (indexname * sort) list 

151 
val term_tvars: term > (indexname * sort) list 

152 
val add_term_tycons: term * string list > string list 

153 
val add_term_vars: term * term list > term list 

154 
val term_vars: term > term list 

155 
val exists_Const: (string * typ > bool) > term > bool 

156 
val compress_type: typ > typ 

157 
val compress_term: term > term 

158 
end; 

0  159 

4444  160 
signature TERM = 
161 
sig 

162 
include BASIC_TERM 

163 
val indexname_ord: indexname * indexname > order 

164 
val typ_ord: typ * typ > order 

165 
val typs_ord: typ list * typ list > order 

166 
val term_ord: term * term > order 

167 
val terms_ord: term list * term list > order 

168 
val termless: term * term > bool 

169 
end; 

170 

171 
structure Term: TERM = 

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

172 
struct 
0  173 

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

175 
for resolution.*) 

176 
type indexname = string*int; 

177 

178 
(* Types are classified by classes. *) 

179 
type class = string; 

180 
type sort = class list; 

181 

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

183 
datatype typ = Type of string * typ list 

184 
 TFree of string * sort 

1460  185 
 TVar of indexname * sort; 
0  186 

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

188 

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

190 
val op > = foldr (op >); 

191 

192 

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

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

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

196 
is enclosed by at least "lev" abstractions. 

197 

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

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

200 

201 

202 

203 
datatype term = 

204 
Const of string * typ 

205 
 Free of string * typ 

206 
 Var of indexname * typ 

207 
 Bound of int 

208 
 Abs of string*typ*term 

3965  209 
 op $ of term*term; 
0  210 

211 

212 
(*For errors involving type mismatches*) 

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

214 

215 
(*For system errors involving terms*) 

216 
exception TERM of string * term list; 

217 

218 

219 
(*Note variable naming conventions! 

220 
a,b,c: string 

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

222 
i,j,m,n: int 

223 
t,u: term 

224 
v,w: indexnames 

225 
x,y: any 

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

227 
T,U: typ 

228 
*) 

229 

230 

231 
(** Discriminators **) 

232 

233 
fun is_Const (Const _) = true 

234 
 is_Const _ = false; 

235 

236 
fun is_Free (Free _) = true 

237 
 is_Free _ = false; 

238 

239 
fun is_Var (Var _) = true 

240 
 is_Var _ = false; 

241 

242 
fun is_TVar (TVar _) = true 

243 
 is_TVar _ = false; 

244 

245 
(** Destructors **) 

246 

247 
fun dest_Const (Const x) = x 

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

249 

250 
fun dest_Free (Free x) = x 

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

252 

253 
fun dest_Var (Var x) = x 

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

255 

256 

4064  257 
fun domain_type (Type("fun", [T,_])) = T; 
258 

0  259 
(* maps [T1,...,Tn]>T to the list [T1,T2,...,Tn]*) 
260 
fun binder_types (Type("fun",[S,T])) = S :: binder_types T 

261 
 binder_types _ = []; 

262 

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

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

265 
 body_type T = T; 

266 

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

268 
fun strip_type T : typ list * typ = 

269 
(binder_types T, body_type T); 

270 

271 

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

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

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

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

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

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

280 
 type_of1 (Ts, f$u) = 

281 
let val U = type_of1(Ts,u) 

282 
and T = type_of1(Ts,f) 

283 
in case T of 

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

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

287 
 _ => raise TYPE 

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

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

0  290 
end; 
291 

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

293 

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

61  295 
fun fastype_of1 (Ts, f$u) = 
296 
(case fastype_of1 (Ts,f) of 

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

61  299 
 fastype_of1 (_, Const (_,T)) = T 
300 
 fastype_of1 (_, Free (_,T)) = T 

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

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

305 

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

0  307 

308 

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

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

311 
 strip_abs_body u = u; 

312 

313 

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

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

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

317 

318 

319 
fun strip_qnt_body qnt = 

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

321 
 strip t = t 

322 
in strip end; 

323 

324 
fun strip_qnt_vars qnt = 

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

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

327 
in strip end; 

328 

329 

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

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

332 

333 

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

335 
fun strip_comb u : term * term list = 

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

337 
 stripc x = x 

338 
in stripc(u,[]) end; 

339 

340 

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

342 
fun head_of (f$t) = head_of f 

343 
 head_of u = u; 

344 

345 

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

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

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

349 
 size_of_term _ = 1; 

350 

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

351 
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

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

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

354 

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

355 
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

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

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

358 

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

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

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

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

364 
 map(t as Bound _) = t 

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

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

367 
in map end; 

368 

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

370 
fun it_term_types f = 

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

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

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

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

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

376 
 iter(Bound _, a) = a 

377 
in iter end 

378 

379 

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

381 

375  382 
val logicC: class = "logic"; 
383 
val logicS: sort = [logicC]; 

384 

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

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

387 

0  388 
val propT : typ = Type("prop",[]); 
389 

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

391 

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

393 

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

395 

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

397 

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

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

400 
 strip_all_body t = t; 

401 

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

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

1460  404 
(a,T) :: strip_all_vars t 
0  405 
 strip_all_vars t = [] : (string*typ) list; 
406 

407 
(*increments a term's nonlocal bound variables 

408 
required when moving a term within abstractions 

409 
inc is increment for bound variables 

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

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

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

1460  413 
Abs(a, T, incr_bv(inc,lev+1,body)) 
0  414 
 incr_bv (inc, lev, f$t) = 
415 
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 

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

417 

418 
fun incr_boundvars 0 t = t 

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

420 

421 

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

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

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

2176  425 
if i<lev then js else (ilev) ins_int js 
0  426 
 add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js) 
427 
 add_loose_bnos (f$t, lev, js) = 

1460  428 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
0  429 
 add_loose_bnos (_, _, js) = js; 
430 

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

432 

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

434 
level k or beyond. *) 

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

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

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

438 
 loose_bvar _ = false; 

439 

2792  440 
fun loose_bvar1(Bound i,k) = i = k 
441 
 loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 

442 
 loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1) 

443 
 loose_bvar1 _ = false; 

0  444 

445 
(*Substitute arguments for loose bound variables. 

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

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

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

451 
*) 

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

453 
let val n = length args; 

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

2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2192
diff
changeset

455 
(if i<lev then t (*var is locally bound*) 
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2192
diff
changeset

456 
else incr_boundvars lev (List.nth(args, ilev)) 
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2192
diff
changeset

457 
handle Subscript => Bound(in) (*loose: change it*)) 
1460  458 
 subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1)) 
459 
 subst (f$t, lev) = subst(f,lev) $ subst(t,lev) 

460 
 subst (t,lev) = t 

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

2192
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

463 
(*Special case: one argument*) 
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

464 
fun subst_bound (arg, t) : term = 
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

465 
let fun subst (t as Bound i, lev) = 
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

466 
if i<lev then t (*var is locally bound*) 
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

467 
else if i=lev then incr_boundvars lev arg 
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

468 
else Bound(i1) (*loose: change it*) 
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

469 
 subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1)) 
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

470 
 subst (f$t, lev) = subst(f,lev) $ subst(t,lev) 
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

471 
 subst (t,lev) = t 
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

472 
in subst (t,0) end; 
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

473 

0  474 
(*betareduce if possible, else form application*) 
2192
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

475 
fun betapply (Abs(_,_,t), u) = subst_bound (u,t) 
0  476 
 betapply (f,u) = f$u; 
477 

2192
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

478 
(** Equality, membership and insertion of indexnames (string*ints) **) 
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

479 

3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

480 
(*optimized equality test for indexnames. Yields a huge gain under Poly/ML*) 
2959  481 
fun eq_ix ((a, i):indexname, (a',i'):indexname) = (a=a') andalso i=i'; 
2192
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

482 

3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

483 
(*membership in a list, optimized version for indexnames*) 
2959  484 
fun mem_ix (_, []) = false 
2192
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

485 
 mem_ix (x, y :: ys) = eq_ix(x,y) orelse mem_ix (x, ys); 
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

486 

3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

487 
(*insertion into list, optimized version for indexnames*) 
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

488 
fun ins_ix (x,xs) = if mem_ix (x, xs) then xs else x :: xs; 
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

489 

0  490 
(*Tests whether 2 terms are alphaconvertible and have same type. 
491 
Note that constants and Vars may have more than one type.*) 

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

2752  493 
 (Free(a,T)) aconv (Free(b,U)) = a=b andalso T=U 
494 
 (Var(v,T)) aconv (Var(w,U)) = eq_ix(v,w) andalso T=U 

495 
 (Bound i) aconv (Bound j) = i=j 

0  496 
 (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u andalso T=U 
2752  497 
 (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u) 
0  498 
 _ aconv _ = false; 
499 

2176  500 
(** Membership, insertion, union for terms **) 
501 

502 
fun mem_term (_, []) = false 

503 
 mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts); 

504 

2182
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2176
diff
changeset

505 
fun subset_term ([], ys) = true 
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2176
diff
changeset

506 
 subset_term (x :: xs, ys) = mem_term (x, ys) andalso subset_term(xs, ys); 
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2176
diff
changeset

507 

29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2176
diff
changeset

508 
fun eq_set_term (xs, ys) = 
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2176
diff
changeset

509 
xs = ys orelse (subset_term (xs, ys) andalso subset_term (ys, xs)); 
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2176
diff
changeset

510 

2176  511 
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; 
512 

513 
fun union_term (xs, []) = xs 

514 
 union_term ([], ys) = ys 

515 
 union_term ((x :: xs), ys) = union_term (xs, ins_term (x, ys)); 

516 

517 
(** Equality, membership and insertion of sorts (string lists) **) 

518 

519 
fun eq_sort ([]:sort, []) = true 

520 
 eq_sort ((s::ss), (t::ts)) = s=t andalso eq_sort(ss,ts) 

521 
 eq_sort (_, _) = false; 

522 

523 
fun mem_sort (_:sort, []) = false 

524 
 mem_sort (S, S'::Ss) = eq_sort (S, S') orelse mem_sort(S,Ss); 

525 

526 
fun ins_sort(S,Ss) = if mem_sort(S,Ss) then Ss else S :: Ss; 

527 

528 
fun union_sort (xs, []) = xs 

529 
 union_sort ([], ys) = ys 

530 
 union_sort ((x :: xs), ys) = union_sort (xs, ins_sort (x, ys)); 

531 

2182
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2176
diff
changeset

532 
fun subset_sort ([], ys) = true 
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2176
diff
changeset

533 
 subset_sort (x :: xs, ys) = mem_sort (x, ys) andalso subset_sort(xs, ys); 
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2176
diff
changeset

534 

29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2176
diff
changeset

535 
fun eq_set_sort (xs, ys) = 
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2176
diff
changeset

536 
xs = ys orelse (subset_sort (xs, ys) andalso subset_sort (ys, xs)); 
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2176
diff
changeset

537 

0  538 
(*are two term lists alphaconvertible in corresponding elements?*) 
539 
fun aconvs ([],[]) = true 

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

541 
 aconvs _ = false; 

542 

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

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

545 
fun could_unify (t,u) = 

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

1460  547 
 matchrands _ = true 
0  548 
in case (head_of t , head_of u) of 
1460  549 
(_, Var _) => true 
0  550 
 (Var _, _) => true 
551 
 (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u) 

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

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

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

555 
 (_, Abs _) => true 

556 
 _ => false 

557 
end; 

558 

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

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

561 
 subst_free pairs = 

562 
let fun substf u = 

1460  563 
case gen_assoc (op aconv) (pairs, u) of 
564 
Some u' => u' 

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

566 
 t$u' => substf t $ substf u' 

567 
 _ => u) 

0  568 
in substf end; 
569 

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

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

572 

573 

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

575 
which must contain no loose bound variables. 

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

577 
fun abstract_over (v,body) = 

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

579 
(case u of 

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

1460  581 
 f$rand => abst(lev,f) $ abst(lev,rand) 
582 
 _ => u) 

0  583 
in abst(0,body) end; 
584 

585 

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

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

588 

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

590 
fun list_abs_free ([ ] , t) = t 

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

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

593 

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

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

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

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

598 

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

600 
fun list_all ([], t) = t 

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

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

603 

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

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

606 
fun subst_atomic [] t = t : term 

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

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

1460  609 
 subst (f$t') = subst f $ subst t' 
610 
 subst t = (case assoc(instl,t) of 

611 
Some u => u  None => t) 

0  612 
in subst t end; 
613 

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

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

1460  617 
 subst(T as TFree _) = T 
618 
 subst(T as TVar(ixn,_)) = 

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

621 

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

622 
(*Substitute for type Vars in a term*) 
0  623 
val subst_TVars = map_term_types o typ_subst_TVars; 
624 

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

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

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

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

630 
 subst(f$t) = subst f $ subst t 

631 
 subst(t) = t 

632 
in subst t end; 

633 

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

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

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

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

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

640 
 Some t => t) 

641 
 subst(b as Bound _) = b 

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

643 
 subst(f$t) = subst f $ subst t 

644 
in subst end; 

645 

646 

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

2146  648 
fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts 
0  649 
 maxidx_of_typ(TFree _) = ~1 
2146  650 
 maxidx_of_typ(TVar((_,i),_)) = i 
651 
and maxidx_of_typs [] = ~1 

652 
 maxidx_of_typs (T::Ts) = Int.max(maxidx_of_typ T, maxidx_of_typs Ts); 

0  653 

654 

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

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

657 
 maxidx_of_term (Bound _) = ~1 

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

2146  659 
 maxidx_of_term (Var ((_,i), T)) = Int.max(i, maxidx_of_typ T) 
660 
 maxidx_of_term (Abs (_,T,u)) = Int.max(maxidx_of_term u, maxidx_of_typ T) 

661 
 maxidx_of_term (f$t) = Int.max(maxidx_of_term f, maxidx_of_term t); 

0  662 

663 

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

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

667 

668 
(**** Syntaxrelated declarations ****) 

669 

670 

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

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

673 

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

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

676 
let val zero = ord"0" 

677 
val limit = zero+radix 

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

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

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

682 
else (num, c::cs) 

0  683 
in scan(0,cs) end; 
684 

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

686 

687 

688 
(*** Printing ***) 

689 

690 

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

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

693 
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

694 
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

695 
fun vary1 c = if (c mem_string bs) then vary2 (c ^ "a") else c 
0  696 
in vary1 (if c="" then "u" else c) end; 
697 

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

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

700 
 variantlist(b::bs, used) = 

701 
let val b' = variant used b 

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

703 

4017
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

704 

63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

705 

63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

706 
(** Consts etc. **) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

707 

63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

708 
fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes (Ts, cs) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

709 
 add_typ_classes (TFree (_, S), cs) = S union cs 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

710 
 add_typ_classes (TVar (_, S), cs) = S union cs; 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

711 

63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

712 
fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (Ts, c ins cs) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

713 
 add_typ_tycons (_, cs) = cs; 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

714 

63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

715 
val add_term_classes = it_term_types add_typ_classes; 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

716 
val add_term_tycons = it_term_types add_typ_tycons; 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

717 

63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

718 
fun add_term_consts (Const (c, _), cs) = c ins cs 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

719 
 add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs)) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

720 
 add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

721 
 add_term_consts (_, cs) = cs; 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

722 

4185  723 
fun exists_Const P t = let 
724 
fun ex (Const c ) = P c 

725 
 ex (t $ u ) = ex t orelse ex u 

726 
 ex (Abs (_, _, t)) = ex t 

727 
 ex _ = false 

728 
in ex t end; 

4017
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

729 

63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

730 
(*map classes, tycons*) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

731 
fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

732 
 map_typ f _ (TFree (x, S)) = TFree (x, map f S) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

733 
 map_typ f _ (TVar (xi, S)) = TVar (xi, map f S); 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

734 

63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

735 
(*map classes, tycons, consts*) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

736 
fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

737 
 map_term f g _ (Free (x, T)) = Free (x, map_typ f g T) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

738 
 map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

739 
 map_term _ _ _ (t as Bound _) = t 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

740 
 map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

741 
 map_term f g h (t $ u) = map_term f g h t $ map_term f g h u; 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

742 

63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

743 

63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

744 

0  745 
(** TFrees and TVars **) 
746 

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

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

749 

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

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

2176  752 
fun add_term_names (Const(a,_), bs) = a ins_string bs 
753 
 add_term_names (Free(a,_), bs) = a ins_string bs 

0  754 
 add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) 
755 
 add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) 

756 
 add_term_names (_, bs) = bs; 

757 

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

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

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

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

762 

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

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

2176  765 
 add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs 
0  766 
 add_typ_tfree_names(TVar(_),fs) = fs; 
767 

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

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

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

771 

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

772 
fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames (Ts,nms) 
2176  773 
 add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms 
774 
 add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms; 

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

775 

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

778 

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

780 
val add_term_tfrees = it_term_types add_typ_tfrees; 

781 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

782 

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

783 
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

784 

0  785 
(*Nonlist versions*) 
786 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

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

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

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

790 

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

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

792 

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

793 
fun add_typ_ixns(ixns,Type(_,Ts)) = foldl add_typ_ixns (ixns,Ts) 
2176  794 
 add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns 
795 
else ixns@[ixn] 

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

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

797 

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

798 
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

799 
 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

800 
 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

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

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

803 
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

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

805 
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

806 

0  807 
(** Frees and Vars **) 
808 

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

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

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

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

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

814 
 atless _ = false; 

815 

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

817 
fun insert_aterm (t,us) = 

818 
let fun inserta [] = [t] 

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

1460  820 
if atless(t,u) then t::us 
821 
else if t=u then us (*duplicate*) 

822 
else u :: inserta(us') 

0  823 
in inserta us end; 
824 

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

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

827 
Var _ => insert_aterm(t,vars) 

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

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

830 
 _ => vars; 

831 

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

833 

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

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

836 
Free _ => insert_aterm(t,frees) 

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

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

839 
 _ => frees; 

840 

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

842 

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

844 
having a unique name. *) 

845 
fun variant_abs (a,T,P) = 

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

2192
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

847 
in (b, subst_bound (Free(b,T), P)) end; 
0  848 

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

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

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

1460  852 
(variant (map #1 vars @ names) a, T) :: vars 
0  853 
in foldl rename_aT ([],vars) end; 
854 

855 
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

856 

1417  857 

4286
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

858 
(* leftroright traversal *) 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

859 

a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

860 
(*foldl atoms of type*) 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

861 
fun foldl_atyps f (x, Type (_, Ts)) = foldl (foldl_atyps f) (x, Ts) 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

862 
 foldl_atyps f x_atom = f x_atom; 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

863 

a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

864 
(*foldl atoms of term*) 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

865 
fun foldl_aterms f (x, t $ u) = foldl_aterms f (foldl_aterms f (x, t), u) 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

866 
 foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t) 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

867 
 foldl_aterms f x_atom = f x_atom; 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

868 

a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

869 
(*foldl types of term*) 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

870 
fun foldl_types f (x, Const (_, T)) = f (x, T) 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

871 
 foldl_types f (x, Free (_, T)) = f (x, T) 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

872 
 foldl_types f (x, Var (_, T)) = f (x, T) 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

873 
 foldl_types f (x, Bound _) = x 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

874 
 foldl_types f (x, Abs (_, T, t)) = foldl_types f (f (x, T), t) 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

875 
 foldl_types f (x, t $ u) = foldl_types f (foldl_types f (x, t), u); 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

876 

a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

877 

1417  878 

4444  879 
(** type and term orders **) 
880 

881 
fun indexname_ord ((x, i), (y, j)) = 

882 
(case int_ord (i, j) of EQUAL => string_ord (x, y)  ord => ord); 

883 

884 

885 
(* typ_ord *) 

886 

887 
(*assumes that TFrees / TVars with the same name have same sorts*) 

888 
fun typ_ord (Type (a, Ts), Type (b, Us)) = 

889 
(case string_ord (a, b) of EQUAL => typs_ord (Ts, Us)  ord => ord) 

890 
 typ_ord (Type _, _) = GREATER 

891 
 typ_ord (TFree _, Type _) = LESS 

892 
 typ_ord (TFree (a, _), TFree (b, _)) = string_ord (a, b) 

893 
 typ_ord (TFree _, TVar _) = GREATER 

894 
 typ_ord (TVar _, Type _) = LESS 

895 
 typ_ord (TVar _, TFree _) = LESS 

896 
 typ_ord (TVar (xi, _), TVar (yj, _)) = indexname_ord (xi, yj) 

897 
and typs_ord Ts_Us = list_ord typ_ord Ts_Us; 

898 

899 

900 
(* term_ord *) 

901 

902 
(*a linear wellfounded ACcompatible ordering for terms: 

903 
s < t <=> 1. size(s) < size(t) or 

904 
2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or 

905 
3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and 

906 
(s1..sn) < (t1..tn) (lexicographically)*) 

907 

908 
fun dest_hd (Const (a, T)) = (((a, 0), T), 0) 

909 
 dest_hd (Free (a, T)) = (((a, 0), T), 1) 

910 
 dest_hd (Var v) = (v, 2) 

911 
 dest_hd (Bound i) = ((("", i), dummyT), 3) 

912 
 dest_hd (Abs (_, T, _)) = ((("", 0), T), 4); 

913 

914 
fun term_ord (Abs (_, T, t), Abs(_, U, u)) = 

915 
(case term_ord (t, u) of EQUAL => typ_ord (T, U)  ord => ord) 

916 
 term_ord (t, u) = 

917 
(case int_ord (size_of_term t, size_of_term u) of 

918 
EQUAL => 

919 
let val (f, ts) = strip_comb t and (g, us) = strip_comb u in 

920 
(case hd_ord (f, g) of EQUAL => terms_ord (ts, us)  ord => ord) 

921 
end 

922 
 ord => ord) 

923 
and hd_ord (f, g) = 

924 
prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g) 

925 
and terms_ord (ts, us) = list_ord term_ord (ts, us); 

926 

927 
fun termless tu = (term_ord tu = LESS); 

928 

929 

930 

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

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

1417  934 

935 
(** Sharing of types **) 

936 

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

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

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

940 

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

942 
 type_tag T = atomic_tag T; 

943 

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

945 

4188
1025a27b08f9
changed libraray function find to find_index_eq, currying it
oheimb
parents:
4185
diff
changeset

946 
(* special case of library/find_first *) 
1417  947 
fun find_type (T, []: typ list) = None 
948 
 find_type (T, T'::Ts) = 

949 
if T=T' then Some T' 

950 
else find_type (T, Ts); 

951 

952 
fun compress_type T = 

953 
let val tag = type_tag T 

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

1460  955 
handle _ => [] 
1417  956 
in 
957 
case find_type (T,tylist) of 

1460  958 
Some T' => T' 
1417  959 
 None => 
1460  960 
let val T' = 
961 
case T of 

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

963 
 _ => T 

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

965 
T 

966 
end 

1417  967 
end 
968 
handle Match => 

969 
let val Type (a,Ts) = T 

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

971 

972 
(** Sharing of atomic terms **) 

973 

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

975 

4188
1025a27b08f9
changed libraray function find to find_index_eq, currying it
oheimb
parents:
4185
diff
changeset

976 
(* special case of library/find_first *) 
1417  977 
fun find_term (t, []: term list) = None 
978 
 find_term (t, t'::ts) = 

979 
if t=t' then Some t' 

980 
else find_term (t, ts); 

981 

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

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

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

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

986 

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

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

989 
 share_term t = 

990 
let val tag = const_tag t 

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

1417  993 
in 
1460  994 
case find_term (t,ts) of 
995 
Some t' => t' 

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

997 
t) 

1417  998 
end; 
999 

1000 
val compress_term = share_term o map_term_types compress_type; 

1001 

4444  1002 

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

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

1004 

4444  1005 

1006 
structure BasicTerm: BASIC_TERM = Term; 

1007 
open BasicTerm; 