tapl7.hs

data Term = Var Int
          | Abs Term
          | App Term Term
  deriving Eq

instance Show Term where
  show (Var index)   = show index
  show (Abs body)    = "λ." ++ show body
  show (App lhs rhs) = "(" ++ show lhs ++ " " ++ show rhs ++ ")"

shift :: Int -> Term -> Term
shift distance term =
  let go cutoff v@(Var index)
        | index >= cutoff     = Var $ index + distance
        | otherwise           = v
      go cutoff (Abs body)    = Abs $ go (cutoff + 1) body
      go cutoff (App lhs rhs) = App (go cutoff lhs) (go cutoff rhs)
  in go 0 term

subst :: Int -> Term -> Term -> Term
subst index substitute term =
  let go offset v@(Var index')
        | index' == index + offset = shift offset substitute
        | otherwise                = v
      go offset (Abs body)         = Abs $ go (offset + 1) body
      go offset (App lhs rhs)      = App (go offset lhs) (go offset rhs)
  in go 0 term

evaluate :: Term -> Term
evaluate term =
  let go (App (Abs body) rhs@(Abs _)) = shift (-1) (subst 0 (shift 1 rhs) body)
      go (App lhs@(Abs _) rhs)        = App lhs (go rhs)
      go (App lhs rhs)                = App (go lhs) rhs
      go term                         = term
      term'                           = go term
  in if term' == term then term else evaluate term'