Struct chalk_solve::infer::unify::Unifier
source · struct Unifier<'t, I: Interner> {
table: &'t mut InferenceTable<I>,
environment: &'t Environment<I>,
goals: Vec<InEnvironment<Goal<I>>>,
interner: I,
db: &'t dyn UnificationDatabase<I>,
}
Fields§
§table: &'t mut InferenceTable<I>
§environment: &'t Environment<I>
§goals: Vec<InEnvironment<Goal<I>>>
§interner: I
§db: &'t dyn UnificationDatabase<I>
Implementations§
source§impl<'t, I: Interner> Unifier<'t, I>
impl<'t, I: Interner> Unifier<'t, I>
fn new( interner: I, db: &'t dyn UnificationDatabase<I>, table: &'t mut InferenceTable<I>, environment: &'t Environment<I>, ) -> Self
sourcefn relate<T>(
self,
variance: Variance,
a: &T,
b: &T,
) -> Fallible<RelationResult<I>>
fn relate<T>( self, variance: Variance, a: &T, b: &T, ) -> Fallible<RelationResult<I>>
The main entry point for the Unifier
type and really the
only type meant to be called externally. Performs a
relation of a
and b
and returns the Unification Result.
sourcefn relate_ty_ty(
&mut self,
variance: Variance,
a: &Ty<I>,
b: &Ty<I>,
) -> Fallible<()>
fn relate_ty_ty( &mut self, variance: Variance, a: &Ty<I>, b: &Ty<I>, ) -> Fallible<()>
Relate a
, b
with the variance such that if variance = Covariant
, a
is
a subtype of b
.
sourcefn unify_var_var(&mut self, a: InferenceVar, b: InferenceVar) -> Fallible<()>
fn unify_var_var(&mut self, a: InferenceVar, b: InferenceVar) -> Fallible<()>
Unify two inference variables
sourcefn unify_general_var_specific_ty(
&mut self,
general_var: InferenceVar,
specific_ty: Ty<I>,
) -> Fallible<()>
fn unify_general_var_specific_ty( &mut self, general_var: InferenceVar, specific_ty: Ty<I>, ) -> Fallible<()>
Unify a general inference variable with a specific inference variable
(type kind is not General
). For example, unify a TyVariableKind::General
inference variable with a TyVariableKind::Integer
variable, resulting in the
general inference variable narrowing to an integer variable.
fn relate_binders<'a, T>( &mut self, variance: Variance, a: &Binders<T>, b: &Binders<T>, ) -> Fallible<()>
sourcefn relate_alias_ty(
&mut self,
variance: Variance,
alias: &AliasTy<I>,
ty: &Ty<I>,
) -> Fallible<()>
fn relate_alias_ty( &mut self, variance: Variance, alias: &AliasTy<I>, ty: &Ty<I>, ) -> Fallible<()>
Relate an alias like <T as Trait>::Item
or impl Trait
with some other
type ty
. If the variance is Invariant
, creates a goal like
AliasEq(<T as Trait>::Item = U) // associated type projection
AliasEq(impl Trait = U) // impl trait
Otherwise, this creates a new variable ?X
, creates a goal like
AliasEq(Alias = ?X)
and relates ?X
and ty
.
fn generalize_ty( &mut self, ty: &Ty<I>, universe_index: UniverseIndex, variance: Variance, ) -> Ty<I>
fn generalize_lifetime( &mut self, lifetime: &Lifetime<I>, universe_index: UniverseIndex, variance: Variance, ) -> Lifetime<I>
fn generalize_const( &mut self, const_: &Const<I>, universe_index: UniverseIndex, ) -> Const<I>
fn generalize_generic_var( &mut self, sub_var: &GenericArg<I>, universe_index: UniverseIndex, variance: Variance, ) -> GenericArg<I>
sourcefn generalize_substitution_skip_self<F: Fn(usize) -> Option<Variance>>(
&mut self,
substitution: &Substitution<I>,
universe_index: UniverseIndex,
get_variance: F,
) -> Substitution<I>
fn generalize_substitution_skip_self<F: Fn(usize) -> Option<Variance>>( &mut self, substitution: &Substitution<I>, universe_index: UniverseIndex, get_variance: F, ) -> Substitution<I>
Generalizes all but the first
fn generalize_substitution<F: Fn(usize) -> Variance>( &mut self, substitution: &Substitution<I>, universe_index: UniverseIndex, get_variance: F, ) -> Substitution<I>
sourcefn relate_var_ty(
&mut self,
variance: Variance,
var: InferenceVar,
var_kind: TyVariableKind,
ty: &Ty<I>,
) -> Fallible<()>
fn relate_var_ty( &mut self, variance: Variance, var: InferenceVar, var_kind: TyVariableKind, ty: &Ty<I>, ) -> Fallible<()>
Unify an inference variable var
with some non-inference
variable ty
, just bind var
to ty
. But we must enforce two conditions:
var
does not appear inside ofty
(the standardOccursCheck
)ty
does not reference anything in a lifetime that could not be named invar
(the extendedOccursCheck
created to handle universes)
fn relate_lifetime_lifetime( &mut self, variance: Variance, a: &Lifetime<I>, b: &Lifetime<I>, ) -> Fallible<()>
fn unify_lifetime_var( &mut self, variance: Variance, var: InferenceVar, value: &Lifetime<I>, value_ui: UniverseIndex, ) -> Fallible<()>
fn relate_const_const<'a>( &mut self, variance: Variance, a: &'a Const<I>, b: &'a Const<I>, ) -> Fallible<()>
fn unify_var_const(&mut self, var: InferenceVar, c: &Const<I>) -> Fallible<()>
sourcefn push_lifetime_outlives_goals(
&mut self,
variance: Variance,
a: Lifetime<I>,
b: Lifetime<I>,
)
fn push_lifetime_outlives_goals( &mut self, variance: Variance, a: Lifetime<I>, b: Lifetime<I>, )
Relate a
, b
such that if variance = Covariant
, a
is a subtype of
b
and thus a
must outlive b
.
sourcefn push_subtype_goal(&mut self, a: Ty<I>, b: Ty<I>)
fn push_subtype_goal(&mut self, a: Ty<I>, b: Ty<I>)
Pushes a goal of a
being a subtype of b
.
Trait Implementations§
source§impl<'i, I: Interner> Zipper<I> for Unifier<'i, I>
impl<'i, I: Interner> Zipper<I> for Unifier<'i, I>
source§fn zip_tys(&mut self, variance: Variance, a: &Ty<I>, b: &Ty<I>) -> Fallible<()>
fn zip_tys(&mut self, variance: Variance, a: &Ty<I>, b: &Ty<I>) -> Fallible<()>
a
and b
were found in matching spots.source§fn zip_lifetimes(
&mut self,
variance: Variance,
a: &Lifetime<I>,
b: &Lifetime<I>,
) -> Fallible<()>
fn zip_lifetimes( &mut self, variance: Variance, a: &Lifetime<I>, b: &Lifetime<I>, ) -> Fallible<()>
a
and b
were found in matching spots.source§fn zip_consts(
&mut self,
variance: Variance,
a: &Const<I>,
b: &Const<I>,
) -> Fallible<()>
fn zip_consts( &mut self, variance: Variance, a: &Const<I>, b: &Const<I>, ) -> Fallible<()>
a
and b
were found in matching spots.source§fn zip_binders<T>(
&mut self,
variance: Variance,
a: &Binders<T>,
b: &Binders<T>,
) -> Fallible<()>
fn zip_binders<T>( &mut self, variance: Variance, a: &Binders<T>, b: &Binders<T>, ) -> Fallible<()>
source§fn unification_database(&self) -> &dyn UnificationDatabase<I>
fn unification_database(&self) -> &dyn UnificationDatabase<I>
UnificationDatabase
from the underlying zipper objectsource§fn zip_substs(
&mut self,
ambient: Variance,
variances: Option<Variances<I>>,
a: &[GenericArg<I>],
b: &[GenericArg<I>],
) -> Result<(), NoSolution>where
Self: Sized,
fn zip_substs(
&mut self,
ambient: Variance,
variances: Option<Variances<I>>,
a: &[GenericArg<I>],
b: &[GenericArg<I>],
) -> Result<(), NoSolution>where
Self: Sized,
Auto Trait Implementations§
impl<'t, I> Freeze for Unifier<'t, I>where
I: Freeze,
impl<'t, I> !RefUnwindSafe for Unifier<'t, I>
impl<'t, I> !Send for Unifier<'t, I>
impl<'t, I> !Sync for Unifier<'t, I>
impl<'t, I> Unpin for Unifier<'t, I>where
I: Unpin,
<I as Interner>::InternedGoal: Unpin,
<I as Interner>::InternedProgramClauses: Unpin,
impl<'t, I> !UnwindSafe for Unifier<'t, I>
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
.