diff --git a/docs/array/docs/docs/Data.Buffer.Core.html b/docs/array/docs/docs/Data.Buffer.Core.html index c49b861c3..f5603d476 100644 --- a/docs/array/docs/docs/Data.Buffer.Core.html +++ b/docs/array/docs/docs/Data.Buffer.Core.html @@ -61,4 +61,4 @@ -
import public Data.Fin
import public Data.Nat
prim__getByte : Buffer -> Bits32 -> Bits8
prim__setByte : Buffer -> Bits32 -> Bits8 -> PrimIO ()
prim__newBuf : Bits32 -> PrimIO Buffer
prim__getString : Buffer -> Bits32 -> Bits32 -> String
prim__fromString : String -> Buffer
prim__copy : Buffer -> Bits32 -> Bits32 -> Buffer -> Bits32 -> PrimIO ()
record IBuffer : Nat -> Type
An immutable byte array of size `n`.
.buf : IBuffer n -> Buffer
at : IBuffer n -> Fin n -> Bits8
Safely access a value in an byte array at the given position.
take : (0 m : Nat) -> IBuffer n -> {auto 0 _ : LTE m n} -> IBuffer m
We can wrap a prefix of a byte array in O(1) simply by giving it
a new size index.
Note: If you only need a small portion of a potentially large
byte array the rest of which you no longer need, consider to
releasing the large byte array from memory by invoking `force`.
fromString : (s : String) -> IBuffer (cast (stringByteLength s))
Convert an UTF-8 string to a buffer
toString : IBuffer n -> (off : Nat) -> (len : Nat) -> {auto 0 _ : LTE (off + len) n} -> String
Convert a section of a byte array to an UTF-8 string.
unsafeGetBuffer : IBuffer n -> Buffer
Extracts the inner buffer held by a byte array without copying.
This allows us to write efficiently write the data to a file
without copying it first. This is a highly unsafe operation,
and client code must make sure never ever to mutate the buffer!
unsafeMakeBuffer : Buffer -> IBuffer k
Wrapps a bare mutable buffer in an `IBuffer`.
Client code is responsible to make sure the original buffer is no longer
used.
data MBuffer' : RTag -> Nat -> Type
A mutable byte array.
InIO (MBuffer' RIO n)
0 MBuffer : Nat -> Type
Convenience alias for `MBuffer' RPure`
0 IOBuffer : Nat -> Type
Convenience alias for `MBuffer' RIO`
newMBuffer : (n : Nat) -> (1 _ : T1 rs) -> A1 rs (MBuffer n)
Creates a new mutable bound to linear computation `s`.
bufferIO : (n : Nat) -> a -> F1 [World] (IOBuffer n)
Creates a new mutable buffer in `T1 [Wrold]`
newIOBuffer : HasIO io => (n : Nat) -> io (IOBuffer n)
Creates a new mutable buffer in `IO`.
set : (r : MBuffer' t n) -> {auto 0 _ : Res r rs} -> Fin n -> Bits8 -> F1' rs
Safely write a value to a mutable byte vector.
get : (r : MBuffer' t n) -> {auto 0 _ : Res r rs} -> Fin n -> F1 rs Bits8
Safely read a value from a mutable byte array.
modify : (r : MBuffer' t n) -> {auto 0 _ : Res r rs} -> Fin n -> (Bits8 -> Bits8) -> F1' rs
Safely modify a value in a mutable byte array.
release : (0 r : MBuffer n) -> {auto 0 p : Res r rs} -> C1' rs (Drop rs p)
Release a byte array.
Afterwards, it can no longer be use with the given linear token.
0 WithMBuffer : Nat -> Type -> Type
0 FromMBuffer : Nat -> Type -> Type
create : (n : Nat) -> FromMBuffer n a -> a
Allocate and potentially freeze a mutable byte array in a linear context.
Note: In case you don't need to freeze the array in the end, using `alloc`
might be more convenient.
alloc : (n : Nat) -> WithMBuffer n a -> a
Allocate, use, and release a mutable byte array in a linear computation.
Note: In case you want to freeze the buffer and return it in the
result, use `create`.
copy : IBuffer m -> (srcOffset : Nat) -> (dstOffset : Nat) -> (len : Nat) -> {auto 0 _ : LTE (srcOffset + len) m} -> {auto 0 _ : LTE (dstOffset + len) n} -> (r : MBuffer n) -> {auto 0 _ : Res r rs} -> F1' rs
thaw : IBuffer n -> FromMBuffer n b -> b
Copy the content of an immutable buffer to a new buffer.
freezeLTE : {auto 0 _ : LTE m n} -> (r : MBuffer n) -> {auto 0 p : Res r rs} -> (0 m : Nat) -> (1 _ : T1 rs) -> R1 (Drop rs p) (IBuffer m)
Wrap a mutable buffer in an `IBuffer` without copying.
In order to make this safe, the associated linear token has to
be discarded.
It is safe to only use a prefix of a properly constructed array,
therefore we are free to give the resulting array a smaller size.
Most of the time, we'd like to use the whole buffer, in which case
we can just use `freezeBufAt`.
freeze : (r : MBuffer n) -> {auto 0 p : Res r rs} -> (1 _ : T1 rs) -> R1 (Drop rs p) (IBuffer n)
toIO : (r : MBuffer n) -> {auto 0 p : Res r rs} -> (1 _ : T1 rs) -> R1 (Drop rs p) (IO Buffer)
Release a mutable linear buffer to `IO`, thus making it freely
shareable.
readIBuffer : HasIO io => Nat -> File -> io (Either FileError (n : Nat ** IBuffer n))
Read up to `n` bytes from a file into an immutable buffer.
writeIBuffer : HasIO io => File -> (offset : Nat) -> (len : Nat) -> IBuffer n -> {auto 0 _ : LTE (offset + len) n} -> io (Either (FileError, Int) ())
Write up to `len` bytes from a buffer to a file, starting
at the given offset.
writeMBuffer : HasIO io => File -> (offset : Nat) -> (len : Nat) -> {auto 0 _ : LTE (offset + len) n} -> (r : MBuffer n) -> {auto 0 p : Res r rs} -> T1 rs -> R1 (Drop rs p) (io (Either (FileError, Int) ()))
Write up to `len` bytes from a buffer to a file, starting
at the given offset.