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§
sourcefn get_global_lineage_reference_at_indexed_location(
&self,
indexed_location: &IndexedLocation,
habitat: &H
) -> Option<&GlobalLineageReference>
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)
sourcefn insert_lineage_locally_coherent(
&mut self,
lineage: Lineage,
habitat: &H
) -> Self::LocalLineageReference
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)
sourcefn extract_lineage_locally_coherent(
&mut self,
reference: Self::LocalLineageReference,
habitat: &H
) -> Lineage
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.