author  nipkow 
Thu, 17 Mar 2005 12:19:50 +0100  
changeset 15612  431b281078b3 
parent 15598  4ab52355bb53 
child 15632  bb178a7a69c1 
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 

15598
4ab52355bb53
Registrations of global locale interpretations: improved, better naming.
ballarin
parents:
15574
diff
changeset

136 
(* note reversed order of args wrt. variant! *) 
4444  137 
val variant_abs: string * typ * term > string * term 
138 
val rename_wrt_term: term > (string * typ) list > (string * typ) list 

139 
val add_new_id: string list * string > string list 

140 
val add_typ_classes: typ * class list > class list 

141 
val add_typ_ixns: indexname list * typ > indexname list 

142 
val add_typ_tfree_names: typ * string list > string list 

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

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

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

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

147 
val add_typ_tycons: typ * string list > string list 

148 
val add_typ_varnames: typ * string list > string list 

149 
val add_term_classes: term * class list > class list 

150 
val add_term_consts: term * string list > string list 

13646  151 
val term_consts: term > string list 
4444  152 
val add_term_frees: term * term list > term list 
153 
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

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

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

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

159 
val add_term_tvar_ixns: term * indexname list > indexname list 

160 
val add_term_tvarnames: term * string list > string list 

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

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

163 
val add_term_tycons: term * string list > string list 

164 
val add_term_vars: term * term list > term list 

165 
val term_vars: term > term list 

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

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

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

4444  173 
signature TERM = 
174 
sig 

175 
include BASIC_TERM 

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

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

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

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

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

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

185 
val typs_ord: typ list * typ list > order 

186 
val term_ord: term * term > order 

187 
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

188 
val hd_ord: term * term > order 
4444  189 
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

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

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

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

193 
val replace_dummy_patterns: int * term > int * term 
10552  194 
val is_replaced_dummy_pattern: indexname > bool 
13484  195 
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

196 
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

197 
val string_of_vname': indexname > string 
15612  198 
val string_of_term: term > string 
4444  199 
end; 
200 

201 
structure Term: TERM = 

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

202 
struct 
0  203 

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

205 
for resolution.*) 

206 
type indexname = string*int; 

207 

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

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

211 
type arity = string * sort list * sort; 
0  212 

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

214 
datatype typ = Type of string * typ list 

215 
 TFree of string * sort 

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

216 
 TVar of indexname * sort; 
0  217 

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

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

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

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

225 

226 

227 

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

233 
 Abs of string*typ*term 

3965  234 
 op $ of term*term; 
0  235 

236 

237 
(*For errors involving type mismatches*) 

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

239 

240 
(*For system errors involving terms*) 

241 
exception TERM of string * term list; 

242 

243 

244 
(*Note variable naming conventions! 

245 
a,b,c: string 

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

247 
i,j,m,n: int 

248 
t,u: term 

249 
v,w: indexnames 

250 
x,y: any 

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

252 
T,U: typ 

253 
*) 

254 

255 

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

256 
(** Types **) 
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 
fun S > T = Type("fun",[S,T]); 
c8c69a4a7762
moved dest_Type to term.ML from HOL/Tools/primrec_package
paulson
parents:
5986
diff
changeset

259 

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

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

262 

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

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

264 
 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

265 

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

266 

0  267 
(** Discriminators **) 
268 

7318  269 
fun is_Bound (Bound _) = true 
270 
 is_Bound _ = false; 

271 

0  272 
fun is_Const (Const _) = true 
273 
 is_Const _ = false; 

274 

275 
fun is_Free (Free _) = true 

276 
 is_Free _ = false; 

277 

278 
fun is_Var (Var _) = true 

279 
 is_Var _ = false; 

280 

281 
fun is_TVar (TVar _) = true 

282 
 is_TVar _ = false; 

283 

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

286 
 is_funtype _ = false; 

287 

0  288 
(** Destructors **) 
289 

290 
fun dest_Const (Const x) = x 

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

292 

293 
fun dest_Free (Free x) = x 

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

