author  wenzelm 
Thu, 10 Nov 2005 20:57:19 +0100  
changeset 18149  c6899e23b5ff 
parent 18131  8c3089df74ba 
child 18183  a9f67248996a 
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 

16537  24 
datatype term = 
25 
Const of string * typ  

26 
Free of string * typ  

27 
Var of indexname * typ  

28 
Bound of int  

29 
Abs of string * typ * term  

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

16710  33 
val dummyT: typ 
34 
val no_dummyT: typ > typ 

4444  35 
val > : typ * typ > typ 
36 
val > : typ list * typ > typ 

16710  37 
val dest_Type: typ > string * typ list 
38 
val dest_TVar: typ > indexname * sort 

39 
val dest_TFree: typ > string * sort 

40 
val is_Bound: term > bool 

41 
val is_Const: term > bool 

42 
val is_Free: term > bool 

43 
val is_Var: term > bool 

4444  44 
val is_TVar: typ > bool 
15573  45 
val is_funtype: typ > bool 
16710  46 
val dest_Const: term > string * typ 
47 
val dest_Free: term > string * typ 

48 
val dest_Var: term > indexname * typ 

4444  49 
val domain_type: typ > typ 
4480  50 
val range_type: typ > typ 
4444  51 
val binder_types: typ > typ list 
52 
val body_type: typ > typ 

53 
val strip_type: typ > typ list * typ 

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

16943  71 
val fold_atyps: (typ > 'a > 'a) > typ > 'a > 'a 
72 
val fold_aterms: (term > 'a > 'a) > term > 'a > 'a 

73 
val fold_term_types: (term > typ > 'a > 'a) > term > 'a > 'a 

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

75 
val add_term_names: term * string list > string list 

76 
val add_term_varnames: term > indexname list > indexname list 

77 
val term_varnames: term > indexname list 

18149  78 
val find_free: term > string > term option 
16710  79 
val aconv: term * term > bool 
80 
val aconvs: term list * term list > bool 

16537  81 
structure Vartab: TABLE 
82 
structure Typtab: TABLE 

83 
structure Termtab: TABLE 

4444  84 
val itselfT: typ > typ 
85 
val a_itselfT: typ 

86 
val propT: typ 

87 
val implies: term 

88 
val all: typ > term 

89 
val equals: typ > term 

90 
val strip_all_body: term > term 

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

92 
val incr_bv: int * int * term > term 

93 
val incr_boundvars: int > term > term 

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

95 
val loose_bnos: term > int list 

96 
val loose_bvar: term * int > bool 

97 
val loose_bvar1: term * int > bool 

98 
val subst_bounds: term list * term > term 

99 
val subst_bound: term * term > term 

100 
val betapply: term * term > term 

101 
val eq_ix: indexname * indexname > bool 

102 
val ins_ix: indexname * indexname list > indexname list 

103 
val mem_ix: indexname * indexname list > bool 

104 
val mem_term: term * term list > bool 

105 
val ins_term: term * term list > term list 

106 
val could_unify: term * term > bool 

107 
val subst_free: (term * term) list > term > term 

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

109 
val abstract_over: term * term > term 

11922  110 
val lambda: term > term > term 
4444  111 
val absfree: string * typ * term > term 
17786  112 
val absdummy: typ * term > term 
4444  113 
val list_abs_free: (string * typ) list * term > term 
114 
val list_all_free: (string * typ) list * term > term 

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

16710  116 
val subst_atomic: (term * term) list > term > term 
117 
val typ_subst_atomic: (typ * typ) list > typ > typ 

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

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

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

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

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

123 
val is_first_order: string list > term > bool 

4444  124 
val maxidx_of_typ: typ > int 
125 
val maxidx_of_typs: typ list > int 

126 
val maxidx_of_term: term > int 

127 
val variant: string list > string > string 

128 
val variantlist: string list * string list > string list 

16537  129 
(*note reversed order of args wrt. variant!*) 
4444  130 
val add_typ_classes: typ * class list > class list 
131 
val add_typ_tycons: typ * string list > string list 

132 
val add_term_classes: term * class list > class list 

16710  133 
val add_term_tycons: term * string list > string list 
4444  134 
val add_term_consts: term * string list > string list 
13646  135 
val term_consts: term > string list 
16943  136 
val exists_subterm: (term > bool) > term > bool 
16710  137 
val exists_Const: (string * typ > bool) > term > bool 
138 
val add_term_free_names: term * string list > string list 

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

140 
val add_typ_tfree_names: typ * string list > string list 

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

142 
val add_typ_varnames: typ * string list > string list 

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

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

145 
val add_term_tfree_names: term * string list > string list 

146 
val add_term_tvarnames: term * string list > string list 

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

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

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

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

151 
val add_typ_ixns: indexname list * typ > indexname list 

152 
val add_term_tvar_ixns: term * indexname list > indexname list 

153 
val add_term_vars: term * term list > term list 

154 
val term_vars: term > term list 

4444  155 
val add_term_frees: term * term list > term list 
156 
val term_frees: term > term list 

16710  157 
val variant_abs: string * typ * term > string * term 
158 
val rename_wrt_term: term > (string * typ) list > (string * typ) list 

15986  159 
val show_question_marks: bool ref 
4444  160 
end; 
0  161 

4444  162 
signature TERM = 
163 
sig 

164 
include BASIC_TERM 

