pub trait GloballyCoherentLineageStore<M: MathsCore, H: Habitat<M>>: LocallyCoherentLineageStore<M, H> {
    type LocationIterator<'a>: Iterator<Item = Location>
       where M: 'a,
             Self: 'a;

    // Provided methods
    fn iter_active_locations(&self, habitat: &H) -> Self::LocationIterator<'_> { ... }
    fn get_local_lineage_references_at_location_unordered(
        &self,
        location: &Location,
        habitat: &H
    ) -> &[Self::LocalLineageReference] { ... }
    fn insert_lineage_globally_coherent(
        &mut self,
        lineage: Lineage,
        habitat: &H
    ) -> Self::LocalLineageReference { ... }
    fn extract_lineage_globally_coherent(
        &mut self,
        reference: Self::LocalLineageReference,
        habitat: &H
    ) -> Lineage { ... }
}

Required Associated Types§

source

type LocationIterator<'a>: Iterator<Item = Location> where M: 'a, Self: 'a

Provided Methods§

source

fn iter_active_locations(&self, habitat: &H) -> Self::LocationIterator<'_>

source

fn get_local_lineage_references_at_location_unordered( &self, location: &Location, habitat: &H ) -> &[Self::LocalLineageReference]

§Contracts

Pre-condition - debug: location is habitable

  • habitat.is_location_habitable(location)
source

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

§Contracts

Post-condition - debug: lineage is now indexed unordered at indexed_location.location()

  • self.get_local_lineage_references_at_location_unordered(&old(lineage.indexed_location.location().clone()), old(habitat)).last() == Some(&ret)

Post-condition - debug: unordered active lineage index at given location has grown by 1

  • old(self.get_local_lineage_references_at_location_unordered(lineage.indexed_location.location(), old(habitat)).len() + 1) == self.get_local_lineage_references_at_location_unordered(&old(lineage.indexed_location.location().clone()), old(habitat)).len()
source

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

§Contracts

Post-condition - debug: unordered active lineage index at returned location has shrunk by 1

  • self.get_local_lineage_references_at_location_unordered(ret.indexed_location.location(), old(habitat),).len() + 1 == old(self.get_local_lineage_references_at_location_unordered(self[&reference].indexed_location.location(), old(habitat),).len())

Object Safety§

This trait is not object safe.

Implementors§