author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 18253  0626a0a217ec 
child 18847  5fac129ae936 
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 

18149  78 
val find_free: term > string > term option 
16710  79 
val aconv: term * term > bool 
80 
val aconvs: term list * term list > bool 

16537  81 
structure Vartab: TABLE 
82 
structure Typtab: TABLE 

83 
structure Termtab: TABLE 

4444  84 
val itselfT: typ > typ 
85 
val a_itselfT: typ 

86 
val propT: typ 

87 
val implies: term 

88 
val all: typ > term 

89 
val equals: typ > term 

90 
val strip_all_body: term > term 

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

92 
val incr_bv: int * int * term > term 

93 
val incr_boundvars: int > term > term 

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

95 
val loose_bnos: term > int list 

96 
val loose_bvar: term * int > bool 

97 
val loose_bvar1: term * int > bool 

98 
val subst_bounds: term list * term > term 

99 
val subst_bound: term * term > term 

100 
val betapply: term * term > term 

18183  101 
val betapplys: term * term list > term 
4444  102 
val eq_ix: indexname * indexname > bool 
103 
val ins_ix: indexname * indexname list > indexname list 

104 
val mem_ix: indexname * indexname list > bool 

105 
val mem_term: term * term list > bool 

106 
val ins_term: term * term list > term list 

107 
val could_unify: term * term > bool 

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

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

110 
val abstract_over: term * term > term 

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

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

16710  117 
val subst_atomic: (term * term) list > term > term 
118 
val typ_subst_atomic: (typ * typ) list > typ > typ 

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

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

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

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

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

124 
val is_first_order: string list > term > bool 

4444  125 
val maxidx_of_typ: typ > int 
126 
val maxidx_of_typs: typ list > int 

127 
val maxidx_of_term: term > int 

128 
val variant: string list > string > string 

129 
val variantlist: string list * string list > string list 

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

133 
val add_term_classes: term * class list > class list 

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

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

141 
val add_typ_tfree_names: typ * string list > string list 

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

143 
val add_typ_varnames: typ * string list > string list 

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

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

146 
val add_term_tfree_names: term * string list > string list 

147 
val add_term_tvarnames: term * string list > string list 

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

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

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

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

152 
val add_typ_ixns: indexname list * typ > indexname list 

153 
val add_term_tvar_ixns: term * indexname list > indexname list 

154 
val add_term_vars: term * term list > term list 

155 
val term_vars: term > term list 

4444  156 
val add_term_frees: term * term list > term list 
157 
val term_frees: term > term list 

16710  158 
val variant_abs: string * typ * term > string * term 
159 
val rename_wrt_term: term > (string * typ) list > (string * typ) list 

15986  160 
val show_question_marks: bool ref 
4444  161 
end; 
0  162 

4444  163 
signature TERM = 
164 
sig 

165 
include BASIC_TERM 

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

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

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

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

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

16678  173 
val fast_indexname_ord: indexname * indexname > order 
16537  174 
val indexname_ord: indexname * indexname > order 
175 
val sort_ord: sort * sort > order 

176 
val typ_ord: typ * typ > order 

16678  177 
val fast_term_ord: term * term > order 
16537  178 
val term_ord: term * term > order 
179 
val hd_ord: term * term > order 

180 
val termless: term * term > bool 

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

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

16882  188 
val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list 
189 
> term > term 

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

16710  191 
val maxidx_typ: typ > int > int 
192 
val maxidx_typs: typ list > int > int 

193 
val maxidx_term: term > int > int 

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

16710  197 
val dest_abs: string * typ * term > string * term 
16990  198 
val bound: int > string 
199 
val is_bound: string > bool 

16943  200 
val zero_var_indexesT: typ > typ 
201 
val zero_var_indexes: term > term 

202 
val zero_var_indexes_inst: term > 

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

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

204 
val dummy_patternN: string 
18253  205 
val dummy_pattern: typ > term 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

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

211 
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

212 
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

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

216 
structure Term: TERM = 

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

217 
struct 
0  218 

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

220 
for resolution.*) 

