Safe Haskell | None |
---|---|

Language | Haskell2010 |

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

## Synopsis

- data Builder :: Nat -> Type
- run :: Nat n -> Builder n -> ByteArray
- pasteGrowST :: Nat n -> Builder n -> MutableByteArrayOffset s -> ST s (MutableByteArrayOffset s)
- empty :: Builder 0
- append :: Builder m -> Builder n -> Builder (m + n)
- weaken :: forall m n. (m <= n) -> Builder m -> Builder n
- substitute :: forall m n. (m :=: n) -> Builder m -> Builder n
- word64Dec :: Word64 -> Builder 19
- word32Dec :: Word32 -> Builder 10
- word16Dec :: Word16 -> Builder 5
- word8Dec :: Word8 -> Builder 3
- wordDec :: Word -> Builder 19
- int64Dec :: Int64 -> Builder 20
- int32Dec :: Int32 -> Builder 11
- int16Dec :: Int16 -> Builder 6
- int8Dec :: Int8 -> Builder 4
- intDec :: Int -> Builder 20
- word128PaddedLowerHex :: Word128 -> Builder 32
- word128PaddedUpperHex :: Word128 -> Builder 32
- word256PaddedLowerHex :: Word256 -> Builder 64
- word256PaddedUpperHex :: Word256 -> Builder 64
- word64PaddedLowerHex :: Word64 -> Builder 16
- word64PaddedUpperHex :: Word64 -> Builder 16
- word48PaddedLowerHex :: Word64 -> Builder 12
- word32PaddedLowerHex :: Word32 -> Builder 8
- word32PaddedUpperHex :: Word32 -> Builder 8
- word16PaddedLowerHex :: Word16 -> Builder 4
- word16PaddedUpperHex :: Word16 -> Builder 4
- word16LowerHex :: Word16 -> Builder 4
- word16UpperHex :: Word16 -> Builder 4
- word8PaddedLowerHex :: Word8 -> Builder 2
- word8PaddedUpperHex :: Word8 -> Builder 2
- word8LowerHex :: Word8 -> Builder 2
- ascii :: Char -> Builder 1
- ascii2 :: Char -> Char -> Builder 2
- ascii3 :: Char -> Char -> Char -> Builder 3
- ascii4 :: Char -> Char -> Char -> Char -> Builder 4
- ascii5 :: Char -> Char -> Char -> Char -> Char -> Builder 5
- ascii6 :: Char -> Char -> Char -> Char -> Char -> Char -> Builder 6
- char :: Char -> Builder 4
- wordPaddedDec2 :: Word -> Builder 2
- wordPaddedDec4 :: Word -> Builder 4
- wordPaddedDec9 :: Word -> Builder 9
- word8 :: Word8 -> Builder 1
- word256BE :: Word256 -> Builder 32
- word128BE :: Word128 -> Builder 16
- word64BE :: Word64 -> Builder 8
- word32BE :: Word32 -> Builder 4
- word16BE :: Word16 -> Builder 2
- int64BE :: Int64 -> Builder 8
- int32BE :: Int32 -> Builder 4
- int16BE :: Int16 -> Builder 2
- word256LE :: Word256 -> Builder 32
- word128LE :: Word128 -> Builder 16
- word64LE :: Word64 -> Builder 8
- word32LE :: Word32 -> Builder 4
- word16LE :: Word16 -> Builder 2
- int64LE :: Int64 -> Builder 8
- int32LE :: Int32 -> Builder 4
- int16LE :: Int16 -> Builder 2
- wordLEB128 :: Word -> Builder 10
- word64LEB128 :: Word64 -> Builder 10
- doubleDec :: Double -> Builder 32

# Builder

data Builder :: Nat -> Type Source #

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

# Execute

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.

:: 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

# Bounds Manipulation

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

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 Source #

Replace the upper bound on size with an equal number.

# Encode Integral Types

## Human-Readable

word64Dec :: Word64 -> Builder 19 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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 Source #

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

## Wide Words

word128PaddedLowerHex :: Word128 -> Builder 32 Source #

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

word128PaddedUpperHex :: Word128 -> Builder 32 Source #

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

word256PaddedLowerHex :: Word256 -> Builder 64 Source #

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

word256PaddedUpperHex :: Word256 -> Builder 64 Source #

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

## 64-bit

