Idris2Doc : Data.String.Parser

Data.String.Parser

A simple parser combinator library for String. Inspired by attoparsec zepto.
(<?>) : 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
recordParseT : (Type -> Type) -> Type -> Type
Totality: total
Constructor: 
P : (State -> m (Resulta)) -> ParseTma

Projection: 
.runParser : ParseTma -> State -> m (Resulta)
Parser : Type -> Type
Totality: total
dataResult : Type -> Type
  Result of applying a parser

Totality: total
Constructors:
Fail : Int -> String -> Resulta
OK : a -> State -> Resulta
recordState : 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 : Applicativem => ParseTmChar
  Parses a letter or digit (a character between \'0\' and \'9\').
Returns the parsed character.

Totality: total
char : Applicativem => Char -> ParseTmChar
  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 (Fin10)
  Matches a single digit

Totality: total
eos : Applicativem => ParseTm ()
  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 => ParseTmInteger
  Matches an integer, eg. "12", "-4"

letter : Applicativem => ParseTmChar
  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 -> EitherString (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 (EitherString (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 -> ParseTm ()
  Succeeds if and only if the argument parser fails.

In Parsec, this combinator is called `notFollowedBy`.

Totality: total
satisfy : Applicativem => (Char -> Bool) -> ParseTmChar
  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
successes.

@ 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 -> ParseTm ()
  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 => ParseTmChar
  Parses a space character

Totality: total
spaces : Monadm => ParseTm ()
  Parses zero or more space characters

spaces1 : Monadm => ParseTm ()
  Parses one or more space characters

string : Applicativem => String -> ParseTmString
  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) -> ParseTmString
  Always succeeds, applies the predicate `f` on chars until it fails and creates a string
from the results.

takeWhile1 : Monadm => (Char -> Bool) -> ParseTmString
  Similar to `takeWhile` but fails if the resulting string is empty.

token : Monadm => String -> ParseTm ()
  Matches a specific string, then skips following whitespace