Text.ILex.State.Streaming

Definitions

record State : Type -> Type -> Type -> Bits32 -> Type -> Type

  A parser state that can be use for streaming lists of values
  such as declarations in a programming language.
  
  The parser stack is stored in mutable field `stack_`, while
  the values parsed so far are stored in `values_`.
  
  In addition, support for working with nested block comments
  is included. This is somewhat opinionated, but client code
  can just ignore it and use an error lexer for the comment field.

Totality: total
Visibility: public export
Constructor: 

SS : (bufSize_ : Nat) -> ByteString -> IBuffer bufSize_ -> Nat -> Nat -> Ref q (LTENat bufSize_) -> Ref q (LTENat bufSize_) -> Ref q (SnocList BytePos) -> Ref q s -> Ref q (Index r) -> Ref q (SnocList a) -> Ref q (SnocList String) -> Ref q (Maybe (BBErr e)) -> Index r -> Ref q Nat -> State e s a r q

Projections:

.bufSize_ : State e s a r q -> Nat

.comment : State e s a r q -> Index r

.curOffset_ : State e s a r q -> Nat

.cur_ : ({rec:0} : State e s a r q) -> IBuffer (bufSize_ {rec:0})

.depth : State e s a r q -> Ref q Nat

.error_ : State e s a r q -> Ref q (Maybe (BBErr e))

.from_ : ({rec:0} : State e s a r q) -> Ref q (LTENat (bufSize_ {rec:0}))

.positions_ : State e s a r q -> Ref q (SnocList BytePos)

.prevOffset_ : State e s a r q -> Nat

.prev_ : State e s a r q -> ByteString

.stack_ : State e s a r q -> Ref q s

.state_ : State e s a r q -> Ref q (Index r)

.strings_ : State e s a r q -> Ref q (SnocList String)

.till_ : ({rec:0} : State e s a r q) -> Ref q (LTENat (bufSize_ {rec:0}))

.values_ : State e s a r q -> Ref q (SnocList a)

Hints:

HasBBErr (State e s a r) e

HasBytes (State e s a r)

HasStack (State e s a r) s

HasStringLits (State e s a r)

.bufSize_ : State e s a r q -> Nat

Totality: total
Visibility: public export

bufSize_ : State e s a r q -> Nat

Totality: total
Visibility: public export

.prev_ : State e s a r q -> ByteString

Totality: total
Visibility: public export

prev_ : State e s a r q -> ByteString

Totality: total
Visibility: public export

.cur_ : ({rec:0} : State e s a r q) -> IBuffer (bufSize_ {rec:0})

Totality: total
Visibility: public export

cur_ : ({rec:0} : State e s a r q) -> IBuffer (bufSize_ {rec:0})

Totality: total
Visibility: public export

.prevOffset_ : State e s a r q -> Nat

Totality: total
Visibility: public export

prevOffset_ : State e s a r q -> Nat

Totality: total
Visibility: public export

.curOffset_ : State e s a r q -> Nat

Totality: total
Visibility: public export

curOffset_ : State e s a r q -> Nat

Totality: total
Visibility: public export

.from_ : ({rec:0} : State e s a r q) -> Ref q (LTENat (bufSize_ {rec:0}))

Totality: total
Visibility: public export

from_ : ({rec:0} : State e s a r q) -> Ref q (LTENat (bufSize_ {rec:0}))

Totality: total
Visibility: public export

.till_ : ({rec:0} : State e s a r q) -> Ref q (LTENat (bufSize_ {rec:0}))

Totality: total
Visibility: public export

till_ : ({rec:0} : State e s a r q) -> Ref q (LTENat (bufSize_ {rec:0}))

Totality: total
Visibility: public export

.positions_ : State e s a r q -> Ref q (SnocList BytePos)

Totality: total
Visibility: public export

positions_ : State e s a r q -> Ref q (SnocList BytePos)

Totality: total
Visibility: public export

.stack_ : State e s a r q -> Ref q s

Totality: total
Visibility: public export

stack_ : State e s a r q -> Ref q s

Totality: total
Visibility: public export

.state_ : State e s a r q -> Ref q (Index r)

Totality: total
Visibility: public export

state_ : State e s a r q -> Ref q (Index r)

Totality: total
Visibility: public export

.values_ : State e s a r q -> Ref q (SnocList a)

Totality: total
Visibility: public export

values_ : State e s a r q -> Ref q (SnocList a)

Totality: total
Visibility: public export

.strings_ : State e s a r q -> Ref q (SnocList String)

Totality: total
Visibility: public export

strings_ : State e s a r q -> Ref q (SnocList String)

Totality: total
Visibility: public export

.error_ : State e s a r q -> Ref q (Maybe (BBErr e))

Totality: total
Visibility: public export

error_ : State e s a r q -> Ref q (Maybe (BBErr e))

Totality: total
Visibility: public export

.comment : State e s a r q -> Index r

Totality: total
Visibility: public export

comment : State e s a r q -> Index r

Totality: total
Visibility: public export

.depth : State e s a r q -> Ref q Nat

Totality: total
Visibility: public export

depth : State e s a r q -> Ref q Nat

Totality: total
Visibility: public export

init : Index r -> s -> (n : Nat) -> IBuffer n -> F1 q (State e s a r q)

Totality: total
Visibility: export

pushValue : State e s a r q => a -> s -> Index r -> F1 q (Index r)

Totality: total
Visibility: export

values : State e s a r q -> F1 q (Either x (List a))

Totality: total
Visibility: export

valuesChunk : State e s a r q -> F1 q (Maybe (List a))

Totality: total
Visibility: export