module Lambda (
  parenthesize
  ) where

import Text.ParserCombinators.Parsec

data BuiltInFunction = Add | Sub

instance Show BuiltInFunction where
  show Add = "+"
  show Sub = "-"

type Variable = Char

data LambdaExpr = Constant Int
                  | Var Variable
                  | Application LambdaExpr LambdaExpr
                  | Abstraction Variable LambdaExpr
                  | BuiltIn BuiltInFunction

parenthesize :: String -> String
parenthesize str = "(" ++ str ++ ")"

instance Show LambdaExpr where
  show expr = case expr of
    Constant c -> show c
    Var variable -> [variable]
    Application expr' expr'' -> show expr' ++ " " ++ show expr''
    Abstraction v expr' -> parenthesize $ "\\" ++ [v] ++ " . " ++ show expr'
    BuiltIn builtIn -> show builtIn

exampleExpr :: LambdaExpr
exampleExpr =
  let plusV = Application (BuiltIn Add) (Var 'v')
      plusVAbstraction = Abstraction 'v' plusV
      plusV4 = Application plusVAbstraction (Constant 4)
      twoPlusFour = Application plusV4 (Constant 2)
  in twoPlusFour


betaReduction :: LambdaExpr -> LambdaExpr
betaReduction (Application (Abstraction v abstractionExpr) expr') = substitute abstractionExpr
  where
    -- substitute v -> expr' in expr
    substitute expr = case expr of
      Abstraction v' expr'' | v' == v -> expr
                            | otherwise -> Abstraction v' (substitute expr'')
      Application op1 op2 -> Application (substitute op1) (substitute op2)
      Var v' | v' == v -> expr'
      x -> x
betaReduction expr = error $ show expr ++ " cannot be beta reduced at the top level"

etaReduction :: LambdaExpr -> LambdaExpr
etaReduction (Abstraction x abstractionExpr) | x `occursFreeIn` abstractionExpr = abstractionExpr
  where
    v `occursFreeIn` expr = case expr of
      (Var v') | v == v' -> True
      (Application e f) -> v `occursFreeIn` e || v `occursFreeIn` f
      (Abstraction w e) -> w /= v && v `occursFreeIn` e
      _ -> False
etaReduction expr = error $ show expr ++ " cannot be eta reduced at the top level"

parseConstant :: Parser LambdaExpr
parseConstant = do
  num <- many1 digit
  return . Constant $ read num

parseVariable :: Parser LambdaExpr
parseVariable = do
  v <- letter
  return $ Var v

parseBuiltIn :: Parser LambdaExpr
parseBuiltIn = do
  operator <- oneOf "+-"
  return . BuiltIn $ case operator of
    '+' -> Add
    '-' -> Sub
    _ -> error $ "Unmatched builtin matched"

wrapParens :: Parser a -> Parser a
wrapParens parser = do
  _ <- char '('
  p <- parser
  _ <- char ')'
  return p

parseAbstraction :: Parser LambdaExpr
parseAbstraction = wrapParens $ do
  _ <- char '\\'
  v <- letter
  _ <- many (char ' ')
  _ <- char '.'
  _ <- many (char ' ')
  expr <- parseExpr
  return $ Abstraction v expr

parseApplication :: Parser LambdaExpr
parseApplication = wrapParens $ do
  expr1 <- parseExpr
  _ <- many (char ' ')
  expr2 <- parseExpr
  return $ Application expr1 expr2

parseExpr :: Parser LambdaExpr
parseExpr = try parseAbstraction <|> try parseConstant <|> try parseVariable <|> try parseBuiltIn <|> parseApplication
