Idris2Doc : Text.ByteBounds

Text.ByteBounds

(source)
Reexports
import public Text.Bounds
import public Text.FC
import public Text.ParseError
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
  
Cast BytePos ByteBounds
  
Eq BytePos
  
Eq BytePos
  
Interpolation BytePos
  
Interpolation BytePos
  
Ord BytePos
  
Ord BytePos
  
Show 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
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
  
Cast BytePos ByteBounds
  
Eq ByteBounds
  
Eq ByteBounds
  
Interpolation ByteBounds
  
Interpolation ByteBounds
  
MapBounds ByteBounds
  
MapBounds ByteBounds
  
Monoid ByteBounds
  
Monoid ByteBounds
  
Semigroup ByteBounds
  
Semigroup ByteBounds
  
Show 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 (ByteError e)
  
MapBounds ByteContext
  
MapBounds (ByteBounded a)
  
MapBounds a => MapBounds b => MapBounds (Either a b)
  
MapBounds a => MapBounds b => MapBounds (a, b)
  
MapBounds a => MapBounds (SnocList a)
  
MapBounds a => MapBounds (List a)
  
MapBounds a => MapBounds (Maybe a)
  
MapBounds ByteBounds
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
  
Applicative ByteBounded
  
Eq ty => Eq (ByteBounded ty)
  
Eq ty => Eq (ByteBounded ty)
  
Foldable ByteBounded
  
Foldable ByteBounded
  
Functor ByteBounded
  
Functor ByteBounded
  
MapBounds (ByteBounded a)
  
MapBounds (ByteBounded a)
  
Monad ByteBounded
  
Monad ByteBounded
  
Show ty => Show (ByteBounded ty)
  
Show ty => Show (ByteBounded ty)
  
Traversable ByteBounded
  
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
  
Eq PositionMap
  
Show 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
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
  
Eq ByteContext
  
Interpolation ByteContext
  
Interpolation ByteContext
  
MapBounds ByteContext
  
MapBounds ByteContext
  
Show 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)
  
Eq e => Eq (ByteError e)
  
Interpolation e => Interpolation (ByteError e)
  
Interpolation e => Interpolation (ByteError e)
  
MapBounds (ByteError e)
  
MapBounds (ByteError e)
  
Show e => Show (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