module Main where

    import Control.Monad.Identity
    import Control.Arrow (second)
    import Text.Parsec

    data Term = Var String
      | Idx Int
      | Abs Term
      | App Term Term
      
    avnames = map (\x -> [x]) "abcdexyzuw"
    names = avnames ++ map ('\'' :) names
    
    nameidx i n (Abs t) = Abs (nameidx (i + 1) n t)
    nameidx i n (App x y) = App (nameidx i n x) (nameidx i n y)
    nameidx i n (Idx d)
      | i == d = Var n
      | otherwise = Idx d
    nameidx _ _ v = v
    
    markfree (Abs t) = Abs (markfree t)
    markfree (App x y) = App (markfree x) (markfree y)
    markfree (Var s) = Var ('*' : s)
    markfree i = i
    
    showTerm :: [String] -> Term -> ShowS
    showTerm (n:ns) (Abs t) =
          showString "(\\"
        . showString n
        . showString ". "
        . showTerm ns (nameidx 0 n t)
        . showString ")"
    showTerm ns (App x y) =
          showChar '('
        . showTerm ns x
        . showChar ' '
        . showTerm ns y
        . showChar ')'
    showTerm ns (Idx i) = ('#' :) . (show i ++)
    showTerm ns (Var s) = (s ++)
    
    instance Show Term where
        show t = showTerm names (markfree t) $ []
    
    type Eval a = Identity a
    
    runEval :: Eval Term -> Term
    runEval = runIdentity
    
    eval :: Term -> Eval Term
    eval (App x y) = do
        x' <- eval x
        case x' of
          (Abs t) -> eval (subst 0 t y)
          proc -> return (App proc y)
    eval other = return other
    
    subst :: Int -> Term -> Term -> Term
    subst i (Idx d) s
      | d == i = s
      | otherwise = Idx d
    subst i (App x y) s = App (subst i x s) (subst i y s)
    subst i (Abs t) s = Abs (subst (i + 1) t s)
    subst i v s = v
    
    setidx :: String -> Int -> Term -> Term
    setidx name i (App x y) = App (setidx name i x) (setidx name i y)
    setidx name i (Abs t) = Abs (setidx name (i + 1) t)
    setidx name i (Var n)
      | name == n = Idx i
      | otherwise = Var n
    setidx _ _ t = t
    
    setVariable :: Term -> (String, Term) -> Term
    setVariable (App x y) bind =
        App (setVariable x bind) (setVariable y bind)
    setVariable (Abs t) bind = Abs (setVariable t bind)
    setVariable (Var s) (name, t')
      | s == name = t'
      | otherwise = Var s
    setVariable other _ = other
    
    identifier :: Parsec String () String
    identifier = many1 alphaNum
    
    lambda :: Parsec String () Term
    lambda = do
        char '('
        char '\\'
        spaces
        varname <- identifier
        spaces
        char '.'
        t <- term
        char ')'
        return $ Abs (setidx varname 0 t)
        
    single :: Parsec String () Term
    single = (spaces >>) $ try (fmap Var identifier) <|> try lambda <|> application
    
    application :: Parsec String () Term
    application = do
        char '('
        f <- term
        char ')'
        return f
    
    substitution :: Parsec String () (String, Term)
    substitution = do
        spaces
        char '['
        spaces
        varname <- identifier
        spaces
        string "->"
        t <- term
        char ']'
        return (varname, t)
    
    procBinds :: [(String, Term)] -> [(String, Term)]
    procBinds = scanl1 $ \x -> second (flip setVariable x)
    
    term :: Parsec String () Term
    term = do
        spaces
        binds <- many (try substitution)
        t <- try (fmap (foldl1 App) (many1 single))
        return (foldl (setVariable) t $ procBinds binds)
            
    lambdaEval str =
        case parse term "lambda" str of
            Right t -> Right $ runEval (eval t)
            Left e -> Left e
    
    loop :: IO ()
    loop = do
      x <- getLine
      case x of
          ":end" -> return ()
          str -> putStr "> " >> print (lambdaEval x) >> loop
    
    main :: IO ()
    main = do
        putStrLn "Lambda-Expressions Evaluator.\n> "
        loop