Struct chalk_solve::rust_ir::AssociatedTyDatum [−][src]
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
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: PartialEq + Interner> PartialEq<AssociatedTyDatum<I>> for AssociatedTyDatum<I> where
I::Identifier: PartialEq,
impl<I: PartialEq + Interner> PartialEq<AssociatedTyDatum<I>> for AssociatedTyDatum<I> where
I::Identifier: PartialEq,
This method tests for self
and other
values to be equal, and is used
by ==
. Read more
This method tests for !=
.
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.
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>).
}
fn visit_with<'i, B>(
&self,
visitor: &mut dyn Visitor<'i, I, BreakTy = B>,
outer_binder: DebruijnIndex
) -> ControlFlow<B> where
I: 'i,
fn visit_with<'i, B>(
&self,
visitor: &mut dyn Visitor<'i, I, BreakTy = B>,
outer_binder: DebruijnIndex
) -> ControlFlow<B> where
I: 'i,
Apply the given visitor 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. Read more
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,
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,
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,
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,
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,
Blanket Implementations
Mutably borrows from an owned value. Read more
fn cast<U>(self, interner: &<U as HasInterner>::Interner) -> U where
Self: CastTo<U>,
U: HasInterner,
fn cast<U>(self, interner: &<U as HasInterner>::Interner) -> U where
Self: CastTo<U>,
U: HasInterner,
Cast a value to type U
using CastTo
.
Compare self to key
and return true
if they are equal.
Instruments this type with the provided Span
, returning an
Instrumented
wrapper. Read more