author  skalberg 
Sun, 13 Feb 2005 17:15:14 +0100  
changeset 15531  08c8dad8e399 
parent 15472  4674102737e9 
child 15570  8d8c70b41bab 
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 

27 
val domain_type: typ > typ 

4480  28 
val range_type: typ > typ 
4444  29 
val binder_types: typ > typ list 
30 
val body_type: typ > typ 

31 
val strip_type: typ > typ list * typ 

32 
datatype term = 

33 
Const of string * typ  

34 
Free of string * typ  

35 
Var of indexname * typ  

36 
Bound of int  

37 
Abs of string * typ * term  

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

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

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

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

47 
val is_Var: term > bool 

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

48 
val dest_Type: typ > string * typ list 
4444  49 
val dest_Const: term > string * typ 
50 
val dest_Free: term > string * typ 

51 
val dest_Var: term > indexname * typ 

52 
val type_of: term > typ 

53 
val type_of1: typ list * term > typ 

54 
val fastype_of: term > typ 

55 
val fastype_of1: typ list * term > typ 

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

59 
val strip_qnt_body: string > term > term 

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

61 
val list_comb: term * term list > term 

62 
val strip_comb: term > term * term list 

63 
val head_of: term > term 

64 
val size_of_term: term > int 

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

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

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

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

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

70 
val map_term: 

71 
(class > class) > 

72 
(string > string) > (string > string) > term > term 

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

8609  74 
val foldl_term_types: (term > 'a * typ > 'a) > 'a * term > 'a 
4444  75 
val foldl_types: ('a * typ > 'a) > 'a * term > 'a 
76 
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

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

4444  80 
val dummyT: typ 
81 
val itselfT: typ > typ 

82 
val a_itselfT: typ 

83 
val propT: typ 

84 
val implies: term 

85 
val all: typ > term 

86 
val equals: typ > term 

87 
val strip_all_body: term > term 

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

89 
val incr_bv: int * int * term > term 

90 
val incr_boundvars: int > term > term 

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

92 
val loose_bnos: term > int list 

93 
val loose_bvar: term * int > bool 

94 
val loose_bvar1: term * int > bool 

95 
val subst_bounds: term list * term > term 

96 
val subst_bound: term * term > term 

97 
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

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

101 
val ins_ix: indexname * indexname list > indexname list 

102 
val mem_ix: indexname * indexname list > bool 

103 
val aconv: term * term > bool 

104 
val aconvs: term list * term list > bool 

105 
val mem_term: term * term list > bool 

106 
val subset_term: term list * term list > bool 

107 
val eq_set_term: term list * term list > bool 

108 
val ins_term: term * term list > term list 

109 
val union_term: term list * term list > term list 

5585  110 
val inter_term: term list * term list > term list 
4444  111 
val could_unify: term * term > bool 
112 
val subst_free: (term * term) list > term > term 

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

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

115 
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

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

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

120 
val atless: term * term > bool 

121 
val insert_aterm: term * term list > term list 

122 
val abstract_over: term * term > term 

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

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

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

128 
val maxidx_of_typ: typ > int 

129 
val maxidx_of_typs: typ list > int 

130 
val maxidx_of_term: term > int 

13665  131 
val maxidx_of_terms: term list > int 
4444  132 
val variant: string list > string > string 
133 
val variantlist: string list * string list > string list 

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

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

136 
val add_new_id: string list * string > string list 

137 
val add_typ_classes: typ * class list > class list 

138 
val add_typ_ixns: indexname list * typ > indexname list 

139 
val add_typ_tfree_names: typ * string list > string list 

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

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

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

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

144 
val add_typ_tycons: typ * string list > string list 

145 
val add_typ_varnames: typ * string list > string list 

146 
val add_term_classes: term * class list > class list 

147 
val add_term_consts: term * string list > string list 

13646  148 
val term_consts: term > string list 
4444  149 
val add_term_frees: term * term list > term list 
150 
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

151 
val add_term_free_names: term * string list > string list 
4444  152 
val add_term_names: term * string list > string list 
153 
val add_term_tfree_names: term * string list > string list 

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

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

156 
val add_term_tvar_ixns: term * indexname list > indexname list 

157 
val add_term_tvarnames: term * string list > string list 

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

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

160 
val add_term_tycons: term * string list > string list 

161 
val add_term_vars: term * term list > term list 

162 
val term_vars: term > term list 

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

