author  wenzelm 
Wed, 22 Jun 2005 19:41:23 +0200  
changeset 16537  954495db0f07 
parent 16338  3d1851acb4d0 
child 16570  861b9fa2c98c 
permissions  rwrr 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright Cambridge University 1992 
1364
8ea1a962ad72
files now define a structure to allow SML/NJ to optimize the code
clasohm
parents:
1029
diff
changeset

5 

4444  6 
Simply typed lambdacalculus: types, terms, and basic operations. 
0  7 
*) 
8 

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

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

10 
infixr 5 >; 
4444  11 
infixr >; 
12 
infix aconv; 

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

13 

4444  14 
signature BASIC_TERM = 
15 
sig 

16 
type indexname 

17 
type class 

18 
type sort 

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

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

22 
TFree of string * sort  

23 
TVar of indexname * sort 

16537  24 
datatype term = 
25 
Const of string * typ  

26 
Free of string * typ  

27 
Var of indexname * typ  

28 
Bound of int  

29 
Abs of string * typ * term  

30 
op $ of term * term 

31 
exception TYPE of string * typ list * term list 

32 
exception TERM of string * term list 

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

35 
val is_TVar: typ > bool 

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

41 
val strip_type: typ > typ list * typ 

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

45 
val is_Var: term > bool 

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

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

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

52 
val dest_Var: term > indexname * typ 

53 
val type_of: term > typ 

54 
val type_of1: typ list * term > typ 

55 
val fastype_of: term > typ 

56 
val fastype_of1: typ list * term > typ 

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

60 
val strip_qnt_body: string > term > term 

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

62 
val list_comb: term * term list > term 

63 
val strip_comb: term > term * term list 

64 
val head_of: term > term 

65 
val size_of_term: term > int 

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

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

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

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

16537  70 
structure Vartab: TABLE 
71 
structure Typtab: TABLE 

72 
structure Termtab: TABLE 

73 
val aconv: term * term > bool 

74 
val aconvs: term list * term list > bool 

4444  75 
val foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a 
8609  76 
val foldl_term_types: (term > 'a * typ > 'a) > 'a * term > 'a 
4444  77 
val foldl_types: ('a * typ > 'a) > 'a * term > 'a 
78 
val foldl_aterms: ('a * term > 'a) > 'a * term > 'a 

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

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

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

84 
val a_itselfT: typ 

85 
val propT: typ 

86 
val implies: term 

87 
val all: typ > term 

88 
val equals: typ > term 

89 
val strip_all_body: term > term 

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

91 
val incr_bv: int * int * term > term 

92 
val incr_boundvars: int > term > term 

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

94 
val loose_bnos: term > int list 

95 
val loose_bvar: term * int > bool 

96 
val loose_bvar1: term * int > bool 

97 
val subst_bounds: term list * term > term 

98 
val subst_bound: term * term > term 

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

100 
val betapply: term * term > term 

101 
val eq_ix: indexname * indexname > bool 

102 
val ins_ix: indexname * indexname list > indexname list 

103 
val mem_ix: indexname * indexname list > bool 

104 
val mem_term: term * term list > bool 

105 
val subset_term: term list * term list > bool 

106 
val eq_set_term: term list * term list > bool 

107 
val ins_term: term * term list > term list 

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

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

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

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

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

117 
val incr_tvar: int > typ > typ 

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

119 
val atless: term * term > bool 

120 
val insert_aterm: term * term list > term list 

121 
val abstract_over: term * term > term 

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

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

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

127 
val maxidx_of_typ: typ > int 

128 
val maxidx_of_typs: typ list > int 

129 
val maxidx_of_term: term > int 

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

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

136 
val add_new_id: string list * string > string list 

137 
val add_typ_classes: typ * class list > class list 

138 
val add_typ_ixns: indexname list * typ > indexname list 

139 
val add_typ_tfree_names: typ * string list > string list 

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

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

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

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

144 
val add_typ_tycons: typ * string list > string list 

145 
val add_typ_varnames: typ * string list > string list 

146 
val add_term_classes: term * class list > class list 

147 
val add_term_consts: term * string list > string list 

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

