Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Parser.Monad

Contents

- The parser monad
- Running the parser
- Manipulating the state
  - Layout
  - Errors

Synopsis

- data Parser a
- data ParseResult a
  - = ParseOk ParseState a
  - | ParseFailed ParseError
- 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]
  - parseAttributes :: !Attributes
  }
- data ParseError
  - = ParseError {
    - errSrcFile :: !SrcFile
    - errPos :: !PositionWithoutFile
    - errInput :: String
    - errPrevToken :: String
    - errMsg :: String
    }
  - | OverlappingTokensError {
    - errRange :: !(Range' SrcFile)
    }
  - | InvalidExtensionError {
    - errPath :: !RangeFile
    - errValidExts :: [String]
    }
  - | ReadFileError {
    - errPath :: !RangeFile
    - errIOError :: IOError
    }
- data ParseWarning
  - = OverlappingTokensWarning {
    - warnRange :: !(Range' SrcFile)
    }
  - | MisplacedAttributes Range String
  - | UnknownPolarity Range String
  - | UnknownAttribute Range String
  - | UnsupportedAttribute Range !(Maybe String)
  - | MultipleAttributes Range !(Maybe String)
- type LexState = Int
- data LayoutBlock = Layout Keyword LayoutStatus Column
- type LayoutContext = [LayoutBlock]
- data LayoutStatus
  - = Tentative
  - | Confirmed
- type Column = Word32
- data ParseFlags = ParseFlags {
  - parseKeepComments :: Bool
  }
- initState :: Maybe RangeFile -> 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

data Parser a Source #

The parse monad.

#### Instances

Instances details

Applicative Parser Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods pure :: a -> Parser a Source # (<*>) :: Parser (a -> b) -> Parser a -> Parser b Source # liftA2 :: (a -> b -> c) -> Parser a -> Parser b -> Parser c Source # (*>) :: Parser a -> Parser b -> Parser b Source # (<*) :: Parser a -> Parser b -> Parser a Source #
Functor Parser Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods fmap :: (a -> b) -> Parser a -> Parser b Source # (<$) :: a -> Parser b -> Parser a Source #
Monad Parser Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods (>>=) :: Parser a -> (a -> Parser b) -> Parser b Source # (>>) :: Parser a -> Parser b -> Parser b Source # return :: a -> Parser a Source #
MonadError ParseError Parser Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods throwError :: ParseError -> Parser a Source # catchError :: Parser a -> (ParseError -> Parser a) -> Parser a Source #
MonadState ParseState Parser Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods get :: Parser ParseState Source # put :: ParseState -> Parser () Source # state :: (ParseState -> (a, ParseState)) -> Parser a Source #

data ParseResult a Source #

The result of parsing something.

Constructors

ParseOk ParseState a |
ParseFailed ParseError |

#### Instances

Instances details

Show a => Show (ParseResult a) Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseResult a -> ShowS Source # show :: ParseResult a -> String Source # showList :: [ParseResult a] -> ShowS Source #

data ParseState Source #

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.

- parseAttributes :: !Attributes

  Every encountered attribute.

#### Instances

Instances details

Show ParseState Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseState -> ShowS Source # show :: ParseState -> String Source # showList :: [ParseState] -> ShowS Source #
MonadState ParseState LexAction Source # |
Instance details Defined in Agda.Syntax.Parser.Alex Methods get :: LexAction ParseState Source # put :: ParseState -> LexAction () Source # state :: (ParseState -> (a, ParseState)) -> LexAction a Source #
MonadState ParseState Parser Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods get :: Parser ParseState Source # put :: ParseState -> Parser () Source # state :: (ParseState -> (a, ParseState)) -> Parser a Source #

data ParseError Source #

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 :: !RangeFile

  The file which the error concerns.

- errValidExts :: [String]

ReadFileError |

Fields

- errPath :: !RangeFile

  The file which the error concerns.

- errIOError :: IOError

#### Instances

Instances details

Pretty ParseError Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods pretty :: ParseError -> Doc Source # prettyPrec :: Int -> ParseError -> Doc Source # prettyList :: [ParseError] -> Doc Source #
HasRange ParseError Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseError -> Range Source #
NFData ParseError Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods rnf :: ParseError -> () Source #
Show ParseError Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseError -> ShowS Source # show :: ParseError -> String Source # showList :: [ParseError] -> ShowS Source #
MonadError ParseError PM Source # |
Instance details Defined in Agda.Syntax.Parser Methods throwError :: ParseError -> PM a Source # catchError :: PM a -> (ParseError -> PM a) -> PM a Source #
MonadError ParseError Parser Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods throwError :: ParseError -> Parser a Source # catchError :: Parser a -> (ParseError -> Parser a) -> Parser a Source #

data ParseWarning Source #

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.

MisplacedAttributes Range String | The `String` is the error message.
UnknownPolarity Range String | Unknown polarity, ignored.
UnknownAttribute Range String | Unknown attribute, ignored. The `Range` includes the "@", the `String` not.
UnsupportedAttribute Range !(Maybe String) | Unsupported attribute.
MultipleAttributes Range !(Maybe String) | Multiple attributes.

#### Instances

Instances details

Pretty ParseWarning Source # | Does not include printing of the range.
Instance details Defined in Agda.Syntax.Parser.Monad Methods pretty :: ParseWarning -> Doc Source # prettyPrec :: Int -> ParseWarning -> Doc Source # prettyList :: [ParseWarning] -> Doc Source #
HasRange ParseWarning Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseWarning -> Range Source #
EmbPrj ParseWarning Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: ParseWarning -> S Word32 Source # icod_ :: ParseWarning -> S Word32 Source # value :: Word32 -> R ParseWarning Source #
NFData ParseWarning Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods rnf :: ParseWarning -> () Source #
Show ParseWarning Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseWarning -> ShowS Source # show :: ParseWarning -> String Source # showList :: [ParseWarning] -> ShowS Source #
MonadState [ParseWarning] PM Source # |
Instance details Defined in Agda.Syntax.Parser Methods get :: PM [ParseWarning] Source # put :: [ParseWarning] -> PM () Source # state :: ([ParseWarning] -> (a, [ParseWarning])) -> PM a Source #

type LexState = Int Source #

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.

Constructors

Layout Keyword LayoutStatus Column | Layout at specified `Column`, introduced by `Keyword`.

#### Instances

Instances details

Show LayoutBlock Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> LayoutBlock -> ShowS Source # show :: LayoutBlock -> String Source # showList :: [LayoutBlock] -> ShowS Source #

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

Instances details

Show LayoutStatus Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> LayoutStatus -> ShowS Source # show :: LayoutStatus -> String Source # showList :: [LayoutStatus] -> ShowS Source #
Eq LayoutStatus Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods (==) :: LayoutStatus -> LayoutStatus -> Bool Source # (/=) :: LayoutStatus -> LayoutStatus -> Bool Source #

type Column = Word32 Source #

A (layout) column.

data ParseFlags Source #

Parser flags.

Constructors

ParseFlags |

Fields

- parseKeepComments :: Bool

  Should comment tokens be returned by the lexer?

#### Instances

Instances details

Show ParseFlags Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseFlags -> ShowS Source # show :: ParseFlags -> String Source # showList :: [ParseFlags] -> ShowS Source #

# Running the parser

initState :: Maybe RangeFile -> 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 #

getParseFlags :: Parser ParseFlags Source #

getLexState :: Parser [LexState] Source #

pushLexState :: LexState -> Parser () Source #

popLexState :: Parser () Source #

## Layout

topBlock :: Parser (Maybe LayoutBlock) Source #

Return the current layout block.

popBlock :: Parser () Source #

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.

parseWarningName :: ParseWarning -> WarningName Source #

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.