Agda.Syntax.Parser

Types

data Parser a

Wrapped Parser type.

Parse functions

parse :: Parser a -> String -> PM (a, Attributes)

Parse without top-level layout.

parsePosString :: Parser a -> Position -> String -> PM (a, Attributes)

parseFile

Arguments

:: Show a

=> Parser a

-> RangeFile

The file.

-> String

The file contents. Note that the file is not read from disk.

-> PM ((a, Attributes), FileType)

Parsers

moduleParser :: Parser Module

Parses a module.

moduleNameParser :: Parser QName

Parses a module name.

acceptableFileExts :: [String]

Extensions supported by parseFile.

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).

Reading files.

readFilePM :: RangeFile -> PM Text

Returns the contents of the given file.

Parse errors

data ParseError

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 :: !RangeFile

  The file which the error concerns.

• errValidExts :: [String]

ReadFileError

Fields

• errPath :: !RangeFile

  The file which the error concerns.

• errIOError :: IOError

Instances

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

Show ParseError

Defined in Agda.Syntax.Parser.Monad

Methods

showsPrec :: Int -> ParseError -> ShowS

show :: ParseError -> String

showList :: [ParseError] -> ShowS

MonadError ParseError PM

Defined in Agda.Syntax.Parser

Methods

throwError :: ParseError -> PM a

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

MonadError ParseError Parser

Defined in Agda.Syntax.Parser.Monad

Methods

throwError :: ParseError -> Parser a

catchError :: Parser a -> (ParseError -> Parser a) -> Parser 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

UnsupportedAttribute Range !(Maybe String)

Unsupported attribute.

MultipleAttributes Range !(Maybe String)

Multiple attributes.

Instances

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

EmbPrj ParseWarning

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ParseWarning -> S Int32

icod_ :: ParseWarning -> S Int32

value :: Int32 -> R ParseWarning

Show ParseWarning

Defined in Agda.Syntax.Parser.Monad

Methods

showsPrec :: Int -> ParseWarning -> ShowS

show :: ParseWarning -> String

showList :: [ParseWarning] -> ShowS

NFData ParseWarning

Defined in Agda.Syntax.Parser.Monad

Methods

rnf :: ParseWarning -> ()

MonadState [ParseWarning] PM

Defined in Agda.Syntax.Parser

Methods

get :: PM [ParseWarning]

put :: [ParseWarning] -> PM ()

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

newtype PM a

A monad for handling parse errors and warnings.

Constructors

PM

Fields

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

Instances

MonadIO PM

Defined in Agda.Syntax.Parser

Methods

liftIO :: IO a -> 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

Functor PM

Defined in Agda.Syntax.Parser

Methods

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

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

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

MonadError ParseError PM

Defined in Agda.Syntax.Parser

Methods

throwError :: ParseError -> PM a

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

MonadState [ParseWarning] PM

Defined in Agda.Syntax.Parser

Methods

get :: PM [ParseWarning]

put :: [ParseWarning] -> PM ()

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

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

Run a PM computation, returning a list of warnings in first-to-last order and either a parse error or the parsed thing.