Idris2Doc : Text.Parser

Text.Parser

Reexports

importpublic Data.List1
importpublic Text.Parser.Core
importpublic Text.Quantity
importpublic Text.Token

Definitions

match : {auto{conArg:983} : TokenKindk} ->Eqk=> (kind : k) ->Grammarstate (Tokenk) True (TokTypekind)
  Parse a terminal based on a kind of token.

Totality: total
Visibility: export
option : a->Grammarstatetokca->GrammarstatetokFalsea
  Optionally parse a thing, with a default value if the grammar doesn't
match. May match the empty input.

Totality: total
Visibility: export
optional : Grammarstatetokca->GrammarstatetokFalse (Maybea)
  Optionally parse a thing.
To provide a default value, use `option` instead.

Totality: total
Visibility: export
choose : Grammarstatetokc1a->Grammarstatetokc2b->Grammarstatetok (c1&& Delay c2) (Eitherab)
  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->Grammarstatetokcb) ->Foldablet=>ta->Grammarstatetokcb
  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 : Foldablet=>t (Grammarstatetokca) ->Grammarstatetokca
  Try each grammar in a container until the first one succeeds.
Fails if the container is empty.

Totality: total
Visibility: export
some : GrammarstatetokTruea->GrammarstatetokTrue (List1a)
  Parse one or more things

Totality: total
Visibility: export
many : GrammarstatetokTruea->GrammarstatetokFalse (Lista)
  Parse zero or more things (may match the empty input)

Totality: total
Visibility: export
count : (q : Quantity) ->GrammarstatetokTruea->Grammarstatetok (isSucc (minq)) (Lista)
  Parse `p`, repeated as specified by `q`, returning the list of values.

Totality: total
Visibility: export
someTill : Grammarstatetokce->GrammarstatetokTruea->GrammarstatetokTrue (List1a)
  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 : Grammarstatetokce->GrammarstatetokTruea->Grammarstatetokc (Lista)
  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 : GrammarstatetokTrues->Grammarstatetokca->GrammarstatetokTruea
  Parse one or more instance of `skip` until `p` is encountered,
returning its value.

Totality: total
Visibility: export
afterMany : GrammarstatetokTrues->Grammarstatetokca->Grammarstatetokca
  Parse zero or more instance of `skip` until `p` is encountered,
returning its value.

Totality: total
Visibility: export
sepBy1 : GrammarstatetokTrues->Grammarstatetokca->Grammarstatetokc (List1a)
  Parse one or more things, each separated by another thing.

Totality: total
Visibility: export
sepBy : GrammarstatetokTrues->Grammarstatetokca->GrammarstatetokFalse (Lista)
  Parse zero or more things, each separated by another thing. May
match the empty input.

Totality: total
Visibility: export
sepEndBy1 : GrammarstatetokTrues->Grammarstatetokca->Grammarstatetokc (List1a)
  Parse one or more instances of `p` separated by and optionally terminated by
`sep`.

Totality: total
Visibility: export
sepEndBy : GrammarstatetokTrues->Grammarstatetokca->GrammarstatetokFalse (Lista)
  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 : GrammarstatetokTrues->Grammarstatetokca->GrammarstatetokTrue (List1a)
  Parse one or more instances of `p`, separated and terminated by `sep`.

Totality: total
Visibility: export
endBy : GrammarstatetokTrues->Grammarstatetokca->GrammarstatetokFalse (Lista)
Totality: total
Visibility: export
between : GrammarstatetokTruel->GrammarstatetokTruer->Grammarstatetokca->GrammarstatetokTruea
  Parse an instance of `p` that is between `left` and `right`.

Totality: total
Visibility: export
location : GrammarstatetokenFalse (Int, Int)
Totality: total
Visibility: export
endLocation : GrammarstatetokenFalse (Int, Int)
Totality: total
Visibility: export
column : GrammarstatetokenFalseInt
Totality: total
Visibility: export
when : Bool-> Lazy (GrammarstatetokenFalse ()) ->GrammarstatetokenFalse ()
Totality: total
Visibility: public export