idris-1.3.0: Functional Programming Language with Dependent Types

MaintainerThe Idris Community.
Safe HaskellNone







type Parser s = StateT s (WriterT FC (Parsec Void String)) Source #

Our parser stack with state of type s

type Parsing m = (MonadParsec Void String m, MonadWriter FC m) Source #

A constraint for parsing without state

runparser :: Parser st res -> st -> String -> String -> Either ParseError res Source #

Run the Idris parser stack

Parse errors

prettyError :: ParseError -> String Source #

A fully formatted parse error, with caret and bar, etc.

Mark and restore

mark :: Parsing m => m Mark Source #

Retrieve the parser state so we can restart from this point later.

restore :: Parsing m => Mark -> m () Source #

Tracking the extent of productions

getFC :: Parsing m => m FC Source #

Get the current parse position.

This is useful when the position is needed in a way unrelated to the heirarchy of parsers. Prefer using withExtent and friends.

addExtent :: MonadWriter FC m => FC -> m () Source #

Add an extent (widen) our current parsing context.

trackExtent :: Parsing m => m a -> m a Source #

Run a parser and track its extent.

Wrap bare Megaparsec parsers with this to make them "visible" in error messages. Do not wrap whitespace or comment parsers. If you find an extent is taking trailing whitespace, it's likely there's a double-wrapped parser (usually via Idris.Parser.Helpers.token).

extent :: MonadWriter FC m => m a -> m FC Source #

Run a parser, discard its value, and return its extent.

withExtent :: MonadWriter FC m => m a -> m (a, FC) Source #

Run a parser and return its value and extent.

appExtent :: MonadWriter FC m => m (FC -> a) -> m a Source #

Run a parser and inject the extent after via function application.