author  wenzelm 
Thu, 02 Sep 2010 00:48:07 +0200  
changeset 38980  af73cf0dc31f 
parent 35986  b7fcca3d9a44 
child 39293  651e5a3e8cfd 
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 
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 

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 
4444  97 
val absfree: string * typ * term > term 
17786  98 
val absdummy: typ * term > term 
4444  99 
val list_abs_free: (string * typ) list * term > term 
100 
val list_all_free: (string * typ) list * term > term 

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

16710  102 
val subst_atomic: (term * term) list > term > term 
103 
val typ_subst_atomic: (typ * typ) list > typ > typ 

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

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

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

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

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

109 
val is_first_order: string list > term > bool 

4444  110 
val maxidx_of_typ: typ > int 
111 
val maxidx_of_typs: typ list > int 

112 
val maxidx_of_term: term > int 

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

4444  119 
signature TERM = 
120 
sig 

121 
include BASIC_TERM 

19394  122 
val aT: sort > typ 
123 
val itselfT: typ > typ 

124 
val a_itselfT: typ 

27335  125 
val all: typ > term 
22908  126 
val argument_type_of: term > int > typ 
29257
660234d959f7
provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
wenzelm
parents:
29256
diff
changeset

127 
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

128 
val add_tvar_names: term > indexname list > indexname list 
16943  129 
val add_tvarsT: typ > (indexname * sort) list > (indexname * sort) list 
130 
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

131 
val add_var_names: term > indexname list > indexname list 
16943  132 
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

133 
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

134 
val add_tfree_names: term > string list > string list 
16943  135 
val add_tfreesT: typ > (string * sort) list > (string * sort) list 
136 
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

137 
val add_free_names: term > string list > string list 
16943  138 
val add_frees: term > (string * typ) list > (string * typ) list 
29286  139 
val add_const_names: term > string list > string list 
140 
val add_consts: term > (string * typ) list > (string * typ) list 

25050  141 
val hidden_polymorphism: term > (indexname * sort) list 
29278  142 
val declare_typ_names: typ > Name.context > Name.context 
143 
val declare_term_names: term > Name.context > Name.context 

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

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

146 
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

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

148 
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

149 
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

150 
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

151 
val could_unify: term * term > bool 
20109  152 
val strip_abs_eta: int > term > (string * typ) list * term 
12981  153 
val match_bvars: (term * term) * (string * string) list > (string * string) list 
22031  154 
val map_abs_vars: (string > string) > term > term 
12981  155 
val rename_abs: term > term > term > term option 
32198  156 
val lambda_name: string * term > term > term 
25050  157 
val close_schematic_term: term > term 
16710  158 
val maxidx_typ: typ > int > int 
159 
val maxidx_typs: typ list > int > int 

160 
val maxidx_term: term > int > int 

24671  161 
val has_abs: term > bool 
20239  162 
val dest_abs: string * typ * term > string * term 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

163 
val dummy_patternN: string 
18253  164 
val dummy_pattern: typ > 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 

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

4064  288 

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

291 
 binder_types _ = []; 

292 

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

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

295 
 body_type T = T; 

296 

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

298 
fun strip_type T : typ list * typ = 

299 
(binder_types T, body_type T); 

300 

301 

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

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

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

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

30146  306 
 type_of1 (Ts, Bound i) = (nth Ts i 
15570  307 
handle Subscript => raise TYPE("type_of: bound variable", [], [Bound i])) 
0  308 
 type_of1 (Ts, Var (_,T)) = T 
309 
 type_of1 (Ts, Abs (_,T,body)) = T > type_of1(T::Ts, body) 

13000  310 
 type_of1 (Ts, f$u) = 
0  311 
let val U = type_of1(Ts,u) 
312 
and T = type_of1(Ts,f) 

313 
in case T of 

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

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

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

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

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

319 
[T,U], [f$u]) 
0  320 
end; 
321 

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

323 

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

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

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

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

30146  331 
 fastype_of1 (Ts, Bound i) = (nth Ts i 
15570  332 
handle Subscript => raise TERM("fastype_of: Bound", [Bound i])) 
13000  333 
 fastype_of1 (_, Var (_,T)) = T 
61  334 
 fastype_of1 (Ts, Abs (_,T,u)) = T > fastype_of1 (T::Ts, u); 
335 

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

0  337 

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

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

