author  wenzelm 
Mon, 04 Jul 2005 17:07:12 +0200  
changeset 16678  dcbdb1373d78 
parent 16667  f56080acd176 
child 16710  3d6335ff3982 
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 

14829
cfa5fe01a7b7
moved read_int etc. to library.ML; added type 'arity';
wenzelm
parents:
14786
diff
changeset

19 
type arity 
4444  20 
datatype typ = 
21 
Type of string * typ list  

22 
TFree of string * sort  

23 
TVar of indexname * sort 

16537  24 
datatype term = 
25 
Const of string * typ  

26 
Free of string * typ  

27 
Var of indexname * typ  

28 
Bound of int  

29 
Abs of string * typ * term  

30 
op $ of term * term 

31 
exception TYPE of string * typ list * term list 

32 
exception TERM of string * term list 

4444  33 
val > : typ * typ > typ 
34 
val > : typ list * typ > typ 

35 
val is_TVar: typ > bool 

15573  36 
val is_funtype: typ > bool 
4444  37 
val domain_type: typ > typ 
4480  38 
val range_type: typ > typ 
4444  39 
val binder_types: typ > typ list 
40 
val body_type: typ > typ 

41 
val strip_type: typ > typ list * typ 

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 

16589  46 
val is_first_order: string list > term > bool 
6033
c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

47 
val dest_Type: typ > string * typ list 
15914  48 
val dest_TVar: typ > indexname * sort 
49 
val dest_TFree: typ > string * sort 

4444  50 
val dest_Const: term > string * typ 
51 
val dest_Free: term > string * typ 

52 
val dest_Var: term > indexname * typ 

53 
val type_of: term > typ 

54 
val type_of1: typ list * term > typ 

55 
val fastype_of: term > typ 

56 
val fastype_of1: typ list * term > typ 

10806  57 
val list_abs: (string * typ) list * term > term 
4444  58 
val strip_abs_body: term > term 
59 
val strip_abs_vars: term > (string * typ) list 

60 
val strip_qnt_body: string > term > term 

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

62 
val list_comb: term * term list > term 

63 
val strip_comb: term > term * term list 

64 
val head_of: term > term 

65 
val size_of_term: term > int 

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

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

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

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

16537  70 
structure Vartab: TABLE 
71 
structure Typtab: TABLE 

72 
structure Termtab: TABLE 

73 
val aconv: term * term > bool 

74 
val aconvs: term list * term list > bool 

4444  75 
val foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a 
8609  76 
val foldl_term_types: (term > 'a * typ > 'a) > 'a * term > 'a 
4444  77 
val foldl_types: ('a * typ > 'a) > 'a * term > 'a 
78 
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

79 
val foldl_map_aterms: ('a * term > 'a * term) > 'a * term > 'a * term 
15025  80 
val add_term_varnames: indexname list * term > indexname list 
81 
val term_varnames: term > indexname list 

4444  82 
val dummyT: typ 
83 
val itselfT: typ > typ 

84 
val a_itselfT: typ 

85 
val propT: typ 

86 
val implies: term 

87 
val all: typ > term 

88 
val equals: typ > term 

89 
val strip_all_body: term > term 

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

91 
val incr_bv: int * int * term > term 

92 
val incr_boundvars: int > term > term 

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

94 
val loose_bnos: term > int list 

95 
val loose_bvar: term * int > bool 

96 
val loose_bvar1: term * int > bool 

97 
val subst_bounds: term list * term > term 

98 
val subst_bound: term * term > term 

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

100 
val betapply: term * term > term 

101 
val eq_ix: indexname * indexname > bool 

102 
val ins_ix: indexname * indexname list > indexname list 

103 
val mem_ix: indexname * indexname list > bool 

104 
val mem_term: term * term list > bool 

105 
val subset_term: term list * term list > bool 

106 
val eq_set_term: term list * term list > bool 

107 
val ins_term: term * term list > term list 

108 
val union_term: term list * term list > term list 

5585  109 
val inter_term: term list * term list > term list 
4444  110 
val could_unify: term * term > bool 
111 
val subst_free: (term * term) list > term > term 

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

15797  113 
val typ_subst_atomic: (typ * typ) list > typ > typ 
16678  114 
val subst_atomic_types: (typ * typ) list > term > term 
4444  115 
val subst_vars: (indexname * typ) list * (indexname * term) list > term > term 
116 
val typ_subst_TVars: (indexname * typ) list > typ > typ 

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

118 
val incr_tvar: int > typ > typ 

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

120 
val atless: term * term > bool 

121 
val insert_aterm: term * term list > term list 

122 
val abstract_over: term * term > term 

11922  123 
val lambda: term > term > term 
4444  124 
val absfree: string * typ * term > term 
125 
val list_abs_free: (string * typ) list * term > term 

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

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

128 
val maxidx_of_typ: typ > int 

129 
val maxidx_of_typs: typ list > int 

130 
val maxidx_of_term: term > int 

13665  131 
val maxidx_of_terms: term list > int 
4444  132 
val variant: string list > string > string 
133 
val variantlist: string list * string list > string list 

16537  134 
(*note reversed order of args wrt. variant!*) 
4444  135 
val variant_abs: string * typ * term > string * term 
136 
val rename_wrt_term: term > (string * typ) list > (string * typ) list 

137 
val add_new_id: string list * string > string list 

138 
val add_typ_classes: typ * class list > class list 

139 
val add_typ_ixns: indexname list * typ > indexname list 

140 
val add_typ_tfree_names: typ * string list > string list 

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

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

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

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

145 
val add_typ_tycons: typ * string list > string list 

146 
val add_typ_varnames: typ * string list > string list 

147 
val add_term_classes: term * class list > class list 

148 
val add_term_consts: term * string list > string list 

13646  149 
val term_consts: term > string list 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
16035
diff
changeset

