Idris2Doc : Text.Lexer


alpha : Lexer
  Recognise a single alpha character

Totality: total
alphaNum : Lexer
  Recognise an alphanumeric character

Totality: total
alphaNums : Lexer
  Recognise one or more alphanumeric characters

Totality: total
alphas : Lexer
  Recognise one or more alpha characters

Totality: total
any : Lexer
  Recognise any character.

Totality: total
approx : String -> Lexer
  Recognise a specific string (case-insensitive).
Fails if the string is empty.

Totality: total
binDigit : Lexer
  Recognise a single binary digit

Totality: total
binDigits : Lexer
  Recognise one or more binary digits

Totality: total
binLit : Lexer
  Recognise a binary literal, prefixed by "0b"

Totality: total
binUnderscoredLit : Lexer
Totality: total
blockComment : Lexer -> Lexer -> Lexer
  Recognise all input between `start` and `end` lexers.
Supports balanced nesting.

For block comments that don't support nesting (such as C-style comments),
use `surround`

Totality: total
charLit : Lexer
  Recognise a character literal, including escaped characters.
(Note: doesn't yet handle escape sequences such as \123)

Totality: total
choice : Foldablet => t (Recognisec) -> Recognisec
  Recognise the first matching recogniser in a container. Consumes input if
recognisers in the list consume. Fails if the container is empty.

Totality: total
choiceMap : Foldablet => (a -> Recognisec) -> ta -> Recognisec
  Produce recognisers by applying a function to elements of a container, and
recognise the first match. Consumes input if the function produces consuming
recognisers. Fails if the container is empty.

Totality: total
concat : (xs : List (Recognisec)) -> Recognise (isConsxs&& Delay c)
  Sequence a list of recognisers. Guaranteed to consume input if the list is
non-empty and the recognisers consume.

Totality: total
control : Lexer
Totality: total
controls : Lexer
  Recognise one or more control characters

Totality: total
count : (q : Quantity) -> Lexer -> Recognise (isSucc (minq))
  Recognise a sub-lexer repeated as specified by `q`. Fails if `q` has
`min` and `max` in the wrong order. Consumes input unless `min q` is zero.

Totality: total
digit : Lexer
  Recognise a single digit 0-9

Totality: total
digits : Lexer
  Recognise one or more digits

Totality: total
digitsUnderscoredLit : Lexer
Totality: total
escape : Lexer -> Lexer -> Lexer
  Recognise an escape sub-lexer (often '\\') followed by
another sub-lexer

Totality: total
exact : String -> Lexer
  Recognise a specific string.
Fails if the string is empty.

Totality: total
hexDigit : Lexer
  Recognise a single hexidecimal digit

Totality: total
hexDigits : Lexer
  Recognise one or more hexidecimal digits

Totality: total
hexLit : Lexer
  Recognise a hexidecimal literal, prefixed by "0x" or "0X"

Totality: total
hexUnderscoredLit : Lexer
Totality: total
intLit : Lexer
  Recognise an integer literal (possibly with a '-' prefix)

Totality: total
is : Char -> Lexer
  Recognise a specific character.

Totality: total
isNot : Char -> Lexer
  Recognise anything but the given character.

Totality: total
like : Char -> Lexer
  Recognise a specific character (case-insensitive).

Totality: total
lineComment : Lexer -> Lexer
  Recognise `start`, then recognise all input until a newline is encountered,
and consume the newline. Will succeed if end-of-input is encountered before
a newline.

Totality: total
lower : Lexer
  Recognise a lowercase alpha character

Totality: total
lowers : Lexer
  Recognise one or more lowercase alpha characters

Totality: total
many : Lexer -> RecogniseFalse
  Recognise a sequence of at zero or more sub-lexers. This is not
guaranteed to consume input

Totality: total
manyThen : Recognisec -> Lexer -> Recognisec
  Repeat the sub-lexer `l` zero or more times until the lexer
`stopAfter` is encountered, and consume it. Guaranteed to
consume if `stopAfter` consumes.

Totality: total
manyUntil : Recognisec -> Lexer -> RecogniseFalse
  Repeat the sub-lexer `l` zero or more times until the lexer
`stopBefore` is encountered. `stopBefore` will not be consumed.
Not guaranteed to consume input.

Totality: total
newline : Lexer
  Recognise a single newline sequence. Understands CRLF, CR, and LF

Totality: total
newlines : Lexer
  Recognise one or more newline sequences. Understands CRLF, CR, and LF

Totality: total
non : Lexer -> Lexer
  Recognise any character if the sub-lexer `l` fails.

Totality: total
notLike : Char -> Lexer
  Recognise anything but the given character (case-insensitive).

Totality: total
octDigit : Lexer
  Recognise a single octal digit

Totality: total
octDigits : Lexer
  Recognise one or more octal digits

Totality: total
octLit : Lexer
  Recognise an octal literal, prefixed by "0o"

Totality: total
octUnderscoredLit : Lexer
Totality: total
oneOf : String -> Lexer
  Recognise any of the characters in the given string.

Totality: total
opt : Lexer -> RecogniseFalse
  Recognise a lexer or recognise no input. This is not guaranteed
to consume input.

Totality: total
quote : Lexer -> Lexer -> Lexer
  Recognise zero or more occurrences of a sub-lexer surrounded
by the same quote lexer on both sides (useful for strings)

Totality: total
range : Char -> Char -> Lexer
  Recognise a character range. Also works in reverse!

Totality: total
some : Lexer -> Lexer
  Recognise a sequence of at least one sub-lexers

Totality: total
someUntil : Recognisec -> Lexer -> Lexer
  Repeat the sub-lexer `l` one or more times until the lexer
`stopBefore` is encountered. `stopBefore` will not be consumed.

Totality: total
space : Lexer
  Recognise a single whitespace character

Totality: total
spaces : Lexer
  Recognise one or more whitespace characters

Totality: total
stringLit : Lexer
  Recognise a string literal, including escaped characters.
(Note: doesn't yet handle escape sequences such as \123)

Totality: total
surround : Lexer -> Lexer -> Lexer -> Lexer
  Recognise zero or more occurrences of a sub-lexer between
delimiting lexers

Totality: total
symbol : Lexer
  Recognise a single non-whitespace, non-alphanumeric character

Totality: total
symbols : Lexer
  Recognise one or more non-whitespace, non-alphanumeric characters

Totality: total
toTokenMap : List (Lexer, k) -> TokenMap (Tokenk)
Totality: total
upper : Lexer
  Recognise an uppercase alpha character

Totality: total
uppers : Lexer
  Recognise one or more uppercase alpha characters

Totality: total