author  wenzelm 
Tue, 13 Aug 2013 17:26:22 +0200  
changeset 53016  fa9c38891cf2 
parent 52920  4539e4a06339 
child 54732  b01bb3d09928 
permissions  rwrr 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1 
(* Title: Pure/term.ML 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

4 

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

29257
660234d959f7
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
wenzelm
parents:
29256
diff
changeset

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

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

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

12 

4444  13 
signature BASIC_TERM = 
14 
sig 

34922  15 
type indexname = string * int 
16 
type class = string 

17 
type sort = class list 

18 
type arity = string * sort list * sort 

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

21 
TFree of string * sort  

22 
TVar of indexname * sort 

16537  23 
datatype term = 
24 
Const of string * typ  

25 
Free of string * typ  

26 
Var of indexname * typ  

27 
Bound of int  

28 
Abs of string * typ * term  

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

21353  32 
val dummyS: sort 
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 
16710  45 
val dest_Const: term > string * typ 
46 
val dest_Free: term > string * typ 

47 
val dest_Var: term > indexname * typ 

35227  48 
val dest_comb: term > term * term 
4444  49 
val domain_type: typ > typ 
4480  50 
val range_type: typ > typ 
40840  51 
val dest_funT: typ > typ * typ 
4444  52 
val binder_types: typ > typ list 
53 
val body_type: typ > typ 

54 
val strip_type: typ > typ list * typ 

16710  55 
val type_of1: typ list * term > typ 
4444  56 
val type_of: term > typ 
16710  57 
val fastype_of1: typ list * term > typ 
4444  58 
val fastype_of: term > typ 
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 

29882
29154e67731d
New command find_consts searching for constants by type (by Timothy Bourke).
kleing
parents:
29286
diff
changeset

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

4444  71 
val map_type_tvar: (indexname * sort > typ) > typ > typ 
72 
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

73 
val map_types: (typ > typ) > term > term 
16943  74 
val fold_atyps: (typ > 'a > 'a) > typ > 'a > 'a 
35986  75 
val fold_atyps_sorts: (typ * sort > 'a > 'a) > typ > 'a > 'a 
16943  76 
val fold_aterms: (term > 'a > 'a) > term > 'a > 'a 
77 
val fold_term_types: (term > typ > 'a > 'a) > term > 'a > 'a 

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

24483  79 
val burrow_types: (typ list > typ list) > term list > term list 
16710  80 
val aconv: term * term > bool 
4444  81 
val propT: typ 
82 
val strip_all_body: term > term 

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

84 
val incr_bv: int * int * term > term 

85 
val incr_boundvars: int > term > term 

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

87 
val loose_bnos: term > int list 

88 
val loose_bvar: term * int > bool 

89 
val loose_bvar1: term * int > bool 

90 
val subst_bounds: term list * term > term 

91 
val subst_bound: term * term > term 

92 
val betapply: term * term > term 

18183  93 
val betapplys: term * term list > term 
4444  94 
val subst_free: (term * term) list > term > term 
95 
val abstract_over: term * term > term 

11922  96 
val lambda: term > term > term 
44241  97 
val absfree: string * typ > term > term 
98 
val absdummy: typ > term > term 

16710  99 
val subst_atomic: (term * term) list > term > term 
100 
val typ_subst_atomic: (typ * typ) list > typ > typ 

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

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

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

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

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

106 
val is_first_order: string list > term > bool 

4444  107 
val maxidx_of_typ: typ > int 
108 
val maxidx_of_typs: typ list > int 

109 
val maxidx_of_term: term > int 

19909  110 
val exists_subtype: (typ > bool) > typ > bool 
20531  111 
val exists_type: (typ > bool) > term > bool 
16943  112 
val exists_subterm: (term > bool) > term > bool 
16710  113 
val exists_Const: (string * typ > bool) > term > bool 
4444  114 
end; 
0  115 

4444  116 
signature TERM = 
117 
sig 

118 
include BASIC_TERM 

19394  119 
val aT: sort > typ 
120 
val itselfT: typ > typ 

121 
val a_itselfT: typ 

22908  122 
val argument_type_of: term > int > typ 
46219
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
46218
diff
changeset

123 
val abs: string * typ > term > term 
29257
660234d959f7
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
wenzelm
parents:
29256
diff
changeset

124 
val add_tvar_namesT: typ > indexname list > indexname list 
660234d959f7
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
wenzelm
parents:
29256
diff
changeset

125 
val add_tvar_names: term > indexname list > indexname list 
16943  126 
val add_tvarsT: typ > (indexname * sort) list > (indexname * sort) list 
127 
val add_tvars: term > (indexname * sort) list > (indexname * sort) list 

29257
660234d959f7
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
wenzelm
parents:
29256
diff
changeset

128 
val add_var_names: term > indexname list > indexname list 
16943  129 
val add_vars: term > (indexname * typ) list > (indexname * typ) list 
29257
660234d959f7
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
wenzelm
parents:
29256
diff
changeset

130 
val add_tfree_namesT: typ > string list > string list 
660234d959f7
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
wenzelm
parents:
29256
diff
changeset

131 
val add_tfree_names: term > string list > string list 
16943  132 
val add_tfreesT: typ > (string * sort) list > (string * sort) list 
133 
val add_tfrees: term > (string * sort) list > (string * sort) list 

29257
660234d959f7
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
wenzelm
parents:
29256
diff
changeset

134 
val add_free_names: term > string list > string list 
16943  135 
val add_frees: term > (string * typ) list > (string * typ) list 
29286  136 
val add_const_names: term > string list > string list 
137 
val add_consts: term > (string * typ) list > (string * typ) list 

25050  138 
val hidden_polymorphism: term > (indexname * sort) list 
29278  139 
val declare_typ_names: typ > Name.context > Name.context 
140 
val declare_term_names: term > Name.context > Name.context 

141 
val declare_term_frees: term > Name.context > Name.context 

142 
val variant_frees: term > (string * 'a) list > (string * 'a) list 

143 
val rename_wrt_term: term > (string * 'a) list > (string * 'a) list 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

144 
val eq_ix: indexname * indexname > bool 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

145 
val eq_tvar: (indexname * sort) * (indexname * sort) > bool 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

146 
val eq_var: (indexname * typ) * (indexname * typ) > bool 
33537
06c87d2c5b5a
locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm
parents:
33063
diff
changeset

147 
val aconv_untyped: term * term > bool 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

148 
val could_unify: term * term > bool 
20109  149 
val strip_abs_eta: int > term > (string * typ) list * term 
48263  150 
val match_bvars: (term * term) > (string * string) list > (string * string) list 
22031  151 
val map_abs_vars: (string > string) > term > term 
12981  152 
val rename_abs: term > term > term > term option 
42083
e1209fc7ecdc
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents:
40844
diff
changeset

153 
val is_open: term > bool 
e1209fc7ecdc
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents:
40844
diff
changeset

154 
val is_dependent: term > bool 
32198  155 
val lambda_name: string * term > term > term 
25050  156 
val close_schematic_term: term > term 
16710  157 
val maxidx_typ: typ > int > int 
158 
val maxidx_typs: typ list > int > int 

159 
val maxidx_term: term > int > int 

24671  160 
val has_abs: term > bool 
20239  161 
val dest_abs: string * typ * term > string * term 
18253  162 
val dummy_pattern: typ > term 
45156  163 
val dummy: term 
164 
val dummy_prop: term 

22723  165 
val is_dummy_pattern: term > bool 
24733  166 
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

167 
val no_dummy_patterns: term > term 
24762  168 
val replace_dummy_patterns: term > int > term * int 
10552  169 
val is_replaced_dummy_pattern: indexname > bool 
16035  170 
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

171 
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

172 
val string_of_vname': indexname > string 
4444  173 
end; 
174 

175 
structure Term: TERM = 

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

176 
struct 
0  177 

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

179 
for resolution.*) 

