author  wenzelm 
Fri, 07 Oct 2005 22:59:24 +0200  
changeset 17786  f06d6498ebf0 
parent 17777  05f5532a8289 
child 17851  2fa4f9b54761 
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  

17756  30 
$ of term * term 
16537  31 
exception TYPE of string * typ list * term list 
32 
exception TERM of string * term list 

16710  33 
val dummyT: typ 
34 
val no_dummyT: typ > typ 

4444  35 
val > : typ * typ > typ 
36 
val > : typ list * typ > typ 

16710  37 
val dest_Type: typ > string * typ list 
38 
val dest_TVar: typ > indexname * sort 

39 
val dest_TFree: typ > string * sort 

40 
val is_Bound: term > bool 

41 
val is_Const: term > bool 

42 
val is_Free: term > bool 

43 
val is_Var: term > bool 

4444  44 
val is_TVar: typ > bool 
15573  45 
val is_funtype: typ > bool 
16710  46 
val dest_Const: term > string * typ 
47 
val dest_Free: term > string * typ 

48 
val dest_Var: term > indexname * typ 

4444  49 
val domain_type: typ > typ 
4480  50 
val range_type: typ > typ 
4444  51 
val binder_types: typ > typ list 
52 
val body_type: typ > typ 

53 
val strip_type: typ > typ list * typ 

16710  54 
val type_of1: typ list * term > typ 
4444  55 
val type_of: term > typ 
16710  56 
val fastype_of1: typ list * term > typ 
4444  57 
val fastype_of: term > typ 
10806  58 
val list_abs: (string * typ) list * term > term 
4444  59 
val strip_abs_body: term > term 
60 
val strip_abs_vars: term > (string * typ) list 

61 
val strip_qnt_body: string > term > term 

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

63 
val list_comb: term * term list > term 

64 
val strip_comb: term > term * term list 

65 
val head_of: term > term 

66 
val size_of_term: term > int 

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

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

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

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

16943  71 
val fold_atyps: (typ > 'a > 'a) > typ > 'a > 'a 
72 
val fold_aterms: (term > 'a > 'a) > term > 'a > 'a 

73 
val fold_term_types: (term > typ > 'a > 'a) > term > 'a > 'a 

74 
val fold_types: (typ > 'a > 'a) > term > 'a > 'a 

75 
val add_term_names: term * string list > string list 

76 
val add_term_varnames: term > indexname list > indexname list 

77 
val term_varnames: term > indexname list 

16710  78 
val aconv: term * term > bool 
79 
val aconvs: term list * term list > bool 

16537  80 
structure Vartab: TABLE 
81 
structure Typtab: TABLE 

82 
structure Termtab: TABLE 

4444  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 betapply: term * term > term 

100 
val eq_ix: indexname * indexname > bool 

101 
val ins_ix: indexname * indexname list > indexname list 

102 
val mem_ix: indexname * indexname list > bool 

103 
val mem_term: term * term list > bool 

104 
val subset_term: term list * term list > bool 

105 
val eq_set_term: term list * term list > bool 

106 
val ins_term: term * term list > term list 

107 
val union_term: term list * term list > term list 

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

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

112 
val abstract_over: term * term > term 

11922  113 
val lambda: term > term > term 
4444  114 
val absfree: string * typ * term > term 
17786  115 
val absdummy: typ * term > term 
4444  116 
val list_abs_free: (string * typ) list * term > term 
117 
val list_all_free: (string * typ) list * term > term 

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

16710  119 
val subst_atomic: (term * term) list > term > term 
120 
val typ_subst_atomic: (typ * typ) list > typ > typ 

121 
val subst_atomic_types: (typ * typ) list > term > term 

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

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

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

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

126 
val is_first_order: string list > term > bool 

4444  127 
val maxidx_of_typ: typ > int 
128 
val maxidx_of_typs: typ list > int 

129 
val maxidx_of_term: term > int 

130 
val variant: string list > string > string 

131 
val variantlist: string list * string list > string list 

16537  132 
(*note reversed order of args wrt. variant!*) 
4444  133 
val add_typ_classes: typ * class list > class list 
134 
val add_typ_tycons: typ * string list > string list 

135 
val add_term_classes: term * class list > class list 

16710  136 
val add_term_tycons: term * string list > string list 
4444  137 
val add_term_consts: term * string list > string list 
13646  138 
val term_consts: term > string list 
16943  139 
val exists_subterm: (term > bool) > term > bool 
16710  140 
val exists_Const: (string * typ > bool) > term > bool 
141 
val add_term_free_names: term * string list > string list 

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

143 
val add_typ_tfree_names: typ * string list > string list 

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

145 
val add_typ_varnames: typ * string list > string list 

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

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

148 
val add_term_tfree_names: term * string list > string list 

149 
val add_term_tvarnames: term * string list > string list 

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

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

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

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

154 
val add_typ_ixns: indexname list * typ > indexname list 

