Idris2Doc : Text.Parser.Core

Text.Parser.Core

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

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

Fixity Declaration: infixl operator, level 3
(<*>) : Grammartokc1 (a -> b) -> Inf (Grammartokc2a) -> Grammartok (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.

Fixity Declaration: infixl operator, level 3
(<|>) : Grammartokc1ty -> Grammartokc2ty -> Grammartok (c1&& Delay c2) ty
Give two alternative grammars. If both consume, the combination is
guaranteed to consume.

Fixity Declaration: infixr operator, level 2
(>>) : Grammartokc1Unit -> infc1 (Grammartokc2a) -> Grammartok (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)

Fixity Declaration: infixl operator, level 1
(>>=) : Grammartokc1a -> infc1 (a -> Grammartokc2b) -> Grammartok (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)

Fixity Declaration: infixl operator, level 1
Grammar : 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 -> GrammartokFalsety
Terminal : String -> (tok -> Maybea) -> GrammartokTruea
NextIs : String -> (tok -> Bool) -> GrammartokFalsetok
EOF : GrammartokFalseUnit
Fail : Bool -> String -> Grammartokcty
Commit : GrammartokFalseUnit
MustWork : Grammartokca -> Grammartokca
SeqEat : GrammartokTruea -> Inf (a -> Grammartokc2b) -> GrammartokTrueb
SeqEmpty : Grammartokc1a -> (a -> Grammartokc2b) -> Grammartok (c1|| Delay c2) b
ThenEat : GrammartokTrueUnit -> Inf (Grammartokc2b) -> GrammartokTrueb
ThenEmpty : Grammartokc1Unit -> Grammartokc2b -> Grammartok (c1|| Delay c2) b
Alt : Grammartokc1ty -> Grammartokc2ty -> Grammartok (c1&& Delay c2) ty
ParseError : Type -> Type
Totality: total
Constructor: 
Error : String -> Listtok -> ParseErrortok
commit : GrammartokFalseUnit
Commit to an alternative; if the current branch of an alternative
fails to parse, no more branches will be tried
eof : GrammartokFalseUnit
Succeed if the input is empty
fail : String -> Grammartokcty
Always fail with a message
fatalError : String -> Grammartokcty
join : Grammartokc1 (Grammartokc2a) -> Grammartok (c1|| Delay c2) a
Sequence a grammar followed by the grammar it returns.
mapToken : (a -> b) -> Grammarbcty -> Grammaracty
Produce a grammar that can parse a different type of token by providing a
function converting the new token type into the original one.
mustWork : Grammartokcty -> Grammartokcty
If the parser fails, treat it as a fatal error
nextIs : String -> (tok -> Bool) -> GrammartokFalsetok
Check whether the next token satisfies a predicate
parse : Grammartokcty -> Listtok -> Either (ParseErrortok) (ty, Listtok)
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).
peek : GrammartokFalsetok
Look at the next token in the input
pure : ty -> GrammartokFalsety
Always succeed with the given value.
seq : Grammartokc1a -> (a -> Grammartokc2b) -> Grammartok (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 `>>=`.
terminal : String -> (tok -> Maybea) -> GrammartokTruea
Succeeds if running the predicate on the next token returns Just x,
returning x. Otherwise fails.