author  wenzelm 
Thu, 17 Jan 2002 21:03:55 +0100  
changeset 12802  c69bd9754473 
parent 12499  1b56e1732a61 
child 12902  a23dc0b7566f 
permissions  rwrr 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1 
(* Title: Pure/term.ML 
0  2 
ID: $Id$ 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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 

4480  27 
val range_type: typ > typ 
4444  28 
val binder_types: typ > typ list 
29 
val body_type: typ > typ 

30 
val strip_type: typ > typ list * typ 

31 
datatype term = 

32 
Const of string * typ  

33 
Free of string * typ  

34 
Var of indexname * typ  

35 
Bound of int  

36 
Abs of string * typ * term  

4493  37 
$ of term * term 
8408
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

38 
structure Vartab : TABLE 
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

39 
structure Termtab : TABLE 
4444  40 
exception TYPE of string * typ list * term list 
41 
exception TERM of string * term list 

7318  42 
val is_Bound: term > bool 
4444  43 
val is_Const: term > bool 
44 
val is_Free: term > bool 

45 
val is_Var: term > bool 

6033
c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

46 
val dest_Type: typ > string * typ list 
4444  47 
val dest_Const: term > string * typ 
48 
val dest_Free: term > string * typ 

49 
val dest_Var: term > indexname * typ 

50 
val type_of: term > typ 

51 
val type_of1: typ list * term > typ 

52 
val fastype_of: term > typ 

53 
val fastype_of1: typ list * term > typ 

10806  54 
val list_abs: (string * typ) list * term > term 
4444  55 
val strip_abs_body: term > term 
56 
val strip_abs_vars: term > (string * typ) list 

57 
val strip_qnt_body: string > term > term 

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

59 
val list_comb: term * term list > term 

60 
val strip_comb: term > term * term list 

61 
val head_of: term > term 

62 
val size_of_term: term > int 

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

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

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

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

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

68 
val map_term: 

69 
(class > class) > 

70 
(string > string) > (string > string) > term > term 

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

8609  72 
val foldl_term_types: (term > 'a * typ > 'a) > 'a * term > 'a 
4444  73 
val foldl_types: ('a * typ > 'a) > 'a * term > 'a 
74 
val foldl_aterms: ('a * term > 'a) > 'a * term > 'a 

6548
9b108dd75c25
val foldl_map_aterms: ('a * term > 'a * term) > 'a * term > 'a * term;
wenzelm
parents:
6033
diff
changeset

75 
val foldl_map_aterms: ('a * term > 'a * term) > 'a * term > 'a * term 
4444  76 
val dummyT: typ 
77 
val logicC: class 

78 
val logicS: sort 

79 
val itselfT: typ > typ 

80 
val a_itselfT: typ 

81 
val propT: typ 

82 
val implies: term 

83 
val all: typ > term 

84 
val equals: typ > term 

85 
val flexpair: typ > term 

86 
val strip_all_body: term > term 

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

88 
val incr_bv: int * int * term > term 

89 
val incr_boundvars: int > term > term 

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

91 
val loose_bnos: term > int list 

92 
val loose_bvar: term * int > bool 

93 
val loose_bvar1: term * int > bool 

94 
val subst_bounds: term list * term > term 

95 
val subst_bound: term * term > term 

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

8408
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

97 
val subst_TVars_Vartab: typ Vartab.table > term > term 
4444  98 
val betapply: term * term > term 
99 
val eq_ix: indexname * indexname > bool 

100 
val ins_ix: indexname * indexname list > indexname list 

101 
val mem_ix: indexname * indexname list > bool 

102 
val eq_sort: sort * class list > bool 

103 
val mem_sort: sort * class list list > bool 

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

105 
val eq_set_sort: sort list * sort list > bool 

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

107 
val union_sort: sort list * sort list > sort list 

7638  108 
val rems_sort: sort list * sort list > sort list 
4444  109 
val aconv: term * term > bool 
110 
val aconvs: term list * term list > bool 

111 
val mem_term: term * term list > bool 

112 
val subset_term: term list * term list > bool 

113 
val eq_set_term: term list * term list > bool 

114 
val ins_term: term * term list > term list 

115 
val union_term: term list * term list > term list 

5585  116 
val inter_term: term list * term list > term list 
4444  117 
val could_unify: term * term > bool 
118 
val subst_free: (term * term) list > term > term 

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

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

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

8408
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

122 
val typ_subst_TVars_Vartab : typ Vartab.table > typ > typ 
4444  123 
val subst_Vars: (indexname * term) list > term > term 
124 
val incr_tvar: int > typ > typ 

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

126 
val atless: term * term > bool 

127 
val insert_aterm: term * term list > term list 

128 
val abstract_over: term * term > term 

11922  129 
val lambda: term > term > term 
4444  130 
val absfree: string * typ * term > term 
131 
val list_abs_free: (string * typ) list * term > term 

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

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

134 
val maxidx_of_typ: typ > int 

135 
val maxidx_of_typs: typ list > int 

136 
val maxidx_of_term: term > int 

4694  137 
val read_radixint: int * string list > int * string list 
138 
val read_int: string list > int * string list 

5986  139 
val oct_char: string > string 
4444  140 
val variant: string list > string > string 
141 
val variantlist: string list * string list > string list 

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

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

144 
val add_new_id: string list * string > string list 

145 
val add_typ_classes: typ * class list > class list 

146 
val add_typ_ixns: indexname list * typ > indexname list 

147 
val add_typ_tfree_names: typ * string list > string list 

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

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

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

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

152 
val add_typ_tycons: typ * string list > string list 

153 
val add_typ_varnames: typ * string list > string list 

154 
val add_term_classes: term * class list > class list 

155 
val add_term_consts: term * string list > string list 

156 
val add_term_frees: term * term list > term list 

157 
val term_frees: term > term list 

12802
c69bd9754473
added add_term_free_names (more precise/efficient than add_term_names);
wenzelm
parents:
12499
diff
changeset

158 
val add_term_free_names: term * string list > string list 
4444  159 
val add_term_names: term * string list > string list 
160 
val add_term_tfree_names: term * string list > string list 

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

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

163 
val add_term_tvar_ixns: term * indexname list > indexname list 

164 
val add_term_tvarnames: term * string list > string list 

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

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

167 
val add_term_tycons: term * string list > string list 

168 
val add_term_vars: term * term list > term list 

169 
val term_vars: term > term list 

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

4631  171 
val exists_subterm: (term > bool) > term > bool 
4444  172 
val compress_type: typ > typ 
173 
val compress_term: term > term 

174 
end; 

0  175 

4444  176 
signature TERM = 
177 
sig 

178 
include BASIC_TERM 

12499  179 
val invent_names: string list > string > int > string list 
180 
val invent_type_names: string list > int > string list 

181 
val add_tvarsT: (indexname * sort) list * typ > (indexname * sort) list 

182 
val add_tvars: (indexname * sort) list * term > (indexname * sort) list 

183 
val add_vars: (indexname * typ) list * term > (indexname * typ) list 

184 
val add_frees: (string * typ) list * term > (string * typ) list 

4444  185 
val indexname_ord: indexname * indexname > order 
186 
val typ_ord: typ * typ > order 

187 
val typs_ord: typ list * typ list > order 

188 
val term_ord: term * term > order 

189 
val terms_ord: term list * term list > order 

190 
val termless: term * term > bool 

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

191 
val dummy_patternN: string 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

192 
val no_dummy_patterns: term > term 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

193 
val replace_dummy_patterns: int * term > int * term 
10552  194 
val is_replaced_dummy_pattern: indexname > bool 
4444  195 
end; 
196 

197 
structure Term: TERM = 

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

198 
struct 
0  199 

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

201 
for resolution.*) 

