Text.ILex.DStack

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 (DStack s e) (Stack True s [<])

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export
Constructor: 

S : (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)) -> DStack s e q

Projections:

.bufSize_ : DStack s e q -> Nat

.curOffset_ : DStack s e q -> Nat

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

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

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

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

.prevOffset_ : DStack s e q -> Nat

.prev_ : DStack s e q -> ByteString

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

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

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

Hints:

HasBBErr (DStack s e) e

HasBytes (DStack s e)

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

HasStringLits (DStack s e)

.bufSize_ : DStack s e q -> Nat

Totality: total
Visibility: public export

bufSize_ : DStack s e q -> Nat

Totality: total
Visibility: public export

.prev_ : DStack s e q -> ByteString

Totality: total
Visibility: public export

prev_ : DStack s e q -> ByteString

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

.prevOffset_ : DStack s e q -> Nat

Totality: total
Visibility: public export

prevOffset_ : DStack s e q -> Nat

Totality: total
Visibility: public export

.curOffset_ : DStack s e q -> Nat

Totality: total
Visibility: public export

curOffset_ : DStack s e q -> Nat

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

init : Stack True s [<] -> (n : Nat) -> IBuffer n -> F1 q (DStack 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 : DStack s e q => StateAct q s r -> F1 q (Index r)

Totality: total
Visibility: export

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

Totality: total
Visibility: export

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

Totality: total
Visibility: export

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

Totality: total
Visibility: export

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

Totality: total
Visibility: export