author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 24850  0cfd722ab579 
child 24982  f2f0722675b1 
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 

22572  16 
eqtype indexname 
17 
eqtype class 

18 
eqtype sort 

19 
eqtype arity 

4444  20 
datatype typ = 
21 
Type of string * typ list  

22 
TFree of string * sort  

23 
TVar of indexname * sort 

16537  24 
datatype term = 
25 
Const of string * typ  

26 
Free of string * typ  

27 
Var of indexname * typ  

28 
Bound of int  

29 
Abs of string * typ * term  

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

21353  33 
val dummyS: sort 
16710  34 
val dummyT: typ 
35 
val no_dummyT: typ > typ 

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

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

40 
val dest_TFree: typ > string * sort 

41 
val is_Bound: term > bool 

42 
val is_Const: term > bool 

43 
val is_Free: term > bool 

44 
val is_Var: term > bool 

4444  45 
val is_TVar: 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 
18927  59 
val strip_abs: term > (string * typ) list * term 
4444  60 
val strip_abs_body: term > term 
61 
val strip_abs_vars: term > (string * typ) list 

62 
val strip_qnt_body: string > term > term 

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

64 
val list_comb: term * term list > term 

65 
val strip_comb: term > term * term list 

66 
val head_of: term > term 

67 
val size_of_term: term > int 

18847  68 
val map_atyps: (typ > typ) > typ > typ 
69 
val map_aterms: (term > term) > term > term 

4444  70 
val map_type_tvar: (indexname * sort > typ) > typ > typ 
71 
val map_type_tfree: (string * sort > typ) > typ > typ 

20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20531
diff
changeset

72 
val map_types: (typ > typ) > term > term 
16943  73 
val fold_atyps: (typ > 'a > 'a) > typ > 'a > 'a 
74 
val fold_aterms: (term > 'a > 'a) > term > 'a > 'a 

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

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

24483  77 
val burrow_types: (typ list > typ list) > term list > term list 
18927  78 
val it_term_types: (typ * 'a > 'a) > term * 'a > 'a 
16943  79 
val add_term_names: term * string list > string list 
16710  80 
val aconv: term * term > bool 
16537  81 
structure Vartab: TABLE 
82 
structure Typtab: TABLE 

83 
structure Termtab: TABLE 

4444  84 
val propT: typ 
85 
val implies: term 

86 
val all: typ > term 

87 
val equals: typ > term 

88 
val strip_all_body: term > term 

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

90 
val incr_bv: int * int * term > term 

91 
val incr_boundvars: int > term > term 

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

93 
val loose_bnos: term > int list 

94 
val loose_bvar: term * int > bool 

95 
val loose_bvar1: term * int > bool 

96 
val subst_bounds: term list * term > term 

97 
val subst_bound: term * term > term 

98 
val betapply: term * term > term 

18183  99 
val betapplys: term * term list > term 
4444  100 
val eq_ix: indexname * indexname > bool 
101 
val could_unify: term * term > bool 

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

103 
val abstract_over: term * term > term 

11922  104 
val lambda: term > term > term 
4444  105 
val absfree: string * typ * term > term 
17786  106 
val absdummy: typ * term > term 
4444  107 
val list_abs_free: (string * typ) list * term > term 
108 
val list_all_free: (string * typ) list * term > term 

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

16710  110 
val subst_atomic: (term * term) list > term > term 
111 
val typ_subst_atomic: (typ * typ) list > typ > typ 

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

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

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

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

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

117 
val is_first_order: string list > term > bool 

4444  118 
val maxidx_of_typ: typ > int 
119 
val maxidx_of_typs: typ list > int 

120 
val maxidx_of_term: term > int 

121 
val add_term_consts: term * string list > string list 

13646  122 
val term_consts: term > string list 
19909  123 
val exists_subtype: (typ > bool) > typ > bool 
20531  124 
val exists_type: (typ > bool) > term > bool 
16943  125 
val exists_subterm: (term > bool) > term > bool 
16710  126 
val exists_Const: (string * typ > bool) > term > bool 
127 
val add_term_free_names: term * string list > string list 

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

129 
val add_typ_tfree_names: typ * string list > string list 

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

131 
val add_typ_varnames: typ * string list > string list 

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

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

134 
val add_term_tfree_names: term * string list > string list 

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

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

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

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

139 
val add_typ_ixns: indexname list * typ > indexname list 

140 
val add_term_tvar_ixns: term * indexname list > indexname list 

141 
val add_term_vars: term * term list > term list 

142 
val term_vars: term > term list 

4444  143 
val add_term_frees: term * term list > term list 
144 
val term_frees: term > term list 

20160  145 
val rename_wrt_term: term > (string * 'a) list > (string * 'a) list 
15986  146 
val show_question_marks: bool ref 
4444  147 
end; 
0  148 

4444  149 
signature TERM = 
150 
sig 

151 
include BASIC_TERM 

19394  152 
val aT: sort > typ 
153 
val itselfT: typ > typ 

154 
val a_itselfT: typ 

