TyRE.Text.Lexer.Core

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

Reexports

Definitions

data Recognise : 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
Visibility: public export
Constructors:

Empty : Recognise False

Fail : Recognise c

Lookahead : Bool -> Recognise c -> Recognise False

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

SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True

SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || Delay e2)

Alt : Recognise e1 -> Recognise e2 -> Recognise (e1 && Delay e2)

Lexer : Type

  A token recogniser. Guaranteed to consume at least one character.

Visibility: public export

(<+>) : Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || Delay c2)

  Sequence two recognisers. If either consumes a character, the sequence
  is guaranteed to consume a character.

Visibility: public export
Fixity Declaration: infixl operator, level 8

(<|>) : Recognise c1 -> Recognise c2 -> Recognise (c1 && Delay c2)

  Alternative recognisers. If both consume, the combination is guaranteed
  to consumer a character.

Visibility: public export
Fixity Declaration: infixr operator, level 2

fail : Recognise c

  A recogniser that always fails.

Visibility: public export

empty : Recognise False

  Recognise no input (doesn't consume any input)

Visibility: public export

pred : (Char -> Bool) -> Lexer

  Recognise a character that matches a predicate

Visibility: public export

expect : Recognise c -> Recognise False

  Positive lookahead. Never consumes input.

Visibility: public export

reject : Recognise c -> Recognise False

  Negative lookahead. Never consumes input.

Visibility: public export

concatMap : (a -> Recognise c) -> (xs : List a) -> Recognise (c && Delay (isCons xs))

  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.

Visibility: public export

data StrLen : Type

Totality: total
Visibility: public export
Constructor: 

MkStrLen : String -> Nat -> StrLen

Hint: 

Show StrLen

getString : StrLen -> String

Visibility: public export

strIndex : StrLen -> Nat -> Maybe Char

Visibility: public export

mkStr : String -> StrLen

Visibility: public export

strTail : Nat -> StrLen -> StrLen

Visibility: public export

unpack' : String -> List Char

Visibility: public export

scan : Recognise c -> List Char -> List Char -> Maybe (List Char, List Char)

Visibility: public export

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`

Visibility: public export

record TokenData : Type -> Type

  A token, and the line and column where it was in the input

Totality: total
Visibility: public export
Constructor: 

MkToken : Int -> Int -> a -> TokenData a

Projections:

.col : TokenData a -> Int

.line : TokenData a -> Int

.tok : TokenData a -> a

Hint: 

Show a => Show (TokenData a)

.line : TokenData a -> Int

Visibility: public export

line : TokenData a -> Int

Visibility: public export

.col : TokenData a -> Int

Visibility: public export

col : TokenData a -> Int

Visibility: public export

.tok : TokenData a -> a

Visibility: public export

tok : TokenData a -> a

Visibility: public export

tokenise : (TokenData a -> Bool) -> Int -> Int -> List (TokenData a) -> TokenMap a -> List Char -> (List (TokenData a), (Int, (Int, List Char)))

Visibility: public export

lex : TokenMap a -> String -> (List (TokenData a), (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.

Visibility: public export

lexTo : (TokenData a -> Bool) -> TokenMap a -> String -> (List (TokenData a), (Int, (Int, String)))

Visibility: public export