Struct chalk_solve::infer::InferenceTable

pub struct InferenceTable<I: Interner> { /* fields omitted */ }

Implementations

impl<I: Interner> InferenceTable<I>

pub fn canonicalize<T>(
    &mut self,
    interner: &I,
    value: &T
) -> Canonicalized<T::Result> where
    T: Fold<I>,
    T::Result: 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 fn instantiate_canonical<T>(
    &mut self,
    interner: &I,
    bound: &Canonical<T>
) -> T::Result where
    T: HasInterner<Interner = I> + Fold<I> + Debug, 

Variant on instantiate that takes a Canonical<T>.

pub fn instantiate_binders_existentially<'a, T>(
    &mut self,
    interner: &'a I,
    arg: impl IntoBindersAndValue<'a, I, Value = T>
) -> T::Result where
    T: Fold<I>, 

Variant on instantiate_in that takes a Binders<T>.

pub fn instantiate_binders_universally<'a, T>(
    &mut self,
    interner: &'a I,
    arg: impl IntoBindersAndValue<'a, I, Value = T>
) -> T::Result where
    T: Fold<I>, 

impl<I: Interner> InferenceTable<I>

pub fn invert<T>(&mut self, interner: &I, value: &T) -> Option<T::Result> where
    T: Fold<I, Result = T> + 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 [1], where negative goals are only permitted if they contain no free (existential) variables.

[1] http://www.doc.ic.ac.uk/~klc/NegAsFailure.pdf

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., TypeName::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::Result>> where
    T: Fold<I, Result = T> + HasInterner<Interner = I>, 

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

impl<I: Interner> InferenceTable<I>

pub fn u_canonicalize<T>(
    &mut self,
    interner: &I,
    value0: &Canonical<T>
) -> UCanonicalized<T::Result> where
    T: HasInterner<Interner = I> + Fold<I> + Visit<I>,
    T::Result: HasInterner<Interner = I>, 

impl<I: Interner> InferenceTable<I>

pub fn unify<T: ?Sized>(
    &mut self,
    interner: &I,
    environment: &Environment<I>,
    a: &T,
    b: &T
) -> Fallible<UnificationResult<I>> where
    T: 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> + Fold<I, Result = T> + 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_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 normalize_ty_shallow(
    &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 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.

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.