Idris2Doc : Data.Buffer.Core

Data.Buffer.Core

(source)
Reexports
import public Data.Fin
import public Data.Nat
Definitions
prim__getByte : Buffer -> Integer -> Bits8
prim__getByteOffset : Buffer -> Integer -> Integer -> Bits8
  This is an optimized version of `getByte` that allows us to read
  at an offset. On Chez, we can use the faster fixnum addition here,
  which can lead to a performance boost.
prim__setByte : Buffer -> Integer -> Bits8 -> PrimIO ()
prim__newBuf : Integer -> PrimIO Buffer
prim__getString : Buffer -> Integer -> Integer -> String
prim__fromString : String -> Buffer
prim__copy : Buffer -> Integer -> Integer -> Buffer -> Integer -> PrimIO ()
record IBuffer : Nat -> Type
  An immutable byte array of size `n`.

  Totality: total
  Visibility: export
  Constructor: 
IB : Buffer -> IBuffer n

  Projection: 
.buf : IBuffer n -> Buffer

  Hints:
  
Eq (IBuffer n)
  
Ord (IBuffer n)
  
Show (IBuffer n)
at : IBuffer n -> Fin n -> Bits8
  Safely access a value in an byte array at the given position.

  Totality: total
  Visibility: export
atOffset : IBuffer n -> Fin m -> (off : Nat) -> {auto 0 _ : LTE (off + m) n} -> Bits8
  Safely access a value in an immutable byte array at the given position
  and offset.

  Totality: total
  Visibility: export
take : (0 m : Nat) -> IBuffer n -> {auto 0 _ : LTE m n} -> IBuffer m
  We can wrap a prefix of an immutable 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`.

  Totality: total
  Visibility: export
fromString : (s : String) -> IBuffer (cast (stringByteLength s))
  Convert an UTF-8 string to an immutable byte array.

  Totality: total
  Visibility: export
toString : IBuffer n -> (off : Nat) -> (len : Nat) -> {auto 0 _ : LTE (off + len) n} -> String
  Convert a section of an immutable byte array to an UTF-8 string.

  Totality: total
  Visibility: export
unsafeGetBuffer : IBuffer n -> Buffer
  Extracts the inner buffer held by an immutable 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!

  Totality: total
  Visibility: export
unsafeMakeBuffer : Buffer -> IBuffer k
  Wraps a bare mutable buffer in an `IBuffer`.
  
  Client code is responsible to make sure the original buffer is no longer
  used.

  Totality: total
  Visibility: export
record AnyBuffer : Type
  Totality: total
  Visibility: public export
  Constructor: 
AB : (size : Nat) -> IBuffer size -> AnyBuffer

  Projections:
  
.ibuf : ({rec:0} : AnyBuffer) -> IBuffer (size {rec:0})
  
.size : AnyBuffer -> Nat

  Hints:
  
Cast AnyBuffer String
  
Eq AnyBuffer
  
FromString AnyBuffer
  
Monoid AnyBuffer
  
Ord AnyBuffer
  
Semigroup AnyBuffer
  
Show AnyBuffer
.size : AnyBuffer -> Nat
  Totality: total
  Visibility: public export
size : AnyBuffer -> Nat
  Totality: total
  Visibility: public export
.ibuf : ({rec:0} : AnyBuffer) -> IBuffer (size {rec:0})
  Totality: total
  Visibility: public export
ibuf : ({rec:0} : AnyBuffer) -> IBuffer (size {rec:0})
  Totality: total
  Visibility: public export
data MBuffer : Type -> Nat -> Type
  A mutable byte array.

  Totality: total
  Visibility: export
  Constructor: 
MB : Buffer -> MBuffer s n
0 IOBuffer : Nat -> Type
  Convenience alias for `MBuffer' RIO`

  Totality: total
  Visibility: public export
unsafeMBuffer : Buffer -> MBuffer s n
  Wraps a `Buffer` in an `IOBuffer`. Use at your own risk.

  Totality: total
  Visibility: export
unsafeFromMBuffer : MBuffer s n -> Buffer
  Extracts the `Buffer` from an `MBuffer`. Use at your own risk.

  Totality: total
  Visibility: export
mbuffer1 : (n : Nat) -> F1 s (MBuffer s n)
  Creates a new mutable byte array bound to linear computation `s`.

  Totality: total
  Visibility: export
mbuffer : Lift1 s f => (n : Nat) -> f (MBuffer s n)
  Creates a new mutable byte array in `IO`.

  Totality: total
  Visibility: export
set : MBuffer s n -> Fin n -> Bits8 -> F1' s
  Safely write a value to a mutable byte array.

  Totality: total
  Visibility: export
get : MBuffer s n -> Fin n -> F1 s Bits8
  Safely read a value from a mutable byte array.

  Totality: total
  Visibility: export
