Text.ILex.DStack

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

Definitions

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

Totality: total
Visibility: public export
Constructors:

Nil : Stack False s []

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

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

Hint: 

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

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export
Constructor: 

S : Ref q Nat -> Ref q Nat -> Ref q (SnocList Position) -> Ref q (SnocList String) -> Ref q (Stack True s []) -> Ref q (Maybe (BoundedErr e)) -> Ref q ByteString -> DStack s e q

Projections:

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

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

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

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

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

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

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

Hints:

HasBytes (DStack s e)

HasError (DStack s e) e

HasPosition (DStack s e)

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

HasStringLits (DStack s e)

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

Totality: total
Visibility: public export

line_ : DStack s e q -> Ref q Nat

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

col_ : DStack s e q -> Ref q Nat

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

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 (BoundedErr e))

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

bytes_ : DStack s e q -> Ref q ByteString

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 -> (List 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

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 => s ts -> Stack b s ts -> F1 q a

Totality: total
Visibility: export