:: a typeCtrl KGHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27
ModuleAgda-2.7.0.1Haskell2010
The parse monad.
Monad ParserDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadFunctor ParserDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadApplicative ParserDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadMonadError ParseError ParserDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadMonadState ParseState ParserDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadThe result of parsing something.
Show a => Show (ParseResult a)Defined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadThe parser state. Contains everything the parser and the lexer could ever need.
PStateparseSrcFile :: !SrcFileparsePos :: !PositionWithoutFileposition at current input location
parseLastPos :: !PositionWithoutFileposition of last token
parseInp :: Stringthe current input
parsePrevChar :: !Charthe character before the input
parsePrevToken :: Stringthe previous token
parseLayout :: LayoutContextthe stack of layout blocks
parseLayStatus :: LayoutStatusthe status of the coming layout block
parseLayKw :: Keywordthe keyword for the coming layout block
parseLexState :: [LexState]the state of the lexer (states can be nested so we need a stack)
parseFlags :: ParseFlagsparametrization of the parser
parseWarnings :: ![ParseWarning]In reverse order.
parseAttributes :: !AttributesEvery encountered attribute.
Show ParseStateDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadMonadState ParseState LexActionDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.AlexMonadState ParseState ParserDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadParse errors: what you get if parsing fails.
ParseErrorErrors that arise at a specific position in the file
errSrcFile :: !SrcFileThe file in which the error occurred.
errPos :: !PositionWithoutFileWhere the error occurred.
errInput :: StringThe remaining input.
errPrevToken :: StringThe previous token.
errMsg :: StringHopefully an explanation of what happened.
OverlappingTokensErrorParse errors that concern a range in a file.
InvalidExtensionErrorParse errors that concern a whole file.
errPath :: !RangeFileThe file which the error concerns.
errValidExts :: [String]ReadFileErrorerrPath :: !RangeFileThe file which the error concerns.
errIOError :: IOErrorShow ParseErrorDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadPretty ParseErrorDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadHasRange ParseErrorDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadMonadError ParseError PMDefined in Agda-2.7.0.1 · Agda.Syntax.ParserMonadError ParseError ParserDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadWarnings for parsing.
OverlappingTokensWarningParse errors that concern a range in a file.
UnsupportedAttribute Range !(Maybe String)Unsupported attribute.
MultipleAttributes Range !(Maybe String)Multiple attributes.
Show ParseWarningDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadNFData ParseWarningDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadPretty ParseWarningDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadHasRange ParseWarningDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadEmbPrj ParseWarningDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Errors · orphanMonadState [ParseWarning] PMDefined in Agda-2.7.0.1 · Agda.Syntax.ParserFor 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.
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.
Show LayoutBlockDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadThe 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.
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.
Eq LayoutStatusDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadShow LayoutStatusDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadA (layout) column.
Parser flags.
ParseFlagsparseKeepComments :: BoolShould comment tokens be returned by the lexer?
Show ParseFlagsDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.MonadConstructs 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.
The default flags.
The most general way of parsing a string. The Agda.Syntax.Parser will define more specialised functions that supply the ParseFlags and the LexState.
The even more general way of parsing a string.
Parses a string as if it were the contents of the given file Useful for integrating preprocessors.
The parse interval is between the last position and the current position.
Return the current layout block.
When we see a layout keyword, by default we expect a Tentative block.
Records a warning.
Throw a parse error at the current position.
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.
Use parseErrorAt or parseError as appropriate.
Report a parse error at the beginning of the given Range.
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.