295 

296 
fun dest_Var (Var x) = x 

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

298 

299 

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

4064  302 

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

305 
 binder_types _ = []; 

306 

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

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

309 
 body_type T = T; 

310 

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

312 
fun strip_type T : typ list * typ = 

313 
(binder_types T, body_type T); 

314 

315 

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

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

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

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

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

0  322 
 type_of1 (Ts, Var (_,T)) = T 
323 
 type_of1 (Ts, Abs (_,T,body)) = T > type_of1(T::Ts, body) 

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

327 
in case T of 

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

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

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

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

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

333 
[T,U], [f$u]) 
0  334 
end; 
335 

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

337 

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

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

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

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

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

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

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

0  351 

352 

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

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

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

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

363 

364 
fun strip_qnt_body qnt = 

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

366 
 strip t = t 

367 
in strip end; 

368 

369 
fun strip_qnt_vars qnt = 

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

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

372 
in strip end; 

373 

374 

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

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

378 

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

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

385 

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

387 
fun head_of (f$t) = head_of f 

388 
 head_of u = u; 

389 

390 

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

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

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

394 
 size_of_term _ = 1; 

395 

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

396 
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

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

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

399 

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

400 
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

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

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

403 

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

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

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

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

409 
 map(t as Bound _) = t 

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

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

412 
in map end; 

413 

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

415 
fun it_term_types f = 

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

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

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

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

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

421 
 iter(Bound _, a) = a 

422 
in iter end 

423 

424 

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

426 

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

0  430 
val propT : typ = Type("prop",[]); 
431 

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

433 

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

435 

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

437 

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

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

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

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

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

447 
(*increments a term's nonlocal bound variables 

448 
required when moving a term within abstractions 

449 
inc is increment for bound variables 

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

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

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

457 

458 
fun incr_boundvars 0 t = t 

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

460 

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

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

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

465 
else (x,y)::al) 

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

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

468 

469 
(* strip abstractions created by parameters *) 

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

471 

472 
fun rename_abs pat obj t = 

473 
let 

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

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

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

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

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

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

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

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

13000  487 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
0  488 
 add_loose_bnos (_, _, js) = js; 
489 

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

491 

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

493 
level k or beyond. *) 

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

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

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

497 
 loose_bvar _ = false; 

498 

2792  499 
fun loose_bvar1(Bound i,k) = i = k 
500 
 loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 

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

502 
 loose_bvar1 _ = false; 

0  503 

504 
(*Substitute arguments for loose bound variables. 

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

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

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

510 
*) 

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

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

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

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

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

517 
 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

518 
 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

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

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

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

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

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

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

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

528 
 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

529 
 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

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

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

532 

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

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

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

537 

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

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

539 

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

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

542 

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

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

545 
 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

546 

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

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

548 
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

549 

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

555 
 (Bound i) aconv (Bound j) = i=j 

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

2176  560 
(** Membership, insertion, union for terms **) 
561 

562 
fun mem_term (_, []) = false 

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

564 

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

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

566 
 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

567 

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

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

569 
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

570 

2176  571 
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; 
572 

573 
fun union_term (xs, []) = xs 

574 
 union_term ([], ys) = ys 

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

576 

5585  577 
fun inter_term ([], ys) = [] 
578 
 inter_term (x::xs, ys) = 

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

580 

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

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

584 
 aconvs _ = false; 

585 

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

589 
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

590 
 matchrands _ = true 
0  591 
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

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

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

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

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

598 
 (_, Abs _) => true 

599 
 _ => false 

600 
end; 

601 

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

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

604 
 subst_free pairs = 

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

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

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

610 
 _ => u) 
0  611 
in substf end; 
612 

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

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

615 

616 

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

620 
fun abstract_over (v,body) = 

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

622 
(case u of 

623 
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

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

625 
 _ => u) 
0  626 
in abst(0,body) end; 
627 

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

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

0  631 

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

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

634 

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

636 
fun list_abs_free ([ ] , t) = t 