202 
type indexname = string*int; 

203 

4626  204 
(* Types are classified by sorts. *) 
0  205 
type class = string; 
206 
type sort = class list; 

207 

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

209 
datatype typ = Type of string * typ list 

210 
 TFree of string * sort 

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

211 
 TVar of indexname * sort; 
0  212 

6033
c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

213 
(*Terms. Bound variables are indicated by depth number. 
0  214 
Free variables, (scheme) variables and constants have names. 
4626  215 
An term is "closed" if every bound variable of level "lev" 
0  216 
is enclosed by at least "lev" abstractions. 
217 

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

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

220 

221 

222 

223 
datatype term = 

224 
Const of string * typ 

225 
 Free of string * typ 

226 
 Var of indexname * typ 

227 
 Bound of int 

228 
 Abs of string*typ*term 

3965  229 
 op $ of term*term; 
0  230 

231 

232 
(*For errors involving type mismatches*) 

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

234 

235 
(*For system errors involving terms*) 

236 
exception TERM of string * term list; 

237 

238 

239 
(*Note variable naming conventions! 

240 
a,b,c: string 

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

242 
i,j,m,n: int 

243 
t,u: term 

244 
v,w: indexnames 

245 
x,y: any 

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

247 
T,U: typ 

248 
*) 

249 

250 

6033
c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

251 
(** Types **) 
c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

252 

c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

253 
fun S > T = Type("fun",[S,T]); 
c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

254 

c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

255 
(*handy for multiple args: [T1,...,Tn]>T gives T1>(T2> ... >T)*) 
c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

256 
val op > = foldr (op >); 
c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

257 

c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

258 
fun dest_Type (Type x) = x 
c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

259 
 dest_Type T = raise TYPE ("dest_Type", [T], []); 
c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

260 

c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

261 

0  262 
(** Discriminators **) 
263 

7318  264 
fun is_Bound (Bound _) = true 
265 
 is_Bound _ = false; 

266 

0  267 
fun is_Const (Const _) = true 
268 
 is_Const _ = false; 

269 

270 
fun is_Free (Free _) = true 

271 
 is_Free _ = false; 

272 

273 
fun is_Var (Var _) = true 

274 
 is_Var _ = false; 

275 

276 
fun is_TVar (TVar _) = true 

277 
 is_TVar _ = false; 

278 

279 
(** Destructors **) 

280 

281 
fun dest_Const (Const x) = x 

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

283 

284 
fun dest_Free (Free x) = x 

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

286 

287 
fun dest_Var (Var x) = x 

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

289 

290 

4464  291 
fun domain_type (Type("fun", [T,_])) = T 
292 
and range_type (Type("fun", [_,T])) = T; 

4064  293 

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

296 
 binder_types _ = []; 

297 

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

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

300 
 body_type T = T; 

301 

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

303 
fun strip_type T : typ list * typ = 

304 
(binder_types T, body_type T); 

305 

306 

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

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

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

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

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

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

312 
handle LIST _ => raise TYPE("type_of: bound variable", [], [Bound i])) 
0  313 
 type_of1 (Ts, Var (_,T)) = T 
