Text.ILex.Interfaces

Definitions

interface HasPosition : (Type -> Type) -> Type

  An interface for mutable parser stacks `s` that allows us to keep
  track of the current position (line and column) in the currently
  parsed string.

Parameters: s
Constructor: 

MkHP

Methods:

line : s q -> Ref q Nat

col : s q -> Ref q Nat

positions : s q -> Ref q (SnocList Position)

Implementation: 

HasPosition (DStack s e)

line : HasPosition s => s q -> Ref q Nat

Totality: total
Visibility: public export

col : HasPosition s => s q -> Ref q Nat

Totality: total
Visibility: public export

positions : HasPosition s => s q -> Ref q (SnocList Position)

Totality: total
Visibility: public export

interface HasError : (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: 

MkHE

Methods:

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

Implementation: 

HasError (DStack s e) e

error : HasError s e => s q -> Ref q (Maybe (BoundedErr 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 (DStack 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 (DStack 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

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

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 : Cast b v => HasStack s a => s q => a -> b -> F1 q v

  Like `putStack` but returns the given result.

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

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

getPosition : s q => HasPosition s => F1 q Position

  Gets the current text position (line and column) from some
  mutable state implementing `HasPosition`.

Totality: total
Visibility: export

inccol : s q => HasPosition s => Nat -> F1 q ()

  Increases the text column of some mutable state implementing
  `HasPosition` by the given amount.

Totality: total
Visibility: export

setcol : s q => HasPosition s => Nat -> F1 q ()

  Increases the text column of some mutable state implementing
  `HasPosition` by the given amount.

Totality: total
Visibility: export

incline : s q => HasPosition s => Nat -> F1 q ()

  Increases the line of some mutable state implementing
  `HasPosition` by the given amount. The column field is
  reset to zero.

Totality: total
Visibility: export

incML : s q => HasPosition s => ByteString -> F1 q ()

  Increases the current text position according to the characters
  encountered in the given byte string.
  
  See also `Text.ILex.Bounds.inBytes`.

Totality: total
Visibility: export

tokenBounds : s q => HasPosition s => Nat -> F1 q Bounds

  Gets the current token bounds from some
  mutable state implementing `HasPosition` after
  increasing the column by `n` characters.

Totality: total
Visibility: export

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

  Pushes the current text 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 => HasPosition s => F1' q

  Discards the latest entry from the positions stack.

Totality: total
Visibility: export

closeBounds : s q => HasPosition s => F1 q Bounds

  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

newline : HasPosition s => RExpOf True b -> (s q => F1 q (Index r)) -> (RExpOf True b, Step q r s)

  Recognizes the given expression and invokes `incline` before
  returning the given result.

Totality: total
Visibility: export

newline' : HasPosition s => Cast t (Index r) => RExpOf True b -> t -> (RExpOf True b, Step q r s)

  Convenience alias for `newline x (pure v)`.

Totality: total
Visibility: export

newlines : HasPosition s => Nat -> RExpOf True b -> (s q => F1 q (Index r)) -> (RExpOf True b, Step q r s)

  Recognizes the given expression and invokes `incline n` before
  returning the given result.

Totality: total
Visibility: export

newlines' : HasPosition s => Nat -> RExpOf True b -> Index r -> (RExpOf True b, Step q r s)

  Convenience alias for `newlines n x (pure v)`.

Totality: total
Visibility: export

linecol : HasPosition s => Nat -> Nat -> RExpOf True b -> (s q => F1 q (Index r)) -> (RExpOf True b, Step q r s)

  Recognizes the given expression, increasing the line count by the given
  number and setting the current column to the given value *after* invoming
  the given action.

Totality: total
Visibility: export

linecol' : HasPosition s => Nat -> Nat -> RExpOf True b -> Index r -> (RExpOf True b, Step q r s)

  Convenience alias for `linecol line col x (pure v)`.

Totality: total
Visibility: export

failWith : HasError s e => s q => BoundedErr e -> v -> F1 q v

  Writes the given exception to the `error` field of some
  mutable state and returns the given result.

Totality: total
Visibility: export

failHere : HasError s e => HasBytes s => HasPosition s => s q => 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

cexpr : (x : RExpOf True b) -> {auto 0 _ : ConstSize n x} -> HasPosition s => (s q => F1 q (Index r)) -> (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 `n` *before* invoking `f`.

Totality: total
Visibility: export

cexpr' : (x : RExpOf True b) -> {auto 0 _ : ConstSize n x} -> HasPosition s => Cast t (Index r) => t -> (RExpOf True b, Step q r s)

  Convenience alias for `cexpr . pure`.

Totality: total
Visibility: export

copen : (x : RExpOf True b) -> {auto 0 _ : ConstSize n x} -> HasPosition s => (s q => F1 q (Index r)) -> (RExpOf True b, 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

copen' : (x : RExpOf True b) -> {auto 0 _ : ConstSize n x} -> HasPosition s => Cast t (Index r) => t -> (RExpOf True b, Step q r s)

  Convenience alias for `copen . pure`.

Totality: total
Visibility: export

cclose : (x : RExpOf True b) -> {auto 0 _ : ConstSize n x} -> HasPosition s => (s q => F1 q (Index r)) -> (RExpOf True b, 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

ccloseStr : (x : RExpOf True b) -> {auto 0 _ : ConstSize n x} -> HasPosition s => HasStringLits s => (s q => String -> F1 q (Index r)) -> (RExpOf True b, 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

ccloseWithBounds : (x : RExpOf True b) -> {auto 0 _ : ConstSize n x} -> HasPosition s => (s q => Bounds -> F1 q (Index r)) -> (RExpOf True b, 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

ccloseBoundedStr : (x : RExpOf True b) -> {auto 0 _ : ConstSize n x} -> HasPosition s => HasStringLits s => (s q => Bounded String -> F1 q (Index r)) -> (RExpOf True b, 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 : HasPosition 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 : HasPosition 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 : HasPosition 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 : HasPosition 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 : HasPosition 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 : HasPosition 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 : HasPosition 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 : HasPosition 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

read : RExpOf True b -> HasPosition s => HasBytes s => (s q => String -> F1 q (Index r)) -> (RExpOf True b, Step q r s)

  Converts the recognized token to a `String`, increases the
  current column by its length and invokes the given state transformer.

Totality: total
Visibility: export

readline : RExpOf True b -> HasPosition s => HasBytes s => (s q => String -> F1 q (Index r)) -> (RExpOf True b, Step q r s)

  Increases the current line by one after invoking the given
  state transformer.

Totality: total
Visibility: export

read' : RExpOf True b -> HasPosition s => HasBytes s => Cast t (Index r) => t -> (RExpOf True b, Step q r s)

  Convenience alias for `read . pure`
  current column by its length after invoking the given state transformer.

Totality: total
Visibility: export

conv : RExpOf True b -> HasPosition s => HasBytes s => (s q => ByteString -> F1 q (Index r)) -> (RExpOf True b, Step q r s)

  Increases the current column by the length of the byte string
  and invokes the given state transformer.

Totality: total
Visibility: export

convline : RExpOf True b -> HasPosition s => HasBytes s => (s q => ByteString -> F1 q (Index r)) -> (RExpOf True b, Step q r s)

  Increases the current line by one after invoking the given
  state transformer.

Totality: total
Visibility: export

multiline : RExpOf True b -> HasPosition s => HasBytes s => (s q => ByteString -> F1 q (Index r)) -> (RExpOf True b, Step q r s)

  Like `conv` but can handle byte sequence with an unknown number
  of line feed characters.
  
  Note: In performance critical parsers, this should be avoided whenever
        possible. Advancing token bounds by inspecting every byte a second
        time *can* have an impact. Whenever possible, try to separate your
        lexems into those which consist of no line breaks and those which
        consist of a predefine (typically only one) number of line breaks.

Totality: total
Visibility: export

conv' : RExpOf True b -> HasPosition s => HasBytes s => Cast t (Index r) => t -> (RExpOf True b, Step q r s)

  Convenience alias for `conv . pure`.

Totality: total
Visibility: export

multiline' : RExpOf True b -> HasPosition s => HasBytes s => Index r -> (RExpOf True b, Step q r s)

  Convenience alias for `convML . pure`.
  
  Please not, that the same performance considerations as for `convML`
  apply.

Totality: total
Visibility: export

jsonSpaced : HasPosition s => HasBytes s => Cast b (Index r) => b -> Steps q r s -> Steps q r s

Totality: total
Visibility: export

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

Totality: total
Visibility: export

unexpected : HasError s e => HasPosition s => HasBytes s => List String -> s q -> F1 q (BoundedErr e)

Totality: total
Visibility: export

unclosed : HasError s e => HasPosition s => HasBytes s => String -> s q -> F1 q (BoundedErr e)

Totality: total
Visibility: export

unclosedIfEOI : HasError s e => HasPosition s => HasBytes s => String -> List String -> s q -> F1 q (BoundedErr e)

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

Totality: total
Visibility: export

unclosedIfNLorEOI : HasError s e => HasPosition s => HasBytes s => String -> List String -> s q -> F1 q (BoundedErr 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 : HasError s e => HasPosition s => HasBytes s => List (Entry n (s q -> F1 q (BoundedErr e))) -> Arr32 n (s q -> F1 q (BoundedErr 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