Idris2Doc : Data.ByteVect

Data.ByteVect

(source)
Reexports
import public Data.Buffer.Core
import public Data.Buffer.Indexed
import public Data.Byte
Definitions
data ByteVect : Nat -> Type
  An immutable, length-indexed byte vector.
  
  Internally represented by a `Data.Buffer` together
  with its length and offset.
  
  The internal buffer is treated as being immutable,
  so operations modifying a `ByteVect` will create
  and write to a new `Buffer`.

  Totality: total
  Visibility: public export
  Constructor: 
BV : IBuffer bufLen -> (offset : Nat) -> (0 _ : LTE (offset + len) bufLen) -> ByteVect len

  Hints:
  
Cast (ByteVect n) ByteString
  
Cast (ByteVect n) ByteString
  
Eq (ByteVect n)
  
Interpolation (ByteVect n)
  
Ord (ByteVect n)
  
Show (ByteVect n)
fromIBuffer : IBuffer n -> ByteVect n
  Wrappes an immutable buffer in a `ByteVect`

  Totality: total
  Visibility: export
toIBuffer : ByteVect n -> IBuffer n
  Converts a `ByteVect n` to an `IBuffer n`.
  
  In case the `ByteVect`'s inner offset is at zero, this just
  unwraps and returns then inner buffer (O(1)), otherwise the buffer's
  substring is copied to a new buffer (O(n)).

  Totality: total
  Visibility: export
record ByteString : Type
  An immutable string of raw bytes. For an length-indexed version,
  see module `ByteVect` and `Data.ByteVect`.

  Totality: total
  Visibility: public export
  Constructor: 
BS : (size : Nat) -> ByteVect size -> ByteString

  Projections:
  
.repr : ({rec:0} : ByteString) -> ByteVect (size {rec:0})
  
.size : ByteString -> Nat

  Hints:
  
Cast String ByteString
  
Cast (List Bits8) ByteString
  
Cast Bits8 ByteString
  
Cast Char ByteString
  
Cast (ByteVect n) ByteString
  
Cast (IBuffer n) ByteString
  
Cast AnyBuffer ByteString
  
Cast AnyBuffer ByteString
  
Cast (IBuffer n) ByteString
  
Cast (ByteVect n) ByteString
  
Cast Char ByteString
  
Cast Bits8 ByteString
  
Cast (List Bits8) ByteString
  
Cast String ByteString
  
Eq ByteString
  
Eq ByteString
  
FromString ByteString
  
FromString ByteString
  
Interpolation ByteString
  
Interpolation ByteString
  
Monoid ByteString
  
Monoid ByteString
  
Ord ByteString
  
Ord ByteString
  
Semigroup ByteString
  
Semigroup ByteString
  
Show ByteString
  
Show ByteString
.size : ByteString -> Nat
  Totality: total
  Visibility: public export
size : ByteString -> Nat
  Totality: total
  Visibility: public export
.repr : ({rec:0} : ByteString) -> ByteVect (size {rec:0})
  Totality: total
  Visibility: public export
repr : ({rec:0} : ByteString) -> ByteVect (size {rec:0})
  Totality: total
  Visibility: public export
freezeByteString : WithMBuffer n ByteString
  Safely wrap a mutable buffer in a `ByteString`.

  Totality: total
  Visibility: export
unsafeFreezeByteString : WithMBuffer n ByteString
  Wrap a mutable buffer in a `ByteString` without copying.
  
  Use this for reasons of efficiency when you are sure the buffer
  will not be shared otherwise.

  Totality: total
  Visibility: export
freezeByteStringLTE : (m : Nat) -> {auto 0 _ : LTE m n} -> WithMBuffer n ByteString
  Safely wrap a mutable buffer in a `ByteString`.

  Totality: total
  Visibility: export
unsafeFreezeByteStringLTE : (m : Nat) -> {auto 0 _ : LTE m n} -> WithMBuffer n ByteString
  Wrap a mutable buffer in a `ByteString` without copying.
  
  Use this for reasons of efficiency when you are sure the buffer
  will not be shared otherwise.

  Totality: total
  Visibility: export
