Trait stable_vec::core::Core

pub trait Core<T> {
    // Required methods
    fn new() -> Self;
    fn len(&self) -> usize;
    unsafe fn set_len(&mut self, new_len: usize);
    fn cap(&self) -> usize;
    unsafe fn realloc(&mut self, new_cap: usize);
    unsafe fn has_element_at(&self, idx: usize) -> bool;
    unsafe fn insert_at(&mut self, idx: usize, elem: T);
    unsafe fn remove_at(&mut self, idx: usize) -> T;
    unsafe fn get_unchecked(&self, idx: usize) -> &T;
    unsafe fn get_unchecked_mut(&mut self, idx: usize) -> &mut T;
    fn clear(&mut self);
    unsafe fn swap(&mut self, a: usize, b: usize);

    // Provided methods
    unsafe fn first_filled_slot_from(&self, idx: usize) -> Option<usize> { ... }
    unsafe fn first_filled_slot_below(&self, idx: usize) -> Option<usize> { ... }
    unsafe fn first_empty_slot_from(&self, idx: usize) -> Option<usize> { ... }
    unsafe fn first_empty_slot_below(&self, idx: usize) -> Option<usize> { ... }
}

The core of a stable vector.

Note: If you are a user of this crate, you probably don’t care about this! See the documentation on StableVecFacade and the different core implementations for more useful information. This trait is only important for you if you want to implement your own core implementation.

Implementors of the trait take the core role in the stable vector: storing elements of type T where each element might be deleted. The elements can be referred to by an index.

Core types must never read deleted elements in drop(). So they must ensure to only ever drop existing elements.

Formal semantics

A core defines a map from usize (the so called “indices”) to elements of type Option<T>. It has a length (len) and a capacity (cap).

It’s best to think of this as a contiguous sequence of “slots”. A slot can either be empty or filled with an element. A core has always cap many slots. Here is an example of such a core with len = 8 and cap = 10.

     0   1   2   3   4   5   6   7   8   9   10
   ┌───┬───┬───┬───┬───┬───┬───┬───┬───┬───┐
   │ a │ - │ b │ c │ - │ - │ d │ - │ - │ - │
   └───┴───┴───┴───┴───┴───┴───┴───┴───┴───┘
                                     ↑       ↑
                                    len     cap

len and cap divide the index space into three parts, which have the following invariants:

• 0 ≤ i < len: slots with index i can be empty or filled
• len ≤ i < cap: slots with index i are always empty
• cap ≤ i: slots with index i are undefined (all methods dealing with indices will exhibit undefined behavior when the index is ≥ cap)

Additional required invariants:

• len ≤ cap
• cap ≤ isize::MAX
• Methods with &self receiver do not change anything observable about the core.

These invariants must not (at any time) be violated by users of this API.

Cloning a core must clone everything, including all empty slots. This means that the capacity of the clone must be at least the capacity of the original value.

Required Methods

fn new() -> Self

Creates an empty instance without any elements. Must not allocate memory.

Formal

Postconditons (of returned instance out):

• out.len() == 0
• out.cap() == 0

fn len(&self) -> usize

Returns the length of this core (the len). See the trait docs for more information.

unsafe fn set_len(&mut self, new_len: usize)

Sets the len to a new value.

Formal

Preconditions:

• new_len ≤ self.cap()
• ∀ i in new_len..self.cap() ⇒ self.has_element_at(i) == false

Invariants:

• slot data

Postconditons:

• self.len() == new_len

fn cap(&self) -> usize

Returns the capacity of this core (the cap). See the trait docs for more information.

unsafe fn realloc(&mut self, new_cap: usize)

Reallocates the memory to have a cap of at least new_cap. This method should try its best to allocate exactly new_cap.

This means that after calling this method, inserting elements at indices in the range 0..new_cap is valid. This method shall not check if there is already enough capacity available.

For implementors: please mark this impl with #[cold] and #[inline(never)].

Formal

Preconditions:

• new_cap ≥ self.len() (as a consequence, this method does not (need to) drop elements; all slots >= new_cap are empty)
• new_cap ≤ isize::MAX

Invariants:

• slot data
• self.len()

Postconditons:

• self.cap() >= new_cap

unsafe fn has_element_at(&self, idx: usize) -> bool

Checks if there exists an element with index idx.

Formal

Preconditions:

• idx < self.cap()

unsafe fn insert_at(&mut self, idx: usize, elem: T)