13000  637 
 list_abs_free ((a,T)::vars, t) = 
0  638 
absfree(a, T, list_abs_free(vars,t)); 
639 

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

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

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

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

646 
fun list_all ([], t) = t 

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

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

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

654 
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

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

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

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

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

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

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

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

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

674 
 subst(t) = t 

675 
in subst t end; 

676 

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

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

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

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

15531  682 
NONE => Var(ixn,typ_subst_TVars iTs T) 
683 
 SOME t => t) 

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

686 
 subst(f$t) = subst f $ subst t 

687 
in subst end; 

688 

689 

15573  690 
(** Identifying firstorder terms **) 
691 

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

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

694 

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

696 
type.*) 

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

698 
 first_order1 Ts t = 

699 
case strip_comb t of 

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

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

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

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

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

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

706 

707 
val is_first_order = first_order1 []; 

708 

709 

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

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

0  716 

717 

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

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

720 
 maxidx_of_term (Bound _) = ~1 

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

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

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

0  725 

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

0  728 

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

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

732 

733 
(**** Syntaxrelated declarations ****) 

734 

735 

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

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

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

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

741 
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

742 
raise TYPE ("Illegal occurrence of '_' dummy type", [T], []) 
15570  743 
 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

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

745 
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

746 

0  747 

748 
(*** Printing ***) 

749 

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

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

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

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

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

758 
in vary1 (if c = "" then "u" else c) ^ u end; 
0  759 

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

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

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

765 

14695  766 
(*Invent fresh names*) 
767 
fun invent_names _ _ 0 = [] 

768 
 invent_names used a n = 

769 
let val b = Symbol.bump_string a in 

770 
if a mem_string used then invent_names used b n 

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

772 
end; 

11353  773 

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

774 

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

775 

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

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

777 

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

778 
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

779 
 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

780 
 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

781 

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

782 
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

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

784 

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

785 
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

786 
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

787 

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

789 
 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

790 
 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

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

792 

13646  793 
fun term_consts t = add_term_consts(t,[]); 
794 

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

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

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

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

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

801 

4631  802 
fun exists_subterm P = 
803 
let fun ex t = P t orelse 

804 
(case t of 

805 
u $ v => ex u orelse ex v 

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

807 
 _ => false) 

808 
in ex end; 

809 

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

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

811 
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

812 
 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

813 
 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

814 

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

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

816 
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

817 
 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

818 
 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

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

820 
 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

821 
 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

822 

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

823 

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

824 

0  825 
(** TFrees and TVars **) 
826 

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

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

829 

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

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

831 
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

832 
 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

833 
 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

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

835 

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

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

842 
 add_term_names (_, bs) = bs; 

843 

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

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

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

848 

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

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

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

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

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

857 

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

858 
fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts 
2176  859 
 add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms 
860 
 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

861 

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

864 

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

866 
val add_term_tfrees = it_term_types add_typ_tfrees; 

867 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

868 

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

869 
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

870 

0  871 
(*Nonlist versions*) 
872 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

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

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

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

876 

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

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

878 

15570  879 
fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts) 
13000  880 
 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

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

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

883 

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

884 
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

885 
 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

886 
 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

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

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

889 
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

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

891 
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

892 

0  893 
(** Frees and Vars **) 
894 

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

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

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

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

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

900 
 atless _ = false; 

901 

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

903 
fun insert_aterm (t,us) = 

904 
let fun inserta [] = [t] 

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

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

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

908 
else u :: inserta(us') 
0  909 
in inserta us end; 
910 

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

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

913 
Var _ => insert_aterm(t,vars) 

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

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

916 
 _ => vars; 

917 

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

919 

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

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

922 
Free _ => insert_aterm(t,frees) 

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

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

925 
 _ => frees; 

926 

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

928 

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

930 
having a unique name. *) 

931 
fun variant_abs (a,T,P) = 

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

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

933 
in (b, subst_bound (Free(b,T), P)) end; 
0  934 

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

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

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

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

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

941 
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

942 