343 

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

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

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

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

22908  348 
in arg k [] tm end; 
16678  349 

0  350 

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

18927  353 
fun strip_abs (Abs (a, T, t)) = 
354 
let val (a', t') = strip_abs t 

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

356 
 strip_abs t = ([], t); 

357 

0  358 
(* maps (x1,...,xn)t to t *) 
13000  359 
fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t 
0  360 
 strip_abs_body u = u; 
361 

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

13000  363 
fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t 
0  364 
 strip_abs_vars u = [] : (string*typ) list; 
365 

366 

367 
fun strip_qnt_body qnt = 

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

369 
 strip t = t 

370 
in strip end; 

371 

372 
fun strip_qnt_vars qnt = 

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

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

375 
in strip end; 

376 

377 

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

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

381 

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

13000  383 
fun strip_comb u : term * term list = 
0  384 
let fun stripc (f$t, ts) = stripc (f, t::ts) 
13000  385 
 stripc x = x 
0  386 
in stripc(u,[]) end; 
387 

388 

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

390 
fun head_of (f$t) = head_of f 

391 
 head_of u = u; 

392 

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

395 
let 

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

396 
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

397 
 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

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

399 
in add_size tm 0 end; 
0  400 

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

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

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

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

404 
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

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

406 
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

407 

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

409 
 map_atyps f T = f T; 
18847  410 

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

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

413 
 map_aterms f t = f t; 

414 

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

417 

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

418 
fun map_types f = 
16678  419 
let 
420 
fun map_aux (Const (a, T)) = Const (a, f T) 

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

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

423 
 map_aux (t as Bound _) = t 

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

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

426 
in map_aux end; 

0  427 

428 

16943  429 
(* fold types and terms *) 
430 

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

432 
 fold_atyps f T = f T; 

433 

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

436 

16943  437 
fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u 
438 
 fold_aterms f (Abs (_, _, t)) = fold_aterms f t 

439 
 fold_aterms f a = f a; 

440 

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

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

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

444 
 fold_term_types f (Bound _) = I 

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

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

447 

448 
fun fold_types f = fold_term_types (K f); 

449 

24483  450 
fun replace_types (Const (c, _)) (T :: Ts) = (Const (c, T), Ts) 
451 
 replace_types (Free (x, _)) (T :: Ts) = (Free (x, T), Ts) 

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

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

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

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

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

457 
 replace_types (t $ u) Ts = 

458 
let 

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

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

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

462 

463 
fun burrow_types f ts = 

464 
let 

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

466 
val Ts' = f Ts; 

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

468 
in ts' end; 

469 

16943  470 
(*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

471 
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

472 
val add_tvar_names = fold_types add_tvar_namesT; 
16943  473 
val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v  _ => I); 
474 
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

475 
val add_var_names = fold_aterms (fn Var (xi, _) => insert (op =) xi  _ => I); 
16943  476 
val add_vars = fold_aterms (fn Var v => insert (op =) v  _ => I); 
33697  477 
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

478 
val add_tfree_names = fold_types add_tfree_namesT; 
16943  479 
val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v  _ => I); 
480 
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

481 
val add_free_names = fold_aterms (fn Free (x, _) => insert (op =) x  _ => I); 
16943  482 
val add_frees = fold_aterms (fn Free v => insert (op =) v  _ => I); 
29286  483 
val add_const_names = fold_aterms (fn Const (c, _) => insert (op =) c  _ => I); 
484 
val add_consts = fold_aterms (fn Const c => insert (op =) c  _ => I); 

16943  485 

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

