author  wenzelm 
Tue, 12 Sep 2006 12:12:55 +0200  
changeset 20511  c7daff0a3193 
parent 20331  ccdd1592f5ff 
child 20531  7de9caf4fd78 
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 
16710  45 
val dest_Const: term > string * typ 
46 
val dest_Free: term > string * typ 

47 
val dest_Var: term > indexname * typ 

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

52 
val strip_type: typ > typ list * typ 

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

18847  67 
val map_atyps: (typ > typ) > typ > typ 
68 
val map_aterms: (term > term) > term > term 

4444  69 
val map_type_tvar: (indexname * sort > typ) > typ > typ 
70 
val map_type_tfree: (string * sort > typ) > typ > typ 

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

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

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

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

18927  76 
val it_term_types: (typ * 'a > 'a) > term * 'a > 'a 
16943  77 
val add_term_names: term * string list > string list 
16710  78 
val aconv: term * term > bool 
16537  79 
structure Vartab: TABLE 
80 
structure Typtab: TABLE 

81 
structure Termtab: TABLE 

4444  82 
val propT: typ 
83 
val implies: term 

84 
val all: typ > term 

85 
val equals: typ > term 

86 
val strip_all_body: term > term 

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

88 
val incr_bv: int * int * term > term 

89 
val incr_boundvars: int > term > term 

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

91 
val loose_bnos: term > int list 

92 
val loose_bvar: term * int > bool 

93 
val loose_bvar1: term * int > bool 

94 
val subst_bounds: term list * term > term 

95 
val subst_bound: term * term > term 

96 
val betapply: term * term > term 

18183  97 
val betapplys: term * term list > term 
4444  98 
val eq_ix: indexname * indexname > bool 
99 
val could_unify: term * term > bool 

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

101 
val abstract_over: term * term > term 

11922  102 
val lambda: term > term > term 
4444  103 
val absfree: string * typ * term > term 
17786  104 
val absdummy: typ * term > term 
4444  105 
val list_abs_free: (string * typ) list * term > term 
106 
val list_all_free: (string * typ) list * term > term 

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

16710  108 
val subst_atomic: (term * term) list > term > term 
109 
val typ_subst_atomic: (typ * typ) list > typ > typ 

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

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

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

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

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

115 
val is_first_order: string list > term > bool 

4444  116 
val maxidx_of_typ: typ > int 
117 
val maxidx_of_typs: typ list > int 

118 
val maxidx_of_term: term > int 

119 
val add_term_consts: term * string list > string list 

13646  120 
val term_consts: term > string list 
19909  121 
val exists_subtype: (typ > bool) > typ > bool 
16943  122 
val exists_subterm: (term > bool) > term > bool 
16710  123 
val exists_Const: (string * typ > bool) > term > bool 
124 
val add_term_free_names: term * string list > string list 

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

126 
val add_typ_tfree_names: typ * string list > string list 

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

128 
val add_typ_varnames: typ * string list > string list 

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

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

131 
val add_term_tfree_names: term * string list > string list 

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

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

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

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

136 
val add_typ_ixns: indexname list * typ > indexname list 

137 
val add_term_tvar_ixns: term * indexname list > indexname list 

138 
val add_term_vars: term * term list > term list 

139 
val term_vars: term > term list 

4444  140 
val add_term_frees: term * term list > term list 
141 
val term_frees: term > term list 

20160  142 
val rename_wrt_term: term > (string * 'a) list > (string * 'a) list 
15986  143 
val show_question_marks: bool ref 
4444  144 
end; 
0  145 

4444  146 
signature TERM = 
147 
sig 

148 
include BASIC_TERM 

19394  149 
val aT: sort > typ 
150 
val itselfT: typ > typ 

151 
val a_itselfT: typ 

16710  152 
val argument_type_of: term > typ 
16943  153 
val add_tvarsT: typ > (indexname * sort) list > (indexname * sort) list 
154 
val add_tvars: term > (indexname * sort) list > (indexname * sort) list 

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

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

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

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

