]>
Commit | Line | Data |
---|---|---|
f9f354fc XL |
1 | use crate::RustIrDatabase; |
2 | use chalk_ir::interner::Interner; | |
3 | use chalk_ir::*; | |
4 | ||
5 | pub 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 | ||
17 | impl<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, | |
f035d41b | 27 | WhereClause::LifetimeOutlives(..) => false, |
3dfed10e | 28 | WhereClause::TypeOutlives(..) => false, |
f9f354fc XL |
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 | ||
39 | impl<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 | } |