at : ByteVect n -> Fin n -> Bits8
  Reads the value of a `ByteVect` at the given position

  Totality: total
  Visibility: export
ix : ByteVect n -> (0 m : Nat) -> Ix (S m) n => Bits8
  Safely access a value in an array at position `n - m`.

  Totality: total
  Visibility: export
atNat : ByteVect n -> (m : Nat) -> {auto 0 _ : LT m n} -> Bits8
  Safely access a value in an array at the given position.

  Totality: total
  Visibility: export
fromEnd : ByteVect n -> (m : Nat) -> {auto 0 _ : LT m n} -> Bits8
  Totality: total
  Visibility: export
empty : ByteVect 0
  The empty `ByteVect`.

  Totality: total
  Visibility: export
pack : (as : List Bits8) -> ByteVect (length as)
  Converts a list of values to a `ByteVect` using
  the given conversion function. O(n).

  Totality: total
  Visibility: export
fromString : (s : String) -> ByteVect (cast (stringByteLength s))
  Converts a `String` to a `ByteVect`. Note: This will
  correctly decode the corresponding UTF-8 string.

  Totality: total
  Visibility: export
toString : ByteVect n -> String
  Converts a `ByteVect` to a UTF-8 encoded string

  Totality: total
  Visibility: export
singleton : Bits8 -> ByteVect 1
  Creates a `ByteVect` holding a single `Bits8` value.

  Totality: total
  Visibility: export
toList : (Bits8 -> a) -> ByteVect n -> List a
  Convert a `ByteVect` to a list of values using
  the given conversion function.

  Totality: total
  Visibility: export
unpack : ByteVect n -> List Bits8
  Converts a `ByteVect` to a list of `Bits8` values. O(n).

  Totality: total
  Visibility: export
hcomp : ByteVect m -> ByteVect n -> Ordering
  Lexicographic comparison of `ByteVect`s of distinct length

  Totality: total
  Visibility: export
heq : ByteVect m -> ByteVect n -> Bool
  Heterogeneous equality for `ByteVect`s

  Totality: total
  Visibility: export
generate : (n : Nat) -> (Fin n -> Bits8) -> ByteVect n
  Totality: total
  Visibility: export
replicate : (n : Nat) -> Bits8 -> ByteVect n
  Totality: total
  Visibility: export
append : ByteVect m -> ByteVect n -> ByteVect (m + n)
  Concatenate two `ByteVect`s. O(n + m).

  Totality: total
  Visibility: export
cons : Bits8 -> ByteVect n -> ByteVect (S n)
  Prepend a single `Bits8` to a `ByteVect`. O(n).

  Totality: total
  Visibility: export
snoc : Bits8 -> ByteVect n -> ByteVect (n + 1)
  Append a single `Bits8` to a `ByteVect`. O(n).

  Totality: total
  Visibility: export
head : ByteVect (S n) -> Bits8
  Read the first element of a `ByteVect`. O(1).

  Totality: total
  Visibility: export
tail : ByteVect (S n) -> ByteVect n
  Drop the first `Bits8` from a `ByteVect`. O(1).

  Totality: total
  Visibility: export
uncons : ByteVect (S n) -> (Bits8, ByteVect n)
  Split the first `Bits8` from a `ByteVect`. O(1).

  Totality: total
  Visibility: export
last : ByteVect (S n) -> Bits8
  Read the last `Bits8` from a `ByteVect`. O(1).

  Totality: total
  Visibility: export
init : ByteVect (S n) -> ByteVect n
  Drop the last `Bits8` from a `ByteVect`. O(1).

  Totality: total
  Visibility: export
unsnoc : ByteVect (S n) -> (Bits8, ByteVect n)
  Split a `ByteVect` at the last byte. O(1).

  Totality: total
  Visibility: export
map : (Bits8 -> Bits8) -> ByteVect n -> ByteVect n
  Converts every `Bits8` in a `ByteVect` by applying the given
  function. O(n).

  Totality: total
  Visibility: export