20199  159 
val add_varnames: term > indexname list > indexname list 
20109  160 
val strip_abs_eta: int > term > (string * typ) list * term 
16678  161 
val fast_indexname_ord: indexname * indexname > order 
16537  162 
val indexname_ord: indexname * indexname > order 
163 
val sort_ord: sort * sort > order 

164 
val typ_ord: typ * typ > order 

16678  165 
val fast_term_ord: term * term > order 
16537  166 
val term_ord: term * term > order 
167 
val hd_ord: term * term > order 

168 
val termless: term * term > bool 

20129
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

169 
val term_lpo: (term > int) > term * term > order 
12981  170 
val match_bvars: (term * term) * (string * string) list > (string * string) list 
171 
val rename_abs: term > term > term > term option 

16943  172 
val eq_tvar: (indexname * sort) * (indexname * sort) > bool 
16882  173 
val eq_var: (indexname * typ) * (indexname * typ) > bool 
16943  174 
val tvar_ord: (indexname * sort) * (indexname * sort) > order 
175 
val var_ord: (indexname * typ) * (indexname * typ) > order 

16710  176 
val maxidx_typ: typ > int > int 
177 
val maxidx_typs: typ list > int > int 

178 
val maxidx_term: term > int > int 

20239  179 
val dest_abs: string * typ * term > string * term 
20148  180 
val declare_term_names: term > Name.context > Name.context 
20160  181 
val variant_frees: term > (string * 'a) list > (string * 'a) list 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

182 
val dummy_patternN: string 
18253  183 
val dummy_pattern: typ > term 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

185 
val replace_dummy_patterns: int * term > int * term 
10552  186 
val is_replaced_dummy_pattern: indexname > bool 
16035  187 
val show_dummy_patterns: term > term 
14786
24a7bc97a27a
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm
parents:
14695
diff
changeset

188 
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

189 
val string_of_vname': indexname > string 
4444  190 
end; 
191 

192 
structure Term: TERM = 

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

193 
struct 
0  194 

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

196 
for resolution.*) 

16537  197 
type indexname = string * int; 
0  198 

4626  199 
(* Types are classified by sorts. *) 
0  200 
type class = string; 
201 
type sort = class list; 

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

202 
type arity = string * sort list * sort; 
0  203 

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

205 
datatype typ = Type of string * typ list 

206 
 TFree of string * sort 

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

207 
 TVar of indexname * sort; 
0  208 

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

