Lambda.hs

{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell   #-}

module Lambda.Parser where

import           Viper.Prelude

import           Data.Attoparsec.Text
import           Data.Eq.Deriving           ( deriveEq1 )
import           Data.Functor.Foldable      ( Fix( Fix ) )
import qualified Data.Text             as T
import           Text.Show.Deriving         ( deriveShow1 )

data ExprF e
  = IConst IntConst
  | Var Variable
  | Appl e e
  | Ab Variable e
  deriving (Eq, Ord, Read, Show)

type Expr = Fix ExprF

newtype Variable = Variable Text
  deriving (Eq, Ord, Read, Show)

newtype IntConst = IntConst Integer
  deriving (Eq, Ord, Read, Show)

mkIConst :: IntConst -> Expr
mkIConst = Fix . IConst

mkVar :: Variable -> Expr
mkVar = Fix . Var

mkAppl :: Expr -> Expr -> Expr
mkAppl = Fix ... Appl

mkAb :: Variable -> Expr -> Expr
mkAb = Fix ... Ab

parseExpr :: Text -> Either Text Expr
parseExpr = first T.pack . parseOnly expr

expr :: Parser Expr
expr = intConst <|> ab <|> var <|> appl

intConst :: Parser Expr
intConst = do
  digits <- (many . satisfy . inClass $ "0-9")
  case readMaybe digits of
    Just n  -> pure . mkIConst . IntConst $ n
    Nothing -> empty

var :: Parser Expr
var = mkVar <$> variable

variable :: Parser Variable
variable = Variable . T.pack <$> ((:) <$> upper <*> many' (letter <|> digit))

appl :: Parser Expr
appl = mkAppl <$> lexeme expr <*> lexeme expr

ab :: Parser Expr
ab = do
  void $ lexeme "λ"
  v <- variable
  void $ lexeme "."
  e <- expr
  pure $ mkAb v e

lexeme :: Parser a -> Parser a
lexeme p = ws *> p <* ws

ws :: Parser String
ws = many (satisfy $ inClass " \t\r\n")

upper :: Parser Char
upper = satisfy $ inClass "A-Z"

lower :: Parser Char
lower = satisfy $ inClass "a-z"

$(deriveEq1   ''ExprF)
$(deriveShow1 ''ExprF)