toUpper : ByteVect n -> ByteVect n
  Interpreting the values stored in a `ByteVect` as 8 bit characters,
  convert every lower-case character to its upper-case form. O(n)

  Totality: total
  Visibility: export
toLower : ByteVect n -> ByteVect n
  Interpreting the values stored in a `ByteVect` as 8 bit characters,
  convert every upper-case character to its lower-case form. O(n)

  Totality: total
  Visibility: export
reverse : ByteVect n -> ByteVect n
  Inverse the order of bytes in a `ByteVect`. O(n)

  Totality: total
  Visibility: export
all : (Bits8 -> Bool) -> ByteVect n -> Bool
  True, if the predicate holds for all bytes
  in the given `ByteVect`. O(n)

  Totality: total
  Visibility: export
any : (Bits8 -> Bool) -> ByteVect n -> Bool
  True, if the predicate holds for at least one byte
  in the given `ByteVect`. O(n)

  Totality: total
  Visibility: export
elem : Bits8 -> ByteVect n -> Bool
  True, if the given `Bits8` appears in the `ByteVect`. O(n)

  Totality: total
  Visibility: export
foldl : (a -> Bits8 -> a) -> a -> ByteVect n -> a
  Fold a `ByteVect` from the left. O(n)

  Totality: total
  Visibility: export
foldr : (Bits8 -> a -> a) -> a -> ByteVect n -> a
  Fold a `ByteVect` from the right. O(n)

  Totality: total
  Visibility: export
findIndex : (Bits8 -> Bool) -> ByteVect n -> Maybe (Fin n)
  The `findIndex` function takes a predicate and a `ByteVect` and
  returns the index of the first element in the ByteVect
  satisfying the predicate. O(n)

  Totality: total
  Visibility: export
elemIndex : Bits8 -> ByteVect n -> Maybe (Fin n)
  Return the index of the first occurence of the given
  byte in the `ByteVect`, or `Nothing`, if the byte
  does not appear in the ByteVect. O(n)

  Totality: total
  Visibility: export
find : (Bits8 -> Bool) -> ByteVect n -> Maybe Bits8
  Returns the first value byte in a `ByteVect` fulfilling
  the given predicate. O(n)

  Totality: total
  Visibility: export
isPrefixOf : ByteVect m -> ByteVect n -> Bool
  Totality: total
  Visibility: export
isSuffixOf : ByteVect m -> ByteVect n -> Bool
  Totality: total
  Visibility: export
substring : (start : Nat) -> (length : Nat) -> ByteVect n -> {auto 0 _ : LTE (start + length) n} -> ByteVect length
  Like `substr` for `String`, this extracts a substring
  of the given `ByteVect` at the given start position
  and of the given length. O(1).

  Totality: total
  Visibility: export
substringFromTill : (from : Nat) -> (till : Nat) -> {auto 0 _ : LTE from till} -> {auto 0 _ : LTE till n} -> ByteVect n -> ByteVect (minus till from)
  Like `substring` but extracts a substring from position
  `from` up to but not including position `till`.

  Totality: total
  Visibility: export
substringFromTo : (from : Nat) -> (to : Nat) -> {auto 0 _ : LTE from to} -> {auto 0 _ : LT to n} -> ByteVect n -> ByteVect (minus (S to) from)
  Like `substring` but extracts a substring from position
  `from` up to and including position `to`.

  Totality: total
  Visibility: export
generateMaybe : (n : Nat) -> (Fin n -> Maybe Bits8) -> ByteString
  Totality: total
  Visibility: export
mapMaybe : (Bits8 -> Maybe Bits8) -> ByteVect n -> ByteString
  Totality: total
  Visibility: export
filter : (Bits8 -> Bool) -> ByteVect n -> ByteString
  Totality: total
  Visibility: export
take : (0 k : Nat) -> {auto 0 _ : LTE k n} -> ByteVect n -> ByteVect k
  Return a `ByteVect` with the first `n` values of
  the input string. O(1)

  Totality: total
  Visibility: export
