Agda.Syntax.Parser

Types

data Parser a

Wrapped Parser type.

Parse functions

parse :: Parser a -> String -> PM a

parsePosString :: Parser a -> Position -> String -> PM a

parseFile' :: Show a => Parser a -> AbsolutePath -> PM a

Parsers

moduleParser :: Parser Module

Parses a module.

moduleNameParser :: Parser QName

Parses a module name.

exprParser :: Parser Expr

Parses an expression.

exprWhereParser :: Parser ExprWhere

Parses an expression followed by a where clause.

holeContentParser :: Parser HoleContent

Parses an expression or some other content of an interaction hole.

tokensParser :: Parser [Token]

Gives the parsed token stream (including comments).

Parse errors

data ParseError

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

Show ParseError

Defined in Agda.Syntax.Parser.Monad

Methods

showsPrec :: Int -> ParseError -> ShowS

show :: ParseError -> String

showList :: [ParseError] -> ShowS

Pretty ParseError

Defined in Agda.Syntax.Parser.Monad

Methods

pretty :: ParseError -> Doc

prettyPrec :: Int -> ParseError -> Doc

prettyList :: [ParseError] -> Doc

HasRange ParseError

Defined in Agda.Syntax.Parser.Monad

Methods

getRange :: ParseError -> Range

MonadError ParseError Parser

Defined in Agda.Syntax.Parser.Monad

Methods

throwError :: ParseError -> Parser a

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

MonadError ParseError PM

Defined in Agda.Syntax.Parser

Methods

throwError :: ParseError -> PM a

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

data ParseWarning

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

Data ParseWarning

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

Defined in Agda.Syntax.Parser.Monad

Methods

showsPrec :: Int -> ParseWarning -> ShowS

show :: ParseWarning -> String

showList :: [ParseWarning] -> ShowS

Pretty ParseWarning

Defined in Agda.Syntax.Parser.Monad

Methods

pretty :: ParseWarning -> Doc

prettyPrec :: Int -> ParseWarning -> Doc

prettyList :: [ParseWarning] -> Doc

HasRange ParseWarning

Defined in Agda.Syntax.Parser.Monad

Methods

getRange :: ParseWarning -> Range

newtype PM a

A monad for handling parse results

Constructors

PM

Fields

• unPM :: ExceptT ParseError (StateT [ParseWarning] IO) a

Instances

Monad PM

Defined in Agda.Syntax.Parser

Methods

(>>=) :: PM a -> (a -> PM b) -> PM b

(>>) :: PM a -> PM b -> PM b

return :: a -> PM a

fail :: String -> PM a

Functor PM

Defined in Agda.Syntax.Parser

Methods

fmap :: (a -> b) -> PM a -> PM b

(<$) :: a -> PM b -> PM a

Applicative PM

Defined in Agda.Syntax.Parser

Methods

pure :: a -> PM a

(<*>) :: PM (a -> b) -> PM a -> PM b

liftA2 :: (a -> b -> c) -> PM a -> PM b -> PM c

(*>) :: PM a -> PM b -> PM b

(<*) :: PM a -> PM b -> PM a

MonadIO PM

Defined in Agda.Syntax.Parser

Methods

liftIO :: IO a -> PM a

MonadError ParseError PM

Defined in Agda.Syntax.Parser

Methods

throwError :: ParseError -> PM a

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

runPMIO :: MonadIO m => PM a -> m (Either ParseError a, [ParseWarning])