Text.ILex.Interfaces

Definitions

interface HasBBErr : (Type -> Type) -> Type -> Type

  An interface for mutable parser stacks `s` that allow us to
  register custom errors, which will then be raised during parsing.

Parameters: s, e
Constructor: 

MkBE

Methods:

error : s q -> Ref q (Maybe (BBErr e))

Implementation: 

HasBBErr (DState s e) e

error : HasBBErr s e => s q -> Ref q (Maybe (BBErr e))

Totality: total
Visibility: public export

interface HasStringLits : (Type -> Type) -> Type

  An interface for mutable parser stacks `s` that facilitates
  parsing string tokens containing escape sequences.

Parameters: s
Constructor: 

MkHSL

Methods:

strings : s q -> Ref q (SnocList String)

Implementation: 

HasStringLits (DState s e)

strings : HasStringLits s => s q -> Ref q (SnocList String)

Totality: total
Visibility: public export

interface HasStack : (Type -> Type) -> Type -> Type

  An interface for mutable parser stacks `s` that facilitates
  parsing string tokens containing escape sequences.

Parameters: s, a
Constructor: 

MkHS

Methods:

stack : s q -> Ref q a

Implementation: 

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

stack : HasStack s a => s q -> Ref q a

Totality: total
Visibility: public export

go : a -> (s q => F1 q (Index r)) -> (a, Step q r s)

Totality: total
Visibility: export

ign : a -> (a, Step q r s)

Totality: total
Visibility: export

goBS : HasBytes s => a -> (s q => ByteString -> F1 q (Index r)) -> (a, Step q r s)

Totality: total
Visibility: export

goStr : HasBytes s => a -> (s q => String -> F1 q (Index r)) -> (a, Step q r s)

Totality: total
Visibility: export

writeAs : Ref q a -> a -> r -> F1 q r

  Writes a mutable reference and returns the given result.

Totality: total
Visibility: export

push1 : Ref q (SnocList a) -> a -> F1' q

  Appends a value to mutable reference of a snoclist.

Totality: total
Visibility: export

pop1 : Ref q (SnocList a) -> F1' q

  Drops and discards a the last entry from a snoclist
  stored in a mutable reference.

Totality: total
Visibility: export

replace1 : Ref q a -> a -> F1 q a

  Returns the value stored in a mutable reference and
  overwrites it with the given replacement.

Totality: total
Visibility: export

getList : Ref q (SnocList a) -> F1 q (List a)

  Empties a mutable reference holding a snoclist and returns
  the corresponding list.

Totality: total
Visibility: export

pushStack : HasStack s (SnocList a) => s q => a -> F1' q

  Appends a value to some mutable state implementing `HasStack`.

Totality: total
Visibility: export

pushStackAs : HasStack s (SnocList a) => s q => a -> v -> F1 q v

  Like `pushStack` but returns the given result.

Totality: total
Visibility: export

countdown : Ref q Nat -> a -> a -> F1 q a

  A small utility for counting down a parser and returning one
  of two possible outcomes.

Totality: total
Visibility: export

countdownAct : Ref q Nat -> F1 q a -> F1 q a -> F1 q a

  A small utility for counting down a parser and returning one
  of two possible actions.

Totality: total
Visibility: export

getStr : s q => HasStringLits s => F1 q String

  Empties the `strings` field of some mutable state implementing
  `HasStringLits` and returns the concatenated string literal.

Totality: total
Visibility: export

pushStr' : s q => HasStringLits s => String -> F1' q

  Appends the given string to the `strings` field of some mutable
  state implementing `HasStringLits`.

Totality: total
Visibility: export

pushStr : s q => HasStringLits s => Cast t (Index r) => t -> String -> F1 q (Index r)

  Appends the given string to the `strings` field of some mutable
  state implementing `HasStringLits` and returns the given result.

Totality: total
Visibility: export

pushChar : s q => HasStringLits s => Cast t (Index r) => t -> Char -> F1 q (Index r)

  Appends the given character to the `strings` field of some mutable
  state implementing `HasStringLits` and returns the given result.

