author  wenzelm 
Sun, 25 Sep 2005 23:36:14 +0200  
changeset 17642  e063c0403650 
parent 17314  04e21a27c0ad 
child 17756  d4a35f82fbb4 
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 

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

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

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

39 
val dest_TFree: typ > string * sort 

40 
val is_Bound: term > bool 

41 
val is_Const: term > bool 

42 
val is_Free: term > bool 

43 
val is_Var: term > bool 

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

48 
val dest_Var: term > indexname * typ 

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

53 
val strip_type: typ > typ list * typ 

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

61 
val strip_qnt_body: string > term > term 

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

63 
val list_comb: term * term list > term 

64 
val strip_comb: term > term * term list 

65 
val head_of: term > term 

66 
val size_of_term: term > int 

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

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

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

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

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

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

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

75 
val add_term_names: term * string list > string list 

76 
val add_term_varnames: term > indexname list > indexname list 

77 
val term_varnames: term > indexname list 

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

16537  80 
structure Vartab: TABLE 
81 
structure Typtab: TABLE 

82 
structure Termtab: TABLE 

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

85 
val propT: typ 

86 
val implies: term 

87 
val all: typ > term 

88 
val equals: typ > term 

89 
val strip_all_body: term > term 

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

91 
val incr_bv: int * int * term > term 

92 
val incr_boundvars: int > term > term 

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

94 
val loose_bnos: term > int list 

95 
val loose_bvar: term * int > bool 

96 
val loose_bvar1: term * int > bool 

97 
val subst_bounds: term list * term > term 

98 
val subst_bound: term * term > term 

99 
val betapply: term * term > term 

100 
val eq_ix: indexname * indexname > bool 

101 
val ins_ix: indexname * indexname list > indexname list 

102 
val mem_ix: indexname * indexname list > bool 

103 
val mem_term: term * term list > bool 

104 
val subset_term: term list * term list > bool 

105 
val eq_set_term: term list * term list > bool 

106 
val ins_term: term * term list > term list 

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

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

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

112 
val abstract_over: term * term > term 

11922  113 
val lambda: term > term > term 
4444  114 
val absfree: string * typ * term > term 
115 
val list_abs_free: (string * typ) list * term > term 

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

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

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

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

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

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

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

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

125 
val is_first_order: string list > term > bool 

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

128 
val maxidx_of_term: term > int 

129 
val variant: string list > string > string 

130 
val variantlist: string list * string list > string list 

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

134 
val add_term_classes: term * class list > class list 

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

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

142 
val add_typ_tfree_names: typ * string list > string list 

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

144 
val add_typ_varnames: typ * string list > string list 

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

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

147 
val add_term_tfree_names: term * string list > string list 

148 
val add_term_tvarnames: term * string list > string list 

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

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

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

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

153 
val add_typ_ixns: indexname list * typ > indexname list 

154 
val add_term_tvar_ixns: term * indexname list > indexname list 

155 
val add_term_vars: term * term list > term list 

156 
val term_vars: term > term list 

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

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

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

4444  164 
signature TERM = 
165 
sig 

166 
include BASIC_TERM 

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

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

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

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

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

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

177 
val typ_ord: typ * typ > order 

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

181 
val termless: term * term > bool 

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

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

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

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

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

194 
val maxidx_term: term > int > int 

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

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

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

203 
val zero_var_indexes_inst: term > 

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

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

205 
val dummy_patternN: string 
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 
4444  213 
end; 
214 

215 
structure Term: TERM = 

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

216 
struct 
0  217 

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

219 
for resolution.*) 

16537  220 
type indexname = string * int; 
0  221 

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

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

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

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

228 
datatype typ = Type of string * typ list 

229 
 TFree of string * sort 

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

230 
 TVar of indexname * sort; 
0  231 

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

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

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

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

239 

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

245 
 Abs of string*typ*term 

3965  246 
 op $ of term*term; 
0  247 

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

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

254 
(*Note variable naming conventions! 

255 
a,b,c: string 

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

257 
i,j,m,n: int 

258 
t,u: term 

259 
v,w: indexnames 

260 
x,y: any 

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

262 
T,U: typ 

263 
*) 