314 
 type_of1 (Ts, Abs (_,T,body)) = T > type_of1(T::Ts, body) 

315 
 type_of1 (Ts, f$u) = 

316 
let val U = type_of1(Ts,u) 

317 
and T = type_of1(Ts,f) 

318 
in case T of 

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

319 
Type("fun",[T1,T2]) => 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

320 
if T1=U then T2 else raise TYPE 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

321 
("type_of: type mismatch in application", [T1,U], [f$u]) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

322 
 _ => raise TYPE 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

323 
("type_of: function type is expected in application", 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

324 
[T,U], [f$u]) 
0  325 
end; 
326 

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

328 

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

61  330 
fun fastype_of1 (Ts, f$u) = 
331 
(case fastype_of1 (Ts,f) of 

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

332 
Type("fun",[_,T]) => T 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

333 
 _ => raise TERM("fastype_of: expected function type", [f$u])) 
61  334 
 fastype_of1 (_, Const (_,T)) = T 
335 
 fastype_of1 (_, Free (_,T)) = T 

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

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

337 
handle LIST _ => raise TERM("fastype_of: Bound", [Bound i])) 
61  338 
 fastype_of1 (_, Var (_,T)) = T 
339 
 fastype_of1 (Ts, Abs (_,T,u)) = T > fastype_of1 (T::Ts, u); 

340 

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

0  342 

343 

10806  344 
val list_abs = foldr (fn ((x, T), t) => Abs (x, T, t)); 
345 

0  346 
(* maps (x1,...,xn)t to t *) 
347 
fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t 

348 
 strip_abs_body u = u; 

349 

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

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

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

353 

354 

355 
fun strip_qnt_body qnt = 

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

357 
 strip t = t 

358 
in strip end; 

359 

360 
fun strip_qnt_vars qnt = 

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

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

363 
in strip end; 

364 

365 

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

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

368 

369 

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

371 
fun strip_comb u : term * term list = 

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

373 
 stripc x = x 

374 
in stripc(u,[]) end; 

375 

376 

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

378 
fun head_of (f$t) = head_of f 

379 
 head_of u = u; 

380 

381 

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

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

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

385 
 size_of_term _ = 1; 

386 

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

387 
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

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

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

390 

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

391 
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

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

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

394 

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

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

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

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

400 
 map(t as Bound _) = t 

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

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

403 
in map end; 

404 

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

406 
fun it_term_types f = 

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

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

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

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

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

412 
 iter(Bound _, a) = a 

413 
in iter end 

414 

415 

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

417 

375  418 
val logicC: class = "logic"; 
419 
val logicS: sort = [logicC]; 

420 

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

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

423 

0  424 
val propT : typ = Type("prop",[]); 
425 

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

427 

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

429 

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

