Text.ILex.Runner1

Reexports

import public Data.ByteString
import public Data.Vect
import public Text.ILex.Parser

Definitions

record LexState : P1 q e a -> Type

  Lexing state.
  
  This encapsulates the current state as well as
  the remainder of the previous chunk that marks
  the beginning of the current token.

Totality: total
Visibility: public export
Constructor:

LST : PIx p -> PST p -> PStepper sts p -> PByteStep sts p -> Maybe (PStep p) -> LexState p

Projections:

.cur : ({rec:0} : LexState p) -> PByteStep (sts {rec:0}) p
.dfa : ({rec:0} : LexState p) -> PStepper (sts {rec:0}) p
.stack : LexState p -> PST p
.state : LexState p -> PIx p
0 .sts : LexState p -> Nat
.tok : LexState p -> Maybe (PStep p)

0 .sts : LexState p -> Nat

Visibility: public export

0 sts : LexState p -> Nat

Visibility: public export

.state : LexState p -> PIx p

Visibility: public export

state : LexState p -> PIx p

Visibility: public export

.stack : LexState p -> PST p

Visibility: public export

stack : LexState p -> PST p

Visibility: public export

.dfa : ({rec:0} : LexState p) -> PStepper (sts {rec:0}) p

Visibility: public export

dfa : ({rec:0} : LexState p) -> PStepper (sts {rec:0}) p

Visibility: public export

.cur : ({rec:0} : LexState p) -> PByteStep (sts {rec:0}) p

Visibility: public export

cur : ({rec:0} : LexState p) -> PByteStep (sts {rec:0}) p

Visibility: public export

.tok : LexState p -> Maybe (PStep p)

Visibility: public export

tok : LexState p -> Maybe (PStep p)

Visibility: public export

init : (p : P1 q e a) -> F1 q (LexState p)

Visibility: export

0 PartRes : P1 q e a -> Type

  Result of a partial lexing step: In such a step, we lex
  till the end of a chunk of bytes, allowing for a remainder of
  bytes that could not yet be identified as a tokens.

Visibility: public export

pparseFrom : (p : P1 q e a) -> LexState p -> (pos : Nat) -> Ix pos n => IBuffer n -> PartRes p

Visibility: export

pparseBytes : (p : P1 q e a) -> LexState p -> ByteString -> PartRes p

Visibility: export