264 

265 

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

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

267 

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

270 

271 
fun no_dummyT typ = 

272 
let 

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

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

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

276 
 check _ = (); 

277 
in check typ; typ end; 

278 

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

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

280 

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

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

283 

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

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

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

288 
fun dest_TFree (TFree x) = x 

289 
 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

290 

16537  291 

0  292 
(** Discriminators **) 
293 

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

296 

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

299 

300 
fun is_Free (Free _) = true 

301 
 is_Free _ = false; 

302 

303 
fun is_Var (Var _) = true 

304 
 is_Var _ = false; 

305 

306 
fun is_TVar (TVar _) = true 

307 
 is_TVar _ = false; 

308 

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

311 
 is_funtype _ = false; 

312 

16537  313 

0  314 
(** Destructors **) 
315 

316 
fun dest_Const (Const x) = x 

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

318 

319 
fun dest_Free (Free x) = x 

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

321 

322 
fun dest_Var (Var x) = x 

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

324 

325 

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

4064  328 

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

331 
 binder_types _ = []; 

332 

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

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

335 
 body_type T = T; 

336 

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

338 
fun strip_type T : typ list * typ = 

339 
(binder_types T, body_type T); 

340 

341 

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

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

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

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

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

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

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

353 
in case T of 

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

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

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

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

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

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

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

363 

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

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

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

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

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

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

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

0  377 

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

380 
let 

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

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

383 

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

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

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

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

388 
in arg 0 [] tm end; 

389 

0  390 

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

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

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

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

401 

402 
fun strip_qnt_body qnt = 

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

404 
 strip t = t 

405 
in strip end; 

406 

407 
fun strip_qnt_vars qnt = 

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

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

410 
in strip end; 

411 

412 

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

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

416 

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

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

423 

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

425 
fun head_of (f$t) = head_of f 

426 
 head_of u = u; 

427 

428 

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

431 
let 

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

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

435 
in add_size (tm, 0) end; 

0  436 

16678  437 
fun map_type_tvar f = 
438 
let 

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

440 
 map_aux (TVar x) = f x 

441 
 map_aux T = T; 

442 
in map_aux end; 

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

443 

16678  444 
fun map_type_tfree f = 
445 
let 

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

447 
 map_aux (TFree x) = f x 

448 
 map_aux T = T; 

449 
in map_aux end; 

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

450 

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

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

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

456 
 map_aux (t as Bound _) = t 

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

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

459 
in map_aux end; 

0  460 

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

462 
fun it_term_types f = 

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

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

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

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

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

468 
 iter(Bound _, a) = a 

469 
in iter end 

470 

471 

16943  472 
(* fold types and terms *) 
473 

474 
(*fold atoms of type*) 

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

476 
 fold_atyps f T = f T; 

477 

478 
(*fold atoms of term*) 

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

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

481 
 fold_aterms f a = f a; 

482 

483 
(*fold types of term*) 

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

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

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

487 
 fold_term_types f (Bound _) = I 

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

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

490 

491 
fun fold_types f = fold_term_types (K f); 

492 

493 
(*collect variables*) 

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

495 
val add_tvars = fold_types add_tvarsT; 

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

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

498 
val add_tfrees = fold_types add_tfreesT; 

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

500 

501 
(*collect variable names*) 

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

503 
fun term_varnames t = add_term_varnames t []; 

504 

505 

16678  506 
(** Comparing terms, types, sorts etc. **) 
16537  507 

16678  508 
(* fast syntactic comparison *) 
509 

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

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

16537  512 

16599  513 
fun sort_ord SS = 
514 
if pointer_eq SS then EQUAL 

16990  515 
else dict_ord fast_string_ord SS; 
16678  516 

517 
local 

16537  518 

16678  519 
fun cons_nr (TVar _) = 0 
520 
 cons_nr (TFree _) = 1 

521 
 cons_nr (Type _) = 2; 

16537  522 

16678  523 
in 
16537  524 

525 
fun typ_ord TU = 

