| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Parser.Monad
Synopsis
- data Parser a
- data ParseResult a
- data ParseState = PState {
- parseSrcFile :: !SrcFile
- parsePos :: !PositionWithoutFile
- parseLastPos :: !PositionWithoutFile
- parseInp :: String
- parsePrevChar :: !Char
- parsePrevToken :: String
- parseLayout :: LayoutContext
- parseLayStatus :: LayoutStatus
- parseLayKw :: Keyword
- parseLexState :: [LexState]
- parseFlags :: ParseFlags
- parseWarnings :: ![ParseWarning]
- 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
- type LexState = Int
- data LayoutBlock = Layout Keyword LayoutStatus Column
- type LayoutContext = [LayoutBlock]
- data LayoutStatus
- type Column = Int32
- data ParseFlags = ParseFlags {}
- initState :: Maybe AbsolutePath -> ParseFlags -> String -> [LexState] -> ParseState
- defaultParseFlags :: ParseFlags
- parse :: ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a
- parsePosString :: Position -> ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a
- parseFromSrc :: ParseFlags -> [LexState] -> Parser a -> SrcFile -> String -> ParseResult a
- setParsePos :: PositionWithoutFile -> Parser ()
- setLastPos :: PositionWithoutFile -> Parser ()
- getParseInterval :: Parser Interval
- setPrevToken :: String -> Parser ()
- getParseFlags :: Parser ParseFlags
- getLexState :: Parser [LexState]
- pushLexState :: LexState -> Parser ()
- popLexState :: Parser ()
- topBlock :: Parser (Maybe LayoutBlock)
- popBlock :: Parser ()
- pushBlock :: LayoutBlock -> Parser ()
- getContext :: MonadState ParseState m => m LayoutContext
- setContext :: LayoutContext -> Parser ()
- modifyContext :: (LayoutContext -> LayoutContext) -> Parser ()
- resetLayoutStatus :: Parser ()
- parseWarning :: ParseWarning -> Parser ()
- parseWarningName :: ParseWarning -> WarningName
- parseError :: String -> Parser a
- parseErrorAt :: PositionWithoutFile -> String -> Parser a
- parseError' :: Maybe PositionWithoutFile -> String -> Parser a
- parseErrorRange :: HasRange r => r -> String -> Parser a
- lexError :: String -> Parser a
The parser monad
The parse monad.
Instances
| Applicative Parser Source # | |
| Functor Parser Source # | |
| Monad Parser Source # | |
| MonadError ParseError Parser Source # | |
Defined in Agda.Syntax.Parser.Monad Methods throwError :: ParseError -> Parser a catchError :: Parser a -> (ParseError -> Parser a) -> Parser a | |
| MonadState ParseState Parser Source # | |
Defined in Agda.Syntax.Parser.Monad Methods get :: Parser ParseState put :: ParseState -> Parser () state :: (ParseState -> (a, ParseState)) -> Parser a | |
data ParseResult a Source #
The result of parsing something.
Constructors
| ParseOk ParseState a | |
| ParseFailed ParseError |
Instances
| Show a => Show (ParseResult a) Source # | |
Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseResult a -> ShowS # show :: ParseResult a -> String # showList :: [ParseResult a] -> ShowS # | |
data ParseState Source #
The parser state. Contains everything the parser and the lexer could ever need.
Constructors
| PState | |
Fields
| |
Instances
| Show ParseState Source # | |
Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseState -> ShowS # show :: ParseState -> String # showList :: [ParseState] -> ShowS # | |
| MonadState ParseState LexAction | |
Defined in Agda.Syntax.Parser.Alex | |
| MonadState ParseState Parser Source # | |
Defined in Agda.Syntax.Parser.Monad Methods get :: Parser ParseState put :: ParseState -> Parser () state :: (ParseState -> (a, ParseState)) -> Parser a | |
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 | |
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
For context sensitive lexing alex provides what is called start codes
in the Alex documentation. It is really an integer representing the state
of the lexer, so we call it LexState instead.
data LayoutBlock Source #
We need to keep track of the context to do layout. The context specifies the indentation columns of the open layout blocks. See Agda.Syntax.Parser.Layout for more informaton.
Instances
| Show LayoutBlock Source # | |
Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> LayoutBlock -> ShowS # show :: LayoutBlock -> String # showList :: [LayoutBlock] -> ShowS # | |
type LayoutContext = [LayoutBlock] Source #
The stack of layout blocks.
When we encounter a layout keyword, we push a Tentative block
with noColumn. This is replaced by aproper column once we
reach the next token.
data LayoutStatus Source #
Status of a layout column (see #1145).
A layout column is Tentative until we encounter a new line.
This allows stacking of layout keywords.
Inside a LayoutContext the sequence of Confirmed columns
needs to be strictly increasing.
'Tentative columns between Confirmed columns need to be
strictly increasing as well.
Constructors
| Tentative | The token defining the layout column was on the same line as the layout keyword and we have not seen a new line yet. |
| Confirmed | We have seen a new line since the layout keyword and the layout column has not been superseded by a smaller column. |
Instances
| Show LayoutStatus Source # | |
Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> LayoutStatus -> ShowS # show :: LayoutStatus -> String # showList :: [LayoutStatus] -> ShowS # | |
| Eq LayoutStatus Source # | |
Defined in Agda.Syntax.Parser.Monad | |
data ParseFlags Source #
Parser flags.
Constructors
| ParseFlags | |
Fields
| |
Instances
| Show ParseFlags Source # | |
Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseFlags -> ShowS # show :: ParseFlags -> String # showList :: [ParseFlags] -> ShowS # | |
Running the parser
initState :: Maybe AbsolutePath -> ParseFlags -> String -> [LexState] -> ParseState Source #
Constructs the initial state of the parser. The string argument is the input string, the file path is only there because it's part of a position.
defaultParseFlags :: ParseFlags Source #
The default flags.
parse :: ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a Source #
The most general way of parsing a string. The Agda.Syntax.Parser will define
more specialised functions that supply the ParseFlags and the
LexState.
parsePosString :: Position -> ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a Source #
The even more general way of parsing a string.
parseFromSrc :: ParseFlags -> [LexState] -> Parser a -> SrcFile -> String -> ParseResult a Source #
Parses a string as if it were the contents of the given file Useful for integrating preprocessors.
Manipulating the state
setParsePos :: PositionWithoutFile -> Parser () Source #
setLastPos :: PositionWithoutFile -> Parser () Source #
getParseInterval :: Parser Interval Source #
The parse interval is between the last position and the current position.
setPrevToken :: String -> Parser () Source #
getLexState :: Parser [LexState] Source #
pushLexState :: LexState -> Parser () Source #
popLexState :: Parser () Source #
Layout
pushBlock :: LayoutBlock -> Parser () Source #
getContext :: MonadState ParseState m => m LayoutContext Source #
setContext :: LayoutContext -> Parser () Source #
modifyContext :: (LayoutContext -> LayoutContext) -> Parser () Source #
resetLayoutStatus :: Parser () Source #
When we see a layout keyword, by default we expect a Tentative block.
Errors
parseWarning :: ParseWarning -> Parser () Source #
Records a warning.
parseError :: String -> Parser a Source #
Throw a parse error at the current position.
parseErrorAt :: PositionWithoutFile -> String -> Parser a Source #
Fake a parse error at the specified position. Used, for instance, when lexing nested comments, which when failing will always fail at the end of the file. A more informative position is the beginning of the failing comment.
parseError' :: Maybe PositionWithoutFile -> String -> Parser a Source #
Use parseErrorAt or parseError as appropriate.
parseErrorRange :: HasRange r => r -> String -> Parser a Source #
Report a parse error at the beginning of the given Range'.
lexError :: String -> Parser a Source #
For lexical errors we want to report the current position as the site of
the error, whereas for parse errors the previous position is the one
we're interested in (since this will be the position of the token we just
lexed). This function does parseErrorAt the current position.