author  skalberg 
Fri, 04 Mar 2005 15:07:34 +0100  
changeset 15574  b1d1b5bfc464 
parent 15573  cf53c2dcf440 
child 15598  4ab52355bb53 
permissions  rwrr 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

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

5 

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

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

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

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

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

13 

4444  14 
signature BASIC_TERM = 
15 
sig 

16 
type indexname 

17 
type class 

18 
type sort 

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

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

22 
TFree of string * sort  

23 
TVar of indexname * sort 

24 
val > : typ * typ > typ 

25 
val > : typ list * typ > typ 

26 
val is_TVar: typ > bool 

15573  27 
val is_funtype: typ > bool 
4444  28 
val domain_type: typ > typ 
4480  29 
val range_type: typ > typ 
4444  30 
val binder_types: typ > typ list 
31 
val body_type: typ > typ 

32 
val strip_type: typ > typ list * typ 

33 
datatype term = 

34 
Const of string * typ  

35 
Free of string * typ  

36 
Var of indexname * typ  

37 
Bound of int  

38 
Abs of string * typ * term  

4493  39 
$ of term * term 
8408
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

40 
structure Vartab : TABLE 
13000  41 
structure Typtab : TABLE 
8408
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

42 
structure Termtab : TABLE 
4444  43 
exception TYPE of string * typ list * term list 
44 
exception TERM of string * term list 

7318  45 
val is_Bound: term > bool 
4444  46 
val is_Const: term > bool 
47 
val is_Free: term > bool 

48 
val is_Var: term > bool 

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

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

53 
val dest_Var: term > indexname * typ 

54 
val type_of: term > typ 

55 
val type_of1: typ list * term > typ 

56 
val fastype_of: term > typ 

57 
val fastype_of1: typ list * term > typ 

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

61 
val strip_qnt_body: string > term > term 

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

63 
val list_comb: term * term list > term 

64 
val strip_comb: term > term * term list 

65 
val head_of: term > term 

66 
val size_of_term: term > int 

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

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

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

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

71 
val map_typ: (class > class) > (string > string) > typ > typ 

72 
val map_term: 

73 
(class > class) > 

74 
(string > string) > (string > string) > term > term 

75 
val foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a 

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

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

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

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

84 
val a_itselfT: typ 

85 
val propT: typ 

86 
val implies: term 

87 
val all: typ > term 

88 
val equals: typ > term 

89 
val strip_all_body: term > term 

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

91 
val incr_bv: int * int * term > term 

92 
val incr_boundvars: int > term > term 

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

94 
val loose_bnos: term > int list 

95 
val loose_bvar: term * int > bool 

96 
val loose_bvar1: term * int > bool 

97 
val subst_bounds: term list * term > term 

98 
val subst_bound: term * term > term 

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

8408
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

100 
val subst_TVars_Vartab: typ Vartab.table > term > term 
4444  101 
val betapply: term * term > term 
102 
val eq_ix: indexname * indexname > bool 

103 
val ins_ix: indexname * indexname list > indexname list 

104 
val mem_ix: indexname * indexname list > bool 

105 
val aconv: term * term > bool 

106 
val aconvs: term list * term list > bool 

107 
val mem_term: term * term list > bool 

108 
val subset_term: term list * term list > bool 

109 
val eq_set_term: term list * term list > bool 

110 
val ins_term: term * term list > term list 

111 
val union_term: term list * term list > term list 

5585  112 
val inter_term: term list * term list > term list 
4444  113 
val could_unify: term * term > bool 
114 
val subst_free: (term * term) list > term > term 

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

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

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

8408
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

118 
val typ_subst_TVars_Vartab : typ Vartab.table > typ > typ 
4444  119 
val subst_Vars: (indexname * term) list > term > term 
120 
val incr_tvar: int > typ > typ 

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

122 
val atless: term * term > bool 

123 
val insert_aterm: term * term list > term list 

124 
val abstract_over: term * term > term 