22908  155 
val argument_type_of: term > int > typ 
21493  156 
val head_name_of: term > string 
16943  157 
val add_tvarsT: typ > (indexname * sort) list > (indexname * sort) list 
158 
val add_tvars: term > (indexname * sort) list > (indexname * sort) list 

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

21682  160 
val add_varnames: term > indexname list > indexname list 
16943  161 
val add_tfreesT: typ > (string * sort) list > (string * sort) list 
162 
val add_tfrees: term > (string * sort) list > (string * sort) list 

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

21682  164 
val hidden_polymorphism: term > typ > (indexname * sort) list 
21797  165 
val equiv_types: term * term > bool 
20109  166 
val strip_abs_eta: int > term > (string * typ) list * term 
16678  167 
val fast_indexname_ord: indexname * indexname > order 
16537  168 
val indexname_ord: indexname * indexname > order 
169 
val sort_ord: sort * sort > order 

170 
val typ_ord: typ * typ > order 

16678  171 
val fast_term_ord: term * term > order 
16537  172 
val term_ord: term * term > order 
173 
val hd_ord: term * term > order 

174 
val termless: term * term > bool 

20129
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

175 
val term_lpo: (term > int) > term * term > order 
12981  176 
val match_bvars: (term * term) * (string * string) list > (string * string) list 
22031  177 
val map_abs_vars: (string > string) > term > term 
12981  178 
val rename_abs: term > term > term > term option 
16943  179 
val eq_tvar: (indexname * sort) * (indexname * sort) > bool 
16882  180 
val eq_var: (indexname * typ) * (indexname * typ) > bool 
16943  181 
val tvar_ord: (indexname * sort) * (indexname * sort) > order 
182 
val var_ord: (indexname * typ) * (indexname * typ) > order 

16710  183 
val maxidx_typ: typ > int > int 
184 
val maxidx_typs: typ list > int > int 

185 
val maxidx_term: term > int > int 

24671  186 
val has_abs: term > bool 
20239  187 
val dest_abs: string * typ * term > string * term 
24762  188 
val declare_typ_names: typ > Name.context > Name.context 
20148  189 
val declare_term_names: term > Name.context > Name.context 
20160  190 
val variant_frees: term > (string * 'a) list > (string * 'a) list 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

191 
val dummy_patternN: string 
18253  192 
val dummy_pattern: typ > term 
22723  193 
val is_dummy_pattern: term > bool 
24733  194 
val free_dummy_patterns: term > Name.context > term * Name.context 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

195 
val no_dummy_patterns: term > term 
24762  196 
val replace_dummy_patterns: term > int > term * int 
10552  197 
val is_replaced_dummy_pattern: indexname > bool 
16035  198 
val show_dummy_patterns: term > term 
14786
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 
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

200 
val string_of_vname': indexname > 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 

21353  256 
(*dummies for typeinference etc.*) 
257 
val dummyS = [""]; 

16537  258 
val dummyT = Type ("dummy", []); 
259 

260 
fun no_dummyT typ = 

261 
let 

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

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

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

265 
 check _ = (); 

266 
in check typ; typ end; 

267 

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

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

269 

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

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

272 

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

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

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

277 
fun dest_TFree (TFree x) = x 

278 
 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

279 

16537  280 

0  281 
(** Discriminators **) 
282 

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

285 

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

288 

289 
fun is_Free (Free _) = true 

290 
 is_Free _ = false; 

291 

292 
fun is_Var (Var _) = true 

293 
 is_Var _ = false; 

294 

295 
fun is_TVar (TVar _) = true 

296 
 is_TVar _ = false; 

297 

16537  298 

0  299 
(** Destructors **) 
300 

301 
fun dest_Const (Const x) = x 

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

303 

304 
fun dest_Free (Free x) = x 

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

306 

307 
fun dest_Var (Var x) = x 

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

309 

310 

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

4064  313 

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

316 
 binder_types _ = []; 

317 

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

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

320 
 body_type T = T; 

321 

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

323 
fun strip_type T : typ list * typ = 

324 
(binder_types T, body_type T); 

325 

326 

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

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

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

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

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

0  333 
 type_of1 (Ts, Var (_,T)) = T 
334 
 type_of1 (Ts, Abs (_,T,body)) = T > type_of1(T::Ts, body) 

13000  335 
 type_of1 (Ts, f$u) = 
0  336 
let val U = type_of1(Ts,u) 
337 
and T = type_of1(Ts,f) 

338 
in case T of 

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

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

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

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

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

344 
[T,U], [f$u]) 
0  345 
end; 
346 

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

348 

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

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

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

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

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

13000  358 
 fastype_of1 (_, Var (_,T)) = T 
61  359 
 fastype_of1 (Ts, Abs (_,T,u)) = T > fastype_of1 (T::Ts, u); 
360 

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

0  362 

16678  363 
(*Determine the argument type of a function*) 
22908  364 
fun argument_type_of tm k = 
16678  365 
let 
366 
fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i  1) U 

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

368 

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

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

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

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

22908  373 
in arg k [] tm end; 
16678  374 

0  375 

19473  376 
val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t))); 
10806  377 

