3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Copyright Cambridge University 1992
6 Simply typed lambda-calculus: types, terms, and basic operations.
14 signature BASIC_TERM =
21 Type of string * typ list |
22 TFree of string * sort |
23 TVar of indexname * sort
25 Const of string * typ |
26 Free of string * typ |
27 Var of indexname * typ |
29 Abs of string * typ * term |
31 exception TYPE of string * typ list * term list
32 exception TERM of string * term list
35 val no_dummyT: typ -> typ
36 val --> : typ * typ -> typ
37 val ---> : typ list * typ -> typ
38 val dest_Type: typ -> string * typ list
39 val dest_TVar: typ -> indexname * sort
40 val dest_TFree: typ -> string * sort
41 val is_Bound: term -> bool
42 val is_Const: term -> bool
43 val is_Free: term -> bool
44 val is_Var: term -> bool
45 val is_TVar: typ -> bool
46 val dest_Const: term -> string * typ
47 val dest_Free: term -> string * typ
48 val dest_Var: term -> indexname * typ
49 val domain_type: typ -> typ
50 val range_type: typ -> typ
51 val binder_types: typ -> typ list
52 val body_type: typ -> typ
53 val strip_type: typ -> typ list * typ
54 val type_of1: typ list * term -> typ
55 val type_of: term -> typ
56 val fastype_of1: typ list * term -> typ
57 val fastype_of: term -> typ
58 val list_abs: (string * typ) list * term -> term
59 val strip_abs: term -> (string * typ) list * term
60 val strip_abs_body: term -> term
61 val strip_abs_vars: term -> (string * typ) list
62 val strip_qnt_body: string -> term -> term
63 val strip_qnt_vars: string -> term -> (string * typ) list
64 val list_comb: term * term list -> term
65 val strip_comb: term -> term * term list
66 val head_of: term -> term
67 val size_of_term: term -> int
68 val map_atyps: (typ -> typ) -> typ -> typ
69 val map_aterms: (term -> term) -> term -> term
70 val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
71 val map_type_tfree: (string * sort -> typ) -> typ -> typ
72 val map_types: (typ -> typ) -> term -> term
73 val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
74 val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
75 val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
76 val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
77 val burrow_types: (typ list -> typ list) -> term list -> term list
78 val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
79 val add_term_names: term * string list -> string list
80 val aconv: term * term -> bool
81 structure Vartab: TABLE
82 structure Typtab: TABLE
83 structure Termtab: TABLE
87 val equals: typ -> term
88 val strip_all_body: term -> term
89 val strip_all_vars: term -> (string * typ) list
90 val incr_bv: int * int * term -> term
91 val incr_boundvars: int -> term -> term
92 val add_loose_bnos: term * int * int list -> int list
93 val loose_bnos: term -> int list
94 val loose_bvar: term * int -> bool
95 val loose_bvar1: term * int -> bool
96 val subst_bounds: term list * term -> term
97 val subst_bound: term * term -> term
98 val betapply: term * term -> term
99 val betapplys: term * term list -> term
100 val eq_ix: indexname * indexname -> bool
101 val could_unify: term * term -> bool
102 val subst_free: (term * term) list -> term -> term
103 val abstract_over: term * term -> term
104 val lambda: term -> term -> term
105 val absfree: string * typ * term -> term
106 val absdummy: typ * term -> term
107 val list_abs_free: (string * typ) list * term -> term
108 val list_all_free: (string * typ) list * term -> term
109 val list_all: (string * typ) list * term -> term
110 val subst_atomic: (term * term) list -> term -> term
111 val typ_subst_atomic: (typ * typ) list -> typ -> typ
112 val subst_atomic_types: (typ * typ) list -> term -> term
113 val typ_subst_TVars: (indexname * typ) list -> typ -> typ
114 val subst_TVars: (indexname * typ) list -> term -> term
115 val subst_Vars: (indexname * term) list -> term -> term
116 val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
117 val is_first_order: string list -> term -> bool
118 val maxidx_of_typ: typ -> int
119 val maxidx_of_typs: typ list -> int
120 val maxidx_of_term: term -> int
121 val add_term_consts: term * string list -> string list
122 val term_consts: term -> string list
123 val exists_subtype: (typ -> bool) -> typ -> bool
124 val exists_type: (typ -> bool) -> term -> bool
125 val exists_subterm: (term -> bool) -> term -> bool
126 val exists_Const: (string * typ -> bool) -> term -> bool
127 val add_term_free_names: term * string list -> string list
128 val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
129 val add_typ_tfree_names: typ * string list -> string list
130 val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
131 val add_typ_varnames: typ * string list -> string list
132 val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
133 val add_term_tfrees: term * (string * sort) list -> (string * sort) list
134 val add_term_tfree_names: term * string list -> string list
135 val typ_tfrees: typ -> (string * sort) list
136 val typ_tvars: typ -> (indexname * sort) list
137 val term_tfrees: term -> (string * sort) list
138 val term_tvars: term -> (indexname * sort) list
139 val add_typ_ixns: indexname list * typ -> indexname list
140 val add_term_tvar_ixns: term * indexname list -> indexname list
141 val add_term_vars: term * term list -> term list
142 val term_vars: term -> term list
143 val add_term_frees: term * term list -> term list
144 val term_frees: term -> term list
145 val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
146 val show_question_marks: bool ref
153 val itselfT: typ -> typ
155 val argument_type_of: term -> int -> typ
156 val head_name_of: term -> string
157 val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
158 val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
159 val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
160 val add_varnames: term -> indexname list -> indexname list
161 val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
162 val add_tfrees: term -> (string * sort) list -> (string * sort) list
163 val add_frees: term -> (string * typ) list -> (string * typ) list
164 val hidden_polymorphism: term -> typ -> (indexname * sort) list
165 val equiv_types: term * term -> bool
166 val strip_abs_eta: int -> term -> (string * typ) list * term
167 val fast_indexname_ord: indexname * indexname -> order
168 val indexname_ord: indexname * indexname -> order
169 val sort_ord: sort * sort -> order
170 val typ_ord: typ * typ -> order
171 val fast_term_ord: term * term -> order
172 val term_ord: term * term -> order
173 val hd_ord: term * term -> order
174 val termless: term * term -> bool
175 val term_lpo: (term -> int) -> term * term -> order
176 val match_bvars: (term * term) * (string * string) list -> (string * string) list
177 val map_abs_vars: (string -> string) -> term -> term
178 val rename_abs: term -> term -> term -> term option
179 val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
180 val eq_var: (indexname * typ) * (indexname * typ) -> bool
181 val tvar_ord: (indexname * sort) * (indexname * sort) -> order
182 val var_ord: (indexname * typ) * (indexname * typ) -> order
183 val maxidx_typ: typ -> int -> int
184 val maxidx_typs: typ list -> int -> int
185 val maxidx_term: term -> int -> int
186 val has_abs: term -> bool
187 val dest_abs: string * typ * term -> string * term
188 val declare_term_names: term -> Name.context -> Name.context
189 val variant_frees: term -> (string * 'a) list -> (string * 'a) list
190 val dummy_patternN: string
191 val dummy_pattern: typ -> term
192 val is_dummy_pattern: term -> bool
193 val no_dummy_patterns: term -> term
194 val replace_dummy_patterns: int * term -> int * term
195 val is_replaced_dummy_pattern: indexname -> bool
196 val show_dummy_patterns: term -> term
197 val string_of_vname: indexname -> string
198 val string_of_vname': indexname -> string
201 structure Term: TERM =
204 (*Indexnames can be quickly renamed by adding an offset to the integer part,
206 type indexname = string * int;
208 (* Types are classified by sorts. *)
210 type sort = class list;
211 type arity = string * sort list * sort;
213 (* The sorts attached to TFrees and TVars specify the sort of that variable *)
214 datatype typ = Type of string * typ list
215 | TFree of string * sort
216 | TVar of indexname * sort;
218 (*Terms. Bound variables are indicated by depth number.
219 Free variables, (scheme) variables and constants have names.
220 An term is "closed" if every bound variable of level "lev"
221 is enclosed by at least "lev" abstractions.
223 It is possible to create meaningless terms containing loose bound vars
224 or type mismatches. But such terms are not allowed in rules. *)
227 Const of string * typ
228 | Free of string * typ
229 | Var of indexname * typ
231 | Abs of string*typ*term
234 (*Errors involving type mismatches*)
235 exception TYPE of string * typ list * term list;
237 (*Errors errors involving terms*)
238 exception TERM of string * term list;
240 (*Note variable naming conventions!
242 f,g,h: functions (including terms of function type)
247 A,B,C: term (denoting formulae)
254 (*dummies for type-inference etc.*)
256 val dummyT = Type ("dummy", []);
260 fun check (T as Type ("dummy", _)) =
261 raise TYPE ("Illegal occurrence of '_' dummy type", [T], [])
262 | check (Type (_, Ts)) = List.app check Ts
264 in check typ; typ end;
266 fun S --> T = Type("fun",[S,T]);
268 (*handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)*)
269 val op ---> = Library.foldr (op -->);
271 fun dest_Type (Type x) = x
272 | dest_Type T = raise TYPE ("dest_Type", [T], []);
273 fun dest_TVar (TVar x) = x
274 | dest_TVar T = raise TYPE ("dest_TVar", [T], []);
275 fun dest_TFree (TFree x) = x
276 | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
279 (** Discriminators **)
281 fun is_Bound (Bound _) = true
282 | is_Bound _ = false;
284 fun is_Const (Const _) = true
285 | is_Const _ = false;
287 fun is_Free (Free _) = true
290 fun is_Var (Var _) = true
293 fun is_TVar (TVar _) = true
299 fun dest_Const (Const x) = x
300 | dest_Const t = raise TERM("dest_Const", [t]);
302 fun dest_Free (Free x) = x
303 | dest_Free t = raise TERM("dest_Free", [t]);
305 fun dest_Var (Var x) = x
306 | dest_Var t = raise TERM("dest_Var", [t]);
309 fun domain_type (Type("fun", [T,_])) = T
310 and range_type (Type("fun", [_,T])) = T;
312 (* maps [T1,...,Tn]--->T to the list [T1,T2,...,Tn]*)
313 fun binder_types (Type("fun",[S,T])) = S :: binder_types T
314 | binder_types _ = [];
316 (* maps [T1,...,Tn]--->T to T*)
317 fun body_type (Type("fun",[S,T])) = body_type T
320 (* maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T) *)
321 fun strip_type T : typ list * typ =
322 (binder_types T, body_type T);
325 (*Compute the type of the term, checking that combinations are well-typed
326 Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
327 fun type_of1 (Ts, Const (_,T)) = T
328 | type_of1 (Ts, Free (_,T)) = T
329 | type_of1 (Ts, Bound i) = (List.nth (Ts,i)
330 handle Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
331 | type_of1 (Ts, Var (_,T)) = T
332 | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
333 | type_of1 (Ts, f$u) =
334 let val U = type_of1(Ts,u)
335 and T = type_of1(Ts,f)
337 Type("fun",[T1,T2]) =>
338 if T1=U then T2 else raise TYPE
339 ("type_of: type mismatch in application", [T1,U], [f$u])
341 ("type_of: function type is expected in application",
345 fun type_of t : typ = type_of1 ([],t);
347 (*Determines the type of a term, with minimal checking*)
348 fun fastype_of1 (Ts, f$u) =
349 (case fastype_of1 (Ts,f) of
350 Type("fun",[_,T]) => T
351 | _ => raise TERM("fastype_of: expected function type", [f$u]))
352 | fastype_of1 (_, Const (_,T)) = T
353 | fastype_of1 (_, Free (_,T)) = T
354 | fastype_of1 (Ts, Bound i) = (List.nth(Ts,i)
355 handle Subscript => raise TERM("fastype_of: Bound", [Bound i]))
356 | fastype_of1 (_, Var (_,T)) = T
357 | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
359 fun fastype_of t : typ = fastype_of1 ([],t);
361 (*Determine the argument type of a function*)
362 fun argument_type_of tm k =
364 fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i - 1) U
365 | argT _ T = raise TYPE ("argument_type_of", [T], []);
367 fun arg 0 _ (Abs (_, T, _)) = T
368 | arg i Ts (Abs (_, T, t)) = arg (i - 1) (T :: Ts) t
369 | arg i Ts (t $ _) = arg (i + 1) Ts t
370 | arg i Ts a = argT i (fastype_of1 (Ts, a));
374 val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t)));
376 fun strip_abs (Abs (a, T, t)) =
377 let val (a', t') = strip_abs t
378 in ((a, T) :: a', t') end
379 | strip_abs t = ([], t);
381 (* maps (x1,...,xn)t to t *)
382 fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t
383 | strip_abs_body u = u;
385 (* maps (x1,...,xn)t to [x1, ..., xn] *)
386 fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t
387 | strip_abs_vars u = [] : (string*typ) list;
390 fun strip_qnt_body qnt =
391 let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
395 fun strip_qnt_vars qnt =
396 let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
397 | strip t = [] : (string*typ) list
401 (* maps (f, [t1,...,tn]) to f(t1,...,tn) *)
402 val list_comb : term * term list -> term = Library.foldl (op $);
405 (* maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tail-recursive*)
406 fun strip_comb u : term * term list =
407 let fun stripc (f$t, ts) = stripc (f, t::ts)
412 (* maps f(t1,...,tn) to f , which is never a combination *)
413 fun head_of (f$t) = head_of f
416 fun head_name_of tm =
419 if NameSpace.is_qualified c then c
420 else raise TERM ("Malformed constant name", [t])
421 | t as Free (x, _) =>
422 if not (NameSpace.is_qualified x) then x
423 else raise TERM ("Malformed fixed variable name", [t])
424 | t => raise TERM ("No fixed head of term", [t]));
426 (*number of atoms and abstractions in a term*)
427 fun size_of_term tm =
429 fun add_size (t $ u, n) = add_size (t, add_size (u, n))
430 | add_size (Abs (_ ,_, t), n) = add_size (t, n + 1)
431 | add_size (_, n) = n + 1;
432 in add_size (tm, 0) end;
434 fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
435 | map_atyps f T = f T;
437 fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u
438 | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
439 | map_aterms f t = f t;
441 fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
442 fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
446 fun map_aux (Const (a, T)) = Const (a, f T)
447 | map_aux (Free (a, T)) = Free (a, f T)
448 | map_aux (Var (v, T)) = Var (v, f T)
449 | map_aux (t as Bound _) = t
450 | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t)
451 | map_aux (t $ u) = map_aux t $ map_aux u;
454 (* iterate a function over all types in a term *)
455 fun it_term_types f =
456 let fun iter(Const(_,T), a) = f(T,a)
457 | iter(Free(_,T), a) = f(T,a)
458 | iter(Var(_,T), a) = f(T,a)
459 | iter(Abs(_,T,t), a) = iter(t,f(T,a))
460 | iter(f$u, a) = iter(f, iter(u, a))
461 | iter(Bound _, a) = a
465 (* fold types and terms *)
467 (*fold atoms of type*)
468 fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
469 | fold_atyps f T = f T;
471 (*fold atoms of term*)
472 fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
473 | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
474 | fold_aterms f a = f a;
476 (*fold types of term*)
477 fun fold_term_types f (t as Const (_, T)) = f t T
478 | fold_term_types f (t as Free (_, T)) = f t T
479 | fold_term_types f (t as Var (_, T)) = f t T
480 | fold_term_types f (Bound _) = I
481 | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b
482 | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u;
484 fun fold_types f = fold_term_types (K f);
486 fun replace_types (Const (c, _)) (T :: Ts) = (Const (c, T), Ts)
487 | replace_types (Free (x, _)) (T :: Ts) = (Free (x, T), Ts)
488 | replace_types (Var (xi, _)) (T :: Ts) = (Var (xi, T), Ts)
489 | replace_types (Bound i) Ts = (Bound i, Ts)
490 | replace_types (Abs (x, _, b)) (T :: Ts) =
491 let val (b', Ts') = replace_types b Ts
492 in (Abs (x, T, b'), Ts') end
493 | replace_types (t $ u) Ts =
495 val (t', Ts') = replace_types t Ts;
496 val (u', Ts'') = replace_types u Ts';
497 in (t' $ u', Ts'') end;
499 fun burrow_types f ts =
501 val Ts = rev (fold (fold_types cons) ts []);
503 val (ts', []) = fold_map replace_types ts Ts';
506 (*collect variables*)
507 val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
508 val add_tvars = fold_types add_tvarsT;
509 val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
510 val add_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
511 val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
512 val add_tfrees = fold_types add_tfreesT;
513 val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
515 (*extra type variables in a term, not covered by the type*)
516 fun hidden_polymorphism t T =
518 val tvarsT = add_tvarsT T [];
519 val extra_tvars = fold_types (fold_atyps
520 (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
524 (** Comparing terms, types, sorts etc. **)
526 (* alpha equivalence -- tuned for equalities *)
529 pointer_eq (tm1, tm2) orelse
531 (t1 $ u1, t2 $ u2) => t1 aconv t2 andalso u1 aconv u2
532 | (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2
533 | (a1, a2) => a1 = a2);
536 (* equivalence up to renaming of types variables *)
540 val invent_names = Name.invents Name.context "'a";
542 fun standard_types t =
544 val tfrees = add_tfrees t [];
545 val tvars = add_tvars t [];
546 val env1 = map2 (fn (a, S) => fn a' => (TFree (a, S), TFree (a', [])))
547 tfrees (invent_names (length tfrees));
548 val env2 = map2 (fn ((a, i), S) => fn a' => (TVar ((a, i), S), TVar ((a', 0), [])))
549 tvars (invent_names (length tvars));
550 in map_types (map_atyps (perhaps (AList.lookup (op =) (env1 @ env2)))) t end;
554 val equiv_types = op aconv o pairself standard_types;
559 (* fast syntactic ordering -- tuned for inequalities *)
561 fun fast_indexname_ord ((x, i), (y, j)) =
562 (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord);
565 if pointer_eq SS then EQUAL
566 else dict_ord fast_string_ord SS;
570 fun cons_nr (TVar _) = 0
571 | cons_nr (TFree _) = 1
572 | cons_nr (Type _) = 2;
577 if pointer_eq TU then EQUAL
580 (Type (a, Ts), Type (b, Us)) =>
581 (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord)
582 | (TFree (a, S), TFree (b, S')) =>
583 (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord)
584 | (TVar (xi, S), TVar (yj, S')) =>
585 (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord)
586 | (T, U) => int_ord (cons_nr T, cons_nr U));
592 fun cons_nr (Const _) = 0
593 | cons_nr (Free _) = 1
594 | cons_nr (Var _) = 2
595 | cons_nr (Bound _) = 3
596 | cons_nr (Abs _) = 4
597 | cons_nr (_ $ _) = 5;
599 fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u)
600 | struct_ord (t1 $ t2, u1 $ u2) =
601 (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord)
602 | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u);
604 fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u)
605 | atoms_ord (t1 $ t2, u1 $ u2) =
606 (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord)
607 | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b)
608 | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
609 | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
610 | atoms_ord (Bound i, Bound j) = int_ord (i, j)
611 | atoms_ord _ = sys_error "atoms_ord";
613 fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
614 (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
615 | types_ord (t1 $ t2, u1 $ u2) =
616 (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord)
617 | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
618 | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
619 | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
620 | types_ord (Bound _, Bound _) = EQUAL
621 | types_ord _ = sys_error "types_ord";
625 fun fast_term_ord tu =
626 if pointer_eq tu then EQUAL
628 (case struct_ord tu of
629 EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
632 structure Vartab = TableFun(type key = indexname val ord = fast_indexname_ord);
633 structure Typtab = TableFun(type key = typ val ord = typ_ord);
634 structure Termtab = TableFun(type key = term val ord = fast_term_ord);
641 (*a linear well-founded AC-compatible ordering for terms:
642 s < t <=> 1. size(s) < size(t) or
643 2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
644 3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
645 (s1..sn) < (t1..tn) (lexicographically)*)
647 fun indexname_ord ((x, i), (y, j)) =
648 (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
652 fun hd_depth (t $ _, n) = hd_depth (t, n + 1)
655 fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
656 | dest_hd (Free (a, T)) = (((a, 0), T), 1)
657 | dest_hd (Var v) = (v, 2)
658 | dest_hd (Bound i) = ((("", i), dummyT), 3)
659 | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
664 if pointer_eq tu then EQUAL
667 (Abs (_, T, t), Abs(_, U, u)) =>
668 (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
670 (case int_ord (size_of_term t, size_of_term u) of
672 (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of
673 EQUAL => args_ord (t, u) | ord => ord)
676 prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
677 and args_ord (f $ t, g $ u) =
678 (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord)
679 | args_ord _ = EQUAL;
681 fun termless tu = (term_ord tu = LESS);
686 (** Lexicographic path order on terms **)
689 See Baader & Nipkow, Term rewriting, CUP 1998.
690 Without variables. Const, Var, Bound, Free and Abs are treated all as
693 f_ord maps terms to integers and serves two purposes:
694 - Predicate on constant symbols. Those that are not recognised by f_ord
695 must be mapped to ~1.
696 - Order on the recognised symbols. These must be mapped to distinct
698 The argument of f_ord is never an application.
703 fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0)
704 | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0)
705 | unrecognized (Var v) = ((1, v), 1)
706 | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2)
707 | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
709 fun dest_hd f_ord t =
710 let val ord = f_ord t in
711 if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0)
714 fun term_lpo f_ord (s, t) =
715 let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
716 if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
717 then case hd_ord f_ord (f, g) of
719 if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
720 then GREATER else LESS
722 if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
723 then list_ord (term_lpo f_ord) (ss, ts)
728 and hd_ord f_ord (f, g) = case (f, g) of
729 (Abs (_, T, t), Abs (_, U, u)) =>
730 (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
731 | (_, _) => prod_ord (prod_ord int_ord
732 (prod_ord indexname_ord typ_ord)) int_ord
733 (dest_hd f_ord f, dest_hd f_ord g)
735 val term_lpo = term_lpo
739 (** Connectives of higher order logic **)
741 fun aT S = TFree ("'a", S);
743 fun itselfT ty = Type ("itself", [ty]);
744 val a_itselfT = itselfT (TFree ("'a", []));
746 val propT : typ = Type("prop",[]);
748 val implies = Const("==>", propT-->propT-->propT);
750 fun all T = Const("all", (T-->propT)-->propT);
752 fun equals T = Const("==", T-->T-->propT);
754 (* maps !!x1...xn. t to t *)
755 fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t
756 | strip_all_body t = t;
758 (* maps !!x1...xn. t to [x1, ..., xn] *)
759 fun strip_all_vars (Const("all",_)$Abs(a,T,t)) =
760 (a,T) :: strip_all_vars t
761 | strip_all_vars t = [] : (string*typ) list;
763 (*increments a term's non-local bound variables
764 required when moving a term within abstractions
765 inc is increment for bound variables
766 lev is level at which a bound variable is considered 'loose'*)
767 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
768 | incr_bv (inc, lev, Abs(a,T,body)) =
769 Abs(a, T, incr_bv(inc,lev+1,body))
770 | incr_bv (inc, lev, f$t) =
771 incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
772 | incr_bv (inc, lev, u) = u;
774 fun incr_boundvars 0 t = t
775 | incr_boundvars inc t = incr_bv(inc,0,t);
777 (*Scan a pair of terms; while they are similar,
778 accumulate corresponding bound vars in "al"*)
779 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
780 match_bvs(s, t, if x="" orelse y="" then al
782 | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
783 | match_bvs(_,_,al) = al;
785 (* strip abstractions created by parameters *)
786 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
788 fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u
789 | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t)
790 | map_abs_vars f t = t;
792 fun rename_abs pat obj t =
794 val ren = match_bvs (pat, obj, []);
795 fun ren_abs (Abs (x, T, b)) =
796 Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b)
797 | ren_abs (f $ t) = ren_abs f $ ren_abs t
799 in if null ren then NONE else SOME (ren_abs t) end;
801 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
802 (Bound 0) is loose at level 0 *)
803 fun add_loose_bnos (Bound i, lev, js) =
804 if i<lev then js else insert (op =) (i - lev) js
805 | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
806 | add_loose_bnos (f$t, lev, js) =
807 add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
808 | add_loose_bnos (_, _, js) = js;
810 fun loose_bnos t = add_loose_bnos (t, 0, []);
812 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
813 level k or beyond. *)
814 fun loose_bvar(Bound i,k) = i >= k
815 | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
816 | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
817 | loose_bvar _ = false;
819 fun loose_bvar1(Bound i,k) = i = k
820 | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
821 | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
822 | loose_bvar1 _ = false;
824 (*Substitute arguments for loose bound variables.
825 Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
826 Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
827 and the appropriate call is subst_bounds([b,a], c) .
828 Loose bound variables >=n are reduced by "n" to
829 compensate for the disappearance of lambdas.
831 fun subst_bounds (args: term list, t) : term =
835 fun subst (t as Bound i, lev) =
836 (if i < lev then raise SAME (*var is locally bound*)
837 else incr_boundvars lev (List.nth (args, i - lev))
838 handle Subscript => Bound (i - n)) (*loose: change it*)
839 | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
840 | subst (f $ t, lev) =
841 (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
842 | subst _ = raise SAME;
843 in case args of [] => t | _ => (subst (t, 0) handle SAME => t) end;
845 (*Special case: one argument*)
846 fun subst_bound (arg, t) : term =
849 fun subst (Bound i, lev) =
850 if i < lev then raise SAME (*var is locally bound*)
851 else if i = lev then incr_boundvars lev arg
852 else Bound (i - 1) (*loose: change it*)
853 | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
854 | subst (f $ t, lev) =
855 (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
856 | subst _ = raise SAME;
857 in subst (t, 0) handle SAME => t end;
859 (*beta-reduce if possible, else form application*)
860 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
861 | betapply (f,u) = f$u;
863 val betapplys = Library.foldl betapply;
866 (*unfolding abstractions with substitution
867 of bound variables and implicit eta-expansion*)
868 fun strip_abs_eta k t =
870 val used = fold_aterms (fn Free (v, _) => Name.declare v | _ => I) t Name.context;
871 fun strip_abs t (0, used) = (([], t), (0, used))
872 | strip_abs (Abs (v, T, t)) (k, used) =
874 val ([v'], used') = Name.variants [v] used;
875 val t' = subst_bound (Free (v', T), t);
876 val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
877 in (((v', T) :: vs, t''), (k', used'')) end
878 | strip_abs t (k, used) = (([], t), (k, used));
879 fun expand_eta [] t _ = ([], t)
880 | expand_eta (T::Ts) t used =
882 val ([v], used') = Name.variants [""] used;
883 val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
884 in ((v, T) :: vs, t') end;
885 val ((vs1, t'), (k', used')) = strip_abs t (k, used);
886 val Ts = (fst o chop k' o fst o strip_type o fastype_of) t';
887 val (vs2, t'') = expand_eta Ts t' used';
888 in (vs1 @ vs2, t'') end;
891 (* comparing variables *)
893 fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
895 fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
896 fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
898 val tvar_ord = prod_ord indexname_ord sort_ord;
899 val var_ord = prod_ord indexname_ord typ_ord;
902 (*A fast unification filter: true unless the two terms cannot be unified.
903 Terms must be NORMAL. Treats all Vars as distinct. *)
904 fun could_unify (t,u) =
905 let fun matchrands (f$t, g$u) = could_unify(t,u) andalso matchrands(f,g)
906 | matchrands _ = true
907 in case (head_of t , head_of u) of
910 | (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u)
911 | (Free(a,_), Free(b,_)) => a=b andalso matchrands(t,u)
912 | (Bound i, Bound j) => i=j andalso matchrands(t,u)
913 | (Abs _, _) => true (*because of possible eta equality*)
918 (*Substitute new for free occurrences of old in a term*)
919 fun subst_free [] = (fn t=>t)
922 case AList.lookup (op aconv) pairs u of
924 | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
925 | t$u' => substf t $ substf u'
929 (*Abstraction of the term "body" over its occurrences of v,
930 which must contain no loose bound variables.
931 The resulting term is ready to become the body of an Abs.*)
932 fun abstract_over (v, body) =
936 if v aconv tm then Bound lev
939 Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
940 | t $ u => (abs lev t $ (abs lev u handle SAME => u) handle SAME => t $ abs lev u)
942 in abs 0 body handle SAME => body end;
947 Const (x, _) => NameSpace.base x
949 | Var ((x, _), _) => x
951 in Abs (x, fastype_of v, abstract_over (v, t)) end;
953 (*Form an abstraction over a free variable.*)
954 fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
955 fun absdummy (T, body) = Abs (Name.internal "uu", T, body);
957 (*Abstraction over a list of free variables*)
958 fun list_abs_free ([ ] , t) = t
959 | list_abs_free ((a,T)::vars, t) =
960 absfree(a, T, list_abs_free(vars,t));
962 (*Quantification over a list of free variables*)
963 fun list_all_free ([], t: term) = t
964 | list_all_free ((a,T)::vars, t) =
965 (all T) $ (absfree(a, T, list_all_free(vars,t)));
967 (*Quantification over a list of variables (already bound in body) *)
968 fun list_all ([], t) = t
969 | list_all ((a,T)::vars, t) =
970 (all T) $ (Abs(a, T, list_all(vars,t)));
972 (*Replace the ATOMIC term ti by ui; inst = [(t1,u1), ..., (tn,un)].
973 A simultaneous substitution: [ (a,b), (b,a) ] swaps a and b. *)
974 fun subst_atomic [] tm = tm
975 | subst_atomic inst tm =
977 fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
978 | subst (t $ u) = subst t $ subst u
979 | subst t = the_default t (AList.lookup (op aconv) inst t);
982 (*Replace the ATOMIC type Ti by Ui; inst = [(T1,U1), ..., (Tn,Un)].*)
983 fun typ_subst_atomic [] ty = ty
984 | typ_subst_atomic inst ty =
986 fun subst (Type (a, Ts)) = Type (a, map subst Ts)
987 | subst T = the_default T (AList.lookup (op = : typ * typ -> bool) inst T);
990 fun subst_atomic_types [] tm = tm
991 | subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm;
993 fun typ_subst_TVars [] ty = ty
994 | typ_subst_TVars inst ty =
996 fun subst (Type (a, Ts)) = Type (a, map subst Ts)
997 | subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi)
1001 fun subst_TVars [] tm = tm
1002 | subst_TVars inst tm = map_types (typ_subst_TVars inst) tm;
1004 fun subst_Vars [] tm = tm
1005 | subst_Vars inst tm =
1007 fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi)
1008 | subst (Abs (a, T, t)) = Abs (a, T, subst t)
1009 | subst (t $ u) = subst t $ subst u
1013 fun subst_vars ([], []) tm = tm
1014 | subst_vars ([], inst) tm = subst_Vars inst tm
1015 | subst_vars (instT, inst) tm =
1017 fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
1018 | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
1019 | subst (t as Var (xi, T)) =
1020 (case AList.lookup (op =) inst xi of
1021 NONE => Var (xi, typ_subst_TVars instT T)
1023 | subst (t as Bound _) = t
1024 | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t)
1025 | subst (t $ u) = subst t $ subst u;
1029 (** Identifying first-order terms **)
1031 (*Differs from proofterm/is_fun in its treatment of TVar*)
1032 fun is_funtype (Type("fun",[_,_])) = true
1033 | is_funtype _ = false;
1035 (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
1036 fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t)));
1038 (*First order means in all terms of the form f(t1,...,tn) no argument has a
1039 function type. The supplied quantifiers are excluded: their argument always
1040 has a function type through a recursive call into its body.*)
1041 fun is_first_order quants =
1042 let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
1043 | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
1044 member (op =) quants q andalso (*it is a known quantifier*)
1045 not (is_funtype T) andalso first_order1 (T::Ts) body
1046 | first_order1 Ts t =
1047 case strip_comb t of
1048 (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
1049 | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
1050 | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
1051 | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
1052 | (Abs _, ts) => false (*not in beta-normal form*)
1053 | _ => error "first_order: unexpected case"
1054 in first_order1 [] end;
1057 (* maximum index of typs and terms *)
1059 fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j)
1060 | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i
1061 | maxidx_typ (TFree _) i = i
1062 and maxidx_typs [] i = i
1063 | maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i);
1065 fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j))
1066 | maxidx_term (Const (_, T)) i = maxidx_typ T i
1067 | maxidx_term (Free (_, T)) i = maxidx_typ T i
1068 | maxidx_term (Bound _) i = i
1069 | maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i)
1070 | maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i);
1072 fun maxidx_of_typ T = maxidx_typ T ~1;
1073 fun maxidx_of_typs Ts = maxidx_typs Ts ~1;
1074 fun maxidx_of_term t = maxidx_term t ~1;
1078 (**** Syntax-related declarations ****)
1082 fun exists_subtype P =
1084 fun ex ty = P ty orelse
1085 (case ty of Type (_, Ts) => exists ex Ts | _ => false);
1090 fun ex (Const (_, T)) = P T
1091 | ex (Free (_, T)) = P T
1092 | ex (Var (_, T)) = P T
1093 | ex (Bound _) = false
1094 | ex (Abs (_, T, t)) = P T orelse ex t
1095 | ex (t $ u) = ex t orelse ex u;
1098 fun exists_subterm P =
1100 fun ex tm = P tm orelse
1102 t $ u => ex t orelse ex u
1103 | Abs (_, _, t) => ex t
1107 fun has_abs (Abs _) = true
1108 | has_abs (t $ u) = has_abs t orelse has_abs u
1109 | has_abs _ = false;
1115 fun add_term_consts (Const (c, _), cs) = insert (op =) c cs
1116 | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
1117 | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
1118 | add_term_consts (_, cs) = cs;
1120 fun term_consts t = add_term_consts(t,[]);
1122 fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
1125 (** TFrees and TVars **)
1127 (*Accumulates the names of Frees in the term, suppressing duplicates.*)
1128 fun add_term_free_names (Free(a,_), bs) = insert (op =) a bs
1129 | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
1130 | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
1131 | add_term_free_names (_, bs) = bs;
1133 (*Accumulates the names in the term, suppressing duplicates.
1134 Includes Frees and Consts. For choosing unambiguous bound var names.*)
1135 fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base a) bs
1136 | add_term_names (Free(a,_), bs) = insert (op =) a bs
1137 | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
1138 | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
1139 | add_term_names (_, bs) = bs;
1141 (*Accumulates the TVars in a type, suppressing duplicates. *)
1142 fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
1143 | add_typ_tvars(TFree(_),vs) = vs
1144 | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
1146 (*Accumulates the TFrees in a type, suppressing duplicates. *)
1147 fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
1148 | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
1149 | add_typ_tfree_names(TVar(_),fs) = fs;
1151 fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
1152 | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
1153 | add_typ_tfrees(TVar(_),fs) = fs;
1155 fun add_typ_varnames(Type(_,Ts),nms) = List.foldr add_typ_varnames nms Ts
1156 | add_typ_varnames(TFree(nm,_),nms) = insert (op =) nm nms
1157 | add_typ_varnames(TVar((nm,_),_),nms) = insert (op =) nm nms;
1159 (*Accumulates the TVars in a term, suppressing duplicates. *)
1160 val add_term_tvars = it_term_types add_typ_tvars;
1162 (*Accumulates the TFrees in a term, suppressing duplicates. *)
1163 val add_term_tfrees = it_term_types add_typ_tfrees;
1164 val add_term_tfree_names = it_term_types add_typ_tfree_names;
1166 (*Non-list versions*)
1167 fun typ_tfrees T = add_typ_tfrees(T,[]);
1168 fun typ_tvars T = add_typ_tvars(T,[]);
1169 fun term_tfrees t = add_term_tfrees(t,[]);
1170 fun term_tvars t = add_term_tvars(t,[]);
1172 (*special code to enforce left-to-right collection of TVar-indexnames*)
1174 fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts)
1175 | add_typ_ixns(ixns,TVar(ixn,_)) = if member (op =) ixns ixn then ixns
1177 | add_typ_ixns(ixns,TFree(_)) = ixns;
1179 fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
1180 | add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T)
1181 | add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T)
1182 | add_term_tvar_ixns(Bound _,ixns) = ixns
1183 | add_term_tvar_ixns(Abs(_,T,t),ixns) =
1184 add_term_tvar_ixns(t,add_typ_ixns(ixns,T))
1185 | add_term_tvar_ixns(f$t,ixns) =
1186 add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
1189 (** Frees and Vars **)
1191 (*Accumulates the Vars in the term, suppressing duplicates*)
1192 fun add_term_vars (t, vars: term list) = case t of
1193 Var _ => OrdList.insert term_ord t vars
1194 | Abs (_,_,body) => add_term_vars(body,vars)
1195 | f$t => add_term_vars (f, add_term_vars(t, vars))
1198 fun term_vars t = add_term_vars(t,[]);
1200 (*Accumulates the Frees in the term, suppressing duplicates*)
1201 fun add_term_frees (t, frees: term list) = case t of
1202 Free _ => OrdList.insert term_ord t frees
1203 | Abs (_,_,body) => add_term_frees(body,frees)
1204 | f$t => add_term_frees (f, add_term_frees(t, frees))
1207 fun term_frees t = add_term_frees(t,[]);
1210 (* dest abstraction *)
1212 fun dest_abs (x, T, body) =
1214 fun name_clash (Free (y, _)) = (x = y)
1215 | name_clash (t $ u) = name_clash t orelse name_clash u
1216 | name_clash (Abs (_, _, t)) = name_clash t
1217 | name_clash _ = false;
1219 if name_clash body then
1220 dest_abs (Name.variant [x] x, T, body) (*potentially slow, but rarely happens*)
1221 else (x, subst_bound (Free (x, T), body))
1225 (* renaming variables *)
1227 fun declare_term_names tm =
1229 (fn Const (a, _) => Name.declare (NameSpace.base a)
1230 | Free (a, _) => Name.declare a
1232 fold_types (fold_atyps (fn TFree (a, _) => Name.declare a | _ => I)) tm;
1234 fun variant_frees t frees =
1235 fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees;
1237 fun rename_wrt_term t frees = rev (variant_frees t frees); (*reversed result!*)
1240 (* dummy patterns *)
1242 val dummy_patternN = "dummy_pattern";
1244 fun dummy_pattern T = Const (dummy_patternN, T);
1246 fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
1247 | is_dummy_pattern _ = false;
1249 fun no_dummy_patterns tm =
1250 if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
1251 else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
1253 fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =
1254 (i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)))
1255 | replace_dummy Ts (i, Abs (x, T, t)) =
1256 let val (i', t') = replace_dummy (T :: Ts) (i, t)
1257 in (i', Abs (x, T, t')) end
1258 | replace_dummy Ts (i, t $ u) =
1259 let val (i', t') = replace_dummy Ts (i, t); val (i'', u') = replace_dummy Ts (i', u)
1260 in (i'', t' $ u') end
1261 | replace_dummy _ (i, a) = (i, a);
1263 val replace_dummy_patterns = replace_dummy [];
1265 fun is_replaced_dummy_pattern ("_dummy_", _) = true
1266 | is_replaced_dummy_pattern _ = false;
1268 fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T)
1269 | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
1270 | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
1271 | show_dummy_patterns a = a;
1274 (* display variables *)
1276 val show_question_marks = ref true;
1278 fun string_of_vname (x, i) =
1280 val question_mark = if ! show_question_marks then "?" else "";
1281 val idx = string_of_int i;
1283 (case rev (Symbol.explode x) of
1284 _ :: "\\<^isub>" :: _ => false
1285 | _ :: "\\<^isup>" :: _ => false
1286 | c :: _ => Symbol.is_digit c
1289 if dot then question_mark ^ x ^ "." ^ idx
1290 else if i <> 0 then question_mark ^ x ^ idx
1291 else question_mark ^ x
1294 fun string_of_vname' (x, ~1) = x
1295 | string_of_vname' xi = string_of_vname xi;
1299 structure BasicTerm: BASIC_TERM = Term;