parser just about taken care of
This commit is contained in:
parent
57bffe00b5
commit
b236bb1753
3 changed files with 125 additions and 129 deletions
44
lib/IR.hs
Normal file
44
lib/IR.hs
Normal file
|
|
@ -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]
|
||||
187
lib/Parser.hs
187
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
|
||||
|
|
|
|||
23
perga.cabal
23
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
|
||||
|
|
|
|||
Loading…
Reference in a new issue