takeEnd : (k : Nat) -> {auto 0 _ : LTE k n} -> ByteVect n -> ByteVect k
  Return a `ByteVect` with the last `n` values of
  the input string. O(1)

  Totality: total
  Visibility: export
drop : (k : Nat) -> {auto 0 _ : LTE k n} -> ByteVect n -> ByteVect (minus n k)
  Remove the first `n` values from a `ByteVect`. O(1)

  Totality: total
  Visibility: export
dropEnd : (0 k : Nat) -> {auto 0 _ : LTE k n} -> ByteVect n -> ByteVect (minus n k)
  Remove the last `n` values from a `ByteVect`. O(1)

  Totality: total
  Visibility: export
splitAt : (k : Nat) -> {auto 0 _ : LTE k n} -> ByteVect n -> (ByteVect k, ByteVect (minus n k))
  Totality: total
  Visibility: export
takeWhile : (Bits8 -> Bool) -> ByteVect n -> ByteString
  Extracts the longest prefix of elements satisfying the
  predicate.

  Totality: total
  Visibility: export
takeWhileEnd : (Bits8 -> Bool) -> ByteVect n -> ByteString
  Returns the longest (possibly empty) suffix of elements
  satisfying the predicate.

  Totality: total
  Visibility: export
dropWhile : (Bits8 -> Bool) -> ByteVect n -> ByteString
  Drops the longest (possibly empty) prefix of elements
  satisfying the predicate and returns the remainder.

  Totality: total
  Visibility: export
dropWhileEnd : (Bits8 -> Bool) -> ByteVect n -> ByteString
  Drops the longest (possibly empty) suffix of elements
  satisfying the predicate and returns the remainder.

  Totality: total
  Visibility: export
trimLeft : ByteVect n -> ByteString
  Remove leading whitespace from a `ByteString`

  Totality: total
  Visibility: export
trimRight : ByteVect n -> ByteString
  Remove trailing whitespace from a `ByteString`

  Totality: total
  Visibility: export
trim : ByteVect n -> ByteString
  Remove all leading and trailing whitespace from a `ByteString`

  Totality: total
  Visibility: export
record BreakRes : Nat -> Type
  Totality: total
  Visibility: public export
  Constructor: 
MkBreakRes : (lenFst : Nat) -> (lenSnd : Nat) -> ByteVect lenFst -> ByteVect lenSnd -> (0 _ : LTE (lenFst + lenSnd) n) -> BreakRes n

  Projections:
  
.fst : ({rec:0} : BreakRes n) -> ByteVect (lenFst {rec:0})
  
.lenFst : BreakRes n -> Nat
  
.lenSnd : BreakRes n -> Nat
  
0 .prf : ({rec:0} : BreakRes n) -> LTE (lenFst {rec:0} + lenSnd {rec:0}) n
  
.snd : ({rec:0} : BreakRes n) -> ByteVect (lenSnd {rec:0})
.lenFst : BreakRes n -> Nat
  Totality: total
  Visibility: public export
lenFst : BreakRes n -> Nat
  Totality: total
  Visibility: public export
.lenSnd : BreakRes n -> Nat
  Totality: total
  Visibility: public export
lenSnd : BreakRes n -> Nat
  Totality: total
  Visibility: public export
.fst : ({rec:0} : BreakRes n) -> ByteVect (lenFst {rec:0})
  Totality: total
  Visibility: public export
fst : ({rec:0} : BreakRes n) -> ByteVect (lenFst {rec:0})
  Totality: total
  Visibility: public export
.snd : ({rec:0} : BreakRes n) -> ByteVect (lenSnd {rec:0})
  Totality: total
  Visibility: public export
snd : ({rec:0} : BreakRes n) -> ByteVect (lenSnd {rec:0})
  Totality: total
  Visibility: public export
0 .prf : ({rec:0} : BreakRes n) -> LTE (lenFst {rec:0} + lenSnd {rec:0}) n
  Totality: total
  Visibility: public export
0 prf : ({rec:0} : BreakRes n) -> LTE (lenFst {rec:0} + lenSnd {rec:0}) n
  Totality: total
  Visibility: public export
