Text.ILex.Stack

Definitions

record Stack : Type -> Type -> Bits32 -> Type -> Type

  A general-purpose mutable parser stack that can be used in many common
  situation, such as when needing just a lexer or wanting to parse
  a single value of a simple type.
  
  For concrete usage examples, see ilex-json and ilex-toml, which both
  make use of this type as their mutable parser state.
  
  If you are writing a parser for something complex such as a programming
  language, you're probably going to need quite a few custom fields, so
  feel free to come up with your own.

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 a -> Ref q (Index r) -> Ref q (SnocList String) -> Ref q (Maybe (BBErr e)) -> Stack e a r q

Projections:

.cur_ : Stack e a r q -> Ref q ByteString

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

.len_ : Stack e a r q -> Ref q Nat

.offset_ : Stack e a r q -> Ref q Nat

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

.prev_ : Stack e a r q -> Ref q ByteString

.relpos_ : Stack e a r q -> Ref q Integer

.stack_ : Stack e a r q -> Ref q a

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

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

Hints:

HasBBErr (Stack e a r) e

HasBytes (Stack e a r)

HasStack (Stack e a r) a

HasStringLits (Stack e a r)

.prev_ : Stack e a r q -> Ref q ByteString

Totality: total
Visibility: public export

prev_ : Stack e a r q -> Ref q ByteString

Totality: total
Visibility: public export

.cur_ : Stack e a r q -> Ref q ByteString

Totality: total
Visibility: public export

cur_ : Stack e a r q -> Ref q ByteString

Totality: total
Visibility: public export

.offset_ : Stack e a r q -> Ref q Nat

Totality: total
Visibility: public export

offset_ : Stack e a r q -> Ref q Nat

Totality: total
Visibility: public export

.relpos_ : Stack e a r q -> Ref q Integer

Totality: total
Visibility: public export

relpos_ : Stack e a r q -> Ref q Integer

Totality: total
Visibility: public export

.len_ : Stack e a r q -> Ref q Nat

Totality: total
Visibility: public export

len_ : Stack e a r q -> Ref q Nat

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

.stack_ : Stack e a r q -> Ref q a

Totality: total
Visibility: public export

stack_ : Stack e a r q -> Ref q a

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

init : {auto 0 _ : 0 < r} -> a -> F1 q (Stack e a r q)

  Initializes a new parser stack.

Totality: total
Visibility: export

0 Tok : Type -> Type

Totality: total
Visibility: public export

0 Toks : Type -> Type

Totality: total
Visibility: public export

0 Skot : Type -> Type

Totality: total
Visibility: public export

0 L1 : Type -> Type -> Type -> Type

Totality: total
Visibility: public export

0 Lexer : Type -> Type -> Type

Totality: total
Visibility: public export

pushBounded : HasBytes s => HasStack s (Skot a) => RExp True -> {auto 0 _ : 0 < r} -> s q => a -> F1 q (Index r)

Totality: total
Visibility: export

tok : HasBytes s => HasStack s (Skot a) => RExp True -> {auto 0 _ : 0 < r} -> a -> (RExp True, Step q r s)

Totality: total
Visibility: export

byteTok : HasBytes s => HasStack s (Skot a) => RExp True -> {auto 0 _ : 0 < r} -> (ByteString -> a) -> (RExp True, Step q r s)

Totality: total
Visibility: export

stringTok : HasBytes s => HasStack s (Skot a) => RExp True -> {auto 0 _ : 0 < r} -> (String -> a) -> (RExp True, Step q r s)

Totality: total
Visibility: export

lexEOI : {auto 0 _ : 0 < r} -> HasStack s (SnocList a) => HasBBErr s e => HasBytes s => Index r -> s q -> F1 q (Either (BBErr e) (List a))

Totality: total
Visibility: export

lexer : {auto 0 _ : 0 < r} -> Steps q r (Stack e (Skot a) r) -> L1 q e a

Totality: total
Visibility: export

data Token : Type -> Type -> Type

  Description of lexicographic tokens

Totality: total
Visibility: public export
Constructors:

Ignore : Token e a

  Marks a terminal state that does not produce a token.
  This can be used for comments or whitespace that should be
  ignored.

Const : a -> Token e a

  A constant token that allows us to emit a value directly.

Txt : (String -> Either e a) -> Token e a

  A token that needs to be parsed from its corresponding bytestring.

Bytes : (ByteString -> Either e a) -> Token e a

  A token that needs to be parsed from its corresponding bytestring.

const : a -> Token e a

Totality: total
Visibility: export

txt : (String -> a) -> Token e a

Totality: total
Visibility: export

bytes : (ByteString -> a) -> Token e a

Totality: total
Visibility: export

0 PVal1 : Type -> Type -> Type -> Type

Totality: total
Visibility: public export

value : Maybe a -> TokenMap (Token e a) -> PVal1 q e a

  Parser for simple values based on regular expressions.

Totality: total
Visibility: export