16537  180 
type indexname = string * int; 
0  181 

4626  182 
(* Types are classified by sorts. *) 
0  183 
type class = string; 
184 
type sort = class list; 

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

185 
type arity = string * sort list * sort; 
0  186 

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

188 
datatype typ = Type of string * typ list 

189 
 TFree of string * sort 

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

190 
 TVar of indexname * sort; 
0  191 

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

192 
(*Terms. Bound variables are indicated by depth number. 
0  193 
Free variables, (scheme) variables and constants have names. 
4626  194 
An term is "closed" if every bound variable of level "lev" 
13000  195 
is enclosed by at least "lev" abstractions. 
0  196 

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

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

199 

13000  200 
datatype term = 
0  201 
Const of string * typ 
13000  202 
 Free of string * typ 
0  203 
 Var of indexname * typ 
204 
 Bound of int 

205 
 Abs of string*typ*term 

3965  206 
 op $ of term*term; 
0  207 

16537  208 
(*Errors involving type mismatches*) 
0  209 
exception TYPE of string * typ list * term list; 
210 

16537  211 
(*Errors errors involving terms*) 
0  212 
exception TERM of string * term list; 
213 

214 
(*Note variable naming conventions! 

215 
a,b,c: string 

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

217 
i,j,m,n: int 

218 
t,u: term 

219 
v,w: indexnames 

220 
x,y: any 

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

222 
T,U: typ 

223 
*) 

224 

225 

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

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

227 

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

16537  230 
val dummyT = Type ("dummy", []); 
231 

232 
fun no_dummyT typ = 

233 
let 

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

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

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

237 
 check _ = (); 

238 
in check typ; typ end; 

239 

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

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

241 

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

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

244 

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

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

246 
 dest_Type T = raise TYPE ("dest_Type", [T], []); 
15914  247 
fun dest_TVar (TVar x) = x 
248 
 dest_TVar T = raise TYPE ("dest_TVar", [T], []); 

249 
fun dest_TFree (TFree x) = x 

250 
 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

251 

16537  252 

0  253 
(** Discriminators **) 
254 

7318  255 
fun is_Bound (Bound _) = true 
256 
 is_Bound _ = false; 

257 

0  258 
fun is_Const (Const _) = true 
259 
 is_Const _ = false; 

260 

261 
fun is_Free (Free _) = true 

262 
 is_Free _ = false; 

263 

264 
fun is_Var (Var _) = true 

265 
 is_Var _ = false; 

266 

267 
fun is_TVar (TVar _) = true 

268 
 is_TVar _ = false; 

269 

16537  270 

0  271 
(** Destructors **) 
272 

273 
fun dest_Const (Const x) = x 

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

275 

276 
fun dest_Free (Free x) = x 

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

278 

279 
fun dest_Var (Var x) = x 

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

281 

35227  282 
fun dest_comb (t1 $ t2) = (t1, t2) 
283 
 dest_comb t = raise TERM("dest_comb", [t]); 

284 

0  285 

40841  286 
fun domain_type (Type ("fun", [T, _])) = T; 
287 

288 
fun range_type (Type ("fun", [_, U])) = U; 

4064  289 

40840  290 
fun dest_funT (Type ("fun", [T, U])) = (T, U) 
291 
 dest_funT T = raise TYPE ("dest_funT", [T], []); 

292 

293 

0  294 
(* maps [T1,...,Tn]>T to the list [T1,T2,...,Tn]*) 
40841  295 
fun binder_types (Type ("fun", [T, U])) = T :: binder_types U 
296 
 binder_types _ = []; 

0  297 

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

40841  299 
fun body_type (Type ("fun", [_, U])) = body_type U 
300 
 body_type T = T; 

0  301 

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

40841  303 
fun strip_type T = (binder_types T, body_type T); 
0  304 

305 

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

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

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

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

30146  310 
 type_of1 (Ts, Bound i) = (nth Ts i 
43278  311 
handle General.Subscript => raise TYPE("type_of: bound variable", [], [Bound i])) 
0  312 
 type_of1 (Ts, Var (_,T)) = T 
313 
 type_of1 (Ts, Abs (_,T,body)) = T > type_of1(T::Ts, body) 

13000  314 
 type_of1 (Ts, f$u) = 
0  315 
let val U = type_of1(Ts,u) 
316 
and T = type_of1(Ts,f) 

317 
in case T of 

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

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

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

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

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

323 
[T,U], [f$u]) 
0  324 
end; 
325 

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