150 
val term_constsT: term > (string * typ) list 
4444  151 
val add_term_frees: term * term list > term list 
152 
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

153 
val add_term_free_names: term * string list > string list 
4444  154 
val add_term_names: term * string list > string list 
155 
val add_term_tfree_names: term * string list > string list 

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

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

158 
val add_term_tvar_ixns: term * indexname list > indexname list 

159 
val add_term_tvarnames: term * string list > string list 

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

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

162 
val add_term_tycons: term * string list > string list 

163 
val add_term_vars: term * term list > term list 

164 
val term_vars: term > term list 

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

4631  166 
val exists_subterm: (term > bool) > term > bool 
4444  167 
val compress_type: typ > typ 
168 
val compress_term: term > term 

15986  169 
val show_question_marks: bool ref 
4444  170 
end; 
0  171 

4444  172 
signature TERM = 
173 
sig 

174 
include BASIC_TERM 

16678  175 
val fast_indexname_ord: indexname * indexname > order 
16537  176 
val indexname_ord: indexname * indexname > order 
177 
val sort_ord: sort * sort > order 

178 
val typ_ord: typ * typ > order 

16678  179 
val fast_term_ord: term * term > order 
16537  180 
val term_ord: term * term > order 
181 
val hd_ord: term * term > order 

182 
val termless: term * term > bool 

16570  183 
val term_lpo: (string > int) > term * term > order 
12981  184 
val match_bvars: (term * term) * (string * string) list > (string * string) list 
185 
val rename_abs: term > term > term > term option 

16678  186 
val argument_type_of: term > typ 
12499  187 
val invent_names: string list > string > int > string list 
16338  188 
val map_typ: (string > string) > (string > string) > typ > typ 
189 
val map_term: (string > string) > (string > string) > (string > string) > term > term 

12499  190 
val add_tvarsT: (indexname * sort) list * typ > (indexname * sort) list 
191 
val add_tvars: (indexname * sort) list * term > (indexname * sort) list 

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

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

16678  194 
val dest_abs: string * typ * term > string * term 
14786
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

195 
val no_dummyT: typ > typ 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

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

198 
val replace_dummy_patterns: int * term > int * term 
10552  199 
val is_replaced_dummy_pattern: indexname > bool 
16035  200 
val show_dummy_patterns: term > term 
13484  201 
val adhoc_freeze_vars: term > term * string list 
14786
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

202 
val string_of_vname: indexname > string 
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

203 
val string_of_vname': indexname > string 
15612  204 
val string_of_term: term > string 
4444  205 
end; 
206 

207 
structure Term: TERM = 

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

208 
struct 
0  209 

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

211 
for resolution.*) 

16537  212 
type indexname = string * int; 
0  213 

4626  214 
(* Types are classified by sorts. *) 
0  215 
type class = string; 
216 
type sort = class list; 

14829
cfa5fe01a7b7
moved read_int etc. to library.ML; added type 'arity';
wenzelm
parents:
14786
diff
changeset

217 
type arity = string * sort list * sort; 
0  218 

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

220 
datatype typ = Type of string * typ list 

221 
 TFree of string * sort 

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

222 
 TVar of indexname * sort; 
0  223 

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

224 
(*Terms. Bound variables are indicated by depth number. 
0  225 
Free variables, (scheme) variables and constants have names. 
4626  226 
An term is "closed" if every bound variable of level "lev" 
13000  227 
is enclosed by at least "lev" abstractions. 
0  228 

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

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

231 

13000  232 
datatype term = 
0  233 
Const of string * typ 
13000  234 
 Free of string * typ 
0  235 
 Var of indexname * typ 
236 
 Bound of int 

237 
 Abs of string*typ*term 

3965  238 
 op $ of term*term; 
0  239 

16537  240 
(*Errors involving type mismatches*) 
0  241 
exception TYPE of string * typ list * term list; 
242 

16537  243 
(*Errors errors involving terms*) 
0  244 
exception TERM of string * term list; 
245 

246 
(*Note variable naming conventions! 

247 
a,b,c: string 

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

249 
i,j,m,n: int 

250 
t,u: term 

251 
v,w: indexnames 

252 
x,y: any 

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

254 
T,U: typ 

255 
*) 

256 

257 

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

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

259 

16537  260 
(*dummy type for parsing and printing etc.*) 
261 
val dummyT = Type ("dummy", []); 

262 

263 
fun no_dummyT typ = 

264 
let 

265 
fun check (T as Type ("dummy", _)) = 

266 
raise TYPE ("Illegal occurrence of '_' dummy type", [T], []) 

267 
 check (Type (_, Ts)) = List.app check Ts 

268 
 check _ = (); 

269 
in check typ; typ end; 

270 

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

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

272 

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

273 
(*handy for multiple args: [T1,...,Tn]>T gives T1>(T2> ... >T)*) 
15570  274 
val op > = Library.foldr (op >); 
6033
c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

275 

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

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

277 
 dest_Type T = raise TYPE ("dest_Type", [T], []); 
15914  278 
fun dest_TVar (TVar x) = x 
279 
 dest_TVar T = raise TYPE ("dest_TVar", [T], []); 

280 
fun dest_TFree (TFree x) = x 

281 
 dest_TFree T = raise TYPE ("dest_TFree", [T], []); 

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

282 

16537  283 

0  284 
(** Discriminators **) 
285 

7318  286 
fun is_Bound (Bound _) = true 
287 
 is_Bound _ = false; 

288 

0  289 
fun is_Const (Const _) = true 
290 
 is_Const _ = false; 

291 

292 
fun is_Free (Free _) = true 

293 
 is_Free _ = false; 

294 

295 
fun is_Var (Var _) = true 

296 
 is_Var _ = false; 

297 

298 
fun is_TVar (TVar _) = true 

299 
 is_TVar _ = false; 

300 

15573  301 
(*Differs from proofterm/is_fun in its treatment of TVar*) 
302 
fun is_funtype (Type("fun",[_,_])) = true 

303 
 is_funtype _ = false; 

304 

16537  305 

0  306 
(** Destructors **) 
307 

308 
fun dest_Const (Const x) = x 

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

310 

311 
fun dest_Free (Free x) = x 

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

313 

314 
fun dest_Var (Var x) = x 

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

316 

317 

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

4064  320 

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

323 
 binder_types _ = []; 

324 

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

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

327 
 body_type T = T; 

328 

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

330 
fun strip_type T : typ list * typ = 

331 
(binder_types T, body_type T); 

332 

333 

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

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

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

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

15570  338 
 type_of1 (Ts, Bound i) = (List.nth (Ts,i) 
339 
handle Subscript => raise TYPE("type_of: bound variable", [], [Bound i])) 

0  340 
 type_of1 (Ts, Var (_,T)) = T 
341 
 type_of1 (Ts, Abs (_,T,body)) = T > type_of1(T::Ts, body) 

13000  342 
 type_of1 (Ts, f$u) = 
0  343 
let val U = type_of1(Ts,u) 
344 
and T = type_of1(Ts,f) 

345 
in case T of 

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

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

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

348 
("type_of: type mismatch in application", [T1,U], [f$u]) 
13000  349 
 _ => raise TYPE 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

351 
[T,U], [f$u]) 
0  352 
end; 
353 

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

