ModuleAgda-2.8.0.2Haskell2010

Agda.Syntax.Parser

4 types
12 values

PackageAgda-2.8.0.2
Exports16
LanguageHaskell2010
LicenceMIT
SourceParser.hs

Types

1 declaration

datadata Parser a

Wrapped Parser type.

Parse functions

3 declarations

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

Parse without top-level layout.

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

valueparseFile

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

7 declarations

valuemoduleParser :: Parser Module

Parses a module.

valuemoduleNameParser :: Parser QName

Parses a module name.

valueagdaFileExtensions :: [String]

Extensions supported by parseFile.

valueexprParser :: Parser Expr

Parses an expression.

valueexprWhereParser :: Parser ExprWhere

Parses an expression followed by a where clause.

valueholeContentParser :: Parser HoleContent

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

valuetokensParser :: Parser [Token]

Gives the parsed token stream (including comments).

Reading files.

1 declaration

valuereadFilePM :: RangeFile -> PM Text

Returns the contents of the given file.

Parse errors

4 declarations

datadata ParseError

Parse errors: what you get if parsing fails.

Constructors

ParseError
Errors that arise at a specific position in the file
- 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.
- errRange :: !Range' SrcFile
  The range of the bigger overlapping token
InvalidExtensionError
Parse errors that concern a whole file.
- errPath :: !RangeFile
  The file which the error concerns.
- errValidExts :: [String]
ReadFileError
- errPath :: !RangeFile
  The file which the error concerns.
- errIOError :: IOError

Instances6Show, NFData, Pretty, HasRange, MonadError

Show ParseErrorDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.Monad
NFData ParseErrorDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.Monad
Pretty ParseErrorDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.Monad
HasRange ParseErrorDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.Monad
MonadError ParseError PMDefined in Agda-2.8.0.2 · Agda.Syntax.Parser
MonadError ParseError ParserDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.Monad

datadata ParseWarning

Warnings for parsing.

Constructors

OverlappingTokensWarning
Parse errors that concern a range in a file.
- warnRange :: !Range' SrcFile
  The range of the bigger overlapping token.
MisplacedAttributes Range String
The String is the error message.
UnknownPolarity Range String
Unknown polarity, ignored.
UnknownAttribute Range String
Unknown attribute, ignored. The Range includes the "@", the String not.
UnsupportedAttribute Range !(Maybe String)
Unsupported attribute.
MultipleAttributes Range !(Maybe String)
Multiple attributes.

Instances6Show, NFData, Pretty, HasRange, EmbPrj, MonadState

Show ParseWarningDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.Monad
NFData ParseWarningDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.Monad
Pretty ParseWarningDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.Monad
Does not include printing of the range.
HasRange ParseWarningDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.Monad
EmbPrj ParseWarningDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
MonadState [ParseWarning] PMDefined in Agda-2.8.0.2 · Agda.Syntax.Parser

newtypenewtype PM a

A monad for handling parse errors and warnings.

Constructors

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

Instances6Monad, Functor, Applicative, MonadIO, MonadError, MonadState

Monad PMDefined in Agda-2.8.0.2 · Agda.Syntax.Parser
Functor PMDefined in Agda-2.8.0.2 · Agda.Syntax.Parser
Applicative PMDefined in Agda-2.8.0.2 · Agda.Syntax.Parser
MonadIO PMDefined in Agda-2.8.0.2 · Agda.Syntax.Parser
MonadError ParseError PMDefined in Agda-2.8.0.2 · Agda.Syntax.Parser
MonadState [ParseWarning] PMDefined in Agda-2.8.0.2 · Agda.Syntax.Parser

valuerunPMIO :: 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.