327 

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

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

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

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

30146  335 
 fastype_of1 (Ts, Bound i) = (nth Ts i 
43278  336 
handle General.Subscript => raise TERM("fastype_of: Bound", [Bound i])) 
13000  337 
 fastype_of1 (_, Var (_,T)) = T 
61  338 
 fastype_of1 (Ts, Abs (_,T,u)) = T > fastype_of1 (T::Ts, u); 
339 

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

0  341 

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

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

347 

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

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

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

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

22908  352 
in arg k [] tm end; 
16678  353 

0  354 

46219
426ed18eba43
discontinued oldstyle Term.list_abs in favour of plain Term.abs;
wenzelm
parents:
46218
diff
changeset

355 
fun abs (x, T) t = Abs (x, T, t); 
10806  356 

18927  357 
fun strip_abs (Abs (a, T, t)) = 
358 
let val (a', t') = strip_abs t 

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

360 
 strip_abs t = ([], t); 

361 

0  362 
(* maps (x1,...,xn)t to t *) 
13000  363 
fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t 
0  364 
 strip_abs_body u = u; 
365 

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

13000  367 
fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t 
0  368 
 strip_abs_vars u = [] : (string*typ) list; 
369 

370 

371 
fun strip_qnt_body qnt = 

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

373 
 strip t = t 

374 
in strip end; 

375 

376 
fun strip_qnt_vars qnt = 

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

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

379 
in strip end; 

380 

381 

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

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

385 

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

13000  387 
fun strip_comb u : term * term list = 
0  388 
let fun stripc (f$t, ts) = stripc (f, t::ts) 
13000  389 
 stripc x = x 
0  390 
in stripc(u,[]) end; 
391 

392 

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

394 
fun head_of (f$t) = head_of f 

395 
 head_of u = u; 

396 

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

399 
let 

30144
56ae4893e8ae
tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;
wenzelm
parents:
29882
diff
changeset

400 
fun add_size (t $ u) n = add_size t (add_size u n) 
56ae4893e8ae
tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;
wenzelm
parents:
29882
diff
changeset

401 
 add_size (Abs (_ ,_, t)) n = add_size t (n + 1) 
56ae4893e8ae
tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;
wenzelm
parents:
29882
diff
changeset

402 
 add_size _ n = n + 1; 
56ae4893e8ae
tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;
wenzelm
parents:
29882
diff
changeset