word64PaddedLowerHex :: Word64 -> Builder 16 Source #

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

.

word64PaddedUpperHex :: Word64 -> Builder 16 Source #

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`

.

## 48-bit

word48PaddedLowerHex :: Word64 -> Builder 12 Source #

Requires exactly 12 bytes. Discards the upper 16 bits of a
64-bit unsigned integer and then encodes the lower 48 bits as
hexadecimal, zero-padding the encoding to 12 digits. This uses
lowercase for the alphabetical digits. For example, this encodes the
number 1022 as `0000000003fe`

.

## 32-bit

word32PaddedLowerHex :: Word32 -> Builder 8 Source #

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

word32PaddedUpperHex :: Word32 -> Builder 8 Source #

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 Source #

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.

`>>>`

0ab0`word16PaddedLowerHex 0xab0`

word16PaddedUpperHex :: Word16 -> Builder 4 Source #

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.

`>>>`

0AB0`word16PaddedUpperHex 0xab0`

word16LowerHex :: Word16 -> Builder 4 Source #

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.

`>>>`

ab0`word16LowerHex 0xab0`

word16UpperHex :: Word16 -> Builder 4 Source #

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.

`>>>`

AB0`word16UpperHex 0xab0`

## 8-bit

word8PaddedLowerHex :: Word8 -> Builder 2 Source #

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

word8PaddedUpperHex :: Word8 -> Builder 2 Source #

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 Source #

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 Source #

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

ascii2 :: Char -> Char -> Builder 2 Source #

Encode two ASCII characters. Precondition: Must be an ASCII characters. This is not checked.

ascii3 :: Char -> Char -> Char -> Builder 3 Source #

Encode three ASCII characters. Precondition: Must be an ASCII characters. This is not checked.

ascii4 :: Char -> Char -> Char -> Char -> Builder 4 Source #

Encode four ASCII characters. Precondition: Must be an ASCII characters. This is not checked.

ascii5 :: Char -> Char -> Char -> Char -> Char -> Builder 5 Source #

Encode five ASCII characters. Precondition: Must be an ASCII characters. This is not checked.

ascii6 :: Char -> Char -> Char -> Char -> Char -> Char -> Builder 6 Source #

Encode six ASCII characters. Precondition: Must be an ASCII characters. This is not checked.

char :: Char -> Builder 4 Source #

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

## Native

wordPaddedDec2 :: Word -> Builder 2 Source #

Encode a number less than 100 as a decimal number, zero-padding it to
two digits. For example: 0 is encoded as `00`

, 5 is encoded as `05`

, and
73 is encoded as `73`

.

Precondition: Argument must be less than 100. Failure to satisfy this precondition will not result in a segfault, but the resulting bytes are undefined. The implemention uses a heuristic for division that is inaccurate for large numbers.

wordPaddedDec4 :: Word -> Builder 4 Source #

Encode a number less than 10000 as a decimal number, zero-padding it to
two digits. For example: 0 is encoded as `0000`

, 5 is encoded as `0005`

,
and 73 is encoded as `0073`

.

Precondition: Argument must be less than 10000. Failure to satisfy this precondition will not result in a segfault, but the resulting bytes are undefined. The implemention uses a heuristic for division that is inaccurate for large numbers.

wordPaddedDec9 :: Word -> Builder 9 Source #

Encode a number less than 1e9 as a decimal number, zero-padding it to
nine digits. For example: 0 is encoded as `000000000`

and 5 is encoded as
`000000005`

.

Precondition: Argument must be less than 1e9. Failure to satisfy this precondition will not result in a segfault, but the resulting bytes are undefined. The implemention uses a heuristic for division that is inaccurate for large numbers.

## Machine-Readable

### One

#### Big Endian

word64BE :: Word64 -> Builder 8 Source #

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

word32BE :: Word32 -> Builder 4 Source #

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

word16BE :: Word16 -> Builder 2 Source #

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

#### Little Endian

word64LE :: Word64 -> Builder 8 Source #

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

word32LE :: Word32 -> Builder 4 Source #

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

word16LE :: Word16 -> Builder 2 Source #

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

#### LEB128

wordLEB128 :: Word -> Builder 10 Source #

Encode a machine-sized word with LEB-128.

word64LEB128 :: Word64 -> Builder 10 Source #

Encode a 64-bit word with LEB-128.