Agda.Syntax.Parser.Monad

The parser monad

data Parser a

The parse monad. Equivalent to StateT ParseState (Either ParseError) except for the definition of fail, which builds a suitable ParseError object.

Instances

Monad Parser

Methods

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

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

return :: a -> Parser a

fail :: String -> Parser a

Functor Parser

Methods

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

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

Applicative Parser

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

MonadState ParseState Parser

Methods

get :: Parser ParseState

put :: ParseState -> Parser ()

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

MonadError ParseError Parser

Methods

throwError :: ParseError -> Parser a

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

data ParseResult a

The result of parsing something.

Constructors

ParseOk ParseState a

ParseFailed ParseError

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 contexts

• parseLexState :: [LexState]

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

• parseFlags :: ParseFlags

  currently there are no flags

Instances

Show ParseState

Methods

showsPrec :: Int -> ParseState -> ShowS

show :: ParseState -> String

showList :: [ParseState] -> ShowS

MonadState ParseState Parser

Methods

get :: Parser ParseState

put :: ParseState -> Parser ()

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

data ParseError

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

Show ParseError

Methods

showsPrec :: Int -> ParseError -> ShowS

show :: ParseError -> String

showList :: [ParseError] -> ShowS

Pretty ParseError

Methods

pretty :: ParseError -> Doc

prettyPrec :: Int -> ParseError -> Doc

prettyList :: [ParseError] -> Doc

HasRange ParseError

Methods

getRange :: ParseError -> Range

MonadError ParseError Parser

Methods

throwError :: ParseError -> Parser a

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

MonadError ParseError PM

Methods

throwError :: ParseError -> PM a

catchError :: PM a -> (ParseError -> PM a) -> PM 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

Instances

Data ParseWarning

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 :: (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

Methods

showsPrec :: Int -> ParseWarning -> ShowS

show :: ParseWarning -> String

showList :: [ParseWarning] -> ShowS

Pretty ParseWarning

Methods

pretty :: ParseWarning -> Doc

prettyPrec :: Int -> ParseWarning -> Doc

prettyList :: [ParseWarning] -> Doc

HasRange ParseWarning

Methods

getRange :: ParseWarning -> Range

type LexState = Int

To do 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 LayoutContext

We need to keep track of the context to do layout. The context specifies the indentation (if any) of a layout block. See Agda.Syntax.Parser.Layout for more informaton.

Constructors

NoLayout

no layout

Layout Int32

layout at specified column

Instances

Show LayoutContext

Methods

showsPrec :: Int -> LayoutContext -> ShowS

show :: LayoutContext -> String

showList :: [LayoutContext] -> ShowS

data ParseFlags

There aren't any parser flags at the moment.

Constructors

ParseFlags

Fields

• parseKeepComments :: Bool

  Should comment tokens be returned by the lexer?

Instances

Show ParseFlags

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.

parseFile :: ParseFlags -> [LexState] -> Parser a -> AbsolutePath -> IO (ParseResult a)

The most general way of parsing a file. The Agda.Syntax.Parser will define more specialised functions that supply the ParseFlags and the LexState.

Note that Agda source files always use the UTF-8 character encoding.

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

topContext :: Parser LayoutContext

Return the current layout context.

popContext :: Parser ()

pushContext :: LayoutContext -> Parser ()

pushCurrentContext :: Parser ()

Should only be used at the beginning of a file. When we start parsing we should be in layout mode. Instead of forcing zero indentation we use the indentation of the first token.

Errors

parseError :: String -> Parser a

parseError = fail

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.

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.