(* Title: Pure/term.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright Cambridge University 1992
Simply typed lambda-calculus: types, terms, and basic operations.
*)
infix 9 $;
infixr 5 -->;
infixr --->;
infix aconv;
signature BASIC_TERM =
sig
eqtype indexname
eqtype class
eqtype sort
eqtype arity
datatype typ =
Type of string * typ list |
TFree of string * sort |
TVar of indexname * sort
datatype term =
Const of string * typ |
Free of string * typ |
Var of indexname * typ |
Bound of int |
Abs of string * typ * term |
$ of term * term
exception TYPE of string * typ list * term list
exception TERM of string * term list
val dummyS: sort
val dummyT: typ
val no_dummyT: typ -> typ
val --> : typ * typ -> typ
val ---> : typ list * typ -> typ
val dest_Type: typ -> string * typ list
val dest_TVar: typ -> indexname * sort
val dest_TFree: typ -> string * sort
val is_Bound: term -> bool
val is_Const: term -> bool
val is_Free: term -> bool
val is_Var: term -> bool
val is_TVar: typ -> bool
val dest_Const: term -> string * typ
val dest_Free: term -> string * typ
val dest_Var: term -> indexname * typ
val domain_type: typ -> typ
val range_type: typ -> typ
val binder_types: typ -> typ list
val body_type: typ -> typ
val strip_type: typ -> typ list * typ
val type_of1: typ list * term -> typ
val type_of: term -> typ
val fastype_of1: typ list * term -> typ
val fastype_of: term -> typ
val list_abs: (string * typ) list * term -> term
val strip_abs: term -> (string * typ) list * term
val strip_abs_body: term -> term
val strip_abs_vars: term -> (string * typ) list
val strip_qnt_body: string -> term -> term
val strip_qnt_vars: string -> term -> (string * typ) list
val list_comb: term * term list -> term
val strip_comb: term -> term * term list
val head_of: term -> term
val size_of_term: term -> int
val map_atyps: (typ -> typ) -> typ -> typ
val map_aterms: (term -> term) -> term -> term
val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
val map_type_tfree: (string * sort -> typ) -> typ -> typ
val map_types: (typ -> typ) -> term -> term
val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
val add_term_names: term * string list -> string list
val aconv: term * term -> bool
structure Vartab: TABLE
structure Typtab: TABLE
structure Termtab: TABLE
val propT: typ
val implies: term
val all: typ -> term
val equals: typ -> term
val strip_all_body: term -> term
val strip_all_vars: term -> (string * typ) list
val incr_bv: int * int * term -> term
val incr_boundvars: int -> term -> term
val add_loose_bnos: term * int * int list -> int list
val loose_bnos: term -> int list
val loose_bvar: term * int -> bool
val loose_bvar1: term * int -> bool
val subst_bounds: term list * term -> term
val subst_bound: term * term -> term
val betapply: term * term -> term
val betapplys: term * term list -> term
val eq_ix: indexname * indexname -> bool
val could_unify: term * term -> bool
val subst_free: (term * term) list -> term -> term
val abstract_over: term * term -> term
val lambda: term -> term -> term
val absfree: string * typ * term -> term
val absdummy: typ * term -> term
val list_abs_free: (string * typ) list * term -> term
val list_all_free: (string * typ) list * term -> term
val list_all: (string * typ) list * term -> term
val subst_atomic: (term * term) list -> term -> term
val typ_subst_atomic: (typ * typ) list -> typ -> typ
val subst_atomic_types: (typ * typ) list -> term -> term
val typ_subst_TVars: (indexname * typ) list -> typ -> typ
val subst_TVars: (indexname * typ) list -> term -> term
val subst_Vars: (indexname * term) list -> term -> term
val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
val is_first_order: string list -> term -> bool
val maxidx_of_typ: typ -> int
val maxidx_of_typs: typ list -> int
val maxidx_of_term: term -> int
val add_term_consts: term * string list -> string list
val term_consts: term -> string list
val exists_subtype: (typ -> bool) -> typ -> bool
val exists_type: (typ -> bool) -> term -> bool
val exists_subterm: (term -> bool) -> term -> bool
val exists_Const: (string * typ -> bool) -> term -> bool
val add_term_free_names: term * string list -> string list
val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list
val add_typ_tfree_names: typ * string list -> string list
val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list
val add_typ_varnames: typ * string list -> string list
val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list
val add_term_tfrees: term * (string * sort) list -> (string * sort) list
val add_term_tfree_names: term * string list -> string list
val typ_tfrees: typ -> (string * sort) list
val typ_tvars: typ -> (indexname * sort) list
val term_tfrees: term -> (string * sort) list
val term_tvars: term -> (indexname * sort) list
val add_typ_ixns: indexname list * typ -> indexname list
val add_term_tvar_ixns: term * indexname list -> indexname list
val add_term_vars: term * term list -> term list
val term_vars: term -> term list
val add_term_frees: term * term list -> term list
val term_frees: term -> term list
val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
val show_question_marks: bool ref
end;
signature TERM =
sig
include BASIC_TERM
val aT: sort -> typ
val itselfT: typ -> typ
val a_itselfT: typ
val argument_type_of: term -> typ
val head_name_of: term -> string
val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
val add_varnames: term -> indexname list -> indexname list
val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
val add_tfrees: term -> (string * sort) list -> (string * sort) list
val add_frees: term -> (string * typ) list -> (string * typ) list
val hidden_polymorphism: term -> typ -> (indexname * sort) list
val equiv_types: term * term -> bool
val strip_abs_eta: int -> term -> (string * typ) list * term
val fast_indexname_ord: indexname * indexname -> order
val indexname_ord: indexname * indexname -> order
val sort_ord: sort * sort -> order
val typ_ord: typ * typ -> order
val fast_term_ord: term * term -> order
val term_ord: term * term -> order
val hd_ord: term * term -> order
val termless: term * term -> bool
val term_lpo: (term -> int) -> term * term -> order
val match_bvars: (term * term) * (string * string) list -> (string * string) list
val map_abs_vars: (string -> string) -> term -> term
val rename_abs: term -> term -> term -> term option
val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
val eq_var: (indexname * typ) * (indexname * typ) -> bool
val tvar_ord: (indexname * sort) * (indexname * sort) -> order
val var_ord: (indexname * typ) * (indexname * typ) -> order
val maxidx_typ: typ -> int -> int
val maxidx_typs: typ list -> int -> int
val maxidx_term: term -> int -> int
val dest_abs: string * typ * term -> string * term
val declare_term_names: term -> Name.context -> Name.context
val variant_frees: term -> (string * 'a) list -> (string * 'a) list
val dummy_patternN: string
val dummy_pattern: typ -> term
val no_dummy_patterns: term -> term
val replace_dummy_patterns: int * term -> int * term
val is_replaced_dummy_pattern: indexname -> bool
val show_dummy_patterns: term -> term
val string_of_vname: indexname -> string
val string_of_vname': indexname -> string
end;
structure Term: TERM =
struct
(*Indexnames can be quickly renamed by adding an offset to the integer part,
for resolution.*)
type indexname = string * int;
(* Types are classified by sorts. *)
type class = string;
type sort = class list;
type arity = string * sort list * sort;
(* The sorts attached to TFrees and TVars specify the sort of that variable *)
datatype typ = Type of string * typ list
| TFree of string * sort
| TVar of indexname * sort;
(*Terms. Bound variables are indicated by depth number.
Free variables, (scheme) variables and constants have names.
An term is "closed" if every bound variable of level "lev"
is enclosed by at least "lev" abstractions.
It is possible to create meaningless terms containing loose bound vars
or type mismatches. But such terms are not allowed in rules. *)
datatype term =
Const of string * typ
| Free of string * typ
| Var of indexname * typ
| Bound of int
| Abs of string*typ*term
| op $ of term*term;
(*Errors involving type mismatches*)
exception TYPE of string * typ list * term list;
(*Errors errors involving terms*)
exception TERM of string * term list;
(*Note variable naming conventions!
a,b,c: string
f,g,h: functions (including terms of function type)
i,j,m,n: int
t,u: term
v,w: indexnames
x,y: any
A,B,C: term (denoting formulae)
T,U: typ
*)
(** Types **)
(*dummies for type-inference etc.*)
val dummyS = [""];
val dummyT = Type ("dummy", []);
fun no_dummyT typ =
let
fun check (T as Type ("dummy", _)) =
raise TYPE ("Illegal occurrence of '_' dummy type", [T], [])
| check (Type (_, Ts)) = List.app check Ts
| check _ = ();
in check typ; typ end;
fun S --> T = Type("fun",[S,T]);
(*handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)*)
val op ---> = Library.foldr (op -->);
fun dest_Type (Type x) = x
| dest_Type T = raise TYPE ("dest_Type", [T], []);
fun dest_TVar (TVar x) = x
| dest_TVar T = raise TYPE ("dest_TVar", [T], []);
fun dest_TFree (TFree x) = x
| dest_TFree T = raise TYPE ("dest_TFree", [T], []);
(** Discriminators **)
fun is_Bound (Bound _) = true
| is_Bound _ = false;
fun is_Const (Const _) = true
| is_Const _ = false;
fun is_Free (Free _) = true
| is_Free _ = false;
fun is_Var (Var _) = true
| is_Var _ = false;
fun is_TVar (TVar _) = true
| is_TVar _ = false;
(** Destructors **)
fun dest_Const (Const x) = x
| dest_Const t = raise TERM("dest_Const", [t]);
fun dest_Free (Free x) = x
| dest_Free t = raise TERM("dest_Free", [t]);
fun dest_Var (Var x) = x
| dest_Var t = raise TERM("dest_Var", [t]);
fun domain_type (Type("fun", [T,_])) = T
and range_type (Type("fun", [_,T])) = T;
(* maps [T1,...,Tn]--->T to the list [T1,T2,...,Tn]*)
fun binder_types (Type("fun",[S,T])) = S :: binder_types T
| binder_types _ = [];
(* maps [T1,...,Tn]--->T to T*)
fun body_type (Type("fun",[S,T])) = body_type T
| body_type T = T;
(* maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T) *)
fun strip_type T : typ list * typ =
(binder_types T, body_type T);
(*Compute the type of the term, checking that combinations are well-typed
Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
fun type_of1 (Ts, Const (_,T)) = T
| type_of1 (Ts, Free (_,T)) = T
| type_of1 (Ts, Bound i) = (List.nth (Ts,i)
handle Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
| type_of1 (Ts, Var (_,T)) = T
| type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
| type_of1 (Ts, f$u) =
let val U = type_of1(Ts,u)
and T = type_of1(Ts,f)
in case T of
Type("fun",[T1,T2]) =>
if T1=U then T2 else raise TYPE
("type_of: type mismatch in application", [T1,U], [f$u])
| _ => raise TYPE
("type_of: function type is expected in application",
[T,U], [f$u])
end;
fun type_of t : typ = type_of1 ([],t);
(*Determines the type of a term, with minimal checking*)
fun fastype_of1 (Ts, f$u) =
(case fastype_of1 (Ts,f) of
Type("fun",[_,T]) => T
| _ => raise TERM("fastype_of: expected function type", [f$u]))
| fastype_of1 (_, Const (_,T)) = T
| fastype_of1 (_, Free (_,T)) = T
| fastype_of1 (Ts, Bound i) = (List.nth(Ts,i)
handle Subscript => raise TERM("fastype_of: Bound", [Bound i]))
| fastype_of1 (_, Var (_,T)) = T
| fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
fun fastype_of t : typ = fastype_of1 ([],t);
(*Determine the argument type of a function*)
fun argument_type_of tm =
let
fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i - 1) U
| argT _ T = raise TYPE ("argument_type_of", [T], []);
fun arg 0 _ (Abs (_, T, _)) = T
| arg i Ts (Abs (_, T, t)) = arg (i - 1) (T :: Ts) t
| arg i Ts (t $ _) = arg (i + 1) Ts t
| arg i Ts a = argT i (fastype_of1 (Ts, a));
in arg 0 [] tm end;
val list_abs = uncurry (fold_rev (fn (x, T) => fn t => Abs (x, T, t)));
fun strip_abs (Abs (a, T, t)) =
let val (a', t') = strip_abs t
in ((a, T) :: a', t') end
| strip_abs t = ([], t);
(* maps (x1,...,xn)t to t *)
fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t
| strip_abs_body u = u;
(* maps (x1,...,xn)t to [x1, ..., xn] *)
fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t
| strip_abs_vars u = [] : (string*typ) list;
fun strip_qnt_body qnt =
let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
| strip t = t
in strip end;
fun strip_qnt_vars qnt =
let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
| strip t = [] : (string*typ) list
in strip end;
(* maps (f, [t1,...,tn]) to f(t1,...,tn) *)
val list_comb : term * term list -> term = Library.foldl (op $);
(* maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tail-recursive*)
fun strip_comb u : term * term list =
let fun stripc (f$t, ts) = stripc (f, t::ts)
| stripc x = x
in stripc(u,[]) end;
(* maps f(t1,...,tn) to f , which is never a combination *)
fun head_of (f$t) = head_of f
| head_of u = u;
fun head_name_of tm =
(case head_of tm of
t as Const (c, _) =>
if NameSpace.is_qualified c then c
else raise TERM ("Malformed constant name", [t])
| t as Free (x, _) =>
if not (NameSpace.is_qualified x) then x
else raise TERM ("Malformed fixed variable name", [t])
| t => raise TERM ("No fixed head of term", [t]));
(*number of atoms and abstractions in a term*)
fun size_of_term tm =
let
fun add_size (t $ u, n) = add_size (t, add_size (u, n))
| add_size (Abs (_ ,_, t), n) = add_size (t, n + 1)
| add_size (_, n) = n + 1;
in add_size (tm, 0) end;
fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
| map_atyps f T = f T;
fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u
| map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
| map_aterms f t = f t;
fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
fun map_types f =
let
fun map_aux (Const (a, T)) = Const (a, f T)
| map_aux (Free (a, T)) = Free (a, f T)
| map_aux (Var (v, T)) = Var (v, f T)
| map_aux (t as Bound _) = t
| map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t)
| map_aux (t $ u) = map_aux t $ map_aux u;
in map_aux end;
(* iterate a function over all types in a term *)
fun it_term_types f =
let fun iter(Const(_,T), a) = f(T,a)
| iter(Free(_,T), a) = f(T,a)
| iter(Var(_,T), a) = f(T,a)
| iter(Abs(_,T,t), a) = iter(t,f(T,a))
| iter(f$u, a) = iter(f, iter(u, a))
| iter(Bound _, a) = a
in iter end
(* fold types and terms *)
(*fold atoms of type*)
fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
| fold_atyps f T = f T;
(*fold atoms of term*)
fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
| fold_aterms f (Abs (_, _, t)) = fold_aterms f t
| fold_aterms f a = f a;
(*fold types of term*)
fun fold_term_types f (t as Const (_, T)) = f t T
| fold_term_types f (t as Free (_, T)) = f t T
| fold_term_types f (t as Var (_, T)) = f t T
| fold_term_types f (Bound _) = I
| fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b
| fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u;
fun fold_types f = fold_term_types (K f);
(*collect variables*)
val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
val add_tvars = fold_types add_tvarsT;
val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
val add_varnames = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
val add_tfrees = fold_types add_tfreesT;
val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
(*extra type variables in a term, not covered by the type*)
fun hidden_polymorphism t T =
let
val tvarsT = add_tvarsT T [];
val extra_tvars = fold_types (fold_atyps
(fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
in extra_tvars end;
(** Comparing terms, types, sorts etc. **)
(* alpha equivalence -- tuned for equalities *)
fun tm1 aconv tm2 =
pointer_eq (tm1, tm2) orelse
(case (tm1, tm2) of
(t1 $ u1, t2 $ u2) => t1 aconv t2 andalso u1 aconv u2
| (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2
| (a1, a2) => a1 = a2);
(* equivalence up to renaming of types variables *)
local
val invent_names = Name.invents Name.context "'a";
fun standard_types t =
let
val tfrees = add_tfrees t [];
val tvars = add_tvars t [];
val env1 = map2 (fn (a, S) => fn a' => (TFree (a, S), TFree (a', [])))
tfrees (invent_names (length tfrees));
val env2 = map2 (fn ((a, i), S) => fn a' => (TVar ((a, i), S), TVar ((a', 0), [])))
tvars (invent_names (length tvars));
in map_types (map_atyps (perhaps (AList.lookup (op =) (env1 @ env2)))) t end;
in
val equiv_types = op aconv o pairself standard_types;
end;
(* fast syntactic ordering -- tuned for inequalities *)
fun fast_indexname_ord ((x, i), (y, j)) =
(case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord);
fun sort_ord SS =
if pointer_eq SS then EQUAL
else dict_ord fast_string_ord SS;
local
fun cons_nr (TVar _) = 0
| cons_nr (TFree _) = 1
| cons_nr (Type _) = 2;
in
fun typ_ord TU =
if pointer_eq TU then EQUAL
else
(case TU of
(Type (a, Ts), Type (b, Us)) =>
(case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord)
| (TFree (a, S), TFree (b, S')) =>
(case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord)
| (TVar (xi, S), TVar (yj, S')) =>
(case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord)
| (T, U) => int_ord (cons_nr T, cons_nr U));
end;
local
fun cons_nr (Const _) = 0
| cons_nr (Free _) = 1
| cons_nr (Var _) = 2
| cons_nr (Bound _) = 3
| cons_nr (Abs _) = 4
| cons_nr (_ $ _) = 5;
fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u)
| struct_ord (t1 $ t2, u1 $ u2) =
(case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord)
| struct_ord (t, u) = int_ord (cons_nr t, cons_nr u);
fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u)
| atoms_ord (t1 $ t2, u1 $ u2) =
(case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord)
| atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b)
| atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
| atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
| atoms_ord (Bound i, Bound j) = int_ord (i, j)
| atoms_ord _ = sys_error "atoms_ord";
fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
(case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
| types_ord (t1 $ t2, u1 $ u2) =
(case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord)
| types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
| types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
| types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
| types_ord (Bound _, Bound _) = EQUAL
| types_ord _ = sys_error "types_ord";
in
fun fast_term_ord tu =
if pointer_eq tu then EQUAL
else
(case struct_ord tu of
EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
| ord => ord);
structure Vartab = TableFun(type key = indexname val ord = fast_indexname_ord);
structure Typtab = TableFun(type key = typ val ord = typ_ord);
structure Termtab = TableFun(type key = term val ord = fast_term_ord);
end;
(* term_ord *)
(*a linear well-founded AC-compatible ordering for terms:
s < t <=> 1. size(s) < size(t) or
2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
(s1..sn) < (t1..tn) (lexicographically)*)
fun indexname_ord ((x, i), (y, j)) =
(case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
local
fun hd_depth (t $ _, n) = hd_depth (t, n + 1)
| hd_depth p = p;
fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
| dest_hd (Free (a, T)) = (((a, 0), T), 1)
| dest_hd (Var v) = (v, 2)
| dest_hd (Bound i) = ((("", i), dummyT), 3)
| dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
in
fun term_ord tu =
if pointer_eq tu then EQUAL
else
(case tu of
(Abs (_, T, t), Abs(_, U, u)) =>
(case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
| (t, u) =>
(case int_ord (size_of_term t, size_of_term u) of
EQUAL =>
(case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of
EQUAL => args_ord (t, u) | ord => ord)
| ord => ord))
and hd_ord (f, g) =
prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
and args_ord (f $ t, g $ u) =
(case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord)
| args_ord _ = EQUAL;
fun termless tu = (term_ord tu = LESS);
end;
(** Lexicographic path order on terms **)
(*
See Baader & Nipkow, Term rewriting, CUP 1998.
Without variables. Const, Var, Bound, Free and Abs are treated all as
constants.
f_ord maps terms to integers and serves two purposes:
- Predicate on constant symbols. Those that are not recognised by f_ord
must be mapped to ~1.
- Order on the recognised symbols. These must be mapped to distinct
integers >= 0.
The argument of f_ord is never an application.
*)
local
fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0)
| unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0)
| unrecognized (Var v) = ((1, v), 1)
| unrecognized (Bound i) = ((1, (("", i), dummyT)), 2)
| unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
fun dest_hd f_ord t =
let val ord = f_ord t in
if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0)
end
fun term_lpo f_ord (s, t) =
let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
then case hd_ord f_ord (f, g) of
GREATER =>
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
then GREATER else LESS
| EQUAL =>
if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
then list_ord (term_lpo f_ord) (ss, ts)
else LESS
| LESS => LESS
else GREATER
end
and hd_ord f_ord (f, g) = case (f, g) of
(Abs (_, T, t), Abs (_, U, u)) =>
(case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
| (_, _) => prod_ord (prod_ord int_ord
(prod_ord indexname_ord typ_ord)) int_ord
(dest_hd f_ord f, dest_hd f_ord g)
in
val term_lpo = term_lpo
end;
(** Connectives of higher order logic **)
fun aT S = TFree ("'a", S);
fun itselfT ty = Type ("itself", [ty]);
val a_itselfT = itselfT (TFree ("'a", []));
val propT : typ = Type("prop",[]);
val implies = Const("==>", propT-->propT-->propT);
fun all T = Const("all", (T-->propT)-->propT);
fun equals T = Const("==", T-->T-->propT);
(* maps !!x1...xn. t to t *)
fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t
| strip_all_body t = t;
(* maps !!x1...xn. t to [x1, ..., xn] *)
fun strip_all_vars (Const("all",_)$Abs(a,T,t)) =
(a,T) :: strip_all_vars t
| strip_all_vars t = [] : (string*typ) list;
(*increments a term's non-local bound variables
required when moving a term within abstractions
inc is increment for bound variables
lev is level at which a bound variable is considered 'loose'*)
fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
| incr_bv (inc, lev, Abs(a,T,body)) =
Abs(a, T, incr_bv(inc,lev+1,body))
| incr_bv (inc, lev, f$t) =
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
| incr_bv (inc, lev, u) = u;
fun incr_boundvars 0 t = t
| incr_boundvars inc t = incr_bv(inc,0,t);
(*Scan a pair of terms; while they are similar,
accumulate corresponding bound vars in "al"*)
fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
match_bvs(s, t, if x="" orelse y="" then al
else (x,y)::al)
| match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
| match_bvs(_,_,al) = al;
(* strip abstractions created by parameters *)
fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al);
fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u
| map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t)
| map_abs_vars f t = t;
fun rename_abs pat obj t =
let
val ren = match_bvs (pat, obj, []);
fun ren_abs (Abs (x, T, b)) =
Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b)
| ren_abs (f $ t) = ren_abs f $ ren_abs t
| ren_abs t = t
in if null ren then NONE else SOME (ren_abs t) end;
(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
(Bound 0) is loose at level 0 *)
fun add_loose_bnos (Bound i, lev, js) =
if i<lev then js else insert (op =) (i - lev) js
| add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
| add_loose_bnos (f$t, lev, js) =
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
| add_loose_bnos (_, _, js) = js;
fun loose_bnos t = add_loose_bnos (t, 0, []);
(* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
level k or beyond. *)
fun loose_bvar(Bound i,k) = i >= k
| loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
| loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
| loose_bvar _ = false;
fun loose_bvar1(Bound i,k) = i = k
| loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
| loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
| loose_bvar1 _ = false;
(*Substitute arguments for loose bound variables.
Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
Note that for ((%x y. c) a b), the bound vars in c are x=1 and y=0
and the appropriate call is subst_bounds([b,a], c) .
Loose bound variables >=n are reduced by "n" to
compensate for the disappearance of lambdas.
*)
fun subst_bounds (args: term list, t) : term =
let
exception SAME;
val n = length args;
fun subst (t as Bound i, lev) =
(if i < lev then raise SAME (*var is locally bound*)
else incr_boundvars lev (List.nth (args, i - lev))
handle Subscript => Bound (i - n)) (*loose: change it*)
| subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
| subst (f $ t, lev) =
(subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
| subst _ = raise SAME;
in case args of [] => t | _ => (subst (t, 0) handle SAME => t) end;
(*Special case: one argument*)
fun subst_bound (arg, t) : term =
let
exception SAME;
fun subst (Bound i, lev) =
if i < lev then raise SAME (*var is locally bound*)
else if i = lev then incr_boundvars lev arg
else Bound (i - 1) (*loose: change it*)
| subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
| subst (f $ t, lev) =
(subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
| subst _ = raise SAME;
in subst (t, 0) handle SAME => t end;
(*beta-reduce if possible, else form application*)
fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
| betapply (f,u) = f$u;
val betapplys = Library.foldl betapply;
(*unfolding abstractions with substitution
of bound variables and implicit eta-expansion*)
fun strip_abs_eta k t =
let
val used = fold_aterms (fn Free (v, _) => Name.declare v | _ => I) t Name.context;
fun strip_abs t (0, used) = (([], t), (0, used))
| strip_abs (Abs (v, T, t)) (k, used) =
let
val ([v'], used') = Name.variants [v] used;
val t' = subst_bound (Free (v', T), t);
val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
in (((v', T) :: vs, t''), (k', used'')) end
| strip_abs t (k, used) = (([], t), (k, used));
fun expand_eta [] t _ = ([], t)
| expand_eta (T::Ts) t used =
let
val ([v], used') = Name.variants [""] used;
val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
in ((v, T) :: vs, t') end;
val ((vs1, t'), (k', used')) = strip_abs t (k, used);
val Ts = (fst o chop k' o fst o strip_type o fastype_of) t';
val (vs2, t'') = expand_eta Ts t' used';
in (vs1 @ vs2, t'') end;
(* comparing variables *)
fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
val tvar_ord = prod_ord indexname_ord sort_ord;
val var_ord = prod_ord indexname_ord typ_ord;
(*A fast unification filter: true unless the two terms cannot be unified.
Terms must be NORMAL. Treats all Vars as distinct. *)
fun could_unify (t,u) =
let fun matchrands (f$t, g$u) = could_unify(t,u) andalso matchrands(f,g)
| matchrands _ = true
in case (head_of t , head_of u) of
(_, Var _) => true
| (Var _, _) => true
| (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u)
| (Free(a,_), Free(b,_)) => a=b andalso matchrands(t,u)
| (Bound i, Bound j) => i=j andalso matchrands(t,u)
| (Abs _, _) => true (*because of possible eta equality*)
| (_, Abs _) => true
| _ => false
end;
(*Substitute new for free occurrences of old in a term*)
fun subst_free [] = (fn t=>t)
| subst_free pairs =
let fun substf u =
case AList.lookup (op aconv) pairs u of
SOME u' => u'
| NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
| t$u' => substf t $ substf u'
| _ => u)
in substf end;
(*Abstraction of the term "body" over its occurrences of v,
which must contain no loose bound variables.
The resulting term is ready to become the body of an Abs.*)
fun abstract_over (v, body) =
let
exception SAME;
fun abs lev tm =
if v aconv tm then Bound lev
else
(case tm of
Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
| t $ u => (abs lev t $ (abs lev u handle SAME => u) handle SAME => t $ abs lev u)
| _ => raise SAME);
in abs 0 body handle SAME => body end;
fun lambda v t =
let val x =
(case v of
Const (x, _) => NameSpace.base x
| Free (x, _) => x
| Var ((x, _), _) => x
| _ => "uu")
in Abs (x, fastype_of v, abstract_over (v, t)) end;
(*Form an abstraction over a free variable.*)
fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
fun absdummy (T, body) = Abs (Name.internal "x", T, body);
(*Abstraction over a list of free variables*)
fun list_abs_free ([ ] , t) = t
| list_abs_free ((a,T)::vars, t) =
absfree(a, T, list_abs_free(vars,t));
(*Quantification over a list of free variables*)
fun list_all_free ([], t: term) = t
| list_all_free ((a,T)::vars, t) =
(all T) $ (absfree(a, T, list_all_free(vars,t)));
(*Quantification over a list of variables (already bound in body) *)
fun list_all ([], t) = t
| list_all ((a,T)::vars, t) =
(all T) $ (Abs(a, T, list_all(vars,t)));
(*Replace the ATOMIC term ti by ui; inst = [(t1,u1), ..., (tn,un)].
A simultaneous substitution: [ (a,b), (b,a) ] swaps a and b. *)
fun subst_atomic [] tm = tm
| subst_atomic inst tm =
let
fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
| subst (t $ u) = subst t $ subst u
| subst t = the_default t (AList.lookup (op aconv) inst t);
in subst tm end;
(*Replace the ATOMIC type Ti by Ui; inst = [(T1,U1), ..., (Tn,Un)].*)
fun typ_subst_atomic [] ty = ty
| typ_subst_atomic inst ty =
let
fun subst (Type (a, Ts)) = Type (a, map subst Ts)
| subst T = the_default T (AList.lookup (op = : typ * typ -> bool) inst T);
in subst ty end;
fun subst_atomic_types [] tm = tm
| subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm;
fun typ_subst_TVars [] ty = ty
| typ_subst_TVars inst ty =
let
fun subst (Type (a, Ts)) = Type (a, map subst Ts)
| subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi)
| subst T = T;
in subst ty end;
fun subst_TVars [] tm = tm
| subst_TVars inst tm = map_types (typ_subst_TVars inst) tm;
fun subst_Vars [] tm = tm
| subst_Vars inst tm =
let
fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi)
| subst (Abs (a, T, t)) = Abs (a, T, subst t)
| subst (t $ u) = subst t $ subst u
| subst t = t;
in subst tm end;
fun subst_vars ([], []) tm = tm
| subst_vars ([], inst) tm = subst_Vars inst tm
| subst_vars (instT, inst) tm =
let
fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
| subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
| subst (t as Var (xi, T)) =
(case AList.lookup (op =) inst xi of
NONE => Var (xi, typ_subst_TVars instT T)
| SOME t => t)
| subst (t as Bound _) = t
| subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t)
| subst (t $ u) = subst t $ subst u;
in subst tm end;
(** Identifying first-order terms **)
(*Differs from proofterm/is_fun in its treatment of TVar*)
fun is_funtype (Type("fun",[_,_])) = true
| is_funtype _ = false;
(*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts,t)));
(*First order means in all terms of the form f(t1,...,tn) no argument has a
function type. The supplied quantifiers are excluded: their argument always
has a function type through a recursive call into its body.*)
fun is_first_order quants =
let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
| first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
member (op =) quants q andalso (*it is a known quantifier*)
not (is_funtype T) andalso first_order1 (T::Ts) body
| first_order1 Ts t =
case strip_comb t of
(Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
| (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
| (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
| (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
| (Abs _, ts) => false (*not in beta-normal form*)
| _ => error "first_order: unexpected case"
in first_order1 [] end;
(* maximum index of typs and terms *)
fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j)
| maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i
| maxidx_typ (TFree _) i = i
and maxidx_typs [] i = i
| maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i);
fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j))
| maxidx_term (Const (_, T)) i = maxidx_typ T i
| maxidx_term (Free (_, T)) i = maxidx_typ T i
| maxidx_term (Bound _) i = i
| maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i)
| maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i);
fun maxidx_of_typ T = maxidx_typ T ~1;
fun maxidx_of_typs Ts = maxidx_typs Ts ~1;
fun maxidx_of_term t = maxidx_term t ~1;
(**** Syntax-related declarations ****)
(* substructure *)
fun exists_subtype P =
let
fun ex ty = P ty orelse
(case ty of Type (_, Ts) => exists ex Ts | _ => false);
in ex end;
fun exists_type P =
let
fun ex (Const (_, T)) = P T
| ex (Free (_, T)) = P T
| ex (Var (_, T)) = P T
| ex (Bound _) = false
| ex (Abs (_, T, t)) = P T orelse ex t
| ex (t $ u) = ex t orelse ex u;
in ex end;
fun exists_subterm P =
let
fun ex tm = P tm orelse
(case tm of
t $ u => ex t orelse ex u
| Abs (_, _, t) => ex t
| _ => false);
in ex end;
(** Consts etc. **)
fun add_term_consts (Const (c, _), cs) = insert (op =) c cs
| add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
| add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
| add_term_consts (_, cs) = cs;
fun term_consts t = add_term_consts(t,[]);
fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
(** TFrees and TVars **)
(*Accumulates the names of Frees in the term, suppressing duplicates.*)
fun add_term_free_names (Free(a,_), bs) = insert (op =) a bs
| add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
| add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
| add_term_free_names (_, bs) = bs;
(*Accumulates the names in the term, suppressing duplicates.
Includes Frees and Consts. For choosing unambiguous bound var names.*)
fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base a) bs
| add_term_names (Free(a,_), bs) = insert (op =) a bs
| add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
| add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
| add_term_names (_, bs) = bs;
(*Accumulates the TVars in a type, suppressing duplicates. *)
fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
| add_typ_tvars(TFree(_),vs) = vs
| add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
(*Accumulates the TFrees in a type, suppressing duplicates. *)
fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
| add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
| add_typ_tfree_names(TVar(_),fs) = fs;
fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
| add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
| add_typ_tfrees(TVar(_),fs) = fs;
fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
| add_typ_varnames(TFree(nm,_),nms) = insert (op =) nm nms
| add_typ_varnames(TVar((nm,_),_),nms) = insert (op =) nm nms;
(*Accumulates the TVars in a term, suppressing duplicates. *)
val add_term_tvars = it_term_types add_typ_tvars;
(*Accumulates the TFrees in a term, suppressing duplicates. *)
val add_term_tfrees = it_term_types add_typ_tfrees;
val add_term_tfree_names = it_term_types add_typ_tfree_names;
(*Non-list versions*)
fun typ_tfrees T = add_typ_tfrees(T,[]);
fun typ_tvars T = add_typ_tvars(T,[]);
fun term_tfrees t = add_term_tfrees(t,[]);
fun term_tvars t = add_term_tvars(t,[]);
(*special code to enforce left-to-right collection of TVar-indexnames*)
fun add_typ_ixns(ixns,Type(_,Ts)) = Library.foldl add_typ_ixns (ixns,Ts)
| add_typ_ixns(ixns,TVar(ixn,_)) = if member (op =) ixns ixn then ixns
else ixns@[ixn]
| add_typ_ixns(ixns,TFree(_)) = ixns;
fun add_term_tvar_ixns(Const(_,T),ixns) = add_typ_ixns(ixns,T)
| add_term_tvar_ixns(Free(_,T),ixns) = add_typ_ixns(ixns,T)
| add_term_tvar_ixns(Var(_,T),ixns) = add_typ_ixns(ixns,T)
| add_term_tvar_ixns(Bound _,ixns) = ixns
| add_term_tvar_ixns(Abs(_,T,t),ixns) =
add_term_tvar_ixns(t,add_typ_ixns(ixns,T))
| add_term_tvar_ixns(f$t,ixns) =
add_term_tvar_ixns(t,add_term_tvar_ixns(f,ixns));
(** Frees and Vars **)
(*Accumulates the Vars in the term, suppressing duplicates*)
fun add_term_vars (t, vars: term list) = case t of
Var _ => OrdList.insert term_ord t vars
| Abs (_,_,body) => add_term_vars(body,vars)
| f$t => add_term_vars (f, add_term_vars(t, vars))
| _ => vars;
fun term_vars t = add_term_vars(t,[]);
(*Accumulates the Frees in the term, suppressing duplicates*)
fun add_term_frees (t, frees: term list) = case t of
Free _ => OrdList.insert term_ord t frees
| Abs (_,_,body) => add_term_frees(body,frees)
| f$t => add_term_frees (f, add_term_frees(t, frees))
| _ => frees;
fun term_frees t = add_term_frees(t,[]);
(* dest abstraction *)
fun dest_abs (x, T, body) =
let
fun name_clash (Free (y, _)) = (x = y)
| name_clash (t $ u) = name_clash t orelse name_clash u
| name_clash (Abs (_, _, t)) = name_clash t
| name_clash _ = false;
in
if name_clash body then
dest_abs (Name.variant [x] x, T, body) (*potentially slow, but rarely happens*)
else (x, subst_bound (Free (x, T), body))
end;
(* renaming variables *)
fun declare_term_names tm =
fold_aterms
(fn Const (a, _) => Name.declare (NameSpace.base a)
| Free (a, _) => Name.declare a
| _ => I) tm #>
fold_types (fold_atyps (fn TFree (a, _) => Name.declare a | _ => I)) tm;
fun variant_frees t frees =
fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees;
fun rename_wrt_term t frees = rev (variant_frees t frees); (*reversed result!*)
(* dummy patterns *)
val dummy_patternN = "dummy_pattern";
fun dummy_pattern T = Const (dummy_patternN, T);
fun is_dummy_pattern (Const ("dummy_pattern", _)) = true
| is_dummy_pattern _ = false;
fun no_dummy_patterns tm =
if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =
(i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)))
| replace_dummy Ts (i, Abs (x, T, t)) =
let val (i', t') = replace_dummy (T :: Ts) (i, t)
in (i', Abs (x, T, t')) end
| replace_dummy Ts (i, t $ u) =
let val (i', t') = replace_dummy Ts (i, t); val (i'', u') = replace_dummy Ts (i', u)
in (i'', t' $ u') end
| replace_dummy _ (i, a) = (i, a);
val replace_dummy_patterns = replace_dummy [];
fun is_replaced_dummy_pattern ("_dummy_", _) = true
| is_replaced_dummy_pattern _ = false;
fun show_dummy_patterns (Var (("_dummy_", _), T)) = Const ("dummy_pattern", T)
| show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
| show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
| show_dummy_patterns a = a;
(* display variables *)
val show_question_marks = ref true;
fun string_of_vname (x, i) =
let
val question_mark = if ! show_question_marks then "?" else "";
val idx = string_of_int i;
val dot =
(case rev (Symbol.explode x) of
_ :: "\\<^isub>" :: _ => false
| _ :: "\\<^isup>" :: _ => false
| c :: _ => Symbol.is_digit c
| _ => true);
in
if dot then question_mark ^ x ^ "." ^ idx
else if i <> 0 then question_mark ^ x ^ idx
else question_mark ^ x
end;
fun string_of_vname' (x, ~1) = x
| string_of_vname' xi = string_of_vname xi;
end;
structure BasicTerm: BASIC_TERM = Term;
open BasicTerm;