16710  165 
val argument_type_of: term > typ 
16943  166 
val add_tvarsT: typ > (indexname * sort) list > (indexname * sort) list 
167 
val add_tvars: term > (indexname * sort) list > (indexname * sort) list 

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

169 
val add_tfreesT: typ > (string * sort) list > (string * sort) list 

170 
val add_tfrees: term > (string * sort) list > (string * sort) list 

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

16678  172 
val fast_indexname_ord: indexname * indexname > order 
16537  173 
val indexname_ord: indexname * indexname > order 
174 
val sort_ord: sort * sort > order 

175 
val typ_ord: typ * typ > order 

16678  176 
val fast_term_ord: term * term > order 
16537  177 
val term_ord: term * term > order 
178 
val hd_ord: term * term > order 

179 
val termless: term * term > bool 

16570  180 
val term_lpo: (string > int) > term * term > order 
12981  181 
val match_bvars: (term * term) * (string * string) list > (string * string) list 
182 
val rename_abs: term > term > term > term option 

16943  183 
val eq_tvar: (indexname * sort) * (indexname * sort) > bool 
16882  184 
val eq_var: (indexname * typ) * (indexname * typ) > bool 
16943  185 
val tvar_ord: (indexname * sort) * (indexname * sort) > order 
186 
val var_ord: (indexname * typ) * (indexname * typ) > order 

16882  187 
val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list 
188 
> term > term 

189 
val instantiateT: ((indexname * sort) * typ) list > typ > typ 

16710  190 
val maxidx_typ: typ > int > int 
191 
val maxidx_typs: typ list > int > int 

192 
val maxidx_term: term > int > int 

12499  193 
val invent_names: string list > string > int > string list 
16338  194 
val map_typ: (string > string) > (string > string) > typ > typ 
195 
val map_term: (string > string) > (string > string) > (string > string) > term > term 

16710  196 
val dest_abs: string * typ * term > string * term 
16990  197 
val bound: int > string 
198 
val is_bound: string > bool 

16943  199 
val zero_var_indexesT: typ > typ 
200 
val zero_var_indexes: term > term 

201 
val zero_var_indexes_inst: term > 

202 
((indexname * sort) * typ) list * ((indexname * typ) * term) list 

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

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

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

205 
val replace_dummy_patterns: int * term > int * term 
10552  206 
val is_replaced_dummy_pattern: indexname > bool 
16035  207 
val show_dummy_patterns: term > term 
13484  208 
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

209 
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

210 
val string_of_vname': indexname > string 
17777
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

211 
val str_of_term: term > string 
4444  212 
end; 
213 

214 
structure Term: TERM = 

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

215 
struct 
0  216 

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

218 
for resolution.*) 

16537  219 
type indexname = string * int; 
0  220 

4626  221 
(* Types are classified by sorts. *) 
0  222 
type class = string; 
223 
type sort = class list; 

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

224 
type arity = string * sort list * sort; 
0  225 

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

227 
datatype typ = Type of string * typ list 

228 
 TFree of string * sort 

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

229 
 TVar of indexname * sort; 
0  230 

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

231 
(*Terms. Bound variables are indicated by depth number. 
0  232 
Free variables, (scheme) variables and constants have names. 
4626  233 
An term is "closed" if every bound variable of level "lev" 
13000  234 
is enclosed by at least "lev" abstractions. 
0  235 

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

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

238 

13000  239 
datatype term = 
0  240 
Const of string * typ 
13000  241 
 Free of string * typ 
0  242 
 Var of indexname * typ 
243 
 Bound of int 

244 
 Abs of string*typ*term 

3965  245 
 op $ of term*term; 
0  246 

16537  247 
(*Errors involving type mismatches*) 
0  248 
exception TYPE of string * typ list * term list; 
249 

16537  250 
(*Errors errors involving terms*) 
0  251 
exception TERM of string * term list; 
252 

253 
(*Note variable naming conventions! 

254 
a,b,c: string 

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

256 
i,j,m,n: int 

257 
t,u: term 

258 
v,w: indexnames 

259 
x,y: any 

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

261 
T,U: typ 

262 
*) 

263 

264 

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

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

266 

16537  267 
(*dummy type for parsing and printing etc.*) 
268 
val dummyT = Type ("dummy", []); 

269 

270 
fun no_dummyT typ = 

271 
let 

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

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

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

275 
 check _ = (); 

276 
in check typ; typ end; 

277 

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

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

279 

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

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

282 

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

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

284 
 dest_Type T = raise TYPE ("dest_Type", [T], []); 
15914  285 
fun dest_TVar (TVar x) = x 
286 
 dest_TVar T = raise TYPE ("dest_TVar", [T], []); 

287 
fun dest_TFree (TFree x) = x 

288 
 dest_TFree T = raise TYPE ("dest_TFree", [T], []); 

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

289 

16537  290 

0  291 
(** Discriminators **) 
292 

7318  293 
fun is_Bound (Bound _) = true 
294 
 is_Bound _ = false; 

295 

0  296 
fun is_Const (Const _) = true 
297 
 is_Const _ = false; 

298 

299 
fun is_Free (Free _) = true 

300 
 is_Free _ = false; 

301 

302 
fun is_Var (Var _) = true 

303 
 is_Var _ = false; 

304 

305 
fun is_TVar (TVar _) = true 

306 
 is_TVar _ = false; 

307 

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

310 
 is_funtype _ = false; 

311 

16537  312 

0  313 
(** Destructors **) 
314 

315 
fun dest_Const (Const x) = x 

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

317 

318 
fun dest_Free (Free x) = x 

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

320 

321 
fun dest_Var (Var x) = x 

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

323 

324 

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

4064  327 

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

330 
 binder_types _ = []; 

331 

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

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

334 
 body_type T = T; 

335 

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

337 
fun strip_type T : typ list * typ = 

338 
(binder_types T, body_type T); 

339 

340 

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

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

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

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

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

0  347 
 type_of1 (Ts, Var (_,T)) = T 
348 
 type_of1 (Ts, Abs (_,T,body)) = T > type_of1(T::Ts, body) 

13000  349 
 type_of1 (Ts, f$u) = 
0  350 
let val U = type_of1(Ts,u) 
351 
and T = type_of1(Ts,f) 

352 
in case T of 

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

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

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

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

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

358 
[T,U], [f$u]) 
0  359 
end; 
360 

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

