Data.ByteArray.Builder.Bounded

The functions in this module are explict about the maximum number of bytes they require.

Builder

data Builder :: Nat -> Type

A builder parameterized by the maximum number of bytes it uses when executed.

Execute

run

Arguments

:: Nat n

-> Builder n

Builder

-> ByteArray

Execute the bounded builder. If the size is a constant, use Arithmetic.Nat.constant as the first argument to let GHC conjure up this value for you.

pasteGrowST

Arguments

:: Nat n

-> Builder n

-> MutableByteArrayOffset s

Initial buffer, used linearly. Do not reuse this argument.

-> ST s (MutableByteArrayOffset s)

Final buffer that accomodated the builder.

Paste the builder into the byte array starting at offset zero. This reallocates the byte array if it cannot accomodate the builder, growing it by the minimum amount necessary.

Combine

empty :: Builder 0

The monoidal unit of append

append :: Builder m -> Builder n -> Builder (m + n) infixr 9

Concatenate two builders.

Bounds Manipulation

weaken :: forall m n. (m <= n) -> Builder m -> Builder n

Weaken the bound on the maximum number of bytes required. For example, to use two builders with unequal bounds in a disjunctive setting:

import qualified Arithmetic.Lte as Lte

buildNumber :: Either Double Word64 -> Builder 32
buildNumber = \case
  Left d  -> doubleDec d
  Right w -> weaken (Lte.constant @19 @32) (word64Dec w)

substitute :: forall m n. (m :=: n) -> Builder m -> Builder n

Replace the upper bound on size with an equal number.

Encode Integral Types

Human-Readable

word64Dec :: Word64 -> Builder 19

Requires up to 19 bytes. Encodes an unsigned 64-bit integer as decimal. This encoding never starts with a zero unless the argument was zero.

word32Dec :: Word32 -> Builder 10

Requires up to 10 bytes. Encodes an unsigned 32-bit integer as decimal. This encoding never starts with a zero unless the argument was zero.

word16Dec :: Word16 -> Builder 5

Requires up to 5 bytes. Encodes an unsigned 16-bit integer as decimal. This encoding never starts with a zero unless the argument was zero.

word8Dec :: Word8 -> Builder 3

Requires up to 3 bytes. Encodes an unsigned 8-bit integer as decimal. This encoding never starts with a zero unless the argument was zero.

wordDec :: Word -> Builder 19

Requires up to 19 bytes. Encodes an unsigned machine-sized integer as decimal. This encoding never starts with a zero unless the argument was zero.

int64Dec :: Int64 -> Builder 20

Requires up to 20 bytes. Encodes a signed 64-bit integer as decimal. This encoding never starts with a zero unless the argument was zero. Negative numbers are preceded by a minus sign. Positive numbers are not preceded by anything.

int32Dec :: Int32 -> Builder 11

Requires up to 11 bytes. Encodes a signed 32-bit integer as decimal. This encoding never starts with a zero unless the argument was zero. Negative numbers are preceded by a minus sign. Positive numbers are not preceded by anything.

int16Dec :: Int16 -> Builder 6

Requires up to 6 bytes. Encodes a signed 16-bit integer as decimal. This encoding never starts with a zero unless the argument was zero. Negative numbers are preceded by a minus sign. Positive numbers are not preceded by anything.

int8Dec :: Int8 -> Builder 4

Requires up to 4 bytes. Encodes a signed 8-bit integer as decimal. This encoding never starts with a zero unless the argument was zero. Negative numbers are preceded by a minus sign. Positive numbers are not preceded by anything.

intDec :: Int -> Builder 20

Requires up to 20 bytes. Encodes a signed machine-sized integer as decimal. This encoding never starts with a zero unless the argument was zero. Negative numbers are preceded by a minus sign. Positive numbers are not preceded by anything.

Unsigned Words

64-bit

word64PaddedUpperHex :: Word64 -> Builder 16