4631  164 
val exists_subterm: (term > bool) > term > bool 
4444  165 
val compress_type: typ > typ 
166 
val compress_term: term > term 

15472  167 
val show_var_qmarks: bool ref 
4444  168 
end; 
0  169 

4444  170 
signature TERM = 
171 
sig 

172 
include BASIC_TERM 

12981  173 
val match_bvars: (term * term) * (string * string) list > (string * string) list 
174 
val rename_abs: term > term > term > term option 

12499  175 
val invent_names: string list > string > int > string list 
176 
val add_tvarsT: (indexname * sort) list * typ > (indexname * sort) list 

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

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

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

4444  180 
val indexname_ord: indexname * indexname > order 
181 
val typ_ord: typ * typ > order 

182 
val typs_ord: typ list * typ list > order 

183 
val term_ord: term * term > order 

184 
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

185 
val hd_ord: term * term > order 
4444  186 
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

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

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

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

190 
val replace_dummy_patterns: int * term > int * term 
10552  191 
val is_replaced_dummy_pattern: indexname > bool 
13484  192 
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

193 
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

194 
val string_of_vname': indexname > string 
4444  195 
end; 
196 

197 
structure Term: TERM = 

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

198 
struct 
0  199 

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

201 
for resolution.*) 

202 
type indexname = string*int; 

203 

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

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

207 
type arity = string * sort list * sort; 
0  208 

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

210 
datatype typ = Type of string * typ list 

211 
 TFree of string * sort 

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

212 
 TVar of indexname * sort; 
0  213 

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

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

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

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

221 

222 

223 

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

229 
 Abs of string*typ*term 

3965  230 
 op $ of term*term; 
0  231 

232 

233 
(*For errors involving type mismatches*) 

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

235 

236 
(*For system errors involving terms*) 

237 
exception TERM of string * term list; 

238 

239 

240 
(*Note variable naming conventions! 

241 
a,b,c: string 

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

243 
i,j,m,n: int 

244 
t,u: term 

245 
v,w: indexnames 

246 
x,y: any 

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

248 
T,U: typ 

249 
*) 

250 

251 

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

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

253 

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

254 
fun S > T = Type("fun",[S,T]); 
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 
(*handy for multiple args: [T1,...,Tn]>T gives T1>(T2> ... >T)*) 
c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

257 
val op > = foldr (op >); 
c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

258 

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

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

260 
 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

261 

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

262 

0  263 
(** Discriminators **) 
264 

7318  265 
fun is_Bound (Bound _) = true 
266 
 is_Bound _ = false; 

267 

0  268 
fun is_Const (Const _) = true 
269 
 is_Const _ = false; 

270 

271 
fun is_Free (Free _) = true 

272 
 is_Free _ = false; 

273 

274 
fun is_Var (Var _) = true 

275 
 is_Var _ = false; 

276 

277 
fun is_TVar (TVar _) = true 

278 
 is_TVar _ = false; 

279 

280 
(** Destructors **) 

281 

282 
fun dest_Const (Const x) = x 

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

284 

285 
fun dest_Free (Free x) = x 

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

287 

288 
fun dest_Var (Var x) = x 

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

290 

291 

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

4064  294 

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

297 
 binder_types _ = []; 

298 

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

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

301 
 body_type T = T; 

302 

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

304 
fun strip_type T : typ list * typ = 

305 
(binder_types T, body_type T); 

306 

307 

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

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

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

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

13000  312 
 type_of1 (Ts, Bound i) = (nth_elem (i,Ts) 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

313 
handle LIST _ => raise TYPE("type_of: bound variable", [], [Bound i])) 
0  314 
 type_of1 (Ts, Var (_,T)) = T 
315 
 type_of1 (Ts, Abs (_,T,body)) = T > type_of1(T::Ts, body) 

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

319 
in case T of 

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

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

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

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

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

325 
[T,U], [f$u]) 
0  326 
end; 
327 

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

329 

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

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

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

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

337 
 fastype_of1 (Ts, Bound i) = (nth_elem(i,Ts) 

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

338 
handle LIST _ => raise TERM("fastype_of: Bound", [Bound i])) 
13000  339 
 fastype_of1 (_, Var (_,T)) = T 
61  340 
 fastype_of1 (Ts, Abs (_,T,u)) = T > fastype_of1 (T::Ts, u); 
341 

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

0  343 

344 

10806  345 
val list_abs = foldr (fn ((x, T), t) => Abs (x, T, t)); 
346 