355 

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

13000  357 
fun fastype_of1 (Ts, f$u) = 
61  358 
(case fastype_of1 (Ts,f) of 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

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

15570  363 
 fastype_of1 (Ts, Bound i) = (List.nth(Ts,i) 
364 
handle Subscript => raise TERM("fastype_of: Bound", [Bound i])) 

13000  365 
 fastype_of1 (_, Var (_,T)) = T 
61  366 
 fastype_of1 (Ts, Abs (_,T,u)) = T > fastype_of1 (T::Ts, u); 
367 

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

0  369 

16678  370 
(*Determine the argument type of a function*) 
371 
fun argument_type_of tm = 

372 
let 

373 
fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i  1) U 

374 
 argT _ T = raise TYPE ("argument_type_of", [T], []); 

375 

376 
fun arg 0 _ (Abs (_, T, _)) = T 

377 
 arg i Ts (Abs (_, T, t)) = arg (i  1) (T :: Ts) t 

378 
 arg i Ts (t $ _) = arg (i + 1) Ts t 

379 
 arg i Ts a = argT i (fastype_of1 (Ts, a)); 

380 
in arg 0 [] tm end; 

381 

0  382 

15570  383 
val list_abs = Library.foldr (fn ((x, T), t) => Abs (x, T, t)); 
10806  384 

0  385 
(* maps (x1,...,xn)t to t *) 
13000  386 
fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t 
0  387 
 strip_abs_body u = u; 
388 

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

13000  390 
fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t 
0  391 
 strip_abs_vars u = [] : (string*typ) list; 
392 

393 

394 
fun strip_qnt_body qnt = 

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

396 
 strip t = t 

397 
in strip end; 

398 

399 
fun strip_qnt_vars qnt = 

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

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

402 
in strip end; 

403 

404 

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

15570  406 
val list_comb : term * term list > term = Library.foldl (op $); 
0  407 

408 

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

13000  410 
fun strip_comb u : term * term list = 
0  411 
let fun stripc (f$t, ts) = stripc (f, t::ts) 
13000  412 
 stripc x = x 
0  413 
in stripc(u,[]) end; 
414 

415 

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

417 
fun head_of (f$t) = head_of f 

418 
 head_of u = u; 

419 

420 

16599  421 
(*number of atoms and abstractions in a term*) 
422 
fun size_of_term tm = 

423 
let 

16678  424 
fun add_size (t $ u, n) = add_size (t, add_size (u, n)) 
425 
 add_size (Abs (_ ,_, t), n) = add_size (t, n + 1) 

426 
 add_size (_, n) = n + 1; 

427 
in add_size (tm, 0) end; 

0  428 

16678  429 
fun map_type_tvar f = 
430 
let 

431 
fun map_aux (Type (a, Ts)) = Type (a, map map_aux Ts) 

432 
 map_aux (TVar x) = f x 

433 
 map_aux T = T; 

434 
in map_aux end; 

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

435 

16678  436 
fun map_type_tfree f = 
437 
let 

438 
fun map_aux (Type (a, Ts)) = Type (a, map map_aux Ts) 

439 
 map_aux (TFree x) = f x 

440 
 map_aux T = T; 

441 
in map_aux end; 

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

442 

0  443 
fun map_term_types f = 
16678  444 
let 
445 
fun map_aux (Const (a, T)) = Const (a, f T) 

446 
 map_aux (Free (a, T)) = Free (a, f T) 

447 
 map_aux (Var (v, T)) = Var (v, f T) 

448 
 map_aux (t as Bound _) = t 

449 
 map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t) 

450 
 map_aux (t $ u) = map_aux t $ map_aux u; 

451 
in map_aux end; 

0  452 

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

454 
fun it_term_types f = 

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

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

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

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

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

460 
 iter(Bound _, a) = a 

461 
in iter end 

462 

463 

16678  464 
(** Comparing terms, types, sorts etc. **) 
16537  465 

16678  466 
(* fast syntactic comparison *) 
467 

468 
fun fast_indexname_ord ((x, i), (y, j)) = 

469 
(case int_ord (i, j) of EQUAL => fast_string_ord (x, y)  ord => ord); 

16537  470 

16599  471 
fun sort_ord SS = 
472 
if pointer_eq SS then EQUAL 

16678  473 
else list_ord fast_string_ord SS; 
474 

475 
local 

16537  476 

