Agda.Syntax.Parser.Monad

The parser monad

data Parser a

The parse monad.

Instances

Applicative Parser

Defined in Agda.Syntax.Parser.Monad

Methods

pure :: a -> Parser a

(<*>) :: Parser (a -> b) -> Parser a -> Parser b

liftA2 :: (a -> b -> c) -> Parser a -> Parser b -> Parser c

(*>) :: Parser a -> Parser b -> Parser b

(<*) :: Parser a -> Parser b -> Parser a

Functor Parser

Defined in Agda.Syntax.Parser.Monad

Methods

fmap :: (a -> b) -> Parser a -> Parser b

(<$) :: a -> Parser b -> Parser a

Monad Parser

Defined in Agda.Syntax.Parser.Monad

Methods

(>>=) :: Parser a -> (a -> Parser b) -> Parser b

(>>) :: Parser a -> Parser b -> Parser b

return :: a -> Parser a

MonadError ParseError Parser

Defined in Agda.Syntax.Parser.Monad

Methods

throwError :: ParseError -> Parser a

catchError :: Parser a -> (ParseError -> Parser a) -> Parser a

MonadState ParseState Parser

Defined in Agda.Syntax.Parser.Monad

Methods

get :: Parser ParseState

put :: ParseState -> Parser ()

state :: (ParseState -> (a, ParseState)) -> Parser a

data ParseResult a

The result of parsing something.

Constructors

ParseOk ParseState a

ParseFailed ParseError

Instances

Show a => Show (ParseResult a)

Defined in Agda.Syntax.Parser.Monad

Methods

showsPrec :: Int -> ParseResult a -> ShowS

show :: ParseResult a -> String

showList :: [ParseResult a] -> ShowS

data ParseState

The parser state. Contains everything the parser and the lexer could ever need.

Constructors

PState

Fields

• parseSrcFile :: !SrcFile
• parsePos :: !PositionWithoutFile

  position at current input location

• parseLastPos :: !PositionWithoutFile

  position of last token

• parseInp :: String

  the current input

• parsePrevChar :: !Char

  the character before the input

• parsePrevToken :: String

  the previous token

• parseLayout :: LayoutContext

  the stack of layout blocks

• parseLayStatus :: LayoutStatus

  the status of the coming layout block

• parseLayKw :: Keyword

  the keyword for the coming layout block

• parseLexState :: [LexState]

  the state of the lexer (states can be nested so we need a stack)

• parseFlags :: ParseFlags

  parametrization of the parser

• parseWarnings :: ![ParseWarning]

  In reverse order.

Instances

Show ParseState

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

Methods

get :: LexAction ParseState

put :: ParseState -> LexAction ()

state :: (ParseState -> (a, ParseState)) -> LexAction a

MonadState ParseState Parser

Defined in Agda.Syntax.Parser.Monad

Methods

get :: Parser ParseState

put :: ParseState -> Parser ()

state :: (ParseState -> (a, ParseState)) -> Parser a

data ParseError

Parse errors: what you get if parsing fails.

Constructors

ParseError

Errors that arise at a specific position in the file

Fields

• errSrcFile :: !SrcFile

  The file in which the error occurred.

• errPos :: !PositionWithoutFile

  Where the error occurred.

• errInput :: String

  The remaining input.

• errPrevToken :: String

  The previous token.

• errMsg :: String

  Hopefully an explanation of what happened.

OverlappingTokensError

Parse errors that concern a range in a file.

Fields

