module Lambda where

import Data.List (union, intersect)
import Data.Char (chr, ord)

data Lambda = Var String
            | App Lambda Lambda
            | Abs String Lambda
            | Macro String

instance Show Lambda where
    show (Var x) = x
    show (App e1 e2) = "(" ++ show e1 ++ " " ++ show e2 ++ ")"
    show (Abs x e) = "L" ++ x ++ "." ++ show e
    show (Macro x) = x

-- λ

instance Eq Lambda where
    e1 == e2 = eq e1 e2 ([],[],[])
      where
        eq (Var x) (Var y) (env,xb,yb) = elem (x,y) env || (not $ elem x xb || elem y yb)
        eq (App e1 e2) (App f1 f2) env = eq e1 f1 env && eq e2 f2 env
        eq (Abs x e) (Abs y f) (env,xb,yb) = eq e f ((x,y):env,x:xb,y:yb)
        eq (Macro x) (Macro y) _ = x == y
        eq _ _ _ = False

-- 1.1.
vars :: Lambda -> [String]
vars l = case l of
          Var x -> [x]
          App e1 e2 -> vars e1 `union` vars e2
          Abs x e -> [x] `union` vars e
          Macro x -> [x]


-- 1.2.
freeVarsHelper :: Lambda -> [String] -> [String]
freeVarsHelper l lst = case l of
                        Var x -> if x `elem` lst  then [] else [x]
                        App e1 e2 -> freeVarsHelper e1 lst `union` freeVarsHelper e2 lst
                        Abs x e -> freeVarsHelper e (x : lst)
                        Macro x -> if x `elem` lst  then [] else [x]

freeVars :: Lambda -> [String]
freeVars l = freeVarsHelper l []

bondedVars :: Lambda -> [String]
bondedVars l = filter (`notElem` freeVars l) (vars l)

-- 1.3.
nextString :: String -> String
nextString s
  | null s = ['a']
  | last s == 'z' = nextString (init s) ++ ['a']
  | otherwise = init s ++ [nextChar (last s)]
                      where nextChar ch = chr (ord ch + 1)

newVarHelper :: String -> [String] -> String
newVarHelper s lst = if s `elem` lst then newVarHelper (nextString s) lst else s

newVar :: [String] -> String
newVar = newVarHelper ['a']

-- 1.4.
isNormalForm :: Lambda -> Bool
isNormalForm l = case l of
                  App e1 e2 -> case e1 of
                    Abs _ _ -> False
                    _ -> isNormalForm e1 && isNormalForm e2
                  Abs _ e -> isNormalForm e
                  _ -> True

-- 1.5.
changeVar :: Lambda -> String -> [String] -> Lambda
changeVar l s lst = case l of
                      Var x -> if x == s then Var $ newVar lst else Var x
                      App e1 e2 -> App (changeVar e1 s lst) (changeVar e2 s lst)
                      Abs x e -> if x == s then Abs (newVar lst) (changeVar e s lst) else Abs x (changeVar e s lst)
                      Macro x -> if x == s then Var $ newVar lst else Var x


addString :: String -> [String] -> [String]
addString s lst = nextString s : lst

changeVars :: Lambda -> [String] -> [String] -> Lambda
changeVars l bad lst = case bad of
                        [] -> l
                        x : xs -> changeVars (changeVar l x lst) xs (addString x lst)

reduceHelper :: String -> Lambda -> Lambda -> Lambda
reduceHelper s l1 l2 = case l1 of
    Var x -> if x == s then l2 else Var x
    App e1 e2 -> App (reduceHelper s e1 l2) (reduceHelper s e2 l2)
    Abs x e -> if x == s
               then Abs x e
               else Abs x (reduceHelper s e l2)
    Macro x -> if x == s then l2 else Var x

reduce :: String -> Lambda -> Lambda -> Lambda
reduce x e1 e2 =
  reduceHelper x e1 (changeVars e2 ( bondedVars e1 `intersect` freeVars e2) (vars e1 `union` vars e2))


-- 1.6.
normalStep :: Lambda -> Lambda
normalStep l = if isNormalForm l then l else case l of
                App (Abs x e1) e2 -> reduce x e1 e2
                App e1 e2 -> if not (isNormalForm e1) then App (normalStep e1) e2 else App e1 (normalStep e2) 
                  -- App (normalStep e1) (normalStep e2)
                Abs x e -> Abs x (normalStep e)
                _ -> l

-- 1.7.
applicativeStep :: Lambda -> Lambda
applicativeStep l = if isNormalForm l then l else case l of
                App (Abs x1 e1) (Abs x2 e2) -> reduce x1 e1 (Abs x2 e2)
                App (Abs x1 e1) (Var x2) -> reduce x1 e1 (Var x2)
                App (Abs x1 e1) (Macro x2) -> reduce x1 e1 (Macro x2)
                App (Abs x e1) e2 -> App (Abs x e1) (applicativeStep e2)
                App e1 e2 -> App (applicativeStep e1) e2
                _ -> l

-- 1.8.
simplify :: (Lambda -> Lambda) -> Lambda -> [Lambda]
simplify func l
  | isNormalForm l = [l]
  | otherwise = l : simplify func (func l)

normal :: Lambda -> [Lambda]
normal = simplify normalStep

applicative :: Lambda -> [Lambda]
applicative = simplify applicativeStep