526 
if pointer_eq TU then EQUAL 

527 
else 

528 
(case TU of 

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

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

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

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

536 

537 
end; 

538 

539 
local 

540 

541 
fun cons_nr (Const _) = 0 

542 
 cons_nr (Free _) = 1 

543 
 cons_nr (Var _) = 2 

544 
 cons_nr (Bound _) = 3 

545 
 cons_nr (Abs _) = 4 

546 
 cons_nr (_ $ _) = 5; 

547 

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

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

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

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

552 

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

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

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

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

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

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

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

560 
 atoms_ord _ = sys_error "atoms_ord"; 

561 

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

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

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

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

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

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

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

569 
 types_ord (Bound _, Bound _) = EQUAL 

570 
 types_ord _ = sys_error "types_ord"; 

571 

572 
in 

573 

574 
fun fast_term_ord tu = 

575 
if pointer_eq tu then EQUAL 

576 
else 

577 
(case struct_ord tu of 

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

579 
 ord => ord); 

580 

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

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

583 

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

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

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

587 

588 
end; 

16537  589 

590 

591 
(* term_ord *) 

592 

593 
(*a linear wellfounded ACcompatible ordering for terms: 

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

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

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

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

16678  598 

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

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

601 

16667  602 
local 
603 

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

605 
 hd_depth p = p; 

16537  606 

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

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

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

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

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

612 

16667  613 
in 
614 

16537  615 
fun term_ord tu = 
616 
if pointer_eq tu then EQUAL 

617 
else 

618 
(case tu of 

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

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

16667  621 
 (t, u) => 
16537  622 
(case int_ord (size_of_term t, size_of_term u) of 
623 
EQUAL => 

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

16537  626 
 ord => ord)) 
627 
and hd_ord (f, g) = 

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

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

631 
 args_ord _ = EQUAL; 

16537  632 

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

634 

16667  635 
end; 
636 

637 

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

639 

640 
(* 

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

643 
constants. 

644 

645 
f_ord maps strings to integers and serves two purposes: 

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

647 
must be mapped to ~1. 

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

649 
integers >= 0. 

650 

16667  651 
*) 
16570  652 

653 
local 

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

657 
end 

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

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

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

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

662 

663 
fun term_lpo f_ord (s, t) = 

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

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

666 
then case hd_ord f_ord (f, g) of 

16667  667 
GREATER => 
668 
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts 

669 
then GREATER else LESS 

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

673 
else LESS 

16570  674 
 LESS => LESS 
675 
else GREATER 

676 
end 

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

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

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

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

681 
(prod_ord indexname_ord typ_ord)) int_ord 

682 
(dest_hd f_ord f, dest_hd f_ord g) 

683 
in 

684 
val term_lpo = term_lpo 

685 
end; 

686 

16537  687 

0  688 
(** Connectives of higher order logic **) 
689 

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

0  693 
val propT : typ = Type("prop",[]); 
694 

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

696 

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

698 

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

700 

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

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

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

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

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

710 
(*increments a term's nonlocal bound variables 

711 
required when moving a term within abstractions 

712 
inc is increment for bound variables 

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

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

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

720 

721 
fun incr_boundvars 0 t = t 

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

723 

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

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

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

728 
else (x,y)::al) 

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

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

731 

732 
(* strip abstractions created by parameters *) 

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

734 

735 
fun rename_abs pat obj t = 

736 
let 

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

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

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

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

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

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

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

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

13000  750 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
0  751 
 add_loose_bnos (_, _, js) = js; 
752 

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

754 

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

756 
level k or beyond. *) 

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

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

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

760 
 loose_bvar _ = false; 

761 

2792  762 
fun loose_bvar1(Bound i,k) = i = k 
763 
 loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 

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

765 
 loose_bvar1 _ = false; 

0  766 

767 
(*Substitute arguments for loose bound variables. 

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

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

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

773 
*) 

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

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

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

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

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

780 
 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

781 
 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

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

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

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

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

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

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

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

791 
 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

792 
 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

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

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

795 

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

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

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

800 

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

802 

16882  803 
(* indexnames *) 
804 

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