155 
val add_term_tvar_ixns: term * indexname list > indexname list 

156 
val add_term_vars: term * term list > term list 

157 
val term_vars: term > term list 

4444  158 
val add_term_frees: term * term list > term list 
159 
val term_frees: term > term list 

16710  160 
val variant_abs: string * typ * term > string * term 
161 
val rename_wrt_term: term > (string * typ) list > (string * typ) list 

15986  162 
val show_question_marks: bool ref 
4444  163 
end; 
0  164 

4444  165 
signature TERM = 
166 
sig 

167 
include BASIC_TERM 

16710  168 
val argument_type_of: term > typ 
16943  169 
val add_tvarsT: typ > (indexname * sort) list > (indexname * sort) list 
170 
val add_tvars: term > (indexname * sort) list > (indexname * sort) list 

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

172 
val add_tfreesT: typ > (string * sort) list > (string * sort) list 

173 
val add_tfrees: term > (string * sort) list > (string * sort) list 

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

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 

16943  186 
val eq_tvar: (indexname * sort) * (indexname * sort) > bool 
16882  187 
val eq_var: (indexname * typ) * (indexname * typ) > bool 
16943  188 
val tvar_ord: (indexname * sort) * (indexname * sort) > order 
189 
val var_ord: (indexname * typ) * (indexname * typ) > order 

16882  190 
val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list 
191 
> term > term 

192 
val instantiateT: ((indexname * sort) * typ) list > typ > typ 

16710  193 
val maxidx_typ: typ > int > int 
194 
val maxidx_typs: typ list > int > int 

195 
val maxidx_term: term > int > int 

12499  196 
val invent_names: string list > string > int > string list 
16338  197 
val map_typ: (string > string) > (string > string) > typ > typ 
198 
val map_term: (string > string) > (string > string) > (string > string) > term > term 

16710  199 
val dest_abs: string * typ * term > string * term 
16990  200 
val bound: int > string 
201 
val is_bound: string > bool 

16943  202 
val zero_var_indexesT: typ > typ 
203 
val zero_var_indexes: term > term 

204 
val zero_var_indexes_inst: term > 

205 
((indexname * sort) * typ) list * ((indexname * typ) * term) list 

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

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

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

208 
val replace_dummy_patterns: int * term > int * term 
10552  209 
val is_replaced_dummy_pattern: indexname > bool 
16035  210 
val show_dummy_patterns: term > term 
13484  211 
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

212 
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

213 
val string_of_vname': indexname > string 
17777
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

214 
val str_of_term: term > string 
4444  215 
end; 
216 

217 
structure Term: TERM = 

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

218 
struct 
0  219 

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

221 
for resolution.*) 

16537  222 
type indexname = string * int; 
0  223 

4626  224 
(* Types are classified by sorts. *) 
0  225 
type class = string; 
226 
type sort = class list; 

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

227 
type arity = string * sort list * sort; 
0  228 

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

230 
datatype typ = Type of string * typ list 

231 
 TFree of string * sort 

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

232 
 TVar of indexname * sort; 
0  233 

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

234 
(*Terms. Bound variables are indicated by depth number. 
0  235 
Free variables, (scheme) variables and constants have names. 
4626  236 
An term is "closed" if every bound variable of level "lev" 
13000  237 
is enclosed by at least "lev" abstractions. 
0  238 

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

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

241 

13000  242 
datatype term = 
0  243 
Const of string * typ 
13000  244 
 Free of string * typ 
0  245 
 Var of indexname * typ 
246 
 Bound of int 

247 
 Abs of string*typ*term 

3965  248 
 op $ of term*term; 
0  249 

16537  250 
(*Errors involving type mismatches*) 
0  251 
exception TYPE of string * typ list * term list; 
252 

16537  253 
(*Errors errors involving terms*) 
0  254 
exception TERM of string * term list; 
255 

256 
(*Note variable naming conventions! 

257 
a,b,c: string 

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

259 
i,j,m,n: int 

260 
t,u: term 

261 
v,w: indexnames 

262 
x,y: any 

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

264 
T,U: typ 

265 
*) 

266 

267 

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

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

269 

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

272 

273 
fun no_dummyT typ = 

274 
let 

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

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

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

278 
 check _ = (); 

279 
in check typ; typ end; 

280 

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

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

282 

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

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

285 

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

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

287 
 dest_Type T = raise TYPE ("dest_Type", [T], []); 
15914  288 
fun dest_TVar (TVar x) = x 
289 
 dest_TVar T = raise TYPE ("dest_TVar", [T], []); 

290 
fun dest_TFree (TFree x) = x 

291 
 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

292 

16537  293 

0  294 
(** Discriminators **) 
295 

7318  296 
fun is_Bound (Bound _) = true 
297 
 is_Bound _ = false; 

298 

0  299 
fun is_Const (Const _) = true 
300 
 is_Const _ = false; 

301 

302 
fun is_Free (Free _) = true 

303 
 is_Free _ = false; 

304 

305 
fun is_Var (Var _) = true 

306 
 is_Var _ = false; 

307 

308 
fun is_TVar (TVar _) = true 

309 
 is_TVar _ = false; 

310 

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

313 
 is_funtype _ = false; 

314 

16537  315 

0  316 
(** Destructors **) 
317 

318 
fun dest_Const (Const x) = x 

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

320 

321 
fun dest_Free (Free x) = x 

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

323 

324 
fun dest_Var (Var x) = x 

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

326 

327 

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

4064  330 

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

333 
 binder_types _ = []; 

334 

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

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

337 
 body_type T = T; 

338 

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

340 
fun strip_type T : typ list * typ = 

341 
(binder_types T, body_type T); 

342 

343 

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

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

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

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

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

0  350 
 type_of1 (Ts, Var (_,T)) = T 
351 
 type_of1 (Ts, Abs (_,T,body)) = T > type_of1(T::Ts, body) 

13000  352 
 type_of1 (Ts, f$u) = 
0  353 
let val U = type_of1(Ts,u) 
354 
and T = type_of1(Ts,f) 

355 
in case T of 

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

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

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

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

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

361 
[T,U], [f$u]) 
0  362 
end; 
363 

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

