| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Parser
Synopsis
- data Parser a
- parse :: Parser a -> String -> PM (a, Attributes)
- parsePosString :: Parser a -> Position -> String -> PM (a, Attributes)
- parseFile :: Show a => Parser a -> RangeFile -> String -> PM ((a, Attributes), FileType)
- moduleParser :: Parser Module
- moduleNameParser :: Parser QName
- acceptableFileExts :: [String]
- exprParser :: Parser Expr
- exprWhereParser :: Parser ExprWhere
- holeContentParser :: Parser HoleContent
- tokensParser :: Parser [Token]
- readFilePM :: RangeFile -> PM Text
- data ParseError
- = ParseError {
- errSrcFile :: !SrcFile
- errPos :: !PositionWithoutFile
- errInput :: String
- errPrevToken :: String
- errMsg :: String
- | OverlappingTokensError { }
- | InvalidExtensionError {
- errPath :: !RangeFile
- errValidExts :: [String]
- | ReadFileError {
- errPath :: !RangeFile
- errIOError :: IOError
- = ParseError {
- data ParseWarning
- = OverlappingTokensWarning { }
- | UnsupportedAttribute Range !(Maybe String)
- | MultipleAttributes Range !(Maybe String)
- newtype PM a = PM {
- unPM :: ExceptT ParseError (StateT [ParseWarning] IO) a
- runPMIO :: MonadIO m => PM a -> m (Either ParseError a, [ParseWarning])
Types
Parse functions
parsePosString :: Parser a -> Position -> String -> PM (a, Attributes) Source #
Arguments
| :: Show a | |
| => Parser a | |
| -> RangeFile | The file. |
| -> String | The file contents. Note that the file is not read from disk. |
| -> PM ((a, Attributes), FileType) |
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 :: RangeFile -> 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
| Pretty ParseError Source # | |
Defined in Agda.Syntax.Parser.Monad Methods pretty :: ParseError -> Doc Source # prettyPrec :: Int -> ParseError -> Doc Source # prettyList :: [ParseError] -> Doc Source # | |
| HasRange ParseError Source # | |
Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseError -> Range Source # | |
| Show ParseError Source # | |
Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseError -> ShowS show :: ParseError -> String showList :: [ParseError] -> ShowS | |
| MonadError ParseError PM | |
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
| Pretty ParseWarning Source # | |
Defined in Agda.Syntax.Parser.Monad Methods pretty :: ParseWarning -> Doc Source # prettyPrec :: Int -> ParseWarning -> Doc Source # prettyList :: [ParseWarning] -> Doc Source # | |
| HasRange ParseWarning Source # | |
Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseWarning -> Range Source # | |
| EmbPrj ParseWarning Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ParseWarning -> S Int32 Source # icod_ :: ParseWarning -> S Int32 Source # value :: Int32 -> R ParseWarning Source # | |
| NFData ParseWarning Source # | |
Defined in Agda.Syntax.Parser.Monad Methods rnf :: ParseWarning -> () | |
| Show ParseWarning Source # | |
Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseWarning -> ShowS show :: ParseWarning -> String showList :: [ParseWarning] -> ShowS | |
| MonadState [ParseWarning] PM | |
Defined in Agda.Syntax.Parser Methods get :: PM [ParseWarning] put :: [ParseWarning] -> PM () state :: ([ParseWarning] -> (a, [ParseWarning])) -> PM a | |
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.