Inserts elem at the index idx. Does not updated the used_len.

Formal

Preconditions:

• idx < self.cap()
• self.has_element_at(idx) == false

Invariants:

• self.len()
• self.cap()

Postconditons:

• self.get_unchecked(idx) == elem

unsafe fn remove_at(&mut self, idx: usize) -> T

Removes the element at index idx and returns it.

Formal

Preconditions:

• idx < self.cap()
• self.has_element_at(idx) == true

Invariants:

• self.len()
• self.cap()

Postconditons:

• self.has_element_at(idx) == false

unsafe fn get_unchecked(&self, idx: usize) -> &T

Returns a reference to the element at the index idx.

Formal

Preconditions:

• idx < self.cap()
• self.has_element_at(idx) == true (implying idx < self.len())

unsafe fn get_unchecked_mut(&mut self, idx: usize) -> &mut T

Returns a mutable reference to the element at the index idx.

Formal

Preconditions:

• idx < self.cap()
• self.has_element_at(idx) == true (implying idx < self.len())

fn clear(&mut self)

Deletes all elements without deallocating memory. Drops all existing elements. Sets len to 0.

Formal

Invariants:

• self.cap()

Postconditons:

• self.len() == 0 (implying all slots are empty)

unsafe fn swap(&mut self, a: usize, b: usize)

Swaps the two slots with indices a and b. That is: the element and the “filled/empty” status are swapped. The slots at indices a and b can be empty or filled.

Formal

Preconditions:

• a < self.cap()
• b < self.cap()

Invariants:

• self.len()
• self.cap()

Postconditons (with before being self before the call):

• before.has_element_at(a) == self.has_element_at(b)
• before.has_element_at(b) == self.has_element_at(a)
• if self.has_element_at(a):
  • self.get_unchecked(a) == before.get_unchecked(b)
• if self.has_element_at(b):
  • self.get_unchecked(b) == before.get_unchecked(a)

Provided Methods

unsafe fn first_filled_slot_from(&self, idx: usize) -> Option<usize>

Performs a forwards search starting at index idx, returning the index of the first filled slot that is found.

Specifically, if an element at index idx exists, Some(idx) is returned.

The inputs idx >= self.len() are only allowed for convenience and because it doesn’t make the implementation more complicated. For those idx values, None is always returned.

Formal

Preconditions:

• idx ≤ self.cap()

Postconditons (for return value out):

• if out == None:
  • ∀ i in idx..self.len() ⇒ self.has_element_at(i) == false
• if out == Some(j):
  • ∀ i in idx..j ⇒ self.has_element_at(i) == false
  • self.has_element_at(j) == true

unsafe fn first_filled_slot_below(&self, idx: usize) -> Option<usize>

Performs a backwards search starting at index idx - 1, returning the index of the first filled slot that is found.

Note: passing in idx >= self.len() just wastes time, as those slots are never filled.

Formal

Preconditions:

• idx <= self.cap()

Postconditons (for return value out):

• if out == None:
  • ∀ i in 0..idx ⇒ self.has_element_at(i) == false
• if out == Some(j):
  • ∀ i in j + 1..idx ⇒ self.has_element_at(i) == false
  • self.has_element_at(j) == true

unsafe fn first_empty_slot_from(&self, idx: usize) -> Option<usize>

Performs a forwards search starting at index idx, returning the index of the first empty slot that is found.

Formal

Preconditions:

• idx ≤ self.cap()

Postconditons (for return value out):

• if out == None:
  • ∀ i in idx..self.len() ⇒ self.has_element_at(i) == true
• if out == Some(j):
  • ∀ i in idx..j ⇒ self.has_element_at(i) == true
  • self.has_element_at(j) == false

unsafe fn first_empty_slot_below(&self, idx: usize) -> Option<usize>

Performs a backwards search starting at index idx - 1, returning the index of the first empty slot that is found.

If idx > self.len(), Some(idx) is always returned (remember the preconditions tho!).

Formal

Preconditions:

• idx <= self.cap() (note: strictly smaller)

Postconditons (for return value out):

• if out == None:
  • ∀ i in 0..=idx ⇒ self.has_element_at(i) == true
• if out == Some(j):
  • ∀ i in j + 1..=idx ⇒ self.has_element_at(i) == true
  • self.has_element_at(j) == false

Object Safety

This trait is not object safe.

Implementors

impl<T> Core<T> for BitVecCore<T>

impl<T> Core<T> for OptionCore<T>