209 
(*Terms. Bound variables are indicated by depth number. 
0  210 
Free variables, (scheme) variables and constants have names. 
4626  211 
An term is "closed" if every bound variable of level "lev" 
13000  212 
is enclosed by at least "lev" abstractions. 
0  213 

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

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

216 

13000  217 
datatype term = 
0  218 
Const of string * typ 
13000  219 
 Free of string * typ 
0  220 
 Var of indexname * typ 
221 
 Bound of int 

222 
 Abs of string*typ*term 

3965  223 
 op $ of term*term; 
0  224 

16537  225 
(*Errors involving type mismatches*) 
0  226 
exception TYPE of string * typ list * term list; 
227 

16537  228 
(*Errors errors involving terms*) 
0  229 
exception TERM of string * term list; 
230 

231 
(*Note variable naming conventions! 

232 
a,b,c: string 

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

234 
i,j,m,n: int 

235 
t,u: term 

236 
v,w: indexnames 

237 
x,y: any 

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

239 
T,U: typ 

240 
*) 

241 

242 

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

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

244 

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

247 

248 
fun no_dummyT typ = 

249 
let 

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

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

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

253 
 check _ = (); 

254 
in check typ; typ end; 

255 

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

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

257 

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

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

260 

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

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

262 
 dest_Type T = raise TYPE ("dest_Type", [T], []); 
15914  263 
fun dest_TVar (TVar x) = x 
264 
 dest_TVar T = raise TYPE ("dest_TVar", [T], []); 

265 
fun dest_TFree (TFree x) = x 

266 
 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

267 

16537  268 

0  269 
(** Discriminators **) 
270 

7318  271 
fun is_Bound (Bound _) = true 
272 
 is_Bound _ = false; 

273 

0  274 
fun is_Const (Const _) = true 
275 
 is_Const _ = false; 

276 

277 
fun is_Free (Free _) = true 

278 
 is_Free _ = false; 

279 

280 
fun is_Var (Var _) = true 

281 
 is_Var _ = false; 

282 

283 
fun is_TVar (TVar _) = true 

284 
 is_TVar _ = false; 

285 

16537  286 

0  287 
(** Destructors **) 
288 

289 
fun dest_Const (Const x) = x 

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

291 

292 
fun dest_Free (Free x) = x 

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

294 

295 
fun dest_Var (Var x) = x 

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

297 

298 

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

4064  301 

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

304 
 binder_types _ = []; 

305 

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

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

308 
 body_type T = T; 

309 

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

311 
fun strip_type T : typ list * typ = 

312 
(binder_types T, body_type T); 

313 

314 

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

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

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

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

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

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

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

326 
in case T of 

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

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

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

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

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

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

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

336 

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

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

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

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

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

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

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

0  350 

16678  351 
(*Determine the argument type of a function*) 
352 
fun argument_type_of tm = 

353 
let 

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

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

356 

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

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

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

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

361 
in arg 0 [] tm end; 

362 

0  363 

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

18927  366 
fun strip_abs (Abs (a, T, t)) = 
367 
let val (a', t') = strip_abs t 

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

369 
 strip_abs t = ([], t); 

370 

0  371 
(* maps (x1,...,xn)t to t *) 
13000  372 
fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t 
0  373 
 strip_abs_body u = u; 
374 

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

13000  376 
fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t 
0  377 
 strip_abs_vars u = [] : (string*typ) list; 
378 

379 

380 
fun strip_qnt_body qnt = 

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

382 
 strip t = t 

383 
in strip end; 

384 

385 
fun strip_qnt_vars qnt = 

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

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

388 
in strip end; 

389 

390 

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

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

394 

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

13000  396 
fun strip_comb u : term * term list = 
0  397 
let fun stripc (f$t, ts) = stripc (f, t::ts) 
13000  398 
 stripc x = x 
0  399 
in stripc(u,[]) end; 
400 

401 

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

403 
fun head_of (f$t) = head_of f 

404 
 head_of u = u; 

405 

406 

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

409 
let 

16678  410 
fun add_size (t $ u, n) = add_size (t, add_size (u, n)) 
411 
 add_size (Abs (_ ,_, t), n) = add_size (t, n + 1) 

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

413 
in add_size (tm, 0) end; 

0  414 

18847  415 
fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts) 
18976
4efb82669880
fixed the most silly bug conceivable in map_atyps
haftmann
parents:
18975
diff
changeset

416 
 map_atyps f T = f T; 
18847  417 

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

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

420 
 map_aterms f t = f t; 

421 

18981  422 
fun map_type_tvar f = map_atyps (fn TVar x => f x  T => T); 
423 
fun map_type_tfree f = map_atyps (fn TFree x => f x  T => T); 

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

424 

0  425 
fun map_term_types f = 
16678  426 
let 
427 
fun map_aux (Const (a, T)) = Const (a, f T) 

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

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

430 
 map_aux (t as Bound _) = t 

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

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

433 
in map_aux end; 

0  434 

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

436 
fun it_term_types f = 

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

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

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

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

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

442 
 iter(Bound _, a) = a 

443 
in iter end 

444 

445 

16943  446 
(* fold types and terms *) 
447 

448 
(*fold atoms of type*) 

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

450 
 fold_atyps f T = f T; 

451 

452 
(*fold atoms of term*) 

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

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

455 
 fold_aterms f a = f a; 

456 

457 
(*fold types of term*) 

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

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

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

461 
 fold_term_types f (Bound _) = I 

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

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

464 

465 
fun fold_types f = fold_term_types (K f); 

466 

467 
(*collect variables*) 

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

469 
val add_tvars = fold_types add_tvarsT; 

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

20199  471 
val add_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi  _ => I); 
16943  472 
val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v  _ => I); 
473 
val add_tfrees = fold_types add_tfreesT; 

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

475 

476 

16678  477 
(** Comparing terms, types, sorts etc. **) 
16537  478 

