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:
  
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
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:
  
Eq ByteBounds
  
Eq ByteBounds
  
Interpolation ByteBounds
  
Interpolation ByteBounds
  
Monoid ByteBounds
  
Monoid ByteBounds
  
Semigroup ByteBounds
  
Semigroup ByteBounds
  
Show ByteBounds
  
Show ByteBounds
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
  
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
prettyBBErr : Interpolation e => BBErr e -> String
  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