16678  477 
fun cons_nr (TVar _) = 0 
478 
 cons_nr (TFree _) = 1 

479 
 cons_nr (Type _) = 2; 

16537  480 

16678  481 
in 
16537  482 

483 
fun typ_ord TU = 

484 
if pointer_eq TU then EQUAL 

485 
else 

486 
(case TU of 

16678  487 
(Type (a, Ts), Type (b, Us)) => 
488 
(case fast_string_ord (a, b) of EQUAL => list_ord typ_ord (Ts, Us)  ord => ord) 

489 
 (TFree (a, S), TFree (b, S')) => 

490 
(case fast_string_ord (a, b) of EQUAL => sort_ord (S, S')  ord => ord) 

491 
 (TVar (xi, S), TVar (yj, S')) => 

492 
(case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S')  ord => ord) 

493 
 (T, U) => int_ord (cons_nr T, cons_nr U)); 

494 

495 
end; 

496 

497 
local 

498 

499 
fun cons_nr (Const _) = 0 

500 
 cons_nr (Free _) = 1 

501 
 cons_nr (Var _) = 2 

502 
 cons_nr (Bound _) = 3 

503 
 cons_nr (Abs _) = 4 

504 
 cons_nr (_ $ _) = 5; 

505 

506 
fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u) 

507 
 struct_ord (t1 $ t2, u1 $ u2) = 

508 
(case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2)  ord => ord) 

509 
 struct_ord (t, u) = int_ord (cons_nr t, cons_nr u); 

510 

511 
fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u) 

512 
 atoms_ord (t1 $ t2, u1 $ u2) = 

513 
(case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2)  ord => ord) 

514 
 atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b) 

515 
 atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y) 

516 
 atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj) 

517 
 atoms_ord (Bound i, Bound j) = int_ord (i, j) 

518 
 atoms_ord _ = sys_error "atoms_ord"; 

519 

520 
fun types_ord (Abs (_, T, t), Abs (_, U, u)) = 

521 
(case typ_ord (T, U) of EQUAL => types_ord (t, u)  ord => ord) 

522 
 types_ord (t1 $ t2, u1 $ u2) = 

523 
(case types_ord (t1, u1) of EQUAL => types_ord (t2, u2)  ord => ord) 

524 
 types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U) 

525 
 types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U) 

526 
 types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U) 

527 
 types_ord (Bound _, Bound _) = EQUAL 

528 
 types_ord _ = sys_error "types_ord"; 

529 

530 
in 

531 

532 
fun fast_term_ord tu = 

533 
if pointer_eq tu then EQUAL 

534 
else 

535 
(case struct_ord tu of 

536 
EQUAL => (case atoms_ord tu of EQUAL => types_ord tu  ord => ord) 

537 
 ord => ord); 

538 

539 
fun op aconv tu = (fast_term_ord tu = EQUAL); 

540 
fun aconvs ts_us = (list_ord fast_term_ord ts_us = EQUAL); 

541 

542 
structure Vartab = TableFun(type key = indexname val ord = fast_indexname_ord); 

543 
structure Typtab = TableFun(type key = typ val ord = typ_ord); 

544 
structure Termtab = TableFun(type key = term val ord = fast_term_ord); 

545 

546 
end; 

16537  547 

548 

549 
(* term_ord *) 

550 

551 
(*a linear wellfounded ACcompatible ordering for terms: 

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

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

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

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

16678  556 

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

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

559 

16667  560 
local 
561 

562 
fun hd_depth (t $ _, n) = hd_depth (t, n + 1) 

563 
 hd_depth p = p; 

16537  564 

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

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

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

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

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

570 

16667  571 
in 
572 

16537  573 
fun term_ord tu = 
574 
if pointer_eq tu then EQUAL 

575 
else 

576 
(case tu of 

577 
(Abs (_, T, t), Abs(_, U, u)) => 

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

16667  579 
 (t, u) => 
16537  580 
(case int_ord (size_of_term t, size_of_term u) of 
581 
EQUAL => 

582 
let 

16667  583 
val (f, m) = hd_depth (t, 0) 
584 
and (g, n) = hd_depth (u, 0); 

585 
in 

586 
(case hd_ord (f, g) of EQUAL => 

587 
(case int_ord (m, n) of EQUAL => args_ord (t, u)  ord => ord) 

588 
 ord => ord) 

589 
end 

16537  590 
 ord => ord)) 
591 
and hd_ord (f, g) = 

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

16667  593 
and args_ord (f $ t, g $ u) = 
594 
(case args_ord (f, g) of EQUAL => term_ord (t, u)  ord => ord) 

595 
 args_ord _ = EQUAL; 

16537  596 

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

598 

16667  599 
end; 
600 

601 

602 
(** Lexicographic path order on terms **) 

603 

604 
(* 

16570  605 
See Baader & Nipkow, Term rewriting, CUP 1998. 
606 
Without variables. Const, Var, Bound, Free and Abs are treated all as 

607 
constants. 

608 

609 
f_ord maps strings to integers and serves two purposes: 

610 
 Predicate on constant symbols. Those that are not recognised by f_ord 

611 
must be mapped to ~1. 

612 
 Order on the recognised symbols. These must be mapped to distinct 

613 
integers >= 0. 

614 

16667  615 
*) 
16570  616 

617 
local 

16667  618 
fun dest_hd f_ord (Const (a, T)) = 
16570  619 
let val ord = f_ord a in 
620 
if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0) 

621 
end 

622 
 dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0) 

623 
 dest_hd _ (Var v) = ((1, v), 1) 

624 
 dest_hd _ (Bound i) = ((1, (("", i), dummyT)), 2) 

625 
 dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3); 

626 

627 
fun term_lpo f_ord (s, t) = 

628 
let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in 

629 
if forall (fn si => term_lpo f_ord (si, t) = LESS) ss 

