module Lambda where

import Data.List (nub, (\\))

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) = "λ" ++ 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 (Var x) = [x]
vars (App e1 e2) = nub (vars e1 ++ vars e2)
vars (Abs x e) = nub (x : vars e) -- num function from Data.List remove duplicates
vars (Macro _) = []


-- 1.2.
freeVars :: Lambda -> [String]
freeVars (Var x) = [x]
freeVars (App e1 e2) = nub (freeVars e1 ++ freeVars e2)
freeVars (Abs x e) = nub (freeVars e \\ [x]) -- \\ removes x from freeVars e
freeVars (Macro _) = []

-- 1.3.
newVar :: [String] -> String
newVar usedVars = head (filter (`notElem` usedVars) allStrings)
  -- filter (notElem usedVars) allStrings creates a list of all strings that are not in usedVars
  -- head extracts the first element of this filtered list, which is the smallest lexicographical string not in usedVars
  where
    allStrings = map return ['a'..'z'] ++ [ c : s | s <- allStrings, c <- ['a'..'z'] ]
    -- map return ['a'..'z'] generates single-character strings from "a" to "z"
    -- [ c : s | s <- allStrings, c <- ['a'..'z'] ] generates all strings of length 2 or more by prepending a character from "a" to "z" to a string from allStrings


-- 1.4.
isNormalForm :: Lambda -> Bool
isNormalForm (Var _) = True -- a variable is always in normal form
isNormalForm (Abs _ e) = isNormalForm(e) -- an abstraction is in normal form if its body is in normal form
isNormalForm (App e1 e2) = not (isAbs e1) && isNormalForm(e1) && isNormalForm(e2) 
  -- not (isAbs e1): The first part of an application should not be an abstraction for the application to be in normal form.
  -- isNormalForm(e1) && isNormalForm(e2): Both parts of the application must be in normal form
  where
    isAbs (Abs _ _) = True -- helper function to check if a lambda is an abstraction
    isAbs _ = False
isNormalForm (Macro _) = True
  -- a macro is always in normal form

-- Substitution helper
subst :: String -> Lambda -> Lambda -> Lambda
subst x e (Var v)
    | v == x    = e
    | otherwise = Var v
subst x e (App e1 e2) = App (subst x e e1) (subst x e e2)
subst x e (Abs v body)
    | v == x    = Abs v body
    | v `elem` freeVars e = 
        let newVarName = newVar (vars (App (Abs v body) e))
        in Abs newVarName (subst x e (subst v (Var newVarName) body))
    | otherwise = Abs v (subst x e body)
subst _ _ (Macro m) = Macro m

-- 1.5.
reduce :: String -> Lambda -> Lambda -> Lambda
reduce x e1 e2 = subst x e2 e1

-- 1.6.
normalStep :: Lambda -> Lambda
normalStep (Var v) = Var v
normalStep (App (Abs x e1) e2) = reduce x e1 e2
normalStep (App e1 e2) =
    let e1' = normalStep e1
    in if e1' /= e1
       then App e1' e2
       else App e1 (normalStep e2)
normalStep (Abs x e) = Abs x (normalStep e)
normalStep (Macro m) = Macro m

-- 1.7.
applicativeStep :: Lambda -> Lambda
applicativeStep (Var v) = Var v
applicativeStep (App (Abs x e1) e2) =
    let e2' = applicativeStep e2
    in if isNormalForm e2'
       then reduce x e1 e2'
       else App (Abs x e1) e2'
applicativeStep (App e1 e2) =
    let e1' = applicativeStep e1
    in if isNormalForm e1'
       then App e1' (applicativeStep e2)
       else App e1' e2
applicativeStep (Abs x e) = Abs x (applicativeStep e)
applicativeStep (Macro m) = Macro m

-- 1.8.
simplify :: (Lambda -> Lambda) -> Lambda -> [Lambda]   Implementați funcția simplify, care primeste o funcție de step și o aplică până expresia rămâne în formă normală, și întoarce o listă cu toți pași intermediari ai reduceri.