Trait chalk_solve::infer::ucanonicalize::UniverseMapExt

pub trait UniverseMapExt {
    // Required methods
    fn add(&mut self, universe: UniverseIndex);
    fn map_universe_to_canonical(
        &self,
        universe: UniverseIndex,
    ) -> Option<UniverseIndex>;
    fn map_universe_from_canonical(
        &self,
        universe: UniverseIndex,
    ) -> UniverseIndex;
    fn map_from_canonical<T, I>(
        &self,
        interner: I,
        canonical_value: &Canonical<T>,
    ) -> Canonical<T>
       where T: Clone + TypeFoldable<I> + HasInterner<Interner = I>,
             I: Interner;
}

Required Methods

fn add(&mut self, universe: UniverseIndex)

fn map_universe_to_canonical( &self, universe: UniverseIndex, ) -> Option<UniverseIndex>

fn map_universe_from_canonical(&self, universe: UniverseIndex) -> UniverseIndex

fn map_from_canonical<T, I>( &self, interner: I, canonical_value: &Canonical<T>, ) -> Canonical<T>

where T: Clone + TypeFoldable<I> + HasInterner<Interner = I>, I: Interner,

Object Safety

This trait is not object safe.

Implementations on Foreign Types

impl UniverseMapExt for UniverseMap

fn map_universe_to_canonical( &self, universe: UniverseIndex, ) -> Option<UniverseIndex>

Given a universe U that appeared in our original value, return the universe to use in the u-canonical value. This is done by looking for the index I of U in self.universes. We will return the universe with “counter” I. This effectively “compresses” the range of universes to things from 0..self.universes.len(). If the universe is not present in the map, we return None.

fn map_universe_from_canonical(&self, universe: UniverseIndex) -> UniverseIndex

Given a “canonical universe” – one found in the u_canonicalize result – returns the original universe that it corresponded to.

fn map_from_canonical<T, I>( &self, interner: I, canonical_value: &Canonical<T>, ) -> Canonical<T>

where T: Clone + TypeFoldable<I> + HasInterner<Interner = I>, I: Interner,

Returns a mapped version of value where the universes have been translated from canonical universes into the original universes.

In some cases, value may contain fresh universes that are not described in the original map. This occurs when we return region constraints – for example, if we were to process a constraint like for<'a> 'a == 'b, where 'b is an inference variable, that would generate a region constraint that !2 == ?0. (This constraint is typically not, as it happens, satisfiable, but it may be, depending on the bounds on !2.) In effect, there is a “for all” binder around the constraint, but it is not represented explicitly – only implicitly, by the presence of a U2 variable.

If we encounter universes like this, which are “out of bounds” from our original set of universes, we map them to a distinct universe in the original space that is greater than all the other universes in the map. That is, if we encounter a canonical universe Ux where our canonical vector is (say) [U0, U3], we would compute the difference d = x - 2 and then return the universe 3 + d + 1.

The important thing is that we preserve (a) the relative order of universes, since that determines visibility, and (b) that the universe we produce does not correspond to any of the other original universes.

fn add(&mut self, universe: UniverseIndex)

Implementors