module ULC where

import Data.Set as S

--untyped lambda calculus - variables are numbers now as it's easier for renaming
data Term
  = Var Int
  | Abs Int Term
  | App Term Term
  deriving (Eq, Ord)

--Show instance TODO brackets convention
instance Show Term where
  show (Var x)      = show x
  show (App t1 t2)  = '(':show t1 ++ ' ':show t2 ++ ")"
  show (Abs x t1)   = '(':"\x03bb" ++ show x++ "." ++ show t1 ++ ")"

--bound variables of a term
bound :: Term -> Set Int
bound (Var n)      = empty
bound (Abs n t)    = insert n $ bound t
bound (App t1 t2)  = union (bound t1) (bound t2)

--free variables of a term
free :: Term -> Set Int
free (Var n)      = singleton n
free (Abs n t)    = delete n (free t)
free (App t1 t2)  = union (free t1) (free t2)

--test to see if a term is closed (has no free vars)
closed :: Term -> Bool
closed = S.null . free

--subterms of a term
sub :: Term -> Set Term
sub t@(Var x)      = singleton t
sub t@(Abs c t')   = insert t $ sub t'
sub t@(App t1 t2)  = insert t $ union (sub t1) (sub t2)

--element is bound in a term
notfree :: Int -> Term -> Bool
notfree x = not . member x . free

--set of variables in a term
vars :: Term -> Set Int
vars (Var x)      = singleton x
vars (App t1 t2)  = union (vars t1) (vars t2)
vars (Abs x t1)   = insert x $ vars t1

--generates a fresh variable name for a term
newlabel :: Term -> Int
newlabel = (+1) . maximum . vars

--rename t (x,y): renames free occurences of x in t to y
rename :: Term -> (Int, Int) -> Term
rename (Var a) (x,y) = if a == x then Var y else Var a
rename t@(Abs a t') (x,y) = if a == x then t else Abs a $ rename t' (x, y)
rename (App t1 t2) (x,y) = App (rename t1 (x,y)) (rename t2 (x,y))

--substitute one term for another in a term
--does capture avoiding substitution
substitute :: Term -> (Term, Term) -> Term
substitute t1@(Var c1) (Var c2, t2)
  = if c1 == c2 then t2 else t1
substitute (App t1 t2) c
  = App (substitute t1 c) (substitute t2 c)
substitute (Abs y s) c@(Var x, t)
  | y == x = Abs y s
  | y `notfree` t = Abs y $ substitute s c
  | otherwise = Abs z $ substitute (rename s (y,z)) c
  where z = max (newlabel s) (newlabel t)

--eta reduction
eta :: Term -> Maybe Term
eta (Abs x (App t (Var y)))
  | x == y && x `notfree` t = Just t
  | otherwise = Nothing

--term is normal form if has no subterms of the form (\x.s) t
isNormalForm :: Term -> Bool
isNormalForm = not . any testnf . sub
  where
    testnf t = case t of
      (App (Abs _ _) _) -> True
      _ -> False

--one-step reduction relation
reduce1 :: Term -> Maybe Term
reduce1 t@(Var x) = Nothing
reduce1 t@(Abs x s) = case reduce1 s of
  Just s' -> Just $ Abs x s'
  Nothing -> Nothing
reduce1 t@(App (Abs x t1) t2)
  = Just $ substitute t1 (Var x, t2)  --beta conversion
reduce1 t@(App t1 t2) = case reduce1 t1 of
  Just t' -> Just $ App t' t2
  _ -> case reduce1 t2 of
    Just t' -> Just $ App t1 t'
    _ -> Nothing

--multi-step reduction relation - NOT GUARANTEED TO TERMINATE
reduce :: Term -> Term
reduce t = case reduce1 t of
    Just t' -> reduce t'
    Nothing -> t

---multi-step reduction relation that accumulates all reduction steps
reductions :: Term -> [Term]
reductions t = case reduce1 t of
    Just t' -> t' : reductions t'
    _       -> []

--common combinators
i = Abs 1 (Var 1)
true = Abs 1 (Abs 2 (Var 1))
false = Abs 1 (Abs 2 (Var 2))
zero = false
xx = Abs 1 (App (Var 1) (Var 1))
omega = App xx xx
_if = \c t f -> App (App c t) f
_isZero = \n -> _if n false true
_succ = Abs 0 $ Abs 1 $ Abs 2 $ App (Var 1) $ App (App (Var 0) (Var 1)) (Var 2)
appsucc = App _succ

toChurch :: Int -> Term
toChurch n = Abs 0 (Abs 1 (toChurch' n))
  where
    toChurch' 0 = Var 1
    toChurch' n = App (Var 0) (toChurch' (n-1))

test1 = App i (Abs 1 (App (Var 1) (Var 1)))
test2 = App (App (Abs 1 (Abs 2 (Var 2))) (Var 2)) (Var 4)
test3 = App (App (toChurch 3) (Abs 0 (App (Var 0) (toChurch 2)))) (toChurch 1)