365 

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

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

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

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

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

13000  375 
 fastype_of1 (_, Var (_,T)) = T 
61  376 
 fastype_of1 (Ts, Abs (_,T,u)) = T > fastype_of1 (T::Ts, u); 
377 

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

0  379 

16678  380 
(*Determine the argument type of a function*) 
381 
fun argument_type_of tm = 

382 
let 

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

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

385 

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

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

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

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

390 
in arg 0 [] tm end; 

391 

0  392 

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

0  395 
(* maps (x1,...,xn)t to t *) 
13000  396 
fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t 
0  397 
 strip_abs_body u = u; 
398 

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

13000  400 
fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t 
0  401 
 strip_abs_vars u = [] : (string*typ) list; 
402 

403 

404 
fun strip_qnt_body qnt = 

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

406 
 strip t = t 

407 
in strip end; 

408 

409 
fun strip_qnt_vars qnt = 

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

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

412 
in strip end; 

413 

414 

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

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

418 

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

13000  420 
fun strip_comb u : term * term list = 
0  421 
let fun stripc (f$t, ts) = stripc (f, t::ts) 
13000  422 
 stripc x = x 
0  423 
in stripc(u,[]) end; 
424 

425 

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

427 
fun head_of (f$t) = head_of f 

428 
 head_of u = u; 

429 

430 

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

433 
let 

16678  434 
fun add_size (t $ u, n) = add_size (t, add_size (u, n)) 
435 
 add_size (Abs (_ ,_, t), n) = add_size (t, n + 1) 

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

437 
in add_size (tm, 0) end; 

0  438 

16678  439 
fun map_type_tvar f = 
440 
let 

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

442 
 map_aux (TVar x) = f x 

443 
 map_aux T = T; 

444 
in map_aux end; 

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

445 

16678  446 
fun map_type_tfree f = 
447 
let 

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

449 
 map_aux (TFree x) = f x 

450 
 map_aux T = T; 

451 
in map_aux end; 

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

452 

0  453 
fun map_term_types f = 
16678  454 
let 
455 
fun map_aux (Const (a, T)) = Const (a, f T) 

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

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

458 
 map_aux (t as Bound _) = t 

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

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

461 
in map_aux end; 

0  462 

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

464 
fun it_term_types f = 

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

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

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

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

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

470 
 iter(Bound _, a) = a 

471 
in iter end 

472 

473 

16943  474 
(* fold types and terms *) 
475 

476 
(*fold atoms of type*) 

477 
fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts 

478 
 fold_atyps f T = f T; 

479 

480 
(*fold atoms of term*) 

481 
fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u 

482 
 fold_aterms f (Abs (_, _, t)) = fold_aterms f t 

483 
 fold_aterms f a = f a; 

484 

485 
(*fold types of term*) 

486 
fun fold_term_types f (t as Const (_, T)) = f t T 

487 
 fold_term_types f (t as Free (_, T)) = f t T 

488 
 fold_term_types f (t as Var (_, T)) = f t T 

489 
 fold_term_types f (Bound _) = I 

490 
 fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b 

491 
 fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u; 

492 

493 
fun fold_types f = fold_term_types (K f); 

494 

495 
(*collect variables*) 

496 
val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v  _ => I); 

497 
val add_tvars = fold_types add_tvarsT; 

498 
val add_vars = fold_aterms (fn Var v => insert (op =) v  _ => I); 

499 
val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v  _ => I); 

500 
val add_tfrees = fold_types add_tfreesT; 

501 
val add_frees = fold_aterms (fn Free v => insert (op =) v  _ => I); 

502 

503 
(*collect variable names*) 