0  347 
(* maps (x1,...,xn)t to t *) 
13000  348 
fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t 
0  349 
 strip_abs_body u = u; 
350 

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

13000  352 
fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t 
0  353 
 strip_abs_vars u = [] : (string*typ) list; 
354 

355 

356 
fun strip_qnt_body qnt = 

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

358 
 strip t = t 

359 
in strip end; 

360 

361 
fun strip_qnt_vars qnt = 

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

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

364 
in strip end; 

365 

366 

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

368 
val list_comb : term * term list > term = foldl (op $); 

369 

370 

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

13000  372 
fun strip_comb u : term * term list = 
0  373 
let fun stripc (f$t, ts) = stripc (f, t::ts) 
13000  374 
 stripc x = x 
0  375 
in stripc(u,[]) end; 
376 

377 

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

379 
fun head_of (f$t) = head_of f 

380 
 head_of u = u; 

381 

382 

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

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

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

386 
 size_of_term _ = 1; 

387 

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

388 
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

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

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

391 

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

392 
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

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

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

395 

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

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

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

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

401 
 map(t as Bound _) = t 

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

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

404 
in map end; 

405 

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

407 
fun it_term_types f = 

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

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

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

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

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

413 
 iter(Bound _, a) = a 

414 
in iter end 

415 

416 

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

418 

375  419 
fun itselfT ty = Type ("itself", [ty]); 
14854  420 
val a_itselfT = itselfT (TFree ("'a", [])); 
375  421 

0  422 
val propT : typ = Type("prop",[]); 
423 

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

425 

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

427 

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

429 

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

13000  431 
fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t 
0  432 
 strip_all_body t = t; 
433 

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

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

13000  436 
(a,T) :: strip_all_vars t 
0  437 
 strip_all_vars t = [] : (string*typ) list; 
438 

439 
(*increments a term's nonlocal bound variables 

440 
required when moving a term within abstractions 

441 
inc is increment for bound variables 

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

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

445 
Abs(a, T, incr_bv(inc,lev+1,body)) 
13000  446 
 incr_bv (inc, lev, f$t) = 
0  447 
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 
448 
 incr_bv (inc, lev, u) = u; 

449 

450 
fun incr_boundvars 0 t = t 

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

452 

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

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

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

457 
else (x,y)::al) 

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

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

460 

461 
(* strip abstractions created by parameters *) 

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

463 

464 
fun rename_abs pat obj t = 

465 
let 

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

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

468 
Abs (if_none (assoc_string (ren, x)) x, T, ren_abs b) 

469 
 ren_abs (f $ t) = ren_abs f $ ren_abs t 

470 
 ren_abs t = t 

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

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

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

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

476 
if i<lev then js else (ilev) ins_int js 
0  477 
 add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js) 
478 
 add_loose_bnos (f$t, lev, js) = 

13000  479 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
0  480 
 add_loose_bnos (_, _, js) = js; 
481 

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

483 

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

485 
level k or beyond. *) 

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

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

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

489 
 loose_bvar _ = false; 

490 

2792  491 
fun loose_bvar1(Bound i,k) = i = k 
492 
 loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 

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

494 
 loose_bvar1 _ = false; 

0  495 

496 
(*Substitute arguments for loose bound variables. 

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

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

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

502 
*) 

13000  503 
fun subst_bounds (args: term list, t) : term = 
0  504 
let val n = length args; 
505 
fun subst (t as Bound i, lev) = 

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

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

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

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

509 
 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

510 
 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

511 
 subst (t,lev) = t 
0  512 
in case args of [] => t  _ => subst (t,0) end; 
513 

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

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

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

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

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

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

520 
 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

521 
 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

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

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

524 

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

526 
fun betapply (Abs(_,_,t), u) = subst_bound (u,t) 
0  527 
 betapply (f,u) = f$u; 
528 

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

529 

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

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

531 

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

532 
(*optimized equality test for indexnames. Yields a huge gain under Poly/ML*) 
2959  533 
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

534 

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

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

537 
 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

538 

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

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

540 
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

541 

0  542 
(*Tests whether 2 terms are alphaconvertible and have same type. 
4626  543 
Note that constants may have more than one type.*) 
0  544 
fun (Const(a,T)) aconv (Const(b,U)) = a=b andalso T=U 
2752  545 
 (Free(a,T)) aconv (Free(b,U)) = a=b andalso T=U 
546 
 (Var(v,T)) aconv (Var(w,U)) = eq_ix(v,w) andalso T=U 