149 
val term_constsT: term > (string * typ) list 
4444  150 
val add_term_frees: term * term list > term list 
151 
val term_frees: term > term list 

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

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

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

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

157 
val add_term_tvar_ixns: term * indexname list > indexname list 

158 
val add_term_tvarnames: term * string list > string list 

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

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

161 
val add_term_tycons: term * string list > string list 

162 
val add_term_vars: term * term list > term list 

163 
val term_vars: term > term list 

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

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

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

4444  171 
signature TERM = 
172 
sig 

173 
include BASIC_TERM 

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

176 
val typ_ord: typ * typ > order 

177 
val typs_ord: typ list * typ list > order 

178 
val term_ord: term * term > order 

179 
val terms_ord: term list * term list > order 

180 
val hd_ord: term * term > order 

181 
val termless: term * term > bool 

12981  182 
val match_bvars: (term * term) * (string * string) list > (string * string) list 
183 
val rename_abs: term > term > term > term option 

12499  184 
val invent_names: string list > string > int > string list 
16338  185 
val map_typ: (string > string) > (string > string) > typ > typ 
186 
val map_term: (string > string) > (string > string) > (string > string) > term > term 

12499  187 
val add_tvarsT: (indexname * sort) list * typ > (indexname * sort) list 
188 
val add_tvars: (indexname * sort) list * term > (indexname * sort) list 

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

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

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

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

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

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

194 
val replace_dummy_patterns: int * term > int * term 
10552  195 
val is_replaced_dummy_pattern: indexname > bool 
16035  196 
val show_dummy_patterns: term > term 
13484  197 
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

198 
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

199 
val string_of_vname': indexname > string 
15612  200 
val string_of_term: term > string 
4444  201 
end; 
202 

203 
structure Term: TERM = 

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

204 
struct 
0  205 

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

207 
for resolution.*) 

16537  208 
type indexname = string * int; 
0  209 

4626  210 
(* Types are classified by sorts. *) 
0  211 
type class = string; 
212 
type sort = class list; 

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

213 
type arity = string * sort list * sort; 
0  214 

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

216 
datatype typ = Type of string * typ list 

217 
 TFree of string * sort 

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

218 
 TVar of indexname * sort; 
0  219 

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

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

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

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

227 

13000  228 
datatype term = 
0  229 
Const of string * typ 
13000  230 
 Free of string * typ 
0  231 
 Var of indexname * typ 
232 
 Bound of int 

233 
 Abs of string*typ*term 

3965  234 
 op $ of term*term; 
0  235 

16537  236 
(*Errors involving type mismatches*) 
0  237 
exception TYPE of string * typ list * term list; 
238 

16537  239 
(*Errors errors involving terms*) 
0  240 
exception TERM of string * term list; 
241 

242 
(*Note variable naming conventions! 

243 
a,b,c: string 

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

245 
i,j,m,n: int 

246 
t,u: term 

247 
v,w: indexnames 

248 
x,y: any 

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

250 
T,U: typ 

251 
*) 

252 

253 

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

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

255 

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

258 

259 
fun no_dummyT typ = 

260 
let 

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

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

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

264 
 check _ = (); 

265 
in check typ; typ end; 

266 

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

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

268 

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

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

271 

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

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

273 
 dest_Type T = raise TYPE ("dest_Type", [T], []); 
15914  274 
fun dest_TVar (TVar x) = x 
275 
 dest_TVar T = raise TYPE ("dest_TVar", [T], []); 

276 
fun dest_TFree (TFree x) = x 

277 
 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

278 

16537  279 

0  280 
(** Discriminators **) 
281 

7318  282 
fun is_Bound (Bound _) = true 
283 
 is_Bound _ = false; 

284 

0  285 
fun is_Const (Const _) = true 
286 
 is_Const _ = false; 

287 

288 
fun is_Free (Free _) = true 

289 
 is_Free _ = false; 

290 

291 
fun is_Var (Var _) = true 

292 
 is_Var _ = false; 

293 

294 
fun is_TVar (TVar _) = true 

295 
 is_TVar _ = false; 

296 

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

299 
 is_funtype _ = false; 

300 

16537  301 