504 
val add_term_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi  _ => I); 

505 
fun term_varnames t = add_term_varnames t []; 

506 

507 

16678  508 
(** Comparing terms, types, sorts etc. **) 
16537  509 

16678  510 
(* fast syntactic comparison *) 
511 

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

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

16537  514 

16599  515 
fun sort_ord SS = 
516 
if pointer_eq SS then EQUAL 

16990  517 
else dict_ord fast_string_ord SS; 
16678  518 

519 
local 

16537  520 

16678  521 
fun cons_nr (TVar _) = 0 
522 
 cons_nr (TFree _) = 1 

523 
 cons_nr (Type _) = 2; 

16537  524 

16678  525 
in 
16537  526 

527 
fun typ_ord TU = 

528 
if pointer_eq TU then EQUAL 

529 
else 

530 
(case TU of 

16678  531 
(Type (a, Ts), Type (b, Us)) => 
16990  532 
(case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us)  ord => ord) 
16678  533 
 (TFree (a, S), TFree (b, S')) => 
534 
(case fast_string_ord (a, b) of EQUAL => sort_ord (S, S')  ord => ord) 

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

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

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

538 

539 
end; 

540 

541 
local 

542 

543 
fun cons_nr (Const _) = 0 

544 
 cons_nr (Free _) = 1 

545 
 cons_nr (Var _) = 2 

546 
 cons_nr (Bound _) = 3 

547 
 cons_nr (Abs _) = 4 

548 
 cons_nr (_ $ _) = 5; 

549 

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

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

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

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

554 

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

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

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

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

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

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

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

562 
 atoms_ord _ = sys_error "atoms_ord"; 

563 

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

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

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

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

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

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

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

571 
 types_ord (Bound _, Bound _) = EQUAL 

572 
 types_ord _ = sys_error "types_ord"; 

573 

574 
in 

575 

576 
fun fast_term_ord tu = 

577 
if pointer_eq tu then EQUAL 

578 
else 

579 
(case struct_ord tu of 

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

581 
 ord => ord); 

582 

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

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

585 

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

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

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

589 

590 
end; 

16537  591 

592 

593 
(* term_ord *) 

594 

595 
(*a linear wellfounded ACcompatible ordering for terms: 

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

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

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

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

16678  600 

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

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

603 

16667  604 
local 
605 

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

607 
 hd_depth p = p; 

16537  608 

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

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

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

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

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

614 

16667  615 
in 
616 

16537  617 
fun term_ord tu = 
618 
if pointer_eq tu then EQUAL 

619 
else 

620 
(case tu of 

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

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

16667  623 
 (t, u) => 
16537  624 
(case int_ord (size_of_term t, size_of_term u) of 
625 
EQUAL => 

16943  626 
(case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of 
627 
EQUAL => args_ord (t, u)  ord => ord) 

16537  628 
 ord => ord)) 
629 
and hd_ord (f, g) = 

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

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

633 
 args_ord _ = EQUAL; 

16537  634 

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

636 

16667  637 
end; 
638 

639 

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

641 

642 
(* 

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

645 
constants. 

646 

647 
f_ord maps strings to integers and serves two purposes: 

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

649 
must be mapped to ~1. 

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

651 
integers >= 0. 

652 

16667  653 
*) 
16570  654 

655 
local 

16667  656 
fun dest_hd f_ord (Const (a, T)) = 
16570  657 
let val ord = f_ord a in 
658 
if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0) 

659 
end 

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

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

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

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

664 

665 
fun term_lpo f_ord (s, t) = 

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

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

668 
then case hd_ord f_ord (f, g) of 

16667  669 
GREATER => 
670 
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts 

671 
then GREATER else LESS 

16570  672 
 EQUAL => 
16667  673 
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts 
674 
then list_ord (term_lpo f_ord) (ss, ts) 

675 
else LESS 

16570  676 
 LESS => LESS 
677 
else GREATER 

678 
end 

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

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

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

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

683 
(prod_ord indexname_ord typ_ord)) int_ord 

684 
(dest_hd f_ord f, dest_hd f_ord g) 

685 
in 

686 
val term_lpo = term_lpo 

687 
end; 

688 

16537  689 

0  690 
(** Connectives of higher order logic **) 
691 

375  692 
fun itselfT ty = Type ("itself", [ty]); 
14854  693 
val a_itselfT = itselfT (TFree ("'a", [])); 
375  694 

0  695 
val propT : typ = Type("prop",[]); 
696 

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

698 

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

700 

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

702 

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

13000  704 
fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t 
0  705 
 strip_all_body t = t; 
706 

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

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

13000  709 
(a,T) :: strip_all_vars t 
0  710 
 strip_all_vars t = [] : (string*typ) list; 
711 

712 
(*increments a term's nonlocal bound variables 

713 
required when moving a term within abstractions 

714 
inc is increment for bound variables 

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

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

718 
Abs(a, T, incr_bv(inc,lev+1,body)) 
13000  719 
 incr_bv (inc, lev, f$t) = 
0  720 
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 
721 
 incr_bv (inc, lev, u) = u; 

722 

723 
fun incr_boundvars 0 t = t 

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

725 

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

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

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

730 
else (x,y)::al) 

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

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

733 

734 
(* strip abstractions created by parameters *) 

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

736 

737 
fun rename_abs pat obj t = 

738 
let 

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

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

17271  741 
Abs (if_none (AList.lookup (op =) ren x) x, T, ren_abs b) 
12981  742 
 ren_abs (f $ t) = ren_abs f $ ren_abs t 
743 
 ren_abs t = t 

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

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

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

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

749 
if i<lev then js else (ilev) ins_int js 
0  750 
 add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js) 
751 
 add_loose_bnos (f$t, lev, js) = 

13000  752 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
0  753 
 add_loose_bnos (_, _, js) = js; 
754 

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

756 

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

758 
level k or beyond. *) 

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

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

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

762 
 loose_bvar _ = false; 

763 

2792  764 
fun loose_bvar1(Bound i,k) = i = k 
765 
 loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 

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

767 
 loose_bvar1 _ = false; 

0  768 

769 
(*Substitute arguments for loose bound variables. 

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

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

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

775 
*) 

13000  776 
fun subst_bounds (args: term list, t) : term = 
0  777 
let val n = length args; 
778 
fun subst (t as Bound i, lev) = 

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

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

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

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

782 
 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

783 
 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

784 
 subst (t,lev) = t 
0  785 
in case args of [] => t  _ => subst (t,0) end; 
786 

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

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

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

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

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

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

793 
 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

794 
 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

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

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

797 

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

799 
fun betapply (Abs(_,_,t), u) = subst_bound (u,t) 
0  800 
 betapply (f,u) = f$u; 
801 

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

802 

16882  803 
(** Specialized equality, membership, insertion etc. **) 
2192
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

804 

16882  805 
(* indexnames *) 
806 

16724  807 
fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y; 
2192
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

808 

2959  809 
fun mem_ix (_, []) = false 
16882  810 
 mem_ix (x, y :: ys) = eq_ix (x, y) orelse mem_ix (x, ys); 
2192
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

811 

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

813 

0  814 

16882  815 
(* variables *) 
816 

16943  817 
fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S'; 
818 
fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T'; 

819 

820 
val tvar_ord = prod_ord indexname_ord sort_ord; 

821 
val var_ord = prod_ord indexname_ord typ_ord; 

16882  822 

823 

824 
(* terms *) 

2176  825 

826 
fun mem_term (_, []) = false 

16882  827 
 mem_term (t, t'::ts) = t aconv t' orelse mem_term (t, ts); 
2176  828 

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

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

830 
 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

831 

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

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

833 
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

834 

2176  835 
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; 
836 

837 
fun union_term (xs, []) = xs 

838 
 union_term ([], ys) = ys 

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

840 

5585  841 
fun inter_term ([], ys) = [] 
842 
 inter_term (x::xs, ys) = 

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

844 

16882  845 

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

849 
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

850 
 matchrands _ = true 
0  851 
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

852 
(_, Var _) => true 
0  853 
 (Var _, _) => true 
854 
 (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u) 

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

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

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

858 
 (_, Abs _) => true 

859 
 _ => false 

860 
end; 

861 

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

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

864 
 subst_free pairs = 

13000  865 
let fun substf u = 
17314  866 
case AList.lookup (op aconv) pairs u of 
15531  867 
SOME u' => u' 
868 
 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

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

870 
 _ => u) 
0  871 
in substf end; 
872 

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

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

875 

876 

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

16882  880 
fun abstract_over (v, body) = 
881 
let 

16990  882 
exception SAME; 
883 
fun abs lev tm = 

884 
if v aconv tm then Bound lev 

16882  885 
else 
16990  886 
(case tm of 
887 
Abs (a, T, t) => Abs (a, T, abs (lev + 1) t) 

888 
 t $ u => (abs lev t $ (abs lev u handle SAME => u) handle SAME => t $ abs lev u) 

889 
 _ => raise SAME); 

890 
in abs 0 body handle SAME => body end; 

0  891 

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

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

0  895 

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

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

17786  898 
fun absdummy (T, body) = Abs ("uu", T, body); 
0  899 

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

901 
fun list_abs_free ([ ] , t) = t 

13000  902 
 list_abs_free ((a,T)::vars, t) = 
0  903 
absfree(a, T, list_abs_free(vars,t)); 
904 

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

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

13000  907 
 list_all_free ((a,T)::vars, t) = 
0  908 
(all T) $ (absfree(a, T, list_all_free(vars,t))); 
909 

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

911 
fun list_all ([], t) = t 

13000  912 
 list_all ((a,T)::vars, t) = 
0  913 
(all T) $ (Abs(a, T, list_all(vars,t))); 
914 

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

919 
let 

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

921 
 subst (t $ u) = subst t $ subst u 

17314  922 
 subst t = if_none (AList.lookup (op aconv) inst t) t; 
16678  923 
in subst tm end; 
0  924 

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

927 
 typ_subst_atomic inst ty = 

928 
let 

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

17314  930 
 subst T = if_none (AList.lookup (op = : typ * typ > bool) inst T) T; 
16678  931 
in subst ty end; 
15797  932 

16678  933 
fun subst_atomic_types [] tm = tm 
934 
 subst_atomic_types inst tm = map_term_types (typ_subst_atomic inst) tm; 

935 

936 
fun typ_subst_TVars [] ty = ty 

937 
 typ_subst_TVars inst ty = 

938 
let 

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

17271  940 
 subst (T as TVar (xi, _)) = if_none (AList.lookup (op =) inst xi) T 
16678  941 
 subst T = T; 
942 
in subst ty end; 

0  943 

16678  944 
fun subst_TVars [] tm = tm 
945 
 subst_TVars inst tm = map_term_types (typ_subst_TVars inst) tm; 

0  946 

16678  947 
(*see also Envir.norm_term*) 
948 
fun subst_Vars [] tm = tm 

949 
 subst_Vars inst tm = 

950 
let 

17271  951 
fun subst (t as Var (xi, _)) = if_none (AList.lookup (op =) inst xi) t 
16678  952 
 subst (Abs (a, T, t)) = Abs (a, T, subst t) 
953 
 subst (t $ u) = subst t $ subst u 

954 
 subst t = t; 

955 
in subst tm end; 

0  956 

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

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

960 
 subst_vars (instT, inst) tm = 

961 
let 

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

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

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

17271  965 
(case AList.lookup (op =) inst xi of 
16678  966 
NONE => Var (xi, typ_subst_TVars instT T) 
967 
 SOME t => t) 

968 
 subst (t as Bound _) = t 

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

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

971 
in subst tm end; 

0  972 

973 

16943  974 
(* instantiation of schematic variables (types before terms) *) 
16882  975 

976 
local exception SAME in 

977 

16943  978 
fun instantiateT_same [] _ = raise SAME 
979 
 instantiateT_same instT ty = 

16882  980 
let 
981 
fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts) 