20511  479 
(* alpha equivalence  tuned for equalities *) 
480 

481 
fun tm1 aconv tm2 = 

482 
pointer_eq (tm1, tm2) orelse 

483 
(case (tm1, tm2) of 

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

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

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

487 

488 

489 
(* fast syntactic ordering  tuned for inequalities *) 

16678  490 

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

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

16537  493 

16599  494 
fun sort_ord SS = 
495 
if pointer_eq SS then EQUAL 

16990  496 
else dict_ord fast_string_ord SS; 
16678  497 

498 
local 

16537  499 

16678  500 
fun cons_nr (TVar _) = 0 
501 
 cons_nr (TFree _) = 1 

502 
 cons_nr (Type _) = 2; 

16537  503 

16678  504 
in 
16537  505 

506 
fun typ_ord TU = 

507 
if pointer_eq TU then EQUAL 

508 
else 

509 
(case TU of 

16678  510 
(Type (a, Ts), Type (b, Us)) => 
16990  511 
(case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us)  ord => ord) 
16678  512 
 (TFree (a, S), TFree (b, S')) => 
513 
(case fast_string_ord (a, b) of EQUAL => sort_ord (S, S')  ord => ord) 

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

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

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

517 

518 
end; 

519 

520 
local 

521 

522 
fun cons_nr (Const _) = 0 

523 
 cons_nr (Free _) = 1 

524 
 cons_nr (Var _) = 2 

525 
 cons_nr (Bound _) = 3 

526 
 cons_nr (Abs _) = 4 

527 
 cons_nr (_ $ _) = 5; 

528 

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

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

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

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

533 

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

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

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

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

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

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

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

541 
 atoms_ord _ = sys_error "atoms_ord"; 

542 

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

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

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

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

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

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

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

550 
 types_ord (Bound _, Bound _) = EQUAL 

551 
 types_ord _ = sys_error "types_ord"; 

552 

553 
in 

554 

555 
fun fast_term_ord tu = 

556 
if pointer_eq tu then EQUAL 

557 
else 

558 
(case struct_ord tu of 

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

560 
 ord => ord); 

561 

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

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

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

565 

566 
end; 

16537  567 

568 

569 
(* term_ord *) 

570 

571 
(*a linear wellfounded ACcompatible ordering for terms: 

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

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

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

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

16678  576 

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

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

579 

16667  580 
local 
581 

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

583 
 hd_depth p = p; 

16537  584 

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

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

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

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

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

590 

16667  591 
in 
592 

16537  593 
fun term_ord tu = 
594 
if pointer_eq tu then EQUAL 

595 
else 

596 
(case tu of 

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

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

16667  599 
 (t, u) => 
16537  600 
(case int_ord (size_of_term t, size_of_term u) of 
601 
EQUAL => 

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

16537  604 
 ord => ord)) 
605 
and hd_ord (f, g) = 

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

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

609 
 args_ord _ = EQUAL; 

16537  610 

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

612 

16667  613 
end; 
614 

615 

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

617 

618 
(* 

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

621 
constants. 

622 

20129
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

623 
f_ord maps terms to integers and serves two purposes: 
16570  624 
 Predicate on constant symbols. Those that are not recognised by f_ord 
625 
must be mapped to ~1. 

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

627 
integers >= 0. 

20129
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

628 
The argument of f_ord is never an application. 
16667  629 
*) 
16570  630 

631 
local 

20129
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

632 

95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

633 
fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0) 
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

634 
 unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0) 
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

635 
 unrecognized (Var v) = ((1, v), 1) 
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

636 
 unrecognized (Bound i) = ((1, (("", i), dummyT)), 2) 
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

637 
 unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3); 
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

638 

95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

639 
fun dest_hd f_ord t = 
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

640 
let val ord = f_ord t in 
95e84d2c9f2c
Term.term_lpo takes order on terms rather than strings as argument.
ballarin
parents:
20122
diff
changeset

641 
if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0) 
16570  642 
end 
643 

644 
fun term_lpo f_ord (s, t) = 

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

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

647 
then case hd_ord f_ord (f, g) of 

16667  648 
GREATER => 
649 
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts 

650 
then GREATER else LESS 

16570  651 
 EQUAL => 
16667  652 
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts 
653 
then list_ord (term_lpo f_ord) (ss, ts) 

654 
else LESS 

16570  655 
 LESS => LESS 
656 
else GREATER 

657 
end 

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

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

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

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

662 
(prod_ord indexname_ord typ_ord)) int_ord 

663 
(dest_hd f_ord f, dest_hd f_ord g) 

664 
in 

665 
val term_lpo = term_lpo 

666 
end; 

667 

16537  668 

0  669 
(** Connectives of higher order logic **) 
670 

19394  671 
fun aT S = TFree ("'a", S); 
672 

375  673 
fun itselfT ty = Type ("itself", [ty]); 
14854  674 
val a_itselfT = itselfT (TFree ("'a", [])); 
375  675 

0  676 
val propT : typ = Type("prop",[]); 
677 

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

679 

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

681 

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

683 

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

13000  685 
fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t 
0  686 
 strip_all_body t = t; 
687 

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

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

13000  690 
(a,T) :: strip_all_vars t 
0  691 
 strip_all_vars t = [] : (string*typ) list; 
692 

693 
(*increments a term's nonlocal bound variables 

694 
required when moving a term within abstractions 

695 
inc is increment for bound variables 

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

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

699 
Abs(a, T, incr_bv(inc,lev+1,body)) 
13000  700 
 incr_bv (inc, lev, f$t) = 
0  701 
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) 
702 
 incr_bv (inc, lev, u) = u; 

703 

704 
fun incr_boundvars 0 t = t 

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

706 

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

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

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

711 
else (x,y)::al) 

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

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

