Merge tag 'debian/1.52.1+dfsg1-1_exp2' into proxmox/buster

[rustc.git] / vendor / chalk-solve-0.55.0 / src / coinductive_goal.rs

diff --git a/vendor/chalk-solve-0.55.0/src/coinductive_goal.rs b/vendor/chalk-solve-0.55.0/src/coinductive_goal.rs
new file mode 100644 (file)
index 0000000..cdb5cca
--- /dev/null
+++ b/vendor/chalk-solve-0.55.0/src/coinductive_goal.rs
@@ -0,0 +1,43 @@
+use crate::RustIrDatabase;
+use chalk_ir::interner::Interner;
+use chalk_ir::*;
+
+pub trait IsCoinductive<I: Interner> {
+    /// A goal G has coinductive semantics if proving G is allowed to
+    /// assume G is true (very roughly speaking). In the case of
+    /// chalk-ir, this is true for goals of the form `T: AutoTrait`,
+    /// or if it is of the form `WellFormed(T: Trait)` where `Trait`
+    /// is any trait. The latter is needed for dealing with WF
+    /// requirements and cyclic traits, which generates cycles in the
+    /// proof tree which must not be rejected but instead must be
+    /// treated as a success.
+    fn is_coinductive(&self, db: &dyn RustIrDatabase<I>) -> bool;
+}
+
+impl<I: Interner> IsCoinductive<I> for Goal<I> {
+    fn is_coinductive(&self, db: &dyn RustIrDatabase<I>) -> bool {
+        let interner = db.interner();
+        match self.data(interner) {
+            GoalData::DomainGoal(DomainGoal::Holds(wca)) => match wca {
+                WhereClause::Implemented(tr) => {
+                    db.trait_datum(tr.trait_id).is_auto_trait()
+                        || db.trait_datum(tr.trait_id).is_coinductive_trait()
+                }
+                WhereClause::AliasEq(..) => false,
+                WhereClause::LifetimeOutlives(..) => false,
+                WhereClause::TypeOutlives(..) => false,
+            },
+            GoalData::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..))) => true,
+            GoalData::Quantified(QuantifierKind::ForAll, goal) => {
+                goal.skip_binders().is_coinductive(db)
+            }
+            _ => false,
+        }
+    }
+}
+
+impl<I: Interner> IsCoinductive<I> for UCanonical<InEnvironment<Goal<I>>> {
+    fn is_coinductive(&self, db: &dyn RustIrDatabase<I>) -> bool {
+        self.canonical.value.goal.is_coinductive(db)
+    }
+}