idris-bytes

A FFI-based implementation of byte buffers for Idris.

This is a snoc-based structure (designed to grow to the right).
Reading is unrestricted -- we provide consView, as well as snocView, subslicing and arbitrary indexing, all in O(1).
Copying is avoided wherever possible (copy-on-second-write) -- snocs and appends will not copy the LHS argument unless necessary. Instead, data is destructively written into pre-allocated spare space, as long as it is safe.
Built on top of Data.ByteArray, IO-based mutable byte arrays.

This is the binary backend for idris-text.

Installation

$ idris --build bytes.ipkg
$ idris --install bytes.ipkg