982 
 subst_typ (TVar v) = 

17314  983 
(case AList.lookup eq_tvar instT v of 
16882  984 
SOME T => T 
985 
 NONE => raise SAME) 

986 
 subst_typ _ = raise SAME 

987 
and subst_typs (T :: Ts) = 

988 
(subst_typ T :: (subst_typs Ts handle SAME => Ts) 

989 
handle SAME => T :: subst_typs Ts) 

990 
 subst_typs [] = raise SAME; 

991 
in subst_typ ty end; 

992 

993 
fun instantiate ([], []) tm = tm 

994 
 instantiate (instT, inst) tm = 

995 
let 

16943  996 
val substT = instantiateT_same instT; 
997 
fun subst (Const (c, T)) = Const (c, substT T) 

998 
 subst (Free (x, T)) = Free (x, substT T) 

16882  999 
 subst (Var (xi, T)) = 
16943  1000 
let val (T', same) = (substT T, false) handle SAME => (T, true) in 
17314  1001 
(case AList.lookup eq_var inst (xi, T') of 
16882  1002 
SOME t => t 
1003 
 NONE => if same then raise SAME else Var (xi, T')) 

1004 
end 

1005 
 subst (Bound _) = raise SAME 

1006 
 subst (Abs (x, T, t)) = 

16943  1007 
(Abs (x, substT T, subst t handle SAME => t) 
16882  1008 
handle SAME => Abs (x, T, subst t)) 
1009 
 subst (t $ u) = (subst t $ (subst u handle SAME => u) handle SAME => t $ subst u); 

1010 
in subst tm handle SAME => tm end; 

1011 

1012 
fun instantiateT instT ty = 

16943  1013 
instantiateT_same instT ty handle SAME => ty; 
16882  1014 

1015 
end; 

1016 

1017 

15573  1018 
(** Identifying firstorder terms **) 
1019 

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

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

1022 

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

16667  1026 
fun is_first_order quants = 
16589  1027 
let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body 
16667  1028 
 first_order1 Ts (Const(q,_) $ Abs(a,T,body)) = 
1029 
q mem_string quants andalso (*it is a known quantifier*) 

16589  1030 
not (is_funtype T) andalso first_order1 (T::Ts) body 
16667  1031 
 first_order1 Ts t = 
1032 
case strip_comb t of 

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

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

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

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

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

1038 
 _ => error "first_order: unexpected case" 

16589  1039 
in first_order1 [] end; 
15573  1040 

16710  1041 

16990  1042 
(* maximum index of typs and terms *) 
0  1043 

16710  1044 
fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j) 
1045 
 maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i 

1046 
 maxidx_typ (TFree _) i = i 

1047 
and maxidx_typs [] i = i 

1048 
 maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i); 

0  1049 

16710  1050 
fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j)) 
1051 
 maxidx_term (Const (_, T)) i = maxidx_typ T i 

