Skip to content

Update the buffer API #3796

Description

@andrevidela
  • I have read CONTRIBUTING.md.
  • I have checked that there is no existing PR/issue about my proposal.
  • I confirm that this contribution did not involve GenerativeAI nor Large Language Models.

Summary

The buffer API has the following problems:

  • No way to create an empty buffer
  • No way to grow a buffer in-place
  • Additional overhead when creating a newBuffer due to Maybe

The proposal

Add the following

allocBuffer : Int -> IO Buffer
allocBuffer n = primtIO $ prim__newBuffer n

emptyBuffer : IO Buffer
emptyBuffer = allocBuffer 0

resize : Buffer -> Int -> IO ()

grow : Buffer -> Int -> IO ()
grow b n = resize b (!(rawSize b) + n)

-- same as newBuffer but without Maybe
nonEmptyBuffer : (n : Int) -> {0 auto notZero : n /= 0} -> IO Buffer

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions