Struct chalk_solve::rust_ir::AssociatedTyDatum
source · pub struct AssociatedTyDatum<I: Interner> {
pub trait_id: TraitId<I>,
pub id: AssocTypeId<I>,
pub name: I::Identifier,
pub binders: Binders<AssociatedTyDatumBound<I>>,
}
Expand description
Represents an associated type declaration found inside of a trait:
trait Foo<P1..Pn> { // P0 is Self
type Bar<Pn..Pm>: [bounds]
where
[where_clauses];
}
The meaning of each of these parts:
- The parameters
P0...Pm
are all in scope for this associated type. - The bounds
bounds
are things that the impl must prove to be true. - The where clauses
where_clauses
are things that the impl can assume to be true (but which projectors must prove).
Fields§
§trait_id: TraitId<I>
The trait this associated type is defined in.
id: AssocTypeId<I>
The ID of this associated type
name: I::Identifier
Name of this associated type.
binders: Binders<AssociatedTyDatumBound<I>>
These binders represent the P0...Pm
variables. The binders
are in the order [Pn..Pm; P0..Pn]
. That is, the variables
from Bar
come first (corresponding to the de bruijn concept
that “inner” binders are lower indices, although within a
given binder we do not have an ordering).
Implementations§
source§impl<I: Interner> AssociatedTyDatum<I>
impl<I: Interner> AssociatedTyDatum<I>
sourcepub fn bounds_on_self(&self, interner: I) -> Vec<QuantifiedWhereClause<I>>
pub fn bounds_on_self(&self, interner: I) -> Vec<QuantifiedWhereClause<I>>
Returns the associated ty’s bounds applied to the projection type, e.g.:
Implemented(<?0 as Foo>::Item<?1>: Sized)
these quantified where clauses are in the scope of the
binders
field.
Trait Implementations§
source§impl<I: Clone + Interner> Clone for AssociatedTyDatum<I>where
I::Identifier: Clone,
impl<I: Clone + Interner> Clone for AssociatedTyDatum<I>where
I::Identifier: Clone,
source§fn clone(&self) -> AssociatedTyDatum<I>
fn clone(&self) -> AssociatedTyDatum<I>
1.0.0 · source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
source
. Read moresource§impl<I: Debug + Interner> Debug for AssociatedTyDatum<I>where
I::Identifier: Debug,
impl<I: Debug + Interner> Debug for AssociatedTyDatum<I>where
I::Identifier: Debug,
source§impl<I: Hash + Interner> Hash for AssociatedTyDatum<I>where
I::Identifier: Hash,
impl<I: Hash + Interner> Hash for AssociatedTyDatum<I>where
I::Identifier: Hash,
source§impl<I: PartialEq + Interner> PartialEq for AssociatedTyDatum<I>where
I::Identifier: PartialEq,
impl<I: PartialEq + Interner> PartialEq for AssociatedTyDatum<I>where
I::Identifier: PartialEq,
source§fn eq(&self, other: &AssociatedTyDatum<I>) -> bool
fn eq(&self, other: &AssociatedTyDatum<I>) -> bool
self
and other
values to be equal, and is used
by ==
.source§impl<I: Interner> RenderAsRust<I> for AssociatedTyDatum<I>
impl<I: Interner> RenderAsRust<I> for AssociatedTyDatum<I>
fn fmt(&self, s: &InternalWriterState<'_, I>, f: &mut Formatter<'_>) -> Result
fn display<'a>(
&'a self,
s: &'a InternalWriterState<'a, I>,
) -> DisplayRenderAsRust<'a, I, Self>where
Self: Sized,
source§impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I>
impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I>
source§fn to_program_clauses(
&self,
builder: &mut ClauseBuilder<'_, I>,
_environment: &Environment<I>,
)
fn to_program_clauses( &self, builder: &mut ClauseBuilder<'_, I>, _environment: &Environment<I>, )
For each associated type, we define the “projection equality” rules. There are always two; one for a successful normalization, and one for the “fallback” notion of equality.
Given: (here, 'a
and T
represent zero or more parameters)
trait Foo {
type Assoc<'a, T>: Bounds where WC;
}
we generate the ‘fallback’ rule:
-- Rule AliasEq-Placeholder
forall<Self, 'a, T> {
AliasEq(<Self as Foo>::Assoc<'a, T> = (Foo::Assoc<'a, T>)<Self>).
}
and
-- Rule AliasEq-Normalize
forall<Self, 'a, T, U> {
AliasEq(<T as Foo>::Assoc<'a, T> = U) :-
Normalize(<T as Foo>::Assoc -> U).
}
We used to generate an “elaboration” rule like this:
forall<T> {
T: Foo :- exists<U> { AliasEq(<T as Foo>::Assoc = U) }.
}
but this caused problems with the recursive solver. In
particular, whenever normalization is possible, we cannot
solve that projection uniquely, since we can now elaborate
AliasEq
to fallback or normalize it. So instead we
handle this kind of reasoning through the FromEnv
predicate.
Another set of clauses we generate for each associated type is about placeholder associated
types (i.e. TyKind::AssociatedType
). Given
trait Foo {
type Assoc<'a, T>: Bar<U = Ty> where WC;
}
we generate
forall<Self, 'a, T> {
Implemented((Foo::Assoc<'a, T>)<Self>: Bar) :- WC.
AliasEq(<<(Foo::Assoc<'a, T>)<Self>> as Bar>::U = Ty) :- WC.
}
We also generate rules specific to WF requirements and implied bounds:
-- Rule WellFormed-AssocTy
forall<Self, 'a, T> {
WellFormed((Foo::Assoc)<Self, 'a, T>) :- WellFormed(Self: Foo), WellFormed(WC).
}
-- Rule Implied-WC-From-AssocTy
forall<Self, 'a, T> {
FromEnv(WC) :- FromEnv((Foo::Assoc)<Self, 'a, T>).
}
-- Rule Implied-Bound-From-AssocTy
forall<Self, 'a, T> {
FromEnv(<Self as Foo>::Assoc<'a,T>: Bounds) :- FromEnv(Self: Foo), WC.
}
-- Rule Implied-Trait-From-AssocTy
forall<Self,'a, T> {
FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)<Self, 'a,T>).
}
source§impl<I: Interner> TypeVisitable<I> for AssociatedTyDatum<I>
impl<I: Interner> TypeVisitable<I> for AssociatedTyDatum<I>
source§fn visit_with<B>(
&self,
visitor: &mut dyn TypeVisitor<I, BreakTy = B>,
outer_binder: DebruijnIndex,
) -> ControlFlow<B>
fn visit_with<B>( &self, visitor: &mut dyn TypeVisitor<I, BreakTy = B>, outer_binder: DebruijnIndex, ) -> ControlFlow<B>
visitor
to self
; binders
is the
number of binders that are in scope when beginning the
visitor. Typically binders
starts as 0, but is adjusted when
we encounter Binders<T>
in the IR or other similar
constructs.impl<I: Eq + Interner> Eq for AssociatedTyDatum<I>where
I::Identifier: Eq,
impl<I: Interner> StructuralPartialEq for AssociatedTyDatum<I>
Auto Trait Implementations§
impl<I> Freeze for AssociatedTyDatum<I>where
<I as Interner>::Identifier: Freeze,
<I as Interner>::DefId: Freeze,
<I as Interner>::InternedVariableKinds: Freeze,
impl<I> RefUnwindSafe for AssociatedTyDatum<I>where
<I as Interner>::Identifier: RefUnwindSafe,
<I as Interner>::DefId: RefUnwindSafe,
<I as Interner>::InternedVariableKinds: RefUnwindSafe,
<I as Interner>::InternedType: RefUnwindSafe,
<I as Interner>::InternedSubstitution: RefUnwindSafe,
<I as Interner>::InternedLifetime: RefUnwindSafe,
<I as Interner>::InternedGenericArg: RefUnwindSafe,
impl<I> Send for AssociatedTyDatum<I>where
<I as Interner>::Identifier: Send,
<I as Interner>::DefId: Send,
<I as Interner>::InternedVariableKinds: Send,
<I as Interner>::InternedType: Send,
<I as Interner>::InternedSubstitution: Send,
<I as Interner>::InternedLifetime: Send,
<I as Interner>::InternedGenericArg: Send,
impl<I> Sync for AssociatedTyDatum<I>where
<I as Interner>::Identifier: Sync,
<I as Interner>::DefId: Sync,
<I as Interner>::InternedVariableKinds: Sync,
<I as Interner>::InternedType: Sync,
<I as Interner>::InternedSubstitution: Sync,
<I as Interner>::InternedLifetime: Sync,
<I as Interner>::InternedGenericArg: Sync,
impl<I> Unpin for AssociatedTyDatum<I>where
<I as Interner>::Identifier: Unpin,
<I as Interner>::DefId: Unpin,
<I as Interner>::InternedVariableKinds: Unpin,
<I as Interner>::InternedType: Unpin,
<I as Interner>::InternedSubstitution: Unpin,
<I as Interner>::InternedLifetime: Unpin,
<I as Interner>::InternedGenericArg: Unpin,
impl<I> UnwindSafe for AssociatedTyDatum<I>where
<I as Interner>::Identifier: UnwindSafe,
<I as Interner>::DefId: UnwindSafe,
<I as Interner>::InternedVariableKinds: UnwindSafe,
<I as Interner>::InternedType: UnwindSafe,
<I as Interner>::InternedSubstitution: UnwindSafe,
<I as Interner>::InternedLifetime: UnwindSafe,
<I as Interner>::InternedGenericArg: UnwindSafe,
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
source§impl<T> Cast for T
impl<T> Cast for T
source§fn cast<U>(self, interner: <U as HasInterner>::Interner) -> Uwhere
Self: CastTo<U>,
U: HasInterner,
fn cast<U>(self, interner: <U as HasInterner>::Interner) -> Uwhere
Self: CastTo<U>,
U: HasInterner,
U
using CastTo
.source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
source§default unsafe fn clone_to_uninit(&self, dst: *mut T)
default unsafe fn clone_to_uninit(&self, dst: *mut T)
clone_to_uninit
)§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
key
and return true
if they are equal.