LambdaR.hs

#!/usr/bin/env runhaskell
{-# LANGUAGE GeneralizedNewtypeDeriving,
             LambdaCase,
             NamedFieldPuns,
             RecordWildCards #-}

import           Control.Applicative ((<$>))
import           Control.Monad
import           Control.Monad.Except
import           Control.Monad.Reader
import           Control.Monad.Writer
import           Data.List (intercalate)
import qualified Data.Map as Map
import           Data.Map (Map)
import           Data.Maybe
import qualified Data.Set as Set
import           Data.Set (Set)
import           Debug.Trace
import           System.Environment
import           Text.ParserCombinators.Parsec hiding (parse)
import qualified Text.ParserCombinators.Parsec as Parsec


data Lambda
  = LAbs String (Lambda)
  | LApp Lambda Lambda
  | LTerm String
  deriving (Eq, Ord)


data Prog
  = Prog (Map String Lambda) Lambda


data Scope
  = Scope
    { context :: Map String Lambda
    }


newtype Generator a
  = Generator
    { runGenerator :: ReaderT Scope (WriterT [Lambda] (Except String)) a
    }
  deriving
    ( Applicative
    , Functor
    , Monad
    , MonadError String
    , MonadReader Scope
    , MonadWriter [Lambda]
    )


instance Show Lambda where
  show (LAbs arg def)
    = "(\\" ++ arg ++ "." ++ show def ++ ")"
  show (LApp lhs rhs)
    = show lhs ++ "(" ++ show rhs ++ ")"
  show (LTerm name)
    = name


instance Show Prog where
  show (Prog defs term)
    = case Map.toList defs of
        [] -> show term
        ds ->
          let defs' = map (\(k, v) -> k ++ " = " ++ show v) ds
          in intercalate ";\n" defs' ++ ";\n" ++ show term


free :: Lambda -> Set String
free (LTerm x)
  = Set.singleton x
free (LApp lhs rhs)
  = free lhs `Set.union` free rhs
free (LAbs x body)
  = Set.delete x (free body)


replace :: String -> Lambda -> Lambda -> Lambda
replace x y (LTerm z)
  | x == z = y
  | otherwise = LTerm z
replace x y (LApp lhs rhs)
  = LApp (replace x y lhs) (replace x y rhs)
replace x y (LAbs z body)
  | x == z = LAbs z body
  | z `Set.member` (free y) = LAbs z' (replace x y (replace z (LTerm z') body))
  | otherwise = LAbs z (replace x y body)
  where
    avail
      = (Set.fromList (map (:[]) ['a'..'z'])
        `Set.difference` (free y))
        `Set.difference` (Set.singleton x)

    z' = (Set.toList avail) !! 0


whitespace :: GenParser Char st ()
whitespace
  = skipMany (space <|> newline)


lambda :: GenParser Char st Lambda
lambda = do
  t:ts <- many1 term
  return $ foldl LApp t ts
  where
    term
      = lTerm <|> lAbs <|> lNest

    lTerm = try $ do
      whitespace
      var <- lower <|> upper
      whitespace
      return $ LTerm [var]

    lAbs = try $ do
      whitespace
      char '\\'
      whitespace
      arg <- lower
      whitespace
      char '.'
      whitespace
      body <- lambda
      return $ LAbs [arg] body

    lNest = try $ do
      whitespace
      char '('
      term <- lambda
      char ')'
      return term


prog :: GenParser Char st Prog
prog = do
  defs <- sepBy def (char ';')
  whitespace
  char ':'
  whitespace
  main <- lambda
  return $ Prog (Map.fromList defs) main
  where
    def = try $ do
      whitespace
      name <- upper
      whitespace
      char '='
      whitespace
      term <- lambda
      return ([name], term)


eval :: Lambda -> Generator Lambda
eval term@(LTerm x) = do
  tell [term]
  Scope{..} <- ask
  case Map.lookup x context of
    Nothing -> return $ LTerm x
    Just t -> eval t

eval term@(LAbs x body) = do
  tell [term]
  body' <- eval body
  return (LAbs x body')

eval term@(LApp (LAbs x body) rhs) = do
  tell [term]
  eval $ replace x rhs body

eval term@(LApp lhs rhs) = do
  tell [term]
  lhs' <- eval lhs
  if lhs == lhs'
    then do
      rhs' <- eval rhs
      return $ LApp lhs rhs'
    else do
      eval (LApp lhs' rhs)


main :: IO ()
main = getArgs >>= \case
  [] -> return ()
  f:_ -> do
    source <- readFile f
    case Parsec.parse prog f source of
      Left err -> putStrLn (show err)
      Right (Prog defs term) -> do
        let scope = Scope defs
        case runExcept . runWriterT . runReaderT (runGenerator (eval term)) $ scope of
          Left err -> putStrLn err
          Right (ret, trace) -> do
            mapM_ (putStrLn . show) trace
            putStrLn (show ret)