Totality: total
Visibility: export

pushBits32 : s q => HasStringLits s => Cast t (Index r) => t -> Bits32 -> F1 q (Index r)

  Appends the given unicode code point to the `strings` field of some mutable
  state implementing `HasStringLits` and returns the given result.

Totality: total
Visibility: export

startPos : s q => HasBytes s => F1 q BytePos

  Gets the absolute position of the
  first byte of the current token.

Totality: total
Visibility: export

endPos : s q => HasBytes s => F1 q BytePos

  Gets the absolute position of the last byte of the current token.

Totality: total
Visibility: export

bounds : s q => HasBytes s => F1 q ByteBounds

  Gets the bounds of the current token.

Totality: total
Visibility: export

bounded : s q => HasBytes s => F1 q a -> F1 q (ByteBounded a)

  Computes the given value and pairs it with the token bounds.

Totality: total
Visibility: export

bounded' : s q => HasBytes s => a -> F1 q (ByteBounded a)

  Pairs the given value with the token bounds.

Totality: total
Visibility: export

pushPosition : s q => HasBytes s => F1' q

  Pushes the current byte position onto the position stack.
  
  This is often used when ecountering some "opening token"
  (such as an opening quote or parenthesis) for which we later
  expect a suitable closing token. If no closing token is encountered,
  we typically want to fail with an error that lists the position
  of the unclosed token.

Totality: total
Visibility: export

popPosition : s q => HasBytes s => F1' q

  Discards the latest entry from the positions stack.

Totality: total
Visibility: export

closeBounds : s q => HasBytes s => F1 q ByteBounds

  Returns the bounds from start to end of some "enclosed" or
  quoted region of text such as an expression in parantheses
  or some text in quotes.

Totality: total
Visibility: export

getStack : HasStack s a => s q => F1 q a

  Returns the content of some mutable state implementing
  `HasStack`.

Totality: total
Visibility: export

putStack : HasStack s a => s q => a -> F1' q

  Overwrites the content of some mutable state implementing
  `HasStack`.

Totality: total
Visibility: export

putStackAs : HasStack s a => s q => a -> v -> F1 q v

  Like `putStack` but returns the given result.

Totality: total
Visibility: export

putStackAsC : HasStack s a => s q => Cast b v => a -> b -> F1 q v

  Like `putStack` but returns the given result.

Totality: total
Visibility: export

withStack : HasStack s a => s q => (a -> F1 q b) -> F1 q b

Totality: total
Visibility: export

boundsWithStack : HasStack s a => s q => HasBytes s => (ByteBounds -> a -> F1 q b) -> F1 q b

Totality: total
Visibility: export

posWithStack : HasStack s a => s q => HasBytes s => (BytePos -> a -> F1 q b) -> F1 q b

Totality: total
Visibility: export

boundedWithStack : HasStack s a => s q => HasBytes s => (ByteBounded x -> a -> F1 q b) -> x -> F1 q b

Totality: total
Visibility: export

modStackAs : (0 s : (Type -> Type)) -> HasStack s a => s q => (a -> a) -> v -> F1 q v

  Reads and updates the stack.

Totality: total
Visibility: export

posModStack : (0 s : (Type -> Type)) -> HasBytes s => HasStack s a => s q => (a -> BytePos -> a) -> v -> F1 q v

Totality: total
Visibility: export

ifNoErrorRaised : HasBBErr s e => s q => F1 q (BBErr e) -> F1 q (BBErr e)

Totality: total
Visibility: export

unexpectedErr : HasBBErr s e => s q => HasBytes s => List String -> F1 q (InnerError e)

Totality: total
Visibility: export

unclosedErr : HasBBErr s e => s q => HasBytes s => String -> F1 q (BBErr e)

Totality: total
Visibility: export

unclosedIfEOIErr : HasBBErr s e => s q => HasBytes s => String -> List String -> F1 q (BBErr e)

  Fails with `unclosed` if this is the end of input, otherwise
  invokes `unexpected`.

