idris-lang/Idris-dev — pull request #816 by shlevy (2014-01-30 06:26:17+00:00)
Title: Buffer

As proposed in #802, this implements `Data.Buffer`, a pure interface to contiguous chunks of memory. At the interface level, this consists of the following terms in `Data.Buffer`:

* An abstract `Buffer : Nat -> Type`, where the `Nat` represents the number of valid (i.e. initialized) bytes in the `Buffer`
* An `allocate : ( sizeHint : Nat ) -> Buffer Z`, where `sizeHint` gives a hint as to how much space should be reserved for future appends to the `Buffer`
* A `copy : Buffer n -> Buffer n`. Multiple `Buffer` objects may point to the same underlying storage, which may mean that some relatively small `Buffer` is keeping a large chunk from being freed. `copy` is semantically equivalent to `id` except that the underlying storage should be initially uniquely pointed-to by the returned `Buffer`.
* A series of `append` functions for appending values to the buffer in various endiannesses. They are named `append{Type}{EN}`, where `Type` is one of `[ Bits8, Bits16, Bits32, Bits64, Buffer ]` and `EN` is one of `[ Native, BE, LE ]`. Each such function has type `Buffer n -> ( count : Nat ) -> ( val : {Type} ) -> Buffer (n + (sizeof {Type}) * count` and adds `count` repetitions of `val` represented in the relevant byte-order. For example, `appendBits32LE : Buffer n -> ( count : Nat ) -> ( val : Bits32 ) -> Buffer (n + 4 * count)` will append the passed `Bits32`, in little-endian byte order, to the `Buffer` `count` times. For `Buffer` and `Bits8` the endianness has no real meaning, but the `BE` and `LE` variants are provided for symmetry.
* A series of `peek` functions for retrieving values from the buffer in various endiannesses. They are named `peek{Type}{EN}`, where `Type` is one of `[ Bits8, Bits16, Bits32, Bits64, Buffer ]` and `EN` is one of `[ Native, BE, LE ]`. Each such function has type `Buffer (sizeof {Type} + n) -> ( offset : Fin S n ) -> ( val : {Type} )` and reads `val` represented in the relevant byte-order at the given byte `offset` in the Buffer. For example, `peekBits16Native : Buffer (2 + n) -> ( offset : Fin S n ) -> ( val : Bits16 )` will read `Bits16`, in machine-native byte order from the `Buffer` starting at `offset` bytes. For `Buffer` and `Bits8` the endianness has no real meaning, but the `BE` and `LE` variants are provided for symmetry.

Under the hood, each function is implemented on top of a primitive that takes `Bits64`s in place of `Fin n`s and `Nat`s, some of which also explicitly take the `Buffer` size as a `Bits64`. As I commented in the `Data.Buffer` module, there are a few issues with this interface:

1. It may be theoretically nice to represent `Buffer` size as `Fin (2 ^ WORD_BITS)` instead of `Nat`
2. Primitives take `Bits64` when really they should take the equivalent of C's `size_t` (ideally unboxed)
3. If we had access to host system information, we could reduce the needed primitives by implementing the LE/BE variants on top of the native variant plus a possible swab function
4. Would be nice to be able to peek/append `Int`, `Char`, and `Float`, all have fixed (though possibly implementation-dependent) widths. Currently not in place due to lack of host system introspection.
5. Would be nice to be able to peek/append the vector types, but for now I'm only touching the C backend which AFAICT doesn't support them.
6. Conversion from `Fin` to `Bits64` (which, re `2`, should eventually be a fixed-width implementation-dependent type) is likely inefficient relative to conversion from `Nat` to `Bits64`

For now, I've only implemented the `Buffer` primitives in the C codegen. There was a fair amount of duplication there, which might be reducible somewhat with macros. The implementation uses a fill value and power-of-2 allocation for efficient appends in many cases, see #802 or the code for details. I can try my hand at the LLVM codegen implementation once this is merged in some form.

Fixes #802