630 
then case hd_ord f_ord (f, g) of 

16667  631 
GREATER => 
632 
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts 

633 
then GREATER else LESS 

16570  634 
 EQUAL => 
16667  635 
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts 
636 
then list_ord (term_lpo f_ord) (ss, ts) 

637 
else LESS 

16570  638 
 LESS => LESS 
639 
else GREATER 

640 
end 

641 
and hd_ord f_ord (f, g) = case (f, g) of 

642 
(Abs (_, T, t), Abs (_, U, u)) => 

643 
(case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U)  ord => ord) 

644 
 (_, _) => prod_ord (prod_ord int_ord 

645 
(prod_ord indexname_ord typ_ord)) int_ord 

646 
(dest_hd f_ord f, dest_hd f_ord g) 

647 
in 

648 
val term_lpo = term_lpo 

649 
end; 

650 

16537  651 

0  652 
(** Connectives of higher order logic **) 
653 

375  654 
fun itselfT ty = Type ("itself", [ty]); 
14854  655 
val a_itselfT = itselfT (TFree ("'a", [])); 
375  656 

0  657 
val propT : typ = Type("prop",[]); 
658 

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

660 

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

662 

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

664 

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

13000  666 
fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t 
0  667 
 strip_all_body t = t; 
668 

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

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

13000  671 
(a,T) :: strip_all_vars t 
0  672 
 strip_all_vars t = [] : (string*typ) list; 
673 

674 
(*increments a term's nonlocal bound variables 

675 
required when moving a term within abstractions 

676 
inc is increment for bound variables 

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

13000  678 
fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u 
0  679 
 incr_bv (inc, lev, Abs(a,T,body)) = 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

680 
Abs(a, T, incr_bv(inc,lev+1,body)) 
13000  681 
 incr_bv (inc, lev, f$t) = 
0  682 
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 
683 
 incr_bv (inc, lev, u) = u; 

684 

685 
fun incr_boundvars 0 t = t 

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

687 

12981  688 
(*Scan a pair of terms; while they are similar, 
689 
accumulate corresponding bound vars in "al"*) 

690 
fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = 

691 
match_bvs(s, t, if x="" orelse y="" then al 

692 
else (x,y)::al) 

693 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 

694 
 match_bvs(_,_,al) = al; 

695 

696 
(* strip abstractions created by parameters *) 

697 
fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al); 

698 

699 
fun rename_abs pat obj t = 

700 
let 

701 
val ren = match_bvs (pat, obj, []); 

702 
fun ren_abs (Abs (x, T, b)) = 

16678  703 
Abs (if_none (assoc_string (ren, x)) x, T, ren_abs b) 
12981  704 
 ren_abs (f $ t) = ren_abs f $ ren_abs t 
705 
 ren_abs t = t 

15531  706 
in if null ren then NONE else SOME (ren_abs t) end; 
0  707 

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

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

13000  710 
fun add_loose_bnos (Bound i, lev, js) = 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

711 
if i<lev then js else (ilev) ins_int js 
0  712 
 add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js) 
713 
 add_loose_bnos (f$t, lev, js) = 

13000  714 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
0  715 
 add_loose_bnos (_, _, js) = js; 
716 

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

718 

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

720 
level k or beyond. *) 

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

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

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

724 
 loose_bvar _ = false; 

725 

2792  726 
fun loose_bvar1(Bound i,k) = i = k 
727 
 loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 

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

729 
 loose_bvar1 _ = false; 

0  730 

731 
(*Substitute arguments for loose bound variables. 

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

4626  733 
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

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

737 
*) 

13000  738 
fun subst_bounds (args: term list, t) : term = 
0  739 
let val n = length args; 
740 
fun subst (t as Bound i, lev) = 

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

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

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

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

744 
 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

745 
 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

746 
 subst (t,lev) = t 
0  747 
in case args of [] => t  _ => subst (t,0) end; 
748 

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

749 
(*Special case: one argument*) 
13000  750 
fun subst_bound (arg, t) : term = 
2192
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

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

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

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

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

755 
 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

756 
 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

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

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

759 

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

761 
fun betapply (Abs(_,_,t), u) = subst_bound (u,t) 
0  762 
 betapply (f,u) = f$u; 
763 

14786
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

764 

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

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

766 

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

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

769 

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

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

772 
 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

773 

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

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

775 
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

776 

0  777 

2176  778 
(** Membership, insertion, union for terms **) 
779 

780 
fun mem_term (_, []) = false 

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

782 

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

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

784 
 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

785 

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

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

787 
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

788 

2176  789 
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; 
790 

791 
fun union_term (xs, []) = xs 

792 
 union_term ([], ys) = ys 

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

794 

5585  795 
fun inter_term ([], ys) = [] 
796 
 inter_term (x::xs, ys) = 

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

798 

13000  799 
(*A fast unification filter: true unless the two terms cannot be unified. 
0  800 
Terms must be NORMAL. Treats all Vars as distinct. *) 
801 
fun could_unify (t,u) = 

802 
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

803 
 matchrands _ = true 
0  804 
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

805 
(_, Var _) => true 
0  806 
 (Var _, _) => true 
807 
 (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u) 

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

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

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

811 
 (_, Abs _) => true 

812 
 _ => false 

813 
end; 

814 

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

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

817 
 subst_free pairs = 

13000  818 
let fun substf u = 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

819 
case gen_assoc (op aconv) (pairs, u) of 
15531  820 
SOME u' => u' 
821 
 NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t) 

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

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

823 
 _ => u) 
0  824 
in substf end; 
825 

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

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

828 

829 

13000  830 
(*Abstraction of the term "body" over its occurrences of v, 
0  831 
which must contain no loose bound variables. 
832 
The resulting term is ready to become the body of an Abs.*) 

833 
fun abstract_over (v,body) = 

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

