ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Parser

4 types
12 values

PackageAgda-2.7.0.1
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.

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

Instances5Show, Pretty, HasRange, MonadError

Show ParseErrorDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.Monad
Pretty ParseErrorDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.Monad
HasRange ParseErrorDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.Monad
MonadError ParseError PMDefined in Agda-2.7.0.1 · Agda.Syntax.Parser
MonadError ParseError ParserDefined in Agda-2.7.0.1 · 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
UnsupportedAttribute Range !(Maybe String)
Unsupported attribute.
MultipleAttributes Range !(Maybe String)
Multiple attributes.

Instances6Show, NFData, Pretty, HasRange, EmbPrj, MonadState

Show ParseWarningDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.Monad
NFData ParseWarningDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.Monad
Pretty ParseWarningDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.Monad
HasRange ParseWarningDefined in Agda-2.7.0.1 · Agda.Syntax.Parser.Monad
EmbPrj ParseWarningDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
MonadState [ParseWarning] PMDefined in Agda-2.7.0.1 · 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.7.0.1 · Agda.Syntax.Parser
Functor PMDefined in Agda-2.7.0.1 · Agda.Syntax.Parser
Applicative PMDefined in Agda-2.7.0.1 · Agda.Syntax.Parser
MonadIO PMDefined in Agda-2.7.0.1 · Agda.Syntax.Parser
MonadError ParseError PMDefined in Agda-2.7.0.1 · Agda.Syntax.Parser
MonadState [ParseWarning] PMDefined in Agda-2.7.0.1 · 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.