714 

715 
(* strip abstractions created by parameters *) 

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

717 

718 
fun rename_abs pat obj t = 

719 
let 

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

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

18942  722 
Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b) 
12981  723 
 ren_abs (f $ t) = ren_abs f $ ren_abs t 
724 
 ren_abs t = t 

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

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

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

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

730 
if i<lev then js else (ilev) ins_int js 
0  731 
 add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js) 
732 
 add_loose_bnos (f$t, lev, js) = 

13000  733 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
0  734 
 add_loose_bnos (_, _, js) = js; 
735 

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

737 

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

739 
level k or beyond. *) 

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

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

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

743 
 loose_bvar _ = false; 

744 

2792  745 
fun loose_bvar1(Bound i,k) = i = k 
746 
 loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k) 

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

748 
 loose_bvar1 _ = false; 

0  749 

750 
(*Substitute arguments for loose bound variables. 

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

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

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

756 
*) 

13000  757 
fun subst_bounds (args: term list, t) : term = 
19065  758 
let 
759 
exception SAME; 

760 
val n = length args; 

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

762 
(if i < lev then raise SAME (*var is locally bound*) 

763 
else incr_boundvars lev (List.nth (args, i  lev)) 

764 
handle Subscript => Bound (i  n)) (*loose: change it*) 

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

766 
 subst (f $ t, lev) = 

767 
(subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev)) 

768 
 subst _ = raise SAME; 

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

0  770 

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

771 
(*Special case: one argument*) 
13000  772 
fun subst_bound (arg, t) : term = 
19065  773 
let 
774 
exception SAME; 

775 
fun subst (Bound i, lev) = 

776 
if i < lev then raise SAME (*var is locally bound*) 

777 
else if i = lev then incr_boundvars lev arg 

778 
else Bound (i  1) (*loose: change it*) 

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

780 
 subst (f $ t, lev) = 

781 
(subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev)) 

782 
 subst _ = raise SAME; 

783 
in subst (t, 0) handle SAME => t end; 

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

784 

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

786 
fun betapply (Abs(_,_,t), u) = subst_bound (u,t) 
0  787 
 betapply (f,u) = f$u; 
788 

18183  789 
val betapplys = Library.foldl betapply; 
790 

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

791 

20109  792 
(*unfolding abstractions with substitution 
793 
of bound variables and implicit etaexpansion*) 

794 
fun strip_abs_eta k t = 

795 
let 

