Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Syntax.Parser

Contents

- Types
- Parse functions
- Parsers
- Reading files.
- Parse errors

Synopsis

- data Parser a
- parse :: Parser a -> String -> PM a
- parsePosString :: Parser a -> Position -> String -> PM a
- parseFile :: Show a => Parser a -> AbsolutePath -> String -> PM (a, FileType)
- moduleParser :: Parser Module
- moduleNameParser :: Parser QName
- acceptableFileExts :: [String]
- exprParser :: Parser Expr
- exprWhereParser :: Parser ExprWhere
- holeContentParser :: Parser HoleContent
- tokensParser :: Parser [Token]
- readFilePM :: AbsolutePath -> PM Text
- data ParseError
  - = ParseError {
    - errSrcFile :: !SrcFile
    - errPos :: !PositionWithoutFile
    - errInput :: String
    - errPrevToken :: String
    - errMsg :: String
    }
  - | OverlappingTokensError {
    - errRange :: !(Range' SrcFile)
    }
  - | InvalidExtensionError {
    - errPath :: !AbsolutePath
    - errValidExts :: [String]
    }
  - | ReadFileError {
    - errPath :: !AbsolutePath
    - errIOError :: IOError
    }
- data ParseWarning
  - = OverlappingTokensWarning {
    - warnRange :: !(Range' SrcFile)
    }
  - | UnsupportedAttribute Range !(Maybe String)
  - | MultipleAttributes Range !(Maybe String)
- newtype PM a = PM {
  - unPM :: ExceptT ParseError (StateT [ParseWarning] IO) a
  }
- runPMIO :: MonadIO m => PM a -> m (Either ParseError a, [ParseWarning])

# Types

data Parser a Source #

Wrapped Parser type.

# Parse functions

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

Parse without top-level layout.

parsePosString :: Parser a -> Position -> 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

- 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

Instances details

HasRange ParseError Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseError -> Range Source #
Pretty ParseError Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods pretty :: ParseError -> Doc Source # prettyPrec :: Int -> ParseError -> Doc Source # prettyList :: [ParseError] -> Doc Source #
Show ParseError Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseError -> ShowS Source # show :: ParseError -> String Source # showList :: [ParseError] -> ShowS Source #
MonadError ParseError PM Source # |
Instance details Defined in Agda.Syntax.Parser Methods throwError :: ParseError -> PM a Source # catchError :: PM a -> (ParseError -> PM a) -> PM a Source #
MonadError ParseError Parser Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods throwError :: ParseError -> Parser a Source # catchError :: Parser a -> (ParseError -> Parser a) -> Parser a Source #

data ParseWarning Source #

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

Instances details

HasRange ParseWarning Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseWarning -> Range Source #
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 #
Pretty ParseWarning Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods pretty :: ParseWarning -> Doc Source # prettyPrec :: Int -> ParseWarning -> Doc Source # prettyList :: [ParseWarning] -> Doc Source #
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 Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ParseWarning Source #

toConstr :: ParseWarning -> Constr Source #

dataTypeOf :: ParseWarning -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ParseWarning) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ParseWarning) Source #

gmapT :: (forall b. Data b => b -> b) -> ParseWarning -> ParseWarning Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ParseWarning -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ParseWarning -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> ParseWarning -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ParseWarning -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning Source #

Show ParseWarning Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseWarning -> ShowS Source # show :: ParseWarning -> String Source # showList :: [ParseWarning] -> ShowS Source #
NFData ParseWarning Source # |
Instance details Defined in Agda.Syntax.Parser.Monad Methods rnf :: ParseWarning -> () Source #
MonadState [ParseWarning] PM Source # |
Instance details Defined in Agda.Syntax.Parser Methods get :: PM [ParseWarning] Source # put :: [ParseWarning] -> PM () Source # state :: ([ParseWarning] -> (a, [ParseWarning])) -> PM a Source #

newtype PM a Source #

A monad for handling parse errors and warnings.

Constructors

PM |

Fields

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

#### Instances

Instances details

MonadIO PM Source # |
Instance details Defined in Agda.Syntax.Parser Methods liftIO :: IO a -> PM a Source #
Applicative PM Source # |
Instance details Defined in Agda.Syntax.Parser Methods pure :: a -> PM a Source # (<*>) :: PM (a -> b) -> PM a -> PM b Source # liftA2 :: (a -> b -> c) -> PM a -> PM b -> PM c Source # (*>) :: PM a -> PM b -> PM b Source # (<*) :: PM a -> PM b -> PM a Source #
Functor PM Source # |
Instance details Defined in Agda.Syntax.Parser Methods fmap :: (a -> b) -> PM a -> PM b Source # (<$) :: a -> PM b -> PM a Source #
Monad PM Source # |
Instance details Defined in Agda.Syntax.Parser Methods (>>=) :: PM a -> (a -> PM b) -> PM b Source # (>>) :: PM a -> PM b -> PM b Source # return :: a -> PM a Source #
MonadError ParseError PM Source # |
Instance details Defined in Agda.Syntax.Parser Methods throwError :: ParseError -> PM a Source # catchError :: PM a -> (ParseError -> PM a) -> PM a Source #
MonadState [ParseWarning] PM Source # |
Instance details Defined in Agda.Syntax.Parser Methods get :: PM [ParseWarning] Source # put :: [ParseWarning] -> PM () Source # state :: ([ParseWarning] -> (a, [ParseWarning])) -> PM a Source #

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.