Totality: total
Visibility: export

unclosedIfNLorEOIErr : HasBBErr s e => s q => HasBytes s => String -> List String -> F1 q (BBErr e)

  Fails with `unclosed` if this is the end of input or
  a linefeed character (`\n`, byte `0x0a`) was encountered,
  otherwise, invokes `unexpected`.

Totality: total
Visibility: export

failWith : HasBBErr s e => s q => BBErr e -> v -> F1 q v

  Writes the given exception to the `error` field of some
  mutable state and returns the given result.
  
  If another error occurred already (the content of `error sk` is
  not `Nothing`), the previous error will take precedence and will
  not be replaced.

Totality: total
Visibility: export

failHere : HasBBErr s e => s q => HasBytes s => InnerError e -> v -> F1 q v

  Like `failWith`, but generates the bounds of the error from the
  current position and the bytes read until the error occurred.

Totality: total
Visibility: export

failUnexpected : HasBBErr s e => s q => HasBytes s => List String -> v -> F1 q v

Totality: total
Visibility: export

failUnclosed : HasBBErr s e => s q => HasBytes s => String -> v -> F1 q v

Totality: total
Visibility: export

failUnclosedIfEOI : HasBBErr s e => s q => HasBytes s => String -> List String -> v -> F1 q v

Totality: total
Visibility: export

ignore : HasBytes s => a -> (a, Step q r s)

Totality: total
Visibility: export

step : HasBytes s => a -> (s q => F1 q (Index r)) -> (a, Step q r s)

Totality: total
Visibility: export

step' : HasBytes s => a -> Cast t (Index r) => t -> (a, Step q r s)

Totality: total
Visibility: export

bytes : HasBytes s => a -> (s q => ByteString -> F1 q (Index r)) -> (a, Step q r s)

Totality: total
Visibility: export

string : HasBytes s => a -> (s q => String -> F1 q (Index r)) -> (a, Step q r s)

Totality: total
Visibility: export

opn : HasBytes s => a -> (s q => F1 q (Index r)) -> (a, Step q r s)

  Recognizes the given character(s)
  and uses it to update the parser state
  as specified by `f`.
  
  The current column is increased by one, and a new entry is pushed onto
  the stack of bounds.

Totality: total
Visibility: export

opn' : HasBytes s => a -> Cast t (Index r) => t -> (a, Step q r s)

  Convenience alias for `copen . pure`.

Totality: total
Visibility: export

close : HasBytes s => a -> (s q => F1 q (Index r)) -> (a, Step q r s)

  Recognizes the given character(s) and uses it to update the parser state
  as specified by `f`.
  
  The current column is increased by `n`, and one `Position` entry
  is popped from the stack.

Totality: total
Visibility: export

closeStr : HasBytes s => a -> HasStringLits s => (s q => String -> F1 q (Index r)) -> (a, Step q r s)

  Recognizes the given character(s) and uses it to
  finalize and assemble a string literal.
  
  The current column is increased by `n`, and one `Position` entry
  is popped from the stack.

Totality: total
Visibility: export

closeWithBounds : HasBytes s => a -> (s q => ByteBounds -> F1 q (Index r)) -> (a, Step q r s)

  Recognizes the given character(s) and uses it to update the parser state
  as specified by `f`.
  
  The current column is increased by one, and on `Bounds` entry
  is popped from the stack.

Totality: total
Visibility: export

closeBoundedStr : HasBytes s => a -> HasStringLits s => (s q => ByteBounded String -> F1 q (Index r)) -> (a, Step q r s)

  Recognizes the given character(s) and uses it to
  finalize and assemble a string literal.
  
  The current column is increased by `n`, and one `Position` entry
  is popped from the stack.

Totality: total
Visibility: export

val : HasBytes s => (a -> String) -> (a -> Step1 q r s) -> a -> Maybe (RExp True, Step q r s)

  Lexes a single value based on its printed form. Returns
  `Nothing` in case `display` returns the empty string.
  
  For instance, `val show soSomething True` would recognice
  the token `"True"` and invoke act with `True`.