806 

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

809 

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

811 

0  812 

16882  813 
(* variables *) 
814 

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

817 

818 
val tvar_ord = prod_ord indexname_ord sort_ord; 

819 
val var_ord = prod_ord indexname_ord typ_ord; 

16882  820 

821 

822 
(* terms *) 

2176  823 

824 
fun mem_term (_, []) = false 

16882  825 
 mem_term (t, t'::ts) = t aconv t' orelse mem_term (t, ts); 
2176  826 

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

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

828 
 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

829 

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

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

831 
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

832 

2176  833 
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; 
834 

835 
fun union_term (xs, []) = xs 

836 
 union_term ([], ys) = ys 

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

838 

5585  839 
fun inter_term ([], ys) = [] 
840 
 inter_term (x::xs, ys) = 

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

842 

16882  843 

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

847 
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

848 
 matchrands _ = true 
0  849 
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

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

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

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

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

856 
 (_, Abs _) => true 

857 
 _ => false 

858 
end; 

859 

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

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

862 
 subst_free pairs = 

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

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

868 
 _ => u) 
0  869 
in substf end; 
870 

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

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

873 

874 

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

16882  878 
fun abstract_over (v, body) = 
879 
let 

16990  880 
exception SAME; 
881 
fun abs lev tm = 

882 
if v aconv tm then Bound lev 

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

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

887 
 _ => raise SAME); 

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

0  889 

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

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

0  893 

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

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

896 

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

898 
fun list_abs_free ([ ] , t) = t 

13000  899 
 list_abs_free ((a,T)::vars, t) = 
0  900 
absfree(a, T, list_abs_free(vars,t)); 
901 

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

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

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

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

908 
fun list_all ([], t) = t 

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

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

916 
let 

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

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

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

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

924 
 typ_subst_atomic inst ty = 

925 
let 

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

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

16678  930 
fun subst_atomic_types [] tm = tm 
931 
 subst_atomic_types inst tm = map_term_types (typ_subst_atomic inst) tm; 

932 

933 
fun typ_subst_TVars [] ty = ty 

934 
 typ_subst_TVars inst ty = 

935 
let 

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

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

0  940 

16678  941 
fun subst_TVars [] tm = tm 
942 
 subst_TVars inst tm = map_term_types (typ_subst_TVars inst) tm; 

0  943 

16678  944 
(*see also Envir.norm_term*) 
945 
fun subst_Vars [] tm = tm 

946 
 subst_Vars inst tm = 

947 
let 

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

951 
 subst t = t; 

952 
in subst tm end; 

0  953 

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

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

957 
 subst_vars (instT, inst) tm = 

958 
let 

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

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

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

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

965 
 subst (t as Bound _) = t 

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

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

968 
in subst tm end; 

0  969 

970 

16943  971 
(* instantiation of schematic variables (types before terms) *) 
16882  972 

973 
local exception SAME in 

974 

16943  975 
fun instantiateT_same [] _ = raise SAME 
976 
 instantiateT_same instT ty = 

16882  977 
let 
978 
fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts) 

979 
 subst_typ (TVar v) = 

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

983 
 subst_typ _ = raise SAME 

984 
and subst_typs (T :: Ts) = 

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

986 
handle SAME => T :: subst_typs Ts) 

987 
 subst_typs [] = raise SAME; 

988 
in subst_typ ty end; 

989 

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

991 
 instantiate (instT, inst) tm = 

992 
let 

16943  993 
val substT = instantiateT_same instT; 
994 
fun subst (Const (c, T)) = Const (c, substT T) 

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

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

1001 
end 

1002 
 subst (Bound _) = raise SAME 

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

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

1007 
in subst tm handle SAME => tm end; 

1008 

1009 
fun instantiateT instT ty = 

16943  1010 
instantiateT_same instT ty handle SAME => ty; 
16882  1011 

1012 
end; 

1013 

1014 

15573  1015 
(** Identifying firstorder terms **) 
1016 

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

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

1019 

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

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

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

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

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

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

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

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

1035 
 _ => error "first_order: unexpected case" 