18927  378 
fun strip_abs (Abs (a, T, t)) = 
379 
let val (a', t') = strip_abs t 

380 
in ((a, T) :: a', t') end 

381 
 strip_abs t = ([], t); 

382 

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

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

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

391 

392 
fun strip_qnt_body qnt = 

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

394 
 strip t = t 

395 
in strip end; 

396 

397 
fun strip_qnt_vars qnt = 

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

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

400 
in strip end; 

401 

402 

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

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

406 

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

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

413 

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

415 
fun head_of (f$t) = head_of f 

416 
 head_of u = u; 

417 

21493  418 
fun head_name_of tm = 
419 
(case head_of tm of 

420 
t as Const (c, _) => 

421 
if NameSpace.is_qualified c then c 

422 
else raise TERM ("Malformed constant name", [t]) 

423 
 t as Free (x, _) => 

424 
if not (NameSpace.is_qualified x) then x 

425 
else raise TERM ("Malformed fixed variable name", [t]) 

426 
 t => raise TERM ("No fixed head of term", [t])); 

0  427 

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

430 
let 

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

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

434 
in add_size (tm, 0) end; 

0  435 

18847  436 
fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts) 
18976
4efb82669880
fixed the most silly bug conceivable in map_atyps
haftmann
parents:
18975
diff
changeset

437 
 map_atyps f T = f T; 
18847  438 

439 
fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u 

440 
 map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t) 

441 
 map_aterms f t = f t; 

442 

18981  443 
fun map_type_tvar f = map_atyps (fn TVar x => f x  T => T); 
444 
fun map_type_tfree f = map_atyps (fn TFree x => f x  T => T); 

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

445 

20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20531
diff
changeset

446 
fun map_types f = 
16678  447 
let 
448 
fun map_aux (Const (a, T)) = Const (a, f T) 

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

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

451 
 map_aux (t as Bound _) = t 

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

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

454 
in map_aux end; 

0  455 

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

457 
fun it_term_types f = 

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

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

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

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

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

463 
 iter(Bound _, a) = a 

464 
in iter end 

465 

466 

16943  467 
(* fold types and terms *) 
468 

469 
(*fold atoms of type*) 

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

471 
 fold_atyps f T = f T; 

472 

473 
(*fold atoms of term*) 

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

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

476 
 fold_aterms f a = f a; 

477 

478 
(*fold types of term*) 

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

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

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

482 
 fold_term_types f (Bound _) = I 

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

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

485 

486 
fun fold_types f = fold_term_types (K f); 

487 

24483  488 
fun replace_types (Const (c, _)) (T :: Ts) = (Const (c, T), Ts) 
489 
 replace_types (Free (x, _)) (T :: Ts) = (Free (x, T), Ts) 

490 
 replace_types (Var (xi, _)) (T :: Ts) = (Var (xi, T), Ts) 

491 
 replace_types (Bound i) Ts = (Bound i, Ts) 

492 
 replace_types (Abs (x, _, b)) (T :: Ts) = 

493 
let val (b', Ts') = replace_types b Ts 

494 
in (Abs (x, T, b'), Ts') end 

495 
 replace_types (t $ u) Ts = 

496 
let 

497 
val (t', Ts') = replace_types t Ts; 

498 
val (u', Ts'') = replace_types u Ts'; 

499 
in (t' $ u', Ts'') end; 

500 

501 
fun burrow_types f ts = 

502 
let 

503 
val Ts = rev (fold (fold_types cons) ts []); 

504 
val Ts' = f Ts; 

505 
val (ts', []) = fold_map replace_types ts Ts'; 

506 
in ts' end; 

507 

16943  508 
(*collect variables*) 
509 
val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v  _ => I); 

510 
val add_tvars = fold_types add_tvarsT; 

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

20199  512 
val add_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi  _ => I); 
16943  513 
val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v  _ => I); 
514 
val add_tfrees = fold_types add_tfreesT; 

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

516 

21682  517 
(*extra type variables in a term, not covered by the type*) 
518 
fun hidden_polymorphism t T = 

519 
let 

520 
val tvarsT = add_tvarsT T []; 

521 
val extra_tvars = fold_types (fold_atyps 

522 
(fn TVar v => if member (op =) tvarsT v then I else insert (op =) v  _ => I)) t []; 

523 
in extra_tvars end; 

524 

16943  525 

16678  526 
(** Comparing terms, types, sorts etc. **) 
16537  527 

20511  528 
(* alpha equivalence  tuned for equalities *) 
529 

530 
fun tm1 aconv tm2 = 

531 
pointer_eq (tm1, tm2) orelse 

532 
(case (tm1, tm2) of 

533 
(t1 $ u1, t2 $ u2) => t1 aconv t2 andalso u1 aconv u2 

534 
 (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2 

535 
 (a1, a2) => a1 = a2); 

536 

537 

21797  538 
(* equivalence up to renaming of types variables *) 
539 

540 
local 

541 

24850  542 
val invent_names = Name.invents Name.context Name.aT; 
21797  543 

544 
fun standard_types t = 

545 
let 

546 
val tfrees = add_tfrees t []; 

547 
val tvars = add_tvars t []; 

548 
val env1 = map2 (fn (a, S) => fn a' => (TFree (a, S), TFree (a', []))) 