403 
in add_size tm 0 end; 
0  404 

30144
56ae4893e8ae
tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;
wenzelm
parents:
29882
diff
changeset

405 
(*number of atoms and constructors in a type*) 
29882
29154e67731d
New command find_consts searching for constants by type (by Timothy Bourke).
kleing
parents:
29286
diff
changeset

406 
fun size_of_typ ty = 
29154e67731d
New command find_consts searching for constants by type (by Timothy Bourke).
kleing
parents:
29286
diff
changeset

407 
let 
30144
56ae4893e8ae
tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;
wenzelm
parents:
29882
diff
changeset

408 
fun add_size (Type (_, tys)) n = fold add_size tys (n + 1) 
56ae4893e8ae
tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;
wenzelm
parents:
29882
diff
changeset

409 
 add_size _ n = n + 1; 
56ae4893e8ae
tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;
wenzelm
parents:
29882
diff
changeset

410 
in add_size ty 0 end; 
29882
29154e67731d
New command find_consts searching for constants by type (by Timothy Bourke).
kleing
parents:
29286
diff
changeset

411 

18847  412 
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

413 
 map_atyps f T = f T; 
18847  414 

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

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

417 
 map_aterms f t = f t; 

418 

18981  419 
fun map_type_tvar f = map_atyps (fn TVar x => f x  T => T); 
420 
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

421 

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

422 
fun map_types f = 
16678  423 
let 
424 
fun map_aux (Const (a, T)) = Const (a, f T) 

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

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

39293  427 
 map_aux (Bound i) = Bound i 
16678  428 
 map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t) 
429 
 map_aux (t $ u) = map_aux t $ map_aux u; 

430 
in map_aux end; 

0  431 

432 

16943  433 
(* fold types and terms *) 
434 

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

436 
 fold_atyps f T = f T; 

437 

35986  438 
fun fold_atyps_sorts f = 
439 
fold_atyps (fn T as TFree (_, S) => f (T, S)  T as TVar (_, S) => f (T, S)); 

440 

16943  441 
fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u 
442 
 fold_aterms f (Abs (_, _, t)) = fold_aterms f t 

443 
 fold_aterms f a = f a; 

444 

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

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

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

448 
 fold_term_types f (Bound _) = I 

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

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

451 

452 
fun fold_types f = fold_term_types (K f); 

453 

24483  454 
fun replace_types (Const (c, _)) (T :: Ts) = (Const (c, T), Ts) 
455 
 replace_types (Free (x, _)) (T :: Ts) = (Free (x, T), Ts) 

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

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

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

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

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

461 
 replace_types (t $ u) Ts = 

462 
let 

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

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

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

466 

467 
fun burrow_types f ts = 

468 
let 

49674
dbadb4d03cbc
report sort assignment of visible type variables;
wenzelm
parents:
48263
diff
changeset

469 
val Ts = rev ((fold o fold_types) cons ts []); 
24483  470 
val Ts' = f Ts; 
471 
val (ts', []) = fold_map replace_types ts Ts'; 

472 
in ts' end; 

473 

16943  474 
(*collect variables*) 
29257
660234d959f7
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
wenzelm
parents:
29256
diff
changeset

475 
val add_tvar_namesT = fold_atyps (fn TVar (xi, _) => insert (op =) xi  _ => I); 
660234d959f7
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
wenzelm
parents:
29256
diff
changeset

476 
val add_tvar_names = fold_types add_tvar_namesT; 
16943  477 
val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v  _ => I); 
478 
val add_tvars = fold_types add_tvarsT; 

29257
660234d959f7
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
wenzelm
parents:
29256
diff
changeset

479 
val add_var_names = fold_aterms (fn Var (xi, _) => insert (op =) xi  _ => I); 
16943  480 
val add_vars = fold_aterms (fn Var v => insert (op =) v  _ => I); 
33697  481 
val add_tfree_namesT = fold_atyps (fn TFree (a, _) => insert (op =) a  _ => I); 
29257
660234d959f7
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
wenzelm
parents:
29256
diff
changeset

482 
val add_tfree_names = fold_types add_tfree_namesT; 
16943  483 
val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v  _ => I); 
484 
val add_tfrees = fold_types add_tfreesT; 

29257
660234d959f7
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
wenzelm
parents:
29256
diff
changeset

485 
val add_free_names = fold_aterms (fn Free (x, _) => insert (op =) x  _ => I); 
16943  486 
val add_frees = fold_aterms (fn Free v => insert (op =) v  _ => I); 
29286  487 
val add_const_names = fold_aterms (fn Const (c, _) => insert (op =) c  _ => I); 
488 
val add_consts = fold_aterms (fn Const c => insert (op =) c  _ => I); 

16943  489 

25050  490 
(*extra type variables in a term, not covered by its type*) 
491 
fun hidden_polymorphism t = 

