From 218caa410aa38c29984be31a5229b9fa717560ee Mon Sep 17 00:00:00 2001
From: Daniel Baumann <daniel.baumann@progress-linux.org>
Date: Wed, 17 Apr 2024 14:19:13 +0200
Subject: Merging upstream version 1.68.2+dfsg1.

Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>
---
 vendor/chalk-solve-0.87.0/src/coinductive_goal.rs | 43 +++++++++++++++++++++++
 1 file changed, 43 insertions(+)
 create mode 100644 vendor/chalk-solve-0.87.0/src/coinductive_goal.rs

(limited to 'vendor/chalk-solve-0.87.0/src/coinductive_goal.rs')

diff --git a/vendor/chalk-solve-0.87.0/src/coinductive_goal.rs b/vendor/chalk-solve-0.87.0/src/coinductive_goal.rs
new file mode 100644
index 000000000..cdb5cca10
--- /dev/null
+++ b/vendor/chalk-solve-0.87.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)
+    }
+}
-- 
cgit v1.2.3