549 
tfrees (invent_names (length tfrees)); 

550 
val env2 = map2 (fn ((a, i), S) => fn a' => (TVar ((a, i), S), TVar ((a', 0), []))) 

551 
tvars (invent_names (length tvars)); 

552 
in map_types (map_atyps (perhaps (AList.lookup (op =) (env1 @ env2)))) t end; 

553 

554 
in 

555 

556 
val equiv_types = op aconv o pairself standard_types; 

557 

558 
end; 

559 

560 

20511  561 
(* fast syntactic ordering  tuned for inequalities *) 
16678  562 

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

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

16537  565 

16599  566 
fun sort_ord SS = 
567 
if pointer_eq SS then EQUAL 

16990  568 
else dict_ord fast_string_ord SS; 
16678  569 

570 
local 

16537  571 

16678  572 
fun cons_nr (TVar _) = 0 
573 
 cons_nr (TFree _) = 1 

574 
 cons_nr (Type _) = 2; 

16537  575 

16678  576 
in 
16537  577 

578 
fun typ_ord TU = 

579 
if pointer_eq TU then EQUAL 

580 
else 

581 
(case TU of 

16678  582 
(Type (a, Ts), Type (b, Us)) => 
16990  583 
(case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us)  ord => ord) 
16678  584 
 (TFree (a, S), TFree (b, S')) => 
585 
(case fast_string_ord (a, b) of EQUAL => sort_ord (S, S')  ord => ord) 

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

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

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

589 

590 
end; 

591 

592 
local 

593 

594 
fun cons_nr (Const _) = 0 

595 
 cons_nr (Free _) = 1 

596 
 cons_nr (Var _) = 2 

597 
 cons_nr (Bound _) = 3 

598 
 cons_nr (Abs _) = 4 

599 
 cons_nr (_ $ _) = 5; 

600 

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

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

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

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

605 

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

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

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

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

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

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

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

613 
 atoms_ord _ = sys_error "atoms_ord"; 

614 

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

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

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

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

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

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

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

622 
 types_ord (Bound _, Bound _) = EQUAL 

623 
 types_ord _ = sys_error "types_ord"; 

624 

625 
in 

626 

627 
fun fast_term_ord tu = 

628 
if pointer_eq tu then EQUAL 

629 
else 

630 
(case struct_ord tu of 

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

632 
 ord => ord); 

633 

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

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

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

637 

638 
end; 

16537  639 

640 

641 
(* term_ord *) 

642 

643 
(*a linear wellfounded ACcompatible ordering for terms: 

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

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

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

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

16678  648 

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

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

651 

16667  652 
local 
653 

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

655 
 hd_depth p = p; 

16537  656 

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

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

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

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

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

662 

16667  663 
in 
664 

16537  665 
fun term_ord tu = 
666 
if pointer_eq tu then EQUAL 

667 
else 

668 
(case tu of 

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

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

16667  671 
 (t, u) => 
16537  672 
(case int_ord (size_of_term t, size_of_term u) of 
673 
EQUAL => 

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

16537  676 
 ord => ord)) 
677 
and hd_ord (f, g) = 

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

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

681 
 args_ord _ = EQUAL; 

16537  682 

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

684 

16667  685 
end; 
686 

687 

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

689 

690 
(* 

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

693 
constants. 

694 

20129
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

695 
f_ord maps terms to integers and serves two purposes: 
16570  696 
 Predicate on constant symbols. Those that are not recognised by f_ord 
697 
must be mapped to ~1. 

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

699 
integers >= 0. 

20129
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

700 
The argument of f_ord is never an application. 
16667  701 
*) 
16570  702 

703 
local 

20129
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

704 

95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

705 
fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0) 
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

706 
 unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0) 
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

707 
 unrecognized (Var v) = ((1, v), 1) 
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

708 
 unrecognized (Bound i) = ((1, (("", i), dummyT)), 2) 
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

709 
 unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3); 
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

710 

95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

711 
fun dest_hd f_ord t = 
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

712 
let val ord = f_ord t in 
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

713 
if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0) 
16570  714 
end 
715 

716 
fun term_lpo f_ord (s, t) = 

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

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

719 
then case hd_ord f_ord (f, g) of 

16667  720 
GREATER => 
721 
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts 

722 
then GREATER else LESS 

16570  723 
 EQUAL => 
16667  724 
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts 
725 
then list_ord (term_lpo f_ord) (ss, ts) 

726 
else LESS 

16570  727 
 LESS => LESS 
728 
else GREATER 

729 
end 

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

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

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

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

734 
(prod_ord indexname_ord typ_ord)) int_ord 

735 
(dest_hd f_ord f, dest_hd f_ord g) 

736 
in 

737 
val term_lpo = term_lpo 

738 
end; 

739 

16537  740 

0  741 
(** Connectives of higher order logic **) 
742 

24850  743 
fun aT S = TFree (Name.aT, S); 
19394  744 

