Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 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.
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 :: !Positionposition at current input location
parseLastPos :: !Positionposition of last token
parseInp :: Stringthe current input
parsePrevChar :: !Charthe character before the input
parsePrevToken :: Stringthe 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 :: ParseFlagscurrently there are no flags
data ParseError Source
What you get if parsing fails.
Constructors
ParseError
errPos :: Positionwhere the error occured
errInput :: Stringthe remaining input
errPrevToken :: Stringthe previous token
errMsg :: Stringhopefully 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.
Constructors
NoLayoutno layout
Layout Int32layout at specified column
data ParseFlags Source
There aren't any parser flags at the moment.
Constructors
ParseFlags
parseKeepComments :: BoolShould 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
setParsePos :: Position -> Parser ()Source
setLastPos :: Position -> Parser ()Source
getParseInterval :: Parser IntervalSource
The parse interval is between the last position and the current position.
setPrevToken :: String -> Parser ()Source
getParseFlags :: Parser ParseFlagsSource
getLexState :: Parser [LexState]Source
pushLexState :: LexState -> Parser ()Source
popLexState :: Parser ()Source
Layout
topContext :: Parser LayoutContextSource
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 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.
Produced by Haddock version 2.6.1