16537  221 
type indexname = string * int; 
0  222 

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

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

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

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

229 
datatype typ = Type of string * typ list 

230 
 TFree of string * sort 

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

231 
 TVar of indexname * sort; 
0  232 

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

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

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

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

240 

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

246 
 Abs of string*typ*term 

3965  247 
 op $ of term*term; 
0  248 

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

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

255 
(*Note variable naming conventions! 

256 
a,b,c: string 

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

258 
i,j,m,n: int 

259 
t,u: term 

260 
v,w: indexnames 

261 
x,y: any 

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

263 
T,U: typ 

264 
*) 

265 

266 

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

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

268 

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

271 

272 
fun no_dummyT typ = 

273 
let 

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

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

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

277 
 check _ = (); 

278 
in check typ; typ end; 

279 

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

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

281 

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

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

284 

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

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

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

289 
fun dest_TFree (TFree x) = x 

290 
 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

291 

16537  292 

0  293 
(** Discriminators **) 
294 

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

297 

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

300 

301 
fun is_Free (Free _) = true 

302 
 is_Free _ = false; 

303 

304 
fun is_Var (Var _) = true 

305 
 is_Var _ = false; 

306 

307 
fun is_TVar (TVar _) = true 

308 
 is_TVar _ = false; 

309 

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

312 
 is_funtype _ = false; 

313 

16537  314 

0  315 
(** Destructors **) 
316 

317 
fun dest_Const (Const x) = x 

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

319 

320 
fun dest_Free (Free x) = x 

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

322 

323 
fun dest_Var (Var x) = x 

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

325 

326 

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

4064  329 

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

332 
 binder_types _ = []; 

333 

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

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

336 
 body_type T = T; 

337 

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

339 
fun strip_type T : typ list * typ = 

340 
(binder_types T, body_type T); 

341 

342 

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

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

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

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

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

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

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

354 
in case T of 

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

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

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

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

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

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

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

364 

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

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

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

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

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

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

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

0  378 

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

381 
let 

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

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

384 

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

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

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

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

389 
in arg 0 [] tm end; 

390 

0  391 

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

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

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

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

402 

403 
fun strip_qnt_body qnt = 

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

405 
 strip t = t 

406 
in strip end; 

407 

408 
fun strip_qnt_vars qnt = 

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

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

411 
in strip end; 

412 

413 

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

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

417 

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

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

424 

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

426 
fun head_of (f$t) = head_of f 

427 
 head_of u = u; 

428 

429 

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

432 
let 

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

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

436 
in add_size (tm, 0) end; 

0  437 

16678  438 
fun map_type_tvar f = 
439 
let 

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

441 
 map_aux (TVar x) = f x 

442 
 map_aux T = T; 

443 
in map_aux end; 

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

444 

16678  445 
fun map_type_tfree f = 
446 
let 

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

448 
 map_aux (TFree x) = f x 

449 
 map_aux T = T; 

450 
in map_aux end; 

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

451 

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

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

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

457 
 map_aux (t as Bound _) = t 

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

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

460 
in map_aux end; 

0  461 

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

463 
fun it_term_types f = 

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

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

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

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

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

469 
 iter(Bound _, a) = a 

470 
in iter end 

471 

472 

16943  473 
(* fold types and terms *) 
474 

475 
(*fold atoms of type*) 

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

477 
 fold_atyps f T = f T; 

478 

479 
(*fold atoms of term*) 

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

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

482 
 fold_aterms f a = f a; 

483 

484 
(*fold types of term*) 

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

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

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

488 
 fold_term_types f (Bound _) = I 

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

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

491 

492 
fun fold_types f = fold_term_types (K f); 

493 

494 
(*collect variables*) 

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

496 
val add_tvars = fold_types add_tvarsT; 

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

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

499 
val add_tfrees = fold_types add_tfreesT; 

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

501 

502 
(*collect variable names*) 

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

504 
fun term_varnames t = add_term_varnames t []; 

505 

18149  506 
fun find_free t x = 
507 
let 

508 
exception Found of term; 