431 

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

433 

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

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

436 
 strip_all_body t = t; 

437 

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

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

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

440 
(a,T) :: strip_all_vars t 
0  441 
 strip_all_vars t = [] : (string*typ) list; 
442 

443 
(*increments a term's nonlocal bound variables 

444 
required when moving a term within abstractions 

445 
inc is increment for bound variables 

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

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

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

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

449 
Abs(a, T, incr_bv(inc,lev+1,body)) 
0  450 
 incr_bv (inc, lev, f$t) = 
451 
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 

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

453 

454 
fun incr_boundvars 0 t = t 

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

456 

457 

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

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

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

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

461 
if i<lev then js else (ilev) ins_int js 
0  462 
 add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js) 
463 
 add_loose_bnos (f$t, lev, js) = 

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

464 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
0  465 
 add_loose_bnos (_, _, js) = js; 
466 

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

468 

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

470 
level k or beyond. *) 

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

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

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

474 
 loose_bvar _ = false; 

475 

2792  476 
fun loose_bvar1(Bound i,k) = i = k 
477 
 loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 

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

479 
 loose_bvar1 _ = false; 

0  480 

481 
(*Substitute arguments for loose bound variables. 

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

4626  483 
Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

487 
*) 

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

489 
let val n = length args; 

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

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

491 
(if i<lev then t (*var is locally bound*) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

492 
else incr_boundvars lev (List.nth(args, ilev)) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

493 
handle Subscript => Bound(in) (*loose: change it*)) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

494 
 subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1)) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

495 
 subst (f$t, lev) = subst(f,lev) $ subst(t,lev) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

496 
 subst (t,lev) = t 
0  497 
in case args of [] => t  _ => subst (t,0) end; 
498 

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

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

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

501 
let fun subst (t as Bound i, lev) = 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

502 
if i<lev then t (*var is locally bound*) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

503 
else if i=lev then incr_boundvars lev arg 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

504 
else Bound(i1) (*loose: change it*) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

505 
 subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1)) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

506 
 subst (f$t, lev) = subst(f,lev) $ subst(t,lev) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

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

509 

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

511 
fun betapply (Abs(_,_,t), u) = subst_bound (u,t) 
0  512 
 betapply (f,u) = f$u; 
513 

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

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

515 

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

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

518 

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

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

521 
 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

522 

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

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

524 
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

525 

0  526 
(*Tests whether 2 terms are alphaconvertible and have same type. 
4626  527 
Note that constants may have more than one type.*) 
0  528 
fun (Const(a,T)) aconv (Const(b,U)) = a=b andalso T=U 
2752  529 
 (Free(a,T)) aconv (Free(b,U)) = a=b andalso T=U 
530 
 (Var(v,T)) aconv (Var(w,U)) = eq_ix(v,w) andalso T=U 

531 
 (Bound i) aconv (Bound j) = i=j 

