module S05 (
Term(..),
vars, freeVars, boundVars,
applySubst
) where
data Term = Var String | Lab String Term | App Term Term
vars :: Term -> [String]
vars (Var x) = [x]
vars (Lab x t) = x : vars t
vars (App s t) = vars s ++ vars t
freeVars :: Term -> [String]
freeVars (Var x) = [x]
freeVars (Lab x t) = [y | y <- freeVars t, y /= x]
freeVars (App s t) = freeVars s ++ freeVars t
boundVars :: Term -> [String]
boundVars (Var _) = []
boundVars (Lab x t) = x : boundVars t
boundVars (App s t) = boundVars s ++ boundVars t
applySubst :: String -> Term -> Term -> Term
applySubst x s (Var y)
| x == y = s
| otherwise = Var y
applySubst x s (App u v) = App (applySubst x s u) (applySubst x s v)
applySubst x s (Lab y t)
| x == y = Lab y t
| y `elem` freeVars s = Lab z (applySubst x s (applySubst y (Var z) t))
| otherwise = Lab y (applySubst x s t)
where z = fresh y
fresh x = if x `elem` tabus then fresh (x++"'") else x
tabus = x : y : vars s ++ vars t