547 
 (Bound i) aconv (Bound j) = i=j 

0  548 
 (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u andalso T=U 
2752  549 
 (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u) 
0  550 
 _ aconv _ = false; 
551 

2176  552 
(** Membership, insertion, union for terms **) 
553 

554 
fun mem_term (_, []) = false 

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

556 

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

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

558 
 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

559 

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

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

561 
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

562 

2176  563 
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; 
564 

565 
fun union_term (xs, []) = xs 

566 
 union_term ([], ys) = ys 

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

568 

5585  569 
fun inter_term ([], ys) = [] 
570 
 inter_term (x::xs, ys) = 

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

572 

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

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

576 
 aconvs _ = false; 

577 

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

581 
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

582 
 matchrands _ = true 
0  583 
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

584 
(_, Var _) => true 
0  585 
 (Var _, _) => true 
586 
 (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u) 

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

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

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

590 
 (_, Abs _) => true 

591 
 _ => false 

592 
end; 

593 

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

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

596 
 subst_free pairs = 

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

598 
case gen_assoc (op aconv) (pairs, u) of 
15531  599 
SOME u' => u' 
600 
 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

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

602 
 _ => u) 
0  603 
in substf end; 
604 

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

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

607 

608 

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

612 
fun abstract_over (v,body) = 

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

614 
(case u of 

615 
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

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

617 
 _ => u) 
0  618 
in abst(0,body) end; 
619 

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

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

0  623 

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

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

626 

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

628 
fun list_abs_free ([ ] , t) = t 

13000  629 
 list_abs_free ((a,T)::vars, t) = 
0  630 
absfree(a, T, list_abs_free(vars,t)); 
631 

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

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

13000  634 
 list_all_free ((a,T)::vars, t) = 
0  635 
(all T) $ (absfree(a, T, list_all_free(vars,t))); 
636 

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

638 
fun list_all ([], t) = t 

13000  639 
 list_all ((a,T)::vars, t) = 
0  640 
(all T) $ (Abs(a, T, list_all(vars,t))); 
641 

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

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

646 
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

647 
 subst (f$t') = subst f $ subst t' 
9721  648 
 subst t = if_none (assoc(instl,t)) t 
0  649 
in subst t end; 
650 

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

651 
(*Substitute for type Vars in a type*) 
0  652 
fun typ_subst_TVars iTs T = if null iTs then T else 
653 
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

654 
 subst(T as TFree _) = T 
9721  655 
 subst(T as TVar(ixn,_)) = if_none (assoc(iTs,ixn)) T 
0  656 
in subst T end; 
657 

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

658 
(*Substitute for type Vars in a term*) 
0  659 
val subst_TVars = map_term_types o typ_subst_TVars; 
660 

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

661 
(*Substitute for Vars in a term; see also envir/norm_term*) 
0  662 
fun subst_Vars itms t = if null itms then t else 
9721  663 
let fun subst(v as Var(ixn,_)) = if_none (assoc(itms,ixn)) v 
0  664 
 subst(Abs(a,T,t)) = Abs(a,T,subst t) 
665 
 subst(f$t) = subst f $ subst t 

666 
 subst(t) = t 

667 
in subst t end; 

668 

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

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

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

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

15531  674 
NONE => Var(ixn,typ_subst_TVars iTs T) 
675 
 SOME t => t) 

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

678 
 subst(f$t) = subst f $ subst t 

679 
in subst end; 

680 

681 

682 
(*Computing the maximum index of a typ*) 

2146  683 
fun maxidx_of_typ(Type(_,Ts)) = maxidx_of_typs Ts 
0  684 
 maxidx_of_typ(TFree _) = ~1 
2146  685 
 maxidx_of_typ(TVar((_,i),_)) = i 
686 
and maxidx_of_typs [] = ~1 

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

0  688 

689 

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

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

692 
 maxidx_of_term (Bound _) = ~1 

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

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

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

0  697 

13665  698 
fun maxidx_of_terms ts = foldl Int.max (~1, map maxidx_of_term ts); 
699 

0  700 

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

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

704 

705 
(**** Syntaxrelated declarations ****) 

706 

707 

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

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

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

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

713 
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

714 
raise TYPE ("Illegal occurrence of '_' dummy type", [T], []) 
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

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

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

717 
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

718 

0  719 

720 
(*** Printing ***) 

721 

