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

Agda.Syntax.Parser

Synopsis

Types

data Parser a Source #

Wrapped Parser type.

Parse functions

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

Parse without top-level layout.

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

parseFile Source #

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

Parses a module.

moduleNameParser :: Parser QName Source #

Parses a module name.

acceptableFileExts :: [String] Source #

Extensions supported by parseFile.

exprParser :: Parser Expr Source #

Parses an expression.

exprWhereParser :: Parser ExprWhere Source #

Parses an expression followed by a where clause.

holeContentParser :: Parser HoleContent Source #

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

tokensParser :: Parser [Token] Source #

Gives the parsed token stream (including comments).

Reading files.

readFilePM :: RangeFile -> PM Text Source #

Returns the contents of the given file.

Parse errors

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

Defined in Agda.Syntax.Parser.Monad

HasRange ParseError Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Show ParseError Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Methods

showsPrec :: Int -> ParseError -> ShowS

show :: ParseError -> String

showList :: [ParseError] -> ShowS

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
Pretty ParseWarning Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

HasRange ParseWarning Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

EmbPrj ParseWarning Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: ParseWarning -> S Int32 Source #

icod_ :: ParseWarning -> S Int32 Source #

value :: Int32 -> R ParseWarning Source #

NFData ParseWarning Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Methods

rnf :: ParseWarning -> ()

Show ParseWarning Source # 
Instance details

Defined in Agda.Syntax.Parser.Monad

Methods

showsPrec :: Int -> ParseWarning -> ShowS

show :: ParseWarning -> String

showList :: [ParseWarning] -> ShowS

MonadState [ParseWarning] PM 
Instance details

Defined in Agda.Syntax.Parser

Methods

get :: PM [ParseWarning]

put :: [ParseWarning] -> PM ()

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

newtype PM a Source #

A monad for handling parse errors and warnings.

Constructors

PM 

Fields

Instances

Instances details
MonadIO PM Source # 
Instance details

Defined in Agda.Syntax.Parser

Methods

liftIO :: IO a -> PM a

Applicative PM Source # 
Instance details

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

Defined in Agda.Syntax.Parser

Methods

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

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

Monad PM Source # 
Instance details

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

Defined in Agda.Syntax.Parser

Methods

throwError :: ParseError -> PM a

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

MonadState [ParseWarning] PM Source # 
Instance details

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]) Source #

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