vendor/chalk-solve/src/coinductive_goal.rs

   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,
  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
  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 }