Totality: total
Visibility: export

valN : HasBytes s => (a -> List String) -> (a -> Step1 q r s) -> a -> List (RExp True, Step q r s)

  Like `val` but for a value that can be displayed in
  different ways.

Totality: total
Visibility: export

writeVal : HasBytes s => (a -> String) -> (s q -> Ref q a) -> Index r -> a -> Maybe (RExp True, Step q r s)

  Specialized version of `val` that writes the lexed value
  to a predefined mutable field of the parser stack.

Totality: total
Visibility: export

writeValN : HasBytes s => (a -> List String) -> (s q -> Ref q a) -> Index r -> a -> List (RExp True, Step q r s)

  Specialized version of `valN` that writes the lexed value
  to a predefined mutable field of the parser stack.

Totality: total
Visibility: export

vals : HasBytes s => (a -> String) -> (a -> Step1 q r s) -> List a -> List (RExp True, Step q r s)

  Applies `val` to a list of values.
  
  Highly useful in combination with the `Finite` interface from
  the idris2-finite library.

Totality: total
Visibility: export

valsN : HasBytes s => (a -> List String) -> (a -> Step1 q r s) -> List a -> List (RExp True, Step q r s)

  Like `vals` but for values that can be displayed in
  several ways.
  
  Highly useful in combination with the `Finite` interface from
  the idris2-finite library.

Totality: total
Visibility: export

writeVals : HasBytes s => (a -> String) -> (s q -> Ref q a) -> Index r -> List a -> List (RExp True, Step q r s)

  Specialized version of `vals` that writes the lexed value
  to a predefined mutable field of the parser stack.

Totality: total
Visibility: export

writeValsN : HasBytes s => (a -> List String) -> (s q -> Ref q a) -> Index r -> List a -> List (RExp True, Step q r s)

  Specialized version of `valsN` that writes the lexed value
  to a predefined mutable field of the parser stack.

Totality: total
Visibility: export

jsonSpace : RExp True

Totality: total
Visibility: export

jsonSpaces : RExp True

Totality: total
Visibility: export

jsonSpaced : HasBytes s => Steps q r s -> Steps q r s

Totality: total
Visibility: export

raise : HasBBErr s e => HasBytes s => InnerError e -> Nat -> s q => v -> F1 q v

Totality: total
Visibility: export

unexpected : HasBBErr s e => HasBytes s => List String -> s q -> F1 q (BBErr e)

Totality: total
Visibility: export

unclosed : HasBBErr s e => HasBytes s => String -> s q -> F1 q (BBErr e)

Totality: total
Visibility: export

unclosedIfEOI : HasBBErr s e => HasBytes s => String -> List String -> s q -> F1 q (BBErr e)

  Fails with `unclosed` if this is the end of input, otherwise
  invokes `unexpected`.

Totality: total
Visibility: export

unclosedIfNLorEOI : HasBBErr s e => HasBytes s => String -> List String -> s q -> F1 q (BBErr e)

  Fails with `unclosed` if this is the end of input or
  a linefeed character (`\n`, byte `0x0a`) was encountered,
  otherwise, invokes `unexpected`.

Totality: total
Visibility: export

errs : HasBBErr s e => HasBytes s => List (Entry n (s q -> F1 q (BBErr e))) -> Arr32 n (s q -> F1 q (BBErr e))

Totality: total
Visibility: export

noChunk : s -> F1 q (Maybe a)

  Never emits a chunk of values during streaming.
  
  This is for parsers that produce a single value after consuming the
  whole input. Such a parser can still be used with the facilities
  from ilex-streams but will only emit a single value at the end of input.
  In general, such a parser consumes a linear amount of memory and can
  typically not be used to process very large amounts of data.

Totality: total
Visibility: export

snocChunk : HasStack s (SnocList a) => s q -> F1 q (Maybe (List a))

  Extracts the values parsed so far from the parser stack
  and emits them during streaming.

Totality: total
Visibility: export