362 

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

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

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

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

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

13000  372 
 fastype_of1 (_, Var (_,T)) = T 
61  373 
 fastype_of1 (Ts, Abs (_,T,u)) = T > fastype_of1 (T::Ts, u); 
374 

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

0  376 

16678  377 
(*Determine the argument type of a function*) 
378 
fun argument_type_of tm = 

379 
let 

380 
fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i  1) U 

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

382 

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

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

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

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

387 
in arg 0 [] tm end; 

388 

0  389 

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

0  392 
(* maps (x1,...,xn)t to t *) 
13000  393 
fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t 
0  394 
 strip_abs_body u = u; 
395 

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

13000  397 
fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t 
0  398 
 strip_abs_vars u = [] : (string*typ) list; 
399 

400 

401 
fun strip_qnt_body qnt = 

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

403 
 strip t = t 

404 
in strip end; 

405 

406 
fun strip_qnt_vars qnt = 

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

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

409 
in strip end; 

410 

411 

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

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

415 

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

13000  417 
fun strip_comb u : term * term list = 
0  418 
let fun stripc (f$t, ts) = stripc (f, t::ts) 
13000  419 
 stripc x = x 
0  420 
in stripc(u,[]) end; 
421 

422 

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

424 
fun head_of (f$t) = head_of f 

425 
 head_of u = u; 

426 

427 

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

430 
let 

16678  431 
fun add_size (t $ u, n) = add_size (t, add_size (u, n)) 
432 
 add_size (Abs (_ ,_, t), n) = add_size (t, n + 1) 

433 
 add_size (_, n) = n + 1; 

434 
in add_size (tm, 0) end; 

0  435 

16678  436 
fun map_type_tvar f = 
437 
let 

438 
fun map_aux (Type (a, Ts)) = Type (a, map map_aux Ts) 

439 
 map_aux (TVar x) = f x 

440 
 map_aux T = T; 

441 
in map_aux end; 

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

442 

16678  443 
fun map_type_tfree f = 
444 
let 

445 
fun map_aux (Type (a, Ts)) = Type (a, map map_aux Ts) 

446 
 map_aux (TFree x) = f x 

447 
 map_aux T = T; 

448 
in map_aux end; 

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

449 

0  450 
fun map_term_types f = 
16678  451 
let 
452 
fun map_aux (Const (a, T)) = Const (a, f T) 

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

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

455 
 map_aux (t as Bound _) = t 

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

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

458 
in map_aux end; 

0  459 

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

461 
fun it_term_types f = 

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

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

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

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

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

467 
 iter(Bound _, a) = a 

468 
in iter end 

469 

470 

16943  471 
(* fold types and terms *) 
472 

473 
(*fold atoms of type*) 

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

475 
 fold_atyps f T = f T; 

476 

477 
(*fold atoms of term*) 

478 
fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u 

479 
 fold_aterms f (Abs (_, _, t)) = fold_aterms f t 

480 
 fold_aterms f a = f a; 

481 

482 
(*fold types of term*) 

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

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

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

486 
 fold_term_types f (Bound _) = I 

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

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

489 

490 
fun fold_types f = fold_term_types (K f); 

491 

492 
(*collect variables*) 

493 
val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v  _ => I); 

494 
val add_tvars = fold_types add_tvarsT; 

495 
val add_vars = fold_aterms (fn Var v => insert (op =) v  _ => I); 

496 
val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v  _ => I); 

497 
val add_tfrees = fold_types add_tfreesT; 

498 
val add_frees = fold_aterms (fn Free v => insert (op =) v  _ => I); 

499 

500 
(*collect variable names*) 

501 
val add_term_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi  _ => I); 

502 
fun term_varnames t = add_term_varnames t []; 

503 

18149  504 
fun find_free t x = 
505 
let 

506 
exception Found of term; 

