- (<?>) : Functor m => ParseT m a -> String -> ParseT m a
Combinator that replaces the error message on failure.
This allows combinators to output relevant errors
Totality: total
Fixity Declaration: infixl operator, level 0- record ParseT : (Type -> Type) -> Type -> Type
- Totality: total
Constructor: - P : (State -> m (Result a)) -> ParseT m a
Projection: - .runParser : ParseT m a -> State -> m (Result a)
- Parser : Type -> Type
- Totality: total
- data Result : Type -> Type
Result of applying a parser
Totality: total
Constructors:
- Fail : Int -> String -> Result a
- OK : a -> State -> Result a
- record State : Type
The input state, pos is position in the string and maxPos is the length of the input string.
Totality: total
Constructor: - S : String -> Int -> Int -> State
Projections:
- .input : State -> String
- .maxPos : State -> Int
- .pos : State -> Int
- alphaNum : Applicative m => ParseT m Char
Parses a letter or digit (a character between \'0\' and \'9\').
Returns the parsed character.
Totality: total- char : Applicative m => Char -> ParseT m Char
Succeeds if the next char is `c`
Totality: total- commaSep : Monad m => ParseT m a -> ParseT m (List a)
Parses /zero/ or more occurrences of `p` separated by `comma`.
- commaSep1 : Monad m => ParseT m a -> ParseT m (List1 a)
Parses /one/ or more occurrences of `p` separated by `comma`.
- digit : Monad m => ParseT m (Fin 10)
Matches a single digit
Totality: total- eos : Applicative m => ParseT m ()
Succeeds if the end of the string is reached.
Totality: total- fail : Applicative m => String -> ParseT m a
Fail with some error message
Totality: total- hchainl : Monad m => ParseT m init -> ParseT m (init -> arg -> init) -> ParseT m arg -> ParseT m init
Parse left-nested lists of the form `((init op arg) op arg) op arg`
- hchainr : Monad m => ParseT m arg -> ParseT m (arg -> end -> end) -> ParseT m end -> ParseT m end
Parse right-nested lists of the form `arg op (arg op (arg op end))`
- integer : Monad m => ParseT m Integer
Matches an integer, eg. "12", "-4"
- letter : Applicative m => ParseT m Char
Parses a letter (an upper case or lower case character). Returns the
parsed character.
Totality: total- lexeme : Monad m => ParseT m a -> ParseT m a
Discards whitespace after a matching parser
- many : Monad m => ParseT m a -> ParseT m (List a)
Always succeeds, will accumulate the results of `p` in a list until it fails.
- natural : Monad m => ParseT m Nat
Matches a natural number
- ntimes : Monad m => (n : Nat) -> ParseT m a -> ParseT m (Vect n a)
Run the specified parser precisely `n` times, returning a vector
of successes.
Totality: total- option : Functor m => a -> ParseT m a -> ParseT m a
Runs the result of the parser `p` or returns `def` if it fails.
Totality: total- optionMap : Functor m => b -> (a -> b) -> ParseT m a -> ParseT m b
Maps the result of the parser `p` or returns `def` if it fails.
Totality: total- optional : Functor m => ParseT m a -> ParseT m (Maybe a)
Returns a Maybe that contains the result of `p` if it succeeds or `Nothing` if it fails.
Totality: total- parens : Monad m => ParseT m a -> ParseT m a
Discards brackets around a matching parser
Totality: total- parse : Parser a -> String -> Either String (a, Int)
Run a parser in a pure function
Returns a tuple of the result and final position on success.
Returns an error message on failure.
Totality: total- parseT : Functor m => ParseT m a -> String -> m (Either String (a, Int))
Run a parser in a monad
Returns a tuple of the result and final position on success.
Returns an error message on failure.
Totality: total- requireFailure : Functor m => ParseT m a -> ParseT m ()
Succeeds if and only if the argument parser fails.
In Parsec, this combinator is called `notFollowedBy`.
Totality: total- satisfy : Applicative m => (Char -> Bool) -> ParseT m Char
Succeeds if the next char satisfies the predicate `f`
Totality: total- sepBy : Monad m => ParseT m a -> ParseT m b -> ParseT m (List a)
Parse zero or more `p`s, separated by `s`s, returning a list of
successes.
@ p the parser for items
@ s the parser for separators
- sepBy1 : Monad m => ParseT m a -> ParseT m b -> ParseT m (List1 a)
Parse repeated instances of at least one `p`, separated by `s`,
returning a list of successes.
@ p the parser for items
@ s the parser for separators
- skip : Functor m => ParseT m a -> ParseT m ()
Discards the result of a parser
Totality: total- some : Monad m => ParseT m a -> ParseT m (List a)
Succeeds if `p` succeeds, will continue to match `p` until it fails
and accumulate the results in a list
- space : Applicative m => ParseT m Char
Parses a space character
Totality: total- spaces : Monad m => ParseT m ()
Parses zero or more space characters
- spaces1 : Monad m => ParseT m ()
Parses one or more space characters
- string : Applicative m => String -> ParseT m String
Succeeds if the string `str` follows.
Totality: total- succeeds : Functor m => ParseT m a -> ParseT m Bool
Returns a Bool indicating whether `p` succeeded
Totality: total- takeWhile : Monad m => (Char -> Bool) -> ParseT m String
Always succeeds, applies the predicate `f` on chars until it fails and creates a string
from the results.
- takeWhile1 : Monad m => (Char -> Bool) -> ParseT m String
Similar to `takeWhile` but fails if the resulting string is empty.
- token : Monad m => String -> ParseT m ()
Matches a specific string, then skips following whitespace