module Main where

import Data.List
import Control.Monad
import Text.Parsec
import Text.Parsec.String

-- Definition

type Sym = String

data Term = Var Sym | Lam Sym Term | App Term Term

-- Substituion

freeVars (Var s)     = [s]
freeVars (Lam s e)   = freeVars e  \\ [s]
freeVars (App e1 e2) = freeVars e1 `union` freeVars e2

subst s1 e2 = subst' where
    subst' e1@(Var s1')
        | s1 == s1' = e2
        | otherwise = e1
    subst' e1@(Lam s1' e1')
        | s1 == s1'                            = e1
        | s1' == "_" || s1' `notElem` frees_e2 = Lam s1' (subst' e1')
        | otherwise                            = Lam s1'' e1'' where
            frees_e2     = freeVars e2
            frees_e2_e1' = frees_e2 `union` freeVars e1'
            s1'' = until (`notElem` frees_e2_e1') ('\'':) s1'
            e1'' = subst' (subst s1' (Var s1'') e1')
    subst' (App e1'1 e1'2) = App (subst' e1'1) (subst' e1'2)

-- Beta-reduction

eager into   (App e1 e2) = case (eager into e1, eager into e2) of
	(Lam s1 e1, e2') -> eager into (subst s1 e2' e1)
	(e1'      , e2') -> App e1' e2'
eager into l@(Lam s e)   = if into then Lam s (eager into e) else l
eager _    v             = v

byvalue = eager False
full    = eager True

-- Printing

pretty = tail . pretty' where
    pretty' (Var s)     = " " ++ s
    pretty' (App e1 e2) = (case e1 of
        Lam _ _ -> " (" ++ pretty e1 ++ ") "
        _       -> " "  ++ pretty e1 ++ " "
        ) ++ case e2 of
        Var s2  -> s2
        _       -> "(" ++ pretty e2 ++ ")"
    pretty'  e          = " \\" ++ tail (pretty'' e) where
        pretty'' (Lam s e) = " " ++ s ++ pretty'' e
        pretty''  e        = ". " ++ pretty e

-- Parsing

betweenSpaces = spaces `between` spaces
sep1Spaces p = spaces >> (p `sepEndBy1` spaces)

ident = string "where!" <|> liftM2 (:) (char '_' <|> letter) (many $ alphaNum <|> oneOf "_\'")

parseOne = liftM Var (try ident) <|> (char '(' `between` char ')' $ parseTerm)

parseAlone = liftM2 (flip $ foldr Lam)
    (spaces >> (option [] $ char '\\' `between` char '.' $ sep1Spaces ident))
    (try (liftM (foldl1 App) $ sep1Spaces parseOne) <|> parseAlone)

parseAss = betweenSpaces $ liftM2 (,) ident (betweenSpaces (char '=') >> parseTerm)

parseTerm :: Parser Term
parseTerm = liftM2 (foldr $ \(s, e2) e1 -> App (Lam s e1) e2) parseAlone
    (option [] $ string "where" `between` char '.' $ parseAss `sepBy` (betweenSpaces $ char ';'))

-- Example

evalAndPrint s = case parse parseTerm "" s of
    Left  err -> error $ show err
    Right res -> putStrLn $ pretty $ full $ byvalue res

main = readFile "term.txt" >>= evalAndPrint