1052 
 maxidx_term (Free (_, T)) i = maxidx_typ T i 

1053 
 maxidx_term (Bound _) i = i 

1054 
 maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i) 

1055 
 maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i); 

0  1056 

16710  1057 
fun maxidx_of_typ T = maxidx_typ T ~1; 
1058 
fun maxidx_of_typs Ts = maxidx_typs Ts ~1; 

1059 
fun maxidx_of_term t = maxidx_term t ~1; 

13665  1060 

0  1061 

1062 

1063 
(**** Syntaxrelated declarations ****) 

1064 

1065 
(*** Printing ***) 

1066 

16943  1067 
(*Makes a variant of a name distinct from the names in 'used'. 
14676  1068 
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

1069 
preserves a suffix of underscores "_". *) 
16943  1070 
fun variant used name = 
12306
749a04f0cfb0
variant: preserve suffix of underscores (for skolem/internal names etc.);
wenzelm
parents:
11922
diff
changeset

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

1072 
val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name)); 
16943  1073 
fun vary2 c = if ((c ^ u) mem_string used) then vary2 (Symbol.bump_string c) else c; 
1074 
fun vary1 c = if ((c ^ u) mem_string used) 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

1075 
in vary1 (if c = "" then "u" else c) ^ u end; 
0  1076 

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

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