375  745 
fun itselfT ty = Type ("itself", [ty]); 
24850  746 
val a_itselfT = itselfT (TFree (Name.aT, [])); 
375  747 

0  748 
val propT : typ = Type("prop",[]); 
749 

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

751 

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

753 

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

755 

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

13000  757 
fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t 
0  758 
 strip_all_body t = t; 
759 

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

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

13000  762 
(a,T) :: strip_all_vars t 
0  763 
 strip_all_vars t = [] : (string*typ) list; 
764 

765 
(*increments a term's nonlocal bound variables 

766 
required when moving a term within abstractions 

767 
inc is increment for bound variables 

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

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

771 
Abs(a, T, incr_bv(inc,lev+1,body)) 
13000  772 
 incr_bv (inc, lev, f$t) = 
0  773 
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 
774 
 incr_bv (inc, lev, u) = u; 

775 

776 
fun incr_boundvars 0 t = t 

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

778 

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

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

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

783 
else (x,y)::al) 

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

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

786 

787 
(* strip abstractions created by parameters *) 

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

789 

22031  790 
fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u 
791 
 map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t) 

792 
 map_abs_vars f t = t; 

793 

12981  794 
fun rename_abs pat obj t = 
795 
let 

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

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

18942  798 
Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b) 
12981  799 
 ren_abs (f $ t) = ren_abs f $ ren_abs t 
800 
 ren_abs t = t 

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

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

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

13000  805 
fun add_loose_bnos (Bound i, lev, js) = 
20854  806 
if i<lev then js else insert (op =) (i  lev) js 
0  807 
 add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js) 
808 
 add_loose_bnos (f$t, lev, js) = 

13000  809 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
0  810 
 add_loose_bnos (_, _, js) = js; 
811 

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

813 

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

815 
level k or beyond. *) 

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

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

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

819 
 loose_bvar _ = false; 

820 

2792  821 
fun loose_bvar1(Bound i,k) = i = k 
822 
 loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 

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

824 
 loose_bvar1 _ = false; 

0  825 

826 
(*Substitute arguments for loose bound variables. 

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

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

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

832 
*) 

13000  833 
fun subst_bounds (args: term list, t) : term = 
19065  834 
let 
835 
exception SAME; 

836 
val n = length args; 

837 
fun subst (t as Bound i, lev) = 

838 
(if i < lev then raise SAME (*var is locally bound*) 

839 
else incr_boundvars lev (List.nth (args, i  lev)) 

840 
handle Subscript => Bound (i  n)) (*loose: change it*) 

841 
 subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1)) 

842 
 subst (f $ t, lev) = 

843 
(subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev)) 

844 
 subst _ = raise SAME; 

845 
in case args of [] => t  _ => (subst (t, 0) handle SAME => t) end; 

0  846 

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

847 
(*Special case: one argument*) 
13000  848 
fun subst_bound (arg, t) : term = 
19065  849 
let 
850 
exception SAME; 

851 
fun subst (Bound i, lev) = 

852 
if i < lev then raise SAME (*var is locally bound*) 

853 
else if i = lev then incr_boundvars lev arg 

854 
else Bound (i  1) (*loose: change it*) 

855 
 subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1)) 

856 
 subst (f $ t, lev) = 

857 
(subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev)) 

858 
 subst _ = raise SAME; 

859 
in subst (t, 0) handle SAME => t end; 

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

860 

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

862 
fun betapply (Abs(_,_,t), u) = subst_bound (u,t) 
0  863 
 betapply (f,u) = f$u; 
864 

18183  865 
val betapplys = Library.foldl betapply; 
866 

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

867 

20109  868 
(*unfolding abstractions with substitution 
869 
of bound variables and implicit etaexpansion*) 

870 
fun strip_abs_eta k t = 

871 
let 

20122  872 
val used = fold_aterms (fn Free (v, _) => Name.declare v  _ => I) t Name.context; 
20109  873 
fun strip_abs t (0, used) = (([], t), (0, used)) 
874 
 strip_abs (Abs (v, T, t)) (k, used) = 

875 
let 