507 
fun find (t as Free (x', _)) = if x = x' then raise Found t else I 

508 
 find _ = I; 

509 
in (fold_aterms find t (); NONE) handle Found v => SOME v end; 

510 

511 

16943  512 

16678  513 
(** Comparing terms, types, sorts etc. **) 
16537  514 

16678  515 
(* fast syntactic comparison *) 
516 

517 
fun fast_indexname_ord ((x, i), (y, j)) = 

518 
(case int_ord (i, j) of EQUAL => fast_string_ord (x, y)  ord => ord); 

16537  519 

16599  520 
fun sort_ord SS = 
521 
if pointer_eq SS then EQUAL 

16990  522 
else dict_ord fast_string_ord SS; 
16678  523 

524 
local 

16537  525 

16678  526 
fun cons_nr (TVar _) = 0 
527 
 cons_nr (TFree _) = 1 

528 
 cons_nr (Type _) = 2; 

16537  529 

16678  530 
in 
16537  531 

532 
fun typ_ord TU = 

533 
if pointer_eq TU then EQUAL 

534 
else 

535 
(case TU of 

16678  536 
(Type (a, Ts), Type (b, Us)) => 
16990  537 
(case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us)  ord => ord) 
16678  538 
 (TFree (a, S), TFree (b, S')) => 
539 
(case fast_string_ord (a, b) of EQUAL => sort_ord (S, S')  ord => ord) 

540 
 (TVar (xi, S), TVar (yj, S')) => 

541 
(case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S')  ord => ord) 

542 
 (T, U) => int_ord (cons_nr T, cons_nr U)); 

543 

544 
end; 

545 

546 
local 

547 

548 
fun cons_nr (Const _) = 0 

549 
 cons_nr (Free _) = 1 

550 
 cons_nr (Var _) = 2 

551 
 cons_nr (Bound _) = 3 

552 
 cons_nr (Abs _) = 4 

553 
 cons_nr (_ $ _) = 5; 

554 

555 
fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u) 

556 
 struct_ord (t1 $ t2, u1 $ u2) = 

557 
(case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2)  ord => ord) 

558 
 struct_ord (t, u) = int_ord (cons_nr t, cons_nr u); 

559 

560 
fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u) 

561 
 atoms_ord (t1 $ t2, u1 $ u2) = 

562 
(case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2)  ord => ord) 

563 
 atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b) 

564 
 atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y) 

565 
 atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj) 

566 
 atoms_ord (Bound i, Bound j) = int_ord (i, j) 

567 
 atoms_ord _ = sys_error "atoms_ord"; 

568 

569 
fun types_ord (Abs (_, T, t), Abs (_, U, u)) = 

570 
(case typ_ord (T, U) of EQUAL => types_ord (t, u)  ord => ord) 

571 
 types_ord (t1 $ t2, u1 $ u2) = 

572 
(case types_ord (t1, u1) of EQUAL => types_ord (t2, u2)  ord => ord) 

573 
 types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U) 

574 
 types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U) 

575 
 types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U) 

576 
 types_ord (Bound _, Bound _) = EQUAL 

577 
 types_ord _ = sys_error "types_ord"; 

578 

579 
in 

580 

581 
fun fast_term_ord tu = 

582 
if pointer_eq tu then EQUAL 

583 
else 

584 
(case struct_ord tu of 

585 
EQUAL => (case atoms_ord tu of EQUAL => types_ord tu  ord => ord) 

586 
 ord => ord); 

587 

588 
fun op aconv tu = (fast_term_ord tu = EQUAL); 

589 
fun aconvs ts_us = (list_ord fast_term_ord ts_us = EQUAL); 

590 

591 
structure Vartab = TableFun(type key = indexname val ord = fast_indexname_ord); 

592 
structure Typtab = TableFun(type key = typ val ord = typ_ord); 

593 
structure Termtab = TableFun(type key = term val ord = fast_term_ord); 

594 

595 
end; 

16537  596 

597 

598 
(* term_ord *) 

599 

600 
(*a linear wellfounded ACcompatible ordering for terms: 

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

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

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

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

16678  605 

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

607 
(case int_ord (i, j) of EQUAL => string_ord (x, y)  ord => ord); 

608 

16667  609 
local 
610 

611 
fun hd_depth (t $ _, n) = hd_depth (t, n + 1) 

612 
 hd_depth p = p; 

16537  613 

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

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

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

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

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

619 

16667  620 
in 
621 

16537  622 
fun term_ord tu = 
623 
if pointer_eq tu then EQUAL 

624 
else 

625 
(case tu of 

626 
(Abs (_, T, t), Abs(_, U, u)) => 

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

16667  628 
 (t, u) => 
16537  629 
(case int_ord (size_of_term t, size_of_term u) of 
630 
EQUAL => 

16943  631 
(case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of 
632 
EQUAL => args_ord (t, u)  ord => ord) 

16537  633 
 ord => ord)) 
634 
and hd_ord (f, g) = 

635 
prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g) 

16667  636 
and args_ord (f $ t, g $ u) = 
637 
(case args_ord (f, g) of EQUAL => term_ord (t, u)  ord => ord) 

638 
 args_ord _ = EQUAL; 

16537  639 

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

641 

16667  642 
end; 
643 

644 

645 
(** Lexicographic path order on terms **) 

646 

647 
(* 

16570  648 
See Baader & Nipkow, Term rewriting, CUP 1998. 
649 
Without variables. Const, Var, Bound, Free and Abs are treated all as 

650 
constants. 

651 

652 
f_ord maps strings to integers and serves two purposes: 

653 
 Predicate on constant symbols. Those that are not recognised by f_ord 

654 
must be mapped to ~1. 

655 
 Order on the recognised symbols. These must be mapped to distinct 

656 
integers >= 0. 

657 

16667  658 
*) 
16570  659 

660 
local 

16667  661 
fun dest_hd f_ord (Const (a, T)) = 
16570  662 
let val ord = f_ord a in 
663 
if ord = ~1 then ((1, ((a, 0), T)), 0) else ((0, (("", ord), T)), 0) 

664 
end 

665 
 dest_hd _ (Free (a, T)) = ((1, ((a, 0), T)), 0) 

666 
 dest_hd _ (Var v) = ((1, v), 1) 