Requires exactly 16 bytes. Encodes a 64-bit unsigned integer as hexadecimal, zero-padding the encoding to 16 digits. This uses uppercase for the alphabetical digits. For example, this encodes the number 1022 as 00000000000003FE.

32-bit

word32PaddedUpperHex :: Word32 -> Builder 8

Requires exactly 8 bytes. Encodes a 32-bit unsigned integer as hexadecimal, zero-padding the encoding to 8 digits. This uses uppercase for the alphabetical digits.

16-bit

word16PaddedLowerHex :: Word16 -> Builder 4

Requires exactly 4 bytes. Encodes a 16-bit unsigned integer as hexadecimal, zero-padding the encoding to 4 digits. This uses lowercase for the alphabetical digits.

>>> word16PaddedLowerHex 0xab0
0ab0

word16PaddedUpperHex :: Word16 -> Builder 4

Requires exactly 4 bytes. Encodes a 16-bit unsigned integer as hexadecimal, zero-padding the encoding to 4 digits. This uses uppercase for the alphabetical digits.

>>> word16PaddedUpperHex 0xab0
0AB0

word16LowerHex :: Word16 -> Builder 4

Requires at most 4 bytes. Encodes a 16-bit unsigned integer as hexadecimal. No leading zeroes are displayed. Letters are presented in lowercase. If the number is zero, a single zero digit is used.

>>> word16LowerHex 0xab0
ab0

word16UpperHex :: Word16 -> Builder 4

Requires at most 4 bytes. Encodes a 16-bit unsigned integer as hexadecimal. No leading zeroes are displayed. Letters are presented in uppercase. If the number is zero, a single zero digit is used.

>>> word16UpperHex 0xab0
AB0

8-bit

word8PaddedUpperHex :: Word8 -> Builder 2

Requires exactly 2 bytes. Encodes a 8-bit unsigned integer as hexadecimal, zero-padding the encoding to 2 digits. This uses uppercase for the alphabetical digits.

word8LowerHex :: Word8 -> Builder 2

Requires at most 2 bytes. Encodes a 8-bit unsigned integer as hexadecimal. No leading zeroes are displayed. If the number is zero, a single zero digit is used.

ascii :: Char -> Builder 1

Encode an ASCII character. Precondition: Input must be an ASCII character. This is not checked.

char :: Char -> Builder 4

Encode a character as UTF-8. This only uses as much space as is required.

Machine-Readable

One

word8 :: Word8 -> Builder 1

Big Endian

word64BE :: Word64 -> Builder 8

Requires exactly 8 bytes. Dump the octets of a 64-bit word in a big-endian fashion.

word32BE :: Word32 -> Builder 4

Requires exactly 4 bytes. Dump the octets of a 32-bit word in a big-endian fashion.

word16BE :: Word16 -> Builder 2

Requires exactly 2 bytes. Dump the octets of a 16-bit word in a big-endian fashion.

int64BE :: Int64 -> Builder 8

int32BE :: Int32 -> Builder 4

int16BE :: Int16 -> Builder 2

Little Endian

word64LE :: Word64 -> Builder 8

Requires exactly 8 bytes. Dump the octets of a 64-bit word in a little-endian fashion.

word32LE :: Word32 -> Builder 4

Requires exactly 4 bytes. Dump the octets of a 32-bit word in a little-endian fashion.

word16LE :: Word16 -> Builder 2

Requires exactly 2 bytes. Dump the octets of a 16-bit word in a little-endian fashion.

int64LE :: Int64 -> Builder 8

int32LE :: Int32 -> Builder 4

int16LE :: Int16 -> Builder 2

Encode Floating-Point Types

doubleDec :: Double -> Builder 32

Encode a double-floating-point number, using decimal notation or scientific notation depending on the magnitude. This has undefined behavior when representing +inf, -inf, and NaN. It will not crash, but the generated numbers will be nonsense.