11922  125 
val lambda: term > term > term 
4444  126 
val absfree: string * typ * term > term 
127 
val list_abs_free: (string * typ) list * term > term 

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

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

130 
val maxidx_of_typ: typ > int 

131 
val maxidx_of_typs: typ list > int 

132 
val maxidx_of_term: term > int 

13665  133 
val maxidx_of_terms: term list > int 
4444  134 
val variant: string list > string > string 
135 
val variantlist: string list * string list > string list 

136 
val variant_abs: string * typ * term > string * term 

137 
val rename_wrt_term: term > (string * typ) list > (string * typ) list 

138 
val add_new_id: string list * string > string list 

139 
val add_typ_classes: typ * class list > class list 

140 
val add_typ_ixns: indexname list * typ > indexname list 

141 
val add_typ_tfree_names: typ * string list > string list 

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

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

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

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

146 
val add_typ_tycons: typ * string list > string list 

147 
val add_typ_varnames: typ * string list > string list 

148 
val add_term_classes: term * class list > class list 

149 
val add_term_consts: term * string list > string list 

13646  150 
val term_consts: term > string list 
4444  151 
val add_term_frees: term * term list > term list 
152 
val term_frees: term > term list 

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

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

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

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

158 
val add_term_tvar_ixns: term * indexname list > indexname list 

159 
val add_term_tvarnames: term * string list > string list 

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

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

162 
val add_term_tycons: term * string list > string list 

163 
val add_term_vars: term * term list > term list 

164 
val term_vars: term > term list 

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

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

15472  169 
val show_var_qmarks: bool ref 
4444  170 
end; 
0  171 

4444  172 
signature TERM = 
173 
sig 

174 
include BASIC_TERM 

12981  175 
val match_bvars: (term * term) * (string * string) list > (string * string) list 
176 
val rename_abs: term > term > term > term option 

12499  177 
val invent_names: string list > string > int > string list 
178 
val add_tvarsT: (indexname * sort) list * typ > (indexname * sort) list 

179 
val add_tvars: (indexname * sort) list * term > (indexname * sort) list 

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

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

4444  182 
val indexname_ord: indexname * indexname > order 
183 
val typ_ord: typ * typ > order 

184 
val typs_ord: typ list * typ list > order 

185 
val term_ord: term * term > order 

186 
val terms_ord: term list * term list > order 

14472
cba7c0a3ffb3
Removing the datatype declaration of "order" allows the standard General.order
paulson
parents:
13665
diff
changeset

187 
val hd_ord: term * term > order 
4444  188 
val termless: term * term > bool 
14786
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

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

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

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

192 
val replace_dummy_patterns: int * term > int * term 
10552  193 
val is_replaced_dummy_pattern: indexname > bool 
13484  194 
val adhoc_freeze_vars: term > term * string list 
14786
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

195 
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

196 
val string_of_vname': indexname > string 
4444  197 
end; 
198 

199 
structure Term: TERM = 

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

200 
struct 
0  201 

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

203 
for resolution.*) 

204 
type indexname = string*int; 

205 

4626  206 
(* Types are classified by sorts. *) 
0  207 
type class = string; 
208 
type sort = class list; 

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

209 
type arity = string * sort list * sort; 
0  210 

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

212 
datatype typ = Type of string * typ list 

213 
 TFree of string * sort 

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

214 
 TVar of indexname * sort; 
0  215 

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

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

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

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

223 

224 

225 

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

231 
 Abs of string*typ*term 

3965  232 
 op $ of term*term; 
0  233 

234 

235 
(*For errors involving type mismatches*) 

236 
exception TYPE of string * typ list * term list; 

237 

238 
(*For system errors involving terms*) 

239 
exception TERM of string * term list; 

240 

241 

242 
(*Note variable naming conventions! 

243 
a,b,c: string 

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

245 
i,j,m,n: int 

246 
t,u: term 

247 
v,w: indexnames 

248 
x,y: any 

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

250 
T,U: typ 

251 
*) 

252 

253 

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

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