0  302 
(** Destructors **) 
303 

304 
fun dest_Const (Const x) = x 

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

306 

307 
fun dest_Free (Free x) = x 

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

309 

310 
fun dest_Var (Var x) = x 

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

312 

313 

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

4064  316 

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

319 
 binder_types _ = []; 

320 

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

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

323 
 body_type T = T; 

324 

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

326 
fun strip_type T : typ list * typ = 

327 
(binder_types T, body_type T); 

328 

329 

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

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

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

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

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

0  336 
 type_of1 (Ts, Var (_,T)) = T 
337 
 type_of1 (Ts, Abs (_,T,body)) = T > type_of1(T::Ts, body) 

13000  338 
 type_of1 (Ts, f$u) = 
0  339 
let val U = type_of1(Ts,u) 
340 
and T = type_of1(Ts,f) 

341 
in case T of 

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

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

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

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

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

347 
[T,U], [f$u]) 
0  348 
end; 
349 

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

351 

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

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

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

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

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

13000  361 
 fastype_of1 (_, Var (_,T)) = T 
61  362 
 fastype_of1 (Ts, Abs (_,T,u)) = T > fastype_of1 (T::Ts, u); 
363 

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

0  365 

366 

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

0  369 
(* maps (x1,...,xn)t to t *) 
13000  370 
fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t 
0  371 
 strip_abs_body u = u; 
372 

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

13000  374 
fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t 
0  375 
 strip_abs_vars u = [] : (string*typ) list; 
376 

377 

378 
fun strip_qnt_body qnt = 

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

380 
 strip t = t 

381 
in strip end; 

382 

383 
fun strip_qnt_vars qnt = 

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

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

386 
in strip end; 

387 

388 

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

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

392 

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

13000  394 
fun strip_comb u : term * term list = 
0  395 
let fun stripc (f$t, ts) = stripc (f, t::ts) 
13000  396 
 stripc x = x 
0  397 
in stripc(u,[]) end; 
398 

399 

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

401 
fun head_of (f$t) = head_of f 

402 
 head_of u = u; 

403 

404 

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

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

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

408 
 size_of_term _ = 1; 

409 

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

410 
fun map_type_tvar f (Type(a,Ts)) = Type(a, map (map_type_tvar f) Ts) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

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

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

413 

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

414 
fun map_type_tfree f (Type(a,Ts)) = Type(a, map (map_type_tfree f) Ts) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

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

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

417 

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

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

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

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

423 
 map(t as Bound _) = t 

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

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

426 
in map end; 

427 

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

429 
fun it_term_types f = 

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

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

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

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

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

435 
 iter(Bound _, a) = a 

436 
in iter end 

437 

438 

16537  439 
(** Comparing terms, types etc. **) 
440 

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

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

443 

444 
val sort_ord = list_ord string_ord; 

445 

446 

447 
(* typ_ord *) 

448 

449 
fun typ_ord TU = 

450 
if pointer_eq TU then EQUAL 

451 
else 

452 
(case TU of 

453 
(Type x, Type y) => prod_ord string_ord typs_ord (x, y) 

454 
 (Type _, _) => GREATER 

455 
 (TFree _, Type _) => LESS 

456 
 (TFree x, TFree y) => prod_ord string_ord sort_ord (x, y) 

457 
 (TFree _, TVar _) => GREATER 

458 
 (TVar _, Type _) => LESS 

459 
 (TVar _, TFree _) => LESS 

460 
 (TVar x, TVar y) => prod_ord indexname_ord sort_ord (x, y)) 

461 
and typs_ord Ts_Us = list_ord typ_ord Ts_Us; 

462 

463 

464 
(* term_ord *) 

465 

466 
(*a linear wellfounded ACcompatible ordering for terms: 

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

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

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

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

471 

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

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

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

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

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

477 

478 
fun term_ord tu = 

479 
if pointer_eq tu then EQUAL 

480 
else 

481 
(case tu of 

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

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

484 
 (t, u) => 

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

486 
EQUAL => 

487 
let 

488 
val (f, ts) = strip_comb t 

489 
and (g, us) = strip_comb u 

490 
in case hd_ord (f, g) of EQUAL => terms_ord (ts, us)  ord => ord end 

491 
 ord => ord)) 