0  532 
 (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u andalso T=U 
2752  533 
 (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u) 
0  534 
 _ aconv _ = false; 
535 

2176  536 
(** Membership, insertion, union for terms **) 
537 

538 
fun mem_term (_, []) = false 

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

540 

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

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

542 
 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

543 

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

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

545 
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

546 

2176  547 
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; 
548 

549 
fun union_term (xs, []) = xs 

550 
 union_term ([], ys) = ys 

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

552 

5585  553 
fun inter_term ([], ys) = [] 
554 
 inter_term (x::xs, ys) = 

555 
if mem_term (x,ys) then x :: inter_term(xs,ys) else inter_term(xs,ys); 

556 

2176  557 
(** Equality, membership and insertion of sorts (string lists) **) 
558 

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

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

561 
 eq_sort (_, _) = false; 

562 

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

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

565 

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

567 

568 
fun union_sort (xs, []) = xs 

569 
 union_sort ([], ys) = ys 

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

571 

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

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

573 
 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

574 

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

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

576 
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

577 

7638  578 
val rems_sort = gen_rems eq_sort; 
579 

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

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

583 
 aconvs _ = false; 

584 

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

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

587 
fun could_unify (t,u) = 

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

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

589 
 matchrands _ = true 
0  590 
in case (head_of t , head_of u) of 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

591 
(_, Var _) => true 
0  592 
 (Var _, _) => true 
593 
 (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u) 

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

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

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

597 
 (_, Abs _) => true 

598 
 _ => false 

599 
end; 

600 

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

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

603 
 subst_free pairs = 

604 
let fun substf u = 

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

605 
case gen_assoc (op aconv) (pairs, u) of 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

606 
Some u' => u' 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

607 
 None => (case u of Abs(a,T,t) => Abs(a, T, substf t) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

608 
 t$u' => substf t $ substf u' 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

609 
 _ => u) 
0  610 
in substf end; 
611 

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

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

614 

615 

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

617 
which must contain no loose bound variables. 

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

619 
fun abstract_over (v,body) = 

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

621 
(case u of 

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

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

623 
 f$rand => abst(lev,f) $ abst(lev,rand) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

624 
 _ => u) 
0  625 
in abst(0,body) end; 
626 

11922  627 
fun lambda v t = 
628 
let val (x, T) = dest_Free v 

629 
in Abs (x, T, abstract_over (v, t)) end; 

0  630 

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

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

633 

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

635 
fun list_abs_free ([ ] , t) = t 

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

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

638 

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

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

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

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

643 

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

645 
fun list_all ([], t) = t 

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

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

648 

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

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

651 
fun subst_atomic [] t = t : term 

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

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

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

654 
 subst (f$t') = subst f $ subst t' 
9721  655 
 subst t = if_none (assoc(instl,t)) t 
0  656 
in subst t end; 
657 

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

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

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

661 
 subst(T as TFree _) = T 
9721  662 
 subst(T as TVar(ixn,_)) = if_none (assoc(iTs,ixn)) T 
0  663 
in subst T end; 
664 

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

665 
(*Substitute for type Vars in a term*) 
0  666 
val subst_TVars = map_term_types o typ_subst_TVars; 
667 

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

668 
(*Substitute for Vars in a term; see also envir/norm_term*) 
0  669 
fun subst_Vars itms t = if null itms then t else 
9721  670 
let fun subst(v as Var(ixn,_)) = if_none (assoc(itms,ixn)) v 
0  671 
 subst(Abs(a,T,t)) = Abs(a,T,subst t) 
672 
 subst(f$t) = subst f $ subst t 

673 
 subst(t) = t 

674 
in subst t end; 

675 

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

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

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

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

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

682 
 Some t => t) 

683 
 subst(b as Bound _) = b 

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

685 
 subst(f$t) = subst f $ subst t 

686 
in subst end; 

687 

688 

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

2146  690 
fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts 
0  691 
 maxidx_of_typ(TFree _) = ~1 
2146  692 
 maxidx_of_typ(TVar((_,i),_)) = i 
693 
and maxidx_of_typs [] = ~1 

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

0  695 

696 

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

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

699 
 maxidx_of_term (Bound _) = ~1 

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

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

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

0  704 

705 

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

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

709 

710 
(**** Syntaxrelated declarations ****) 

711 

712 

4626  713 
(*Dummy type for parsing and printing. Will be replaced during type inference. *) 
0  714 
val dummyT = Type("dummy",[]); 
715 

4694  716 
(*read a numeral of the given radix, normally 10*) 
717 
fun read_radixint (radix: int, cs) : int * string list = 

0  718 
let val zero = ord"0" 
719 
val limit = zero+radix 

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

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

721 
 scan (num, c::cs) = 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

722 
if zero <= ord c andalso ord c < limit 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

723 
then scan(radix*num + ord c  zero, cs) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

724 
else (num, c::cs) 
0  725 
in scan(0,cs) end; 
726 

5986  727 
fun read_int cs = read_radixint (10, cs); 
728 

729 
fun octal s = #1 (read_radixint (8, explode s)); 

730 
val oct_char = chr o octal; 

0  731 

732 

733 
(*** Printing ***) 

734 

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

12306
749a04f0cfb0
variant: preserve suffix of underscores (for skolem/internal names etc.);
wenzelm
parents:
11922
diff
changeset

736 
First attaches the suffix "a" and then increments this; 
749a04f0cfb0
variant: preserve suffix of underscores (for skolem/internal names etc.);
wenzelm
parents:
11922
diff
changeset

737 
preserves a suffix of underscores "_". *) 
749a04f0cfb0
variant: preserve suffix of underscores (for skolem/internal names etc.);
wenzelm
parents:
11922
diff
changeset

738 
fun variant bs name = 
749a04f0cfb0
variant: preserve suffix of underscores (for skolem/internal names etc.);
wenzelm
parents:
11922
diff
changeset

739 
let 
749a04f0cfb0
variant: preserve suffix of underscores (for skolem/internal names etc.);
wenzelm
parents:
11922
diff
changeset

740 
val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name)); 
749a04f0cfb0
variant: preserve suffix of underscores (for skolem/internal names etc.);
wenzelm
parents:
11922
diff
changeset