21682  492 
let 
25050  493 
val T = fastype_of t; 
21682  494 
val tvarsT = add_tvarsT T []; 
495 
val extra_tvars = fold_types (fold_atyps 

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

497 
in extra_tvars end; 

498 

16943  499 

29278  500 
(* renaming variables *) 
501 

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

503 

504 
fun declare_term_names tm = 

505 
fold_aterms 

30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30285
diff
changeset

506 
(fn Const (a, _) => Name.declare (Long_Name.base_name a) 
29278  507 
 Free (a, _) => Name.declare a 
508 
 _ => I) tm #> 

509 
fold_types declare_typ_names tm; 

510 

511 
val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x  _ => I); 

512 

513 
fun variant_frees t frees = 

43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
43324
diff
changeset

514 
fst (fold_map Name.variant (map fst frees) (declare_term_names t Name.context)) ~~ 
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
43324
diff
changeset

515 
map snd frees; 
29278  516 

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

518 

519 

25050  520 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

521 
(** Comparing terms **) 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

522 

5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

523 
(* variables *) 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

524 

5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

525 
fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y; 
16537  526 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

527 
fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S'; 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

528 
fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T'; 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

529 

5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

530 

5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

531 
(* alpha equivalence *) 
20511  532 

533 
fun tm1 aconv tm2 = 

534 
pointer_eq (tm1, tm2) orelse 

535 
(case (tm1, tm2) of 

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

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

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

539 

33537
06c87d2c5b5a
locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm
parents:
33063
diff
changeset

540 
fun aconv_untyped (tm1, tm2) = 
06c87d2c5b5a
locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm
parents:
33063
diff
changeset

541 
pointer_eq (tm1, tm2) orelse 
06c87d2c5b5a
locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm
parents:
33063
diff
changeset

542 
(case (tm1, tm2) of 
06c87d2c5b5a
locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm
parents:
33063
diff
changeset

543 
(t1 $ u1, t2 $ u2) => aconv_untyped (t1, t2) andalso aconv_untyped (u1, u2) 
06c87d2c5b5a
locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm
parents:
33063
diff
changeset

544 
 (Abs (_, _, t1), Abs (_, _, t2)) => aconv_untyped (t1, t2) 
06c87d2c5b5a
locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm
parents:
33063
diff
changeset

545 
 (Const (a, _), Const (b, _)) => a = b 
06c87d2c5b5a
locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm
parents:
33063
diff
changeset

546 
 (Free (x, _), Free (y, _)) => x = y 
06c87d2c5b5a
locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm
parents:
33063
diff
changeset

547 
 (Var (xi, _), Var (yj, _)) => xi = yj 
06c87d2c5b5a
locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm
parents:
33063
diff
changeset

548 
 (Bound i, Bound j) => i = j 
06c87d2c5b5a
locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm
parents:
33063
diff
changeset

549 
 _ => false); 
06c87d2c5b5a
locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm
parents:
33063
diff
changeset

550 

20511  551 

29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

552 
(*A fast unification filter: true unless the two terms cannot be unified. 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

553 
Terms must be NORMAL. Treats all Vars as distinct. *) 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

554 
fun could_unify (t, u) = 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

555 
let 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

556 
fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

557 
 matchrands _ _ = true; 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

558 
in 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

559 
case (head_of t, head_of u) of 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

560 
(_, Var _) => true 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

561 
 (Var _, _) => true 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

562 
 (Const (a, _), Const (b, _)) => a = b andalso matchrands t u 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

563 
 (Free (a, _), Free (b, _)) => a = b andalso matchrands t u 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

564 
 (Bound i, Bound j) => i = j andalso matchrands t u 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

565 
 (Abs _, _) => true (*because of possible eta equality*) 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

566 
 (_, Abs _) => true 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

567 
 _ => false 
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
29265
diff
changeset

568 
end; 
16678  569 

16570  570 

16537  571 

0  572 
(** Connectives of higher order logic **) 
573 

24850  574 
fun aT S = TFree (Name.aT, S); 
19394  575 

375  576 
fun itselfT ty = Type ("itself", [ty]); 
24850  577 
val a_itselfT = itselfT (TFree (Name.aT, [])); 
375  578 

46217
7b19666f0e3d
renamed Term.all to Logic.all_const, in accordance to HOLogic.all_const;
wenzelm
parents:
46215
diff
changeset

579 
val propT : typ = Type ("prop",[]); 
0  580 

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

13000  582 
fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t 
0  583 
 strip_all_body t = t; 
584 

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

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

13000  587 
(a,T) :: strip_all_vars t 
0  588 
 strip_all_vars t = [] : (string*typ) list; 
589 

590 
(*increments a term's nonlocal bound variables 

591 
required when moving a term within abstractions 

592 
inc is increment for bound variables 

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

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

596 
Abs(a, T, incr_bv(inc,lev+1,body)) 
13000  597 
 incr_bv (inc, lev, f$t) = 
0  598 
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 
599 
 incr_bv (inc, lev, u) = u; 

600 

601 
fun incr_boundvars 0 t = t 

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

603 

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

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

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

608 
else (x,y)::al) 

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

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

611 

612 
(* strip abstractions created by parameters *) 

48263  613 
fun match_bvars (s,t) al = match_bvs(strip_abs_body s, strip_abs_body t, al); 
12981  614 

22031  615 
fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u 
616 
 map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t) 