492 
and hd_ord (f, g) = 

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

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

495 

496 
fun op aconv tu = (term_ord tu = EQUAL); 

497 
fun aconvs ts_us = (list_ord term_ord ts_us = EQUAL); 

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

499 

500 
structure Vartab = TableFun(type key = indexname val ord = indexname_ord); 

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

502 
structure Termtab = TableFun(type key = term val ord = term_ord); 

503 

504 

0  505 
(** Connectives of higher order logic **) 
506 

375  507 
fun itselfT ty = Type ("itself", [ty]); 
14854  508 
val a_itselfT = itselfT (TFree ("'a", [])); 
375  509 

0  510 
val propT : typ = Type("prop",[]); 
511 

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

513 

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

515 

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

517 

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

13000  519 
fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t 
0  520 
 strip_all_body t = t; 
521 

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

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

13000  524 
(a,T) :: strip_all_vars t 
0  525 
 strip_all_vars t = [] : (string*typ) list; 
526 

527 
(*increments a term's nonlocal bound variables 

528 
required when moving a term within abstractions 

529 
inc is increment for bound variables 

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

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

533 
Abs(a, T, incr_bv(inc,lev+1,body)) 
13000  534 
 incr_bv (inc, lev, f$t) = 
0  535 
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 
536 
 incr_bv (inc, lev, u) = u; 

537 

538 
fun incr_boundvars 0 t = t 

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

540 

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

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

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

545 
else (x,y)::al) 

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

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

548 

549 
(* strip abstractions created by parameters *) 

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

551 

552 
fun rename_abs pat obj t = 

553 
let 

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

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

15570  556 
Abs (getOpt (assoc_string (ren, x), x), T, ren_abs b) 
12981  557 
 ren_abs (f $ t) = ren_abs f $ ren_abs t 
558 
 ren_abs t = t 

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

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

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

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

564 
if i<lev then js else (ilev) ins_int js 
0  565 
 add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js) 
566 
 add_loose_bnos (f$t, lev, js) = 

13000  567 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
0  568 
 add_loose_bnos (_, _, js) = js; 
569 

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

571 

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

573 
level k or beyond. *) 

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

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

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

577 
 loose_bvar _ = false; 

578 

2792  579 
fun loose_bvar1(Bound i,k) = i = k 
580 
 loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 

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

582 
 loose_bvar1 _ = false; 

0  583 

584 
(*Substitute arguments for loose bound variables. 

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

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

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

590 
*) 

13000  591 
fun subst_bounds (args: term list, t) : term = 
0  592 
let val n = length args; 
593 
fun subst (t as Bound i, lev) = 

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

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

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

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

597 
 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

598 
 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

599 
 subst (t,lev) = t 
0  600 
in case args of [] => t  _ => subst (t,0) end; 
601 

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

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

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

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

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

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

608 
 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

609 
 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

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

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

612 

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

614 
fun betapply (Abs(_,_,t), u) = subst_bound (u,t) 
0  615 
 betapply (f,u) = f$u; 
616 

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

617 

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

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

619 

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

620 
(*optimized equality test for indexnames. Yields a huge gain under Poly/ML*) 
2959  621 
fun eq_ix ((a, i):indexname, (a',i'):indexname) = (a=a') andalso i=i'; 
2192
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

622 

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

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

625 
 mem_ix (x, y :: ys) = eq_ix(x,y) orelse mem_ix (x, ys); 
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

626 

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

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

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

629 

0  630 

2176  631 
(** Membership, insertion, union for terms **) 
632 

633 
fun mem_term (_, []) = false 

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

635 

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

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

637 
 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

638 

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

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

640 
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

641 

2176  642 
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; 
643 

644 
fun union_term (xs, []) = xs 

645 
 union_term ([], ys) = ys 

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

647 

5585  648 
fun inter_term ([], ys) = [] 
649 
 inter_term (x::xs, ys) = 

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

651 

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

655 
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

656 
 matchrands _ = true 
0  657 
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

658 
(_, Var _) => true 
0  659 
 (Var _, _) => true 
660 
 (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u) 

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

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

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

664 
 (_, Abs _) => true 

665 
 _ => false 

666 
end; 

667 

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

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

670 
 subst_free pairs = 

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

672 
case gen_assoc (op aconv) (pairs, u) of 
15531  673 
SOME u' => u' 
674 
 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

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

676 
 _ => u) 
