91 lines
2 KiB
Haskell
91 lines
2 KiB
Haskell
|
module Parser where
|
|||
|
|
|
|||
|
|
import Control.Monad (void)
|
|||
|
|
import Data.Bifunctor (first)
|
|||
|
|
import Data.Void (Void)
|
|||
|
|
import Expr (Expr (..))
|
|||
|
|
import Text.Megaparsec
|
|||
|
|
( MonadParsec (eof, label),
|
|||
|
|
Parsec,
|
|||
|
|
between,
|
|||
|
|
choice,
|
|||
|
|
errorBundlePretty,
|
|||
|
|
parse,
|
|||
|
|
(<|>),
|
|||
|
|
)
|
|||
|
|
import Control.Applicative.Combinators.NonEmpty (some)
|
|||
|
|
import Text.Megaparsec.Char
|
|||
|
|
( char,
|
|||
|
|
space1,
|
|||
|
|
string,
|
|||
|
|
)
|
|||
|
|
import qualified Text.Megaparsec.Char.Lexer as L
|
|||
|
|
import Data.Either (fromRight)
|
|||
|
|
|
|||
|
|
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 Integer
|
|||
|
|
pVar = label "variable" $ lexeme L.decimal
|
|||
|
|
|
|||
|
|
-- 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 "λ"
|
|||
|
|
|
|||
|
|
pPi :: Parser ()
|
|||
|
|
pPi = lexeme $ label "Π" $ void $ string "Pi" <|> string "Π"
|
|||
|
|
|
|||
|
|
pLAbs :: Parser Expr
|
|||
|
|
pLAbs = lexeme $ label "λ-abstraction" $ do
|
|||
|
|
Abs <$> between pLambda pDot pExpr <*> pExpr
|
|||
|
|
|
|||
|
|
pPAbs :: Parser Expr
|
|||
|
|
pPAbs = lexeme $ label "Π-abstraction" $ do
|
|||
|
|
Pi <$> between pPi pDot pExpr <*> pExpr
|
|||
|
|
|
|||
|
|
pApp :: Parser Expr
|
|||
|
|
pApp = foldl1 App <$> some pTerm
|
|||
|
|
|
|||
|
|
pDot :: Parser ()
|
|||
|
|
pDot = lexeme $ label "." $ void $ char '.'
|
|||
|
|
|
|||
|
|
pStar :: Parser Expr
|
|||
|
|
pStar = lexeme $ label "∗" $ Star <$ (string "*" <|> string "∗")
|
|||
|
|
|
|||
|
|
pSquare :: Parser Expr
|
|||
|
|
pSquare = lexeme $ label "□" $ Square <$ (string "□" <|> string "[]")
|
|||
|
|
|
|||
|
|
pTerm :: Parser Expr
|
|||
|
|
pTerm =
|
|||
|
|
lexeme $
|
|||
|
|
label "term" $
|
|||
|
|
choice
|
|||
|
|
[ between (char '(') (char ')') pExpr,
|
|||
|
|
Var <$> pVar,
|
|||
|
|
pStar,
|
|||
|
|
pSquare
|
|||
|
|
]
|
|||
|
|
|
|||
|
|
pExpr :: Parser Expr
|
|||
|
|
pExpr = lexeme $ pLAbs <|> pApp <|> pPAbs
|
|||
|
|
|
|||
|
|
pAll :: String -> Either String Expr
|
|||
|
|
pAll = first errorBundlePretty . parse (between skipSpace eof pExpr) ""
|
|||
|
|
|
|||
|
|
p :: String -> Expr
|
|||
|
|
p = fromRight Star . pAll
|