741 
fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (bump_string c) else c; 
749a04f0cfb0
variant: preserve suffix of underscores (for skolem/internal names etc.);
wenzelm
parents:
11922
diff
changeset

742 
fun vary1 c = if ((c ^ u) mem_string bs) then vary2 (c ^ "a") else c; 
749a04f0cfb0
variant: preserve suffix of underscores (for skolem/internal names etc.);
wenzelm
parents:
11922
diff
changeset

743 
in vary1 (if c = "" then "u" else c) ^ u end; 
0  744 

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

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

747 
 variantlist(b::bs, used) = 

748 
let val b' = variant used b 

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

750 

12499  751 
fun invent_names used prfx n = variantlist (Library.replicate n prfx, prfx :: used); 
752 
fun invent_type_names used = invent_names used "'"; 

11353  753 

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

754 

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

755 

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

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

757 

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

758 
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

759 
 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

760 
 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

761 

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

762 
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

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

764 

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

765 
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

766 
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

767 

9319  768 
fun add_term_consts (Const (c, _), cs) = c ins_string cs 
4017
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

769 
 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

770 
 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

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

772 

4185  773 
fun exists_Const P t = let 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

774 
fun ex (Const c ) = P c 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

775 
 ex (t $ u ) = ex t orelse ex u 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

776 
 ex (Abs (_, _, t)) = ex t 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

777 
 ex _ = false 
4185  778 
in ex t end; 
4017
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

779 

4631  780 
fun exists_subterm P = 
781 
let fun ex t = P t orelse 

782 
(case t of 

783 
u $ v => ex u orelse ex v 

784 
 Abs(_, _, u) => ex u 

785 
 _ => false) 

786 
in ex end; 

787 

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

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

789 
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

790 
 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

791 
 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

792 

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

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

794 
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

795 
 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

796 
 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

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

798 
 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

799 
 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

800 

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

801 

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

802 

0  803 
(** TFrees and TVars **) 
804 

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

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

807 

12802
c69bd9754473
added add_term_free_names (more precise/efficient than add_term_names);
wenzelm
parents:
12499
diff
changeset

808 
(*Accumulates the names of Frees in the term, suppressing duplicates.*) 
c69bd9754473
added add_term_free_names (more precise/efficient than add_term_names);
wenzelm
parents:
12499
diff
changeset

809 
fun add_term_free_names (Free(a,_), bs) = a ins_string bs 
c69bd9754473
added add_term_free_names (more precise/efficient than add_term_names);
wenzelm
parents:
12499
diff
changeset

810 
 add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs)) 
c69bd9754473
added add_term_free_names (more precise/efficient than add_term_names);
wenzelm
parents:
12499
diff
changeset

811 
 add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs) 
c69bd9754473
added add_term_free_names (more precise/efficient than add_term_names);
wenzelm
parents:
12499
diff
changeset

812 
 add_term_free_names (_, bs) = bs; 
c69bd9754473
added add_term_free_names (more precise/efficient than add_term_names);
wenzelm
parents:
12499
diff
changeset

813 

0  814 
(*Accumulates the names in the term, suppressing duplicates. 
815 
Includes Frees and Consts. For choosing unambiguous bound var names.*) 

10666  816 
fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs 
2176  817 
 add_term_names (Free(a,_), bs) = a ins_string bs 
0  818 
 add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) 
819 
 add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) 

820 
 add_term_names (_, bs) = bs; 

821 

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

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

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

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

826 

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

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

2176  829 
 add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs 
0  830 
 add_typ_tfree_names(TVar(_),fs) = fs; 
831 

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

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

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

835 

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

836 
fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames (Ts,nms) 
2176  837 
 add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms 
838 
 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

839 

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

842 

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

844 
val add_term_tfrees = it_term_types add_typ_tfrees; 

845 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

846 

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

847 
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

848 

0  849 
(*Nonlist versions*) 
850 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

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

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

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

854 

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

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

856 

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

857 
fun add_typ_ixns(ixns,Type(_,Ts)) = foldl add_typ_ixns (ixns,Ts) 
2176  858 
 add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

859 
else ixns@[ixn] 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

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

861 

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

862 
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

863 
 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

864 
 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

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

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

867 
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

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

869 
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

870 

0  871 
(** Frees and Vars **) 
872 

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

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

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

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

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

878 
 atless _ = false; 

879 

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

881 
fun insert_aterm (t,us) = 

882 
let fun inserta [] = [t] 

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

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

884 
if atless(t,u) then t::us 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

885 
else if t=u then us (*duplicate*) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

