Struct AssocReftId

#[non_exhaustive]
pub struct AssocReftId<Id = DefId> {
    pub container_id: Id,
    pub name: Symbol,
}

An id for an associated refinement with a type-level invariant ensuring that it exists.

We represent the id as a container id and an arbitrary name. This doesn’t guarantee the existence of the associated refinement, so we must be careful when creating instances of this struct.

We mark the struct as non_exhaustive to make it harder to create one by mistake without calling AssocReftId::new. We also have a clippy lint disallowing AssocReftId::new which can be disabled selectively when we can ensure the associated refinement exists.

The struct is generic on the container Id because we use it with various kinds of ids, e.g., DefId, [MaybeExternId], …

Fields (Non-exhaustive)

Non-exhaustive structs could have additional fields added in future. Therefore, non-exhaustive structs cannot be constructed in external crates using the traditional Struct { .. } syntax; cannot be matched against without a wildcard ..; and struct update syntax will not work.

container_id: Id

Id of the container, i.e., the impl block or trait.

name: Symbol

Name of the associated refinement

Implementations

impl<Id> AssocReftId<Id>

pub fn new(container_id: Id, name: Symbol) -> Self

impl AssocReftId

pub fn index(self) -> AssocReftId<DefIndex>

Trait Implementations

impl<Id: Clone> Clone for AssocReftId<Id>

fn clone(&self) -> AssocReftId<Id>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<Id, __D: SpanDecoder> Decodable<__D> for AssocReftId<Id>

where Id: Decodable<__D>,

fn decode(__decoder: &mut __D) -> Self

impl<Id, __E: SpanEncoder> Encodable<__E> for AssocReftId<Id>

where Id: Encodable<__E>,

fn encode(&self, __encoder: &mut __E)

impl<Id: Hash> Hash for AssocReftId<Id>

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl<Id: PartialEq> PartialEq for AssocReftId<Id>

fn eq(&self, other: &AssocReftId<Id>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl SliceInternable for AssocReftId

fn storage() -> &'static InternStorage<[Self]>

impl<Id> TypeFoldable for AssocReftId<Id>

where Id: TypeFoldable,

fn try_fold_with<__F: FallibleTypeFolder>( &self, __folder: &mut __F, ) -> Result<Self, __F::Error>

fn fold_with<F: TypeFolder>(&self, folder: &mut F) -> Self

fn normalize(&self, defns: &SpecFuncDefns) -> Self

Normalize expressions by applying beta reductions for tuples and lambda abstractions.

fn replace_holes( &self, f: impl FnMut(&[BoundVariableKinds], HoleKind) -> Expr, ) -> Self

Replaces all holes with the result of calling a closure. The closure takes a list with all the layers of bound variables at the point the hole was found. Each layer corresponds to the list of bound variables at that level. The list is ordered from outermost to innermost binder, i.e., the last element is the binder closest to the hole.

fn with_holes(&self) -> Self

Remove all refinements and turn each underlying BaseTy into a TyKind::Exists with a TyKind::Constr and a hole. For example, Vec<{v. i32[v] | v > 0}>[n] becomes {n. Vec<{v. i32[v] | *}>[n] | *}.

fn replace_evars( &self, f: &mut impl FnMut(EVid) -> Option<Expr>, ) -> Result<Self, EVid>

fn shift_in_escaping(&self, amount: u32) -> Self

fn shift_out_escaping(&self, amount: u32) -> Self

fn erase_regions(&self) -> Self

impl<Id> TypeVisitable for AssocReftId<Id>

where Id: TypeVisitable,

fn visit_with<__V: TypeVisitor>( &self, __visitor: &mut __V, ) -> ControlFlow<__V::BreakTy>

fn has_escaping_bvars(&self) -> bool

fn has_escaping_bvars_at_or_above(&self, binder: DebruijnIndex) -> bool

Returns true if self has any late-bound vars that are either bound by binder or bound by some binder outside of binder. If binder is ty::INNERMOST, this indicates whether there are any late-bound vars that appear free.

fn fvars(&self) -> FxHashSet<Name>

Returns the set of all free variables. For example, Vec<i32[n]>{v : v > m} returns {n, m}.

impl<Id: Copy> Copy for AssocReftId<Id>

impl<Id: Eq> Eq for AssocReftId<Id>

impl<Id> StructuralPartialEq for AssocReftId<Id>