20122  796 
val used = fold_aterms (fn Free (v, _) => Name.declare v  _ => I) t Name.context; 
20109  797 
fun strip_abs t (0, used) = (([], t), (0, used)) 
798 
 strip_abs (Abs (v, T, t)) (k, used) = 

799 
let 

20122  800 
val ([v'], used') = Name.variants [v] used; 
20109  801 
val t' = subst_bound (Free (v, T), t); 
20122  802 
val ((vs, t''), (k', used'')) = strip_abs t' (k  1, used'); 
803 
in (((v', T) :: vs, t''), (k', used'')) end 

20109  804 
 strip_abs t (k, used) = (([], t), (k, used)); 
805 
fun expand_eta [] t _ = ([], t) 

806 
 expand_eta (T::Ts) t used = 

807 
let 

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

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

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

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

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

815 

816 

20199  817 
(* comparing variables *) 
16882  818 

16724  819 
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

820 

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

823 

824 
val tvar_ord = prod_ord indexname_ord sort_ord; 

825 
val var_ord = prod_ord indexname_ord typ_ord; 

16882  826 

827 

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

831 
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

832 
 matchrands _ = true 
0  833 
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

834 
(_, Var _) => true 
0  835 
 (Var _, _) => true 
836 
 (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u) 

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

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

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

840 
 (_, Abs _) => true 

841 
 _ => false 

842 
end; 

843 

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

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

846 
 subst_free pairs = 

13000  847 
let fun substf u = 
17314  848 
case AList.lookup (op aconv) pairs u of 
15531  849 
SOME u' => u' 
850 
 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

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

852 
 _ => u) 
0  853 
in substf end; 
854 

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

16882  858 
fun abstract_over (v, body) = 
859 
let 

16990  860 
exception SAME; 
861 
fun abs lev tm = 

862 
if v aconv tm then Bound lev 

16882  863 
else 
16990  864 
(case tm of 
865 
Abs (a, T, t) => Abs (a, T, abs (lev + 1) t) 

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

867 
 _ => raise SAME); 

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

0  869 

18975  870 
fun lambda (v as Const (x, T)) t = Abs (NameSpace.base x, T, abstract_over (v, t)) 
18942  871 
 lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t)) 
13665  872 
 lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t)) 
873 
 lambda v t = raise TERM ("lambda", [v, t]); 

0  874 

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

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

17786  877 
fun absdummy (T, body) = Abs ("uu", T, body); 
0  878 

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

880 
fun list_abs_free ([ ] , t) = t 

13000  881 
 list_abs_free ((a,T)::vars, t) = 
0  882 
absfree(a, T, list_abs_free(vars,t)); 
883 

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

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

13000  886 
 list_all_free ((a,T)::vars, t) = 
0  887 
(all T) $ (absfree(a, T, list_all_free(vars,t))); 
888 

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

890 
fun list_all ([], t) = t 

13000  891 
 list_all ((a,T)::vars, t) = 
0  892 
(all T) $ (Abs(a, T, list_all(vars,t))); 
893 

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

898 
let 

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

900 
 subst (t $ u) = subst t $ subst u 

18942  901 
 subst t = the_default t (AList.lookup (op aconv) inst t); 
16678  902 
in subst tm end; 
0  903 

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

906 
 typ_subst_atomic inst ty = 

907 
let 

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

18942  909 
 subst T = the_default T (AList.lookup (op = : typ * typ > bool) inst T); 
16678  910 
in subst ty end; 
15797  911 

16678  912 
fun subst_atomic_types [] tm = tm 
913 
 subst_atomic_types inst tm = map_term_types (typ_subst_atomic inst) tm; 

914 

915 
fun typ_subst_TVars [] ty = ty 

916 
 typ_subst_TVars inst ty = 

917 
let 

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

18942  919 
 subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi) 
16678  920 
 subst T = T; 
921 
in subst ty end; 

0  922 

16678  923 
fun subst_TVars [] tm = tm 
924 
 subst_TVars inst tm = map_term_types (typ_subst_TVars inst) tm; 

0  925 

16678  926 
fun subst_Vars [] tm = tm 
927 
 subst_Vars inst tm = 

