Idris2Doc : Text.Parser.Core

Text.Parser.Core

(*>) : Grammar state tok c1 a -> Grammar state tok c2 b -> Grammar state tok (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
(<*) : Grammar state tok c1 a -> Grammar state tok c2 b -> Grammar state tok (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
(<*>) : Grammar state tok c1 (a -> b) -> Grammar state tok c2 a -> Grammar state tok (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
(<|>) : Grammar state tok c1 ty -> Lazy (Grammar state tok c2 ty) -> Grammar state tok (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
(<||>) : Grammar state tok c1 a -> Lazy (Grammar state tok c2 b) -> Grammar state tok (c1 && Delay c2) (Either a b)
  Take the tagged disjunction of two grammars. If both consume, the
  combination is guaranteed to consume.

  Totality: total
  Fixity Declaration: infixr operator, level 2
(>>) : Grammar state tok c1 () -> inf c1 (Grammar state tok c2 a) -> Grammar state tok (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
(>>=) : Grammar state tok c1 a -> inf c1 (a -> Grammar state tok c2 b) -> Grammar state tok (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
data Grammar : 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 -> Grammar state tok False ty
  
Terminal : String -> (tok -> Maybe a) -> Grammar state tok True a
  
NextIs : String -> (tok -> Bool) -> Grammar state tok False tok
  
EOF : Grammar state tok False ()
  
Fail : Maybe Bounds -> Bool -> String -> Grammar state tok c ty
  
Try : Grammar state tok c ty -> Grammar state tok c ty
  
Commit : Grammar state tok False ()
  
MustWork : Grammar state tok c a -> Grammar state tok c a
  
SeqEat : Grammar state tok True a -> Inf (a -> Grammar state tok c2 b) -> Grammar state tok True b
  
SeqEmpty : Grammar state tok c1 a -> (a -> Grammar state tok c2 b) -> Grammar state tok (c1 || Delay c2) b
  
ThenEat : Grammar state tok True () -> Inf (Grammar state tok c2 a) -> Grammar state tok True a
  
ThenEmpty : Grammar state tok c1 () -> Grammar state tok c2 a -> Grammar state tok (c1 || Delay c2) a
  
Alt : Grammar state tok c1 ty -> Lazy (Grammar state tok c2 ty) -> Grammar state tok (c1 && Delay c2) ty
  
Bounds : Grammar state tok c ty -> Grammar state tok c (WithBounds ty)
  
Position : Grammar state tok False Bounds
  
Act : state -> Grammar state tok False ()
data ParsingError : Type -> Type
  Totality: total
  Constructor: 
Error : String -> Maybe Bounds -> ParsingError tok
act : state -> Grammar state tok False ()
  Totality: total
bounds : Grammar state tok c ty -> Grammar state tok c (WithBounds ty)
  Totality: total
commit : Grammar state tok False ()
  Commit to an alternative; if the current branch of an alternative
  fails to parse, no more branches will be tried

  Totality: total
eof : Grammar state tok False ()
  Succeed if the input is empty

  Totality: total
fail : String -> Grammar state tok c ty
  Always fail with a message

  Totality: total
failLoc : Bounds -> String -> Grammar state tok c ty
  Always fail with a message and a location

  Totality: total
fatalError : String -> Grammar state tok c ty
  Fail with no possibility for recovery (i.e.
  no alternative parsing can succeed).

  Totality: total
fatalLoc : Bounds -> String -> Grammar state tok c ty
  Fail with no possibility for recovery (i.e.
  no alternative parsing can succeed).

  Totality: total
join : Grammar state tok c1 (Grammar state tok c2 a) -> Grammar state tok (c1 || Delay c2) a
  Sequence a grammar followed by the grammar it returns.

  Totality: total
mapToken : (a -> b) -> Grammar state b c ty -> Grammar state a c ty
  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 : Grammar state tok c ty -> Grammar state tok c ty
  If the parser fails, treat it as a fatal error

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

  Totality: total
parse : Grammar () tok c ty -> List (WithBounds tok) -> Either (List1 (ParsingError tok)) (ty, List (WithBounds tok))
  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 : Monoid state => Grammar state tok c ty -> List (WithBounds tok) -> Either (List1 (ParsingError tok)) (state, (ty, List (WithBounds tok)))
  Totality: total
peek : Grammar state tok False tok
  Look at the next token in the input

  Totality: total
position : Grammar state tok False Bounds
  Totality: total
pure : ty -> Grammar state tok False ty
  Always succeed with the given value.

  Totality: total
seq : Grammar state tok c1 a -> (a -> Grammar state tok c2 b) -> Grammar state tok (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 -> Maybe a) -> Grammar state tok True a
  Succeeds if running the predicate on the next token returns Just x,
  returning x. Otherwise fails.

  Totality: total
try : Grammar state tok c ty -> Grammar state tok c ty
  Catch a fatal error

  Totality: total