Agda-2.6.1.3: 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 Source #

parseFile Source #

Arguments

:: Show a 
=> Parser a 
-> AbsolutePath

The path to the file.

-> String

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

-> PM (a, 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 :: AbsolutePath -> 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
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

newtype PM a Source #

A monad for handling parse results

Constructors

PM 

Instances

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

Functor PM Source # 
Instance details

Defined in Agda.Syntax.Parser

Methods

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

(<$) :: a -> PM b -> 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 #

MonadIO PM Source # 
Instance details

Defined in Agda.Syntax.Parser

Methods

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