835 
(case u of 

836 
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

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

838 
 _ => u) 
0  839 
in abst(0,body) end; 
840 

13665  841 
fun lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t)) 
842 
 lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t)) 

843 
 lambda v t = raise TERM ("lambda", [v, t]); 

0  844 

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

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

847 

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

849 
fun list_abs_free ([ ] , t) = t 

13000  850 
 list_abs_free ((a,T)::vars, t) = 
0  851 
absfree(a, T, list_abs_free(vars,t)); 
852 

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

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

13000  855 
 list_all_free ((a,T)::vars, t) = 
0  856 
(all T) $ (absfree(a, T, list_all_free(vars,t))); 
857 

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

859 
fun list_all ([], t) = t 

13000  860 
 list_all ((a,T)::vars, t) = 
0  861 
(all T) $ (Abs(a, T, list_all(vars,t))); 
862 

16678  863 
(*Replace the ATOMIC term ti by ui; inst = [(t1,u1), ..., (tn,un)]. 
0  864 
A simultaneous substitution: [ (a,b), (b,a) ] swaps a and b. *) 
16678  865 
fun subst_atomic [] tm = tm 
866 
 subst_atomic inst tm = 

867 
let 

868 
fun subst (Abs (a, T, body)) = Abs (a, T, subst body) 

869 
 subst (t $ u) = subst t $ subst u 

870 
 subst t = if_none (gen_assoc (op aconv) (inst, t)) t; 

871 
in subst tm end; 

0  872 

16678  873 
(*Replace the ATOMIC type Ti by Ui; inst = [(T1,U1), ..., (Tn,Un)].*) 
874 
fun typ_subst_atomic [] ty = ty 

875 
 typ_subst_atomic inst ty = 

876 
let 

877 
fun subst (Type (a, Ts)) = Type (a, map subst Ts) 

878 
 subst T = if_none (gen_assoc (op = : typ * typ > bool) (inst, T)) T; 

879 
in subst ty end; 

15797  880 

16678  881 
fun subst_atomic_types [] tm = tm 
882 
 subst_atomic_types inst tm = map_term_types (typ_subst_atomic inst) tm; 

883 

884 
fun typ_subst_TVars [] ty = ty 

885 
 typ_subst_TVars inst ty = 

886 
let 

887 
fun subst (Type (a, Ts)) = Type (a, map subst Ts) 

888 
 subst (T as TVar (xi, _)) = if_none (assoc_string_int (inst, xi)) T 

889 
 subst T = T; 

890 
in subst ty end; 

0  891 

16678  892 
fun subst_TVars [] tm = tm 
893 
 subst_TVars inst tm = map_term_types (typ_subst_TVars inst) tm; 

0  894 

16678  895 
(*see also Envir.norm_term*) 
896 
fun subst_Vars [] tm = tm 

897 
 subst_Vars inst tm = 

898 
let 

899 
fun subst (t as Var (xi, _)) = if_none (assoc_string_int (inst, xi)) t 

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

901 
 subst (t $ u) = subst t $ subst u 

902 
 subst t = t; 

903 
in subst tm end; 

0  904 

16678  905 
(*see also Envir.norm_term*) 
906 
fun subst_vars ([], []) tm = tm 

907 
 subst_vars ([], inst) tm = subst_Vars inst tm 

908 
 subst_vars (instT, inst) tm = 

909 
let 

910 
fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T) 

911 
 subst (Free (a, T)) = Free (a, typ_subst_TVars instT T) 

912 
 subst (t as Var (xi, T)) = 

913 
(case assoc_string_int (inst, xi) of 

914 
NONE => Var (xi, typ_subst_TVars instT T) 

915 
 SOME t => t) 

916 
 subst (t as Bound _) = t 

917 
 subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t) 

918 
 subst (t $ u) = subst t $ subst u; 

919 
in subst tm end; 

0  920 

921 

15573  922 
(** Identifying firstorder terms **) 
923 

924 
(*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*) 

925 
fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t))); 

926 

16537  927 
(*First order means in all terms of the form f(t1,...,tn) no argument has a 
16589  928 
function type. The supplied quantifiers are excluded: their argument always 
929 
has a function type through a recursive call into its body.*) 

16667  930 
fun is_first_order quants = 
16589  931 
let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body 
16667  932 
 first_order1 Ts (Const(q,_) $ Abs(a,T,body)) = 
933 
q mem_string quants andalso (*it is a known quantifier*) 

16589  934 
not (is_funtype T) andalso first_order1 (T::Ts) body 
16667  935 
 first_order1 Ts t = 
936 
case strip_comb t of 

937 
(Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts 

938 
 (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts 

939 
 (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts 

940 
 (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts 

941 
 (Abs _, ts) => false (*not in betanormal form*) 

942 
 _ => error "first_order: unexpected case" 

16589  943 
in first_order1 [] end; 
15573  944 

0  945 
(*Computing the maximum index of a typ*) 
2146  946 
fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts 
0  947 
 maxidx_of_typ(TFree _) = ~1 
2146  948 
 maxidx_of_typ(TVar((_,i),_)) = i 
949 
and maxidx_of_typs [] = ~1 

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

0  951 

952 

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

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

955 
 maxidx_of_term (Bound _) = ~1 

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

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

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

0  960 

15570  961 
fun maxidx_of_terms ts = Library.foldl Int.max (~1, map maxidx_of_term ts); 
13665  962 

0  963 

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

16678  965 
fun incr_tvar 0 T = T 
966 
 incr_tvar k T = map_type_tvar (fn ((a,i),S) => TVar((a,i+k),S)) T; 

0  967 

968 

969 
(**** Syntaxrelated declarations ****) 

970 

971 
(*** Printing ***) 

972 

14676  973 
(*Makes a variant of a name distinct from the names in bs. 
974 
First attaches the suffix and then increments this; 

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

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

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

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

978 
val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name)); 
12902  979 
fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_string c) else c; 
14676  980 
fun vary1 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_init c) else c; 
12306
749a04f0cfb0
variant: preserve suffix of underscores (for skolem/internal names etc.);
wenzelm
parents:
11922
diff
changeset

981 
in vary1 (if c = "" then "u" else c) ^ u end; 
0  982 

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

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

13000  985 
 variantlist(b::bs, used) = 
0  986 
let val b' = variant used b 
987 
in b' :: variantlist (bs, b'::used) end; 

