[−][src]Struct chalk_solve::rust_ir::AssociatedTyDatum
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
impl<I: Interner> AssociatedTyDatum<I>
[src]
pub fn bounds_on_self(&self, interner: &I) -> Vec<QuantifiedWhereClause<I>>
[src]
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
impl<I: Clone + Interner> Clone for AssociatedTyDatum<I> where
I::Identifier: Clone,
[src]
I::Identifier: Clone,
fn clone(&self) -> AssociatedTyDatum<I>
[src]
fn clone_from(&mut self, source: &Self)
1.0.0[src]
impl<I: Debug + Interner> Debug for AssociatedTyDatum<I> where
I::Identifier: Debug,
[src]
I::Identifier: Debug,
impl<I: Eq + Interner> Eq for AssociatedTyDatum<I> where
I::Identifier: Eq,
[src]
I::Identifier: Eq,
impl<I: Hash + Interner> Hash for AssociatedTyDatum<I> where
I::Identifier: Hash,
[src]
I::Identifier: Hash,
fn hash<__H: Hasher>(&self, state: &mut __H)
[src]
fn hash_slice<H>(data: &[Self], state: &mut H) where
H: Hasher,
1.3.0[src]
H: Hasher,
impl<I: PartialEq + Interner> PartialEq<AssociatedTyDatum<I>> for AssociatedTyDatum<I> where
I::Identifier: PartialEq,
[src]
I::Identifier: PartialEq,
fn eq(&self, other: &AssociatedTyDatum<I>) -> bool
[src]
fn ne(&self, other: &AssociatedTyDatum<I>) -> bool
[src]
impl<I: Interner> StructuralEq for AssociatedTyDatum<I>
[src]
impl<I: Interner> StructuralPartialEq for AssociatedTyDatum<I>
[src]
impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I>
[src]
fn to_program_clauses(
&self,
builder: &mut ClauseBuilder<'_, I>,
_environment: &Environment<I>
)
[src]
&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.
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>).
}
impl<I: Interner> Visit<I> for AssociatedTyDatum<I>
[src]
fn visit_with<'i, R: VisitResult>(
&self,
visitor: &mut dyn Visitor<'i, I, Result = R>,
outer_binder: DebruijnIndex
) -> R where
I: 'i,
[src]
&self,
visitor: &mut dyn Visitor<'i, I, Result = R>,
outer_binder: DebruijnIndex
) -> R where
I: 'i,
Auto Trait Implementations
impl<I> RefUnwindSafe for AssociatedTyDatum<I> where
<I as Interner>::DefId: RefUnwindSafe,
<I as Interner>::Identifier: RefUnwindSafe,
<I as Interner>::InternedGenericArg: RefUnwindSafe,
<I as Interner>::InternedLifetime: RefUnwindSafe,
<I as Interner>::InternedSubstitution: RefUnwindSafe,
<I as Interner>::InternedType: RefUnwindSafe,
<I as Interner>::InternedVariableKinds: RefUnwindSafe,
<I as Interner>::DefId: RefUnwindSafe,
<I as Interner>::Identifier: RefUnwindSafe,
<I as Interner>::InternedGenericArg: RefUnwindSafe,
<I as Interner>::InternedLifetime: RefUnwindSafe,
<I as Interner>::InternedSubstitution: RefUnwindSafe,
<I as Interner>::InternedType: RefUnwindSafe,
<I as Interner>::InternedVariableKinds: RefUnwindSafe,
impl<I> Send for AssociatedTyDatum<I> where
<I as Interner>::DefId: Send,
<I as Interner>::Identifier: Send,
<I as Interner>::InternedGenericArg: Send,
<I as Interner>::InternedLifetime: Send,
<I as Interner>::InternedSubstitution: Send,
<I as Interner>::InternedType: Send,
<I as Interner>::InternedVariableKinds: Send,
<I as Interner>::DefId: Send,
<I as Interner>::Identifier: Send,
<I as Interner>::InternedGenericArg: Send,
<I as Interner>::InternedLifetime: Send,
<I as Interner>::InternedSubstitution: Send,
<I as Interner>::InternedType: Send,
<I as Interner>::InternedVariableKinds: Send,
impl<I> Sync for AssociatedTyDatum<I> where
<I as Interner>::DefId: Sync,
<I as Interner>::Identifier: Sync,
<I as Interner>::InternedGenericArg: Sync,
<I as Interner>::InternedLifetime: Sync,
<I as Interner>::InternedSubstitution: Sync,
<I as Interner>::InternedType: Sync,
<I as Interner>::InternedVariableKinds: Sync,
<I as Interner>::DefId: Sync,
<I as Interner>::Identifier: Sync,
<I as Interner>::InternedGenericArg: Sync,
<I as Interner>::InternedLifetime: Sync,
<I as Interner>::InternedSubstitution: Sync,
<I as Interner>::InternedType: Sync,
<I as Interner>::InternedVariableKinds: Sync,
impl<I> Unpin for AssociatedTyDatum<I> where
<I as Interner>::DefId: Unpin,
<I as Interner>::Identifier: Unpin,
<I as Interner>::InternedGenericArg: Unpin,
<I as Interner>::InternedLifetime: Unpin,
<I as Interner>::InternedSubstitution: Unpin,
<I as Interner>::InternedType: Unpin,
<I as Interner>::InternedVariableKinds: Unpin,
<I as Interner>::DefId: Unpin,
<I as Interner>::Identifier: Unpin,
<I as Interner>::InternedGenericArg: Unpin,
<I as Interner>::InternedLifetime: Unpin,
<I as Interner>::InternedSubstitution: Unpin,
<I as Interner>::InternedType: Unpin,
<I as Interner>::InternedVariableKinds: Unpin,
impl<I> UnwindSafe for AssociatedTyDatum<I> where
<I as Interner>::DefId: UnwindSafe,
<I as Interner>::Identifier: UnwindSafe,
<I as Interner>::InternedGenericArg: UnwindSafe,
<I as Interner>::InternedLifetime: UnwindSafe,
<I as Interner>::InternedSubstitution: UnwindSafe,
<I as Interner>::InternedType: UnwindSafe,
<I as Interner>::InternedVariableKinds: UnwindSafe,
<I as Interner>::DefId: UnwindSafe,
<I as Interner>::Identifier: UnwindSafe,
<I as Interner>::InternedGenericArg: UnwindSafe,
<I as Interner>::InternedLifetime: UnwindSafe,
<I as Interner>::InternedSubstitution: UnwindSafe,
<I as Interner>::InternedType: UnwindSafe,
<I as Interner>::InternedVariableKinds: UnwindSafe,
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Cast for T
[src]
fn cast<U>(self, interner: &<U as HasInterner>::Interner) -> U where
Self: CastTo<U>,
U: HasInterner,
[src]
Self: CastTo<U>,
U: HasInterner,
impl<Q, K> Equivalent<K> for Q where
K: Borrow<Q> + ?Sized,
Q: Eq + ?Sized,
[src]
K: Borrow<Q> + ?Sized,
Q: Eq + ?Sized,
fn equivalent(&self, key: &K) -> bool
[src]
impl<T> From<T> for T
[src]
impl<T> Instrument for T
[src]
fn instrument(self, span: Span) -> Instrumented<Self>
[src]
fn in_current_span(self) -> Instrumented<Self>
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T, I> VisitExt<I> for T where
I: Interner,
T: Visit<I>,
[src]
I: Interner,
T: Visit<I>,