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

Projections:

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

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

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

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

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

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

HasBytes (Stack e a r)

HasError (Stack e a r) e

HasPosition (Stack e a r)

HasStack (Stack e a r) a

HasStringLits (Stack e a r)

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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

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

data Tok : Type -> Type -> Type

  Description of lexicographic tokens
  
  These are used to convert a lexer state to a token (or an error)
  of the appropriate type. Every lexer state corresponds to exactly
  one convertion. Typically, most lexer states are non-terminal
  states, so they correspond to `Bottom`.

Totality: total
Visibility: public export
Constructors:

Ignore : Tok 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 -> Tok e a

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

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

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

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

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

const : a -> Tok e a

Totality: total
Visibility: export

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

Totality: total
Visibility: export

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

Totality: total
Visibility: export

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

Totality: total
Visibility: public export

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

  Parser for simple values based on regular expressions.

Totality: total
Visibility: export

lexPushNL : s q => HasPosition s => HasStack s (SnocList (Bounded a)) => {auto 0 _ : 0 < r} -> Nat -> a -> F1 q (Index r)

Totality: total
Visibility: export

lexPush : s q => HasPosition s => HasStack s (SnocList (Bounded a)) => {auto 0 _ : 0 < r} -> Nat -> a -> F1 q (Index r)

Totality: total
Visibility: export

ctok : (x : RExpOf True b) -> HasPosition s => HasStack s (SnocList (Bounded a)) => {auto 0 _ : 0 < r} -> {auto 0 _ : ConstSize n x} -> a -> (RExpOf True b, Step q r s)

  Recognizes the given character and uses it to update the parser state
  as specified by `f`.
  
  The current column is increased by one *after* invoking `f`.

Totality: total
Visibility: export

readTok : RExpOf True b -> HasPosition s => HasStack s (SnocList (Bounded a)) => {auto 0 _ : 0 < r} -> HasBytes s => (String -> a) -> (RExpOf True b, Step q r s)

Totality: total
Visibility: export

convTok : RExpOf True b -> HasPosition s => HasStack s (SnocList (Bounded a)) => {auto 0 _ : 0 < r} -> HasBytes s => (ByteString -> a) -> (RExpOf True b, Step q r s)

Totality: total
Visibility: export

nltok : RExpOf True b -> HasPosition s => HasStack s (SnocList (Bounded a)) => {auto 0 _ : 0 < r} -> HasBytes s => a -> (RExpOf True b, Step q r s)

Totality: total
Visibility: export

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

Totality: total
Visibility: export

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

Totality: total
Visibility: public export

0 Lexer : Type -> Type -> Type

Totality: total
Visibility: public export

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

Totality: total
Visibility: export