| Safe Haskell | Safe-Inferred |
|---|---|
| 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 -> String -> PM (a, FileType)
- moduleParser :: Parser Module
- moduleNameParser :: Parser QName
- acceptableFileExts :: [String]
- exprParser :: Parser Expr
- exprWhereParser :: Parser ExprWhere
- holeContentParser :: Parser HoleContent
- tokensParser :: Parser [Token]
- readFilePM :: AbsolutePath -> PM Text
- 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
- newtype PM a = PM {
- unPM :: ExceptT ParseError (StateT [ParseWarning] IO) a
- runPMIO :: MonadIO m => PM a -> m (Either ParseError a, [ParseWarning])
Types
Parse functions
Parsers
moduleParser :: Parser Module Source #
Parses a module.
moduleNameParser :: Parser QName Source #
Parses a module name.
acceptableFileExts :: [String] Source #
Extensions supported by parseFile.
exprParser :: Parser Expr Source #
Parses an expression.
exprWhereParser :: Parser ExprWhere Source #
Parses an expression followed by a where clause.
holeContentParser :: Parser HoleContent Source #
Parses an expression or some other content of an interaction hole.
tokensParser :: Parser [Token] Source #
Gives the parsed token stream (including comments).
Reading files.
readFilePM :: AbsolutePath -> PM Text Source #
Returns the contents of the given file.
Parse errors
data ParseError Source #
Parse errors: 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
| HasRange ParseError Source # | |
Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseError -> Range Source # | |
| Pretty ParseError Source # | |
Defined in Agda.Syntax.Parser.Monad Methods pretty :: ParseError -> Doc Source # prettyPrec :: Int -> ParseError -> Doc Source # prettyList :: [ParseError] -> Doc Source # | |
| Show ParseError Source # | |
Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseError -> ShowS # show :: ParseError -> String # showList :: [ParseError] -> ShowS # | |
| MonadError ParseError PM Source # | |
Defined in Agda.Syntax.Parser | |
| MonadError ParseError Parser Source # | |
Defined in Agda.Syntax.Parser.Monad Methods throwError :: ParseError -> Parser a # catchError :: Parser a -> (ParseError -> Parser a) -> Parser a # | |
data ParseWarning Source #
Warnings for parsing.
Constructors
| OverlappingTokensWarning | Parse errors that concern a range in a file. |
| UnsupportedAttribute Range !(Maybe String) | Unsupported attribute. |
| MultipleAttributes Range !(Maybe String) | Multiple attributes. |
Instances
A monad for handling parse errors and warnings.
Constructors
| PM | |
Fields
| |
Instances
| MonadIO PM Source # | |
Defined in Agda.Syntax.Parser | |
| Applicative PM Source # | |
| Functor PM Source # | |
| Monad PM Source # | |
| MonadError ParseError PM Source # | |
Defined in Agda.Syntax.Parser | |
| MonadState [ParseWarning] PM Source # | |
Defined in Agda.Syntax.Parser Methods get :: PM [ParseWarning] # put :: [ParseWarning] -> PM () # state :: ([ParseWarning] -> (a, [ParseWarning])) -> PM a # | |
runPMIO :: MonadIO m => PM a -> m (Either ParseError a, [ParseWarning]) Source #
Run a PM computation, returning a list of warnings in first-to-last order
and either a parse error or the parsed thing.