Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Syntax.Parser
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 { }
- | InvalidExtensionError {
- errPath :: !AbsolutePath
- errValidExts :: [String]
- | ReadFileError {
- errPath :: !AbsolutePath
- errIOError :: IOError
- = ParseError {
- data ParseWarning = OverlappingTokensWarning {}
- newtype PM a = PM {
- unPM :: ExceptT ParseError (StateT [ParseWarning] IO) a
- runPMIO :: MonadIO m => PM a -> m (Either ParseError a, [ParseWarning])
Types
Parse functions
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
| |
OverlappingTokensError | Parse errors that concern a range in a file. |
InvalidExtensionError | Parse errors that concern a whole file. |
Fields
| |
ReadFileError | |
Fields
|
Instances
Show ParseError Source # | |
Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseError -> ShowS show :: ParseError -> String showList :: [ParseError] -> ShowS | |
Pretty ParseError Source # | |
Defined in Agda.Syntax.Parser.Monad Methods pretty :: ParseError -> Doc Source # prettyPrec :: Int -> ParseError -> Doc Source # prettyList :: [ParseError] -> Doc Source # | |
HasRange ParseError Source # | |
Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseError -> Range Source # | |
MonadError ParseError Parser Source # | |
Defined in Agda.Syntax.Parser.Monad Methods throwError :: ParseError -> Parser a # catchError :: Parser a -> (ParseError -> Parser a) -> Parser a # | |
MonadError ParseError PM Source # | |
Defined in Agda.Syntax.Parser |
data ParseWarning Source #
Warnings for parsing.
Constructors
OverlappingTokensWarning | Parse errors that concern a range in a file. |
Instances
Data ParseWarning Source # | |
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 gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ParseWarning toConstr :: ParseWarning -> Constr dataTypeOf :: ParseWarning -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ParseWarning) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ParseWarning) gmapT :: (forall b. Data b => b -> b) -> ParseWarning -> ParseWarning gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ParseWarning -> r gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ParseWarning -> r gmapQ :: (forall d. Data d => d -> u) -> ParseWarning -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> ParseWarning -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ParseWarning -> m ParseWarning | |
Show ParseWarning Source # | |
Defined in Agda.Syntax.Parser.Monad Methods showsPrec :: Int -> ParseWarning -> ShowS show :: ParseWarning -> String showList :: [ParseWarning] -> ShowS | |
Pretty ParseWarning Source # | |
Defined in Agda.Syntax.Parser.Monad Methods pretty :: ParseWarning -> Doc Source # prettyPrec :: Int -> ParseWarning -> Doc Source # prettyList :: [ParseWarning] -> Doc Source # | |
HasRange ParseWarning Source # | |
Defined in Agda.Syntax.Parser.Monad Methods getRange :: ParseWarning -> Range Source # |
A monad for handling parse results
Constructors
PM | |
Fields
|
Instances
Monad PM Source # | |
Functor PM Source # | |
Applicative PM Source # | |
MonadIO PM Source # | |
Defined in Agda.Syntax.Parser | |
MonadError ParseError PM Source # | |
Defined in Agda.Syntax.Parser |
runPMIO :: MonadIO m => PM a -> m (Either ParseError a, [ParseWarning]) Source #