TyRE.Text.Parser

This is a slightly modified copy of the same module from `contrib` package.

Reexports

Definitions

match : {auto {conArg:977} : (Eq k, TokenKind k)} -> (kind : k) -> Grammar (Token k) True (TokType kind)

  Parse a terminal based on a kind of token.

Visibility: public export

option : a -> Grammar tok c a -> Grammar tok False a

  Optionally parse a thing, with a default value if the grammar doesn't
  match. May match the empty input.

Visibility: public export

optional : Grammar tok c a -> Grammar tok False (Maybe a)

  Optionally parse a thing.
  To provide a default value, use `option` instead.

Visibility: public export

choose : Grammar tok c1 a -> Grammar tok c2 b -> Grammar tok (c1 && Delay c2) (Either a b)

  Try to parse one thing or the other, producing a value that indicates
  which option succeeded. If both would succeed, the left option
  takes priority.

Visibility: public export

choiceMap : (a -> Grammar tok c b) -> Foldable t => t a -> Grammar tok c b

  Produce a grammar by applying a function to each element of a container,
  then try each resulting grammar until the first one succeeds. Fails if the
  container is empty.

Visibility: public export

choice : Foldable t => t (Grammar tok c a) -> Grammar tok c a

  Try each grammar in a container until the first one succeeds.
  Fails if the container is empty.

Visibility: public export

some : Grammar tok True a -> Grammar tok True (List1 a)

  Parse one or more things

Visibility: public export

many : Grammar tok True a -> Grammar tok False (List a)

  Parse zero or more things (may match the empty input)

Visibility: public export

some' : Grammar tok True a -> Grammar tok True (xs : List a ** NonEmpty xs)

  Parse one or more instances of `p`, returning the parsed items and proof
  that the resulting list is non-empty.

Visibility: public export

count1 : Quantity -> Grammar tok True a -> Grammar tok True (List a)

Visibility: public export

count : (q : Quantity) -> Grammar tok True a -> Grammar tok (isSucc (min q)) (List a)

  Parse `p`, repeated as specified by `q`, returning the list of values.

Visibility: public export

countExactly : (n : Nat) -> Grammar tok True a -> Grammar tok (isSucc n) (Vect n a)

  Parse `p` `n` times, returning the vector of values.

Visibility: public export

someTill : Grammar tok c e -> Grammar tok True a -> Grammar tok True (List1 a)

  Parse one or more instances of `p` until `end` succeeds, returning the
  list of values from `p`. Guaranteed to consume input.

Visibility: public export

manyTill : Grammar tok c e -> Grammar tok True a -> Grammar tok c (List a)

  Parse zero or more instances of `p` until `end` succeeds, returning the
  list of values from `p`. Guaranteed to consume input if `end` consumes.

Visibility: public export

afterSome : Grammar tok True s -> Grammar tok c a -> Grammar tok True a

  Parse one or more instance of `skip` until `p` is encountered,
  returning its value.

Visibility: public export

afterMany : Grammar tok True s -> Grammar tok c a -> Grammar tok c a

  Parse zero or more instance of `skip` until `p` is encountered,
  returning its value.

Visibility: public export

sepBy1 : Grammar tok True s -> Grammar tok c a -> Grammar tok c (List1 a)

  Parse one or more things, each separated by another thing.

Visibility: public export

sepBy : Grammar tok True s -> Grammar tok c a -> Grammar tok False (List a)

  Parse zero or more things, each separated by another thing. May
  match the empty input.

Visibility: public export

sepEndBy1 : Grammar tok True s -> Grammar tok c a -> Grammar tok c (List1 a)

  Parse one or more instances of `p` separated by and optionally terminated by
  `sep`.

Visibility: public export

sepEndBy : Grammar tok True s -> Grammar tok c a -> Grammar tok False (List a)

  Parse zero or more instances of `p`, separated by and optionally terminated
  by `sep`. Will not match a separator by itself.

Visibility: public export

endBy1 : Grammar tok True s -> Grammar tok c a -> Grammar tok True (List1 a)

  Parse one or more instances of `p`, separated and terminated by `sep`.

Visibility: public export

endBy : Grammar tok True s -> Grammar tok c a -> Grammar tok False (List a)

Visibility: public export

between : Grammar tok True l -> Inf (Grammar tok True r) -> Inf (Grammar tok c a) -> Grammar tok True a

  Parse an instance of `p` that is between `left` and `right`.

Visibility: public export