Idris2Doc : Data.ByteString

Data.ByteString

(source)
Immutable strings of raw bytes.

Reexports

import public Data.ByteVect as BV

Definitions

null : ByteString -> Bool
Totality: total
Visibility: export
length : ByteString -> Nat
Totality: total
Visibility: export
index : Nat -> ByteString -> Maybe Bits8
  Tries to read the value of a `ByteString` at the given position

Totality: total
Visibility: export
empty : ByteString
  The empty `ByteString`.

Totality: total
Visibility: export
pack : List Bits8 -> ByteString
  Converts a list of `Bits8` values to a `ByteString`.

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

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

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

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

Totality: total
Visibility: export
generate : (n : Nat) -> (Fin n -> Bits8) -> ByteString
Totality: total
Visibility: export
replicate : Nat -> Bits8 -> ByteString
Totality: total
Visibility: export
unsafeByteString : Nat -> Buffer -> ByteString
Totality: total
Visibility: export
toBuffer : ByteString -> IO Buffer
  Copy the given `ByteString` and write its content to a freshly
  allocated buffer.

Totality: total
Visibility: export
fromIBuffer : IBuffer n -> ByteString
  Wrappes an immutable buffer in a `ByteString`

Totality: total
Visibility: export
TotLength : List ByteString -> Nat
Totality: total
Visibility: public export
copyMany : (ps : List ByteString) -> (pos : Nat) -> {auto 0 _ : pos + TotLength ps = n} -> MBuffer s n -> F1' s
Totality: total
Visibility: export
fastConcat : List ByteString -> ByteString
  Concatenate a list of `ByteString`. This allocates
  a buffer of sufficient size in advance, so it is much
  faster than `concat`, or `concatMap` for large `ByteString`s.

Totality: total
Visibility: export
concatSep : ByteString -> List ByteString -> ByteString
  Concatenates a list of bytestrings, separating them with the
  given separator `sep`.

Totality: total
Visibility: export
concatSep1 : Bits8 -> List ByteString -> ByteString
  Concatenates a list of bytestrings, using the given byte to
  separate them.

Totality: total
Visibility: export
unixUnlines : List ByteString -> ByteString
  Concatenates the given list of bytestring by interspersing them
  with Unix linebreaks (byte `0x0A`).

Totality: total
Visibility: export
append : ByteString -> ByteString -> ByteString
  Concatenate two `ByteString`s. O(n + m).

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

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

Totality: total
Visibility: export
padLeft : Nat -> Bits8 -> ByteString -> ByteString
Totality: total
Visibility: export
padRight : Nat -> Bits8 -> ByteString -> ByteString
Totality: total
Visibility: export
head : ByteString -> Maybe Bits8
  Read the first element of a `ByteString`. O(1).

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

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

Totality: total
Visibility: export
last : ByteString -> Maybe Bits8
  Read the last `Bits8` from a `ByteString`. O(1).

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

Totality: total
Visibility: export
unsnoc : ByteString -> Maybe (Bits8, ByteString)
  Split the last `Bits8` from a `ByteString`. O(1).

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

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

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

Totality: total
Visibility: export
reverse : ByteString -> ByteString
Totality: total
Visibility: export
all : (Bits8 -> Bool) -> ByteString -> Bool
  True, if the predicate holds for all bytes in the given `ByteString`

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

Totality: total
Visibility: export
elem : Bits8 -> ByteString -> Bool
  True, if the given `Bits8` appears in the `ByteString`.

Totality: total
Visibility: export
foldl : (a -> Bits8 -> a) -> a -> ByteString -> a
Totality: total
Visibility: export
foldr : (Bits8 -> a -> a) -> a -> ByteString -> a
Totality: total
Visibility: export
findIndex : (Bits8 -> Bool) -> ByteString -> Maybe Nat
  The `findIndex` function takes a predicate and a `ByteString` and
  returns the index of the first element in the ByteString
  satisfying the predicate.

Totality: total
Visibility: export
elemIndex : Bits8 -> ByteString -> Maybe Nat
  Return the index of the first occurence of the given
  byte in the `ByteString`, or `Nothing`, if the byte
  does not appear in the ByteString.

Totality: total
Visibility: export
find : (Bits8 -> Bool) -> ByteString -> Maybe Bits8
Totality: total
Visibility: export
isInfixOf : ByteString -> ByteString -> Bool
Totality: total
Visibility: export
isPrefixOf : ByteString -> ByteString -> Bool
Totality: total
Visibility: export
isSuffixOf : ByteString -> ByteString -> Bool
Totality: total
Visibility: export
substring : Nat -> Nat -> ByteString -> ByteString
  Like `substr` for `String`, this extracts a substring
  of the given `ByteString` at the given start position
  and of the given length.

Totality: total
Visibility: export
mapMaybe : (Bits8 -> Maybe Bits8) -> ByteString -> ByteString
Totality: total
Visibility: export
filter : (Bits8 -> Bool) -> ByteString -> ByteString
Totality: total
Visibility: export
take : Nat -> ByteString -> ByteString
  Return a `ByteString` with the first `n` values of
  the input string. Returns the whole string if
  `k` is larger than the bytestring. O(1)

