Text.ByteBounds

Reexports

Definitions

record BytePos : Type

  Position in a byte string or stream.

Totality: total
Visibility: public export
Constructor: 

BP : Nat -> BytePos

Projection: 

.pos : BytePos -> Nat

Hints:

Cast BytePos ByteBounds

Eq BytePos

Interpolation BytePos

Ord BytePos

Show BytePos

.pos : BytePos -> Nat

Totality: total
Visibility: public export

pos : BytePos -> Nat

Totality: total
Visibility: public export

incLen : Nat -> BytePos -> BytePos

  Increases the position by the given length
  of a byte sequence.

Totality: total
Visibility: export

endPos : Nat -> Nat -> BytePos

  Computes the end position of a token by reducing
  the start position of the next token by one
  (unless this is a zero-byte token corresponding to the
  end of input).

Totality: total
Visibility: export

offsetTo : BytePos -> BytePos -> BytePos

  Returns the offset of the second byte position relative to the first.

Totality: total
Visibility: export

data ByteBounds : Type

  A pair of `BytePos`s, describing a range in a byte stream, or `NoBB` for
  use - for instance - with programmatically created tokens.

Totality: total
Visibility: public export
Constructors:

BB : BytePos -> BytePos -> ByteBounds

NoBB : ByteBounds

Hints:

Cast BytePos ByteBounds

Eq ByteBounds

Interpolation ByteBounds

MapBounds ByteBounds

Monoid ByteBounds

Semigroup ByteBounds

Show ByteBounds

interface MapBounds : Type -> Type

Parameters: a
Methods:

mapBounds : (ByteBounds -> ByteBounds) -> a -> a

Implementations:

MapBounds ByteBounds

MapBounds a => MapBounds (Maybe a)

MapBounds a => MapBounds (List a)

MapBounds a => MapBounds (SnocList a)

MapBounds a => MapBounds b => MapBounds (a, b)

MapBounds a => MapBounds b => MapBounds (Either a b)

MapBounds (ByteBounded a)

MapBounds ByteContext

MapBounds (ByteError e)

mapBounds : MapBounds a => (ByteBounds -> ByteBounds) -> a -> a

Totality: total
Visibility: public export

clearBounds : MapBounds a => a -> a

Totality: total
Visibility: export

fromPos : Cast t ByteBounds => BytePos -> t -> ByteBounds

Totality: total
Visibility: export

tillPos : Cast t ByteBounds => t -> BytePos -> ByteBounds

Totality: total
Visibility: export

record ByteBounded : Type -> Type

  Pairs a value with the bounds in the byte stream from where it was parsed.

Totality: total
Visibility: public export
Constructor: 

B : ty -> ByteBounds -> ByteBounded ty

Projections:

.bounds : ByteBounded ty -> ByteBounds

.val : ByteBounded ty -> ty

Hints:

Applicative ByteBounded

Eq ty => Eq (ByteBounded ty)

Foldable ByteBounded

Functor ByteBounded

MapBounds (ByteBounded a)

Monad ByteBounded

Show ty => Show (ByteBounded ty)

Traversable ByteBounded

.val : ByteBounded ty -> ty

Totality: total
Visibility: public export

val : ByteBounded ty -> ty

Totality: total
Visibility: public export

.bounds : ByteBounded ty -> ByteBounds

Totality: total
Visibility: public export

bounds : ByteBounded ty -> ByteBounds

Totality: total
Visibility: public export

fromBytePos : ByteBounded a -> BytePos -> ByteBounded a

Totality: total
Visibility: export

record PositionMap : Type

Totality: total
Visibility: public export
Constructor: 

PM : (size : Nat) -> IArray size Position -> PositionMap

Projections:

.arr : ({rec:0} : PositionMap) -> IArray (size {rec:0}) Position

.size : PositionMap -> Nat

Hints:

Eq PositionMap

Show PositionMap

.size : PositionMap -> Nat

Totality: total
Visibility: public export

size : PositionMap -> Nat

Totality: total
Visibility: public export

.arr : ({rec:0} : PositionMap) -> IArray (size {rec:0}) Position

Totality: total
Visibility: public export

arr : ({rec:0} : PositionMap) -> IArray (size {rec:0}) Position

Totality: total
Visibility: public export

bytePositionMapFrom : Position -> ByteString -> PositionMap

Totality: total
Visibility: export

stringPositionMapFrom : Position -> String -> PositionMap

Totality: total
Visibility: export

bytePositionMap : ByteString -> PositionMap

Totality: total
Visibility: export

stringPositionMap : String -> PositionMap

Totality: total
Visibility: export

position : PositionMap => BytePos -> Maybe Position

Totality: total
Visibility: export

toBounds : PositionMap => ByteBounds -> Bounds

Totality: total
Visibility: export

toBounded : PositionMap => ByteBounded a -> Bounded a

Totality: total
Visibility: export

0 BBErr : Type -> Type

Totality: total
Visibility: public export

injectBBErr : Cast e f => ByteBounded e -> BBErr f

Totality: total
Visibility: export

toParseError : Origin -> String -> BBErr e -> ParseError e

  Converts an error with byte bounds to a `ParseError` by pairing it with
  an origin and the parsed string.

Totality: total
Visibility: export

record ByteContext : Type

Totality: total
Visibility: public export
Constructor: 

BC : Origin -> ByteBounds -> ByteContext

Projections:

.bounds : ByteContext -> ByteBounds

.origin : ByteContext -> Origin

Hints:

Eq ByteContext

Interpolation ByteContext

MapBounds ByteContext

Show ByteContext

.origin : ByteContext -> Origin

Totality: total
Visibility: public export

origin : ByteContext -> Origin

Totality: total
Visibility: public export

.bounds : ByteContext -> ByteBounds

Totality: total
Visibility: public export

bounds : ByteContext -> ByteBounds

Totality: total
Visibility: public export

record ByteError : Type -> Type

Totality: total
Visibility: public export
Constructor: 

BE : Origin -> ByteBounds -> Maybe ByteString -> e -> ByteError e

Projections:

.bounds : ByteError e -> ByteBounds

.content : ByteError e -> Maybe ByteString

.error : ByteError e -> e

.origin : ByteError e -> Origin

Hints:

Eq e => Eq (ByteError e)

Interpolation e => Interpolation (ByteError e)

MapBounds (ByteError e)

Show e => Show (ByteError e)

.origin : ByteError e -> Origin

Totality: total
Visibility: public export

origin : ByteError e -> Origin

Totality: total
Visibility: public export

.bounds : ByteError e -> ByteBounds

Totality: total
Visibility: public export

bounds : ByteError e -> ByteBounds

Totality: total
Visibility: public export

.content : ByteError e -> Maybe ByteString

Totality: total
Visibility: public export

content : ByteError e -> Maybe ByteString

Totality: total
Visibility: public export

.error : ByteError e -> e

Totality: total
Visibility: public export

error : ByteError e -> e

Totality: total
Visibility: public export

0 ByteErr : Type -> Type

Totality: total
Visibility: public export

byteError : Origin -> ByteBounded e -> ByteError e

Totality: total
Visibility: export

prettyByteErr : Interpolation e => ByteError e -> String

Totality: total
Visibility: export