| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 Int

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

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

The result of parsing something.
Constructors

ParseOk ParseState a |
ParseFailed ParseError |

data ParseState | Source

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

PState |

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

What you get if parsing fails.
Constructors

ParseError |

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

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 | 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 Int | layout at specified column

Instances

Show LayoutContext

data ParseFlags | Source

There aren't any parser flags at the moment.
Constructors

ParseFlags |

parseKeepComments :: Bool | Should comment tokens be returned by the lexer?

Instances

Show ParseFlags

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.

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

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 () | Source

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

parseError :: String -> Parser a | Source

    parseError = fail

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

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.
Produced by Haddock version 2.4.2