module S05 (
  -- * Exercises 2 to 4
  -- | See <../solutions/s05.pdf>.
  Term(..),
  -- * Exercise 5
  vars, freeVars, boundVars,
  -- * Exercise 6
  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