928 
let 

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

932 
 subst t = t; 

933 
in subst tm end; 

0  934 

16678  935 
fun subst_vars ([], []) tm = tm 
936 
 subst_vars ([], inst) tm = subst_Vars inst tm 

937 
 subst_vars (instT, inst) tm = 

938 
let 

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

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

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

17271  942 
(case AList.lookup (op =) inst xi of 
16678  943 
NONE => Var (xi, typ_subst_TVars instT T) 
944 
 SOME t => t) 

945 
 subst (t as Bound _) = t 

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

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

948 
in subst tm end; 

0  949 

950 

15573  951 
(** Identifying firstorder terms **) 
952 

20199  953 
(*Differs from proofterm/is_fun in its treatment of TVar*) 
954 
fun is_funtype (Type("fun",[_,_])) = true 

955 
 is_funtype _ = false; 

956 

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

959 

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

16667  963 
fun is_first_order quants = 
16589  964 
let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body 
16667  965 
 first_order1 Ts (Const(q,_) $ Abs(a,T,body)) = 
966 
q mem_string quants andalso (*it is a known quantifier*) 

16589  967 
not (is_funtype T) andalso first_order1 (T::Ts) body 
16667  968 
 first_order1 Ts t = 
969 
case strip_comb t of 

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

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

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

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

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

975 
 _ => error "first_order: unexpected case" 

16589  976 
in first_order1 [] end; 
15573  977 

16710  978 

16990  979 
(* maximum index of typs and terms *) 
0  980 

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

983 
 maxidx_typ (TFree _) i = i 

984 
and maxidx_typs [] i = i 

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

0  986 

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

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

990 
 maxidx_term (Bound _) i = i 

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

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

0  993 

16710  994 
fun maxidx_of_typ T = maxidx_typ T ~1; 
995 
fun maxidx_of_typs Ts = maxidx_typs Ts ~1; 

996 
fun maxidx_of_term t = maxidx_term t ~1; 

13665  997 

0  998 

999 

1000 
(**** Syntaxrelated declarations ****) 

1001 

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

1003 

19909  1004 
fun exists_subtype P = 
1005 
let 

1006 
fun ex ty = P ty orelse 

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

1008 
in ex end; 

13646  1009 

16943  1010 
fun exists_subterm P = 
1011 
let 

1012 
fun ex tm = P tm orelse 

1013 
(case tm of 

1014 
t $ u => ex t orelse ex u 

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

1016 
 _ => false); 

1017 
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

1018 

19909  1019 

1020 
(** Consts etc. **) 

1021 

1022 
fun add_term_consts (Const (c, _), cs) = insert (op =) c cs 

1023 
 add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs)) 

1024 
 add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs) 

1025 
 add_term_consts (_, cs) = cs; 

1026 

1027 
fun term_consts t = add_term_consts(t,[]); 

1028 

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

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

1031 

0  1032 
(** TFrees and TVars **) 
1033 

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

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

1035 
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

1036 
 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

1037 
 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

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

1039 

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

10666  1042 
fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs 
2176  1043 
 add_term_names (Free(a,_), bs) = a ins_string bs 
0  1044 
 add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) 
1045 
 add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) 

1046 
 add_term_names (_, bs) = bs; 

1047 

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

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

1049 
fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts 
0  1050 
 add_typ_tvars(TFree(_),vs) = vs 
16294  1051 
 add_typ_tvars(TVar(v),vs) = insert (op =) v vs; 
0  1052 

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

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

1054 
fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts 
2176  1055 
 add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs 
0  1056 
 add_typ_tfree_names(TVar(_),fs) = fs; 
1057 

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

1058 
fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts 
16294  1059 
 add_typ_tfrees(TFree(f),fs) = insert (op =) f fs 
0  1060 
 add_typ_tfrees(TVar(_),fs) = fs; 
1061 

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

1062 
fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts 
2176  1063 
 add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms 
1064 
 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

1065 

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

1068 

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

1070 
val add_term_tfrees = it_term_types add_typ_tfrees; 

1071 
val add_term_tfree_names = it_term_types add_typ_tfree_names; 