1417  943 

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

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

945 

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

946 
(*foldl atoms of type*) 
15570  947 
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

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

949 

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

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

951 
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

952 
 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

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

954 

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

955 
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

956 
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

957 
in (x'', t' $ u') 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, Abs (a, T, t)) = 
9b108dd75c25
val foldl_map_aterms: ('a * term > 'a * term) > 'a * term > 'a * term;
wenzelm
parents:
6033
diff
changeset

959 
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

960 
 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

961 

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

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

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

966 
 foldl_term_types f (x, Bound _) = x 

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

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

969 

970 
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

971 

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

974 
val add_tvars = foldl_types add_tvarsT; 

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

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

977 

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

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

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

981 

1417  982 

4444  983 
(** type and term orders **) 
984 

985 
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

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

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

988 
val sort_ord = list_ord String.compare; 
13000  989 

4444  990 

991 
(* typ_ord *) 

992 

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

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

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

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

999 
 typ_ord (TVar _, TFree _) = LESS 

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

1003 

1004 
(* term_ord *) 

1005 

1006 
(*a linear wellfounded ACcompatible ordering for terms: 

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

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

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

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

1011 

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

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

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

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

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

1017 

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

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

1020 
 term_ord (t, u) = 

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

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

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

1025 
end 

1026 
 ord => ord) 

1027 
and hd_ord (f, g) = 

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

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

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

1032 

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

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

1035 
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

1036 

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

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

1038 
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

1039 
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

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

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

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

1044 

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

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

1046 
val subst_TVars_Vartab = map_term_types o typ_subst_TVars_Vartab; 
4444  1047 

1048 

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

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

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

1417  1053 

1054 
(** Sharing of types **) 

1055 

13000  1056 
val memo_types = ref (Typtab.empty: typ Typtab.table); 
1417  1057 

1058 
fun compress_type T = 

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

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

1064 

1417  1065 

1066 
(** Sharing of atomic terms **) 

1067 

13000  1068 
val memo_terms = ref (Termtab.empty : term Termtab.table); 
1417  1069 

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

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

1417  1076 

1077 
val compress_term = share_term o map_term_types compress_type; 

1078 

4444  1079 

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

1080 
(* dummy patterns *) 
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 
val dummy_patternN = "dummy_pattern"; 
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

1083 

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

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

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

1086 

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

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

1088 
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

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

1090 

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

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

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

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

1096 
 replace_dummy Ts (i, t $ u) = 

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

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

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

1100 

1101 
val replace_dummy_patterns = replace_dummy []; 

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

1102 

10552  1103 
fun is_replaced_dummy_pattern ("_dummy_", _) = true 
1104 
 is_replaced_dummy_pattern _ = false; 

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

1105 

13484  1106 

1107 
(* adhoc freezing *) 

1108 

1109 
fun adhoc_freeze_vars tm = 

1110 
let 

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

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

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

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

1115 
in (subst_atomic insts tm, xs) end; 

1116 

1117 

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

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

1119 

15472  1120 
val show_var_qmarks = ref true; 
1121 

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

1122 
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

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

1124 
val si = string_of_int i; 
15570  1125 
val dot = getOpt (try (Symbol.is_digit o List.last o Symbol.explode) x, true); 
15472  1126 
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

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

1130 
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

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

1132 

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

1133 
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

1134 
 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

1135 

15612  1136 
fun string_of_term (Const(s,_)) = s 
1137 
 string_of_term (Free(s,_)) = s 

1138 
 string_of_term (Var(ix,_)) = string_of_vname ix 

1139 
 string_of_term (Bound i) = string_of_int i 

1140 
 string_of_term (Abs(x,_,t)) = "%" ^ x ^ ". " ^ string_of_term t 

1141 
 string_of_term (s $ t) = 

1142 
"(" ^ string_of_term s ^ " " ^ string_of_term t ^ ")" 

1143 

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

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

1145 

4444  1146 
structure BasicTerm: BASIC_TERM = Term; 
1147 
open BasicTerm; 