Struct chalk_engine::slg::resolvent::AnswerSubstitutor

struct AnswerSubstitutor<'t, I: Interner> {
    table: &'t mut InferenceTable<I>,
    environment: &'t Environment<I>,
    answer_subst: &'t Substitution<I>,
    outer_binder: DebruijnIndex,
    ex_clause: &'t mut ExClause<I>,
    interner: I,
    unification_database: &'t dyn UnificationDatabase<I>,
}

Fields

table: &'t mut InferenceTable<I>

environment: &'t Environment<I>

answer_subst: &'t Substitution<I>

outer_binder: DebruijnIndex

Tracks the debrujn index of the first binder that is outside the term we are traversing. This starts as DebruijnIndex::INNERMOST, since we have not yet traversed any binders, but when we visit the inside of a binder, it would be incremented.

Example: If we are visiting (for<type> A, B, C, for<type> for<type> D), then this would be:

• 1, when visiting A,
• 0, when visiting B and C,
• 2, when visiting D.

ex_clause: &'t mut ExClause<I>

interner: I

unification_database: &'t dyn UnificationDatabase<I>

Implementations

impl<I: Interner> AnswerSubstitutor<'_, I>

fn substitute<T: Zip<I>>( interner: I, unification_database: &dyn UnificationDatabase<I>, table: &mut InferenceTable<I>, environment: &Environment<I>, answer_subst: &Substitution<I>, ex_clause: &mut ExClause<I>, answer: &T, pending: &T, ) -> Fallible<()>

fn unify_free_answer_var( &mut self, interner: I, db: &dyn UnificationDatabase<I>, variance: Variance, answer_var: BoundVar, pending: GenericArgData<I>, ) -> Fallible<bool>

fn assert_matching_vars( &mut self, answer_var: BoundVar, pending_var: BoundVar, ) -> Fallible<()>

When we encounter a variable in the answer goal, we first try unify_free_answer_var. Assuming that this fails, the variable must be a bound variable in the answer goal – in that case, there should be a corresponding bound variable in the pending goal. This bit of code just checks that latter case.

Trait Implementations

impl<'i, I: Interner> Zipper<I> for AnswerSubstitutor<'i, I>

fn zip_tys( &mut self, variance: Variance, answer: &Ty<I>, pending: &Ty<I>, ) -> Fallible<()>

Indicates that the two types a and b were found in matching spots.

fn zip_lifetimes( &mut self, variance: Variance, answer: &Lifetime<I>, pending: &Lifetime<I>, ) -> Fallible<()>

Indicates that the two lifetimes a and b were found in matching spots.

fn zip_consts( &mut self, variance: Variance, answer: &Const<I>, pending: &Const<I>, ) -> Fallible<()>

Indicates that the two consts a and b were found in matching spots.

fn zip_binders<T>( &mut self, variance: Variance, answer: &Binders<T>, pending: &Binders<T>, ) -> Fallible<()>

where T: HasInterner<Interner = I> + Zip<I> + TypeFoldable<I>,

Zips two values appearing beneath binders.

fn interner(&self) -> I

Retrieves the interner from the underlying zipper object

fn unification_database(&self) -> &dyn UnificationDatabase<I>

Retrieves the UnificationDatabase from the underlying zipper object

fn zip_substs( &mut self, ambient: Variance, variances: Option<Variances<I>>, a: &[GenericArg<I>], b: &[GenericArg<I>], ) -> Result<(), NoSolution>

where Self: Sized,

Zips two substs