author  paulson 
Tue, 22 Jul 1997 11:14:18 +0200  
changeset 3538  ed9de44032e0 
parent 2959  071bfb16586f 
child 3781  ec519ba6196e 
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) = 

2176  271 
if i<lev then js else (ilev) ins_int 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 

2792  286 
fun loose_bvar1(Bound i,k) = i = k 
287 
 loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 

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

289 
 loose_bvar1 _ = false; 

0  290 

291 
(*Substitute arguments for loose bound variables. 

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

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

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

297 
*) 

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

299 
let val n = length args; 

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

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

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

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

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

306 
 subst (t,lev) = t 

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

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

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

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

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

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

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

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

315 
 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

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

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

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

319 

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

321 
fun betapply (Abs(_,_,t), u) = subst_bound (u,t) 
0  322 
 betapply (f,u) = f$u; 
323 

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

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

325 

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

326 
(*optimized equality test for indexnames. Yields a huge gain under Poly/ML*) 
2959  327 
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

328 

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

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

331 
 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

332 

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

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

334 
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

335 

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

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

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

341 
 (Bound i) aconv (Bound j) = i=j 

0  342 
 (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u andalso T=U 
2752  343 
 (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u) 
0  344 
 _ aconv _ = false; 
345 

2176  346 
(** Membership, insertion, union for terms **) 
347 

348 
fun mem_term (_, []) = false 

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

350 

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

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

352 
 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

353 

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

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

355 
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

356 

2176  357 
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; 
358 

359 
fun union_term (xs, []) = xs 

360 
 union_term ([], ys) = ys 

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

362 

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

364 

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

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

367 
 eq_sort (_, _) = false; 

368 

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

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

371 

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

373 

374 
fun union_sort (xs, []) = xs 

375 
 union_sort ([], ys) = ys 

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

377 

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

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

379 
 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

380 

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

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

382 
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

383 

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

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

387 
 aconvs _ = false; 

388 

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

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

391 
fun could_unify (t,u) = 

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

1460  393 
 matchrands _ = true 
0  394 
in case (head_of t , head_of u) of 
1460  395 
(_, Var _) => true 
0  396 
 (Var _, _) => true 
397 
 (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u) 

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

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

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

401 
 (_, Abs _) => true 

402 
 _ => false 

403 
end; 

404 

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

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

407 
 subst_free pairs = 

408 
let fun substf u = 

1460  409 
case gen_assoc (op aconv) (pairs, u) of 
410 
Some u' => u' 

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

412 
 t$u' => substf t $ substf u' 

413 
 _ => u) 

0  414 
in substf end; 
415 

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

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

418 

419 

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

421 
which must contain no loose bound variables. 

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

423 
fun abstract_over (v,body) = 

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

425 
(case u of 

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

1460  427 
 f$rand => abst(lev,f) $ abst(lev,rand) 
428 
 _ => u) 

0  429 
in abst(0,body) end; 
430 

431 

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

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

434 

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

436 
fun list_abs_free ([ ] , t) = t 

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

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

439 

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

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

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

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

444 

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

446 
fun list_all ([], t) = t 

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

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

449 

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

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

452 
fun subst_atomic [] t = t : term 

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

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

1460  455 
 subst (f$t') = subst f $ subst t' 
456 
 subst t = (case assoc(instl,t) of 

457 
Some u => u  None => t) 

0  458 
in subst t end; 
459 

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

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

1460  463 
 subst(T as TFree _) = T 
464 
 subst(T as TVar(ixn,_)) = 

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

467 

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

468 
(*Substitute for type Vars in a term*) 
0  469 
val subst_TVars = map_term_types o typ_subst_TVars; 
470 

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

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

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

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

476 
 subst(f$t) = subst f $ subst t 

477 
 subst(t) = t 

478 
in subst t end; 

479 

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

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

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

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

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

486 
 Some t => t) 

487 
 subst(b as Bound _) = b 

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

489 
 subst(f$t) = subst f $ subst t 

490 
in subst end; 

491 

492 

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

2146  494 
fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts 
0  495 
 maxidx_of_typ(TFree _) = ~1 
2146  496 
 maxidx_of_typ(TVar((_,i),_)) = i 
497 
and maxidx_of_typs [] = ~1 

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

0  499 

