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, CohesionAttributes)
parsePosString :: Parser a -> Position -> String -> PM (a, CohesionAttributes)
parseFile :: Show a => Parser a -> RangeFile -> String -> PM ((a, CohesionAttributes), FileType)
moduleParser :: Parser Module
moduleNameParser :: Parser QName
acceptableFileExts :: [String]
exprParser :: Parser Expr
exprWhereParser :: Parser ExprWhere
holeContentParser :: Parser HoleContent
tokensParser :: Parser [Token]
readFilePM :: RangeFile -> PM Text
data ParseError
- = ParseError {
  - errSrcFile :: !SrcFile
  - errPos :: !PositionWithoutFile
  - errInput :: String
  - errPrevToken :: String
  - errMsg :: String
  }
- | OverlappingTokensError {
  - errRange :: !(Range' SrcFile)
  }
- | InvalidExtensionError {
  - errPath :: !RangeFile
  - errValidExts :: [String]
  }
- | ReadFileError {
  - errPath :: !RangeFile
  - 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, CohesionAttributes) Source #

Parse without top-level layout.

parsePosString :: Parser a -> Position -> String -> PM (a, CohesionAttributes) 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, CohesionAttributes), 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 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

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 # show :: ParseError -> String # showList :: [ParseError] -> ShowS #
MonadError ParseError PM Source #
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 Methods throwError :: ParseError -> Parser a # catchError :: Parser a -> (ParseError -> Parser a) -> Parser a #

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 #
Show ParseWarning Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseWarning -> ShowS # show :: ParseWarning -> String # showList :: [ParseWarning] -> ShowS #
NFData ParseWarning Source #
Instance details Defined in Agda.Syntax.Parser.Monad Methods rnf :: ParseWarning -> () #
MonadState [ParseWarning] PM Source #
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 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 #
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.