From b236bb1753e1dfc6b98a492cd7e8a51f75d5616b Mon Sep 17 00:00:00 2001 From: William Ball Date: Sat, 30 Nov 2024 20:34:09 -0800 Subject: [PATCH] parser just about taken care of --- lib/IR.hs | 44 ++++++++++++ lib/Parser.hs | 187 ++++++++++++++++++-------------------------------- perga.cabal | 23 ++++--- 3 files changed, 125 insertions(+), 129 deletions(-) create mode 100644 lib/IR.hs diff --git a/lib/IR.hs b/lib/IR.hs new file mode 100644 index 0000000..b5bedbe --- /dev/null +++ b/lib/IR.hs @@ -0,0 +1,44 @@ +{-# LANGUAGE TemplateHaskell #-} + +module IR where + +import Control.Lens + +type Param = (Text, IRExpr) + +data IRExpr + = Var {_varName :: Text} + | Axiom + | Level {_level :: Integer} + | App + { _appFunc :: IRExpr + , _appArg :: IRExpr + } + | Abs + { _absParamName :: Text + , _absParamType :: IRExpr + , _absBody :: IRExpr + } + | Pi + { _piParamName :: Text + , _piParamType :: IRExpr + , _piBody :: IRExpr + } + | Let + { _letVarName :: Text + , _letAscription :: Maybe IRExpr + , _letValue :: IRExpr + , _letBody :: IRExpr + } + deriving (Show, Eq, Ord) + +makeLenses ''IRExpr + +data IRDef = Def + { _defName :: Text + , _defParams :: [Param] + , _defAscription :: Maybe IRExpr + , _defBody :: IRExpr + } + +type IRProgram = [IRDef] diff --git a/lib/Parser.hs b/lib/Parser.hs index 8297d26..ca5ef3d 100644 --- a/lib/Parser.hs +++ b/lib/Parser.hs @@ -1,37 +1,21 @@ -{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE TupleSections #-} -module Parser (parseDef, parseDefEmpty, parseExpr, parseProgram, handleFile) where +module Parser where -import Check import Control.Monad.Except -import Data.List (elemIndex, foldl, foldl1) -import qualified Data.Map.Strict as M +import Data.List (foldl1) import qualified Data.Text as T import Errors (Error (..)) -import Eval -import Expr (Expr (..), incIndices) +import IR import Preprocessor -import Relude.Extra.Lens -import Text.Megaparsec (ParsecT, ShowErrorComponent (..), between, choice, chunk, customFailure, errorBundlePretty, label, runParserT, try) +import Text.Megaparsec (Parsec, ShowErrorComponent (..), between, choice, chunk, errorBundlePretty, label, runParser, try) import Text.Megaparsec.Char import qualified Text.Megaparsec.Char.Lexer as L -data InnerState = IS {_binders :: [Text], _env :: Env} - -bindsL :: Lens' InnerState [Text] -bindsL = lens _binders setter - where - setter (IS{_env}) new = IS{_env, _binders = new} - -envL :: Lens' InnerState Env -envL = lens _env setter - where - setter (IS{_binders}) new = IS{_env = new, _binders} - newtype TypeError = TE Error deriving (Eq, Ord) -type Parser = ParsecT TypeError Text (State InnerState) +type Parser = Parsec TypeError Text instance ShowErrorComponent TypeError where showErrorComponent (TE e) = toString e @@ -62,142 +46,112 @@ pIdentifier = try $ label "identifier" $ lexeme $ do "Reserved word: " ++ T.unpack ident pure ident -pVar :: Parser Expr -pVar = label "variable" $ lexeme $ do - name <- pIdentifier - binders <- view bindsL <$> get - pure $ Var name . fromIntegral <$> elemIndex name binders ?: Free name +pVar :: Parser IRExpr +pVar = label "variable" $ lexeme $ Var <$> pIdentifier defChoice :: NonEmpty Text -> Parser () defChoice options = lexeme $ label (T.unpack $ head options) $ void $ choice $ fmap chunk options -pParamGroup :: Parser [(Text, Expr)] +pParamGroup :: Parser [Param] pParamGroup = lexeme $ label "parameter group" $ between (char '(') (char ')') $ do idents <- some pIdentifier eat ":" - ty <- pExpr - modify $ over bindsL $ flip (foldl $ flip (:)) idents - pure $ zip idents (iterate incIndices ty) + ty <- pIRExpr + pure $ map (,ty) idents -pSomeParams :: Parser [(Text, Expr)] +pSomeParams :: Parser [Param] pSomeParams = lexeme $ concat <$> some pParamGroup -pManyParams :: Parser [(Text, Expr)] +pManyParams :: Parser [Param] pManyParams = lexeme $ concat <$> many pParamGroup -withBinders :: Parser a -> Parser a -withBinders parser = do - oldBinders <- view bindsL <$> get - result <- parser - modify $ set bindsL oldBinders - pure result - -pLAbs :: Parser Expr -pLAbs = lexeme $ label "λ-abstraction" $ withBinders $ do +pLAbs :: Parser IRExpr +pLAbs = lexeme $ label "λ-abstraction" $ do _ <- defChoice $ "λ" :| ["fun"] params <- pSomeParams _ <- defChoice $ "=>" :| ["⇒"] - body <- pExpr + body <- pIRExpr pure $ foldr (uncurry Abs) body params -pPAbs :: Parser Expr -pPAbs = lexeme $ label "Π-abstraction" $ withBinders $ do +pPAbs :: Parser IRExpr +pPAbs = lexeme $ label "Π-abstraction" $ do _ <- defChoice $ "∏" :| ["forall", "∀"] params <- pSomeParams eat "," - body <- pExpr + body <- pIRExpr pure $ foldr (uncurry Pi) body params -pBinding :: Parser (Text, Expr) +pBinding :: Parser (Text, Maybe IRExpr, IRExpr) pBinding = lexeme $ label "binding" $ do - env <- get eat "(" ident <- pIdentifier params <- pManyParams + ascription <- pAscription eat ":=" - value <- pExpr + value <- pIRExpr eat ")" - put env - modify $ over bindsL (ident :) - pure (ident, foldr (uncurry Abs) value params) + pure + ( ident + , flip (foldr (uncurry Pi)) params <$> ascription + , foldr (uncurry Abs) value params + ) -pLet :: Parser Expr -pLet = lexeme $ label "let expression" $ withBinders $ do +pLet :: Parser IRExpr +pLet = lexeme $ label "let expression" $ do eat "let" bindings <- some pBinding eat "in" - body <- try pExpr + body <- try pIRExpr eat "end" - pure $ foldr (uncurry Let) body bindings + pure $ foldr letTuple body bindings + where + letTuple :: (Text, Maybe IRExpr, IRExpr) -> IRExpr -> IRExpr + letTuple (name, ascription, value) = Let name ascription value -pArrow :: Parser Expr +pArrow :: Parser IRExpr pArrow = lexeme $ label "->" $ do a <- pAppTerm _ <- defChoice $ "->" :| ["→"] - Pi "" a . incIndices <$> pExpr + Pi "" a <$> pIRExpr -pApp :: Parser Expr +pApp :: Parser IRExpr pApp = lexeme $ foldl1 App <$> some pTerm -pStar :: Parser Expr +pStar :: Parser IRExpr pStar = lexeme $ Level 0 <$ eat "*" -pNumSort :: Parser Expr +pNumSort :: Parser IRExpr pNumSort = lexeme $ label "sort" $ eat "*" >> Level <$> L.decimal -pSort :: Parser Expr +pSort :: Parser IRExpr pSort = try pNumSort <|> pStar -checkAscription :: Text -> Expr -> Maybe Expr -> Parser () -checkAscription ident value massert = do - env <- get - ty <- either (customFailure . TE) pure (checkType (env ^. envL) value) - case massert of - Nothing -> updateStateDefinition ident ty value - Just assert -> do - equiv <- either (customFailure . TE) pure (checkBeta (env ^. envL) ty assert) - unless equiv $ customFailure $ TE $ NotEquivalent ty assert value - updateStateDefinition ident assert value +pAxiom :: Parser IRExpr +pAxiom = Axiom <$ eat "axiom" -updateStateDefinition :: Text -> Expr -> Expr -> Parser () -updateStateDefinition ident ty value = do - env <- get - when (M.member ident (env ^. envL)) (customFailure $ TE $ DuplicateDefinition ident) - modify $ over envL $ M.insert ident $ makeDef ty value - -pAxiom :: Text -> Maybe Expr -> Parser () -pAxiom ident Nothing = customFailure $ TE $ PNMissingType ident -pAxiom ident (Just ascription) = do - eat "axiom" - eat ";" - updateStateDefinition ident ascription (Axiom ident) - -pBody :: [(Text, Expr)] -> Text -> Maybe Expr -> Parser () -pBody params ident ascription = do - value <- flip (foldr (uncurry Abs)) params <$> pExpr - checkAscription ident value ascription - eat ";" - -pDef :: Parser () -pDef = lexeme $ label "definition" $ withBinders $ do +pIRDef :: Parser IRDef +pIRDef = lexeme $ label "definition" $ do skipSpace ident <- pIdentifier params <- pManyParams ascription <- fmap (flip (foldr (uncurry Pi)) params) <$> pAscription eat ":=" - choice [pAxiom ident ascription, pBody params ident ascription] + body <- pIRExpr + eat ";" + pure $ Def ident params ascription body -pTerm :: Parser Expr +pTerm :: Parser IRExpr pTerm = lexeme $ label "term" $ choice - [ between (char '(') (char ')') pExpr + [ between (char '(') (char ')') pIRExpr , pSort + , pAxiom , pVar ] -pAppTerm :: Parser Expr +pAppTerm :: Parser IRExpr pAppTerm = lexeme $ choice @@ -207,33 +161,26 @@ pAppTerm = , pApp ] -pExpr :: Parser Expr -pExpr = lexeme $ try pArrow <|> pAppTerm +pIRExpr :: Parser IRExpr +pIRExpr = lexeme $ try pArrow <|> pAppTerm -pAscription :: Parser (Maybe Expr) -pAscription = lexeme $ optional $ try $ defChoice (pure ":") >> label "type" pExpr +pAscription :: Parser (Maybe IRExpr) +pAscription = lexeme $ optional $ try $ eat ":" >> label "type" pIRExpr -pProgram :: Parser Env -pProgram = lexeme $ skipSpace >> many pDef >> _env <$> get +pIRProgram :: Parser IRProgram +pIRProgram = many pIRDef -emptyBinders :: Env -> InnerState -emptyBinders env = IS{_binders = [], _env = env} +parserWrapper :: Parser a -> String -> Text -> Either String a +parserWrapper p filename input = first errorBundlePretty $ runParser p filename input -parseDef :: Text -> State Env (Either String ()) -parseDef input = do - env <- get - let (output, IS{_env}) = runState (runParserT pDef "" input) (emptyBinders env) - put _env - pure $ first errorBundlePretty output +parseProgram :: String -> Text -> Either String IRProgram +parseProgram = parserWrapper pIRProgram -parseExpr :: Env -> Text -> Either String Expr -parseExpr env input = first errorBundlePretty $ evalState (runParserT pExpr "" input) $ emptyBinders env +parseDef :: String -> Text -> Either String IRDef +parseDef = parserWrapper pIRDef -parseDefEmpty :: Env -> Text -> (Either String (), Env) -parseDefEmpty env input = runState (parseDef input) env +parseExpr :: String -> Text -> Either String IRExpr +parseExpr = parserWrapper pIRExpr -parseProgram :: Env -> Text -> Either String Env -parseProgram initial input = first errorBundlePretty $ evalState (runParserT pProgram "" input) $ emptyBinders initial - -handleFile :: Env -> String -> ExceptT String IO Env -handleFile initial filename = (toString `withExceptT` runPreprocessor filename) >>= liftEither . parseProgram initial +handleFile :: String -> ExceptT String IO IRProgram +handleFile filename = (toString `withExceptT` runPreprocessor filename) >>= hoistEither . parseProgram filename diff --git a/perga.cabal b/perga.cabal index de684d6..0b3cf4a 100644 --- a/perga.cabal +++ b/perga.cabal @@ -26,25 +26,30 @@ common warnings library perga-lib import: warnings exposed-modules: Check - Parser - Expr - Eval + Elaborator Errors + Eval + Expr + IR + Parser Preprocessor hs-source-dirs: lib build-depends: base ^>=4.19.1.0 , relude - , mtl - , megaparsec - , parser-combinators , filepath + , lens + , megaparsec + , mtl + , parser-combinators mixins: base hiding (Prelude) , relude (Relude as Prelude) , relude default-language: Haskell2010 default-extensions: OverloadedStrings , GADTs + , DuplicateRecordFields + , OverloadedRecordDot executable perga import: warnings @@ -53,11 +58,11 @@ executable perga build-depends: base ^>=4.19.1.0 , relude - , perga-lib - , haskeline - , mtl , directory , filepath + , haskeline + , mtl + , perga-lib mixins: base hiding (Prelude) , relude (Relude as Prelude) , relude