667 
 dest_hd _ (Bound i) = ((1, (("", i), dummyT)), 2) 

668 
 dest_hd _ (Abs (_, T, _)) = ((1, (("", 0), T)), 3); 

669 

670 
fun term_lpo f_ord (s, t) = 

671 
let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in 

672 
if forall (fn si => term_lpo f_ord (si, t) = LESS) ss 

673 
then case hd_ord f_ord (f, g) of 

16667  674 
GREATER => 
675 
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts 

676 
then GREATER else LESS 

16570  677 
 EQUAL => 
16667  678 
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts 
679 
then list_ord (term_lpo f_ord) (ss, ts) 

680 
else LESS 

16570  681 
 LESS => LESS 
682 
else GREATER 

683 
end 

684 
and hd_ord f_ord (f, g) = case (f, g) of 

685 
(Abs (_, T, t), Abs (_, U, u)) => 

686 
(case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U)  ord => ord) 

687 
 (_, _) => prod_ord (prod_ord int_ord 

688 
(prod_ord indexname_ord typ_ord)) int_ord 

689 
(dest_hd f_ord f, dest_hd f_ord g) 

690 
in 

691 
val term_lpo = term_lpo 

692 
end; 

693 

16537  694 

0  695 
(** Connectives of higher order logic **) 
696 

375  697 
fun itselfT ty = Type ("itself", [ty]); 
14854  698 
val a_itselfT = itselfT (TFree ("'a", [])); 
375  699 

0  700 
val propT : typ = Type("prop",[]); 
701 

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

703 

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

705 

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

707 

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

13000  709 
fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t 
0  710 
 strip_all_body t = t; 
711 

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

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

13000  714 
(a,T) :: strip_all_vars t 
0  715 
 strip_all_vars t = [] : (string*typ) list; 
716 

717 
(*increments a term's nonlocal bound variables 

718 
required when moving a term within abstractions 

719 
inc is increment for bound variables 

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

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

723 
Abs(a, T, incr_bv(inc,lev+1,body)) 
13000  724 
 incr_bv (inc, lev, f$t) = 
0  725 
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 
726 
 incr_bv (inc, lev, u) = u; 

727 

728 
fun incr_boundvars 0 t = t 

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

730 

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

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

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

735 
else (x,y)::al) 

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

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

738 

739 
(* strip abstractions created by parameters *) 

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

741 

742 
fun rename_abs pat obj t = 

743 
let 

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

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

17271  746 
Abs (if_none (AList.lookup (op =) ren x) x, T, ren_abs b) 
12981  747 
 ren_abs (f $ t) = ren_abs f $ ren_abs t 
748 
 ren_abs t = t 

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

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

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

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

754 
if i<lev then js else (ilev) ins_int js 
0  755 
 add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js) 
756 
 add_loose_bnos (f$t, lev, js) = 

13000  757 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
0  758 
 add_loose_bnos (_, _, js) = js; 
759 

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

761 

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

763 
level k or beyond. *) 

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

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

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

767 
 loose_bvar _ = false; 

768 

2792  769 
fun loose_bvar1(Bound i,k) = i = k 
770 
 loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 

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

772 
 loose_bvar1 _ = false; 

0  773 

774 
(*Substitute arguments for loose bound variables. 

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

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

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

780 
*) 

13000  781 
fun subst_bounds (args: term list, t) : term = 
0  782 
let val n = length args; 
783 
fun subst (t as Bound i, lev) = 

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

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

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

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

787 
 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

788 
 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

789 
 subst (t,lev) = t 
0  790 
in case args of [] => t  _ => subst (t,0) end; 
791 

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

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

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

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

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

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

798 
 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

799 
 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

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

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

802 

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

804 
fun betapply (Abs(_,_,t), u) = subst_bound (u,t) 
0  805 
 betapply (f,u) = f$u; 
806 

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

807 

16882  808 
(** Specialized equality, membership, insertion etc. **) 
2192
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

809 

16882  810 
(* indexnames *) 
811 

16724  812 
fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y; 
2192
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

813 

2959  814 
fun mem_ix (_, []) = false 
16882  815 
 mem_ix (x, y :: ys) = eq_ix (x, y) orelse mem_ix (x, ys); 
2192
3bf092b5310b
Optimizations: removal of polymorphic equality; oneargument case
paulson
parents:
2182
diff
changeset

816 

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

818 

0  819 

16882  820 
(* variables *) 
821 

16943  822 
fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S'; 
823 
fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T'; 

824 

825 
val tvar_ord = prod_ord indexname_ord sort_ord; 

826 
val var_ord = prod_ord indexname_ord typ_ord; 

16882  827 

828 

829 
(* terms *) 

2176  830 

831 
fun mem_term (_, []) = false 

16882  832 
 mem_term (t, t'::ts) = t aconv t' orelse mem_term (t, ts); 
2176  833 

834 
fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; 

835 

16882  836 

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

840 
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

841 
 matchrands _ = true 
0  842 
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

843 
(_, Var _) => true 
0  844 
 (Var _, _) => true 
845 
 (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u) 

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

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

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

849 
 (_, Abs _) => true 

850 
 _ => false 

851 
end; 

852 

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

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

855 
 subst_free pairs = 

13000  856 
let fun substf u = 
17314  857 
case AList.lookup (op aconv) pairs u of 
15531  858 
SOME u' => u' 
859 
 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

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

861 
 _ => u) 
0  862 
in substf end; 
863 

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

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

866 

867 

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

