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




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.

data ParseResult a Source

The result of parsing something.

data ParseState Source

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




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

data ParseError Source

What you get if parsing fails.




errPos :: Position

where the error occured

errInput :: String

the remaining input

errPrevToken :: String

the previous token

errMsg :: String

hopefully an explanation of what happened

type LexState = IntSource

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.



no layout

Layout Int32

layout at specified column


data ParseFlags Source

There aren't any parser flags at the moment.




parseKeepComments :: Bool

Should comment tokens be returned by the lexer?


Running the parser

initState :: Maybe AbsolutePath -> ParseFlags -> String -> [LexState] -> ParseStateSource

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 :: ParseFlagsSource

The default flags.

parse :: ParseFlags -> [LexState] -> Parser a -> String -> ParseResult aSource

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 aSource

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

getParseInterval :: Parser IntervalSource

The parse interval is between the last position and the current position.


topContext :: Parser LayoutContextSource

Return the current layout context.

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.


parseError :: String -> Parser aSource

parseError = fail

parseErrorAt :: Position -> String -> Parser aSource

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 aSource

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.