Text.Lex.Tokenizer

Definitions

data Tokenizer : Type -> Type -> Type

  Description of a language's tokenization rule.

Totality: total
Visibility: public export
Constructors:

Direct : Tok True e tt -> Tokenizer e tt

  Use this for fast, direct lexing of constant tokens.
  Note: It is assumed that the lexed characters do *NOT* contain
  any line breaks.

Compose : Tok True e (tt, tag) -> Inf (tag -> Tokenizer e tt) -> (tag -> Tok True e tt) -> Tokenizer e tt

(<|>) : Tokenizer e tt -> Lazy (Tokenizer e tt) -> Tokenizer e tt

choiceMap : (a -> Tokenizer e tt) -> (as : List a) -> {auto 0 _ : NonEmpty as} -> Tokenizer e tt

Totality: total
Visibility: export

choice : (rs : List (Tokenizer e tt)) -> {auto 0 _ : NonEmpty rs} -> Tokenizer e tt

Totality: total
Visibility: export

record TokRes : Bool -> List Char -> Type -> Type -> Type

  Result of running a `Tokenizer` repeatedly over a
  sequence of characters.

Totality: total
Visibility: public export
Constructor: 

TR : Position -> SnocList (Bounded a) -> Maybe r -> (rem : List Char) -> (0 _ : Suffix strict rem cs) -> TokRes strict cs r a

Projections:

.pos : TokRes strict cs r a -> Position

.reason : TokRes strict cs r a -> Maybe r

.rem : TokRes strict cs r a -> List Char

0 .suf : ({rec:0} : TokRes strict cs r a) -> Suffix strict (rem {rec:0}) cs

.toks : TokRes strict cs r a -> SnocList (Bounded a)

.pos : TokRes strict cs r a -> Position

Totality: total
Visibility: public export

pos : TokRes strict cs r a -> Position

Totality: total
Visibility: public export

.toks : TokRes strict cs r a -> SnocList (Bounded a)

Totality: total
Visibility: public export

toks : TokRes strict cs r a -> SnocList (Bounded a)

Totality: total
Visibility: public export

.reason : TokRes strict cs r a -> Maybe r

Totality: total
Visibility: public export

reason : TokRes strict cs r a -> Maybe r

Totality: total
Visibility: public export

.rem : TokRes strict cs r a -> List Char

Totality: total
Visibility: public export

rem : TokRes strict cs r a -> List Char

Totality: total
Visibility: public export

0 .suf : ({rec:0} : TokRes strict cs r a) -> Suffix strict (rem {rec:0}) cs

Totality: total
Visibility: public export

0 suf : ({rec:0} : TokRes strict cs r a) -> Suffix strict (rem {rec:0}) cs

Totality: total
Visibility: public export

lex : Interpolation a => Tokenizer e a -> (s : String) -> TokRes False (unpack s) (Bounded (InnerError e)) a

  Given a tokenizer 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
Visibility: export