• errRange :: !(Range' SrcFile)

  The range of the bigger overlapping token

InvalidExtensionError

Parse errors that concern a whole file.

Fields

• errPath :: !AbsolutePath

  The file which the error concerns.

• errValidExts :: [String]

ReadFileError

Fields

• errPath :: !AbsolutePath

  The file which the error concerns.

• errIOError :: IOError

Instances

HasRange ParseError

Defined in Agda.Syntax.Parser.Monad

Methods

getRange :: ParseError -> Range

Pretty ParseError

Defined in Agda.Syntax.Parser.Monad

Methods

pretty :: ParseError -> Doc

prettyPrec :: Int -> ParseError -> Doc

prettyList :: [ParseError] -> Doc

Show ParseError

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

Methods

throwError :: ParseError -> PM a

catchError :: PM a -> (ParseError -> PM a) -> PM a

MonadError ParseError Parser

Defined in Agda.Syntax.Parser.Monad

Methods

throwError :: ParseError -> Parser a

catchError :: Parser a -> (ParseError -> Parser a) -> Parser a

data ParseWarning

Warnings for parsing.

Constructors

OverlappingTokensWarning

Parse errors that concern a range in a file.

Fields

• warnRange :: !(Range' SrcFile)

  The range of the bigger overlapping token

UnsupportedAttribute Range !(Maybe String)

Unsupported attribute.

MultipleAttributes Range !(Maybe String)

Multiple attributes.

Instances

HasRange ParseWarning

Defined in Agda.Syntax.Parser.Monad

Methods

getRange :: ParseWarning -> Range

EmbPrj ParseWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ParseWarning -> S Int32

icod_ :: ParseWarning -> S Int32

value :: Int32 -> R ParseWarning

Pretty ParseWarning

Defined in Agda.Syntax.Parser.Monad

Methods

pretty :: ParseWarning -> Doc

prettyPrec :: Int -> ParseWarning -> Doc

prettyList :: [ParseWarning] -> Doc

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 :: forall r r'. (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

NFData ParseWarning

Defined in Agda.Syntax.Parser.Monad

Methods

rnf :: ParseWarning -> ()

MonadState [ParseWarning] PM

Defined in Agda.Syntax.Parser

Methods

get :: PM [ParseWarning]

put :: [ParseWarning] -> PM ()

state :: ([ParseWarning] -> (a, [ParseWarning])) -> PM a

type LexState = Int

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

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.

Constructors

Layout Keyword LayoutStatus Column

Layout at specified Column, introduced by Keyword.

Instances

Show LayoutBlock

Defined in Agda.Syntax.Parser.Monad

Methods

showsPrec :: Int -> LayoutBlock -> ShowS

show :: LayoutBlock -> String

showList :: [LayoutBlock] -> ShowS

type LayoutContext = [LayoutBlock]

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

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

Defined in Agda.Syntax.Parser.Monad

Methods

showsPrec :: Int -> LayoutStatus -> ShowS

show :: LayoutStatus -> String

showList :: [LayoutStatus] -> ShowS

Eq LayoutStatus

Defined in Agda.Syntax.Parser.Monad

Methods

(==) :: LayoutStatus -> LayoutStatus -> Bool

(/=) :: LayoutStatus -> LayoutStatus -> Bool

type Column = Int32

A (layout) column.

data ParseFlags

Parser flags.

Constructors

ParseFlags

Fields

• parseKeepComments :: Bool

  Should comment tokens be returned by the lexer?

Instances

Show ParseFlags

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

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

The default flags.

parse :: ParseFlags -> [LexState] -> Parser a -> String -> ParseResult a

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

The even more general way of parsing a string.

parseFromSrc :: ParseFlags -> [LexState] -> Parser a -> SrcFile -> String -> ParseResult a

Parses a string as if it were the contents of the given file Useful for integrating preprocessors.

Manipulating the state

setParsePos :: PositionWithoutFile -> Parser ()

setLastPos :: PositionWithoutFile -> Parser ()

getParseInterval :: Parser Interval

The parse interval is between the last position and the current position.

setPrevToken :: String -> Parser ()

getParseFlags :: Parser ParseFlags

getLexState :: Parser [LexState]

pushLexState :: LexState -> Parser ()

popLexState :: Parser ()

Layout

topBlock :: Parser (Maybe LayoutBlock)

Return the current layout block.

popBlock :: Parser ()

pushBlock :: LayoutBlock -> Parser ()

getContext :: MonadState ParseState m => m LayoutContext

setContext :: LayoutContext -> Parser ()

modifyContext :: (LayoutContext -> LayoutContext) -> Parser ()

resetLayoutStatus :: Parser ()

When we see a layout keyword, by default we expect a Tentative block.

Errors

parseWarning :: ParseWarning -> Parser ()

Records a warning.

parseWarningName :: ParseWarning -> WarningName

parseError :: String -> Parser a

Throw a parse error at the current position.

parseErrorAt :: PositionWithoutFile -> String -> Parser a

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

Use parseErrorAt or parseError as appropriate.

parseErrorRange :: HasRange r => r -> String -> Parser a

Report a parse error at the beginning of the given Range'.

lexError :: String -> Parser a

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.