breakRes : ByteVect n -> SubLength n -> BreakRes n
  Totality: total
  Visibility: export
break : (Bits8 -> Bool) -> ByteVect n -> BreakRes n
  Returns the longest (possibly empty) prefix of elements which do not
  satisfy the predicate and the remainder of the string.

  Totality: total
  Visibility: export
breakNL : ByteVect n -> BreakRes n
  Returns the longest (possibly empty) prefix before the first newline character

  Totality: total
  Visibility: export
breakEnd : (Bits8 -> Bool) -> ByteVect n -> BreakRes n
  Returns the longest (possibly empty) suffix of elements which do not
  satisfy the predicate and the remainder of the string.

  Totality: total
  Visibility: export
span : (Bits8 -> Bool) -> ByteVect n -> BreakRes n
  Returns the longest (possibly empty) prefix of elements
  satisfying the predicate and the remainder of the string.

  Totality: total
  Visibility: export
spanEnd : (Bits8 -> Bool) -> ByteVect n -> BreakRes n
  Returns the longest (possibly empty) suffix of elements
  satisfying the predicate and the remainder of the string.

  Totality: total
  Visibility: export
substringIndex : ByteVect k -> ByteVect n -> SubLength n
  Returns the index where the given substring occurs in the
  given bytevector for the first time

  Totality: total
  Visibility: export
breakAtSubstring : ByteVect k -> ByteVect n -> BreakRes n
  Returns the longest (possibly empty) prefix of a
  byte vector that does not contain the given substring
  plus the remainder of the byte vector.

  Totality: total
  Visibility: export
splitWith : (Bits8 -> Bool) -> ByteVect n -> List ByteString
  Splits a 'ByteVect' into components delimited by
  separators, where the predicate returns True for a separator element.
  The resulting components do not contain the separators. Two adjacent
  separators result in an empty component in the output. eg.

  Totality: total
  Visibility: export
splitWithNonEmpty : (Bits8 -> Bool) -> ByteVect n -> List ByteString
  Like `splitWith`, but removes empty components.

  Totality: total
  Visibility: export
split : Bits8 -> ByteVect n -> List ByteString
  Break a `ByteVect` into pieces separated by the byte
  argument, consuming the delimiter.
  
  As for all splitting functions in this library, this function does
  not copy the substrings, it just constructs new `ByteString`s that
  are slices of the original.

  Totality: total
  Visibility: export
splitNonEmpty : Bits8 -> ByteVect n -> List ByteString
  Like `split`, but removes empty components.

  Totality: total
  Visibility: export
lines : ByteVect n -> List ByteString
  Totality: total
  Visibility: export
splitAtSubstring : ByteVect k -> ByteVect n -> List ByteString
  Splits the second byte vector whenever the first called
  `sep` occurs.
  
  The bytestrings in the result no longer contain `sep` as
  a substring.
  
  Note: If `sep` is the empty byte vector, `[BS n val]` is returned
        as the result.

  Totality: total
  Visibility: export
isInfixOf : ByteVect m -> ByteVect n -> Bool
  Totality: total
  Visibility: export
parseAnyNat : (base : Nat) -> {auto 0 _ : LTE 2 base} -> {auto 0 _ : LTE base 16} -> ByteVect n -> Maybe Nat
  Parse a natural number in the given base.

  Totality: total
  Visibility: export
parseDecimalNat : ByteVect n -> Maybe Nat
  Parses a natural number in decimal notation.

  Totality: total
  Visibility: export
parseHexadecimalNat : ByteVect n -> Maybe Nat
  Totality: total
  Visibility: export
parseOctalNat : ByteVect n -> Maybe Nat
  Totality: total
  Visibility: export
parseBinaryNat : ByteVect n -> Maybe Nat
  Totality: total
  Visibility: export
parseInteger : ByteVect n -> Maybe Integer
  Totality: total
  Visibility: export
parseDouble : ByteVect n -> Maybe Double
  Totality: total
  Visibility: export
putByteVect : Builder q => ByteVect n -> F1' q
  Totality: total
  Visibility: export