1072 

1073 
(*Nonlist versions*) 

1074 
fun typ_tfrees T = add_typ_tfrees(T,[]); 

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

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

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

1078 

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

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

1080 

15570  1081 
fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts) 
20082
b0f5981b9267
removed obsolete ins_ix, mem_ix, ins_term, mem_term;
wenzelm
parents:
20001
diff
changeset

1082 
 add_typ_ixns(ixns,TVar(ixn,_)) = if member (op =) ixns ixn then ixns 
9536
b79b002f32ae
added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
wenzelm
parents:
9319
diff
changeset

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

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

1085 

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

1086 
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

1087 
 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

1088 
 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

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

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

1091 
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

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

1093 
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

1094 

16537  1095 

0  1096 
(** Frees and Vars **) 
1097 

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

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

16990  1100 
Var _ => OrdList.insert term_ord t vars 
0  1101 
 Abs (_,_,body) => add_term_vars(body,vars) 
1102 
 f$t => add_term_vars (f, add_term_vars(t, vars)) 

1103 
 _ => vars; 

1104 

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

1106 

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

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

16990  1109 
Free _ => OrdList.insert term_ord t frees 
0  1110 
 Abs (_,_,body) => add_term_frees(body,frees) 
1111 
 f$t => add_term_frees (f, add_term_frees(t, frees)) 

1112 
 _ => frees; 

1113 

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

1115 

20199  1116 

1117 
(* dest abstraction *) 

0  1118 

16678  1119 
fun dest_abs (x, T, body) = 
1120 
let 

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

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

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

1124 
 name_clash _ = false; 

1125 
in 

1126 
if name_clash body then 

20082
b0f5981b9267
removed obsolete ins_ix, mem_ix, ins_term, mem_term;
wenzelm
parents:
20001
diff
changeset

1127 
dest_abs (Name.variant [x] x, T, body) (*potentially slow, but rarely happens*) 
16678  1128 
else (x, subst_bound (Free (x, T), body)) 
1129 
end; 

1130 

20160  1131 

1132 
(* renaming variables *) 

0  1133 

20239  1134 
fun declare_term_names tm = 
1135 
fold_aterms 

1136 
(fn Const (a, _) => Name.declare (NameSpace.base a) 

1137 
 Free (a, _) => Name.declare a 

1138 
 _ => I) tm #> 

1139 
fold_types (fold_atyps (fn TFree (a, _) => Name.declare a  _ => I)) tm; 

1140 

20160  1141 
fun variant_frees t frees = 
1142 
fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees; 

1143 

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

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

1145 

1417  1146 

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

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

1148 

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

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

1150 

18253  1151 
fun dummy_pattern T = Const (dummy_patternN, T); 
1152 

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

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

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

1155 

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

1156 
fun no_dummy_patterns tm = 
16787  1157 
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

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

1159 

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

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

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

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

1165 
 replace_dummy Ts (i, t $ u) = 

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

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

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

1169 

1170 
val replace_dummy_patterns = replace_dummy []; 

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

1171 

10552  1172 
fun is_replaced_dummy_pattern ("_dummy_", _) = true 
1173 
 is_replaced_dummy_pattern _ = false; 

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

1174 

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

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

1178 
 show_dummy_patterns a = a; 

1179 

13484  1180 

20100  1181 
(* display variables *) 
1182 

15986  1183 
val show_question_marks = ref true; 
15472  1184 

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

1185 
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

1186 
let 
15986  1187 
val question_mark = if ! show_question_marks then "?" else ""; 
1188 
val idx = string_of_int i; 

1189 
val dot = 

1190 
(case rev (Symbol.explode x) of 

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

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

1193 
 c :: _ => Symbol.is_digit c 

1194 
 _ => true); 

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

1195 
in 
15986  1196 
if dot then question_mark ^ x ^ "." ^ idx 
1197 
else if i <> 0 then question_mark ^ x ^ idx 

1198 
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

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

1200 

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

1201 
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

1202 
 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

1203 

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

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

1205 

4444  1206 
structure BasicTerm: BASIC_TERM = Term; 
1207 
open BasicTerm; 