255 

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

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

257 

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

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

260 

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

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

262 
 dest_Type T = raise TYPE ("dest_Type", [T], []); 
c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

263 

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

264 

0  265 
(** Discriminators **) 
266 

7318  267 
fun is_Bound (Bound _) = true 
268 
 is_Bound _ = false; 

269 

0  270 
fun is_Const (Const _) = true 
271 
 is_Const _ = false; 

272 

273 
fun is_Free (Free _) = true 

274 
 is_Free _ = false; 

275 

276 
fun is_Var (Var _) = true 

277 
 is_Var _ = false; 

278 

279 
fun is_TVar (TVar _) = true 

280 
 is_TVar _ = false; 

281 

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

284 
 is_funtype _ = false; 

285 

0  286 
(** Destructors **) 
287 

288 
fun dest_Const (Const x) = x 

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

290 

291 
fun dest_Free (Free x) = x 

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

293 

294 
fun dest_Var (Var x) = x 

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

296 

297 

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

4064  300 

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

303 
 binder_types _ = []; 

304 

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

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

307 
 body_type T = T; 

308 

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

310 
fun strip_type T : typ list * typ = 

311 
(binder_types T, body_type T); 

312 

313 

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

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

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

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

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

0  320 
 type_of1 (Ts, Var (_,T)) = T 
321 
 type_of1 (Ts, Abs (_,T,body)) = T > type_of1(T::Ts, body) 

13000  322 
 type_of1 (Ts, f$u) = 
0  323 
let val U = type_of1(Ts,u) 
324 
and T = type_of1(Ts,f) 

325 
in case T of 

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

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

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

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

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

331 
[T,U], [f$u]) 
0  332 
end; 
333 

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

335 

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

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

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

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

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

13000  345 
 fastype_of1 (_, Var (_,T)) = T 
61  346 
 fastype_of1 (Ts, Abs (_,T,u)) = T > fastype_of1 (T::Ts, u); 
347 

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

0  349 

350 

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

0  353 
(* maps (x1,...,xn)t to t *) 
13000  354 
fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t 
0  355 
 strip_abs_body u = u; 
356 

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

13000  358 
fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t 
0  359 
 strip_abs_vars u = [] : (string*typ) list; 
360 

361 

362 
fun strip_qnt_body qnt = 

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

364 
 strip t = t 

365 
in strip end; 

366 

367 
fun strip_qnt_vars qnt = 

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

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

370 
in strip end; 

371 

372 

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

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

376 

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

13000  378 
fun strip_comb u : term * term list = 
0  379 
let fun stripc (f$t, ts) = stripc (f, t::ts) 
13000  380 
 stripc x = x 
0  381 
in stripc(u,[]) end; 
382 

383 

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

385 
fun head_of (f$t) = head_of f 

386 
 head_of u = u; 

387 

388 

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

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

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

392 
 size_of_term _ = 1; 

393 

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

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

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

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

397 

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

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

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

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

401 

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

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

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

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

407 
 map(t as Bound _) = t 

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

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

410 
in map end; 

411 

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

413 
fun it_term_types f = 

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

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

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

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

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

419 
 iter(Bound _, a) = a 

420 
in iter end 

421 

422 

423 
(** Connectives of higher order logic **) 

424 

375  425 
fun itselfT ty = Type ("itself", [ty]); 
14854  426 
val a_itselfT = itselfT (TFree ("'a", [])); 
375  427 

0  428 
val propT : typ = Type("prop",[]); 
429 

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

431 

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

433 

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

435 

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

13000  437 
fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t 
0  438 
 strip_all_body t = t; 
439 

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

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

13000  442 
(a,T) :: strip_all_vars t 
0  443 
 strip_all_vars t = [] : (string*typ) list; 
444 

