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>

Zips two substs