Idris.Parser.Stack

Parsing

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

Our parser stack with state of type s

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

A constraint for parsing without state

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

Run the Idris parser stack

Parse errors

data ParseError

Instances

Message ParseError

Methods

messageExtent :: ParseError -> FC

messageText :: ParseError -> OutputDoc

messageSource :: ParseError -> Maybe String

prettyError :: ParseError -> String

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

Mark and restore

type Mark = State String

mark :: Parsing m => m Mark

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

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

Tracking the extent of productions

getFC :: Parsing m => m FC

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 ()

Add an extent (widen) our current parsing context.

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

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

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

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

Run a parser and return its value and extent.

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

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