16882  871 
fun abstract_over (v, body) = 
872 
let 

16990  873 
exception SAME; 
874 
fun abs lev tm = 

875 
if v aconv tm then Bound lev 

16882  876 
else 
16990  877 
(case tm of 
878 
Abs (a, T, t) => Abs (a, T, abs (lev + 1) t) 

879 
 t $ u => (abs lev t $ (abs lev u handle SAME => u) handle SAME => t $ abs lev u) 

880 
 _ => raise SAME); 

881 
in abs 0 body handle SAME => body end; 

0  882 

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

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

0  886 

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

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

17786  889 
fun absdummy (T, body) = Abs ("uu", T, body); 
0  890 

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

892 
fun list_abs_free ([ ] , t) = t 

13000  893 
 list_abs_free ((a,T)::vars, t) = 
0  894 
absfree(a, T, list_abs_free(vars,t)); 
895 

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

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

13000  898 
 list_all_free ((a,T)::vars, t) = 
0  899 
(all T) $ (absfree(a, T, list_all_free(vars,t))); 
900 

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

902 
fun list_all ([], t) = t 

13000  903 
 list_all ((a,T)::vars, t) = 
0  904 
(all T) $ (Abs(a, T, list_all(vars,t))); 
905 

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

910 
let 

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

912 
 subst (t $ u) = subst t $ subst u 

17314  913 
 subst t = if_none (AList.lookup (op aconv) inst t) t; 
16678  914 
in subst tm end; 
0  915 

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

918 
 typ_subst_atomic inst ty = 

919 
let 

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

17314  921 
 subst T = if_none (AList.lookup (op = : typ * typ > bool) inst T) T; 
16678  922 
in subst ty end; 
15797  923 

16678  924 
fun subst_atomic_types [] tm = tm 
925 
 subst_atomic_types inst tm = map_term_types (typ_subst_atomic inst) tm; 

926 

927 
fun typ_subst_TVars [] ty = ty 

928 
 typ_subst_TVars inst ty = 

929 
let 

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

17271  931 
 subst (T as TVar (xi, _)) = if_none (AList.lookup (op =) inst xi) T 
16678  932 
 subst T = T; 
933 
in subst ty end; 

0  934 

16678  935 
fun subst_TVars [] tm = tm 
936 
 subst_TVars inst tm = map_term_types (typ_subst_TVars inst) tm; 

0  937 

16678  938 
(*see also Envir.norm_term*) 
939 
fun subst_Vars [] tm = tm 

940 
 subst_Vars inst tm = 

941 
let 

17271  942 
fun subst (t as Var (xi, _)) = if_none (AList.lookup (op =) inst xi) t 
16678  943 
 subst (Abs (a, T, t)) = Abs (a, T, subst t) 
944 
 subst (t $ u) = subst t $ subst u 

945 
 subst t = t; 

946 
in subst tm end; 

0  947 

16678  948 
(*see also Envir.norm_term*) 
949 
fun subst_vars ([], []) tm = tm 

950 
 subst_vars ([], inst) tm = subst_Vars inst tm 

951 
 subst_vars (instT, inst) tm = 

952 
let 

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

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

955 
 subst (t as Var (xi, T)) = 

17271  956 
(case AList.lookup (op =) inst xi of 
16678  957 
NONE => Var (xi, typ_subst_TVars instT T) 
958 
 SOME t => t) 

959 
 subst (t as Bound _) = t 

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

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

962 
in subst tm end; 

0  963 

964 

16943  965 
(* instantiation of schematic variables (types before terms) *) 
16882  966 

967 
local exception SAME in 

968 

16943  969 
fun instantiateT_same [] _ = raise SAME 
970 
 instantiateT_same instT ty = 

16882  971 
let 
972 
fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts) 

973 
 subst_typ (TVar v) = 

17314  974 
(case AList.lookup eq_tvar instT v of 
16882  975 
SOME T => T 
976 
 NONE => raise SAME) 

977 
 subst_typ _ = raise SAME 

978 
and subst_typs (T :: Ts) = 

979 
(subst_typ T :: (subst_typs Ts handle SAME => Ts) 

980 
handle SAME => T :: subst_typs Ts) 

981 
 subst_typs [] = raise SAME; 

982 
in subst_typ ty end; 

983 

984 
fun instantiate ([], []) tm = tm 

985 
 instantiate (instT, inst) tm = 

986 
let 

16943  987 
val substT = instantiateT_same instT; 
988 
fun subst (Const (c, T)) = Const (c, substT T) 

989 
 subst (Free (x, T)) = Free (x, substT T) 

16882  990 
 subst (Var (xi, T)) = 
