module Main where

    import Control.Monad.Identity
    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 n
        . (". " ++)
        . showTerm ns (nameidx 0 n t)
        . (")" ++)
    showTerm ns (App x y) =
          ("(" ++)
        . showTerm ns x
        . (" " ++)
        . showTerm ns y
        . (")" ++)
    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 (Var x) s = Var x
    subst i (Abs t) s = Abs (subst (i + 1) t s)
    
    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 :: String -> Term -> Term -> Term
    setVariable name t' (App x y) =
        App (setVariable name t' x) (setVariable name t' y)
    setVariable name t' (Abs t) = Abs (setVariable name t' t)
    setVariable name t' (Var s)
      | 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
        char '['
        spaces
        varname <- identifier
        spaces
        string "->"
        t <- term
        char ']'
        return (varname, t)
    
    term :: Parsec String () Term
    term = do
        spaces
        sub <- try (optionMaybe substitution)
        t <- try (fmap (foldl1 App) (many1 single))
        case sub of
            Nothing -> return t
            Just (var, t') -> return (setVariable var t' t)
            
    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