0  677 
in substf end; 
678 

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

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

681 

682 

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

686 
fun abstract_over (v,body) = 

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

688 
(case u of 

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

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

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

691 
 _ => u) 
0  692 
in abst(0,body) end; 
693 

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

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

0  697 

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

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

700 

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

702 
fun list_abs_free ([ ] , t) = t 

13000  703 
 list_abs_free ((a,T)::vars, t) = 
0  704 
absfree(a, T, list_abs_free(vars,t)); 
705 

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

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

13000  708 
 list_all_free ((a,T)::vars, t) = 
0  709 
(all T) $ (absfree(a, T, list_all_free(vars,t))); 
710 

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

712 
fun list_all ([], t) = t 

13000  713 
 list_all ((a,T)::vars, t) = 
0  714 
(all T) $ (Abs(a, T, list_all(vars,t))); 
715 

13000  716 
(*Replace the ATOMIC term ti by ui; instl = [(t1,u1), ..., (tn,un)]. 
0  717 
A simultaneous substitution: [ (a,b), (b,a) ] swaps a and b. *) 
718 
fun subst_atomic [] t = t : term 

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

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

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

721 
 subst (f$t') = subst f $ subst t' 
15570  722 
 subst t = getOpt (assoc(instl,t),t) 
0  723 
in subst t end; 
724 

15797  725 
(*Replace the ATOMIC type Ti by Ui; instl = [(T1,U1), ..., (Tn,Un)].*) 
726 
fun typ_subst_atomic [] T = T 

727 
 typ_subst_atomic instl (Type (s, Ts)) = 

728 
Type (s, map (typ_subst_atomic instl) Ts) 

729 
 typ_subst_atomic instl T = getOpt (assoc (instl, T), T); 

730 

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

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

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

734 
 subst(T as TFree _) = T 
15570  735 
 subst(T as TVar(ixn,_)) = getOpt (assoc(iTs,ixn),T) 
0  736 
in subst T end; 
737 

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

738 
(*Substitute for type Vars in a term*) 
0  739 
val subst_TVars = map_term_types o typ_subst_TVars; 
740 

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

741 
(*Substitute for Vars in a term; see also envir/norm_term*) 
0  742 
fun subst_Vars itms t = if null itms then t else 
15570  743 
let fun subst(v as Var(ixn,_)) = getOpt (assoc(itms,ixn),v) 
0  744 
 subst(Abs(a,T,t)) = Abs(a,T,subst t) 
745 
 subst(f$t) = subst f $ subst t 

746 
 subst(t) = t 

747 
in subst t end; 

748 

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

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

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

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

15531  754 
NONE => Var(ixn,typ_subst_TVars iTs T) 
755 
 SOME t => t) 

0  756 
 subst(b as Bound _) = b 
757 
 subst(Abs(a,T,t)) = Abs(a,typ_subst_TVars iTs T,subst t) 

758 
 subst(f$t) = subst f $ subst t 

759 
in subst end; 

760 

761 

15573  762 
(** Identifying firstorder terms **) 
763 

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

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

766 

16537  767 
(*First order means in all terms of the form f(t1,...,tn) no argument has a 
768 
function type. The metaquantifier "all" is excludedits argument always 

15962  769 
has a function typethrough a recursive call into its body.*) 
15573  770 
fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body 
16537  771 
 first_order1 Ts (Const("all",_)$Abs(a,T,body)) = 
15954  772 
not (is_funtype T) andalso first_order1 (T::Ts) body 
15573  773 
 first_order1 Ts t = 
774 
case strip_comb t of 