Totality: total
Visibility: export
takeEnd : Nat -> ByteString -> ByteString
  Return a `ByteString` with the last `n` values of
  the input string. O(1)

Totality: total
Visibility: export
drop : Nat -> ByteString -> ByteString
  Remove the first `n` values from a `ByteString`. O(1)

Totality: total
Visibility: export
dropEnd : Nat -> ByteString -> ByteString
  Remove the last `n` values from a `ByteString`. O(1)

Totality: total
Visibility: export
splitAt : Nat -> ByteString -> Maybe (ByteString, ByteString)
Totality: total
Visibility: export
takeWhile : (Bits8 -> Bool) -> ByteString -> ByteString
  Extracts the longest prefix of elements satisfying the
  predicate.

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

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

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

Totality: total
Visibility: export
break : (Bits8 -> Bool) -> ByteString -> (ByteString, ByteString)
  Returns the longest (possibly empty) prefix of elements which do not
  satisfy the predicate and the remainder of the string.

Totality: total
Visibility: export
breakEnd : (Bits8 -> Bool) -> ByteString -> (ByteString, ByteString)
  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) -> ByteString -> (ByteString, ByteString)
  Returns the longest (possibly empty) prefix of elements
  satisfying the predicate and the remainder of the string.

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

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

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

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

Totality: total
Visibility: export
splitWith : (Bits8 -> Bool) -> ByteString -> List ByteString
  Splits a 'ByteString' 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) -> ByteString -> List ByteString
  Like `splitWith`, but removes empty components.

Totality: total
Visibility: export
split : Bits8 -> ByteString -> List ByteString
  Break a `ByteString` 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 -> ByteString -> List ByteString
  Like `splitWith`, but removes empty components.

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

Totality: total
Visibility: export
breakDropAtSubstring : ByteString -> ByteString -> (ByteString, ByteString)
  Like `breakAtSubstring` but removes the
  substring from the remainder

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

Totality: total
Visibility: export
unixLines : ByteString -> List ByteString
  Breakes the given bytestring at Unix linebreaks (byte `0x0A`).

Totality: total
Visibility: export
breakAround : ByteString -> ByteString -> ByteString -> Maybe (ByteString, (ByteString, ByteString))
  Extracts the string encountered between `start` and `end`
  returning a triple containing the prefix, string in the middle,
  and suffix.
  
  Note: The `start` and `end` tag will *not*
        be included in the resulting triple.
  
  Returns `Nothing` in case the prefix or suffix was the empty string.
  In particular, this will return `Nothing` in case `start` or `end`
  is the empty string.

Totality: total
Visibility: export
between : ByteString -> ByteString -> ByteString -> Maybe ByteString
  Extracts the string encountered between `start` and `end`.
  
  This will look for the *first* occurrence of `start` and
  will take everything until (but not including) the *first*
  occurrence of `end` after `start`.
  
  Returns `Nothing` if `end` or `start` is the empty string or
  either of the two was not found.

Totality: total
Visibility: export
nonEmpty : ByteString -> Maybe ByteString
  Returns the given byte string wrapped in a `Just` if and only if
  it is non-empty.

Totality: total
Visibility: export
manyBetween : ByteString -> ByteString -> ByteString -> List ByteString
  Extracts *all* occurrences of strings encountered between
  the given `start` and `end` tags.
  
  Returns an empty list if the start or end tag is the empty
  bytestring.

Totality: total
Visibility: export
betweenNonEmpty : ByteString -> ByteString -> ByteString -> Maybe ByteString
  Like `between` but returns `Nothing` in case the resulting
  bytestring would be empty.

Totality: total
Visibility: export
modBetween : ByteString -> ByteString -> (ByteString -> ByteString) -> ByteString -> ByteString
  Replaces the first byte sequence in the target string
  found between the given `start` and `end` tag by
  applying the given function.
  
  In case `start` or `end` is the empty string, this will return
  the unmodified bytestring.

Totality: total
Visibility: export
modBetweenAll : ByteString -> ByteString -> (ByteString -> ByteString) -> ByteString -> ByteString
  Replaces all byte sequences in the target string
  found between the given `start` and `end` tag by
  applying the given function to each of them.
  
  In case `start` or `end` is the empty string, this will return
  the unmodified bytestring.

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

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

Totality: total
Visibility: export
parseHexadecimalNat : ByteString -> Maybe Nat
Totality: total
Visibility: export
parseOctalNat : ByteString -> Maybe Nat
Totality: total
Visibility: export
parseBinaryNat : ByteString -> Maybe Nat
Totality: total
Visibility: export
parseInteger : ByteString -> Maybe Integer
Totality: total
Visibility: export
parseDouble : ByteString -> Maybe Double
Totality: total
Visibility: export
readByteString : HasIO io => Nat -> File -> io (Either FileError ByteString)
Totality: total
Visibility: export
writeByteVect : HasIO io => File -> ByteVect n -> io (Either (FileError, Int) ())
Totality: total
Visibility: export
writeByteString : HasIO io => File -> ByteString -> io (Either (FileError, Int) ())
Totality: total
Visibility: export
putByteString : Builder q => ByteString -> F1' q
Totality: total
Visibility: export
getByteString : Builder q => F1 q ByteString
Totality: total
Visibility: export