Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Parser.Monad

Synopsis

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

MonadError ParseError Parser Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

data ParseResult a Source #

The result of parsing something.

Instances

Instances details
Show a => Show (ParseResult a) Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

data ParseState Source #

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

Constructors

PState 

Fields

Instances

Instances details
Show ParseState Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

MonadState ParseState Parser Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

data ParseError Source #

Parse errors: what you get if parsing fails.

Constructors

ParseError

Errors that arise at a specific position in the file

Fields

OverlappingTokensError

Parse errors that concern a range in a file.

Fields

InvalidExtensionError

Parse errors that concern a whole file.

Fields

ReadFileError 

Fields

Instances

Instances details
Show ParseError Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Pretty ParseError Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

HasRange ParseError Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

MonadError ParseError Parser Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

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

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

Pretty ParseWarning Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

HasRange ParseWarning Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

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

data ParseFlags Source #

Parser flags.

Constructors

ParseFlags 

Fields

Instances

Instances details
Show ParseFlags Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

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

getParseInterval :: Parser Interval Source #

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

Layout

topContext :: Parser LayoutContext Source #

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.

Errors

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.

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.