diff options
Diffstat (limited to 'vendor/chalk-solve-0.87.0/src/infer/invert.rs')
-rw-r--r-- | vendor/chalk-solve-0.87.0/src/infer/invert.rs | 174 |
1 files changed, 174 insertions, 0 deletions
diff --git a/vendor/chalk-solve-0.87.0/src/infer/invert.rs b/vendor/chalk-solve-0.87.0/src/infer/invert.rs new file mode 100644 index 000000000..e5bc3590c --- /dev/null +++ b/vendor/chalk-solve-0.87.0/src/infer/invert.rs @@ -0,0 +1,174 @@ +use chalk_derive::FallibleTypeFolder; +use chalk_ir::fold::shift::Shift; +use chalk_ir::fold::{TypeFoldable, TypeFolder}; +use chalk_ir::interner::HasInterner; +use chalk_ir::interner::Interner; +use chalk_ir::*; +use rustc_hash::FxHashMap; + +use super::canonicalize::Canonicalized; +use super::{EnaVariable, InferenceTable}; + +impl<I: Interner> InferenceTable<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: + /// + /// ```rust,ignore + /// 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<T>(&mut self, interner: I, value: T) -> Option<T> + where + T: TypeFoldable<I> + HasInterner<Interner = I>, + { + let Canonicalized { + free_vars, + quantified, + .. + } = self.canonicalize(interner, value); + + // If the original contains free existential variables, give up. + if !free_vars.is_empty() { + return None; + } + + // If this contains free universal variables, replace them with existentials. + assert!(quantified.binders.is_empty(interner)); + let inverted = quantified + .value + .try_fold_with(&mut Inverter::new(interner, self), DebruijnIndex::INNERMOST) + .unwrap(); + Some(inverted) + } + + /// As `negated_instantiated`, but canonicalizes before + /// returning. Just a convenience function. + pub fn invert_then_canonicalize<T>(&mut self, interner: I, value: T) -> Option<Canonical<T>> + where + T: TypeFoldable<I> + HasInterner<Interner = I>, + { + let snapshot = self.snapshot(); + let result = self.invert(interner, value); + let result = result.map(|r| self.canonicalize(interner, r).quantified); + self.rollback_to(snapshot); + result + } +} + +#[derive(FallibleTypeFolder)] +struct Inverter<'q, I: Interner> { + table: &'q mut InferenceTable<I>, + inverted_ty: FxHashMap<PlaceholderIndex, EnaVariable<I>>, + inverted_lifetime: FxHashMap<PlaceholderIndex, EnaVariable<I>>, + interner: I, +} + +impl<'q, I: Interner> Inverter<'q, I> { + fn new(interner: I, table: &'q mut InferenceTable<I>) -> Self { + Inverter { + table, + inverted_ty: FxHashMap::default(), + inverted_lifetime: FxHashMap::default(), + interner, + } + } +} + +impl<'i, I: Interner> TypeFolder<I> for Inverter<'i, I> { + fn as_dyn(&mut self) -> &mut dyn TypeFolder<I> { + self + } + + fn fold_free_placeholder_ty( + &mut self, + universe: PlaceholderIndex, + _outer_binder: DebruijnIndex, + ) -> Ty<I> { + let table = &mut self.table; + self.inverted_ty + .entry(universe) + .or_insert_with(|| table.new_variable(universe.ui)) + .to_ty(TypeFolder::interner(self)) + .shifted_in(TypeFolder::interner(self)) + } + + fn fold_free_placeholder_lifetime( + &mut self, + universe: PlaceholderIndex, + _outer_binder: DebruijnIndex, + ) -> Lifetime<I> { + let table = &mut self.table; + self.inverted_lifetime + .entry(universe) + .or_insert_with(|| table.new_variable(universe.ui)) + .to_lifetime(TypeFolder::interner(self)) + .shifted_in(TypeFolder::interner(self)) + } + + fn forbid_free_vars(&self) -> bool { + true + } + + fn forbid_inference_vars(&self) -> bool { + true + } + + fn interner(&self) -> I { + self.interner + } +} |