Agda-2.6.2.1.20220327: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Parser.Monad

Synopsis

The parser monad

data Parser a Source #

The parse monad.

Instances

Instances details
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 #

Functor Parser Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Methods

fmap :: (a -> b) -> Parser a -> Parser b #

(<$) :: a -> Parser b -> Parser a #

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 #

MonadError ParseError Parser Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

MonadState ParseState 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 LexAction 
Instance details

Defined in Agda.Syntax.Parser.Alex

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
HasRange ParseError Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Pretty ParseError Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Show ParseError Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

MonadError ParseError PM 
Instance details

Defined in Agda.Syntax.Parser

Methods

throwError :: ParseError -> PM a

catchError :: PM a -> (ParseError -> PM a) -> PM a

MonadError ParseError Parser Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

data ParseWarning Source #

Warnings for parsing.

Constructors

OverlappingTokensWarning

Parse errors that concern a range in a file.

Fields

UnsupportedAttribute Range !(Maybe String)

Unsupported attribute.

MultipleAttributes Range !(Maybe String)

Multiple attributes.

Instances

Instances details
HasRange ParseWarning Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

EmbPrj ParseWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Pretty ParseWarning Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

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

NFData ParseWarning Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Methods

rnf :: ParseWarning -> () #

MonadState [ParseWarning] PM 
Instance details

Defined in Agda.Syntax.Parser

Methods

get :: PM [ParseWarning]

put :: [ParseWarning] -> PM ()

state :: ([ParseWarning] -> (a, [ParseWarning])) -> PM a

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 LayoutBlock Source #

We need to keep track of the context to do layout. The context specifies the indentation columns of the open layout blocks. See Agda.Syntax.Parser.Layout for more informaton.

Constructors

Layout Keyword LayoutStatus Column

Layout at specified Column, introduced by Keyword.

Instances

Instances details
Show LayoutBlock Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

type LayoutContext = [LayoutBlock] Source #

The stack of layout blocks.

When we encounter a layout keyword, we push a Tentative block with noColumn. This is replaced by aproper column once we reach the next token.

data LayoutStatus Source #

Status of a layout column (see #1145). A layout column is Tentative until we encounter a new line. This allows stacking of layout keywords.

Inside a LayoutContext the sequence of Confirmed columns needs to be strictly increasing. 'Tentative columns between Confirmed columns need to be strictly increasing as well.

Constructors

Tentative

The token defining the layout column was on the same line as the layout keyword and we have not seen a new line yet.

Confirmed

We have seen a new line since the layout keyword and the layout column has not been superseded by a smaller column.

Instances

Instances details
Show LayoutStatus Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Eq LayoutStatus Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

type Column = Int32 Source #

A (layout) column.

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

topBlock :: Parser (Maybe LayoutBlock) Source #

Return the current layout block.

resetLayoutStatus :: Parser () Source #

When we see a layout keyword, by default we expect a Tentative block.

Errors

parseWarning :: ParseWarning -> Parser () Source #

Records a warning.

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.