]>
Commit | Line | Data |
---|---|---|
f035d41b XL |
1 | use chalk_ir::fold::shift::Shift; |
2 | use chalk_ir::fold::{Fold, Folder}; | |
3 | use chalk_ir::interner::HasInterner; | |
4 | use chalk_ir::interner::Interner; | |
5 | use chalk_ir::*; | |
6 | use rustc_hash::FxHashMap; | |
7 | ||
8 | use super::canonicalize::Canonicalized; | |
9 | use super::{EnaVariable, InferenceTable}; | |
10 | ||
11 | impl<I: Interner> InferenceTable<I> { | |
12 | /// Converts `value` into a "negation" value -- meaning one that, | |
13 | /// if we can find any answer to it, then the negation fails. For | |
14 | /// goals that do not contain any free variables, then this is a | |
15 | /// no-op operation. | |
16 | /// | |
17 | /// If `value` contains any existential variables that have not | |
18 | /// yet been assigned a value, then this function will return | |
19 | /// `None`, indicating that we cannot prove negation for this goal | |
20 | /// yet. This follows the approach in Clark's original | |
21 | /// negation-as-failure paper [1], where negative goals are only | |
22 | /// permitted if they contain no free (existential) variables. | |
23 | /// | |
24 | /// [1] http://www.doc.ic.ac.uk/~klc/NegAsFailure.pdf | |
25 | /// | |
26 | /// Restricting free existential variables is done because the | |
27 | /// semantics of such queries is not what you expect: it basically | |
28 | /// treats the existential as a universal. For example, consider: | |
29 | /// | |
30 | /// ```rust,ignore | |
31 | /// struct Vec<T> {} | |
32 | /// struct i32 {} | |
33 | /// struct u32 {} | |
34 | /// trait Foo {} | |
35 | /// impl Foo for Vec<u32> {} | |
36 | /// ``` | |
37 | /// | |
38 | /// If we ask `exists<T> { not { Vec<T>: Foo } }`, what should happen? | |
39 | /// If we allow negative queries to be definitively answered even when | |
40 | /// they contain free variables, we will get a definitive *no* to the | |
41 | /// entire goal! From a logical perspective, that's just wrong: there | |
42 | /// does exists a `T` such that `not { Vec<T>: Foo }`, namely `i32`. The | |
43 | /// problem is that the proof search procedure is actually trying to | |
44 | /// prove something stronger, that there is *no* such `T`. | |
45 | /// | |
46 | /// An additional complication arises around free universal | |
47 | /// variables. Consider a query like `not { !0 = !1 }`, where | |
48 | /// `!0` and `!1` are placeholders for universally quantified | |
49 | /// types (i.e., `TypeName::Placeholder`). If we just tried to | |
50 | /// prove `!0 = !1`, we would get false, because those types | |
51 | /// cannot be unified -- this would then allow us to conclude that | |
52 | /// `not { !0 = !1 }`, i.e., `forall<X, Y> { not { X = Y } }`, but | |
53 | /// this is clearly not true -- what if X were to be equal to Y? | |
54 | /// | |
55 | /// Interestingly, the semantics of existential variables turns | |
56 | /// out to be exactly what we want here. So, in addition to | |
57 | /// forbidding existential variables in the original query, the | |
58 | /// `negated` query also converts all universals *into* | |
59 | /// existentials. Hence `negated` applies to `!0 = !1` would yield | |
60 | /// `exists<X,Y> { X = Y }` (note that a canonical, i.e. closed, | |
61 | /// result is returned). Naturally this has a solution, and hence | |
62 | /// `not { !0 = !1 }` fails, as we expect. | |
63 | /// | |
64 | /// (One could imagine converting free existentials into | |
65 | /// universals, rather than forbidding them altogether. This would | |
66 | /// be conceivable, but overly strict. For example, the goal | |
67 | /// `exists<T> { not { ?T: Clone }, ?T = Vec<i32> }` would come | |
68 | /// back as false, when clearly this is true. This is because we | |
69 | /// would wind up proving that `?T: Clone` can *never* be | |
70 | /// satisfied (which is false), when we only really care about | |
71 | /// `?T: Clone` in the case where `?T = Vec<i32>`. The current | |
72 | /// version would delay processing the negative goal (i.e., return | |
73 | /// `None`) until the second unification has occurred.) | |
74 | pub(crate) fn invert<T>(&mut self, interner: &I, value: &T) -> Option<T::Result> | |
75 | where | |
76 | T: Fold<I, Result = T> + HasInterner<Interner = I>, | |
77 | { | |
78 | let Canonicalized { | |
79 | free_vars, | |
80 | quantified, | |
81 | .. | |
82 | } = self.canonicalize(interner, &value); | |
83 | ||
84 | // If the original contains free existential variables, give up. | |
85 | if !free_vars.is_empty() { | |
86 | return None; | |
87 | } | |
88 | ||
89 | // If this contains free universal variables, replace them with existentials. | |
90 | assert!(quantified.binders.is_empty(interner)); | |
91 | let inverted = quantified | |
92 | .value | |
93 | .fold_with(&mut Inverter::new(interner, self), DebruijnIndex::INNERMOST) | |
94 | .unwrap(); | |
95 | Some(inverted) | |
96 | } | |
97 | ||
98 | /// As `negated_instantiated`, but canonicalizes before | |
99 | /// returning. Just a convenience function. | |
100 | pub(crate) fn invert_then_canonicalize<T>( | |
101 | &mut self, | |
102 | interner: &I, | |
103 | value: &T, | |
104 | ) -> Option<Canonical<T::Result>> | |
105 | where | |
106 | T: Fold<I, Result = T> + HasInterner<Interner = I>, | |
107 | { | |
108 | let snapshot = self.snapshot(); | |
109 | let result = self.invert(interner, value); | |
110 | let result = result.map(|r| self.canonicalize(interner, &r).quantified); | |
111 | self.rollback_to(snapshot); | |
112 | result | |
113 | } | |
114 | } | |
115 | ||
116 | struct Inverter<'q, I: Interner> { | |
117 | table: &'q mut InferenceTable<I>, | |
118 | inverted_ty: FxHashMap<PlaceholderIndex, EnaVariable<I>>, | |
119 | inverted_lifetime: FxHashMap<PlaceholderIndex, EnaVariable<I>>, | |
120 | interner: &'q I, | |
121 | } | |
122 | ||
123 | impl<'q, I: Interner> Inverter<'q, I> { | |
124 | fn new(interner: &'q I, table: &'q mut InferenceTable<I>) -> Self { | |
125 | Inverter { | |
126 | table, | |
127 | inverted_ty: FxHashMap::default(), | |
128 | inverted_lifetime: FxHashMap::default(), | |
129 | interner, | |
130 | } | |
131 | } | |
132 | } | |
133 | ||
134 | impl<'i, I: Interner> Folder<'i, I> for Inverter<'i, I> | |
135 | where | |
136 | I: 'i, | |
137 | { | |
138 | fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> { | |
139 | self | |
140 | } | |
141 | ||
142 | fn fold_free_placeholder_ty( | |
143 | &mut self, | |
144 | universe: PlaceholderIndex, | |
145 | _outer_binder: DebruijnIndex, | |
146 | ) -> Fallible<Ty<I>> { | |
147 | let table = &mut self.table; | |
148 | Ok(self | |
149 | .inverted_ty | |
150 | .entry(universe) | |
151 | .or_insert_with(|| table.new_variable(universe.ui)) | |
152 | .to_ty(self.interner()) | |
153 | .shifted_in(self.interner())) | |
154 | } | |
155 | ||
156 | fn fold_free_placeholder_lifetime( | |
157 | &mut self, | |
158 | universe: PlaceholderIndex, | |
159 | _outer_binder: DebruijnIndex, | |
160 | ) -> Fallible<Lifetime<I>> { | |
161 | let table = &mut self.table; | |
162 | Ok(self | |
163 | .inverted_lifetime | |
164 | .entry(universe) | |
165 | .or_insert_with(|| table.new_variable(universe.ui)) | |
166 | .to_lifetime(self.interner()) | |
167 | .shifted_in(self.interner())) | |
168 | } | |
169 | ||
170 | fn forbid_free_vars(&self) -> bool { | |
171 | true | |
172 | } | |
173 | ||
174 | fn forbid_inference_vars(&self) -> bool { | |
175 | true | |
176 | } | |
177 | ||
178 | fn interner(&self) -> &'i I { | |
179 | self.interner | |
180 | } | |
181 | ||
182 | fn target_interner(&self) -> &'i I { | |
183 | self.interner() | |
184 | } | |
185 | } |