988 

14695  989 
(*Invent fresh names*) 
990 
fun invent_names _ _ 0 = [] 

991 
 invent_names used a n = 

992 
let val b = Symbol.bump_string a in 

993 
if a mem_string used then invent_names used b n 

994 
else a :: invent_names used b (n  1) 

995 
end; 

11353  996 

16537  997 

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

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

999 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15573
diff
changeset

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

1001 
 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

1002 
 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

1003 

16294  1004 
fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (c ins_string cs) Ts 
4017
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

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

1006 

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

1007 
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

1008 
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

1009 

9319  1010 
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

1011 
 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

1012 
 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

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

1014 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
16035
diff
changeset

1015 
fun add_term_constsT (Const c, cs) = c::cs 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
16035
diff
changeset

1016 
 add_term_constsT (t $ u, cs) = add_term_constsT (t, add_term_constsT (u, cs)) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
16035
diff
changeset

1017 
 add_term_constsT (Abs (_, _, t), cs) = add_term_constsT (t, cs) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
16035
diff
changeset

1018 
 add_term_constsT (_, cs) = cs; 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
16035
diff
changeset

1019 

13646  1020 
fun term_consts t = add_term_consts(t,[]); 
1021 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
16035
diff
changeset

1022 
fun term_constsT t = add_term_constsT(t,[]); 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
16035
diff
changeset

1023 

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

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

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

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

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

1030 

4631  1031 
fun exists_subterm P = 
1032 
let fun ex t = P t orelse 

1033 
(case t of 

1034 
u $ v => ex u orelse ex v 

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

1036 
 _ => false) 

1037 
in ex end; 

1038 

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

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

1040 
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

1041 
 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

1042 
 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

1043 

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

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

1045 
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

1046 
 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

1047 
 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

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

1049 
 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

1050 
 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

1051 

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

1052 

0  1053 
(** TFrees and TVars **) 
1054 

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

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

1057 

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

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

1059 
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

1060 
 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

1061 
 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

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

1063 

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

10666  1066 
fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs 
2176  1067 
 add_term_names (Free(a,_), bs) = a ins_string bs 
0  1068 
 add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) 
1069 
 add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) 

1070 
 add_term_names (_, bs) = bs; 

1071 

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

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15573
diff
changeset

1073 
fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts 
0  1074 
 add_typ_tvars(TFree(_),vs) = vs 
16294  1075 
 add_typ_tvars(TVar(v),vs) = insert (op =) v vs; 
0  1076 

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

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15573
diff
changeset

1078 
fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts 
2176  1079 
 add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs 
0  1080 
 add_typ_tfree_names(TVar(_),fs) = fs; 
1081 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15573
diff
changeset

1082 
fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts 
16294  1083 
 add_typ_tfrees(TFree(f),fs) = insert (op =) f fs 
0  1084 
 add_typ_tfrees(TVar(_),fs) = fs; 
1085 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15573
diff
changeset

1086 
fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts 
2176  1087 
 add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms 
1088 
 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

1089 

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

1092 

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

1094 
val add_term_tfrees = it_term_types add_typ_tfrees; 

1095 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

1096 

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

1097 
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

1098 

0  1099 
(*Nonlist versions*) 
1100 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

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

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

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

1104 

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

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

1106 

15570  1107 
fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts) 
13000  1108 
 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

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

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

1111 

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

1112 
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

1113 
 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

1114 
 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

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

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

1117 
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

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

1119 
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

1120 

16537  1121 

0  1122 
(** Frees and Vars **) 
1123 

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

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

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

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

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

1129 
 atless _ = false; 

1130 

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

1132 
fun insert_aterm (t,us) = 

1133 
let fun inserta [] = [t] 

13000  1134 
 inserta (us as u::us') = 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

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

1137 
else u :: inserta(us') 
0  1138 
in inserta us end; 
1139 

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

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

1142 
Var _ => insert_aterm(t,vars) 

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

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

1145 
 _ => vars; 

1146 

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

1148 

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

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

1151 
Free _ => insert_aterm(t,frees) 

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

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

1154 
 _ => frees; 

1155 

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

1157 

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

16678  1159 
having a unique name*) 
0  1160 
fun variant_abs (a,T,P) = 
1161 
let val b = variant (add_term_names(P,[])) a 

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

1162 
in (b, subst_bound (Free(b,T), P)) end; 
0  1163 

16678  1164 
fun dest_abs (x, T, body) = 
1165 
let 

1166 
fun name_clash (Free (y, _)) = (x = y) 

1167 
 name_clash (t $ u) = name_clash t orelse name_clash u 

1168 
 name_clash (Abs (_, _, t)) = name_clash t 

1169 
 name_clash _ = false; 

1170 
in 

1171 
if name_clash body then 

1172 
dest_abs (variant [x] x, T, body) (*potentially slow, but rarely happens*) 

1173 
else (x, subst_bound (Free (x, T), body)) 

1174 
end; 

1175 

0  1176 
(* renames and reverses the strings in vars away from names *) 
1177 
fun rename_aTs names vars : (string*typ)list = 

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

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

1179 
(variant (map #1 vars @ names) a, T) :: vars 
15570  1180 
in Library.foldl rename_aT ([],vars) end; 
0  1181 

1182 
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

1183 

1417  1184 

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

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

1186 

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

1187 
(*foldl atoms of type*) 
15570  1188 
fun foldl_atyps f (x, Type (_, Ts)) = Library.foldl (foldl_atyps f) (x, Ts) 
4286
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

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

1190 

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

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

1192 
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

1193 
 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

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

1195 

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

1196 
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

1197 
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

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

1199 
 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

1200 
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

1201 
 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

1202 

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

1203 
(*foldl types of term*) 
8609  1204 
fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T) 
1205 
 foldl_term_types f (x, t as Free (_, T)) = f t (x, T) 

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

1207 
 foldl_term_types f (x, Bound _) = x 

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

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

1210 

1211 
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

1212 

12499  1213 
(*collect variables*) 
16294  1214 
val add_tvarsT = foldl_atyps (fn (vs, TVar v) => insert (op =) v vs  (vs, _) => vs); 
12499  1215 
val add_tvars = foldl_types add_tvarsT; 
16294  1216 
val add_vars = foldl_aterms (fn (vs, Var v) => insert (op =) v vs  (vs, _) => vs); 
1217 
val add_frees = foldl_aterms (fn (vs, Free v) => insert (op =) v vs  (vs, _) => vs); 

12499  1218 

15025  1219 
(*collect variable names*) 
1220 
val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs)  (xs, _) => xs); 

