module LambdaCalc where

import Data.Char (isSpace)

data Term = Variable String
          | Abstraction Term Term
          | Application Term Term
          deriving (Eq)

instance Show Term where
  show (Variable s) = s

  show (Abstraction varName body) = '\x03BB':show varName ++ '.':show body

  show (Application x y) = x' ++ ' ':y'
    where
      x' = if isAbstraction x then '(':show x ++ ")" else show x
      y' = if isVariable y then show y else '(':show y ++ ")"

var :: String -> Term
var "" = error "cannot name a variable with an empty string"
var s
  | any ( \c -> isSpace c || c `elem` "().\x03BB") s = error "name has forbidden characters"
  | otherwise = Variable s

lambda :: String -> Term -> Term
lambda s t = Abstraction (var s) t

apply :: Term -> Term -> Term
apply = Application

infixl 6 <+>
(<+>) :: Term -> Term -> Term
(<+>) = apply

-- same as apply or <+>, but also beta reduces the result
infixl 6 <++>
(<++>) :: Term -> Term -> Term
x <++> y = betaReduce $ x <+> y

isVariable :: Term -> Bool
isVariable (Variable _) = True
isVariable _            = False

isAbstraction :: Term -> Bool
isAbstraction (Abstraction _ _) = True
isAbstraction _                 = False

isApplication :: Term -> Bool
isApplication (Application _ _) = True
isApplication _                 = False

isNormal :: Term -> Bool
isNormal (Variable _) = True
isNormal (Abstraction _ b) = isNormal b
isNormal (Application x y) = not (isAbstraction x) && isNormal x && isNormal y

betaStep :: Term -> Term
betaStep (Variable v)         = Variable v
betaStep (Abstraction v body) = Abstraction v $ betaStep body
betaStep (Application x y)
  | isAbstraction x           = deAbstract x y
  | otherwise                 = Application (betaStep x) (betaStep y)

betaPath :: Term -> [Term]
betaPath e
  | isNormal e = [e]
  | otherwise  = e:betaPath (betaStep e) 

betaReduce :: Term -> Term
betaReduce = last . betaPath

deAbstract :: Term -> Term -> Term
deAbstract (Abstraction v body) arg = go body
  where
    go v'@(Variable _)
      | v == v'          = arg
      | otherwise        = v'
    go a@(Abstraction v' body')
      | v == v'          = a
      | otherwise        = Abstraction v' $ go body'
    go (Application x y) = Application (go x) (go y)
deAbstract _ _ = error "deAbstract: first argument must an abstraction"

{- Common combinators -}

combI :: Term
combI = lambda "x" $ var "x"

identity :: Term
identity = combI

combK :: Term
combK = lambda "a" $ lambda "b" $ var "a"

constant :: Term
constant = combK

combKI :: Term
combKI = lambda "a" $ lambda "b" $ var "b"

combB :: Term
combB = lambda "f" $ lambda "g" $ lambda "a" body
  where
    body = var "f" <+> (var "g" <+> var "a")

compose :: Term
compose = combB

combC :: Term
combC = lambda "f" $ lambda "a" $ lambda "b" $ var "f" <+> var "b" <+> var "a"

{- Boolean values and operations -}

-- assumes valid input
fromBool :: Term -> Bool
fromBool e = case e <++> var "_TRUE" <++> var "_FALSE" of
  Variable "_TRUE"  -> True
  Variable "_FALSE" -> False
  _                 -> error "could not recognize lambda expression as boolean"

bTrue :: Term
bTrue = lambda "x" $ lambda "y" $ var "x"

bFalse :: Term
bFalse = lambda "x" $ lambda "y" $ var "y"

bNot :: Term
bNot = lambda "b" $ var "b" <++> bFalse <++> bTrue

bOr :: Term
bOr = lambda "p" $ lambda "q" body
  where
    body = var "p" <++> var "p" <++> var "q"

bAnd :: Term
bAnd = lambda "p" $ lambda "q" body
  where
    body = var "p" <++> var "q" <++> var "p"

bEq :: Term
bEq = lambda "p" $ lambda "q" body
  where
    body = var "p" <++> var "q" <++> (bNot <++> var "q")

bXor :: Term
bXor = lambda "p" $ lambda "q" body
  where
    body = var "p" <++> (bNot <++> var "q") <++> var "q"

bImplies :: Term
bImplies = lambda "p" $ lambda "q" body
  where
    body = var "p" <++> var "q" <++> bTrue

bConverse :: Term
bConverse = combC <++> bImplies