1 files changed, 0 insertions, 174 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
deleted file mode 100644
index e5bc3590c..000000000
--- a/vendor/chalk-solve-0.87.0/src/infer/invert.rs
+++ /dev/null
@@ -1,174 +0,0 @@
-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
-    }
-}