13000  1079 
 variantlist(b::bs, used) = 
0  1080 
let val b' = variant used b 
1081 
in b' :: variantlist (bs, b'::used) end; 

1082 

14695  1083 
(*Invent fresh names*) 
1084 
fun invent_names _ _ 0 = [] 

1085 
 invent_names used a n = 

1086 
let val b = Symbol.bump_string a in 

1087 
if a mem_string used then invent_names used b n 

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

1089 
end; 

11353  1090 

16537  1091 

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

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

1093 

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

1094 
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

1095 
 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

1096 
 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

1097 

16294  1098 
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

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

1100 

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

1101 
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

1102 
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

1103 

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

1105 
 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

1106 
 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

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

1108 

13646  1109 
fun term_consts t = add_term_consts(t,[]); 
1110 

16943  1111 
fun exists_subterm P = 
1112 
let 

1113 
fun ex tm = P tm orelse 

1114 
(case tm of 

1115 
t $ u => ex t orelse ex u 

1116 
 Abs (_, _, t) => ex t 

1117 
 _ => false); 

1118 
in ex end; 

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

1119 

16943  1120 
fun exists_Const P = exists_subterm (fn Const c => P c  _ => false); 
4631  1121 

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

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

1123 
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

1124 
 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

1125 
 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

1126 

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

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

1128 
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

1129 
 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

1130 
 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

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

1132 
 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

1133 
 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

1134 

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

1135 

0  1136 
(** TFrees and TVars **) 
1137 

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

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

1139 
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

1140 
 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

1141 
 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

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

1143 

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

10666  1146 
fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs 
2176  1147 
 add_term_names (Free(a,_), bs) = a ins_string bs 
0  1148 
 add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) 
1149 
 add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) 

1150 
 add_term_names (_, bs) = bs; 

1151 

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

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

1153 
fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts 
0  1154 
 add_typ_tvars(TFree(_),vs) = vs 
16294  1155 
 add_typ_tvars(TVar(v),vs) = insert (op =) v vs; 
0  1156 

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

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

1158 
fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts 
2176  1159 
 add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs 
0  1160 
 add_typ_tfree_names(TVar(_),fs) = fs; 
1161 

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

1162 
fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts 
16294  1163 
 add_typ_tfrees(TFree(f),fs) = insert (op =) f fs 
0  1164 
 add_typ_tfrees(TVar(_),fs) = fs; 
1165 

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

1166 
fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts 
2176  1167 
 add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms 
1168 
 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

1169 

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

1172 

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

1174 
val add_term_tfrees = it_term_types add_typ_tfrees; 

1175 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

1176 

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

1177 
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

1178 

0  1179 
(*Nonlist versions*) 
1180 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

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

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

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

1184 

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

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

1186 

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

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

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

1191 

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

1192 
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

1193 
 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

1194 
 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

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

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

1197 
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

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

1199 
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

1200 

16537  1201 

0  1202 
(** Frees and Vars **) 
1203 

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

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

16990  1206 
Var _ => OrdList.insert term_ord t vars 
0  1207 
 Abs (_,_,body) => add_term_vars(body,vars) 
1208 
 f$t => add_term_vars (f, add_term_vars(t, vars)) 

1209 
 _ => vars; 

1210 

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

1212 

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

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

16990  1215 
Free _ => OrdList.insert term_ord t frees 
0  1216 
 Abs (_,_,body) => add_term_frees(body,frees) 