886 
else u :: inserta(us') 
0  887 
in inserta us end; 
888 

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

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

891 
Var _ => insert_aterm(t,vars) 

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

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

894 
 _ => vars; 

895 

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

897 

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

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

900 
Free _ => insert_aterm(t,frees) 

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

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

903 
 _ => frees; 

904 

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

906 

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

908 
having a unique name. *) 

909 
fun variant_abs (a,T,P) = 

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

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

911 
in (b, subst_bound (Free(b,T), P)) end; 
0  912 

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

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

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

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

916 
(variant (map #1 vars @ names) a, T) :: vars 
0  917 
in foldl rename_aT ([],vars) end; 
918 

919 
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

920 

1417  921 

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

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

923 

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

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

925 
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

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

927 

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

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

929 
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

930 
 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

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

932 

6548
9b108dd75c25
val foldl_map_aterms: ('a * term > 'a * term) > 'a * term > 'a * term;
wenzelm
parents:
6033
diff
changeset

933 
fun foldl_map_aterms f (x, t $ u) = 
9b108dd75c25
val foldl_map_aterms: ('a * term > 'a * term) > 'a * term > 'a * term;
wenzelm
parents:
6033
diff
changeset

934 
let val (x', t') = foldl_map_aterms f (x, t); val (x'', u') = foldl_map_aterms f (x', u); 
9b108dd75c25
val foldl_map_aterms: ('a * term > 'a * term) > 'a * term > 'a * term;
wenzelm
parents:
6033
diff
changeset

935 
in (x'', t' $ u') end 
9b108dd75c25
val foldl_map_aterms: ('a * term > 'a * term) > 'a * term > 'a * term;
wenzelm
parents:
6033
diff
changeset

936 
 foldl_map_aterms f (x, Abs (a, T, t)) = 
9b108dd75c25
val foldl_map_aterms: ('a * term > 'a * term) > 'a * term > 'a * term;
wenzelm
parents:
6033
diff
changeset

937 
let val (x', t') = foldl_map_aterms f (x, t) in (x', Abs (a, T, t')) end 
9b108dd75c25
val foldl_map_aterms: ('a * term > 'a * term) > 'a * term > 'a * term;
wenzelm
parents:
6033
diff
changeset

938 
 foldl_map_aterms f x_atom = f x_atom; 
9b108dd75c25
val foldl_map_aterms: ('a * term > 'a * term) > 'a * term > 'a * term;
wenzelm
parents:
6033
diff
changeset

939 

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

940 
(*foldl types of term*) 
8609  941 
fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T) 
942 
 foldl_term_types f (x, t as Free (_, T)) = f t (x, T) 

943 
 foldl_term_types f (x, t as Var (_, T)) = f t (x, T) 

944 
 foldl_term_types f (x, Bound _) = x 

945 
 foldl_term_types f (x, t as Abs (_, T, b)) = foldl_term_types f (f t (x, T), b) 

946 
 foldl_term_types f (x, t $ u) = foldl_term_types f (foldl_term_types f (x, t), u); 

947 

948 
fun foldl_types f = foldl_term_types (fn _ => f); 

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

949 

12499  950 
(*collect variables*) 
951 
val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs  (vs, _) => vs); 

952 
val add_tvars = foldl_types add_tvarsT; 

953 
val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs  (vs, _) => vs); 

954 
val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs  (vs, _) => vs); 

955 

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

956 

1417  957 

4444  958 
(** type and term orders **) 
959 

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

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

962 

963 

964 
(* typ_ord *) 

965 

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

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

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

969 
 typ_ord (Type _, _) = GREATER 

970 
 typ_ord (TFree _, Type _) = LESS 

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

972 
 typ_ord (TFree _, TVar _) = GREATER 

973 
 typ_ord (TVar _, Type _) = LESS 

974 
 typ_ord (TVar _, TFree _) = LESS 

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

976 
and typs_ord Ts_Us = list_ord typ_ord Ts_Us; 

977 

978 

979 
(* term_ord *) 

980 

981 
(*a linear wellfounded ACcompatible ordering for terms: 

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

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

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

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

986 

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

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

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

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

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

992 

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

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

995 
 term_ord (t, u) = 

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

997 
EQUAL => 

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

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

1000 
end 

1001 
 ord => ord) 

1002 
and hd_ord (f, g) = 

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

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

1005 

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

1007 

8408
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1008 
structure Vartab = TableFun(type key = indexname val ord = indexname_ord); 
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1009 
structure Termtab = TableFun(type key = term val ord = term_ord); 
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1010 

