chalk_solve/
coinductive_goal.rs

1use crate::RustIrDatabase;
2use chalk_ir::interner::Interner;
3use chalk_ir::*;
4
5pub trait IsCoinductive<I: Interner> {
6    /// A goal G has coinductive semantics if proving G is allowed to
7    /// assume G is true (very roughly speaking). In the case of
8    /// chalk-ir, this is true for goals of the form `T: AutoTrait`,
9    /// or if it is of the form `WellFormed(T: Trait)` where `Trait`
10    /// is any trait. The latter is needed for dealing with WF
11    /// requirements and cyclic traits, which generates cycles in the
12    /// proof tree which must not be rejected but instead must be
13    /// treated as a success.
14    fn is_coinductive(&self, db: &dyn RustIrDatabase<I>) -> bool;
15}
16
17impl<I: Interner> IsCoinductive<I> for Goal<I> {
18    fn is_coinductive(&self, db: &dyn RustIrDatabase<I>) -> bool {
19        let interner = db.interner();
20        match self.data(interner) {
21            GoalData::DomainGoal(DomainGoal::Holds(wca)) => match wca {
22                WhereClause::Implemented(tr) => {
23                    db.trait_datum(tr.trait_id).is_auto_trait()
24                        || db.trait_datum(tr.trait_id).is_coinductive_trait()
25                }
26                WhereClause::AliasEq(..) => false,
27                WhereClause::LifetimeOutlives(..) => false,
28                WhereClause::TypeOutlives(..) => false,
29            },
30            GoalData::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..))) => true,
31            GoalData::Quantified(QuantifierKind::ForAll, goal) => {
32                goal.skip_binders().is_coinductive(db)
33            }
34            _ => false,
35        }
36    }
37}
38
39impl<I: Interner> IsCoinductive<I> for UCanonical<InEnvironment<Goal<I>>> {
40    fn is_coinductive(&self, db: &dyn RustIrDatabase<I>) -> bool {
41        self.canonical.value.goal.is_coinductive(db)
42    }
43}
chalk_solve/coinductive_goal.rs

chalk_solve/
coinductive_goal.rs
