Safe Haskell	None
Language	Haskell2010

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 {
- parseSrcFile :: !SrcFile
- parsePos :: !PositionWithoutFile
- parseLastPos :: !PositionWithoutFile
- parseInp :: String
- parsePrevChar :: !Char
- parsePrevToken :: String
- parseLayout :: [LayoutContext]
- parseLexState :: [LexState]
- parseFlags :: ParseFlags
}
data ParseError
- = ParseError {
  - errSrcFile :: !SrcFile
  - errPos :: !PositionWithoutFile
  - errInput :: String
  - errPrevToken :: String
  - errMsg :: String
  }
- | OverlappingTokensError {
  - errRange :: !(Range' SrcFile)
  }
- | InvalidExtensionError {
  - errPath :: !AbsolutePath
  - errValidExts :: [String]
  }
- | ReadFileError {
  - errPath :: !AbsolutePath
  - errIOError :: IOError
  }
data ParseWarning = OverlappingTokensWarning {
- warnRange :: !(Range' SrcFile)
}
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
parseFromSrc :: ParseFlags -> [LexState] -> Parser a -> SrcFile -> String -> ParseResult a
setParsePos :: PositionWithoutFile -> Parser ()
setLastPos :: PositionWithoutFile -> 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 ()
parseWarningName :: ParseWarning -> WarningName
parseError :: String -> Parser a
parseErrorAt :: PositionWithoutFile -> String -> Parser a
parseError' :: Maybe PositionWithoutFile -> String -> Parser a
parseErrorRange :: HasRange r => r -> String -> Parser a
lexError :: String -> Parser a

The parser monad

data Parser a Source #

The parse monad.

Instances

Instances details

Monad Parser Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods (>>=) :: Parser a -> (a -> Parser b) -> Parser b # (>>) :: Parser a -> Parser b -> Parser b # return :: a -> Parser a #
Functor Parser Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods fmap :: (a -> b) -> Parser a -> Parser b # (<$) :: a -> Parser b -> Parser a #
Applicative Parser Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods pure :: a -> Parser a # (<>) :: Parser (a -> b) -> Parser a -> Parser b # liftA2 :: (a -> b -> c) -> Parser a -> Parser b -> Parser c # (>) :: Parser a -> Parser b -> Parser b # (<*) :: Parser a -> Parser b -> Parser a #
MonadState ParseState Parser Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods get :: Parser ParseState # put :: ParseState -> Parser () # state :: (ParseState -> (a, ParseState)) -> Parser a #
MonadError ParseError Parser Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods throwError :: ParseError -> Parser a # catchError :: Parser a -> (ParseError -> Parser a) -> Parser a #

data ParseResult a Source #

The result of parsing something.

Constructors

ParseOk ParseState a
ParseFailed ParseError

Instances

Instances details

Show a => Show (ParseResult a) Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseResult a -> ShowS # show :: ParseResult a -> String # showList :: [ParseResult a] -> ShowS #

data ParseState Source #

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

Constructors

PState

Fields

parseSrcFile :: !SrcFile
parsePos :: !PositionWithoutFile
position at current input location
parseLastPos :: !PositionWithoutFile
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
parametrization of the parser

Instances

Instances details

Show ParseState Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseState -> ShowS # show :: ParseState -> String # showList :: [ParseState] -> ShowS #
MonadState ParseState Parser Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods get :: Parser ParseState # put :: ParseState -> Parser () # state :: (ParseState -> (a, ParseState)) -> Parser a #

data ParseError Source #

Parse errors: what you get if parsing fails.

Constructors

ParseError	Errors that arise at a specific position in the file
Fields errSrcFile :: !SrcFile The file in which the error occurred. errPos :: !PositionWithoutFile Where the error occurred. errInput :: String The remaining input. errPrevToken :: String The previous token. errMsg :: String Hopefully an explanation of what happened.
OverlappingTokensError	Parse errors that concern a range in a file.
Fields errRange :: !(Range' SrcFile) The range of the bigger overlapping token
InvalidExtensionError	Parse errors that concern a whole file.
Fields errPath :: !AbsolutePath The file which the error concerns. errValidExts :: [String]
ReadFileError
Fields errPath :: !AbsolutePath The file which the error concerns. errIOError :: IOError

Instances

Instances details

Show ParseError Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseError -> ShowS # show :: ParseError -> String # showList :: [ParseError] -> ShowS #
Pretty ParseError Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods pretty :: ParseError -> Doc Source # prettyPrec :: Int -> ParseError -> Doc Source # prettyList :: [ParseError] -> Doc Source #
HasRange ParseError Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseError -> Range Source #
MonadError ParseError Parser Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods throwError :: ParseError -> Parser a # catchError :: Parser a -> (ParseError -> Parser a) -> Parser a #
MonadError ParseError PM Source #
Instance details Defined in Agda.Syntax.Parser Methods throwError :: ParseError -> PM a # catchError :: PM a -> (ParseError -> PM a) -> PM a #

data ParseWarning Source #

Warnings for parsing.

Constructors

OverlappingTokensWarning	Parse errors that concern a range in a file.
Fields warnRange :: !(Range' SrcFile) The range of the bigger overlapping token

Instances

Instances details

Data ParseWarning Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ParseWarning -> c ParseWarning # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ParseWarning # toConstr :: ParseWarning -> Constr # dataTypeOf :: ParseWarning -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ParseWarning) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ParseWarning) # gmapT :: (forall b. Data b => b -> b) -> ParseWarning -> ParseWarning # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ParseWarning -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ParseWarning -> r # gmapQ :: (forall d. Data d => d -> u) -> ParseWarning -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ParseWarning -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning #
Show ParseWarning Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseWarning -> ShowS # show :: ParseWarning -> String # showList :: [ParseWarning] -> ShowS #
Pretty ParseWarning Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods pretty :: ParseWarning -> Doc Source # prettyPrec :: Int -> ParseWarning -> Doc Source # prettyList :: [ParseWarning] -> Doc Source #
HasRange ParseWarning Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseWarning -> Range Source #

type LexState = Int Source #

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

Instances

Instances details

Show LayoutContext Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> LayoutContext -> ShowS # show :: LayoutContext -> String # showList :: [LayoutContext] -> ShowS #

data ParseFlags Source #

Parser flags.

Constructors

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

Instances

Instances details

Show ParseFlags Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseFlags -> ShowS # show :: ParseFlags -> String # showList :: [ParseFlags] -> ShowS #

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.

parseFromSrc :: ParseFlags -> [LexState] -> Parser a -> SrcFile -> String -> ParseResult a Source #

Parses a string as if it were the contents of the given file Useful for integrating preprocessors.

Manipulating the state

setParsePos :: PositionWithoutFile -> Parser () Source #

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

parseWarningName :: ParseWarning -> WarningName Source #

parseError :: String -> Parser a Source #

Throw a parse error at the current position.

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

parseError' :: Maybe PositionWithoutFile -> String -> Parser a Source #

Use parseErrorAt or parseError as appropriate.

parseErrorRange :: HasRange r => r -> String -> Parser a Source #

Report a parse error at the beginning of the given Range.

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.