modify : MBuffer s n -> Fin n -> (Bits8 -> Bits8) -> F1' s
  Safely modify a value in a mutable byte array.

  Totality: total
  Visibility: export
bufString : MBuffer s n -> (m : Nat) -> {auto 0 _ : LTE m n} -> F1 s String
  Extracts a string from a (possibly partially) filled mutable byte array.

  Totality: total
  Visibility: export
bufStringFromTill : MBuffer s n -> (from : Nat) -> (till : Nat) -> {auto 0 _ : LTE from till} -> {auto 0 _ : LTE till n} -> F1 s String
  Like `bufString` but extracts a substring from position
  `from` up to but not including position `till`.

  Totality: total
  Visibility: export
bufStringFromTo : MBuffer s n -> (from : Nat) -> (to : Nat) -> {auto 0 _ : LTE from to} -> {auto 0 _ : LT to n} -> F1 s String
  Like `bufString` but extracts a substring from position
  `from` up to and including position `to`.

  Totality: total
  Visibility: export
mtake : MBuffer s n -> (0 m : Nat) -> {auto 0 _ : LTE m n} -> F1 s (MBuffer s m)
  Wraps a mutable byte array in a shorter one.

  Totality: total
  Visibility: export
0 WithMBuffer : Nat -> Type -> Type
  Totality: total
  Visibility: public export
alloc : (n : Nat) -> WithMBuffer n a -> a
  Allocate and potentially freeze a mutable byte array in a linear context.

  Totality: total
  Visibility: export
copy : MBuffer s m -> (srcOffset : Nat) -> (dstOffset : Nat) -> (len : Nat) -> {auto 0 _ : LTE (srcOffset + len) m} -> {auto 0 _ : LTE (dstOffset + len) n} -> MBuffer s n -> F1' s
  Totality: total
  Visibility: export
icopy : IBuffer m -> (srcOffset : Nat) -> (dstOffset : Nat) -> (len : Nat) -> {auto 0 _ : LTE (srcOffset + len) m} -> {auto 0 _ : LTE (dstOffset + len) n} -> MBuffer s n -> F1' s
  Totality: total
  Visibility: export
bufSubstring : MBuffer s n -> (off : Nat) -> (len : Nat) -> {auto 0 _ : LTE (off + len) n} -> F1 s (IBuffer len)
  Extracts an immutable sub-array from a mutable byte array.

  Totality: total
  Visibility: export
bufSubstringFromTill : MBuffer s n -> (from : Nat) -> (till : Nat) -> {auto 0 _ : LTE from till} -> {auto 0 _ : LTE till n} -> F1 s (IBuffer (minus till from))
  Like `bufSubstring` but extracts a substring from position
  `from` up to but not including position `till`.

  Totality: total
  Visibility: export
bufSubstringFromTo : MBuffer s n -> (from : Nat) -> (to : Nat) -> {auto 0 _ : LTE from to} -> {auto 0 _ : LT to n} -> F1 s (IBuffer (minus (S to) from))
  Like `bufSubstring` but extracts a substring from position
  `from` up to and including position `to`.

  Totality: total
  Visibility: export
thaw : IBuffer n -> F1 s (MBuffer s n)
  Copy the content of an immutable byte array to a new byte array.

  Totality: total
  Visibility: export
unsafeFreezeLTE : MBuffer s n -> (0 m : Nat) -> {auto 0 _ : LTE m n} -> F1 s (IBuffer m)
  Wrap a mutable byte array in an immutable byte array 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`.
  
  Note: For reasons of efficiency, this does not copy the buffer,
        and therefore, it must no longer be modified after calling
        this function.

  Totality: total
  Visibility: export
unsafeFreeze : MBuffer s n -> F1 s (IBuffer n)
  Convenience alias for `unsafeFreezeLTE @{reflexive}`

  Totality: total
  Visibility: export
freezeLTE : MBuffer s n -> (m : Nat) -> {auto 0 _ : LTE m n} -> F1 s (IBuffer m)
  Copy a prefix of a mutable byte arrya into an immutable byte array.

  Totality: total
  Visibility: export
freeze : MBuffer s n -> F1 s (IBuffer n)
  Copy a mutable byte array into an immutable byte array.

  Totality: total
  Visibility: export
readIBuffer : HasIO io => Nat -> File -> io (Either FileError (n : Nat ** IBuffer n))
  Read up to `n` bytes from a file into an immutable byte array.

  Totality: total
  Visibility: export
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 an immutable byte array to a file, starting
  at the given offset.

  Totality: total
  Visibility: export
writeMBuffer : HasIO io => File -> (offset : Nat) -> (len : Nat) -> {auto 0 _ : LTE (offset + len) n} -> MBuffer s n -> io (Either (FileError, Int) ())
  Write up to `len` bytes from a mutable byte array to a file, starting
  at the given offset.

  Totality: total
  Visibility: export