445 
(*increments a term's nonlocal bound variables 

446 
required when moving a term within abstractions 

447 
inc is increment for bound variables 

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

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

451 
Abs(a, T, incr_bv(inc,lev+1,body)) 
13000  452 
 incr_bv (inc, lev, f$t) = 
0  453 
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 
454 
 incr_bv (inc, lev, u) = u; 

455 

456 
fun incr_boundvars 0 t = t 

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

458 

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

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

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

463 
else (x,y)::al) 

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

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

466 

467 
(* strip abstractions created by parameters *) 

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

469 

470 
fun rename_abs pat obj t = 

471 
let 

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

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

15570  474 
Abs (getOpt (assoc_string (ren, x), x), T, ren_abs b) 
12981  475 
 ren_abs (f $ t) = ren_abs f $ ren_abs t 
476 
 ren_abs t = t 

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

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

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

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

482 
if i<lev then js else (ilev) ins_int js 
0  483 
 add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js) 
484 
 add_loose_bnos (f$t, lev, js) = 

13000  485 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
0  486 
 add_loose_bnos (_, _, js) = js; 
487 

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

489 

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

491 
level k or beyond. *) 

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

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

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

495 
 loose_bvar _ = false; 

496 

2792  497 
fun loose_bvar1(Bound i,k) = i = k 
498 
 loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 

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

500 
 loose_bvar1 _ = false; 

0  501 

502 
(*Substitute arguments for loose bound variables. 

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

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

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

508 
*) 

13000  509 
fun subst_bounds (args: term list, t) : term = 
0  510 
let val n = length args; 
511 
fun subst (t as Bound i, lev) = 

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

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

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

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

515 
 subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1)) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

516 
 subst (f$t, lev) = subst(f,lev) $ subst(t,lev) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

517 
 subst (t,lev) = t 
0  518 
in case args of [] => t  _ => subst (t,0) end; 
519 

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

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

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

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

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

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

526 
 subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1)) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

527 
 subst (f$t, lev) = subst(f,lev) $ subst(t,lev) 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

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

530 

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

532 
fun betapply (Abs(_,_,t), u) = subst_bound (u,t) 
0  533 
 betapply (f,u) = f$u; 
534 

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

535 

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

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

537 

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

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

540 

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

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

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

544 

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

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

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

547 

0  548 
(*Tests whether 2 terms are alphaconvertible and have same type. 
4626  549 
Note that constants may have more than one type.*) 
0  550 
fun (Const(a,T)) aconv (Const(b,U)) = a=b andalso T=U 
2752  551 
 (Free(a,T)) aconv (Free(b,U)) = a=b andalso T=U 
552 
 (Var(v,T)) aconv (Var(w,U)) = eq_ix(v,w) andalso T=U 

553 
 (Bound i) aconv (Bound j) = i=j 

0  554 
 (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u andalso T=U 
2752  555 
 (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u) 
0  556 
 _ aconv _ = false; 
557 

2176  558 
(** Membership, insertion, union for terms **) 
559 

560 
fun mem_term (_, []) = false 

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

562 

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

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

564 
 subset_term (x :: xs, ys) = mem_term (x, ys) andalso subset_term(xs, ys); 
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2176
diff
changeset

565 

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

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

567 
xs = ys orelse (subset_term (xs, ys) andalso subset_term (ys, xs)); 
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2176
diff
changeset

568 

2176  569 
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; 
570 

571 
fun union_term (xs, []) = xs 

572 
 union_term ([], ys) = ys 

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

574 

5585  575 
fun inter_term ([], ys) = [] 
576 
 inter_term (x::xs, ys) = 

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

578 

0  579 
(*are two term lists alphaconvertible in corresponding elements?*) 
580 
fun aconvs ([],[]) = true 

581 
 aconvs (t::ts, u::us) = t aconv u andalso aconvs(ts,us) 

582 
 aconvs _ = false; 

583 

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

587 
let fun matchrands (f$t, g$u) = could_unify(t,u) andalso matchrands(f,g) 

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

588 
 matchrands _ = true 
0  589 
in case (head_of t , head_of u) of 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

590 
(_, Var _) => true 
0  591 
 (Var _, _) => true 
592 
 (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u) 

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

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

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

596 
 (_, Abs _) => true 

597 
 _ => false 

598 
end; 

599 

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

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

602 
 subst_free pairs = 

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

604 
case gen_assoc (op aconv) (pairs, u) of 
15531  605 
SOME u' => u' 
606 
 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

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

608 
 _ => u) 