617 
 map_abs_vars f t = t; 

618 

12981  619 
fun rename_abs pat obj t = 
620 
let 

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

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

18942  623 
Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b) 
12981  624 
 ren_abs (f $ t) = ren_abs f $ ren_abs t 
625 
 ren_abs t = t 

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

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

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

13000  630 
fun add_loose_bnos (Bound i, lev, js) = 
20854  631 
if i<lev then js else insert (op =) (i  lev) js 
0  632 
 add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js) 
633 
 add_loose_bnos (f$t, lev, js) = 

13000  634 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
0  635 
 add_loose_bnos (_, _, js) = js; 
636 

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

638 

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

640 
level k or beyond. *) 

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

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

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

644 
 loose_bvar _ = false; 

645 

2792  646 
fun loose_bvar1(Bound i,k) = i = k 
647 
 loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 

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

649 
 loose_bvar1 _ = false; 

0  650 

42083
e1209fc7ecdc
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents:
40844
diff
changeset

651 
fun is_open t = loose_bvar (t, 0); 
e1209fc7ecdc
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents:
40844
diff
changeset

652 
fun is_dependent t = loose_bvar1 (t, 0); 
e1209fc7ecdc
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents:
40844
diff
changeset

653 

0  654 
(*Substitute arguments for loose bound variables. 
655 
Betareduction of arg(n1)...arg0 into t replacing (Bound i) with (argi). 

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

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

660 
*) 

13000  661 
fun subst_bounds (args: term list, t) : term = 
19065  662 
let 
663 
val n = length args; 

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

32020  665 
(if i < lev then raise Same.SAME (*var is locally bound*) 
30146  666 
else incr_boundvars lev (nth args (i  lev)) 
43278  667 
handle General.Subscript => Bound (i  n)) (*loose: change it*) 
19065  668 
 subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1)) 
669 
 subst (f $ t, lev) = 

32020  670 
(subst (f, lev) $ (subst (t, lev) handle Same.SAME => t) 
671 
handle Same.SAME => f $ subst (t, lev)) 

672 
 subst _ = raise Same.SAME; 

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

0  674 

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

675 
(*Special case: one argument*) 
13000  676 
fun subst_bound (arg, t) : term = 
19065  677 
let 
678 
fun subst (Bound i, lev) = 

32020  679 
if i < lev then raise Same.SAME (*var is locally bound*) 
19065  680 
else if i = lev then incr_boundvars lev arg 
681 
else Bound (i  1) (*loose: change it*) 

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

683 
 subst (f $ t, lev) = 

32020  684 
(subst (f, lev) $ (subst (t, lev) handle Same.SAME => t) 
685 
handle Same.SAME => f $ subst (t, lev)) 

686 
 subst _ = raise Same.SAME; 

687 
in subst (t, 0) handle Same.SAME => t end; 

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

688 

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

690 
fun betapply (Abs(_,_,t), u) = subst_bound (u,t) 
0  691 
 betapply (f,u) = f$u; 
692 

18183  693 
val betapplys = Library.foldl betapply; 
694 

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

695 

20109  696 
(*unfolding abstractions with substitution 
697 
of bound variables and implicit etaexpansion*) 

698 
fun strip_abs_eta k t = 

699 
let 

29278  700 
val used = fold_aterms declare_term_frees t Name.context; 
20109  701 
fun strip_abs t (0, used) = (([], t), (0, used)) 
702 
 strip_abs (Abs (v, T, t)) (k, used) = 

703 
let 

43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
43324
diff
changeset

