Struct chalk_solve::infer::InferenceTable

pub struct InferenceTable<I: Interner> {
    unify: InPlaceUnificationTable<EnaVariable<I>>,
    vars: Vec<EnaVariable<I>>,
    max_universe: UniverseIndex,
}

Fields

unify: InPlaceUnificationTable<EnaVariable<I>>

vars: Vec<EnaVariable<I>>

max_universe: UniverseIndex

Implementations

impl<I: Interner> InferenceTable<I>

pub fn canonicalize<T>(&mut self, interner: I, value: T) -> Canonicalized<T>

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

Given a value value with variables in it, replaces those variables with their instantiated values; any variables not yet instantiated are replaced with a small integer index 0..N in order of appearance. The result is a canonicalized representation of value.

Example:

?22: Foo<?23>

would be quantified to

Canonical { value: ?0: Foo<?1>, binders: [ui(?22), ui(?23)] }

where ui(?22) and ui(?23) are the universe indices of ?22 and ?23 respectively.

A substitution mapping from the free variables to their re-bound form is also returned.

impl<I: Interner> InferenceTable<I>

pub(super) fn fresh_subst( &mut self, interner: I, binders: &[CanonicalVarKind<I>], ) -> Substitution<I>

Given the binders from a canonicalized value C, returns a substitution S mapping each free variable in C to a fresh inference variable. This substitution can then be applied to C, which would be equivalent to self.instantiate_canonical(v).

pub fn instantiate_canonical<T>( &mut self, interner: I, bound: Canonical<T>, ) -> T

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

Variant on instantiate that takes a Canonical<T>.

fn instantiate_in<T>( &mut self, interner: I, universe: UniverseIndex, binders: impl Iterator<Item = VariableKind<I>>, arg: T, ) -> T

where T: TypeFoldable<I>,

Instantiates arg with fresh existential variables in the given universe; the kinds of the variables are implied by binders. This is used to apply a universally quantified clause like forall X, 'Y. P => Q. Here the binders argument is referring to X, 'Y.

pub fn instantiate_binders_existentially<T>( &mut self, interner: I, arg: Binders<T>, ) -> T

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

Variant on instantiate_in that takes a Binders<T>.

pub fn instantiate_binders_universally<T>( &mut self, interner: I, arg: Binders<T>, ) -> T

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

impl<I: Interner> InferenceTable<I>

pub fn invert<T>(&mut self, interner: I, value: T) -> Option<T>

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

Converts value into a “negation” value – meaning one that, if we can find any answer to it, then the negation fails. For goals that do not contain any free variables, then this is a no-op operation.

If value contains any existential variables that have not yet been assigned a value, then this function will return None, indicating that we cannot prove negation for this goal yet. This follows the approach in Clark’s original negation-as-failure paper, where negative goals are only permitted if they contain no free (existential) variables.

Restricting free existential variables is done because the semantics of such queries is not what you expect: it basically treats the existential as a universal. For example, consider:

struct Vec<T> {}
struct i32 {}
struct u32 {}
trait Foo {}
impl Foo for Vec<u32> {}

If we ask exists<T> { not { Vec<T>: Foo } }, what should happen? If we allow negative queries to be definitively answered even when they contain free variables, we will get a definitive no to the entire goal! From a logical perspective, that’s just wrong: there does exists a T such that not { Vec<T>: Foo }, namely i32. The problem is that the proof search procedure is actually trying to prove something stronger, that there is no such T.

An additional complication arises around free universal variables. Consider a query like not { !0 = !1 }, where !0 and !1 are placeholders for universally quantified types (i.e., TyKind::Placeholder). If we just tried to prove !0 = !1, we would get false, because those types cannot be unified – this would then allow us to conclude that not { !0 = !1 }, i.e., forall<X, Y> { not { X = Y } }, but this is clearly not true – what if X were to be equal to Y?

Interestingly, the semantics of existential variables turns out to be exactly what we want here. So, in addition to forbidding existential variables in the original query, the negated query also converts all universals into existentials. Hence negated applies to !0 = !1 would yield exists<X,Y> { X = Y } (note that a canonical, i.e. closed, result is returned). Naturally this has a solution, and hence not { !0 = !1 } fails, as we expect.

