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 : (bufSize_ : Nat) -> ByteString -> IBuffer bufSize_ -> Nat -> Nat -> Ref q (LTENat bufSize_) -> Ref q (LTENat bufSize_) -> 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:

.bufSize_ : Stack e a r q -> Nat

.curOffset_ : Stack e a r q -> Nat

.cur_ : ({rec:0} : Stack e a r q) -> IBuffer (bufSize_ {rec:0})

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

.from_ : ({rec:0} : Stack e a r q) -> Ref q (LTENat (bufSize_ {rec:0}))

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

.prevOffset_ : Stack e a r q -> Nat

.prev_ : Stack e a r q -> ByteString

.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)

.till_ : ({rec:0} : Stack e a r q) -> Ref q (LTENat (bufSize_ {rec:0}))

Hints:

HasBBErr (Stack e a r) e

HasBytes (Stack e a r)

HasStack (Stack e a r) a

HasStringLits (Stack e a r)

.bufSize_ : Stack e a r q -> Nat

Totality: total
Visibility: public export

bufSize_ : Stack e a r q -> Nat

Totality: total
Visibility: public export

.prev_ : Stack e a r q -> ByteString

Totality: total
Visibility: public export

prev_ : Stack e a r q -> ByteString

Totality: total
Visibility: public export

.cur_ : ({rec:0} : Stack e a r q) -> IBuffer (bufSize_ {rec:0})

Totality: total
Visibility: public export

cur_ : ({rec:0} : Stack e a r q) -> IBuffer (bufSize_ {rec:0})

Totality: total
Visibility: public export

.prevOffset_ : Stack e a r q -> Nat

Totality: total
Visibility: public export

prevOffset_ : Stack e a r q -> Nat

Totality: total
Visibility: public export

.curOffset_ : Stack e a r q -> Nat

Totality: total
Visibility: public export

curOffset_ : Stack e a r q -> Nat

Totality: total
Visibility: public export

.from_ : ({rec:0} : Stack e a r q) -> Ref q (LTENat (bufSize_ {rec:0}))

Totality: total
Visibility: public export

from_ : ({rec:0} : Stack e a r q) -> Ref q (LTENat (bufSize_ {rec:0}))

Totality: total
Visibility: public export

.till_ : ({rec:0} : Stack e a r q) -> Ref q (LTENat (bufSize_ {rec:0}))

Totality: total
Visibility: public export

till_ : ({rec:0} : Stack e a r q) -> Ref q (LTENat (bufSize_ {rec:0}))

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 -> (n : Nat) -> IBuffer n -> 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