704 
val (v', used') = Name.variant v used; 
21013  705 
val t' = subst_bound (Free (v', T), t); 
20122  706 
val ((vs, t''), (k', used'')) = strip_abs t' (k  1, used'); 
707 
in (((v', T) :: vs, t''), (k', used'')) end 

20109  708 
 strip_abs t (k, used) = (([], t), (k, used)); 
709 
fun expand_eta [] t _ = ([], t) 

710 
 expand_eta (T::Ts) t used = 

711 
let 

43326
47cf4bc789aa
simplified Name.variant  discontinued builtin fold_map;
wenzelm
parents:
43324
diff
changeset

712 
val (v, used') = Name.variant "" used; 
20122  713 
val (vs, t') = expand_eta Ts (t $ Free (v, T)) used'; 
20109  714 
in ((v, T) :: vs, t') end; 
715 
val ((vs1, t'), (k', used')) = strip_abs t (k, used); 

40844  716 
val Ts = fst (chop k' (binder_types (fastype_of t'))); 
20109  717 
val (vs2, t'') = expand_eta Ts t' used'; 
718 
in (vs1 @ vs2, t'') end; 

719 

720 

0  721 
(*Substitute new for free occurrences of old in a term*) 
29256  722 
fun subst_free [] = I 
0  723 
 subst_free pairs = 
13000  724 
let fun substf u = 
17314  725 
case AList.lookup (op aconv) pairs u of 
15531  726 
SOME u' => u' 
727 
 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

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

729 
 _ => u) 
0  730 
in substf end; 
731 

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

16882  735 
fun abstract_over (v, body) = 
736 
let 

16990  737 
fun abs lev tm = 
738 
if v aconv tm then Bound lev 

16882  739 
else 
16990  740 
(case tm of 
741 
Abs (a, T, t) => Abs (a, T, abs (lev + 1) t) 

32020  742 
 t $ u => 
743 
(abs lev t $ (abs lev u handle Same.SAME => u) 

744 
handle Same.SAME => t $ abs lev u) 

745 
 _ => raise Same.SAME); 

746 
in abs 0 body handle Same.SAME => body end; 

0  747 

32198  748 
fun term_name (Const (x, _)) = Long_Name.base_name x 
749 
 term_name (Free (x, _)) = x 

750 
 term_name (Var ((x, _), _)) = x 

751 
 term_name _ = Name.uu; 

752 

753 
fun lambda_name (x, v) t = 

754 
Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t)); 

755 

756 
fun lambda v t = lambda_name ("", v) t; 

0  757 

44241  758 
fun absfree (a, T) body = Abs (a, T, abstract_over (Free (a, T), body)); 
759 
fun absdummy T body = Abs (Name.uu_, T, body); 

0  760 

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

765 
let 

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

767 
 subst (t $ u) = subst t $ subst u 

18942  768 
 subst t = the_default t (AList.lookup (op aconv) inst t); 
16678  769 
in subst tm end; 
0  770 

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

773 
 typ_subst_atomic inst ty = 

774 
let 

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

18942  776 
 subst T = the_default T (AList.lookup (op = : typ * typ > bool) inst T); 
16678  777 
in subst ty end; 
15797  778 

16678  779 
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

780 
 subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm; 
16678  781 

782 
fun typ_subst_TVars [] ty = ty 

783 
 typ_subst_TVars inst ty = 

784 
let 

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

18942  786 
 subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi) 
16678  787 
 subst T = T; 
788 
in subst ty end; 

0  789 

16678  790 
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

791 
 subst_TVars inst tm = map_types (typ_subst_TVars inst) tm; 
0  792 

16678  793 
fun subst_Vars [] tm = tm 
794 
 subst_Vars inst tm = 

795 
let 

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

799 
 subst t = t; 

800 
in subst tm end; 

0  801 

16678  802 
fun subst_vars ([], []) tm = tm 
803 
 subst_vars ([], inst) tm = subst_Vars inst tm 

804 
 subst_vars (instT, inst) tm = 

805 
let 

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

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

32784  808 
 subst (Var (xi, T)) = 
17271  809 
(case AList.lookup (op =) inst xi of 
16678  810 
NONE => Var (xi, typ_subst_TVars instT T) 
811 
 SOME t => t) 

812 
 subst (t as Bound _) = t 

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

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

815 
in subst tm end; 

0  816 

25050  817 
fun close_schematic_term t = 
818 
let 

819 
val extra_types = map (fn v => Const ("TYPE", itselfT (TVar v))) (hidden_polymorphism t); 

30285
a135bfab6e83
close_schematic_term: uniform order of types/terms;
wenzelm
parents:
30280
diff
changeset

820 
val extra_terms = map Var (add_vars t []); 
a135bfab6e83
close_schematic_term: uniform order of types/terms;
wenzelm
parents:
30280
diff
changeset

821 
in fold lambda (extra_terms @ extra_types) t end; 
25050  822 

823 

0  824 

15573  825 
(** Identifying firstorder terms **) 
826 

20199  827 
(*Differs from proofterm/is_fun in its treatment of TVar*) 
29256  828 
fun is_funtype (Type ("fun", [_, _])) = true 
20199  829 
 is_funtype _ = false; 
830 

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

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

16667  837 
fun is_first_order quants = 
16589  838 
let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body 
16667  839 
 first_order1 Ts (Const(q,_) $ Abs(a,T,body)) = 
20664  840 
member (op =) quants q andalso (*it is a known quantifier*) 
16589  841 
not (is_funtype T) andalso first_order1 (T::Ts) body 
16667  842 
 first_order1 Ts t = 
843 
case strip_comb t of 

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

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

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

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

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

849 
 _ => error "first_order: unexpected case" 

16589  850 
in first_order1 [] end; 
15573  851 

16710  852 

16990  853 
(* maximum index of typs and terms *) 
0  854 

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

857 
 maxidx_typ (TFree _) i = i 

858 
and maxidx_typs [] i = i 

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

0  860 

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

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

864 
 maxidx_term (Bound _) i = i 

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

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

0  867 

16710  868 
fun maxidx_of_typ T = maxidx_typ T ~1; 
869 
fun maxidx_of_typs Ts = maxidx_typs Ts ~1; 

870 
fun maxidx_of_term t = maxidx_term t ~1; 

13665  871 

0  872 

873 

29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset

874 
(** misc syntax operations **) 
0  875 

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

877 

19909  878 
fun exists_subtype P = 
879 
let 

880 
fun ex ty = P ty orelse 

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

882 
in ex end; 

13646  883 

20531  884 
fun exists_type P = 
885 
let 

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

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

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

889 
 ex (Bound _) = false 

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

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

892 
in ex end; 

893 

16943  894 
fun exists_subterm P = 
895 
let 

896 
fun ex tm = P tm orelse 

897 
(case tm of 

898 
t $ u => ex t orelse ex u 

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

900 
 _ => false); 

901 
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

902 

29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset

903 
fun exists_Const P = exists_subterm (fn Const c => P c  _ => false); 
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset

904 

24671  905 
fun has_abs (Abs _) = true 
906 
 has_abs (t $ u) = has_abs t orelse has_abs u 

907 
 has_abs _ = false; 

908 

909 

20199  910 
(* dest abstraction *) 
0  911 

16678  912 
fun dest_abs (x, T, body) = 
913 
let 

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

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

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

917 
 name_clash _ = false; 

918 
in 

43324
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
43278
diff
changeset

919 
if name_clash body then 
2b47822868e4
discontinued Name.variant to emphasize that this is oldstyle / indirect;
wenzelm
parents:
43278
diff
changeset

920 
dest_abs (singleton (Name.variant_list [x]) x, T, body) (*potentially slow*) 
16678  921 
else (x, subst_bound (Free (x, T), body)) 
922 
end; 

923 

20160  924 

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

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

926 

52161  927 
fun dummy_pattern T = Const ("dummy_pattern", T); 
45156  928 
val dummy = dummy_pattern dummyT; 
929 
val dummy_prop = dummy_pattern propT; 

18253  930 

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

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

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

933 

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

934 
fun no_dummy_patterns tm = 
16787  935 
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

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

937 

24733  938 
fun free_dummy_patterns (Const ("dummy_pattern", T)) used = 
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset

939 
let val [x] = Name.invent used Name.uu 1 
24733  940 
in (Free (Name.internal x, T), Name.declare x used) end 
941 
 free_dummy_patterns (Abs (x, T, b)) used = 

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

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

944 
 free_dummy_patterns (t $ u) used = 

945 
let 

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

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

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

949 
 free_dummy_patterns a used = (a, used); 

950 

24762  951 
fun replace_dummy Ts (Const ("dummy_pattern", T)) i = 
33063  952 
(list_comb (Var (("_dummy_", i), Ts > T), map_range Bound (length Ts)), i + 1) 
24762  953 
 replace_dummy Ts (Abs (x, T, t)) i = 
954 
let val (t', i') = replace_dummy (T :: Ts) t i 

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

956 
 replace_dummy Ts (t $ u) i = 

957 
let 

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

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

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

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

11903  962 

963 
val replace_dummy_patterns = replace_dummy []; 

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

964 

10552  965 
fun is_replaced_dummy_pattern ("_dummy_", _) = true 
966 
 is_replaced_dummy_pattern _ = false; 

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

967 

45156  968 
fun show_dummy_patterns (Var (("_dummy_", _), T)) = dummy_pattern T 
16035  969 
 show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u 
970 
 show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t) 

971 
 show_dummy_patterns a = a; 

972 

13484  973 

20100  974 
(* display variables *) 
975 

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

976 
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

977 
let 
15986  978 
val idx = string_of_int i; 
979 
val dot = 

980 
(case rev (Symbol.explode x) of 

50242
56b9c792a98b
support for substructured identifier syntax (inactive);
wenzelm
parents:
49674
diff
changeset

981 
_ :: "\\<^sub>" :: _ => false 
53016
fa9c38891cf2
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fallback;
wenzelm
parents:
52920
diff
changeset

982 
 _ :: "\\<^isub>" :: _ => false (*legacy*) 
fa9c38891cf2
disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fallback;
wenzelm
parents:
52920
diff
changeset

983 
 _ :: "\\<^isup>" :: _ => false (*legacy*) 
15986  984 
 c :: _ => Symbol.is_digit c 
985 
 _ => true); 

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

986 
in 
38980
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
35986
diff
changeset

987 
if dot then "?" ^ x ^ "." ^ idx 
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
35986
diff
changeset

988 
else if i <> 0 then "?" ^ x ^ idx 
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
35986
diff
changeset

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

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

991 

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

992 
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

993 
 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

994 

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

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

996 

40841  997 
structure Basic_Term: BASIC_TERM = Term; 
998 
open Basic_Term; 