20122  876 
val ([v'], used') = Name.variants [v] used; 
21013  877 
val t' = subst_bound (Free (v', T), t); 
20122  878 
val ((vs, t''), (k', used'')) = strip_abs t' (k  1, used'); 
879 
in (((v', T) :: vs, t''), (k', used'')) end 

20109  880 
 strip_abs t (k, used) = (([], t), (k, used)); 
881 
fun expand_eta [] t _ = ([], t) 

882 
 expand_eta (T::Ts) t used = 

883 
let 

20122  884 
val ([v], used') = Name.variants [""] used; 
885 
val (vs, t') = expand_eta Ts (t $ Free (v, T)) used'; 

20109  886 
in ((v, T) :: vs, t') end; 
887 
val ((vs1, t'), (k', used')) = strip_abs t (k, used); 

888 
val Ts = (fst o chop k' o fst o strip_type o fastype_of) t'; 

889 
val (vs2, t'') = expand_eta Ts t' used'; 

890 
in (vs1 @ vs2, t'') end; 

891 

892 

20199  893 
(* comparing variables *) 
16882  894 

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

896 

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

899 

900 
val tvar_ord = prod_ord indexname_ord sort_ord; 

901 
val var_ord = prod_ord indexname_ord typ_ord; 

16882  902 

903 

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

907 
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

908 
 matchrands _ = true 
0  909 
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

910 
(_, Var _) => true 
0  911 
 (Var _, _) => true 
912 
 (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u) 

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

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

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

916 
 (_, Abs _) => true 

917 
 _ => false 

918 
end; 

919 

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

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

922 
 subst_free pairs = 

13000  923 
let fun substf u = 
17314  924 
case AList.lookup (op aconv) pairs u of 
15531  925 
SOME u' => u' 
926 
 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

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

928 
 _ => u) 
0  929 
in substf end; 
930 

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

16882  934 
fun abstract_over (v, body) = 
935 
let 

16990  936 
exception SAME; 
937 
fun abs lev tm = 

938 
if v aconv tm then Bound lev 

16882  939 
else 
16990  940 
(case tm of 
941 
Abs (a, T, t) => Abs (a, T, abs (lev + 1) t) 

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

943 
 _ => raise SAME); 

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

0  945 

21975
1152dc45d591
Term.lambda: abstract over arbitrary closed terms;
wenzelm
parents:
21797
diff
changeset

946 
fun lambda v t = 
1152dc45d591
Term.lambda: abstract over arbitrary closed terms;
wenzelm
parents:
21797
diff
changeset

947 
let val x = 
1152dc45d591
Term.lambda: abstract over arbitrary closed terms;
wenzelm
parents:
21797
diff
changeset

948 
(case v of 
1152dc45d591
Term.lambda: abstract over arbitrary closed terms;
wenzelm
parents:
21797
diff
changeset

949 
Const (x, _) => NameSpace.base x 
1152dc45d591
Term.lambda: abstract over arbitrary closed terms;
wenzelm
parents:
21797
diff
changeset

950 
 Free (x, _) => x 
1152dc45d591
Term.lambda: abstract over arbitrary closed terms;
wenzelm
parents:
21797
diff
changeset

951 
 Var ((x, _), _) => x 
24850  952 
 _ => Name.uu) 
21975
1152dc45d591
Term.lambda: abstract over arbitrary closed terms;
wenzelm
parents:
21797
diff
changeset

953 
in Abs (x, fastype_of v, abstract_over (v, t)) end; 
0  954 

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

21975
1152dc45d591
Term.lambda: abstract over arbitrary closed terms;
wenzelm
parents:
21797
diff
changeset

956 
fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body)); 
24850  957 
fun absdummy (T, body) = Abs (Name.internal Name.uu, T, body); 
0  958 

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

960 
fun list_abs_free ([ ] , t) = t 

13000  961 
 list_abs_free ((a,T)::vars, t) = 
0  962 
absfree(a, T, list_abs_free(vars,t)); 
963 

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

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

13000  966 
 list_all_free ((a,T)::vars, t) = 
0  967 
(all T) $ (absfree(a, T, list_all_free(vars,t))); 
968 

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

970 
fun list_all ([], t) = t 

13000  971 
 list_all ((a,T)::vars, t) = 
0  972 
(all T) $ (Abs(a, T, list_all(vars,t))); 
973 

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

978 
let 

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

980 
 subst (t $ u) = subst t $ subst u 

18942  981 
 subst t = the_default t (AList.lookup (op aconv) inst t); 
16678  982 
in subst tm end; 
0  983 

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

986 
 typ_subst_atomic inst ty = 

987 
let 

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

18942  989 
 subst T = the_default T (AList.lookup (op = : typ * typ > bool) inst T); 
16678  990 
in subst ty end; 
15797  991 

16678  992 
fun subst_atomic_types [] tm = tm 
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20531
diff
changeset

993 
 subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm; 
16678  994 

995 
fun typ_subst_TVars [] ty = ty 

996 
 typ_subst_TVars inst ty = 

997 
let 

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

18942  999 
 subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi) 
16678  1000 
 subst T = T; 
1001 
in subst ty end; 

0  1002 

16678  1003 
fun subst_TVars [] tm = tm 
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20531
diff
changeset

1004 
 subst_TVars inst tm = map_types (typ_subst_TVars inst) tm; 
0  1005 

16678  1006 
fun subst_Vars [] tm = tm 
1007 
 subst_Vars inst tm = 

1008 
let 

18942  1009 
fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi) 
16678  1010 
 subst (Abs (a, T, t)) = Abs (a, T, subst t) 
1011 
 subst (t $ u) = subst t $ subst u 

1012 
 subst t = t; 

1013 
in subst tm end; 

0  1014 

16678  1015 
fun subst_vars ([], []) tm = tm 
1016 
 subst_vars ([], inst) tm = subst_Vars inst tm 

1017 
 subst_vars (instT, inst) tm = 

1018 
let 

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

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

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

17271  1022 
(case AList.lookup (op =) inst xi of 
16678  1023 
NONE => Var (xi, typ_subst_TVars instT T) 
1024 
 SOME t => t) 

1025 
 subst (t as Bound _) = t 

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

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

1028 
in subst tm end; 

0  1029 

1030 

15573  1031 
(** Identifying firstorder terms **) 
1032 

20199  1033 
(*Differs from proofterm/is_fun in its treatment of TVar*) 
1034 
fun is_funtype (Type("fun",[_,_])) = true 

1035 
 is_funtype _ = false; 

1036 

15573  1037 
(*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*) 
1038 
fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t))); 

1039 

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

16667  1043 
fun is_first_order quants = 
16589  1044 
let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body 
16667  1045 
 first_order1 Ts (Const(q,_) $ Abs(a,T,body)) = 
20664  1046 
member (op =) quants q andalso (*it is a known quantifier*) 
16589  1047 
not (is_funtype T) andalso first_order1 (T::Ts) body 
16667  1048 
 first_order1 Ts t = 
1049 
case strip_comb t of 

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

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

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

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

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

1055 
 _ => error "first_order: unexpected case" 

16589  1056 
in first_order1 [] end; 
15573  1057 

16710  1058 

16990  1059 
(* maximum index of typs and terms *) 
0  1060 

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

1063 
 maxidx_typ (TFree _) i = i 

1064 
and maxidx_typs [] i = i 

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

0  1066 

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

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

1070 
 maxidx_term (Bound _) i = i 

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

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

0  1073 

16710  1074 
fun maxidx_of_typ T = maxidx_typ T ~1; 
1075 
fun maxidx_of_typs Ts = maxidx_typs Ts ~1; 

1076 
fun maxidx_of_term t = maxidx_term t ~1; 

13665  1077 

0  1078 

1079 

1080 
(**** Syntaxrelated declarations ****) 

1081 

19909  1082 
(* substructure *) 
4017
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

1083 

19909  1084 
fun exists_subtype P = 
1085 
let 

1086 
fun ex ty = P ty orelse 

1087 
(case ty of Type (_, Ts) => exists ex Ts  _ => false); 

1088 
in ex end; 

13646  1089 

20531  1090 
fun exists_type P = 
1091 
let 

1092 
fun ex (Const (_, T)) = P T 

1093 
 ex (Free (_, T)) = P T 

1094 
 ex (Var (_, T)) = P T 

1095 
 ex (Bound _) = false 

1096 
 ex (Abs (_, T, t)) = P T orelse ex t 

1097 
 ex (t $ u) = ex t orelse ex u; 

1098 
in ex end; 

1099 

16943  1100 
fun exists_subterm P = 
1101 
let 

1102 
fun ex tm = P tm orelse 

1103 
(case tm of 

1104 
t $ u => ex t orelse ex u 

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

1106 
 _ => false); 

1107 
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

1108 

24671  1109 
fun has_abs (Abs _) = true 
1110 
 has_abs (t $ u) = has_abs t orelse has_abs u 

1111 
 has_abs _ = false; 

1112 

1113 

19909  1114 

1115 
(** Consts etc. **) 

1116 

1117 
fun add_term_consts (Const (c, _), cs) = insert (op =) c cs 

1118 
 add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs)) 