0  609 
in substf end; 
610 

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

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

613 

614 

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

618 
fun abstract_over (v,body) = 

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

620 
(case u of 

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

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

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

623 
 _ => u) 
0  624 
in abst(0,body) end; 
625 

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

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

0  629 

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

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

632 

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

634 
fun list_abs_free ([ ] , t) = t 

13000  635 
 list_abs_free ((a,T)::vars, t) = 
0  636 
absfree(a, T, list_abs_free(vars,t)); 
637 

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

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

13000  640 
 list_all_free ((a,T)::vars, t) = 
0  641 
(all T) $ (absfree(a, T, list_all_free(vars,t))); 
642 

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

644 
fun list_all ([], t) = t 

13000  645 
 list_all ((a,T)::vars, t) = 
0  646 
(all T) $ (Abs(a, T, list_all(vars,t))); 
647 

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

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

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

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

653 
 subst (f$t') = subst f $ subst t' 
15570  654 
 subst t = getOpt (assoc(instl,t),t) 
0  655 
in subst t end; 
656 

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

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

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

660 
 subst(T as TFree _) = T 
15570  661 
 subst(T as TVar(ixn,_)) = getOpt (assoc(iTs,ixn),T) 
0  662 
in subst T end; 
663 

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

664 
(*Substitute for type Vars in a term*) 
0  665 
val subst_TVars = map_term_types o typ_subst_TVars; 
666 

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

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

672 
 subst(t) = t 

673 
in subst t end; 

674 

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

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

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

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

15531  680 
NONE => Var(ixn,typ_subst_TVars iTs T) 
681 
 SOME t => t) 

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

684 
 subst(f$t) = subst f $ subst t 

685 
in subst end; 

686 

687 

15573  688 
(** Identifying firstorder terms **) 
689 

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

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

692 

693 
(*First order means in all terms of the form f(t1,...,tn) no argument has a function 

694 
type.*) 

695 
fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body 

696 
 first_order1 Ts t = 

697 
case strip_comb t of 

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

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

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

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

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

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

704 

705 
val is_first_order = first_order1 []; 

706 

707 

0  708 
(*Computing the maximum index of a typ*) 
2146  709 
fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts 
0  710 
 maxidx_of_typ(TFree _) = ~1 
2146  711 
 maxidx_of_typ(TVar((_,i),_)) = i 
712 
and maxidx_of_typs [] = ~1 

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

0  714 

715 

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

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

718 
 maxidx_of_term (Bound _) = ~1 

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

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

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

0  723 

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

0  726 

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

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

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

730 

731 
(**** Syntaxrelated declarations ****) 

732 

733 

4626  734 
(*Dummy type for parsing and printing. Will be replaced during type inference. *) 
0  735 
val dummyT = Type("dummy",[]); 
736 

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

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

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

739 
fun check (T as Type ("dummy", _)) = 
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

740 
raise TYPE ("Illegal occurrence of '_' dummy type", [T], []) 
15570  741 
 check (Type (_, Ts)) = List.app check Ts 
14786
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

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

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

744 

0  745 

746 
(*** Printing ***) 

747 

14676  748 
(*Makes a variant of a name distinct from the names in bs. 
749 
First attaches the suffix and then increments this; 

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

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

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

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

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

756 
in vary1 (if c = "" then "u" else c) ^ u end; 
0  757 

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

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

13000  760 
 variantlist(b::bs, used) = 
0  761 
let val b' = variant used b 
762 
in b' :: variantlist (bs, b'::used) end; 

763 

14695  764 
(*Invent fresh names*) 
765 
fun invent_names _ _ 0 = [] 

766 
 invent_names used a n = 