16537  775 
(Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts 
776 
 (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts 

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

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

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

780 
 _ => error "first_order: unexpected case"; 

15573  781 

782 
val is_first_order = first_order1 []; 

783 

0  784 
(*Computing the maximum index of a typ*) 
2146  785 
fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts 
0  786 
 maxidx_of_typ(TFree _) = ~1 
2146  787 
 maxidx_of_typ(TVar((_,i),_)) = i 
788 
and maxidx_of_typs [] = ~1 

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

0  790 

791 

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

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

794 
 maxidx_of_term (Bound _) = ~1 

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

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

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

0  799 

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

0  802 

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

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

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

806 

807 
(**** Syntaxrelated declarations ****) 

808 

809 
(*** Printing ***) 

810 

14676  811 
(*Makes a variant of a name distinct from the names in bs. 
812 
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

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

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

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

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

819 
in vary1 (if c = "" then "u" else c) ^ u end; 
0  820 

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

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

13000  823 
 variantlist(b::bs, used) = 
0  824 
let val b' = variant used b 
825 
in b' :: variantlist (bs, b'::used) end; 

826 

14695  827 
(*Invent fresh names*) 
828 
fun invent_names _ _ 0 = [] 

829 
 invent_names used a n = 

830 
let val b = Symbol.bump_string a in 

831 
if a mem_string used then invent_names used b n 

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

833 
end; 

11353  834 

16537  835 

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

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

837 

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

838 
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

839 
 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

840 
 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

841 

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

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

844 

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

845 
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

846 
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

847 

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

849 
 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

850 
 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

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

852 

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

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

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

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

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

857 

13646  858 
fun term_consts t = add_term_consts(t,[]); 
859 

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

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

861 

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

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

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

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

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

868 

4631  869 
fun exists_subterm P = 
870 
let fun ex t = P t orelse 

871 
(case t of 

872 
u $ v => ex u orelse ex v 

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

874 
 _ => false) 

875 
in ex end; 

876 

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

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

878 
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

879 
 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

880 
 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

881 

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

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

883 
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

884 
 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

885 
 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

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

887 
 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

888 
 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

889 

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

890 

0  891 
(** TFrees and TVars **) 
892 

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

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

895 

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

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

897 
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

898 
 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

899 
 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

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

901 

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

10666  904 
fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs 
2176  905 
 add_term_names (Free(a,_), bs) = a ins_string bs 
0  906 
 add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) 
907 
 add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) 

908 
 add_term_names (_, bs) = bs; 

909 

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

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

911 
fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts 
0  912 
 add_typ_tvars(TFree(_),vs) = vs 
16294  913 
 add_typ_tvars(TVar(v),vs) = insert (op =) v vs; 
0  914 

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

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

916 
fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts 
2176  917 
 add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs 
0  918 
 add_typ_tfree_names(TVar(_),fs) = fs; 
919 

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

920 
fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts 
16294  921 
 add_typ_tfrees(TFree(f),fs) = insert (op =) f fs 
0  922 
 add_typ_tfrees(TVar(_),fs) = fs; 
923 

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

924 
fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts 
2176  925 
 add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms 
926 
 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

927 

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

930 

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

932 
val add_term_tfrees = it_term_types add_typ_tfrees; 

933 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

934 

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

935 
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

936 

0  937 
(*Nonlist versions*) 
938 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

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

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

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

942 

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

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

944 

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

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

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

949 

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

950 
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

951 
 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

952 
 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

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

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

955 
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

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

957 
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

958 

16537  959 

0  960 
(** Frees and Vars **) 
961 

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

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

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

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

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

967 
 atless _ = false; 

968 

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

970 
fun insert_aterm (t,us) = 

971 
let fun inserta [] = [t] 

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

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

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

975 
else u :: inserta(us') 
0  976 
in inserta us end; 
977 

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

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

980 
Var _ => insert_aterm(t,vars) 

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

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

983 
 _ => vars; 

984 

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

986 

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

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

989 
Free _ => insert_aterm(t,frees) 

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

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

992 
 _ => frees; 

993 

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

995 

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

997 
having a unique name. *) 

998 
fun variant_abs (a,T,P) = 

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

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

1000 
in (b, subst_bound (Free(b,T), P)) end; 
0  1001 

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

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

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

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

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

1008 
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

1009 

1417  1010 

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

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

