|
|
|
|
|
|
Synopsis |
|
|
|
|
The parser monad
|
|
|
|
|
|
The result of parsing something.
| Constructors | |
|
|
|
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
|
|
|
|
|
|
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
|
|
|
|
|
|
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.
|
|
|
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
|
|
|
|
|
There aren't any parser flags at the moment.
| Constructors | ParseFlags | | parseKeepComments :: Bool | Should comment tokens be returned by the lexer?
|
|
|
|
|
Running the parser
|
|
|
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.
|
|
|
The default flags.
|
|
|
The most general way of parsing a string. The Agda.Syntax.Parser will define
more specialised functions that supply the ParseFlags and the
LexState.
|
|
|
The even more general way of parsing a string.
|
|
|
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
|
|
|
|
|
|
|
The parse interval is between the last position and the current position.
|
|
|
|
|
|
|
|
|
|
|
|
Layout
|
|
|
Return the current layout context.
|
|
|
|
|
|
|
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 = fail |
|
|
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.
|
|
|
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.6.1 |