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

Safe Haskell | None

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 {
  - parsePos :: !Position
  - parseLastPos :: !Position
  - parseInp :: String
  - parsePrevChar :: !Char
  - parsePrevToken :: String
  - parseLayout :: [LayoutContext]
  - parseLexState :: [LexState]
  - parseFlags :: ParseFlags
  }
- data ParseError = ParseError {
  - errPos :: Position
  - errInput :: String
  - errPrevToken :: String
  - errMsg :: String
  }
- 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
- parseFile :: ParseFlags -> [LexState] -> Parser a -> AbsolutePath -> IO (ParseResult a)
- setParsePos :: Position -> Parser ()
- setLastPos :: Position -> 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 ()
- parseError :: String -> Parser a
- parseErrorAt :: Position -> String -> Parser a
- lexError :: String -> Parser a

# 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 |
Functor Parser |
Applicative Parser |
MonadError ParseError Parser |
MonadState ParseState Parser |

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

parsePos :: !Position

  position at current input location

parseLastPos :: !Position

  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 |
MonadState ParseState Parser |

data ParseError

What you get if parsing fails.

Constructors

ParseError |

Fields

errPos :: Position

  where the error occured

errInput :: String

  the remaining input

errPrevToken :: String

  the previous token

errMsg :: String

  hopefully an explanation of what happened

Instances

Show ParseError |
Typeable ParseError |
Exception ParseError |
HasRange ParseError |
MonadError ParseError Parser |

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 |

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 |

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

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.

# Manipulating the state

setParsePos :: Position -> Parser ()

setLastPos :: Position -> 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 :: Position -> 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.

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.