use crate::RustIrDatabase;
use chalk_ir::interner::Interner;
use chalk_ir::*;
pub trait IsCoinductive<I: Interner> {
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)
}
}