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