1119 
 add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs) 

1120 
 add_term_consts (_, cs) = cs; 

1121 

1122 
fun term_consts t = add_term_consts(t,[]); 

1123 

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

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

1126 

0  1127 
(** TFrees and TVars **) 
1128 

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

1129 
(*Accumulates the names of Frees in the term, suppressing duplicates.*) 
20854  1130 
fun add_term_free_names (Free(a,_), bs) = insert (op =) a bs 
12802
c69bd9754473
added add_term_free_names (more precise/efficient than add_term_names);
wenzelm
parents:
12499
diff
changeset

1131 
 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

1132 
 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

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

1134 

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

20854  1137 
fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base a) bs 
1138 
 add_term_names (Free(a,_), bs) = insert (op =) a bs 

0  1139 
 add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) 
1140 
 add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) 

1141 
 add_term_names (_, bs) = bs; 

1142 

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

23178  1144 
fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts 
0  1145 
 add_typ_tvars(TFree(_),vs) = vs 
16294  1146 
 add_typ_tvars(TVar(v),vs) = insert (op =) v vs; 
0  1147 

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

23178  1149 
fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts 
20854  1150 
 add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs 
0  1151 
 add_typ_tfree_names(TVar(_),fs) = fs; 
1152 

23178  1153 
fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts 
16294  1154 
 add_typ_tfrees(TFree(f),fs) = insert (op =) f fs 
0  1155 
 add_typ_tfrees(TVar(_),fs) = fs; 
1156 

23178  1157 
fun add_typ_varnames(Type(_,Ts),nms) = List.foldr add_typ_varnames nms Ts 
20854  1158 
 add_typ_varnames(TFree(nm,_),nms) = insert (op =) nm nms 
1159 
 add_typ_varnames(TVar((nm,_),_),nms) = insert (op =) nm nms; 

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

1160 

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

1163 

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

1165 
val add_term_tfrees = it_term_types add_typ_tfrees; 

1166 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

1167 

1168 
(*Nonlist versions*) 

1169 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

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

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

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