16943  991 
let val (T', same) = (substT T, false) handle SAME => (T, true) in 
17314  992 
(case AList.lookup eq_var inst (xi, T') of 
16882  993 
SOME t => t 
994 
 NONE => if same then raise SAME else Var (xi, T')) 

995 
end 

996 
 subst (Bound _) = raise SAME 

997 
 subst (Abs (x, T, t)) = 

16943  998 
(Abs (x, substT T, subst t handle SAME => t) 
16882  999 
handle SAME => Abs (x, T, subst t)) 
1000 
 subst (t $ u) = (subst t $ (subst u handle SAME => u) handle SAME => t $ subst u); 

1001 
in subst tm handle SAME => tm end; 

1002 

1003 
fun instantiateT instT ty = 

16943  1004 
instantiateT_same instT ty handle SAME => ty; 
16882  1005 

1006 
end; 

1007 

1008 

15573  1009 
(** Identifying firstorder terms **) 
1010 

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

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

1013 

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

16667  1017 
fun is_first_order quants = 
16589  1018 
let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body 
16667  1019 
 first_order1 Ts (Const(q,_) $ Abs(a,T,body)) = 
1020 
q mem_string quants andalso (*it is a known quantifier*) 

16589  1021 
not (is_funtype T) andalso first_order1 (T::Ts) body 
16667  1022 
 first_order1 Ts t = 
1023 
case strip_comb t of 

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

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

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

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

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

1029 
 _ => error "first_order: unexpected case" 

16589  1030 
in first_order1 [] end; 
15573  1031 

16710  1032 

16990  1033 
(* maximum index of typs and terms *) 
0  1034 

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

1037 
 maxidx_typ (TFree _) i = i 

1038 
and maxidx_typs [] i = i 

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

0  1040 

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

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

1044 
 maxidx_term (Bound _) i = i 

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

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

0  1047 

16710  1048 
fun maxidx_of_typ T = maxidx_typ T ~1; 
1049 
fun maxidx_of_typs Ts = maxidx_typs Ts ~1; 

1050 
fun maxidx_of_term t = maxidx_term t ~1; 

13665  1051 

0  1052 

1053 

1054 
(**** Syntaxrelated declarations ****) 

1055 

1056 
(*** Printing ***) 

1057 

16943  1058 
(*Makes a variant of a name distinct from the names in 'used'. 
14676  1059 
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

1060 
preserves a suffix of underscores "_". *) 
16943  1061 
fun variant used name = 
12306
749a04f0cfb0
variant: preserve suffix of underscores (for skolem/internal names etc.);
wenzelm
parents:
11922
diff
changeset

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

1063 
val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name)); 
16943  1064 
fun vary2 c = if ((c ^ u) mem_string used) then vary2 (Symbol.bump_string c) else c; 
1065 
fun vary1 c = if ((c ^ u) mem_string used) 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

1066 
in vary1 (if c = "" then "u" else c) ^ u end; 
0  1067 

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

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

13000  1070 
 variantlist(b::bs, used) = 
0  1071 
let val b' = variant used b 
1072 
in b' :: variantlist (bs, b'::used) end; 

1073 

14695  1074 
(*Invent fresh names*) 
1075 
fun invent_names _ _ 0 = [] 

1076 
 invent_names used a n = 

1077 
let val b = Symbol.bump_string a in 

1078 
if a mem_string used then invent_names used b n 

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

1080 
end; 

11353  1081 

16537  1082 

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

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

1084 

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

1085 
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

1086 
 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

1087 
 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

1088 

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

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

1091 

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

1092 
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

1093 
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

1094 

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

1096 
 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

1097 
 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

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

1099 

13646  1100 
fun term_consts t = add_term_consts(t,[]); 
1101 

16943  1102 
fun exists_subterm P = 
1103 
let 

1104 
fun ex tm = P tm orelse 

1105 
(case tm of 

1106 
t $ u => ex t orelse ex u 

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

1108 
 _ => false); 

1109 
in ex end; 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
16035
diff
changeset

1110 

16943  1111 
fun exists_Const P = exists_subterm (fn Const c => P c  _ => false); 
4631  1112 

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

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

1114 
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

1115 
 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

1116 
 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

1117 

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

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

1119 
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

1120 
 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

1121 
 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

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

1123 
 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

1124 
 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

1125 

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

1126 

0  1127 
(** TFrees and TVars **) 
1128 

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

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

1130 
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

1131 
 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

1132 
 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

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

1134 

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

10666  1137 
fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs 
2176  1138 
 add_term_names (Free(a,_), bs) = a ins_string bs 
0  1139 
 add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) 
1140 
 add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) 

1141 
 add_term_names (_, bs) = bs; 

1142 

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

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

1144 
fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts 
0  1145 
 add_typ_tvars(TFree(_),vs) = vs 
16294  1146 
 add_typ_tvars(TVar(v),vs) = insert (op =) v vs; 
0  1147 

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

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

1149 
fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts 
2176  1150 
 add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs 
0  1151 
 add_typ_tfree_names(TVar(_),fs) = fs; 
1152 

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

1153 
fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts 
16294  1154 
 add_typ_tfrees(TFree(f),fs) = insert (op =) f fs 
0  1155 
 add_typ_tfrees(TVar(_),fs) = fs; 
1156 

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

1157 
fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts 
2176  1158 
 add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms 
1159 
 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

1160 

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

1163 

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

1165 
val add_term_tfrees = it_term_types add_typ_tfrees; 

1166 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

1167 

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

1168 
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

1169 

0  1170 
(*Nonlist versions*) 
1171 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

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

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

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

1175 

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

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

1177 

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

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

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

1182 

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

1183 
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

1184 
 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

1185 
 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

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

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

1188 
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

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

1190 
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

1191 

16537  1192 

0  1193 
(** Frees and Vars **) 
1194 

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

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

16990  1197 
Var _ => OrdList.insert term_ord t vars 
0  1198 
 Abs (_,_,body) => add_term_vars(body,vars) 
1199 
 f$t => add_term_vars (f, add_term_vars(t, vars)) 

1200 
 _ => vars; 

1201 

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

1203 

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

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

16990  1206 
Free _ => OrdList.insert term_ord t frees 
0  1207 
 Abs (_,_,body) => add_term_frees(body,frees) 