(One could imagine converting free existentials into universals, rather than forbidding them altogether. This would be conceivable, but overly strict. For example, the goal exists<T> { not { ?T: Clone }, ?T = Vec<i32> } would come back as false, when clearly this is true. This is because we would wind up proving that ?T: Clone can never be satisfied (which is false), when we only really care about ?T: Clone in the case where ?T = Vec<i32>. The current version would delay processing the negative goal (i.e., return None) until the second unification has occurred.)

pub fn invert_then_canonicalize<T>( &mut self, interner: I, value: T, ) -> Option<Canonical<T>>

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

As negated_instantiated, but canonicalizes before returning. Just a convenience function.

impl<I: Interner> InferenceTable<I>

pub fn u_canonicalize<T>( interner: I, value0: &Canonical<T>, ) -> UCanonicalized<T>

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

impl<I: Interner> InferenceTable<I>

pub fn relate<T>( &mut self, interner: I, db: &dyn UnificationDatabase<I>, environment: &Environment<I>, variance: Variance, a: &T, b: &T, ) -> Fallible<RelationResult<I>>

where T: ?Sized + Zip<I>,

impl<I: Interner> InferenceTable<I>

pub fn new() -> Self

Create an empty inference table with no variables.

pub fn from_canonical<T>( interner: I, num_universes: usize, canonical: Canonical<T>, ) -> (Self, Substitution<I>, T)

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

Creates a new inference table, pre-populated with num_universes fresh universes. Instantiates the canonical value canonical within those universes (which must not reference any universe greater than num_universes). Returns the substitution mapping from each canonical binder to its corresponding existential variable, along with the instantiated result.

pub fn new_universe(&mut self) -> UniverseIndex

Creates and returns a fresh universe that is distinct from all others created within this inference table. This universe is able to see all previously created universes (though hopefully it is only brought into contact with its logical parents).

pub fn new_variable(&mut self, ui: UniverseIndex) -> EnaVariable<I>

Creates a new inference variable and returns its index. The kind of the variable should be known by the caller, but is not tracked directly by the inference table.

pub fn snapshot(&mut self) -> InferenceSnapshot<I>

Takes a “snapshot” of the current state of the inference table. Later, you must invoke either rollback_to or commit with that snapshot. Snapshots can be nested, but you must respect a stack discipline (i.e., rollback or commit snapshots in reverse order of that with which they were created).

pub fn rollback_to(&mut self, snapshot: InferenceSnapshot<I>)

Restore the table to the state it had when the snapshot was taken.

pub fn commit(&mut self, snapshot: InferenceSnapshot<I>)

Make permanent the changes made since the snapshot was taken.

pub fn normalize_ty_shallow( &mut self, interner: I, leaf: &Ty<I>, ) -> Option<Ty<I>>

fn normalize_ty_shallow_inner( &mut self, interner: I, leaf: &Ty<I>, ) -> Option<Ty<I>>

pub fn normalize_lifetime_shallow( &mut self, interner: I, leaf: &Lifetime<I>, ) -> Option<Lifetime<I>>

pub fn normalize_const_shallow( &mut self, interner: I, leaf: &Const<I>, ) -> Option<Const<I>>

pub fn ty_root(&mut self, interner: I, leaf: &Ty<I>) -> Option<Ty<I>>

pub fn lifetime_root( &mut self, interner: I, leaf: &Lifetime<I>, ) -> Option<Lifetime<I>>

pub fn inference_var_root(&mut self, var: InferenceVar) -> InferenceVar

Finds the root inference var for the given variable.

The returned variable will be exactly equivalent to the given variable except in name. All variables which have been unified to eachother (but don’t yet have a value) have the same “root”.

This is useful for DeepNormalizer.

pub fn probe_var(&mut self, leaf: InferenceVar) -> Option<GenericArg<I>>

If type leaf is a free inference variable, and that variable has been bound, returns Some(P) where P is the parameter to which it has been bound.

fn universe_of_unbound_var(&mut self, var: EnaVariable<I>) -> UniverseIndex

Given an unbound variable, returns its universe.

Panics

Panics if the variable is bound.

Trait Implementations

impl<I: Clone + Interner> Clone for InferenceTable<I>

fn clone(&self) -> InferenceTable<I>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.