4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1011 
(*Substitute for type Vars in a type, version using Vartab*) 
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1012 
fun typ_subst_TVars_Vartab iTs T = if Vartab.is_empty iTs then T else 
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1013 
let fun subst(Type(a, Ts)) = Type(a, map subst Ts) 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1014 
 subst(T as TFree _) = T 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1015 
 subst(T as TVar(ixn, _)) = 
8408
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1016 
(case Vartab.lookup (iTs, ixn) of None => T  Some(U) => U) 
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1017 
in subst T end; 
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1018 

4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1019 
(*Substitute for type Vars in a term, version using Vartab*) 
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1020 
val subst_TVars_Vartab = map_term_types o typ_subst_TVars_Vartab; 
4444  1021 

1022 

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

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

1417  1026 

1027 
(** Sharing of types **) 

1028 

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

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

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

1032 

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

1034 
 type_tag T = atomic_tag T; 

1035 

4487  1036 
val memo_types = ref (Symtab.empty : typ list Symtab.table); 
1417  1037 

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

1038 
(* special case of library/find_first *) 
1417  1039 
fun find_type (T, []: typ list) = None 
1040 
 find_type (T, T'::Ts) = 

1041 
if T=T' then Some T' 

1042 
else find_type (T, Ts); 

1043 

1044 
fun compress_type T = 

1045 
let val tag = type_tag T 

6963  1046 
val tylist = Symtab.lookup_multi (!memo_types, tag) 
1417  1047 
in 
1048 
case find_type (T,tylist) of 

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1049 
Some T' => T' 
1417  1050 
 None => 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1051 
let val T' = 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1052 
case T of 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1053 
Type (a,Ts) => Type (a, map compress_type Ts) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1054 
 _ => T 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1055 
in memo_types := Symtab.update ((tag, T'::tylist), !memo_types); 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1056 
T 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1057 
end 
1417  1058 
end 
1059 
handle Match => 

1060 
let val Type (a,Ts) = T 

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

1062 

1063 
(** Sharing of atomic terms **) 

1064 

4487  1065 
val memo_terms = ref (Symtab.empty : term list Symtab.table); 
1417  1066 

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

1067 
(* special case of library/find_first *) 
1417  1068 
fun find_term (t, []: term list) = None 
1069 
 find_term (t, t'::ts) = 

1070 
if t=t' then Some t' 

1071 
else find_term (t, ts); 

1072 

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

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

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

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

1077 

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

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

1080 
 share_term t = 

1081 
let val tag = const_tag t 

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1082 
val ts = Symtab.lookup_multi (!memo_terms, tag) 
1417  1083 
in 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1084 
case find_term (t,ts) of 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1085 
Some t' => t' 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1086 
 None => (memo_terms := Symtab.update ((tag, t::ts), !memo_terms); 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1087 
t) 
1417  1088 
end; 
1089 

1090 
val compress_term = share_term o map_term_types compress_type; 

1091 

4444  1092 

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1093 
(* dummy patterns *) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1094 

b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1095 
val dummy_patternN = "dummy_pattern"; 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1096 

b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1097 
fun is_dummy_pattern (Const ("dummy_pattern", _)) = true 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1098 
 is_dummy_pattern _ = false; 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1099 

b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1100 
fun no_dummy_patterns tm = 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1101 
if not (foldl_aterms (fn (b, t) => b orelse is_dummy_pattern t) (false, tm)) then tm 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1102 
else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]); 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1103 

11903  1104 
fun replace_dummy Ts (i, Const ("dummy_pattern", T)) = 
1105 
(i + 1, list_comb (Var (("_dummy_", i), Ts > T), map Bound (0 upto length Ts  1))) 

1106 
 replace_dummy Ts (i, Abs (x, T, t)) = 

1107 
let val (i', t') = replace_dummy (T :: Ts) (i, t) 

1108 
in (i', Abs (x, T, t')) end 

1109 
 replace_dummy Ts (i, t $ u) = 

1110 
let val (i', t') = replace_dummy Ts (i, t); val (i'', u') = replace_dummy Ts (i', u) 

1111 
in (i'', t' $ u') end 

1112 
 replace_dummy _ (i, a) = (i, a); 

1113 

1114 
val replace_dummy_patterns = replace_dummy []; 

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1115 

10552  1116 
fun is_replaced_dummy_pattern ("_dummy_", _) = true 
1117 
 is_replaced_dummy_pattern _ = false; 

9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1118 

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

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

1120 

4444  1121 

1122 
structure BasicTerm: BASIC_TERM = Term; 

1123 
open BasicTerm; 