14676  722 
(*Makes a variant of a name distinct from the names in bs. 
723 
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

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

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

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

727 
val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name)); 
12902  728 
fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_string c) else c; 
14676  729 
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

730 
in vary1 (if c = "" then "u" else c) ^ u end; 
0  731 

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

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

13000  734 
 variantlist(b::bs, used) = 
0  735 
let val b' = variant used b 
736 
in b' :: variantlist (bs, b'::used) end; 

737 

14695  738 
(*Invent fresh names*) 
739 
fun invent_names _ _ 0 = [] 

740 
 invent_names used a n = 

741 
let val b = Symbol.bump_string a in 

742 
if a mem_string used then invent_names used b n 

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

744 
end; 

11353  745 

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

746 

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

747 

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

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

749 

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

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

751 
 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

752 
 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

753 

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

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

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

756 

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

757 
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

758 
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

759 

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

761 
 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

762 
 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

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

764 

13646  765 
fun term_consts t = add_term_consts(t,[]); 
766 

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

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

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

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

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

773 

4631  774 
fun exists_subterm P = 
775 
let fun ex t = P t orelse 

776 
(case t of 

777 
u $ v => ex u orelse ex v 

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

779 
 _ => false) 

780 
in ex end; 

781 

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

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

783 
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

784 
 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

785 
 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

786 

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

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

788 
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

789 
 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

790 
 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

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

792 
 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

793 
 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

794 

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

795 

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

796 

0  797 
(** TFrees and TVars **) 
798 

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

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

801 

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

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

803 
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

804 
 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

805 
 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

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

807 

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

10666  810 
fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs 
2176  811 
 add_term_names (Free(a,_), bs) = a ins_string bs 
0  812 
 add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) 
813 
 add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) 

814 
 add_term_names (_, bs) = bs; 

815 

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

817 
fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars (Ts,vs) 

818 
 add_typ_tvars(TFree(_),vs) = vs 

819 
 add_typ_tvars(TVar(v),vs) = v ins vs; 

820 

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

822 
fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names (Ts,fs) 

2176  823 
 add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs 
0  824 
 add_typ_tfree_names(TVar(_),fs) = fs; 
825 

826 
fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees (Ts,fs) 

827 
 add_typ_tfrees(TFree(f),fs) = f ins fs 

828 
 add_typ_tfrees(TVar(_),fs) = fs; 

829 

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

830 
fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames (Ts,nms) 
2176  831 
 add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms 
832 
 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

833 

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

836 

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

838 
val add_term_tfrees = it_term_types add_typ_tfrees; 

839 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

840 

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

841 
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

842 

0  843 
(*Nonlist versions*) 
844 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

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

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

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

848 

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

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

850 

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

851 
fun add_typ_ixns(ixns,Type(_,Ts)) = foldl add_typ_ixns (ixns,Ts) 
13000  852 
 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

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

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

855 

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

856 
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

857 
 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

858 
 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

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

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

861 
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

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

863 
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

864 

0  865 
(** Frees and Vars **) 
866 

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

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

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

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

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

872 
 atless _ = false; 

873 

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

875 
fun insert_aterm (t,us) = 

876 
let fun inserta [] = [t] 

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

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

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

880 
else u :: inserta(us') 
0  881 
in inserta us end; 
882 

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

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

885 
Var _ => insert_aterm(t,vars) 

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

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

888 
 _ => vars; 

889 

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

891 

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

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

894 
Free _ => insert_aterm(t,frees) 

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

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

897 
 _ => frees; 

898 

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

900 

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

902 
having a unique name. *) 

903 
fun variant_abs (a,T,P) = 

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

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

905 
in (b, subst_bound (Free(b,T), P)) end; 
0  906 

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

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

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

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

