module Lambda_Calculus where

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


instance Show Term where
  show (Var name) = name
  show (App fun arg) = f ++ " " ++ a
    where
      f = case fun of
        Abs _ _ -> "(" ++ show fun ++ ")"
        _ -> show fun
      a = case arg of
        App _ _ -> "(" ++ show arg ++ ")"
        _ -> show arg
  show (Abs arg t) = "\\" ++ arg ++ ". " ++ show t 


remove x xs = filter (\y -> y /= x) xs

frees :: Term -> [String]  
frees (Var x) = [x]
frees (App t1 t2) = frees t1 ++ frees t2
frees (Abs x t) = remove x (frees t)

new :: String -> [String] -> String
new n xs = if n `elem` xs then new (n ++ "'") xs else n

{- subst x s t   ~     t[s/x] -}
subst :: String -> Term -> Term -> Term
subst x s (Var y)
  | x == y    = s
  | otherwise = Var y
subst x s (App t1 t2) = App (subst x s t1) (subst x s t2)
subst x s (Abs y t) = Abs n (subst x s (subst y (Var n) t))
  where
    n = new y (frees s ++ remove y (frees t) ++ [x])
    
beta :: Term -> Term
beta (Var x) = Var x
beta (Abs n t) = Abs n t
beta (App (Var n) t) = App (Var n) t
beta (App (Abs n t1) t2) = subst n t2 t1
beta (App (App t1 t2) t3) = App (beta (App t1 t2)) t3