16589  1036 
in first_order1 [] end; 
15573  1037 

16710  1038 

16990  1039 
(* maximum index of typs and terms *) 
0  1040 

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

1043 
 maxidx_typ (TFree _) i = i 

1044 
and maxidx_typs [] i = i 

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

0  1046 

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

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

1050 
 maxidx_term (Bound _) i = i 

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

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

0  1053 

16710  1054 
fun maxidx_of_typ T = maxidx_typ T ~1; 
1055 
fun maxidx_of_typs Ts = maxidx_typs Ts ~1; 

1056 
fun maxidx_of_term t = maxidx_term t ~1; 

13665  1057 

0  1058 

1059 

1060 
(**** Syntaxrelated declarations ****) 

1061 

1062 
(*** Printing ***) 

1063 

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

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

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

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

1072 
in vary1 (if c = "" then "u" else c) ^ u end; 
0  1073 

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

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

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

1079 

14695  1080 
(*Invent fresh names*) 
1081 
fun invent_names _ _ 0 = [] 

1082 
 invent_names used a n = 

1083 
let val b = Symbol.bump_string a in 

1084 
if a mem_string used then invent_names used b n 

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

1086 
end; 

11353  1087 

16537  1088 

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

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

1090 

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

1091 
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

1092 
 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

1093 
 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

1094 

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

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

1097 

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

1098 
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

1099 
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

1100 

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

1102 
 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

1103 
 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

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

1105 

13646  1106 
fun term_consts t = add_term_consts(t,[]); 
1107 

16943  1108 
fun exists_subterm P = 
1109 
let 

1110 
fun ex tm = P tm orelse 

1111 
(case tm of 

1112 
t $ u => ex t orelse ex u 

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

1114 
 _ => false); 

1115 
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

1116 

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

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

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

1120 
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

1121 
 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

1122 
 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

1123 

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

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

1125 
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

1126 
 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

1127 
 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

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

1129 
 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

1130 
 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

1131 

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

1132 

0  1133 
(** TFrees and TVars **) 
1134 

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

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

1136 
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

1137 
 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

1138 
 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

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

1140 

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

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

1147 
 add_term_names (_, bs) = bs; 

1148 

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

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

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

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

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

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

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

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

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

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

1166 

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

1169 

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

1171 
val add_term_tfrees = it_term_types add_typ_tfrees; 

1172 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

1173 

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

1174 
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

1175 

0  1176 
(*Nonlist versions*) 
1177 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

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

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

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

1181 

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

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

1183 

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

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

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

1188 

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

1189 
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

1190 
 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

1191 
 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

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

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

1194 
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

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

1196 
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

1197 

16537  1198 

0  1199 
(** Frees and Vars **) 
1200 

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

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

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

1206 
 _ => vars; 

1207 

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

1209 

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

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

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

1215 
 _ => frees; 

1216 

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

1218 

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

16678  1220 
having a unique name*) 
0  1221 
fun variant_abs (a,T,P) = 
1222 
let val b = variant (add_term_names(P,[])) a 

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

1223 
in (b, subst_bound (Free(b,T), P)) end; 
0  1224 

16678  1225 
fun dest_abs (x, T, body) = 
1226 
let 

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

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

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

1230 
 name_clash _ = false; 

1231 
in 

1232 
if name_clash body then 

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

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

1235 
end; 

1236 

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

1239 
local 

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

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

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

1243 
in 

1244 
fun bound n = 

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

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

1247 
end; 

1248 

1249 
val is_bound = String.isPrefix ":"; 

16943  1250 

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

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

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

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

1257 
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

1258 

1417  1259 

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

1261 

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

1264 
let 

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

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

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

1269 

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

16790  1272 

16943  1273 
fun zero_var_indexes_inst tm = 
1274 
let 

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

1276 
val inst = 

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

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

1279 
in (instT, inst) end; 

12499  1280 

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

1282 

1417  1283 

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

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

1285 

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

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

1287 

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 

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

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

1351 

4444  1352 
structure BasicTerm: BASIC_TERM = Term; 
1353 
open BasicTerm; 