767 
let val b = Symbol.bump_string a in 

768 
if a mem_string used then invent_names used b n 

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

770 
end; 

11353  771 

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

772 

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

773 

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

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

775 

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

776 
fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes cs Ts 
4017
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

777 
 add_typ_classes (TFree (_, S), cs) = S union cs 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

778 
 add_typ_classes (TVar (_, S), cs) = S union cs; 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

779 

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

780 
fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (c ins cs) Ts 
4017
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

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

782 

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

783 
val add_term_classes = it_term_types add_typ_classes; 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

784 
val add_term_tycons = it_term_types add_typ_tycons; 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

785 

9319  786 
fun add_term_consts (Const (c, _), cs) = c ins_string cs 
4017
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

787 
 add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs)) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

788 
 add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

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

790 

13646  791 
fun term_consts t = add_term_consts(t,[]); 
792 

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

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

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

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

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

799 

4631  800 
fun exists_subterm P = 
801 
let fun ex t = P t orelse 

802 
(case t of 

803 
u $ v => ex u orelse ex v 

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

805 
 _ => false) 

806 
in ex end; 

807 

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

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

809 
fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

810 
 map_typ f _ (TFree (x, S)) = TFree (x, map f S) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

811 
 map_typ f _ (TVar (xi, S)) = TVar (xi, map f S); 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

812 

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

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

814 
fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

815 
 map_term f g _ (Free (x, T)) = Free (x, map_typ f g T) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

816 
 map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

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

818 
 map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t) 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

819 
 map_term f g h (t $ u) = map_term f g h t $ map_term f g h u; 
63878e2587a7
add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
wenzelm
parents:
3965
diff
changeset

820 

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

821 

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

822 

0  823 
(** TFrees and TVars **) 
824 

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

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

827 

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

828 
(*Accumulates the names of Frees in the term, suppressing duplicates.*) 
c69bd9754473
added add_term_free_names (more precise/efficient than add_term_names);
wenzelm
parents:
12499
diff
changeset

829 
fun add_term_free_names (Free(a,_), bs) = a ins_string bs 
c69bd9754473
added add_term_free_names (more precise/efficient than add_term_names);
wenzelm
parents:
12499
diff
changeset

830 
 add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs)) 
c69bd9754473
added add_term_free_names (more precise/efficient than add_term_names);
wenzelm
parents:
12499
diff
changeset

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

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

833 

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

10666  836 
fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs 
2176  837 
 add_term_names (Free(a,_), bs) = a ins_string bs 
0  838 
 add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) 
839 
 add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) 

840 
 add_term_names (_, bs) = bs; 

841 

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

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

843 
fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts 
0  844 
 add_typ_tvars(TFree(_),vs) = vs 
845 
 add_typ_tvars(TVar(v),vs) = v ins vs; 

846 

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

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

848 
fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts 
2176  849 
 add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs 
0  850 
 add_typ_tfree_names(TVar(_),fs) = fs; 
851 

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

852 
fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts 
0  853 
 add_typ_tfrees(TFree(f),fs) = f ins fs 
854 
 add_typ_tfrees(TVar(_),fs) = fs; 

855 

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

856 
fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts 
2176  857 
 add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms 
858 
 add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms; 

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

859 

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

862 

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

864 
val add_term_tfrees = it_term_types add_typ_tfrees; 

865 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

866 

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

867 
val add_term_tvarnames = it_term_types add_typ_varnames; 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

868 

0  869 
(*Nonlist versions*) 
870 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

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

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

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

874 

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

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

876 

15570  877 
fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts) 
13000  878 
 add_typ_ixns(ixns,TVar(ixn,_)) = if mem_ix (ixn, ixns) then ixns 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

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

881 

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

882 
fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

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

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

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

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

887 
add_term_tvar_ixns(t,add_typ_ixns(ixns,T)) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
728
diff
changeset

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

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

890 

0  891 
(** Frees and Vars **) 
892 

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

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

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

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

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

