Text.ILex.State.Dependent

This module provides an experimental alternative
to `Text.ILex.Stack` with a correctly typed parser
stack.

Definitions

data Stack : Bool -> (SnocList Type -> Type) -> SnocList Type -> Type

Totality: total
Visibility: public export
Constructors:

Lin : Stack False s [<]

(:>) : Stack b s ts -> s ts -> Stack True s [<]

(:<) : Stack b s ts -> t -> Stack False s (ts :< t)

Hint: 

HasStack (DState s e) (Stack True s [<])

push : Stack b s [<] -> t -> s [<t] -> Stack True s [<]

Totality: total
Visibility: public export

record DState : (SnocList Type -> Type) -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

DS : (bufSize_ : Nat) -> ByteString -> IBuffer bufSize_ -> Nat -> Nat -> Ref q (LTENat bufSize_) -> Ref q (LTENat bufSize_) -> Ref q (SnocList BytePos) -> Ref q (SnocList String) -> Ref q (Stack True s [<]) -> Ref q (Maybe (BBErr e)) -> DState s e q

Projections:

.bufSize_ : DState s e q -> Nat

.curOffset_ : DState s e q -> Nat

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

.error_ : DState s e q -> Ref q (Maybe (BBErr e))

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

.positions_ : DState s e q -> Ref q (SnocList BytePos)

.prevOffset_ : DState s e q -> Nat

.prev_ : DState s e q -> ByteString

.stack_ : DState s e q -> Ref q (Stack True s [<])

.strings_ : DState s e q -> Ref q (SnocList String)

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

Hints:

HasBBErr (DState s e) e

HasBytes (DState s e)

HasStack (DState s e) (Stack True s [<])

HasStringLits (DState s e)

.bufSize_ : DState s e q -> Nat

Totality: total
Visibility: public export

bufSize_ : DState s e q -> Nat

Totality: total
Visibility: public export

.prev_ : DState s e q -> ByteString

Totality: total
Visibility: public export

prev_ : DState s e q -> ByteString

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

cur_ : ({rec:0} : DState s e q) -> IBuffer (bufSize_ {rec:0})

Totality: total
Visibility: public export

.prevOffset_ : DState s e q -> Nat

Totality: total
Visibility: public export

prevOffset_ : DState s e q -> Nat

Totality: total
Visibility: public export

.curOffset_ : DState s e q -> Nat

Totality: total
Visibility: public export

curOffset_ : DState s e q -> Nat

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

.positions_ : DState s e q -> Ref q (SnocList BytePos)

Totality: total
Visibility: public export

positions_ : DState s e q -> Ref q (SnocList BytePos)

Totality: total
Visibility: public export

.strings_ : DState s e q -> Ref q (SnocList String)

Totality: total
Visibility: public export

strings_ : DState s e q -> Ref q (SnocList String)

Totality: total
Visibility: public export

.stack_ : DState s e q -> Ref q (Stack True s [<])

Totality: total
Visibility: public export

stack_ : DState s e q -> Ref q (Stack True s [<])

Totality: total
Visibility: public export

.error_ : DState s e q -> Ref q (Maybe (BBErr e))

Totality: total
Visibility: public export

error_ : DState s e q -> Ref q (Maybe (BBErr e))

Totality: total
Visibility: public export

init : Stack True s [<] -> (n : Nat) -> IBuffer n -> F1 q (DState s e q)

  Initializes a new parser stack.

Totality: total
Visibility: export

0 StateAct : Type -> (SnocList Type -> Type) -> Bits32 -> Type

Totality: total
Visibility: public export

dact : DState s e q => StateAct q s r -> F1 q (Index r)

Totality: total
Visibility: export

dput : DState s e q => s ts -> Cast (s ts) a => Stack b s ts -> F1 q a

Totality: total
Visibility: export

dpush0 : DState s e q => s [<] -> Cast (s [<]) a => F1 q a

Totality: total
Visibility: export

dpush : DState s e q => s [<t] -> Cast (s [<t]) a => t -> F1 q a

Totality: total
Visibility: export

derr : DState s e q => s [<] -> Cast (s [<]) a => Stack b s ts -> s ts -> F1 q a

Totality: total
Visibility: export