| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Parser
Synopsis
- data Parser a
- parse :: Parser a -> String -> PM a
- parsePosString :: Parser a -> Position -> String -> PM a
- parseFile' :: Show a => Parser a -> AbsolutePath -> PM a
- moduleParser :: Parser Module
- moduleNameParser :: Parser QName
- exprParser :: Parser Expr
- exprWhereParser :: Parser ExprWhere
- holeContentParser :: Parser HoleContent
- tokensParser :: Parser [Token]
- data ParseError
- = ParseError {
- errSrcFile :: !SrcFile
- errPos :: !PositionWithoutFile
- errInput :: String
- errPrevToken :: String
- errMsg :: String
- | OverlappingTokensError { }
- | InvalidExtensionError {
- errPath :: !AbsolutePath
- errValidExts :: [String]
- | ReadFileError {
- errPath :: !AbsolutePath
- errIOError :: IOError
- = ParseError {
- data ParseWarning = OverlappingTokensWarning {}
- newtype PM a = PM {
- unPM :: ExceptT ParseError (StateT [ParseWarning] IO) a
- runPMIO :: MonadIO m => PM a -> m (Either ParseError a, [ParseWarning])
Types
Parse functions
parseFile' :: Show a => Parser a -> AbsolutePath -> PM a #
Parsers
moduleParser :: Parser Module #
Parses a module.
moduleNameParser :: Parser QName #
Parses a module name.
exprParser :: Parser Expr #
Parses an expression.
exprWhereParser :: Parser ExprWhere #
Parses an expression followed by a where clause.
holeContentParser :: Parser HoleContent #
Parses an expression or some other content of an interaction hole.
tokensParser :: Parser [Token] #
Gives the parsed token stream (including comments).
Parse errors
data ParseError #
What you get if parsing fails.
Constructors
| ParseError | Errors that arise at a specific position in the file |
Fields
| |
| OverlappingTokensError | Parse errors that concern a range in a file. |
| InvalidExtensionError | Parse errors that concern a whole file. |
Fields
| |
| ReadFileError | |
Fields
| |
Instances
| Show ParseError # | |
Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseError -> ShowS # show :: ParseError -> String # showList :: [ParseError] -> ShowS # | |
| Pretty ParseError # | |
Defined in Agda.Syntax.Parser.Monad Methods pretty :: ParseError -> Doc # prettyPrec :: Int -> ParseError -> Doc # prettyList :: [ParseError] -> Doc # | |
| HasRange ParseError # | |
Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseError -> Range # | |
| MonadError ParseError Parser # | |
Defined in Agda.Syntax.Parser.Monad Methods throwError :: ParseError -> Parser a # catchError :: Parser a -> (ParseError -> Parser a) -> Parser a # | |
| MonadError ParseError PM # | |
Defined in Agda.Syntax.Parser | |
data ParseWarning #
Warnings for parsing
Constructors
| OverlappingTokensWarning | Parse errors that concern a range in a file. |
Instances
| Data ParseWarning # | |
Defined in Agda.Syntax.Parser.Monad Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ParseWarning -> c ParseWarning # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ParseWarning # toConstr :: ParseWarning -> Constr # dataTypeOf :: ParseWarning -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ParseWarning) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ParseWarning) # gmapT :: (forall b. Data b => b -> b) -> ParseWarning -> ParseWarning # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ParseWarning -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ParseWarning -> r # gmapQ :: (forall d. Data d => d -> u) -> ParseWarning -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ParseWarning -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning # | |
| Show ParseWarning # | |
Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseWarning -> ShowS # show :: ParseWarning -> String # showList :: [ParseWarning] -> ShowS # | |
| Pretty ParseWarning # | |
Defined in Agda.Syntax.Parser.Monad Methods pretty :: ParseWarning -> Doc # prettyPrec :: Int -> ParseWarning -> Doc # prettyList :: [ParseWarning] -> Doc # | |
| HasRange ParseWarning # | |
Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseWarning -> Range # | |
A monad for handling parse results
Constructors
| PM | |
Fields
| |
Instances
| Monad PM # | |
| Functor PM # | |
| Applicative PM # | |
| MonadIO PM # | |
Defined in Agda.Syntax.Parser | |
| MonadError ParseError PM # | |
Defined in Agda.Syntax.Parser | |
runPMIO :: MonadIO m => PM a -> m (Either ParseError a, [ParseWarning]) #