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 : Ref q ByteString -> Ref q ByteString -> Ref q Nat -> Ref q Integer -> Ref q Nat -> Ref q (SnocList BytePos) -> Ref q (SnocList String) -> Ref q (Stack True s [<]) -> Ref q (Maybe (BBErr e)) -> DStack s e q

Projections:

.cur_ : DStack s e q -> Ref q ByteString

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

.len_ : DStack s e q -> Ref q Nat

.offset_ : DStack s e q -> Ref q Nat

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

.prev_ : DStack s e q -> Ref q ByteString

.relpos_ : DStack s e q -> Ref q Integer

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

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

Hints:

HasBBErr (DStack s e) e

HasBytes (DStack s e)

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

HasStringLits (DStack s e)

.prev_ : DStack s e q -> Ref q ByteString

Totality: total
Visibility: public export

prev_ : DStack s e q -> Ref q ByteString

Totality: total
Visibility: public export

.cur_ : DStack s e q -> Ref q ByteString

Totality: total
Visibility: public export

cur_ : DStack s e q -> Ref q ByteString

Totality: total
Visibility: public export

.offset_ : DStack s e q -> Ref q Nat

Totality: total
Visibility: public export

offset_ : DStack s e q -> Ref q Nat

Totality: total
Visibility: public export

.relpos_ : DStack s e q -> Ref q Integer

Totality: total
Visibility: public export

relpos_ : DStack s e q -> Ref q Integer

Totality: total
Visibility: public export

.len_ : DStack s e q -> Ref q Nat

Totality: total
Visibility: public export

len_ : DStack s e q -> Ref q Nat

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 [<] -> 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