509 
fun find (t as Free (x', _)) = if x = x' then raise Found t else I 

510 
 find _ = I; 

511 
in (fold_aterms find t (); NONE) handle Found v => SOME v end; 

512 

513 

16943  514 

16678  515 
(** Comparing terms, types, sorts etc. **) 
16537  516 

16678  517 
(* fast syntactic comparison *) 
518 

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

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

16537  521 

16599  522 
fun sort_ord SS = 
523 
if pointer_eq SS then EQUAL 

16990  524 
else dict_ord fast_string_ord SS; 
16678  525 

526 
local 

16537  527 

16678  528 
fun cons_nr (TVar _) = 0 
529 
 cons_nr (TFree _) = 1 

530 
 cons_nr (Type _) = 2; 

16537  531 

16678  532 
in 
16537  533 

534 
fun typ_ord TU = 

535 
if pointer_eq TU then EQUAL 

536 
else 

537 
(case TU of 

16678  538 
(Type (a, Ts), Type (b, Us)) => 
16990  539 
(case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us)  ord => ord) 
16678  540 
 (TFree (a, S), TFree (b, S')) => 
541 
(case fast_string_ord (a, b) of EQUAL => sort_ord (S, S')  ord => ord) 

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

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

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

545 

546 
end; 

547 

548 
local 

549 

550 
fun cons_nr (Const _) = 0 

551 
 cons_nr (Free _) = 1 

552 
 cons_nr (Var _) = 2 

553 
 cons_nr (Bound _) = 3 

554 
 cons_nr (Abs _) = 4 

555 
 cons_nr (_ $ _) = 5; 

556 

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

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

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

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

561 

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

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

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

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

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

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

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

569 
 atoms_ord _ = sys_error "atoms_ord"; 

570 

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

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

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

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

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

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

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

578 
 types_ord (Bound _, Bound _) = EQUAL 

579 
 types_ord _ = sys_error "types_ord"; 

580 

581 
in 

582 

583 
fun fast_term_ord tu = 

584 
if pointer_eq tu then EQUAL 

585 
else 

586 
(case struct_ord tu of 

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

588 
 ord => ord); 

589 

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

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

592 

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

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

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

596 

597 
end; 

16537  598 

599 

600 
(* term_ord *) 

601 

602 
(*a linear wellfounded ACcompatible ordering for terms: 

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

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

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

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

16678  607 

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

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

610 

16667  611 
local 
612 

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

614 
 hd_depth p = p; 

16537  615 

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

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

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

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

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

621 

16667  622 
in 
623 

16537  624 
fun term_ord tu = 
625 
if pointer_eq tu then EQUAL 

626 
else 

627 
(case tu of 

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

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

16667  630 
 (t, u) => 
16537  631 
(case int_ord (size_of_term t, size_of_term u) of 
632 
EQUAL => 

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

16537  635 
 ord => ord)) 
636 
and hd_ord (f, g) = 

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

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

640 
 args_ord _ = EQUAL; 

16537  641 

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

643 

16667  644 
end; 
645 

646 

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

648 

649 
(* 

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

652 
constants. 

653 

654 
f_ord maps strings to integers and serves two purposes: 

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

656 
must be mapped to ~1. 

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

658 
integers >= 0. 

659 

16667  660 
*) 
16570  661 

662 
local 

16667  663 
fun dest_hd f_ord (Const (a, T)) = 
16570  664 
let val ord = f_ord a in 
665 
if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0) 

666 
end 

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

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

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

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

671 

672 
fun term_lpo f_ord (s, t) = 

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

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

675 
then case hd_ord f_ord (f, g) of 

16667  676 
GREATER => 
677 
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts 

678 
then GREATER else LESS 

16570  679 
 EQUAL => 
16667  680 
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts 
681 
then list_ord (term_lpo f_ord) (ss, ts) 

682 
else LESS 

16570  683 
 LESS => LESS 
684 
else GREATER 

685 
end 

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

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

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

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

690 
(prod_ord indexname_ord typ_ord)) int_ord 

691 
(dest_hd f_ord f, dest_hd f_ord g) 

692 
in 

693 
val term_lpo = term_lpo 

694 
end; 

695 

16537  696 

0  697 
(** Connectives of higher order logic **) 
698 

375  699 
fun itselfT ty = Type ("itself", [ty]); 
14854  700 
val a_itselfT = itselfT (TFree ("'a", [])); 
375  701 

0  702 
val propT : typ = Type("prop",[]); 
703 

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

705 

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

707 

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

709 

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

13000  711 
fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t 
0  712 
 strip_all_body t = t; 
713 

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

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

13000  716 
(a,T) :: strip_all_vars t 
0  717 
 strip_all_vars t = [] : (string*typ) list; 
718 

719 
(*increments a term's nonlocal bound variables 

720 
required when moving a term within abstractions 

721 
inc is increment for bound variables 

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

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

725 
Abs(a, T, incr_bv(inc,lev+1,body)) 
13000  726 
 incr_bv (inc, lev, f$t) = 
0  727 
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 
728 
 incr_bv (inc, lev, u) = u; 

729 

730 
fun incr_boundvars 0 t = t 

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

732 

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

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

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

737 
else (x,y)::al) 

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

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

740 

741 
(* strip abstractions created by parameters *) 

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

743 

744 
fun rename_abs pat obj t = 

745 
let 

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

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

17271  748 
Abs (if_none (AList.lookup (op =) ren x) x, T, ren_abs b) 
12981  749 
 ren_abs (f $ t) = ren_abs f $ ren_abs t 
750 
 ren_abs t = t 

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

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

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

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

756 
if i<lev then js else (ilev) ins_int js 
0  757 
 add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js) 
758 
 add_loose_bnos (f$t, lev, js) = 

13000  759 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
0  760 
 add_loose_bnos (_, _, js) = js; 
761 

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

763 

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

765 
level k or beyond. *) 

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

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

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

769 
 loose_bvar _ = false; 

770 

2792  771 
fun loose_bvar1(Bound i,k) = i = k 
772 
 loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 

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

774 
 loose_bvar1 _ = false; 

0  775 

776 
(*Substitute arguments for loose bound variables. 

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

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

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

782 
*) 

13000  783 
fun subst_bounds (args: term list, t) : term = 
0  784 
let val n = length args; 
785 
fun subst (t as Bound i, lev) = 

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

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

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

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

789 
 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

790 
 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

791 
 subst (t,lev) = t 
0  792 
in case args of [] => t  _ => subst (t,0) end; 
793 

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

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

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

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

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

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

800 
 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

801 
 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

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

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

804 

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

806 
fun betapply (Abs(_,_,t), u) = subst_bound (u,t) 
0  807 
 betapply (f,u) = f$u; 
808 

18183  809 
val betapplys = Library.foldl betapply; 
810 

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

811 

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

813 

16882  814 
(* indexnames *) 
815 

16724  816 
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

817 

2959  818 
fun mem_ix (_, []) = false 
16882  819 
 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

820 

16882  821 
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

822 

0  823 

16882  824 
(* variables *) 
825 

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

828 

829 
val tvar_ord = prod_ord indexname_ord sort_ord; 

830 
val var_ord = prod_ord indexname_ord typ_ord; 

16882  831 

832 

833 
(* terms *) 

2176  834 

835 
fun mem_term (_, []) = false 

16882  836 
 mem_term (t, t'::ts) = t aconv t' orelse mem_term (t, ts); 
2176  837 

838 
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; 

839 

16882  840 

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

844 
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

845 
 matchrands _ = true 
0  846 
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

847 
(_, Var _) => true 
0  848 
 (Var _, _) => true 
849 
 (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u) 

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

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

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

853 
 (_, Abs _) => true 

854 
 _ => false 

855 
end; 

856 

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

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

859 
 subst_free pairs = 

13000  860 
let fun substf u = 
17314  861 
case AList.lookup (op aconv) pairs u of 
15531  862 
SOME u' => u' 
863 
 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

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

865 
 _ => u) 
0  866 
in substf end; 
867 

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

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

870 

871 

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

16882  875 
fun abstract_over (v, body) = 
876 
let 

16990  877 
exception SAME; 
878 
fun abs lev tm = 

879 
if v aconv tm then Bound lev 

16882  880 
else 
16990  881 
(case tm of 
882 
Abs (a, T, t) => Abs (a, T, abs (lev + 1) t) 

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

884 
 _ => raise SAME); 

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

0  886 

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

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

0  890 

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

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

17786  893 
fun absdummy (T, body) = Abs ("uu", T, body); 
0  894 

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

896 
fun list_abs_free ([ ] , t) = t 

13000  897 
 list_abs_free ((a,T)::vars, t) = 
0  898 
absfree(a, T, list_abs_free(vars,t)); 
899 

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

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

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

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

906 
fun list_all ([], t) = t 

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

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

914 
let 

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

916 
 subst (t $ u) = subst t $ subst u 

17314  917 
 subst t = if_none (AList.lookup (op aconv) inst t) t; 
16678  918 
in subst tm end; 
0  919 

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

922 
 typ_subst_atomic inst ty = 

923 
let 

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

17314  925 
 subst T = if_none (AList.lookup (op = : typ * typ > bool) inst T) T; 
16678  926 
in subst ty end; 
15797  927 

16678  928 
fun subst_atomic_types [] tm = tm 
929 
 subst_atomic_types inst tm = map_term_types (typ_subst_atomic inst) tm; 

930 

931 
fun typ_subst_TVars [] ty = ty 

932 
 typ_subst_TVars inst ty = 

933 
let 

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

17271  935 
 subst (T as TVar (xi, _)) = if_none (AList.lookup (op =) inst xi) T 
16678  936 
 subst T = T; 
937 
in subst ty end; 

0  938 

16678  939 
fun subst_TVars [] tm = tm 
940 
 subst_TVars inst tm = map_term_types (typ_subst_TVars inst) tm; 

0  941 

16678  942 
(*see also Envir.norm_term*) 
943 
fun subst_Vars [] tm = tm 

944 
 subst_Vars inst tm = 

945 
let 

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

949 
 subst t = t; 

950 
in subst tm end; 

0  951 

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

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

955 
 subst_vars (instT, inst) tm = 

956 
let 

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

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

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

17271  960 
(case AList.lookup (op =) inst xi of 
16678  961 
NONE => Var (xi, typ_subst_TVars instT T) 
962 
 SOME t => t) 

963 
 subst (t as Bound _) = t 

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

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

966 
in subst tm end; 

0  967 

968 

16943  969 
(* instantiation of schematic variables (types before terms) *) 
16882  970 

971 
local exception SAME in 

972 

16943  973 
fun instantiateT_same [] _ = raise SAME 
974 
 instantiateT_same instT ty = 

16882  975 
let 
976 
fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts) 

977 
 subst_typ (TVar v) = 

17314  978 
(case AList.lookup eq_tvar instT v of 
16882  979 
SOME T => T 
980 
 NONE => raise SAME) 

981 
 subst_typ _ = raise SAME 

982 
and subst_typs (T :: Ts) = 

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

984 
handle SAME => T :: subst_typs Ts) 

985 
 subst_typs [] = raise SAME; 

986 
in subst_typ ty end; 

987 

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

989 
 instantiate (instT, inst) tm = 

990 
let 

16943  991 
val substT = instantiateT_same instT; 
992 
fun subst (Const (c, T)) = Const (c, substT T) 

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

16882  994 
 subst (Var (xi, T)) = 
16943  995 
let val (T', same) = (substT T, false) handle SAME => (T, true) in 
17314  996 
(case AList.lookup eq_var inst (xi, T') of 
16882  997 
SOME t => t 
998 
 NONE => if same then raise SAME else Var (xi, T')) 

999 
end 

1000 
 subst (Bound _) = raise SAME 

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

16943  1002 
(Abs (x, substT T, subst t handle SAME => t) 
16882  1003 
handle SAME => Abs (x, T, subst t)) 
1004 
 subst (t $ u) = (subst t $ (subst u handle SAME => u) handle SAME => t $ subst u); 

1005 
in subst tm handle SAME => tm end; 

1006 

1007 
fun instantiateT instT ty = 

16943  1008 
instantiateT_same instT ty handle SAME => ty; 
16882  1009 

1010 
end; 

1011 

1012 

15573  1013 
(** Identifying firstorder terms **) 
1014 

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

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

1017 

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

16667  1021 
fun is_first_order quants = 
16589  1022 
let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body 
16667  1023 
 first_order1 Ts (Const(q,_) $ Abs(a,T,body)) = 
1024 
q mem_string quants andalso (*it is a known quantifier*) 

16589  1025 
not (is_funtype T) andalso first_order1 (T::Ts) body 
16667  1026 
 first_order1 Ts t = 
1027 
case strip_comb t of 

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

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

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

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

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

1033 
 _ => error "first_order: unexpected case" 

16589  1034 
in first_order1 [] end; 
15573  1035 

16710  1036 

16990  1037 
(* maximum index of typs and terms *) 
0  1038 

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

1041 
 maxidx_typ (TFree _) i = i 

1042 
and maxidx_typs [] i = i 

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

0  1044 

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

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

1048 
 maxidx_term (Bound _) i = i 

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

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

0  1051 

16710  1052 
fun maxidx_of_typ T = maxidx_typ T ~1; 
1053 
fun maxidx_of_typs Ts = maxidx_typs Ts ~1; 

1054 
fun maxidx_of_term t = maxidx_term t ~1; 

13665  1055 

0  1056 

1057 

1058 
(**** Syntaxrelated declarations ****) 

1059 

1060 
(*** Printing ***) 

1061 

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

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

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

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

1070 
in vary1 (if c = "" then "u" else c) ^ u end; 
0  1071 

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

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

13000  1074 
 variantlist(b::bs, used) = 
0  1075 
let val b' = variant used b 
1076 
in b' :: variantlist (bs, b'::used) end; 

1077 

14695  1078 
(*Invent fresh names*) 
1079 
fun invent_names _ _ 0 = [] 

1080 
 invent_names used a n = 

1081 
let val b = Symbol.bump_string a in 

1082 
if a mem_string used then invent_names used b n 

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

1084 
end; 

11353  1085 

16537  1086 

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

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

1088 

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

1089 
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

1090 
 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

1091 
 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

1092 

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

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

1095 

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

1096 
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

1097 
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

1098 

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

1100 
 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

1101 
 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

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

1103 

13646  1104 
fun term_consts t = add_term_consts(t,[]); 
1105 

16943  1106 
fun exists_subterm P = 
1107 
let 

1108 
fun ex tm = P tm orelse 

1109 
(case tm of 

1110 
t $ u => ex t orelse ex u 

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

1112 
 _ => false); 

1113 
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

1114 

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

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

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

1118 
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

1119 
 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

1120 
 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

1121 

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

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

1123 
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

1124 
 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

1125 
 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

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

1127 
 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

1128 
 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

1129 

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

1130 

0  1131 
(** TFrees and TVars **) 
1132 

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

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

1134 
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

1135 
 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

1136 
 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

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

1138 

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

10666  1141 
fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs 
2176  1142 
 add_term_names (Free(a,_), bs) = a ins_string bs 
0  1143 
 add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) 
1144 
 add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) 

1145 
 add_term_names (_, bs) = bs; 

1146 

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

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

1148 
fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts 
0  1149 
 add_typ_tvars(TFree(_),vs) = vs 
16294  1150 
 add_typ_tvars(TVar(v),vs) = insert (op =) v vs; 
0  1151 

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

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

1153 
fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts 
2176  1154 
 add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs 
0  1155 
 add_typ_tfree_names(TVar(_),fs) = fs; 
1156 

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

1157 
fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts 
16294  1158 
 add_typ_tfrees(TFree(f),fs) = insert (op =) f fs 
0  1159 
 add_typ_tfrees(TVar(_),fs) = fs; 
1160 

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

1161 
fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts 
2176  1162 
 add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms 
1163 
 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

1164 

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

1167 

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

1169 
val add_term_tfrees = it_term_types add_typ_tfrees; 

1170 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

1171 

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

1172 
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

1173 

0  1174 
(*Nonlist versions*) 
1175 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

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

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

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

1179 

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

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

1181 

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

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

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

1186 

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

1187 
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

1188 
 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

1189 
 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

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

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

1192 
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

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

1194 
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

1195 

16537  1196 

0  1197 
(** Frees and Vars **) 
1198 

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

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

16990  1201 
Var _ => OrdList.insert term_ord t vars 
0  1202 
 Abs (_,_,body) => add_term_vars(body,vars) 
1203 
 f$t => add_term_vars (f, add_term_vars(t, vars)) 

1204 
 _ => vars; 

1205 

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

1207 

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

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

16990  1210 
Free _ => OrdList.insert term_ord t frees 
0  1211 
 Abs (_,_,body) => add_term_frees(body,frees) 
1212 
 f$t => add_term_frees (f, add_term_frees(t, frees)) 

1213 
 _ => frees; 

1214 

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

1216 

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

17851  1218 
having a unique name  SLOW!*) 
0  1219 
fun variant_abs (a,T,P) = 
1220 
let val b = variant (add_term_names(P,[])) a 

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

1221 
in (b, subst_bound (Free(b,T), P)) end; 
0  1222 

16678  1223 
fun dest_abs (x, T, body) = 
1224 
let 

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

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

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

1228 
 name_clash _ = false; 

1229 
in 

1230 
if name_clash body then 

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

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

1233 
end; 

1234 

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

1237 
local 

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

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

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

1241 
in 

1242 
fun bound n = 

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

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

1245 
end; 

1246 

1247 
val is_bound = String.isPrefix ":"; 

16943  1248 

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

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

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

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

1255 
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

1256 

1417  1257 

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

1259 

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

1262 
let 

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

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

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

1267 

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

16790  1270 

16943  1271 
fun zero_var_indexes_inst tm = 
1272 
let 

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

1274 
val inst = 

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

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

1277 
in (instT, inst) end; 

12499  1278 

16943  1279 
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

1280 

1417  1281 

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

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

1283 

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

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

1285 

18253  1286 
fun dummy_pattern T = Const (dummy_patternN, T); 
1287 

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

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

1289 
 is_dummy_pattern _ = false; 
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 no_dummy_patterns tm = 
16787  1292 
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

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

1294 

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

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

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

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

1300 
 replace_dummy Ts (i, t $ u) = 

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

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

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

1304 

1305 
val replace_dummy_patterns = replace_dummy []; 

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

1306 

10552  1307 
fun is_replaced_dummy_pattern ("_dummy_", _) = true 
1308 
 is_replaced_dummy_pattern _ = false; 

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

1309 

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

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

1313 
 show_dummy_patterns a = a; 

1314 

13484  1315 

1316 
(* adhoc freezing *) 

1317 

1318 
fun adhoc_freeze_vars tm = 

1319 
let 

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

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

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

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

1324 
in (subst_atomic insts tm, xs) end; 

1325 

1326 

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

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

1328 

15986  1329 
val show_question_marks = ref true; 
15472  1330 

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

1331 
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

1332 
let 
15986  1333 
val question_mark = if ! show_question_marks then "?" else ""; 
1334 
val idx = string_of_int i; 

1335 
val dot = 

1336 
(case rev (Symbol.explode x) of 

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

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

1339 
 c :: _ => Symbol.is_digit c 

1340 
 _ => true); 

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

1341 
in 
15986  1342 
if dot then question_mark ^ x ^ "." ^ idx 
1343 
else if i <> 0 then question_mark ^ x ^ idx 

1344 
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

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

1346 

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

1347 
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

1348 
 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

1349 

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

1350 

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

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

1352 

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

1353 
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

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

1355 
 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

1356 
 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

1357 
 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

1358 
 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

1359 

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

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

1361 

4444  1362 
structure BasicTerm: BASIC_TERM = Term; 
1363 
open BasicTerm; 