]>
Commit | Line | Data |
---|---|---|
f9f354fc XL |
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> { | |
a2a8927a | 7 | fn map<OP, U>(self, interner: I, op: OP) -> Canonical<U::Result> |
f9f354fc XL |
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. | |
a2a8927a | 27 | fn map<OP, U>(self, interner: I, op: OP) -> Canonical<U::Result> |
f9f354fc XL |
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(); | |
5869c6ff | 45 | let instantiated_value = infer.instantiate_canonical(interner, self); |
f9f354fc | 46 | let mapped_value = op(instantiated_value); |
5869c6ff | 47 | let result = infer.canonicalize(interner, mapped_value); |
f9f354fc XL |
48 | infer.rollback_to(snapshot); |
49 | result.quantified | |
50 | } | |
51 | } | |
52 | ||
53 | pub trait GoalExt<I: Interner> { | |
a2a8927a XL |
54 | fn into_peeled_goal(self, interner: I) -> UCanonical<InEnvironment<Goal<I>>>; |
55 | fn into_closed_goal(self, interner: I) -> UCanonical<InEnvironment<Goal<I>>>; | |
f9f354fc XL |
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. | |
a2a8927a | 65 | fn into_peeled_goal(self, interner: I) -> UCanonical<InEnvironment<Goal<I>>> { |
f9f354fc XL |
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) => { | |
5869c6ff XL |
73 | let subgoal = |
74 | infer.instantiate_binders_universally(interner, subgoal.clone()); | |
f9f354fc XL |
75 | env_goal = InEnvironment::new(&environment, subgoal); |
76 | } | |
77 | ||
78 | GoalData::Quantified(QuantifierKind::Exists, subgoal) => { | |
5869c6ff XL |
79 | let subgoal = |
80 | infer.instantiate_binders_existentially(interner, subgoal.clone()); | |
f9f354fc XL |
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 | }; | |
5869c6ff XL |
94 | let canonical = infer.canonicalize(interner, peeled_goal).quantified; |
95 | InferenceTable::u_canonicalize(interner, &canonical).quantified | |
f9f354fc XL |
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. | |
a2a8927a | 107 | fn into_closed_goal(self, interner: I) -> UCanonical<InEnvironment<Goal<I>>> { |
f9f354fc XL |
108 | let mut infer = InferenceTable::new(); |
109 | let env_goal = InEnvironment::new(&Environment::new(interner), self); | |
5869c6ff XL |
110 | let canonical_goal = infer.canonicalize(interner, env_goal).quantified; |
111 | InferenceTable::u_canonicalize(interner, &canonical_goal).quantified | |
f9f354fc XL |
112 | } |
113 | } |