vendor/chalk-solve/src/ext.rs

   1 use crate::infer::InferenceTable;
   2 use chalk_ir::fold::Fold;
   3 use chalk_ir::interner::{HasInterner, Interner};
   4 use chalk_ir::*;
   5
   6 pub trait CanonicalExt<T: HasInterner, I: Interner> {
   7     fn map<OP, U>(self, interner: I, op: OP) -> Canonical<U::Result>
   8     where
   9         OP: FnOnce(T::Result) -> U,
  10         T: Fold<I>,
  11         U: Fold<I>,
  12         U::Result: HasInterner<Interner = I>;
  13 }
  14
  15 impl<T, I> CanonicalExt<T, I> for Canonical<T>
  16 where
  17     T: HasInterner<Interner = I>,
  18     I: Interner,
  19 {
  20     /// Maps the contents using `op`, but preserving the binders.
  21     ///
  22     /// NB. `op` will be invoked with an instantiated version of the
  23     /// canonical value, where inference variables (from a fresh
  24     /// inference context) are used in place of the quantified free
  25     /// variables. The result should be in terms of those same
  26     /// inference variables and will be re-canonicalized.
  27     fn map<OP, U>(self, interner: I, op: OP) -> Canonical<U::Result>
  28     where
  29         OP: FnOnce(T::Result) -> U,
  30         T: Fold<I>,
  31         U: Fold<I>,
  32         U::Result: HasInterner<Interner = I>,
  33     {
  34         // Subtle: It is only quite rarely correct to apply `op` and
  35         // just re-use our existing binders. For that to be valid, the
  36         // result of `op` would have to ensure that it re-uses all the
  37         // existing free variables and in the same order. Otherwise,
  38         // the canonical form would be different: the variables might
  39         // be numbered differently, or some may not longer be used.
  40         // This would mean that two canonical values could no longer
  41         // be compared with `Eq`, which defeats a key invariant of the
  42         // `Canonical` type (indeed, its entire reason for existence).
  43         let mut infer = InferenceTable::new();
  44         let snapshot = infer.snapshot();
  45         let instantiated_value = infer.instantiate_canonical(interner, self);
  46         let mapped_value = op(instantiated_value);
  47         let result = infer.canonicalize(interner, mapped_value);
  48         infer.rollback_to(snapshot);
  49         result.quantified
  50     }
  51 }
  52
  53 pub trait GoalExt<I: Interner> {
  54     fn into_peeled_goal(self, interner: I) -> UCanonical<InEnvironment<Goal<I>>>;
  55     fn into_closed_goal(self, interner: I) -> UCanonical<InEnvironment<Goal<I>>>;
  56 }
  57
  58 impl<I: Interner> GoalExt<I> for Goal<I> {
  59     /// Returns a canonical goal in which the outermost `exists<>` and
  60     /// `forall<>` quantifiers (as well as implications) have been
  61     /// "peeled" and are converted into free universal or existential
  62     /// variables. Assumes that this goal is a "closed goal" which
  63     /// does not -- at present -- contain any variables. Useful for
  64     /// REPLs and tests but not much else.
  65     fn into_peeled_goal(self, interner: I) -> UCanonical<InEnvironment<Goal<I>>> {
  66         let mut infer = InferenceTable::new();
  67         let peeled_goal = {
  68             let mut env_goal = InEnvironment::new(&Environment::new(interner), self);
  69             loop {
  70                 let InEnvironment { environment, goal } = env_goal;
  71                 match goal.data(interner) {
  72                     GoalData::Quantified(QuantifierKind::ForAll, subgoal) => {
  73                         let subgoal =
  74                             infer.instantiate_binders_universally(interner, subgoal.clone());
  75                         env_goal = InEnvironment::new(&environment, subgoal);
  76                     }
  77
  78                     GoalData::Quantified(QuantifierKind::Exists, subgoal) => {
  79                         let subgoal =
  80                             infer.instantiate_binders_existentially(interner, subgoal.clone());
  81                         env_goal = InEnvironment::new(&environment, subgoal);
  82                     }
  83
  84                     GoalData::Implies(wc, subgoal) => {
  85                         let new_environment =
  86                             environment.add_clauses(interner, wc.iter(interner).cloned());
  87                         env_goal = InEnvironment::new(&new_environment, Goal::clone(subgoal));
  88                     }
  89
  90                     _ => break InEnvironment::new(&environment, goal),
  91                 }
  92             }
  93         };
  94         let canonical = infer.canonicalize(interner, peeled_goal).quantified;
  95         InferenceTable::u_canonicalize(interner, &canonical).quantified
  96     }
  97
  98     /// Given a goal with no free variables (a "closed" goal), creates
  99     /// a canonical form suitable for solving. This is a suitable
 100     /// choice if you don't actually care about the values of any of
 101     /// the variables within; otherwise, you might want
 102     /// `into_peeled_goal`.
 103     ///
 104     /// # Panics
 105     ///
 106     /// Will panic if this goal does in fact contain free variables.
 107     fn into_closed_goal(self, interner: I) -> UCanonical<InEnvironment<Goal<I>>> {
 108         let mut infer = InferenceTable::new();
 109         let env_goal = InEnvironment::new(&Environment::new(interner), self);
 110         let canonical_goal = infer.canonicalize(interner, env_goal).quantified;
 111         InferenceTable::u_canonicalize(interner, &canonical_goal).quantified
 112     }
 113 }