Wrapped Parser type.
ModuleAgda-2.8.0.2Haskell2010
Agda.Syntax.Parser
Synopsis
- data Parser
- value parse
- value parsePosString
- value parseFile
- value moduleParser
- value moduleNameParser
- value agdaFileExtensions
- value exprParser
- value exprWhereParser
- value holeContentParser
- value tokensParser
- value readFilePM
- data ParseError
- data ParseWarning
- newtype PM
- value runPMIO
- PackageAgda-2.8.0.2
- Exports16
- LanguageHaskell2010
- LicenceMIT
- SourceParser.hs
Types
Parse functions
Parse without top-level layout.
Parsers
Parses a module.
Parses a module name.
Extensions supported by parseFile.
Parses an expression.
Parses an expression followed by a where clause.
Parses an expression or some other content of an interaction hole.
Gives the parsed token stream (including comments).
Reading files.
Returns the contents of the given file.
Parse errors
Parse errors: what you get if parsing fails.
Constructors
ParseErrorErrors that arise at a specific position in the file
errSrcFile :: !SrcFileThe file in which the error occurred.
errPos :: !PositionWithoutFileWhere the error occurred.
errInput :: StringThe remaining input.
errPrevToken :: StringThe previous token.
errMsg :: StringHopefully an explanation of what happened.
OverlappingTokensErrorParse errors that concern a range in a file.
InvalidExtensionErrorParse errors that concern a whole file.
errPath :: !RangeFileThe file which the error concerns.
errValidExts :: [String]
ReadFileErrorerrPath :: !RangeFileThe file which the error concerns.
errIOError :: IOError
Instances6Show, NFData, Pretty, HasRange, MonadError
Show ParseErrorDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.MonadNFData ParseErrorDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.MonadPretty ParseErrorDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.MonadHasRange ParseErrorDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.MonadMonadError ParseError PMDefined in Agda-2.8.0.2 · Agda.Syntax.ParserMonadError ParseError ParserDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.Monad
Warnings for parsing.
Constructors
OverlappingTokensWarningParse errors that concern a range in a file.
MisplacedAttributes Range StringThe String is the error message.
UnknownPolarity Range StringUnknown polarity, ignored.
UnknownAttribute Range StringUnsupportedAttribute 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.MonadNFData ParseWarningDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.MonadPretty ParseWarningDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.MonadDoes not include printing of the range.
HasRange ParseWarningDefined in Agda-2.8.0.2 · Agda.Syntax.Parser.MonadEmbPrj ParseWarningDefined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Errors · orphanMonadState [ParseWarning] PMDefined in Agda-2.8.0.2 · Agda.Syntax.Parser
A monad for handling parse errors and warnings.
Constructors
PMunPM :: ExceptT ParseError (StateT [ParseWarning] IO) a
Instances6Monad, Functor, Applicative, MonadIO, MonadError, MonadState
Monad PMDefined in Agda-2.8.0.2 · Agda.Syntax.ParserFunctor PMDefined in Agda-2.8.0.2 · Agda.Syntax.ParserApplicative PMDefined in Agda-2.8.0.2 · Agda.Syntax.ParserMonadIO PMDefined in Agda-2.8.0.2 · Agda.Syntax.ParserMonadError ParseError PMDefined in Agda-2.8.0.2 · Agda.Syntax.ParserMonadState [ParseWarning] PMDefined in Agda-2.8.0.2 · Agda.Syntax.Parser
Run a PM computation, returning a list of warnings in first-to-last order and either a parse error or the parsed thing.