pub trait LocallyCoherentLineageStore<M: MathsCore, H: Habitat<M>>: LineageStore<M, H> + for<'a> Index<&'a Self::LocalLineageReference, Output = Lineage> {
    // Provided methods
    fn get_global_lineage_reference_at_indexed_location(
        &self,
        indexed_location: &IndexedLocation,
        habitat: &H
    ) -> Option<&GlobalLineageReference> { ... }
    fn insert_lineage_locally_coherent(
        &mut self,
        lineage: Lineage,
        habitat: &H
    ) -> Self::LocalLineageReference { ... }
    fn extract_lineage_locally_coherent(
        &mut self,
        reference: Self::LocalLineageReference,
        habitat: &H
    ) -> Lineage { ... }
}

Provided Methods§

source

fn get_global_lineage_reference_at_indexed_location( &self, indexed_location: &IndexedLocation, habitat: &H ) -> Option<&GlobalLineageReference>

§Contracts

Pre-condition - debug: indexed location is habitable

  • habitat.is_indexed_location_habitable(indexed_location)
source

fn insert_lineage_locally_coherent( &mut self, lineage: Lineage, habitat: &H ) -> Self::LocalLineageReference

§Contracts

Pre-condition - debug: indexed location is habitable

  • habitat.is_indexed_location_habitable(&lineage.indexed_location)

Post-condition - debug: lineage was activated

  • self.get_lineage_for_local_reference(&ret).is_some()

Post-condition - debug: lineage was added to indexed_location

  • self [&ret].indexed_location == old(lineage.indexed_location.clone())

Post-condition - debug: lineage is now indexed at indexed_location

  • self.get_global_lineage_reference_at_indexed_location(&old(lineage.indexed_location.clone()), old(habitat)) == Some(&self[&ret].global_reference)
source

fn extract_lineage_locally_coherent( &mut self, reference: Self::LocalLineageReference, habitat: &H ) -> Lineage

§Contracts

Pre-condition - debug: lineage is active

  • self.get_lineage_for_local_reference(&reference).is_some()

Post-condition - debug: prior indexed location is habitable

  • old(habitat).is_indexed_location_habitable(&ret.indexed_location)

Post-condition - debug: lineage was deactivated

  • self.get_lineage_for_local_reference(&old(unsafe { crate::cogs::Backup::backup_unchecked(&reference) })).is_none()

Post-condition - debug: returns the individual corresponding to reference

  • ret == old(self[&reference].clone())

Post-condition - debug: lineage is no longer indexed at its prior IndexedLocation

  • self.get_global_lineage_reference_at_indexed_location(&ret.indexed_location, old(habitat)).is_none()

Object Safety§

This trait is not object safe.

Implementors§