1012 

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

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

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

1016 

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

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

1018 
fun foldl_aterms f (x, t $ u) = foldl_aterms f (foldl_aterms f (x, t), u) 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

1019 
 foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t) 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

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

1021 

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

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

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

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

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

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

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

1028 

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

1029 
(*foldl types of term*) 
8609  1030 
fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T) 
1031 
 foldl_term_types f (x, t as Free (_, T)) = f t (x, T) 

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

1033 
 foldl_term_types f (x, Bound _) = x 

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

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

1036 

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

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

1038 

12499  1039 
(*collect variables*) 
16294  1040 
val add_tvarsT = foldl_atyps (fn (vs, TVar v) => insert (op =) v vs  (vs, _) => vs); 
12499  1041 
val add_tvars = foldl_types add_tvarsT; 
16294  1042 
val add_vars = foldl_aterms (fn (vs, Var v) => insert (op =) v vs  (vs, _) => vs); 
1043 
val add_frees = foldl_aterms (fn (vs, Free v) => insert (op =) v vs  (vs, _) => vs); 

12499  1044 

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

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

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

1048 

1417  1049 

4444  1050 

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

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

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

1417  1055 

16338  1056 

1417  1057 
(** Sharing of types **) 
1058 

13000  1059 
val memo_types = ref (Typtab.empty: typ Typtab.table); 
1417  1060 

1061 
fun compress_type T = 

13000  1062 
(case Typtab.lookup (! memo_types, T) of 
15531  1063 
SOME T' => T' 
1064 
 NONE => 

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

1067 

1417  1068 

1069 
(** Sharing of atomic terms **) 

1070 

13000  1071 
val memo_terms = ref (Termtab.empty : term Termtab.table); 
1417  1072 

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

13000  1074 
 share_term (Abs (a, T, u)) = Abs (a, T, share_term u) 
1417  1075 
 share_term t = 
13000  1076 
(case Termtab.lookup (! memo_terms, t) of 
15531  1077 
SOME t' => t' 
1078 
 NONE => (memo_terms := Termtab.update ((t, t), ! memo_terms); t)); 

1417  1079 

1080 
val compress_term = share_term o map_term_types compress_type; 

1081 

4444  1082 

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

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

1084 

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

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

1086 

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

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

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

1089 

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

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

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

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

1093 

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

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

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

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

1099 
 replace_dummy Ts (i, t $ u) = 

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

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

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

1103 

1104 
val replace_dummy_patterns = replace_dummy []; 

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

1105 

10552  1106 
fun is_replaced_dummy_pattern ("_dummy_", _) = true 
1107 
 is_replaced_dummy_pattern _ = false; 

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

1108 

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

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

1112 
 show_dummy_patterns a = a; 

1113 

13484  1114 

1115 
(* adhoc freezing *) 

1116 

1117 
fun adhoc_freeze_vars tm = 

1118 
let 

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

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

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

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

1123 
in (subst_atomic insts tm, xs) end; 

1124 

1125 

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

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

1127 

15986  1128 
val show_question_marks = ref true; 
15472  1129 

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

1130 
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

1131 
let 
15986  1132 
val question_mark = if ! show_question_marks then "?" else ""; 
1133 
val idx = string_of_int i; 

1134 
val dot = 

1135 
(case rev (Symbol.explode x) of 

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

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

1138 
 c :: _ => Symbol.is_digit c 

1139 
 _ => true); 

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

1140 
in 
15986  1141 
if dot then question_mark ^ x ^ "." ^ idx 
1142 
else if i <> 0 then question_mark ^ x ^ idx 

1143 
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

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

1145 

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

1146 
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

1147 
 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

1148 

15612  1149 
fun string_of_term (Const(s,_)) = s 
1150 
 string_of_term (Free(s,_)) = s 

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

1152 
 string_of_term (Bound i) = string_of_int i 

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

1154 
 string_of_term (s $ t) = 

1155 
"(" ^ string_of_term s ^ " " ^ string_of_term t ^ ")" 

1156 

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

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

1158 

4444  1159 
structure BasicTerm: BASIC_TERM = Term; 
1160 
open BasicTerm; 