1221 
fun term_varnames t = add_term_varnames ([], t); 

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

1222 

1417  1223 

4444  1224 

13000  1225 
(*** Compression of terms and types by sharing common subtrees. 
1226 
Saves 5075% on storage requirements. As it is a bit slow, 

1227 
it should be called only for axioms, stored theorems, etc. 

1228 
Recorded term and type fragments are never disposed. ***) 

1417  1229 

16338  1230 

1417  1231 
(** Sharing of types **) 
1232 

13000  1233 
val memo_types = ref (Typtab.empty: typ Typtab.table); 
1417  1234 

1235 
fun compress_type T = 

13000  1236 
(case Typtab.lookup (! memo_types, T) of 
15531  1237 
SOME T' => T' 
1238 
 NONE => 

13000  1239 
let val T' = (case T of Type (a, Ts) => Type (a, map compress_type Ts)  _ => T) 
1240 
in memo_types := Typtab.update ((T', T'), ! memo_types); T' end); 

1241 

1417  1242 

1243 
(** Sharing of atomic terms **) 

1244 

13000  1245 
val memo_terms = ref (Termtab.empty : term Termtab.table); 
1417  1246 

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

13000  1248 
 share_term (Abs (a, T, u)) = Abs (a, T, share_term u) 
1417  1249 
 share_term t = 
13000  1250 
(case Termtab.lookup (! memo_terms, t) of 
15531  1251 
SOME t' => t' 
1252 
 NONE => (memo_terms := Termtab.update ((t, t), ! memo_terms); t)); 

1417  1253 

1254 
val compress_term = share_term o map_term_types compress_type; 

1255 

4444  1256 

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

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

1258 

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

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

1260 

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

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

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

1263 

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

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

1265 
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

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

1267 

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

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

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

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

1273 
 replace_dummy Ts (i, t $ u) = 

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

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

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

1277 

1278 
val replace_dummy_patterns = replace_dummy []; 

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

1279 

10552  1280 
fun is_replaced_dummy_pattern ("_dummy_", _) = true 
1281 
 is_replaced_dummy_pattern _ = false; 

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

1282 

16035  1283 
fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T) 
1284 
 show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u 

1285 
 show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t) 

1286 
 show_dummy_patterns a = a; 

1287 

13484  1288 

1289 
(* adhoc freezing *) 

1290 

1291 
fun adhoc_freeze_vars tm = 

1292 
let 

1293 
fun mk_inst (var as Var ((a, i), T)) = 

1294 
let val x = a ^ Library.gensym "_" ^ string_of_int i 

1295 
in ((var, Free(x, T)), x) end; 

1296 
val (insts, xs) = split_list (map mk_inst (term_vars tm)); 

1297 
in (subst_atomic insts tm, xs) end; 

1298 

1299 

14786
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

1300 
(* string_of_vname *) 
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

1301 

15986  1302 
val show_question_marks = ref true; 
15472  1303 

14786
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

1304 
fun string_of_vname (x, i) = 
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

1305 
let 
15986  1306 
val question_mark = if ! show_question_marks then "?" else ""; 
1307 
val idx = string_of_int i; 

1308 
val dot = 

1309 
(case rev (Symbol.explode x) of 

1310 
_ :: "\\<^isub>" :: _ => false 

1311 
 _ :: "\\<^isup>" :: _ => false 

1312 
 c :: _ => Symbol.is_digit c 

1313 
 _ => true); 

14786
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

1314 
in 
15986  1315 
if dot then question_mark ^ x ^ "." ^ idx 
1316 
else if i <> 0 then question_mark ^ x ^ idx 

1317 
else question_mark ^ x 

14786
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

1318 
end; 
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

1319 

24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

1320 
fun string_of_vname' (x, ~1) = x 
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

1321 
 string_of_vname' xi = string_of_vname xi; 
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

1322 

15612  1323 
fun string_of_term (Const(s,_)) = s 
1324 
 string_of_term (Free(s,_)) = s 

1325 
 string_of_term (Var(ix,_)) = string_of_vname ix 

1326 
 string_of_term (Bound i) = string_of_int i 

1327 
 string_of_term (Abs(x,_,t)) = "%" ^ x ^ ". " ^ string_of_term t 

1328 
 string_of_term (s $ t) = 

1329 
"(" ^ string_of_term s ^ " " ^ string_of_term t ^ ")" 

1330 

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

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

1332 

4444  1333 
structure BasicTerm: BASIC_TERM = Term; 
1334 
open BasicTerm; 