[−][src]Struct chalk_solve::infer::InferenceTable
Implementations
impl<I: Interner> InferenceTable<I>
[src]
pub fn canonicalize<T>(
&mut self,
interner: &I,
value: &T
) -> Canonicalized<T::Result> where
T: Fold<I>,
T::Result: HasInterner<Interner = I>,
[src]
&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>
[src]
pub fn instantiate_canonical<T>(
&mut self,
interner: &I,
bound: &Canonical<T>
) -> T::Result where
T: HasInterner<Interner = I> + Fold<I> + Debug,
[src]
&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> + Debug
) -> T::Result where
T: Fold<I>,
[src]
&mut self,
interner: &'a I,
arg: impl IntoBindersAndValue<'a, I, Value = T> + Debug
) -> 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> + Debug
) -> T::Result where
T: Fold<I>,
[src]
&mut self,
interner: &'a I,
arg: impl IntoBindersAndValue<'a, I, Value = T> + Debug
) -> T::Result where
T: Fold<I>,
impl<I: Interner> InferenceTable<I>
[src]
pub fn invert<T>(&mut self, interner: &I, value: &T) -> Option<T::Result> where
T: Fold<I, Result = T> + HasInterner<Interner = I>,
[src]
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] https://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., 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::Result>> where
T: Fold<I, Result = T> + HasInterner<Interner = I>,
[src]
&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>
[src]
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>,
[src]
&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>
[src]
pub fn relate<T: ?Sized>(
&mut self,
interner: &I,
db: &dyn UnificationDatabase<I>,
environment: &Environment<I>,
variance: Variance,
a: &T,
b: &T
) -> Fallible<RelationResult<I>> where
T: Zip<I>,
[src]
&mut self,
interner: &I,
db: &dyn UnificationDatabase<I>,
environment: &Environment<I>,
variance: Variance,
a: &T,
b: &T
) -> Fallible<RelationResult<I>> where
T: Zip<I>,
impl<I: Interner> InferenceTable<I>
[src]
pub fn new() -> Self
[src]
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,
[src]
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>
[src]
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>>
[src]
&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>>
[src]
&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>>
[src]
&mut self,
interner: &I,
leaf: &Const<I>
) -> Option<Const<I>>
pub fn inference_var_root(&mut self, var: InferenceVar) -> InferenceVar
[src]
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>>
[src]
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>
[src]
pub fn clone(&self) -> InferenceTable<I>
[src]
pub fn clone_from(&mut self, source: &Self)
1.0.0[src]
Auto Trait Implementations
impl<I> RefUnwindSafe for InferenceTable<I> where
I: RefUnwindSafe,
<I as Interner>::InternedGenericArg: RefUnwindSafe,
I: RefUnwindSafe,
<I as Interner>::InternedGenericArg: RefUnwindSafe,
impl<I> Send for InferenceTable<I> where
I: Send,
<I as Interner>::InternedGenericArg: Send,
I: Send,
<I as Interner>::InternedGenericArg: Send,
impl<I> Sync for InferenceTable<I> where
I: Sync,
<I as Interner>::InternedGenericArg: Sync,
I: Sync,
<I as Interner>::InternedGenericArg: Sync,
impl<I> Unpin for InferenceTable<I> where
I: Unpin,
<I as Interner>::InternedGenericArg: Unpin,
I: Unpin,
<I as Interner>::InternedGenericArg: Unpin,
impl<I> UnwindSafe for InferenceTable<I> where
I: UnwindSafe,
<I as Interner>::InternedGenericArg: UnwindSafe,
I: UnwindSafe,
<I as Interner>::InternedGenericArg: UnwindSafe,
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
pub fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Cast for T
[src]
pub fn cast<U>(self, interner: &<U as HasInterner>::Interner) -> U where
Self: CastTo<U>,
U: HasInterner,
[src]
Self: CastTo<U>,
U: HasInterner,
impl<T> From<T> for T
[src]
impl<T> Instrument for T
[src]
pub fn instrument(self, span: Span) -> Instrumented<Self>
[src]
pub fn in_current_span(self) -> Instrumented<Self>
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
pub fn to_owned(&self) -> T
[src]
pub fn clone_into(&self, target: &mut T)
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
pub fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,