2024-06-20 14:31:39 -07:00
|
|
|
{-# OPTIONS_GHC -Wno-missing-export-lists #-}
|
|
|
|
|
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
|
|
|
|
|
|
|
|
|
|
module Parser where
|
|
|
|
|
|
|
|
|
|
import Control.Monad (void)
|
|
|
|
|
import Data.Bifunctor (first)
|
|
|
|
|
import Data.Void (Void)
|
2024-08-28 12:49:47 -07:00
|
|
|
import Lambda (Term (..))
|
2024-06-20 14:31:39 -07:00
|
|
|
import Text.Megaparsec
|
|
|
|
|
import Text.Megaparsec.Char
|
|
|
|
|
import qualified Text.Megaparsec.Char.Lexer as L
|
|
|
|
|
|
|
|
|
|
type Parser = Parsec Void String
|
|
|
|
|
|
|
|
|
|
skipSpace :: Parser ()
|
|
|
|
|
skipSpace =
|
|
|
|
|
L.space
|
|
|
|
|
space1
|
|
|
|
|
(L.skipLineComment "--")
|
|
|
|
|
(L.skipBlockCommentNested "(*" "*)")
|
|
|
|
|
|
|
|
|
|
lexeme :: Parser a -> Parser a
|
|
|
|
|
lexeme = L.lexeme skipSpace
|
|
|
|
|
|
|
|
|
|
pVar :: Parser String
|
|
|
|
|
pVar = label "variable" $ lexeme $ do
|
|
|
|
|
firstChar <- letterChar <|> char '_'
|
|
|
|
|
rest <- many $ alphaNumChar <|> char '_'
|
|
|
|
|
return $ firstChar : rest
|
|
|
|
|
|
|
|
|
|
pLambda :: Parser ()
|
|
|
|
|
pLambda = lexeme $ label "λ" $ void $ string "lambda" <|> string "λ"
|
|
|
|
|
|
|
|
|
|
pAbs :: Parser Term
|
|
|
|
|
pAbs = lexeme $ label "abstraction" $ do
|
|
|
|
|
vars <- between pLambda pDot (many pVar)
|
|
|
|
|
body <- pExpr
|
|
|
|
|
return $ foldr Abs body vars
|
|
|
|
|
|
|
|
|
|
pApp :: Parser Term
|
|
|
|
|
pApp = foldl1 App <$> some pTerm
|
|
|
|
|
|
|
|
|
|
pDot :: Parser ()
|
|
|
|
|
pDot = lexeme $ label "." $ void $ char '.'
|
|
|
|
|
|
|
|
|
|
pTerm :: Parser Term
|
|
|
|
|
pTerm =
|
|
|
|
|
lexeme $
|
|
|
|
|
label "term" $
|
|
|
|
|
choice
|
|
|
|
|
[ between (char '(') (char ')') pExpr
|
|
|
|
|
, Var <$> pVar
|
|
|
|
|
]
|
|
|
|
|
|
|
|
|
|
pExpr :: Parser Term
|
|
|
|
|
pExpr = lexeme $ pAbs <|> pApp
|
|
|
|
|
|
|
|
|
|
pAll :: String -> Either String Term
|
|
|
|
|
pAll = first errorBundlePretty . parse (between skipSpace eof pExpr) ""
|
|
|
|
|
|
|
|
|
|
unwrap :: Either a b -> b
|
|
|
|
|
unwrap (Right x) = x
|
|
|
|
|
|
|
|
|
|
p :: String -> Term
|
|
|
|
|
p = unwrap . pAll
|