std.vec

A growable owner. Growth is the only allocation and it is visible in every caller's effect row.

// Lent where a view is expected: `io.print(line)` passes the elements it holds, `line.data[0..line.len]`.
pub struct Vec[T:affine] { data:Buf[T]; len:usize; lends data[0..len]; }

pub fn new[T:affine]() -> Vec[T]  // effects: alloc, free, trap, zero_init
pub fn with_capacity[T:affine](capacity:usize) -> Vec[T]  // effects: alloc, free, trap, zero_init
pub fn capacity[T:affine](v:ro<Vec[T]>) -> usize  // effects: read:v

// A Vec holding a copy of `src`, in one allocation of exactly its length: `vec.from(input.data[lo..hi])`.
// effects: alloc, ffi_precondition, free, local_read, local_write, read:src, trap, zero_init
pub fn from[T:copy](n:usize, src:ro<T>[n]@host) -> Vec[T]

// Doubling keeps pushes amortized constant; elements move by swap, so owners are never copied. Cost: one allocation,
// and one pass over the elements held with no guard in it.
// effects: alloc, ffi_precondition, free, local_read, local_write, read:v, trap, write:v, zero_init
pub fn reserve[T:affine](v:rw<Vec[T]>, wanted:usize)

// effects: alloc, ffi_precondition, free, local_read, local_write, read:v, trap, write:v, zero_init
pub fn push[T:affine](v:rw<Vec[T]>, item:T)

pub fn pop[T:affine](v:rw<Vec[T]>) -> Option[T]  // effects: read:v, trap, write:v

// Put `item` at `i` and move the tail up by one; an index past the end is a guard failure.
// effects: alloc, diverge, ffi_precondition, free, local_read, local_write, read:v, trap, write:v, zero_init
pub fn insert[T:affine](v:rw<Vec[T]>, i:usize, item:T)

// Take the element at `i` out and close the gap, keeping the order of the rest.
pub fn remove[T:affine](v:rw<Vec[T]>, i:usize) -> Option[T]  // effects: read:v, trap, write:v

// Take the element at `i` out and move the last one into its place: one swap, no shift.
pub fn swap_remove[T:affine](v:rw<Vec[T]>, i:usize) -> Option[T]  // effects: read:v, trap, write:v

// The first index holding an element equal to `item`, by the element type's Eq.
// effects: diverge, ffi_precondition, local_read, local_write, read:item, read:v, stack_storage, trap, zero_init
pub fn find[T:Eq + affine](v:ro<Vec[T]>, item:ro<T>) -> Option[usize]

pub fn get[T:copy](v:ro<Vec[T]>, i:usize) -> T  // effects: read:v, trap
pub fn set[T:affine](v:rw<Vec[T]>, i:usize, item:T)  // effects: free, read:v, trap, write:v
pub fn clear[T:affine](v:rw<Vec[T]>)  // effects: free, read:v, trap, write:v

// Append a view. Copying elements, so it instantiates only for copyable ones; an owner would have to be moved out of
// the source view, which no borrow allows. Cost: amortized one pass over `src`, one guard for the part it lands in.
// effects: alloc, ffi_precondition, free, local_read, local_write, read:src, read:v, trap, write:v, zero_init
pub fn extend_from[T:copy](v:rw<Vec[T]>, n:usize, src:ro<T>[n]@host)

// Release the tail now instead of at the owner's scope exit; capacity is kept.
pub fn truncate[T:affine](v:rw<Vec[T]>, count:usize)  // effects: free, read:v, trap, write:v

// effects: diverge, ffi_precondition, local_read, local_write, read:a, read:b, stack_storage, trap, zero_init
impl Eq for Vec[T]: fn same[T:Eq + affine](a:ro<Vec[T]>, b:ro<Vec[T]>) -> bool

// effects: diverge, ffi_precondition, local_read, local_write, read:a, read:b, stack_storage, trap, zero_init
impl Ord for Vec[T]: fn less[T:Ord + affine](a:ro<Vec[T]>, b:ro<Vec[T]>) -> bool

// effects: diverge, ffi_precondition, local_read, local_write, read:value, stack_storage, trap, zero_init
impl Hash for Vec[T]: fn hash[T:Hash + affine](value:ro<Vec[T]>) -> u64

// The hash of a Vec holding `xs`, FNV-1a over its elements' own hashes, so a view finds the Vec that holds the same
// elements (map.find_view) without a Vec being made for it. Cost: one pass over `xs`.
// effects: diverge, ffi_precondition, local_read, local_write, read:xs, stack_storage, trap, zero_init
pub fn hash_view[T:Hash](n:usize, xs:ro<T>[n]@host) -> u64

A generic function's effects are what it may do for any arguments within its bounds, besides what their own trait members do.