vendor/chalk-solve-0.14.0/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 = infer.instantiate_binders_universally(interner, subgoal);
  74                         env_goal = InEnvironment::new(&environment, subgoal);
  75                     }
  76
  77                     GoalData::Quantified(QuantifierKind::Exists, subgoal) => {
  78                         let subgoal = infer.instantiate_binders_existentially(interner, subgoal);
  79                         env_goal = InEnvironment::new(&environment, subgoal);
  80                     }
  81
  82                     GoalData::Implies(wc, subgoal) => {
  83                         let new_environment =
  84                             environment.add_clauses(interner, wc.iter(interner).cloned());
  85                         env_goal = InEnvironment::new(&new_environment, Goal::clone(subgoal));
  86                     }
  87
  88                     _ => break InEnvironment::new(&environment, goal),
  89                 }
  90             }
  91         };
  92         let canonical = infer.canonicalize(interner, &peeled_goal).quantified;
  93         infer.u_canonicalize(interner, &canonical).quantified
  94     }
  95
  96     /// Given a goal with no free variables (a "closed" goal), creates
  97     /// a canonical form suitable for solving. This is a suitable
  98     /// choice if you don't actually care about the values of any of
  99     /// the variables within; otherwise, you might want
 100     /// `into_peeled_goal`.
 101     ///
 102     /// # Panics
 103     ///
 104     /// Will panic if this goal does in fact contain free variables.
 105     fn into_closed_goal(self, interner: &I) -> UCanonical<InEnvironment<Goal<I>>> {
 106         let mut infer = InferenceTable::new();
 107         let env_goal = InEnvironment::new(&Environment::new(interner), self);
 108         let canonical_goal = infer.canonicalize(interner, &env_goal).quantified;
 109         infer.u_canonicalize(interner, &canonical_goal).quantified
 110     }
 111 }