Agda-2.6.0.1: 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]
  - parseLexState :: [LexState]
  - parseFlags :: ParseFlags
  }
- data ParseError
  - = ParseError {
    - errSrcFile :: !SrcFile
    - errPos :: !PositionWithoutFile
    - errInput :: String
    - errPrevToken :: String
    - errMsg :: String
    }
  - | OverlappingTokensError {
    - errRange :: !(Range' SrcFile)
    }
  - | InvalidExtensionError {
    - errPath :: !AbsolutePath
    - errValidExts :: [String]
    }
  - | ReadFileError {
    - errPath :: !AbsolutePath
    - errIOError :: IOError
    }
- data ParseWarning = OverlappingTokensWarning {
  - warnRange :: !(Range' SrcFile)
  }
- type LexState = Int
- data LayoutContext
  - = NoLayout
  - | Layout Int32
- data ParseFlags = ParseFlags {
  - parseKeepComments :: Bool
  }
- 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 ()
- topContext :: Parser LayoutContext
- popContext :: Parser ()
- pushContext :: LayoutContext -> Parser ()
- pushCurrentContext :: 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

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 # fail :: String -> 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 #
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 #
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 #
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 ParseResult a Source #

The result of parsing something.

Constructors

ParseOk ParseState a |
ParseFailed ParseError |

Instances

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 contexts

- parseLexState :: [LexState]

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

- parseFlags :: ParseFlags

  parametrization of the parser

Instances

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

  The file which the error concerns.

- errValidExts :: [String]

ReadFileError |

Fields

- errPath :: !AbsolutePath

  The file which the error concerns.

- errIOError :: IOError

Instances

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 #
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 #
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 #
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 #

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

Instances

Data ParseWarning Source # |

Instance details

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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ParseWarning Source #

toConstr :: ParseWarning -> Constr Source #

dataTypeOf :: ParseWarning -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ParseWarning) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ParseWarning) Source #

gmapT :: (forall b. Data b => b -> b) -> ParseWarning -> ParseWarning Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ParseWarning -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ParseWarning -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ParseWarning -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ParseWarning -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ParseWarning -> m 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 #
Pretty ParseWarning Source # |
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 #

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 LayoutContext Source #

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 Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> LayoutContext -> ShowS Source # show :: LayoutContext -> String Source # showList :: [LayoutContext] -> ShowS Source #

data ParseFlags Source #

Parser flags.

Constructors

ParseFlags |

Fields

- parseKeepComments :: Bool

  Should comment tokens be returned by the lexer?

Instances

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 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 #

getParseFlags :: Parser ParseFlags Source #

getLexState :: Parser [LexState] Source #

pushLexState :: LexState -> Parser () Source #

popLexState :: Parser () Source #

## Layout

topContext :: Parser LayoutContext Source #

Return the current layout context.

popContext :: Parser () Source #

pushContext :: LayoutContext -> Parser () Source #

pushCurrentContext :: Parser () Source #

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

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.