910 
(variant (map #1 vars @ names) a, T) :: vars 
0  911 
in foldl rename_aT ([],vars) end; 
912 

913 
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

914 

1417  915 

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

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

917 

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

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

919 
fun foldl_atyps f (x, Type (_, Ts)) = foldl (foldl_atyps f) (x, Ts) 
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

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

921 

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

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

923 
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

924 
 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

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

926 

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

927 
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

928 
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

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

930 
 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

931 
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

932 
 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

933 

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

934 
(*foldl types of term*) 
8609  935 
fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T) 
936 
 foldl_term_types f (x, t as Free (_, T)) = f t (x, T) 

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

938 
 foldl_term_types f (x, Bound _) = x 

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

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

941 

942 
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

943 

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

946 
val add_tvars = foldl_types add_tvarsT; 

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

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

949 

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

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

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

953 

1417  954 

4444  955 
(** type and term orders **) 
956 

957 
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

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

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

960 
val sort_ord = list_ord String.compare; 
13000  961 

4444  962 

963 
(* typ_ord *) 

964 

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

965 
fun typ_ord (Type x, Type y) = prod_ord String.compare typs_ord (x, y) 
4444  966 
 typ_ord (Type _, _) = GREATER 
967 
 typ_ord (TFree _, Type _) = LESS 

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

968 
 typ_ord (TFree x, TFree y) = prod_ord String.compare sort_ord (x, y) 
4444  969 
 typ_ord (TFree _, TVar _) = GREATER 
970 
 typ_ord (TVar _, Type _) = LESS 

971 
 typ_ord (TVar _, TFree _) = LESS 

13000  972 
 typ_ord (TVar x, TVar y) = prod_ord indexname_ord sort_ord (x, y) 
4444  973 
and typs_ord Ts_Us = list_ord typ_ord Ts_Us; 
974 

975 

976 
(* term_ord *) 

977 

978 
(*a linear wellfounded ACcompatible ordering for terms: 

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

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

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

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

983 

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

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

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

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

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

989 

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

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

992 
 term_ord (t, u) = 

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

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

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

997 
end 

998 
 ord => ord) 

999 
and hd_ord (f, g) = 

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

1000 
prod_ord (prod_ord indexname_ord typ_ord) Int.compare (dest_hd f, dest_hd g) 
4444  1001 
and terms_ord (ts, us) = list_ord term_ord (ts, us); 
1002 

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

1004 

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

1005 
structure Vartab = TableFun(type key = indexname val ord = indexname_ord); 
13000  1006 
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

1007 
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

1008 

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

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

1010 
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

1011 
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

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

1013 
 subst(T as TVar(ixn, _)) = 
15531  1014 
(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

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

1016 

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

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

1018 
val subst_TVars_Vartab = map_term_types o typ_subst_TVars_Vartab; 
4444  1019 

1020 

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

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

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

1417  1025 

1026 
(** Sharing of types **) 

1027 

13000  1028 
val memo_types = ref (Typtab.empty: typ Typtab.table); 
1417  1029 

1030 
fun compress_type T = 

13000  1031 
(case Typtab.lookup (! memo_types, T) of 
15531  1032 
SOME T' => T' 
1033 
 NONE => 

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

1036 

1417  1037 

1038 
(** Sharing of atomic terms **) 

1039 

13000  1040 
val memo_terms = ref (Termtab.empty : term Termtab.table); 
1417  1041 

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

13000  1043 
 share_term (Abs (a, T, u)) = Abs (a, T, share_term u) 
1417  1044 
 share_term t = 
13000  1045 
(case Termtab.lookup (! memo_terms, t) of 
15531  1046 
SOME t' => t' 
1047 
 NONE => (memo_terms := Termtab.update ((t, t), ! memo_terms); t)); 

1417  1048 

1049 
val compress_term = share_term o map_term_types compress_type; 

1050 

4444  1051 

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

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

1053 

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

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

1055 

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

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

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

1058 

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

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

1060 
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

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

1062 

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

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

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

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

1068 
 replace_dummy Ts (i, t $ u) = 

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

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

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

1072 

1073 
val replace_dummy_patterns = replace_dummy []; 

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

1074 

10552  1075 
fun is_replaced_dummy_pattern ("_dummy_", _) = true 
1076 
 is_replaced_dummy_pattern _ = false; 

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

1077 

13484  1078 

1079 
(* adhoc freezing *) 

1080 

1081 
fun adhoc_freeze_vars tm = 

1082 
let 

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

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

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

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

1087 
in (subst_atomic insts tm, xs) end; 

1088 

1089 

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

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

1091 

15472  1092 
val show_var_qmarks = ref true; 
1093 

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

1094 
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

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

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

1097 
val dot = if_none (try (Symbol.is_digit o last_elem o Symbol.explode) x) true; 
15472  1098 
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

1099 
in 
15472  1100 
if dot then qmark ^ x ^ "." ^ si 
1101 
else if i = 0 then qmark ^ x 

1102 
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

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

1104 

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

1105 
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

1106 
 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

1107 

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

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

1109 

4444  1110 
structure BasicTerm: BASIC_TERM = Term; 
1111 
open BasicTerm; 