open AlphaLib
open Term
module T = Toolbox.Make(Term)
open T
let rec red t =
match t with
| TVar x ->
TVar x
| TLambda (x, t) ->
begin match red t with
| TApp (u, TVar y) when Atom.equal x y && not (occurs_term x u) ->
(* Eta-reduction. *)
u
| t ->
TLambda (x, t)
end
| TApp (t1, t2) ->
let t1 = red t1
and t2 = red t2 in
match t1 with
| TLambda (x, u1) ->
(* method 1: copy [u1] so as to avoid name capture *)
(* subst_TVar_term1 (fun t2 -> t2) t2 x (copy_term u1) *)
(* method 2: impose the invariant that our terms do not
have shadowing; this invariant guarantees that [u1]
does not need to be copied; instead, [t2] must be
copied so as to maintain the invariant. *)
subst_TVar_term1 copy_term t2 x u1
| _ ->
TApp (t1, t2)