1208 
 f$t => add_term_frees (f, add_term_frees(t, frees)) 

1209 
 _ => frees; 

1210 

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

1212 

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

17851  1214 
having a unique name  SLOW!*) 
0  1215 
fun variant_abs (a,T,P) = 
1216 
let val b = variant (add_term_names(P,[])) a 

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

1217 
in (b, subst_bound (Free(b,T), P)) end; 
0  1218 

16678  1219 
fun dest_abs (x, T, body) = 
1220 
let 

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

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

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

1224 
 name_clash _ = false; 

1225 
in 

1226 
if name_clash body then 

1227 
dest_abs (variant [x] x, T, body) (*potentially slow, but rarely happens*) 

1228 
else (x, subst_bound (Free (x, T), body)) 

1229 
end; 

1230 

16990  1231 
(*names for numbered variables  
1232 
preserves order wrt. int_ord vs. string_ord, avoids allocating new strings*) 

1233 
local 

1234 
val small_int = Vector.tabulate (1000, fn i => 

1235 
let val leading = if i < 10 then "00" else if i < 100 then "0" else "" 

1236 
in ":" ^ leading ^ string_of_int i end); 

1237 
in 

1238 
fun bound n = 

1239 
if n < 1000 then Vector.sub (small_int, n) 

1240 
else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000); 

1241 
end; 

1242 

1243 
val is_bound = String.isPrefix ":"; 

16943  1244 

0  1245 
(* renames and reverses the strings in vars away from names *) 
1246 
fun rename_aTs names vars : (string*typ)list = 

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

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

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

1251 
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

1252 

1417  1253 

16943  1254 
(* zero var indexes *) 
4286
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

1255 

16943  1256 
fun zero_var_inst vars = 
1257 
fold (fn v as ((x, i), X) => fn (used, inst) => 

1258 
let 

17642  1259 
val x' = variant used (if is_bound x then "u" else x); 
16943  1260 
val used' = x' :: used; 
1261 
in if x = x' andalso i = 0 then (used', inst) else (used', (v, ((x', 0), X)) :: inst) end) 

1262 
vars ([], []) > #2; 

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

1263 

16943  1264 
fun zero_var_indexesT ty = 
1265 
instantiateT (map (apsnd TVar) (zero_var_inst (sort tvar_ord (add_tvarsT ty [])))) ty; 

16790  1266 

16943  1267 
fun zero_var_indexes_inst tm = 
1268 
let 

1269 
val instT = map (apsnd TVar) (zero_var_inst (sort tvar_ord (fold_types add_tvarsT tm []))); 

1270 
val inst = 

1271 
add_vars tm [] > map (apsnd (instantiateT instT)) 

1272 
> sort var_ord > zero_var_inst > map (apsnd Var); 

1273 
in (instT, inst) end; 

12499  1274 

16943  1275 
fun zero_var_indexes tm = instantiate (zero_var_indexes_inst tm) tm; 
4286
a09e3e6da2de
added foldl_atyps: ('a * typ > 'a) > 'a * typ > 'a;
wenzelm
parents:
4188
diff
changeset

1276 

1417  1277 

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

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

1279 

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

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

1281 

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

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

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

1284 

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

1285 
fun no_dummy_patterns tm = 
16787  1286 
if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

1288 

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

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

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

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

1294 
 replace_dummy Ts (i, t $ u) = 

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

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

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

1298 

1299 
val replace_dummy_patterns = replace_dummy []; 

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

1300 

10552  1301 
fun is_replaced_dummy_pattern ("_dummy_", _) = true 
1302 
 is_replaced_dummy_pattern _ = false; 

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

1303 

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

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

1307 
 show_dummy_patterns a = a; 

1308 

13484  1309 

1310 
(* adhoc freezing *) 

1311 

1312 
fun adhoc_freeze_vars tm = 

1313 
let 

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

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

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

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

1318 
in (subst_atomic insts tm, xs) end; 

1319 

1320 

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

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

1322 

15986  1323 
val show_question_marks = ref true; 
15472  1324 

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

1325 
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

1326 
let 
15986  1327 
val question_mark = if ! show_question_marks then "?" else ""; 
1328 
val idx = string_of_int i; 

1329 
val dot = 

1330 
(case rev (Symbol.explode x) of 

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

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

1333 
 c :: _ => Symbol.is_digit c 

1334 
 _ => true); 

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

1335 
in 
15986  1336 
if dot then question_mark ^ x ^ "." ^ idx 
1337 
else if i <> 0 then question_mark ^ x ^ idx 

1338 
else question_mark ^ x 

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

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

1340 

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

1341 
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

1342 
 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

1343 

17777
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1344 

05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1345 
(* str_of_term *) 
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1346 

05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1347 
fun str_of_term (Const (c, _)) = c 
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1348 
 str_of_term (Free (x, _)) = x 
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1349 
 str_of_term (Var (xi, _)) = string_of_vname xi 
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1350 
 str_of_term (Bound i) = string_of_int i 
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1351 
 str_of_term (Abs (x, _, t)) = "%" ^ x ^ ". " ^ str_of_term t 
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1352 
 str_of_term (t $ u) = "(" ^ str_of_term t ^ " " ^ str_of_term u ^ ")"; 
05f5532a8289
added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
wenzelm
parents:
17756
diff
changeset

1353 

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

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

1355 

4444  1356 
structure BasicTerm: BASIC_TERM = Term; 
1357 
open BasicTerm; 