Idris2Doc : Text.Parser.Core

Text.Parser.Core

(*>) : Grammarstatetokc1a -> Grammarstatetokc2b -> Grammarstatetok (c1|| Delay c2) b
  Sequence two grammars. If both succeed, use the value of the second one.
Guaranteed to consume if either grammar consumes.

Totality: total
Fixity Declaration: infixl operator, level 3
(<*) : Grammarstatetokc1a -> Grammarstatetokc2b -> Grammarstatetok (c1|| Delay c2) a
  Sequence two grammars. If both succeed, use the value of the first one.
Guaranteed to consume if either grammar consumes.

Totality: total
Fixity Declaration: infixl operator, level 3
(<*>) : Grammarstatetokc1 (a -> b) -> Grammarstatetokc2a -> Grammarstatetok (c1|| Delay c2) b
  Sequence a grammar with value type `a -> b` and a grammar
with value type `a`. If both succeed, apply the function
from the first grammar to the value from the second grammar.
Guaranteed to consume if either grammar consumes.

Totality: total
Fixity Declaration: infixl operator, level 3
(<|>) : Grammarstatetokc1ty -> Lazy (Grammarstatetokc2ty) -> Grammarstatetok (c1&& Delay c2) ty
  Give two alternative grammars. If both consume, the combination is
guaranteed to consume.

Totality: total
Fixity Declaration: infixr operator, level 2
(<||>) : Grammarstatetokc1a -> Lazy (Grammarstatetokc2b) -> Grammarstatetok (c1&& Delay c2) (Eitherab)
  Take the tagged disjunction of two grammars. If both consume, the
combination is guaranteed to consume.

Totality: total
Fixity Declaration: infixr operator, level 2
(>>) : Grammarstatetokc1 () -> infc1 (Grammarstatetokc2a) -> Grammarstatetok (c1|| Delay c2) a
  Sequence two grammars. If either consumes some input, the sequence is
guaranteed to consume some input. If the first one consumes input, the
second is allowed to be recursive (because it means some input has been
consumed and therefore the input is smaller)

Totality: total
Fixity Declaration: infixl operator, level 1
(>>=) : Grammarstatetokc1a -> infc1 (a -> Grammarstatetokc2b) -> Grammarstatetok (c1|| Delay c2) b
  Sequence two grammars. If either consumes some input, the sequence is
guaranteed to consume some input. If the first one consumes input, the
second is allowed to be recursive (because it means some input has been
consumed and therefore the input is smaller)

Totality: total
Fixity Declaration: infixl operator, level 1
dataGrammar : Type -> Type -> Bool -> Type -> Type
  Description of a language's grammar. The `tok` parameter is the type
of tokens, and the `consumes` flag is True if the language is guaranteed
to be non-empty - that is, successfully parsing the language is guaranteed
to consume some input.

Totality: total
Constructors:
Empty : ty -> GrammarstatetokFalsety
Terminal : String -> (tok -> Maybea) -> GrammarstatetokTruea
NextIs : String -> (tok -> Bool) -> GrammarstatetokFalsetok
EOF : GrammarstatetokFalse ()
Fail : MaybeBounds -> Bool -> String -> Grammarstatetokcty
Try : Grammarstatetokcty -> Grammarstatetokcty
Commit : GrammarstatetokFalse ()
MustWork : Grammarstatetokca -> Grammarstatetokca
SeqEat : GrammarstatetokTruea -> Inf (a -> Grammarstatetokc2b) -> GrammarstatetokTrueb
SeqEmpty : Grammarstatetokc1a -> (a -> Grammarstatetokc2b) -> Grammarstatetok (c1|| Delay c2) b
ThenEat : GrammarstatetokTrue () -> Inf (Grammarstatetokc2a) -> GrammarstatetokTruea
ThenEmpty : Grammarstatetokc1 () -> Grammarstatetokc2a -> Grammarstatetok (c1|| Delay c2) a
Alt : Grammarstatetokc1ty -> Lazy (Grammarstatetokc2ty) -> Grammarstatetok (c1&& Delay c2) ty
Bounds : Grammarstatetokcty -> Grammarstatetokc (WithBoundsty)
Position : GrammarstatetokFalseBounds
Act : state -> GrammarstatetokFalse ()
dataParsingError : Type -> Type
Totality: total
Constructor: 
Error : String -> MaybeBounds -> ParsingErrortok
act : state -> GrammarstatetokFalse ()
Totality: total
bounds : Grammarstatetokcty -> Grammarstatetokc (WithBoundsty)
Totality: total
commit : GrammarstatetokFalse ()
  Commit to an alternative; if the current branch of an alternative
fails to parse, no more branches will be tried

Totality: total
eof : GrammarstatetokFalse ()
  Succeed if the input is empty

Totality: total
fail : String -> Grammarstatetokcty
  Always fail with a message

Totality: total
failLoc : Bounds -> String -> Grammarstatetokcty
  Always fail with a message and a location

Totality: total
fatalError : String -> Grammarstatetokcty
  Fail with no possibility for recovery (i.e.
no alternative parsing can succeed).

Totality: total
fatalLoc : Bounds -> String -> Grammarstatetokcty
  Fail with no possibility for recovery (i.e.
no alternative parsing can succeed).

Totality: total
join : Grammarstatetokc1 (Grammarstatetokc2a) -> Grammarstatetok (c1|| Delay c2) a
  Sequence a grammar followed by the grammar it returns.

Totality: total
mapToken : (a -> b) -> Grammarstatebcty -> Grammarstateacty
  Produce a grammar that can parse a different type of token by providing a
function converting the new token type into the original one.

Totality: total
mustWork : Grammarstatetokcty -> Grammarstatetokcty
  If the parser fails, treat it as a fatal error

Totality: total
nextIs : String -> (tok -> Bool) -> GrammarstatetokFalsetok
  Check whether the next token satisfies a predicate

Totality: total
parse : Grammar () tokcty -> List (WithBoundstok) -> Either (List1 (ParsingErrortok)) (ty, List (WithBoundstok))
  Parse a list of tokens according to the given grammar. If successful,
returns a pair of the parse result and the unparsed tokens (the remaining
input).

Totality: total
parseWith : Monoidstate => Grammarstatetokcty -> List (WithBoundstok) -> Either (List1 (ParsingErrortok)) (state, (ty, List (WithBoundstok)))
Totality: total
peek : GrammarstatetokFalsetok
  Look at the next token in the input

Totality: total
position : GrammarstatetokFalseBounds
Totality: total
pure : ty -> GrammarstatetokFalsety
  Always succeed with the given value.

Totality: total
seq : Grammarstatetokc1a -> (a -> Grammarstatetokc2b) -> Grammarstatetok (c1|| Delay c2) b
  Sequence two grammars. If either consumes some input, the sequence is
guaranteed to consume input. This is an explicitly non-infinite version
of `>>=`.

Totality: total
terminal : String -> (tok -> Maybea) -> GrammarstatetokTruea
  Succeeds if running the predicate on the next token returns Just x,
returning x. Otherwise fails.

Totality: total
try : Grammarstatetokcty -> Grammarstatetokcty
  Catch a fatal error

Totality: total