1217 
 f$t => add_term_frees (f, add_term_frees(t, frees)) 

1218 
 _ => frees; 

1219 

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

1221 

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

16678  1223 
having a unique name*) 
0  1224 
fun variant_abs (a,T,P) = 
1225 
let val b = variant (add_term_names(P,[])) a 

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

1226 
in (b, subst_bound (Free(b,T), P)) end; 
0  1227 

16678  1228 
fun dest_abs (x, T, body) = 
1229 
let 

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

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

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

1233 
 name_clash _ = false; 

1234 
in 

1235 
if name_clash body then 

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

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

1238 
end; 

1239 

16990  1240 
(*names for numbered variables  
1241 
preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*) 

1242 
local 

1243 
val small_int = Vector.tabulate (1000, fn i => 

1244 
let val leading = if i < 10 then "00" else if i < 100 then "0" else "" 

1245 
in ":" ^ leading ^ string_of_int i end); 

1246 
in 

1247 
fun bound n = 

1248 
if n < 1000 then Vector.sub (small_int, n) 

1249 
else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000); 

1250 
end; 

1251 

1252 
val is_bound = String.isPrefix ":"; 

16943  1253 

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

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

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

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

1260 
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

1261 

1417  1262 

16943  1263 
(* zero var indexes *) 
4286
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

1264 

16943  1265 
fun zero_var_inst vars = 
1266 
fold (fn v as ((x, i), X) => fn (used, inst) => 

1267 
let 

17642  1268 
val x' = variant used (if is_bound x then "u" else x); 
16943  1269 
val used' = x' :: used; 
1270 
in if x = x' andalso i = 0 then (used', inst) else (used', (v, ((x', 0), X)) :: inst) end) 

1271 
vars ([], []) > #2; 

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

1272 

16943  1273 
fun zero_var_indexesT ty = 
1274 
instantiateT (map (apsnd TVar) (zero_var_inst (sort tvar_ord (add_tvarsT ty [])))) ty; 

16790  1275 

16943  1276 
fun zero_var_indexes_inst tm = 
1277 
let 

1278 
val instT = map (apsnd TVar) (zero_var_inst (sort tvar_ord (fold_types add_tvarsT tm []))); 

1279 
val inst = 

1280 
add_vars tm [] > map (apsnd (instantiateT instT)) 

1281 
> sort var_ord > zero_var_inst > map (apsnd Var); 

1282 
in (instT, inst) end; 

12499  1283 

16943  1284 
fun zero_var_indexes tm = instantiate (zero_var_indexes_inst tm) tm; 
4286
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

1285 

1417  1286 

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

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

1288 

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

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

1290 

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

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

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

1293 

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

1294 
fun no_dummy_patterns tm = 
16787  1295 
if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

1297 

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

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

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

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

1303 
 replace_dummy Ts (i, t $ u) = 

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

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

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

1307 

1308 
val replace_dummy_patterns = replace_dummy []; 

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

1309 

10552  1310 
fun is_replaced_dummy_pattern ("_dummy_", _) = true 
1311 
 is_replaced_dummy_pattern _ = false; 

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

1312 

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

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

1316 
 show_dummy_patterns a = a; 

1317 

13484  1318 

1319 
(* adhoc freezing *) 

1320 

1321 
fun adhoc_freeze_vars tm = 

1322 
let 

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

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

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

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

1327 
in (subst_atomic insts tm, xs) end; 

1328 

1329 

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

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

1331 

15986  1332 
val show_question_marks = ref true; 
15472  1333 

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

1334 
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

1335 
let 
15986  1336 
val question_mark = if ! show_question_marks then "?" else ""; 
1337 
val idx = string_of_int i; 

1338 
val dot = 

1339 
(case rev (Symbol.explode x) of 

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

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

1342 
 c :: _ => Symbol.is_digit c 

1343 
 _ => true); 

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

1344 
in 
15986  1345 
if dot then question_mark ^ x ^ "." ^ idx 
1346 
else if i <> 0 then question_mark ^ x ^ idx 

1347 
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

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

1349 

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

1350 
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

1351 
 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

1352 

17777
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1353 

05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1354 
(* str_of_term *) 
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1355 

05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1356 
fun str_of_term (Const (c, _)) = c 
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1357 
 str_of_term (Free (x, _)) = x 
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1358 
 str_of_term (Var (xi, _)) = string_of_vname xi 
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1359 
 str_of_term (Bound i) = string_of_int i 
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1360 
 str_of_term (Abs (x, _, t)) = "%" ^ x ^ ". " ^ str_of_term t 
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1361 
 str_of_term (t $ u) = "(" ^ str_of_term t ^ " " ^ str_of_term u ^ ")"; 
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1362 

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

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

1364 

4444  1365 
structure BasicTerm: BASIC_TERM = Term; 
1366 
open BasicTerm; 