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

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.

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).

Variant on instantiate that takes a Canonical<T>.

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.

Variant on instantiate_in that takes a Binders<T>.

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.)

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

Create an empty inference table with no variables.

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.

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).

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.

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).

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

Make permanent the changes made since the snapshot was taken.

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.

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.

Given an unbound variable, returns its universe.

Panics

Panics if the variable is bound.

Trait Implementations

Returns a copy of the value. Read more

Performs copy-assignment from source. Read more

Auto Trait Implementations

Blanket Implementations

Gets the TypeId of self. Read more

Immutably borrows from an owned value. Read more

Mutably borrows from an owned value. Read more

Cast a value to type U using CastTo.

Returns the argument unchanged.

Instruments this type with the provided Span, returning an Instrumented wrapper. Read more

Instruments this type with the current Span, returning an Instrumented wrapper. Read more

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

The resulting type after obtaining ownership.

Creates owned data from borrowed data, usually by cloning. Read more

Uses borrowed data to replace owned data, usually by cloning. Read more

The type returned in the event of a conversion error.

Performs the conversion.

The type returned in the event of a conversion error.

Performs the conversion.

Attaches the provided Subscriber to this type, returning a WithDispatch wrapper. Read more

Attaches the current default Subscriber to this type, returning a WithDispatch wrapper. Read more