Data.String.Parser

A simple parser combinator library for String. Inspired by attoparsec zepto.

Reexports

Definitions

record State : Type

  The input state, pos is position in the string and maxPos is the length of the input string.

Totality: total
Visibility: public export
Constructor: 

S : String -> Int -> Int -> State

Projections:

.input : State -> String

.maxPos : State -> Int

.pos : State -> Int

Hint: 

Show State

.input : State -> String

Totality: total
Visibility: public export

input : State -> String

Totality: total
Visibility: public export

.pos : State -> Int

Totality: total
Visibility: public export

pos : State -> Int

Totality: total
Visibility: public export

.maxPos : State -> Int

Totality: total
Visibility: public export

maxPos : State -> Int

Totality: total
Visibility: public export

data Result : Type -> Type

  Result of applying a parser

Totality: total
Visibility: public export
Constructors:

Fail : Int -> String -> Result a

OK : a -> State -> Result a

Hint: 

Functor Result

record ParseT : (Type -> Type) -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

P : (State -> m (Result a)) -> ParseT m a

Projection: 

.runParser : ParseT m a -> State -> m (Result a)

Hints:

Monad m => Alternative (ParseT m)

Monad m => Applicative (ParseT m)

Functor m => Functor (ParseT m)

Monad m => Monad (ParseT m)

MonadTrans ParseT

.runParser : ParseT m a -> State -> m (Result a)

Totality: total
Visibility: public export

runParser : ParseT m a -> State -> m (Result a)

Totality: total
Visibility: public export

Parser : Type -> Type

Totality: total
Visibility: public export

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
Visibility: export

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
Visibility: export

(<?>) : 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
Visibility: export
Fixity Declaration: infixl operator, level 0

skip : Functor m => ParseT m a -> ParseT m ()

  Discards the result of a parser

Totality: total
Visibility: export

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
Visibility: export

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
Visibility: export

succeeds : Functor m => ParseT m a -> ParseT m Bool

  Returns a Bool indicating whether `p` succeeded

Totality: total
Visibility: export

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
Visibility: export

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
Visibility: export

fail : Applicative m => String -> ParseT m a

  Fail with some error message

Totality: total
Visibility: export

satisfy : Applicative m => (Char -> Bool) -> ParseT m Char

  Succeeds if the next char satisfies the predicate `f`

Totality: total
Visibility: export

string : Applicative m => String -> ParseT m String

  Succeeds if the string `str` follows.

Totality: total
Visibility: export

eos : Applicative m => ParseT m ()

  Succeeds if the end of the string is reached.

Totality: total
Visibility: export

char : Applicative m => Char -> ParseT m Char

  Succeeds if the next char is `c`

Totality: total
Visibility: export

space : Applicative m => ParseT m Char

  Parses a space character

Totality: total
Visibility: export

alphaNum : Applicative m => ParseT m Char

  Parses a letter or digit (a character between \'0\' and \'9\').
  Returns the parsed character.

Totality: total
Visibility: export

letter : Applicative m => ParseT m Char

  Parses a letter (an upper case or lower case character). Returns the
  parsed character.

Totality: total
Visibility: export

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

Visibility: export

many : Monad m => ParseT m a -> ParseT m (List a)

  Always succeeds, will accumulate the results of `p` in a list until it fails.

Visibility: export

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`

Visibility: export

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

Visibility: export

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.

Visibility: export

takeWhile1 : Monad m => (Char -> Bool) -> ParseT m String

  Similar to `takeWhile` but fails if the resulting string is empty.

Visibility: export

takeUntil : Monad m => String -> ParseT m String

  Takes from the input until the `stop` string is found.
  Fails if the `stop` string cannot be found.

Visibility: export

spaces : Monad m => ParseT m ()

  Parses zero or more space characters

Visibility: export

spaces1 : Monad m => ParseT m ()

  Parses one or more space characters

Visibility: export

between : Monad m => ParseT m o -> ParseT m c -> ParseT m p -> ParseT m p

  Run the parser p between the opening parser `o` and the closing parser `c`,
  returning the result of p.

Totality: total
Visibility: export

parens : Monad m => ParseT m a -> ParseT m a

  Discards brackets around a matching parser

Totality: total
Visibility: export

lexeme : Monad m => ParseT m a -> ParseT m a

  Discards whitespace after a matching parser

Visibility: export

token : Monad m => String -> ParseT m ()

  Matches a specific string, then skips following whitespace

Visibility: export

digit : Monad m => ParseT m (Fin 10)

  Matches a single digit

Totality: total
Visibility: export

natural : Monad m => ParseT m Nat

  Matches a natural number

Visibility: export

integer : Monad m => ParseT m Integer

  Matches an integer, eg. "12", "-4"

Visibility: export

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

Visibility: export

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

Visibility: export

commaSep1 : Monad m => ParseT m a -> ParseT m (List1 a)

  Parses /one/ or more occurrences of `p` separated by `comma`.

Visibility: export

commaSep : Monad m => ParseT m a -> ParseT m (List a)

  Parses /zero/ or more occurrences of `p` separated by `comma`.

Visibility: export

alternating : Monad m => ParseT m a -> ParseT m b -> ParseT m (Odd a b)

  Parses alternating occurrences of `a`s and `b`s.
  Can be thought of as parsing:
  - a list of `b`s, separated, and surrounded, by `a`s
  - a non-empty list of `a`s, separated by `b`s
  where we care about the separators

Visibility: export

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
Visibility: export