chalk_solve/
ext.rs

1use crate::infer::InferenceTable;
2use chalk_ir::fold::TypeFoldable;
3use chalk_ir::interner::{HasInterner, Interner};
4use chalk_ir::*;
5
6pub trait CanonicalExt<T: HasInterner, I: Interner> {
7    fn map<OP, U>(self, interner: I, op: OP) -> Canonical<U>
8    where
9        OP: FnOnce(T) -> U,
10        T: TypeFoldable<I>,
11        U: TypeFoldable<I>,
12        U: HasInterner<Interner = I>;
13}
14
15impl<T, I> CanonicalExt<T, I> for Canonical<T>
16where
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>
28    where
29        OP: FnOnce(T) -> U,
30        T: TypeFoldable<I>,
31        U: TypeFoldable<I>,
32        U: 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
53pub 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
58impl<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}
chalk_solve/ext.rs

chalk_solve/
ext.rs
