Text.Parser

Reexports

import public Data.Nat
import public Data.List1
import public Text.Parser.Core
import public Text.Quantity
import public Text.Token

Definitions

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

  Parse a terminal based on a kind of token.

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

choose : Grammar state tok c1 a -> Grammar state tok c2 b -> Grammar state 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.

Totality: total
Visibility: export

choiceMap : (a -> Grammar state tok c b) -> Foldable t => t a -> Grammar state 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.

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

  Parse one or more things

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

someTill : Grammar state tok c e -> Grammar state tok True a -> Grammar state 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.

Totality: total
Visibility: export

manyTill : Grammar state tok c e -> Grammar state tok True a -> Grammar state 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.

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

sepEndBy : Grammar state tok True s -> Grammar state tok c a -> Grammar state 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.

Totality: total
Visibility: export

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

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

Totality: total
Visibility: export

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

Totality: total
Visibility: export

between : Grammar state tok True l -> Grammar state tok True r -> Grammar state tok c a -> Grammar state tok True a

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

Totality: total
Visibility: export

location : Grammar state token False (Int, Int)

Totality: total
Visibility: export

endLocation : Grammar state token False (Int, Int)

Totality: total
Visibility: export

column : Grammar state token False Int

Totality: total
Visibility: export

when : Bool -> Lazy (Grammar state token False ()) -> Grammar state token False ()

Totality: total
Visibility: public export