500 

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

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

503 
 maxidx_of_term (Bound _) = ~1 

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

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

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

0  508 

509 

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

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

513 

514 
(**** Syntaxrelated declarations ****) 

515 

516 

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

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

519 

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

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

522 
let val zero = ord"0" 

523 
val limit = zero+radix 

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

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

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

528 
else (num, c::cs) 

0  529 
in scan(0,cs) end; 
530 

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

532 

533 

534 
(*** Printing ***) 

535 

536 

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

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

539 
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

540 
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

541 
fun vary1 c = if (c mem_string bs) then vary2 (c ^ "a") else c 
0  542 
in vary1 (if c="" then "u" else c) end; 
543 

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

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

546 
 variantlist(b::bs, used) = 

547 
let val b' = variant used b 

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

549 

550 
(** TFrees and TVars **) 

551 

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

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

554 

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

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

2176  557 
fun add_term_names (Const(a,_), bs) = a ins_string bs 
558 
 add_term_names (Free(a,_), bs) = a ins_string bs 

0  559 
 add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) 
560 
 add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) 

561 
 add_term_names (_, bs) = bs; 

562 

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

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

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

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

567 

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

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

2176  570 
 add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs 
0  571 
 add_typ_tfree_names(TVar(_),fs) = fs; 
572 

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

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

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

576 

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

577 
fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames (Ts,nms) 
2176  578 
 add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms 
579 
 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

580 

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

583 

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

585 
val add_term_tfrees = it_term_types add_typ_tfrees; 

586 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

587 

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

588 
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

589 

0  590 
(*Nonlist versions*) 
591 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

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

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

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

595 

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

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

597 

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

598 
fun add_typ_ixns(ixns,Type(_,Ts)) = foldl add_typ_ixns (ixns,Ts) 
2176  599 
 add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns 
600 
else ixns@[ixn] 

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

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

602 

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

603 
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

604 
 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

605 
 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

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

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

608 
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

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

610 
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

611 

0  612 
(** Frees and Vars **) 
613 

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

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

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

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

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

619 
 atless _ = false; 

620 

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

622 
fun insert_aterm (t,us) = 

623 
let fun inserta [] = [t] 

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

1460  625 
if atless(t,u) then t::us 
626 
else if t=u then us (*duplicate*) 

627 
else u :: inserta(us') 

0  628 
in inserta us end; 
629 

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

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

632 
Var _ => insert_aterm(t,vars) 

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

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

635 
 _ => vars; 

636 

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

638 

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

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

641 
Free _ => insert_aterm(t,frees) 

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

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

644 
 _ => frees; 

645 

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

647 

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

649 
having a unique name. *) 

650 
fun variant_abs (a,T,P) = 

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

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

652 
in (b, subst_bound (Free(b,T), P)) end; 
0  653 

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

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

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

1460  657 
(variant (map #1 vars @ names) a, T) :: vars 
0  658 
in foldl rename_aT ([],vars) end; 
659 

660 
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

661 

1417  662 

663 

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

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

1417  667 

668 
(** Sharing of types **) 

669 

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

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

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

673 

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

675 
 type_tag T = atomic_tag T; 

676 

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

678 

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

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

681 
if T=T' then Some T' 

682 
else find_type (T, Ts); 

683 

684 
fun compress_type T = 

685 
let val tag = type_tag T 

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

1460  687 
handle _ => [] 
1417  688 
in 
689 
case find_type (T,tylist) of 

1460  690 
Some T' => T' 
1417  691 
 None => 
1460  692 
let val T' = 
693 
case T of 

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

695 
 _ => T 

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

697 
T 

698 
end 

1417  699 
end 
700 
handle Match => 

701 
let val Type (a,Ts) = T 

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

703 

704 
(** Sharing of atomic terms **) 

705 

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

707 

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

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

710 
if t=t' then Some t' 

711 
else find_term (t, ts); 

712 

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

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

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

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

717 

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

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

720 
 share_term t = 

721 
let val tag = const_tag t 

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

1417  724 
in 
1460  725 
case find_term (t,ts) of 
726 
Some t' => t' 

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

728 
t) 

1417  729 
end; 
730 

731 
val compress_term = share_term o map_term_types compress_type; 

732 

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

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

734 

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

735 
open Term; 