21682  488 
let 
25050  489 
val T = fastype_of t; 
21682  490 
val tvarsT = add_tvarsT T []; 
491 
val extra_tvars = fold_types (fold_atyps 

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

493 
in extra_tvars end; 

494 

16943  495 

29278  496 
(* renaming variables *) 
497 

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

499 

500 
fun declare_term_names tm = 

501 
fold_aterms 

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

502 
(fn Const (a, _) => Name.declare (Long_Name.base_name a) 
29278  503 
 Free (a, _) => Name.declare a 
504 
 _ => I) tm #> 

505 
fold_types declare_typ_names tm; 

506 

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

508 

509 
fun variant_frees t frees = 

510 
fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees; 

511 

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

513 

514 

25050  515 

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

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

517 

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

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

519 

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

520 
fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y; 
16537  521 

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

522 
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

523 
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

524 

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

525 

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

526 
(* alpha equivalence *) 
20511  527 

528 
fun tm1 aconv tm2 = 

529 
pointer_eq (tm1, tm2) orelse 

530 
(case (tm1, tm2) of 

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

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

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

534 

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

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

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

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

538 
(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

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

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

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

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

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

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

545 

20511  546 

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

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

548 
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

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

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

551 
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

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

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

554 
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

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

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

557 
 (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

558 
 (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

559 
 (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

560 
 (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

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

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

563 
end; 
16678  564 

16570  565 

16537  566 

0  567 
(** Connectives of higher order logic **) 
568 

24850  569 
fun aT S = TFree (Name.aT, S); 
19394  570 

375  571 
fun itselfT ty = Type ("itself", [ty]); 
24850  572 
val a_itselfT = itselfT (TFree (Name.aT, [])); 
375  573 

0  574 
val propT : typ = Type("prop",[]); 
575 

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

577 

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

13000  579 
fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t 
0  580 
 strip_all_body t = t; 
581 

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

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

13000  584 
(a,T) :: strip_all_vars t 
0  585 
 strip_all_vars t = [] : (string*typ) list; 
586 

587 
(*increments a term's nonlocal bound variables 

588 
required when moving a term within abstractions 

589 
inc is increment for bound variables 

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

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

593 
Abs(a, T, incr_bv(inc,lev+1,body)) 
13000  594 
 incr_bv (inc, lev, f$t) = 
0  595 
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 
596 
 incr_bv (inc, lev, u) = u; 

597 

598 
fun incr_boundvars 0 t = t 

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

600 

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

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

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

605 
else (x,y)::al) 

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

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

608 

609 
(* strip abstractions created by parameters *) 

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

611 

22031  612 
fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u 
613 
 map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t) 

614 
 map_abs_vars f t = t; 

615 

12981  616 
fun rename_abs pat obj t = 
617 
let 

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

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

18942  620 
Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b) 
12981  621 
 ren_abs (f $ t) = ren_abs f $ ren_abs t 
622 
 ren_abs t = t 

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

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

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

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

13000  631 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
0  632 
 add_loose_bnos (_, _, js) = js; 
633 

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

635 

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

637 
level k or beyond. *) 

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

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

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

641 
 loose_bvar _ = false; 

642 

2792  643 
fun loose_bvar1(Bound i,k) = i = k 
644 
 loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 

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

646 
 loose_bvar1 _ = false; 

0  647 

648 
(*Substitute arguments for loose bound variables. 

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

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

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

654 
*) 

13000  655 
fun subst_bounds (args: term list, t) : term = 
19065  656 
let 
657 
val n = length args; 

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

32020  659 
(if i < lev then raise Same.SAME (*var is locally bound*) 
30146  660 
else incr_boundvars lev (nth args (i  lev)) 
19065  661 
handle Subscript => Bound (i  n)) (*loose: change it*) 
662 
 subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1)) 

663 
 subst (f $ t, lev) = 

32020  664 
(subst (f, lev) $ (subst (t, lev) handle Same.SAME => t) 
665 
handle Same.SAME => f $ subst (t, lev)) 

666 
 subst _ = raise Same.SAME; 

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

0  668 

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

669 
(*Special case: one argument*) 
13000  670 
fun subst_bound (arg, t) : term = 
19065  671 
let 
672 
fun subst (Bound i, lev) = 

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

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

677 
 subst (f $ t, lev) = 

32020  678 
(subst (f, lev) $ (subst (t, lev) handle Same.SAME => t) 
679 
handle Same.SAME => f $ subst (t, lev)) 

680 
 subst _ = raise Same.SAME; 

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

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

682 

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

684 
fun betapply (Abs(_,_,t), u) = subst_bound (u,t) 
0  685 
 betapply (f,u) = f$u; 
686 

18183  687 
val betapplys = Library.foldl betapply; 
688 

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

689 

20109  690 
(*unfolding abstractions with substitution 
691 
of bound variables and implicit etaexpansion*) 

692 
fun strip_abs_eta k t = 

693 
let 

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

697 
let 

20122  698 
val ([v'], used') = Name.variants [v] used; 
21013  699 
val t' = subst_bound (Free (v', T), t); 
20122  700 
val ((vs, t''), (k', used'')) = strip_abs t' (k  1, used'); 
701 
in (((v', T) :: vs, t''), (k', used'')) end 

20109  702 
 strip_abs t (k, used) = (([], t), (k, used)); 
703 
fun expand_eta [] t _ = ([], t) 

704 
 expand_eta (T::Ts) t used = 

705 
let 

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

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

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

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

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

713 

714 

0  715 
(*Substitute new for free occurrences of old in a term*) 
29256  716 
fun subst_free [] = I 
0  717 
 subst_free pairs = 
13000  718 
let fun substf u = 
17314  719 
case AList.lookup (op aconv) pairs u of 
15531  720 
SOME u' => u' 
721 
 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

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

723 
 _ => u) 
0  724 
in substf end; 
725 

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

16882  729 
fun abstract_over (v, body) = 
730 
let 

16990  731 
fun abs lev tm = 
732 
if v aconv tm then Bound lev 

16882  733 
else 
16990  734 
(case tm of 
735 
Abs (a, T, t) => Abs (a, T, abs (lev + 1) t) 

32020  736 
 t $ u => 
737 
(abs lev t $ (abs lev u handle Same.SAME => u) 

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

739 
 _ => raise Same.SAME); 

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

0  741 

32198  742 
fun term_name (Const (x, _)) = Long_Name.base_name x 
743 
 term_name (Free (x, _)) = x 

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

745 
 term_name _ = Name.uu; 

746 

747 
fun lambda_name (x, v) t = 

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

749 

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

0  751 

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

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

753 
fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body)); 
24850  754 
fun absdummy (T, body) = Abs (Name.internal Name.uu, T, body); 
0  755 

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

757 
fun list_abs_free ([ ] , t) = t 

13000  758 
 list_abs_free ((a,T)::vars, t) = 
0  759 
absfree(a, T, list_abs_free(vars,t)); 
760 

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

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

13000  763 
 list_all_free ((a,T)::vars, t) = 
0  764 
(all T) $ (absfree(a, T, list_all_free(vars,t))); 
765 

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

767 
fun list_all ([], t) = t 

13000  768 
 list_all ((a,T)::vars, t) = 
0  769 
(all T) $ (Abs(a, T, list_all(vars,t))); 
770 

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

775 
let 

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

777 
 subst (t $ u) = subst t $ subst u 

18942  778 
 subst t = the_default t (AList.lookup (op aconv) inst t); 
16678  779 
in subst tm end; 
0  780 

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

783 
 typ_subst_atomic inst ty = 

784 
let 

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

18942  786 
 subst T = the_default T (AList.lookup (op = : typ * typ > bool) inst T); 
16678  787 
in subst ty end; 
15797  788 

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

790 
 subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm; 
16678  791 

792 
fun typ_subst_TVars [] ty = ty 

793 
 typ_subst_TVars inst ty = 

794 
let 

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

18942  796 
 subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi) 
16678  797 
 subst T = T; 
798 
in subst ty end; 

0  799 

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

801 
 subst_TVars inst tm = map_types (typ_subst_TVars inst) tm; 
0  802 

16678  803 
fun subst_Vars [] tm = tm 
804 
 subst_Vars inst tm = 

805 
let 

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

809 
 subst t = t; 

810 
in subst tm end; 

0  811 

16678  812 
fun subst_vars ([], []) tm = tm 
813 
 subst_vars ([], inst) tm = subst_Vars inst tm 

814 
 subst_vars (instT, inst) tm = 

815 
let 

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

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

32784  818 
 subst (Var (xi, T)) = 
17271  819 
(case AList.lookup (op =) inst xi of 
16678  820 
NONE => Var (xi, typ_subst_TVars instT T) 
821 
 SOME t => t) 

822 
 subst (t as Bound _) = t 

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

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

825 
in subst tm end; 

0  826 

25050  827 
fun close_schematic_term t = 
828 
let 

829 
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

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

831 
in fold lambda (extra_terms @ extra_types) t end; 
25050  832 

833 

0  834 

15573  835 
(** Identifying firstorder terms **) 
836 

20199  837 
(*Differs from proofterm/is_fun in its treatment of TVar*) 
29256  838 
fun is_funtype (Type ("fun", [_, _])) = true 
20199  839 
 is_funtype _ = false; 
840 

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

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

16667  847 
fun is_first_order quants = 
16589  848 
let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body 
16667  849 
 first_order1 Ts (Const(q,_) $ Abs(a,T,body)) = 
20664  850 
member (op =) quants q andalso (*it is a known quantifier*) 
16589  851 
not (is_funtype T) andalso first_order1 (T::Ts) body 
16667  852 
 first_order1 Ts t = 
853 
case strip_comb t of 

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

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

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

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

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

859 
 _ => error "first_order: unexpected case" 

16589  860 
in first_order1 [] end; 
15573  861 

16710  862 

16990  863 
(* maximum index of typs and terms *) 
0  864 

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

867 
 maxidx_typ (TFree _) i = i 

868 
and maxidx_typs [] i = i 

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

0  870 

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

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

874 
 maxidx_term (Bound _) i = i 

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

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

0  877 

16710  878 
fun maxidx_of_typ T = maxidx_typ T ~1; 
879 
fun maxidx_of_typs Ts = maxidx_typs Ts ~1; 

880 
fun maxidx_of_term t = maxidx_term t ~1; 

13665  881 

0  882 

883 

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

884 
(** misc syntax operations **) 
0  885 

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

887 

19909  888 
fun exists_subtype P = 
889 
let 

890 
fun ex ty = P ty orelse 

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

892 
in ex end; 

13646  893 

20531  894 
fun exists_type P = 
895 
let 

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

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

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

899 
 ex (Bound _) = false 

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

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

902 
in ex end; 

903 

16943  904 
fun exists_subterm P = 
905 
let 

906 
fun ex tm = P tm orelse 

907 
(case tm of 

908 
t $ u => ex t orelse ex u 

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

910 
 _ => false); 

911 
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

912 

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

913 
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

914 

24671  915 
fun has_abs (Abs _) = true 
916 
 has_abs (t $ u) = has_abs t orelse has_abs u 

917 
 has_abs _ = false; 

918 

919 

20199  920 
(* dest abstraction *) 
0  921 

16678  922 
fun dest_abs (x, T, body) = 
923 
let 

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

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

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

927 
 name_clash _ = false; 

928 
in 

27335  929 
if name_clash body then dest_abs (Name.variant [x] x, T, body) (*potentially slow*) 
16678  930 
else (x, subst_bound (Free (x, T), body)) 
931 
end; 

932 

20160  933 

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

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

935 

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

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

937 

18253  938 
fun dummy_pattern T = Const (dummy_patternN, T); 
939 

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

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

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

942 

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

943 
fun no_dummy_patterns tm = 
16787  944 
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

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

946 

24733  947 
fun free_dummy_patterns (Const ("dummy_pattern", T)) used = 
24850  948 
let val [x] = Name.invents used Name.uu 1 
24733  949 
in (Free (Name.internal x, T), Name.declare x used) end 
950 
 free_dummy_patterns (Abs (x, T, b)) used = 

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

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

953 
 free_dummy_patterns (t $ u) used = 

954 
let 

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

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

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

958 
 free_dummy_patterns a used = (a, used); 

959 

24762  960 
fun replace_dummy Ts (Const ("dummy_pattern", T)) i = 
33063  961 
(list_comb (Var (("_dummy_", i), Ts > T), map_range Bound (length Ts)), i + 1) 
24762  962 
 replace_dummy Ts (Abs (x, T, t)) i = 
963 
let val (t', i') = replace_dummy (T :: Ts) t i 

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

965 
 replace_dummy Ts (t $ u) i = 

966 
let 

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

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

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

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

11903  971 

972 
val replace_dummy_patterns = replace_dummy []; 

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

973 

10552  974 
fun is_replaced_dummy_pattern ("_dummy_", _) = true 
975 
 is_replaced_dummy_pattern _ = false; 

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

976 

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

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

980 
 show_dummy_patterns a = a; 

981 

13484  982 

20100  983 
(* display variables *) 
984 

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

985 
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

986 
let 
15986  987 
val idx = string_of_int i; 
988 
val dot = 

989 
(case rev (Symbol.explode x) of 

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

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

992 
 c :: _ => Symbol.is_digit c 

993 
 _ => true); 

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

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

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

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

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

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

999 

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

1000 
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

1001 
 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

1002 

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

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

1004 

4444  1005 
structure BasicTerm: BASIC_TERM = Term; 
1006 
open BasicTerm; 