898 
 atless _ = false; 

899 

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

901 
fun insert_aterm (t,us) = 

902 
let fun inserta [] = [t] 

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

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

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

906 
else u :: inserta(us') 
0  907 
in inserta us end; 
908 

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

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

911 
Var _ => insert_aterm(t,vars) 

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

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

914 
 _ => vars; 

915 

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

917 

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

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

920 
Free _ => insert_aterm(t,frees) 

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

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

923 
 _ => frees; 

924 

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

926 

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

928 
having a unique name. *) 

929 
fun variant_abs (a,T,P) = 

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

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

931 
in (b, subst_bound (Free(b,T), P)) end; 
0  932 

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

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

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

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

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

939 
fun rename_wrt_term t = rename_aTs (add_term_names(t,[])); 

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

940 

1417  941 

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

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

943 

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

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

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

947 

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

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

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

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

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

952 

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

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

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

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

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

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

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

959 

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

960 
(*foldl types of term*) 
8609  961 
fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T) 
962 
 foldl_term_types f (x, t as Free (_, T)) = f t (x, T) 

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

964 
 foldl_term_types f (x, Bound _) = x 

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

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

967 

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

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

969 

12499  970 
(*collect variables*) 
971 
val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs  (vs, _) => vs); 

972 
val add_tvars = foldl_types add_tvarsT; 

973 
val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs  (vs, _) => vs); 

974 
val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs  (vs, _) => vs); 

975 

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

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

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

979 

1417  980 

4444  981 
(** type and term orders **) 
982 

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

14472
cba7c0a3ffb3
Removing the datatype declaration of "order" allows the standard General.order
paulson
parents:
13665
diff
changeset

984 
(case Int.compare (i, j) of EQUAL => String.compare (x, y)  ord => ord); 
4444  985 

14472
cba7c0a3ffb3
Removing the datatype declaration of "order" allows the standard General.order
paulson
parents:
13665
diff
changeset

986 
val sort_ord = list_ord String.compare; 
13000  987 

4444  988 

989 
(* typ_ord *) 

990 

14472
cba7c0a3ffb3
Removing the datatype declaration of "order" allows the standard General.order
paulson
parents:
13665
diff
changeset

991 
fun typ_ord (Type x, Type y) = prod_ord String.compare typs_ord (x, y) 
4444  992 
 typ_ord (Type _, _) = GREATER 
993 
 typ_ord (TFree _, Type _) = LESS 

14472
cba7c0a3ffb3
Removing the datatype declaration of "order" allows the standard General.order
paulson
parents:
13665
diff
changeset

994 
 typ_ord (TFree x, TFree y) = prod_ord String.compare sort_ord (x, y) 
4444  995 
 typ_ord (TFree _, TVar _) = GREATER 
996 
 typ_ord (TVar _, Type _) = LESS 

997 
 typ_ord (TVar _, TFree _) = LESS 

13000  998 
 typ_ord (TVar x, TVar y) = prod_ord indexname_ord sort_ord (x, y) 
4444  999 
and typs_ord Ts_Us = list_ord typ_ord Ts_Us; 
1000 

1001 

1002 
(* term_ord *) 

1003 

