Text.Lex.Core

A simple library of lexers and their combinators. A `Lexer` is
just a (dependent) function, which is guaranteed to consume a non-empty
prefix of the input list of characters.

As such, high-performance lexers can be written manually, while
many convenient combinators exist for less performance-critical
applications.

Reexports

Definitions

data Recognise : Bool -> Type

Totality: total
Visibility: public export
Constructors:

Lift : Shifter b -> Recognise b

(<+>) : Recognise b1 -> Recognise b2 -> Recognise (b1 || Delay b2)

(<++>) : Recognise True -> Inf (Recognise b) -> Recognise True

(<|>) : Recognise b1 -> Lazy (Recognise b2) -> Recognise (b1 && Delay b2)

swapOr : Recognise (x || Delay y) -> Recognise (y || Delay x)

Totality: total
Visibility: public export

orSame : Recognise (x || Delay x) -> Recognise x

Totality: total
Visibility: public export

orTrue : Recognise (x || Delay True) -> Recognise True

Totality: total
Visibility: public export

orFalse : Recognise (x || Delay False) -> Recognise x

Totality: total
Visibility: public export

swapAnd : Recognise (x && Delay y) -> Recognise (y && Delay x)

Totality: total
Visibility: public export

andSame : Recognise (x && Delay x) -> Recognise x

Totality: total
Visibility: public export

andTrue : Recognise (x && Delay True) -> Recognise x

Totality: total
Visibility: public export

andFalse : Recognise (x && Delay False) -> Recognise False

Totality: total
Visibility: public export

autoLift : AutoShift b -> Recognise b

Totality: total
Visibility: public export

0 Lexer : Type

  Alias for `Recognise True Char`.

Totality: total
Visibility: public export

run : Recognise b -> (st : SnocList Char) -> (ts : List Char) -> (0 _ : SuffixAcc ts) -> ShiftRes b st ts

Totality: total
Visibility: public export

empty : Recognise False

  Lexer succeeding always without consuming input

Totality: total
Visibility: public export

opt : Recognise True -> Recognise False

  Renders the given lexer optional.

Totality: total
Visibility: public export

expect : Recognise b -> Recognise False

  Positive look-ahead. Does not consume any input.

Totality: total
Visibility: public export

reject : Recognise b -> Recognise False

  Negative look-ahead. Does not consume any input.

Totality: total
Visibility: public export

seqSame : Recognise b -> Recognise b -> Recognise b

Totality: total
Visibility: public export

altSame : Recognise b -> Recognise b -> Recognise b

Totality: total
Visibility: public export

fail : Recognise True

  The lexer which always fails.

Totality: total
Visibility: public export

many : Recognise True -> Recognise False

  Runs the given lexer zero or more times.

Totality: total
Visibility: public export

some : Recognise True -> Recognise True

  Runs the given lexer several times, but at least once.

Totality: total
Visibility: public export

pred : (Char -> Bool) -> Recognise True

  Lexer consuming one item if it fulfills the given predicate.

Totality: total
Visibility: public export

preds : (Char -> Bool) -> Recognise True

  Lexer consuming items while they fulfill the given predicate.
  This is an optimized version of `some . pred`.

Totality: total
Visibility: public export

preds0 : (Char -> Bool) -> Recognise False

  Recogniser consuming items while they fulfill the given predicate.
  This is an optimized version of `many . pred`.

Totality: total
Visibility: public export

concatMap : (a -> Recognise c) -> (xs : List a) -> {auto 0 _ : NonEmpty xs} -> Recognise c

Totality: total
Visibility: public export

choiceMap : Foldable t => (a -> Recognise True) -> t a -> Recognise True

Totality: total
Visibility: public export

choice : Foldable t => t (Recognise True) -> Recognise True

Totality: total
Visibility: public export

0 TokenMap : Type -> Type

Totality: total
Visibility: public export

step : Recognise True -> (SnocList Char -> a) -> Tok True e a

Totality: total
Visibility: public export

first : (ps : TokenMap a) -> {auto 0 _ : NonEmpty ps} -> Tok True e a

Totality: total
Visibility: public export