Idris2Doc : Data.String.Parser


(<?>) : Functorm => ParseTma -> String -> ParseTma
Combinator that replaces the error message on failure.
This allows combinators to output relevant errors
Totality: total
Fixity Declaration: infixl operator, level 0
ParseT : (Type -> Type) -> Type -> Type
Totality: total
Parser : Type -> Type
Totality: total
Result : Type -> Type
Result of applying a parser
Totality: total
Fail : Int -> String -> Resulta
OK : a -> State -> Resulta
State : Type
The input state, pos is position in the string and maxPos is the length of the input string.
Totality: total
alphaNum : Applicativem => ParseTm Char
Parses a letter or digit (a character between \'0\' and \'9\').
Returns the parsed character.
Totality: total
char : Applicativem => Char -> ParseTm Char
Succeeds if the next char is `c`
Totality: total
commaSep : Monadm => ParseTma -> ParseTm (Lista)
Parses /zero/ or more occurrences of `p` separated by `comma`.
commaSep1 : Monadm => ParseTma -> ParseTm (List1a)
Parses /one/ or more occurrences of `p` separated by `comma`.
digit : Monadm => ParseTm (Fin 10)
Matches a single digit
Totality: total
eos : Applicativem => ParseTmUnit
Succeeds if the end of the string is reached.
Totality: total
fail : Applicativem => String -> ParseTma
Fail with some error message
Totality: total
hchainl : Monadm => ParseTminit -> ParseTm (init -> arg -> init) -> ParseTmarg -> ParseTminit
Parse left-nested lists of the form `((init op arg) op arg) op arg`
hchainr : Monadm => ParseTmarg -> ParseTm (arg -> end -> end) -> ParseTmend -> ParseTmend
Parse right-nested lists of the form `arg op (arg op (arg op end))`
integer : Monadm => ParseTm Integer
Matches an integer, eg. "12", "-4"
letter : Applicativem => ParseTm Char
Parses a letter (an upper case or lower case character). Returns the
parsed character.
Totality: total
lexeme : Monadm => ParseTma -> ParseTma
Discards whitespace after a matching parser
many : Monadm => ParseTma -> ParseTm (Lista)
Always succeeds, will accumulate the results of `p` in a list until it fails.
natural : Monadm => ParseTmNat
Matches a natural number
ntimes : Monadm => (n : Nat) -> ParseTma -> ParseTm (Vectna)
Run the specified parser precisely `n` times, returning a vector
of successes.
Totality: total
option : Functorm => a -> ParseTma -> ParseTma
Runs the result of the parser `p` or returns `def` if it fails.
Totality: total
optionMap : Functorm => b -> (a -> b) -> ParseTma -> ParseTmb
Maps the result of the parser `p` or returns `def` if it fails.
Totality: total
optional : Functorm => ParseTma -> ParseTm (Maybea)
Returns a Maybe that contains the result of `p` if it succeeds or `Nothing` if it fails.
Totality: total
parens : Monadm => ParseTma -> ParseTma
Discards brackets around a matching parser
Totality: total
parse : Parsera -> 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 : Functorm => ParseTma -> 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 : Functorm => ParseTma -> ParseTmUnit
Succeeds if and only if the argument parser fails.

In Parsec, this combinator is called `notFollowedBy`.
Totality: total
satisfy : Applicativem => (Char -> Bool) -> ParseTm Char
Succeeds if the next char satisfies the predicate `f`
Totality: total
sepBy : Monadm => ParseTma -> ParseTmb -> ParseTm (Lista)
Parse zero or more `p`s, separated by `s`s, returning a list of

@ p the parser for items
@ s the parser for separators
sepBy1 : Monadm => ParseTma -> ParseTmb -> ParseTm (List1a)
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 : Functorm => ParseTma -> ParseTmUnit
Discards the result of a parser
Totality: total
some : Monadm => ParseTma -> ParseTm (Lista)
Succeeds if `p` succeeds, will continue to match `p` until it fails
and accumulate the results in a list
space : Applicativem => ParseTm Char
Parses a space character
Totality: total
spaces : Monadm => ParseTmUnit
Parses zero or more space characters
spaces1 : Monadm => ParseTmUnit
Parses one or more space characters
string : Applicativem => String -> ParseTm String
Succeeds if the string `str` follows.
Totality: total
succeeds : Functorm => ParseTma -> ParseTmBool
Returns a Bool indicating whether `p` succeeded
Totality: total
takeWhile : Monadm => (Char -> Bool) -> ParseTm String
Always succeeds, applies the predicate `f` on chars until it fails and creates a string
from the results.
takeWhile1 : Monadm => (Char -> Bool) -> ParseTm String
Similar to `takeWhile` but fails if the resulting string is empty.
token : Monadm => String -> ParseTmUnit
Matches a specific string, then skips following whitespace