1173 

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

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

1175 

15570  1176 
fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts) 
20082
b0f5981b9267
removed obsolete ins_ix, mem_ix, ins_term, mem_term;
wenzelm
parents:
20001
diff
changeset

1177 
 add_typ_ixns(ixns,TVar(ixn,_)) = if member (op =) ixns ixn then ixns 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

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

1180 

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

1181 
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

1182 
 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

1183 
 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

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

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

1186 
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

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

1188 
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

1189 

16537  1190 

0  1191 
(** Frees and Vars **) 
1192 

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

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

16990  1195 
Var _ => OrdList.insert term_ord t vars 
0  1196 
 Abs (_,_,body) => add_term_vars(body,vars) 
1197 
 f$t => add_term_vars (f, add_term_vars(t, vars)) 

1198 
 _ => vars; 

1199 

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

1201 

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

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

16990  1204 
Free _ => OrdList.insert term_ord t frees 
0  1205 
 Abs (_,_,body) => add_term_frees(body,frees) 
1206 
 f$t => add_term_frees (f, add_term_frees(t, frees)) 

1207 
 _ => frees; 

1208 

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

1210 

20199  1211 

1212 
(* dest abstraction *) 

0  1213 

16678  1214 
fun dest_abs (x, T, body) = 
1215 
let 

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

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

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

1219 
 name_clash _ = false; 

1220 
in 

1221 
if name_clash body then 

20082
b0f5981b9267
removed obsolete ins_ix, mem_ix, ins_term, mem_term;
wenzelm
parents:
20001
diff
changeset

1222 
dest_abs (Name.variant [x] x, T, body) (*potentially slow, but rarely happens*) 
16678  1223 
else (x, subst_bound (Free (x, T), body)) 
1224 
end; 

1225 

20160  1226 

1227 
(* renaming variables *) 

0  1228 

24762  1229 
val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a  _ => I); 
1230 

20239  1231 
fun declare_term_names tm = 
1232 
fold_aterms 

1233 
(fn Const (a, _) => Name.declare (NameSpace.base a) 

1234 
 Free (a, _) => Name.declare a 

1235 
 _ => I) tm #> 

24762  1236 
fold_types declare_typ_names tm; 
20239  1237 

20160  1238 
fun variant_frees t frees = 
1239 
fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees; 

1240 

1241 
fun rename_wrt_term t frees = rev (variant_frees t frees); (*reversed result!*) 

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

1242 

1417  1243 

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

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

1245 

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

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

1247 

18253  1248 
fun dummy_pattern T = Const (dummy_patternN, T); 
1249 

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

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

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

1252 

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

1253 
fun no_dummy_patterns tm = 
16787  1254 
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

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

1256 

24733  1257 
fun free_dummy_patterns (Const ("dummy_pattern", T)) used = 
24850  1258 
let val [x] = Name.invents used Name.uu 1 
24733  1259 
in (Free (Name.internal x, T), Name.declare x used) end 
1260 
 free_dummy_patterns (Abs (x, T, b)) used = 

1261 
let val (b', used') = free_dummy_patterns b used 

1262 
in (Abs (x, T, b'), used') end 

1263 
 free_dummy_patterns (t $ u) used = 

1264 
let 

1265 
val (t', used') = free_dummy_patterns t used; 

1266 
val (u', used'') = free_dummy_patterns u used'; 

1267 
in (t' $ u', used'') end 

1268 
 free_dummy_patterns a used = (a, used); 

1269 

24762  1270 
fun replace_dummy Ts (Const ("dummy_pattern", T)) i = 
1271 
(list_comb (Var (("_dummy_", i), Ts > T), map Bound (0 upto length Ts  1)), i + 1) 

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

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

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

1275 
 replace_dummy Ts (t $ u) i = 

1276 
let 

1277 
val (t', i') = replace_dummy Ts t i; 

1278 
val (u', i'') = replace_dummy Ts u i'; 

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

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

11903  1281 

1282 
val replace_dummy_patterns = replace_dummy []; 

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

1283 

10552  1284 
fun is_replaced_dummy_pattern ("_dummy_", _) = true 
1285 
 is_replaced_dummy_pattern _ = false; 

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

1286 

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

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

1290 
 show_dummy_patterns a = a; 

1291 

13484  1292 

20100  1293 
(* display variables *) 
1294 

15986  1295 
val show_question_marks = ref true; 
15472  1296 

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

1297 
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

1298 
let 
15986  1299 
val question_mark = if ! show_question_marks then "?" else ""; 
1300 
val idx = string_of_int i; 

1301 
val dot = 

1302 
(case rev (Symbol.explode x) of 

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

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

1305 
 c :: _ => Symbol.is_digit c 

1306 
 _ => true); 

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

1307 
in 
15986  1308 
if dot then question_mark ^ x ^ "." ^ idx 
1309 
else if i <> 0 then question_mark ^ x ^ idx 

1310 
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

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

1312 

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

1313 
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

1314 
 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

1315 

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

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

1317 

4444  1318 
structure BasicTerm: BASIC_TERM = Term; 
1319 
open BasicTerm; 