Idris2Doc : Text.Lexer.Core


(<+>) : Recognisec1 -> infc1 (Recognisec2) -> Recognise (c1|| Delay c2)
  Sequence two recognisers. If either consumes a character, the sequence
is guaranteed to consume a character.

Totality: total
Fixity Declaration: infixl operator, level 8
(<|>) : Recognisec1 -> Recognisec2 -> Recognise (c1&& Delay c2)
  Alternative recognisers. If both consume, the combination is guaranteed
to consume a character.

Totality: total
Fixity Declaration: infixr operator, level 2
Lexer : Type
  A token recogniser. Guaranteed to consume at least one character.

Totality: total
dataRecognise : Bool -> Type
  A language of token recognisers.
@ consumes If `True`, this recogniser is guaranteed to consume at
least one character of input when it succeeds.

Totality: total
Empty : RecogniseFalse
Fail : Recognisec
Lookahead : Bool -> Recognisec -> RecogniseFalse
Pred : (Char -> Bool) -> RecogniseTrue
SeqEat : RecogniseTrue -> Inf (Recognisee) -> RecogniseTrue
SeqEmpty : Recognisee1 -> Recognisee2 -> Recognise (e1|| Delay e2)
SeqSame : Recognisee -> Recognisee -> Recognisee
Alt : Recognisee1 -> Recognisee2 -> Recognise (e1&& Delay e2)
TokenMap : Type -> Type
  A mapping from lexers to the tokens they produce.
This is a list of pairs `(Lexer, String -> tokenType)`
For each Lexer in the list, if a substring in the input matches, run
the associated function to produce a token of type `tokenType`

Totality: total
concatMap : (a -> Recognisec) -> (xs : Lista) -> Recognise (isConsxs&& Delay c)
  Sequence the recognisers resulting from applying a function to each element
of a list. The resulting recogniser will consume input if the produced
recognisers consume and the list is non-empty.

Totality: total
empty : RecogniseFalse
  Recognise no input (doesn't consume any input)

Totality: total
expect : Recognisec -> RecogniseFalse
  Positive lookahead. Never consumes input.

Totality: total
fail : Recognisec
  A recogniser that always fails.

Totality: total
lex : TokenMapa -> String -> (List (WithBoundsa), (Int, (Int, String)))
  Given a mapping from lexers to token generating functions (the
TokenMap a) and an input string, return a list of recognised tokens,
and the line, column, and remainder of the input at the first point in the
string where there are no recognised tokens.

Totality: total
lexTo : (a -> Bool) -> TokenMapa -> String -> (List (WithBoundsa), (Int, (Int, String)))
Totality: total
pred : (Char -> Bool) -> Lexer
  Recognise a character that matches a predicate

Totality: total
reject : Recognisec -> RecogniseFalse
  Negative lookahead. Never consumes input.

Totality: total
scan : Recognisec -> ListChar -> ListChar -> Maybe (ListChar, ListChar)
Totality: total