1004 
(*a linear wellfounded ACcompatible ordering for terms: 

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

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

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

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

1009 

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

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

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

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

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

1015 

1016 
fun term_ord (Abs (_, T, t), Abs(_, U, u)) = 

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

1018 
 term_ord (t, u) = 

14472
cba7c0a3ffb3
Removing the datatype declaration of "order" allows the standard General.order
paulson
parents:
13665
diff
changeset

1019 
(case Int.compare (size_of_term t, size_of_term u) of 
4444  1020 
EQUAL => 
1021 
let val (f, ts) = strip_comb t and (g, us) = strip_comb u in 

1022 
(case hd_ord (f, g) of EQUAL => terms_ord (ts, us)  ord => ord) 

1023 
end 

1024 
 ord => ord) 

1025 
and hd_ord (f, g) = 

14472
cba7c0a3ffb3
Removing the datatype declaration of "order" allows the standard General.order
paulson
parents:
13665
diff
changeset

1026 
prod_ord (prod_ord indexname_ord typ_ord) Int.compare (dest_hd f, dest_hd g) 
4444  1027 
and terms_ord (ts, us) = list_ord term_ord (ts, us); 
1028 

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

1030 

8408
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1031 
structure Vartab = TableFun(type key = indexname val ord = indexname_ord); 
13000  1032 
structure Typtab = TableFun(type key = typ val ord = typ_ord); 
8408
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1033 
structure Termtab = TableFun(type key = term val ord = term_ord); 
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1034 

4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1035 
(*Substitute for type Vars in a type, version using Vartab*) 
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1036 
fun typ_subst_TVars_Vartab iTs T = if Vartab.is_empty iTs then T else 
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1037 
let fun subst(Type(a, Ts)) = Type(a, map subst Ts) 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1038 
 subst(T as TFree _) = T 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1039 
 subst(T as TVar(ixn, _)) = 
15531  1040 
(case Vartab.lookup (iTs, ixn) of NONE => T  SOME(U) => U) 
8408
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1041 
in subst T end; 
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1042 

4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1043 
(*Substitute for type Vars in a term, version using Vartab*) 
4d981311dab7
Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
berghofe
parents:
7638
diff
changeset

1044 
val subst_TVars_Vartab = map_term_types o typ_subst_TVars_Vartab; 
4444  1045 

1046 

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

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

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

1417  1051 

1052 
(** Sharing of types **) 

1053 

13000  1054 
val memo_types = ref (Typtab.empty: typ Typtab.table); 
1417  1055 

1056 
fun compress_type T = 

13000  1057 
(case Typtab.lookup (! memo_types, T) of 
15531  1058 
SOME T' => T' 
1059 
 NONE => 

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

1062 

1417  1063 

1064 
(** Sharing of atomic terms **) 

1065 

13000  1066 
val memo_terms = ref (Termtab.empty : term Termtab.table); 
1417  1067 

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

13000  1069 
 share_term (Abs (a, T, u)) = Abs (a, T, share_term u) 
1417  1070 
 share_term t = 
13000  1071 
(case Termtab.lookup (! memo_terms, t) of 
15531  1072 
SOME t' => t' 
1073 
 NONE => (memo_terms := Termtab.update ((t, t), ! memo_terms); t)); 

1417  1074 

1075 
val compress_term = share_term o map_term_types compress_type; 

1076 

4444  1077 

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

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

1079 

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

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

1081 

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

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

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

1084 

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

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

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

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

1088 

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

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

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

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

1094 
 replace_dummy Ts (i, t $ u) = 

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

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

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

1098 

1099 
val replace_dummy_patterns = replace_dummy []; 

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

1100 

10552  1101 
fun is_replaced_dummy_pattern ("_dummy_", _) = true 
1102 
 is_replaced_dummy_pattern _ = false; 

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

1103 

13484  1104 

1105 
(* adhoc freezing *) 

1106 

1107 
fun adhoc_freeze_vars tm = 

1108 
let 

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

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

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

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

1113 
in (subst_atomic insts tm, xs) end; 

1114 

1115 

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

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

1117 

15472  1118 
val show_var_qmarks = ref true; 
1119 

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

1120 
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

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

1122 
val si = string_of_int i; 
15570  1123 
val dot = getOpt (try (Symbol.is_digit o List.last o Symbol.explode) x, true); 
15472  1124 
val qmark = if !show_var_qmarks then "?" else ""; 
14786
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

1125 
in 
15472  1126 
if dot then qmark ^ x ^ "." ^ si 
1127 
else if i = 0 then qmark ^ x 

1128 
else qmark ^ x ^ si 

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

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

1130 

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

1131 
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

1132 
 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

1133 

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

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

1135 

4444  1136 
structure BasicTerm: BASIC_TERM = Term; 
1137 
open BasicTerm; 