Idris2Doc : TyRE.Text.Lexer

TyRE.Text.Lexer

(source)
This is a slightly modified copy of the same module from `contrib` package.

Reexports

importpublic Data.Bool
importpublic Data.List
importpublic Data.Nat
importpublic TyRE.Text.Lexer.Core
importpublic TyRE.Text.Quantity
importpublic TyRE.Text.Token

Definitions

toTokenMap : List (Lexer, k) ->TokenMap (Tokenk)
Visibility: public export
any : Lexer
  Recognise any character.
/./

Visibility: public export
opt : Lexer->RecogniseFalse
  Recognise a lexer or recognise no input. This is not guaranteed
to consume input.
/`l`?/

Visibility: public export
non : Lexer->Lexer
  Recognise any character if the sub-lexer `l` fails.
/(?!`l`)./

Visibility: public export
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.

Visibility: public export
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.

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

Visibility: public export
is : Char->Lexer
  Recognise a specific character.
/[`x`]/

Visibility: public export
isNot : Char->Lexer
  Recognise anything but the given character.
/[\^`x`]/

Visibility: public export
like : Char->Lexer
  Recognise a specific character (case-insensitive).
/[`x`]/i

Visibility: public export
notLike : Char->Lexer
  Recognise anything but the given character (case-insensitive).
/[\^`x`]/i

Visibility: public export
exact : String->Lexer
  Recognise a specific string.
Fails if the string is empty.
/`str`/

Visibility: public export
approx : String->Lexer
  Recognise a specific string (case-insensitive).
Fails if the string is empty.
/`str`/i

Visibility: public export
oneOf : String->Lexer
  Recognise any of the characters in the given string.
/[`chars`]/

Visibility: public export
range : Char->Char->Lexer
  Recognise a character range. Also works in reverse!
/[`start`-`end`]/

Visibility: public export
some : Lexer->Lexer
  Recognise a sequence of at least one sub-lexers
/`l`+/

Visibility: public export
many : Lexer->RecogniseFalse
  Recognise a sequence of at zero or more sub-lexers. This is not
guaranteed to consume input
/`l`\*/

Visibility: public export
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.
/((?!`stopBefore`)`l`)\*/

Visibility: public export
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.
/`l`\*?`stopAfter`/

Visibility: public export
manyTill : Lexer->Lexer->RecogniseFalse
  Recognise many instances of `l` until an instance of `end` is
encountered.

Useful for defining comments.

Visibility: public export
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.
/`l`{`q`}/

Visibility: public export
digit : Lexer
  Recognise a single digit 0-9
/[0-9]/

Visibility: public export
digits : Lexer
  Recognise one or more digits
/[0-9]+/

Visibility: public export
hexDigit : Lexer
  Recognise a single hexidecimal digit
/[0-9A-Fa-f]/

Visibility: public export
hexDigits : Lexer
  Recognise one or more hexidecimal digits
/[0-9A-Fa-f]+/

Visibility: public export
octDigit : Lexer
  Recognise a single octal digit
/[0-8]/

Visibility: public export
octDigits : Lexer
  Recognise one or more octal digits
/[0-8]+/

Visibility: public export
alpha : Lexer
  Recognise a single alpha character
/[A-Za-z]/

Visibility: public export
alphas : Lexer
  Recognise one or more alpha characters
/[A-Za-z]+/

Visibility: public export
lower : Lexer
  Recognise a lowercase alpha character
/[a-z]/

Visibility: public export
lowers : Lexer
  Recognise one or more lowercase alpha characters
/[a-z]+/

Visibility: public export
upper : Lexer
  Recognise an uppercase alpha character
/[A-Z]/

Visibility: public export
uppers : Lexer
  Recognise one or more uppercase alpha characters
/[A-Z]+/

Visibility: public export
alphaNum : Lexer
  Recognise an alphanumeric character
/[A-Za-z0-9]/

Visibility: public export
alphaNums : Lexer
  Recognise one or more alphanumeric characters
/[A-Za-z0-9]+/

Visibility: public export
space : Lexer
  Recognise a single whitespace character
/\\s/

Visibility: public export
spaces : Lexer
  Recognise one or more whitespace characters
/\\s+/

Visibility: public export
newline : Lexer
  Recognise a single newline sequence. Understands CRLF, CR, and LF
/\\r\\n|[\\r\\n]/

Visibility: public export
newlines : Lexer
  Recognise one or more newline sequences. Understands CRLF, CR, and LF
/(\\r\\n|[\\r\\n])+)/

Visibility: public export
symbol : Lexer
  Recognise a single non-whitespace, non-alphanumeric character
/[\^\\sA-Za-z0-9]/

Visibility: public export
symbols : Lexer
  Recognise one or more non-whitespace, non-alphanumeric characters
/[\^\\sA-Za-z0-9]+/

Visibility: public export
control : Lexer
Visibility: public export
controls : Lexer
  Recognise one or more control characters
/[\\x00-\\x1f\\x7f-\\x9f]+/

Visibility: public export
surround : Lexer->Lexer->Lexer->Lexer
  Recognise zero or more occurrences of a sub-lexer between
delimiting lexers
/`start`(`l`)\*?`end`/

Visibility: public export
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)
/`q`(`l`)\*?`q`/

Visibility: public export
escape : Char->Lexer->Lexer
  Recognise an escape character (often '\\') followed by a sub-lexer
/[`esc`]`l`/

Visibility: public export
stringLit : Lexer
  Recognise a string literal, including escaped characters.
(Note: doesn't yet handle escape sequences such as \123)
/"(\\\\.|.)\*?"/

Visibility: public export
charLit : Lexer
  Recognise a character literal, including escaped characters.
(Note: doesn't yet handle escape sequences such as \123)
/'(\\\\.|[\^'])'/

Visibility: public export
intLit : Lexer
  Recognise an integer literal (possibly with a '-' prefix)
/-?[0-9]+/

Visibility: public export
hexLit : Lexer
  Recognise a hexidecimal literal, prefixed by "0x" or "0X"
/0[Xx][0-9A-Fa-f]+/

Visibility: public export
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.
/`start`[\^\\r\\n]+(\\r\\n|[\\r\\n])?/

Visibility: public export
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`

Visibility: public export