import Data.List (union, (\\))
import Data.Maybe
type Symb = String
infixl 2 :@
infix 1 `alphaEq`

data Expr = Var Symb
          | Expr :@ Expr
          | Lam Symb Expr
          deriving (Eq, Read, Show)

subst :: Symb -> Expr -> Expr -> Expr
subst v n m = sub m where
  sub e@(Var i)
    | v == i    = n
    | otherwise = e
  sub (f :@ x) = (sub f) :@ (sub x)
  sub (Lam i e)
    | v == i          = Lam i  e
    | i `notElem` fvn = Lam i  (sub e)
    | otherwise       = Lam i' (sub e')
    where
      fvn  = freeVars n
      i' = freshVarName i (fvn `union` freeVars e)
      e' = substVar i i' e

freeVars :: Expr -> [Symb]
freeVars (Var s)   = [s]
freeVars (f :@ a) = freeVars f `union` freeVars a
freeVars (Lam i e) = freeVars e \\ [i]

substVar :: Symb -> Symb -> Expr -> Expr
substVar s s' e = subst s (Var s') e

freshVarName :: Symb -> [Symb] -> Symb
freshVarName j js
  | j `elem` js = freshVarName (j ++ "'") js
  | otherwise   = j

alphaEq :: Expr -> Expr -> Bool
alphaEq (Var v)   (Var v')    = v == v'
alphaEq (f :@ x)  (f' :@ x')  = alphaEq f f' && alphaEq x x'
alphaEq (Lam s e) (Lam s' e')
  | s == s'                   = e `alphaEq` e'
  | otherwise                 =  substVar s fv e `alphaEq` substVar s' fv e'
  where fv = freshVarName s (freeVars e `union` freeVars e')
alphaEq _         _           = False

reduceOnce :: Expr -> Maybe Expr
reduceOnce ((Lam v e) :@ x) = Just $ subst v x e
reduceOnce (f :@ x) | m /= Nothing = Just $ fromJust m :@ x
                    | y /= Nothing = Just $ f :@ (fromJust y)
                    | otherwise = Nothing
                        where
                            m = reduceOnce f
                            y = reduceOnce x
reduceOnce (Lam v e) = if (f /= Nothing) then Just $ Lam v (fromJust f) else Nothing
                           where
                               f = reduceOnce e
reduceOnce _ = Nothing