]>
Commit | Line | Data |
---|---|---|
0bf4aa26 XL |
1 | mod environment; |
2 | ||
0531ce1d XL |
3 | use rustc::hir::def_id::DefId; |
4 | use rustc::hir::intravisit::{self, NestedVisitorMap, Visitor}; | |
83c7162d XL |
5 | use rustc::hir::map::definitions::DefPathData; |
6 | use rustc::hir::{self, ImplPolarity}; | |
8faf50e0 | 7 | use rustc::traits::{ |
0bf4aa26 XL |
8 | Clause, |
9 | Clauses, | |
10 | DomainGoal, | |
11 | FromEnv, | |
12 | GoalKind, | |
13 | PolyDomainGoal, | |
14 | ProgramClause, | |
15 | ProgramClauseCategory, | |
16 | WellFormed, | |
8faf50e0 XL |
17 | WhereClause, |
18 | }; | |
19 | use rustc::ty::query::Providers; | |
b7449926 | 20 | use rustc::ty::{self, List, TyCtxt}; |
a1dfa0c6 | 21 | use rustc::ty::subst::{Subst, Substs}; |
0531ce1d | 22 | use syntax::ast; |
83c7162d XL |
23 | |
24 | use std::iter; | |
0531ce1d | 25 | |
9fa01778 | 26 | crate fn provide(p: &mut Providers<'_>) { |
8faf50e0 XL |
27 | *p = Providers { |
28 | program_clauses_for, | |
0bf4aa26 XL |
29 | program_clauses_for_env: environment::program_clauses_for_env, |
30 | environment: environment::environment, | |
8faf50e0 XL |
31 | ..*p |
32 | }; | |
33 | } | |
34 | ||
94b46f34 | 35 | crate trait Lower<T> { |
0731742a | 36 | /// Lower a rustc construct (e.g., `ty::TraitPredicate`) to a chalk-like type. |
0531ce1d XL |
37 | fn lower(&self) -> T; |
38 | } | |
39 | ||
83c7162d XL |
40 | impl<T, U> Lower<Vec<U>> for Vec<T> |
41 | where | |
42 | T: Lower<U>, | |
43 | { | |
0531ce1d XL |
44 | fn lower(&self) -> Vec<U> { |
45 | self.iter().map(|item| item.lower()).collect() | |
46 | } | |
47 | } | |
48 | ||
8faf50e0 XL |
49 | impl<'tcx> Lower<WhereClause<'tcx>> for ty::TraitPredicate<'tcx> { |
50 | fn lower(&self) -> WhereClause<'tcx> { | |
51 | WhereClause::Implemented(*self) | |
0531ce1d XL |
52 | } |
53 | } | |
54 | ||
8faf50e0 XL |
55 | impl<'tcx> Lower<WhereClause<'tcx>> for ty::ProjectionPredicate<'tcx> { |
56 | fn lower(&self) -> WhereClause<'tcx> { | |
57 | WhereClause::ProjectionEq(*self) | |
0531ce1d XL |
58 | } |
59 | } | |
60 | ||
8faf50e0 XL |
61 | impl<'tcx> Lower<WhereClause<'tcx>> for ty::RegionOutlivesPredicate<'tcx> { |
62 | fn lower(&self) -> WhereClause<'tcx> { | |
63 | WhereClause::RegionOutlives(*self) | |
0531ce1d XL |
64 | } |
65 | } | |
66 | ||
8faf50e0 XL |
67 | impl<'tcx> Lower<WhereClause<'tcx>> for ty::TypeOutlivesPredicate<'tcx> { |
68 | fn lower(&self) -> WhereClause<'tcx> { | |
69 | WhereClause::TypeOutlives(*self) | |
0531ce1d XL |
70 | } |
71 | } | |
72 | ||
8faf50e0 XL |
73 | impl<'tcx, T> Lower<DomainGoal<'tcx>> for T |
74 | where | |
75 | T: Lower<WhereClause<'tcx>>, | |
76 | { | |
0531ce1d | 77 | fn lower(&self) -> DomainGoal<'tcx> { |
8faf50e0 | 78 | DomainGoal::Holds(self.lower()) |
0531ce1d XL |
79 | } |
80 | } | |
81 | ||
82 | /// `ty::Binder` is used for wrapping a rustc construction possibly containing generic | |
0731742a XL |
83 | /// lifetimes, e.g., `for<'a> T: Fn(&'a i32)`. Instead of representing higher-ranked things |
84 | /// in that leaf-form (i.e., `Holds(Implemented(Binder<TraitPredicate>))` in the previous | |
85 | /// example), we model them with quantified domain goals, e.g., as for the previous example: | |
0531ce1d XL |
86 | /// `forall<'a> { T: Fn(&'a i32) }` which corresponds to something like |
87 | /// `Binder<Holds(Implemented(TraitPredicate))>`. | |
83c7162d XL |
88 | impl<'tcx, T> Lower<PolyDomainGoal<'tcx>> for ty::Binder<T> |
89 | where | |
90 | T: Lower<DomainGoal<'tcx>> + ty::fold::TypeFoldable<'tcx>, | |
0531ce1d | 91 | { |
83c7162d XL |
92 | fn lower(&self) -> PolyDomainGoal<'tcx> { |
93 | self.map_bound_ref(|p| p.lower()) | |
0531ce1d XL |
94 | } |
95 | } | |
96 | ||
83c7162d XL |
97 | impl<'tcx> Lower<PolyDomainGoal<'tcx>> for ty::Predicate<'tcx> { |
98 | fn lower(&self) -> PolyDomainGoal<'tcx> { | |
8faf50e0 | 99 | use rustc::ty::Predicate; |
0531ce1d XL |
100 | |
101 | match self { | |
8faf50e0 XL |
102 | Predicate::Trait(predicate) => predicate.lower(), |
103 | Predicate::RegionOutlives(predicate) => predicate.lower(), | |
104 | Predicate::TypeOutlives(predicate) => predicate.lower(), | |
105 | Predicate::Projection(predicate) => predicate.lower(), | |
a1dfa0c6 XL |
106 | |
107 | Predicate::WellFormed(..) | | |
108 | Predicate::ObjectSafe(..) | | |
109 | Predicate::ClosureKind(..) | | |
110 | Predicate::Subtype(..) | | |
111 | Predicate::ConstEvaluatable(..) => { | |
112 | bug!("unexpected predicate {}", self) | |
83c7162d | 113 | } |
0531ce1d XL |
114 | } |
115 | } | |
116 | } | |
117 | ||
8faf50e0 | 118 | /// Used for implied bounds related rules (see rustc guide). |
83c7162d | 119 | trait IntoFromEnvGoal { |
8faf50e0 | 120 | /// Transforms an existing goal into a `FromEnv` goal. |
83c7162d XL |
121 | fn into_from_env_goal(self) -> Self; |
122 | } | |
0531ce1d | 123 | |
8faf50e0 XL |
124 | /// Used for well-formedness related rules (see rustc guide). |
125 | trait IntoWellFormedGoal { | |
126 | /// Transforms an existing goal into a `WellFormed` goal. | |
127 | fn into_well_formed_goal(self) -> Self; | |
128 | } | |
129 | ||
83c7162d XL |
130 | impl<'tcx> IntoFromEnvGoal for DomainGoal<'tcx> { |
131 | fn into_from_env_goal(self) -> DomainGoal<'tcx> { | |
8faf50e0 XL |
132 | use self::WhereClause::*; |
133 | ||
134 | match self { | |
135 | DomainGoal::Holds(Implemented(trait_ref)) => { | |
136 | DomainGoal::FromEnv(FromEnv::Trait(trait_ref)) | |
137 | } | |
138 | other => other, | |
139 | } | |
140 | } | |
141 | } | |
142 | ||
143 | impl<'tcx> IntoWellFormedGoal for DomainGoal<'tcx> { | |
144 | fn into_well_formed_goal(self) -> DomainGoal<'tcx> { | |
145 | use self::WhereClause::*; | |
146 | ||
83c7162d | 147 | match self { |
8faf50e0 XL |
148 | DomainGoal::Holds(Implemented(trait_ref)) => { |
149 | DomainGoal::WellFormed(WellFormed::Trait(trait_ref)) | |
150 | } | |
151 | other => other, | |
83c7162d | 152 | } |
0531ce1d XL |
153 | } |
154 | } | |
155 | ||
83c7162d XL |
156 | crate fn program_clauses_for<'a, 'tcx>( |
157 | tcx: TyCtxt<'a, 'tcx, 'tcx>, | |
158 | def_id: DefId, | |
159 | ) -> Clauses<'tcx> { | |
160 | match tcx.def_key(def_id).disambiguated_data.data { | |
9fa01778 XL |
161 | DefPathData::Trait(_) | |
162 | DefPathData::TraitAlias(_) => program_clauses_for_trait(tcx, def_id), | |
83c7162d XL |
163 | DefPathData::Impl => program_clauses_for_impl(tcx, def_id), |
164 | DefPathData::AssocTypeInImpl(..) => program_clauses_for_associated_type_value(tcx, def_id), | |
8faf50e0 XL |
165 | DefPathData::AssocTypeInTrait(..) => program_clauses_for_associated_type_def(tcx, def_id), |
166 | DefPathData::TypeNs(..) => program_clauses_for_type_def(tcx, def_id), | |
b7449926 | 167 | _ => List::empty(), |
83c7162d XL |
168 | } |
169 | } | |
170 | ||
83c7162d XL |
171 | fn program_clauses_for_trait<'a, 'tcx>( |
172 | tcx: TyCtxt<'a, 'tcx, 'tcx>, | |
173 | def_id: DefId, | |
174 | ) -> Clauses<'tcx> { | |
0531ce1d | 175 | // `trait Trait<P1..Pn> where WC { .. } // P0 == Self` |
83c7162d XL |
176 | |
177 | // Rule Implemented-From-Env (see rustc guide) | |
0531ce1d XL |
178 | // |
179 | // ``` | |
180 | // forall<Self, P1..Pn> { | |
181 | // Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>) | |
182 | // } | |
183 | // ``` | |
184 | ||
a1dfa0c6 XL |
185 | let bound_vars = Substs::bound_vars_for_item(tcx, def_id); |
186 | ||
0531ce1d XL |
187 | // `Self: Trait<P1..Pn>` |
188 | let trait_pred = ty::TraitPredicate { | |
a1dfa0c6 XL |
189 | trait_ref: ty::TraitRef { |
190 | def_id, | |
191 | substs: bound_vars, | |
192 | }, | |
0531ce1d | 193 | }; |
8faf50e0 | 194 | |
0531ce1d | 195 | // `Implemented(Self: Trait<P1..Pn>)` |
9fa01778 | 196 | let impl_trait: DomainGoal<'_> = trait_pred.lower(); |
8faf50e0 XL |
197 | |
198 | // `FromEnv(Self: Trait<P1..Pn>)` | |
0bf4aa26 | 199 | let from_env_goal = tcx.mk_goal(impl_trait.into_from_env_goal().into_goal()); |
8faf50e0 | 200 | let hypotheses = tcx.intern_goals(&[from_env_goal]); |
0531ce1d XL |
201 | |
202 | // `Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)` | |
83c7162d XL |
203 | let implemented_from_env = ProgramClause { |
204 | goal: impl_trait, | |
8faf50e0 | 205 | hypotheses, |
0bf4aa26 | 206 | category: ProgramClauseCategory::ImpliedBound, |
83c7162d | 207 | }; |
8faf50e0 | 208 | |
a1dfa0c6 | 209 | let implemented_from_env = Clause::ForAll(ty::Binder::bind(implemented_from_env)); |
83c7162d | 210 | |
a1dfa0c6 XL |
211 | let predicates = &tcx.predicates_defined_on(def_id).predicates; |
212 | let where_clauses = &predicates | |
213 | .iter() | |
0bf4aa26 XL |
214 | .map(|(wc, _)| wc.lower()) |
215 | .collect::<Vec<_>>(); | |
8faf50e0 | 216 | |
83c7162d XL |
217 | // Rule Implied-Bound-From-Trait |
218 | // | |
219 | // For each where clause WC: | |
220 | // ``` | |
221 | // forall<Self, P1..Pn> { | |
222 | // FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn) | |
223 | // } | |
224 | // ``` | |
225 | ||
226 | // `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`, for each where clause WC | |
8faf50e0 | 227 | let implied_bound_clauses = where_clauses |
0bf4aa26 XL |
228 | .iter() |
229 | .cloned() | |
83c7162d | 230 | |
8faf50e0 | 231 | // `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)` |
a1dfa0c6 XL |
232 | .map(|wc| { |
233 | // we move binders to the left | |
234 | wc.map_bound(|goal| ProgramClause { | |
0731742a XL |
235 | // FIXME: As where clauses can only bind lifetimes for now, and that named |
236 | // bound regions have a def-id, it is safe to just inject `bound_vars` and | |
237 | // `hypotheses` (which contain named vars bound at index `0`) into this | |
238 | // binding level. This may change if we ever allow where clauses to bind | |
239 | // types (e.g. for GATs things), because bound types only use a `BoundVar` | |
a1dfa0c6 | 240 | // index (no def-id). |
0731742a | 241 | goal: goal.subst(tcx, bound_vars).into_from_env_goal(), |
a1dfa0c6 XL |
242 | hypotheses, |
243 | ||
244 | category: ProgramClauseCategory::ImpliedBound, | |
245 | }) | |
246 | }) | |
8faf50e0 | 247 | .map(Clause::ForAll); |
0531ce1d | 248 | |
8faf50e0 XL |
249 | // Rule WellFormed-TraitRef |
250 | // | |
251 | // Here `WC` denotes the set of all where clauses: | |
252 | // ``` | |
253 | // forall<Self, P1..Pn> { | |
254 | // WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC) | |
255 | // } | |
256 | // ``` | |
257 | ||
a1dfa0c6 XL |
258 | // `WellFormed(WC)` |
259 | let wf_conditions = where_clauses | |
260 | .into_iter() | |
261 | .map(|wc| wc.map_bound(|goal| goal.into_well_formed_goal())); | |
83c7162d | 262 | |
8faf50e0 XL |
263 | // `WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)` |
264 | let wf_clause = ProgramClause { | |
265 | goal: DomainGoal::WellFormed(WellFormed::Trait(trait_pred)), | |
266 | hypotheses: tcx.mk_goals( | |
a1dfa0c6 XL |
267 | iter::once(tcx.mk_goal(GoalKind::DomainGoal(impl_trait))).chain( |
268 | wf_conditions.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))) | |
269 | ) | |
8faf50e0 | 270 | ), |
0bf4aa26 | 271 | category: ProgramClauseCategory::WellFormed, |
8faf50e0 | 272 | }; |
a1dfa0c6 | 273 | let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause)); |
8faf50e0 XL |
274 | |
275 | tcx.mk_clauses( | |
a1dfa0c6 | 276 | iter::once(implemented_from_env) |
8faf50e0 | 277 | .chain(implied_bound_clauses) |
a1dfa0c6 | 278 | .chain(iter::once(wf_clause)) |
8faf50e0 | 279 | ) |
83c7162d XL |
280 | } |
281 | ||
282 | fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId) -> Clauses<'tcx> { | |
0531ce1d | 283 | if let ImplPolarity::Negative = tcx.impl_polarity(def_id) { |
b7449926 | 284 | return List::empty(); |
0531ce1d XL |
285 | } |
286 | ||
287 | // Rule Implemented-From-Impl (see rustc guide) | |
288 | // | |
289 | // `impl<P0..Pn> Trait<A1..An> for A0 where WC { .. }` | |
290 | // | |
291 | // ``` | |
292 | // forall<P0..Pn> { | |
293 | // Implemented(A0: Trait<A1..An>) :- WC | |
294 | // } | |
295 | // ``` | |
296 | ||
a1dfa0c6 XL |
297 | let bound_vars = Substs::bound_vars_for_item(tcx, def_id); |
298 | ||
299 | let trait_ref = tcx.impl_trait_ref(def_id) | |
300 | .expect("not an impl") | |
301 | .subst(tcx, bound_vars); | |
8faf50e0 | 302 | |
0531ce1d XL |
303 | // `Implemented(A0: Trait<A1..An>)` |
304 | let trait_pred = ty::TraitPredicate { trait_ref }.lower(); | |
8faf50e0 | 305 | |
83c7162d | 306 | // `WC` |
a1dfa0c6 XL |
307 | let predicates = &tcx.predicates_of(def_id).predicates; |
308 | let where_clauses = predicates | |
309 | .iter() | |
310 | .map(|(wc, _)| wc.lower()) | |
311 | .map(|wc| wc.subst(tcx, bound_vars)); | |
0531ce1d | 312 | |
83c7162d XL |
313 | // `Implemented(A0: Trait<A1..An>) :- WC` |
314 | let clause = ProgramClause { | |
315 | goal: trait_pred, | |
316 | hypotheses: tcx.mk_goals( | |
317 | where_clauses | |
0bf4aa26 | 318 | .map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))), |
83c7162d | 319 | ), |
0bf4aa26 | 320 | category: ProgramClauseCategory::Other, |
83c7162d | 321 | }; |
a1dfa0c6 | 322 | tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::bind(clause)))) |
83c7162d XL |
323 | } |
324 | ||
8faf50e0 XL |
325 | pub fn program_clauses_for_type_def<'a, 'tcx>( |
326 | tcx: TyCtxt<'a, 'tcx, 'tcx>, | |
327 | def_id: DefId, | |
328 | ) -> Clauses<'tcx> { | |
329 | // Rule WellFormed-Type | |
330 | // | |
331 | // `struct Ty<P1..Pn> where WC1, ..., WCm` | |
332 | // | |
333 | // ``` | |
334 | // forall<P1..Pn> { | |
335 | // WellFormed(Ty<...>) :- WC1, ..., WCm` | |
336 | // } | |
337 | // ``` | |
338 | ||
a1dfa0c6 XL |
339 | let bound_vars = Substs::bound_vars_for_item(tcx, def_id); |
340 | ||
8faf50e0 | 341 | // `Ty<...>` |
a1dfa0c6 | 342 | let ty = tcx.type_of(def_id).subst(tcx, bound_vars); |
8faf50e0 XL |
343 | |
344 | // `WC` | |
0bf4aa26 | 345 | let where_clauses = tcx.predicates_of(def_id).predicates |
a1dfa0c6 | 346 | .iter() |
0bf4aa26 XL |
347 | .map(|(wc, _)| wc.lower()) |
348 | .collect::<Vec<_>>(); | |
8faf50e0 XL |
349 | |
350 | // `WellFormed(Ty<...>) :- WC1, ..., WCm` | |
a1dfa0c6 | 351 | let well_formed_clause = ProgramClause { |
8faf50e0 XL |
352 | goal: DomainGoal::WellFormed(WellFormed::Ty(ty)), |
353 | hypotheses: tcx.mk_goals( | |
354 | where_clauses | |
355 | .iter() | |
0731742a | 356 | .map(|wc| wc.subst(tcx, bound_vars)) |
0bf4aa26 | 357 | .map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))), |
8faf50e0 | 358 | ), |
0bf4aa26 | 359 | category: ProgramClauseCategory::WellFormed, |
8faf50e0 | 360 | }; |
a1dfa0c6 | 361 | let well_formed_clause = Clause::ForAll(ty::Binder::bind(well_formed_clause)); |
8faf50e0 | 362 | |
a1dfa0c6 | 363 | // Rule Implied-Bound-From-Type |
8faf50e0 XL |
364 | // |
365 | // For each where clause `WC`: | |
366 | // ``` | |
367 | // forall<P1..Pn> { | |
368 | // FromEnv(WC) :- FromEnv(Ty<...>) | |
369 | // } | |
370 | // ``` | |
371 | ||
372 | // `FromEnv(Ty<...>)` | |
0bf4aa26 | 373 | let from_env_goal = tcx.mk_goal(DomainGoal::FromEnv(FromEnv::Ty(ty)).into_goal()); |
8faf50e0 XL |
374 | let hypotheses = tcx.intern_goals(&[from_env_goal]); |
375 | ||
376 | // For each where clause `WC`: | |
377 | let from_env_clauses = where_clauses | |
378 | .into_iter() | |
379 | ||
380 | // `FromEnv(WC) :- FromEnv(Ty<...>)` | |
a1dfa0c6 XL |
381 | .map(|wc| { |
382 | // move the binders to the left | |
383 | wc.map_bound(|goal| ProgramClause { | |
0731742a XL |
384 | // FIXME: we inject `bound_vars` and `hypotheses` into this binding |
385 | // level, which may be incorrect in the future: see the FIXME in | |
386 | // `program_clauses_for_trait`. | |
387 | goal: goal.subst(tcx, bound_vars).into_from_env_goal(), | |
a1dfa0c6 XL |
388 | hypotheses, |
389 | ||
390 | category: ProgramClauseCategory::ImpliedBound, | |
391 | }) | |
392 | }) | |
8faf50e0 XL |
393 | |
394 | .map(Clause::ForAll); | |
395 | ||
a1dfa0c6 | 396 | tcx.mk_clauses(iter::once(well_formed_clause).chain(from_env_clauses)) |
8faf50e0 XL |
397 | } |
398 | ||
399 | pub fn program_clauses_for_associated_type_def<'a, 'tcx>( | |
0bf4aa26 XL |
400 | tcx: TyCtxt<'a, 'tcx, 'tcx>, |
401 | item_id: DefId, | |
8faf50e0 | 402 | ) -> Clauses<'tcx> { |
a1dfa0c6 | 403 | // Rule ProjectionEq-Placeholder |
0bf4aa26 XL |
404 | // |
405 | // ``` | |
406 | // trait Trait<P1..Pn> { | |
407 | // type AssocType<Pn+1..Pm>; | |
408 | // } | |
409 | // ``` | |
410 | // | |
411 | // `ProjectionEq` can succeed by skolemizing, see "associated type" | |
412 | // chapter for more: | |
413 | // ``` | |
414 | // forall<Self, P1..Pn, Pn+1..Pm> { | |
415 | // ProjectionEq( | |
416 | // <Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> = | |
417 | // (Trait::AssocType)<Self, P1..Pn, Pn+1..Pm> | |
418 | // ) | |
419 | // } | |
420 | // ``` | |
421 | ||
422 | let item = tcx.associated_item(item_id); | |
423 | debug_assert_eq!(item.kind, ty::AssociatedKind::Type); | |
424 | let trait_id = match item.container { | |
425 | ty::AssociatedItemContainer::TraitContainer(trait_id) => trait_id, | |
426 | _ => bug!("not an trait container"), | |
427 | }; | |
a1dfa0c6 XL |
428 | |
429 | let trait_bound_vars = Substs::bound_vars_for_item(tcx, trait_id); | |
430 | let trait_ref = ty::TraitRef { | |
431 | def_id: trait_id, | |
432 | substs: trait_bound_vars, | |
433 | }; | |
0bf4aa26 XL |
434 | |
435 | let projection_ty = ty::ProjectionTy::from_ref_and_name(tcx, trait_ref, item.ident); | |
436 | let placeholder_ty = tcx.mk_ty(ty::UnnormalizedProjection(projection_ty)); | |
437 | let projection_eq = WhereClause::ProjectionEq(ty::ProjectionPredicate { | |
438 | projection_ty, | |
439 | ty: placeholder_ty, | |
440 | }); | |
441 | ||
442 | let projection_eq_clause = ProgramClause { | |
443 | goal: DomainGoal::Holds(projection_eq), | |
444 | hypotheses: ty::List::empty(), | |
445 | category: ProgramClauseCategory::Other, | |
446 | }; | |
a1dfa0c6 | 447 | let projection_eq_clause = Clause::ForAll(ty::Binder::bind(projection_eq_clause)); |
0bf4aa26 XL |
448 | |
449 | // Rule WellFormed-AssocTy | |
450 | // ``` | |
451 | // forall<Self, P1..Pn, Pn+1..Pm> { | |
452 | // WellFormed((Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>) | |
453 | // :- Implemented(Self: Trait<P1..Pn>) | |
454 | // } | |
455 | // ``` | |
456 | ||
457 | let trait_predicate = ty::TraitPredicate { trait_ref }; | |
458 | let hypothesis = tcx.mk_goal( | |
459 | DomainGoal::Holds(WhereClause::Implemented(trait_predicate)).into_goal() | |
460 | ); | |
a1dfa0c6 | 461 | |
0bf4aa26 XL |
462 | let wf_clause = ProgramClause { |
463 | goal: DomainGoal::WellFormed(WellFormed::Ty(placeholder_ty)), | |
464 | hypotheses: tcx.mk_goals(iter::once(hypothesis)), | |
465 | category: ProgramClauseCategory::WellFormed, | |
466 | }; | |
a1dfa0c6 | 467 | let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause)); |
0bf4aa26 XL |
468 | |
469 | // Rule Implied-Trait-From-AssocTy | |
470 | // ``` | |
471 | // forall<Self, P1..Pn, Pn+1..Pm> { | |
472 | // FromEnv(Self: Trait<P1..Pn>) | |
473 | // :- FromEnv((Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>) | |
474 | // } | |
475 | // ``` | |
476 | ||
477 | let hypothesis = tcx.mk_goal( | |
478 | DomainGoal::FromEnv(FromEnv::Ty(placeholder_ty)).into_goal() | |
479 | ); | |
a1dfa0c6 | 480 | |
0bf4aa26 XL |
481 | let from_env_clause = ProgramClause { |
482 | goal: DomainGoal::FromEnv(FromEnv::Trait(trait_predicate)), | |
483 | hypotheses: tcx.mk_goals(iter::once(hypothesis)), | |
484 | category: ProgramClauseCategory::ImpliedBound, | |
485 | }; | |
a1dfa0c6 XL |
486 | let from_env_clause = Clause::ForAll(ty::Binder::bind(from_env_clause)); |
487 | ||
488 | // Rule ProjectionEq-Normalize | |
489 | // | |
490 | // ProjectionEq can succeed by normalizing: | |
491 | // ``` | |
492 | // forall<Self, P1..Pn, Pn+1..Pm, U> { | |
493 | // ProjectionEq(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> = U) :- | |
494 | // Normalize(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> -> U) | |
495 | // } | |
496 | // ``` | |
497 | ||
498 | let offset = tcx.generics_of(trait_id).params | |
499 | .iter() | |
500 | .map(|p| p.index) | |
501 | .max() | |
502 | .unwrap_or(0); | |
503 | // Add a new type param after the existing ones (`U` in the comment above). | |
504 | let ty_var = ty::Bound( | |
505 | ty::INNERMOST, | |
506 | ty::BoundVar::from_u32(offset + 1).into() | |
507 | ); | |
508 | ||
509 | // `ProjectionEq(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> = U)` | |
510 | let projection = ty::ProjectionPredicate { | |
511 | projection_ty, | |
512 | ty: tcx.mk_ty(ty_var), | |
513 | }; | |
514 | ||
515 | // `Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> U)` | |
516 | let hypothesis = tcx.mk_goal( | |
517 | DomainGoal::Normalize(projection).into_goal() | |
518 | ); | |
519 | ||
520 | // ProjectionEq(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> = U) :- | |
521 | // Normalize(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> -> U) | |
522 | let normalize_clause = ProgramClause { | |
523 | goal: DomainGoal::Holds(WhereClause::ProjectionEq(projection)), | |
524 | hypotheses: tcx.mk_goals(iter::once(hypothesis)), | |
525 | category: ProgramClauseCategory::Other, | |
526 | }; | |
527 | let normalize_clause = Clause::ForAll(ty::Binder::bind(normalize_clause)); | |
0bf4aa26 XL |
528 | |
529 | let clauses = iter::once(projection_eq_clause) | |
530 | .chain(iter::once(wf_clause)) | |
a1dfa0c6 XL |
531 | .chain(iter::once(from_env_clause)) |
532 | .chain(iter::once(normalize_clause)); | |
533 | ||
0bf4aa26 | 534 | tcx.mk_clauses(clauses) |
8faf50e0 XL |
535 | } |
536 | ||
83c7162d XL |
537 | pub fn program_clauses_for_associated_type_value<'a, 'tcx>( |
538 | tcx: TyCtxt<'a, 'tcx, 'tcx>, | |
539 | item_id: DefId, | |
540 | ) -> Clauses<'tcx> { | |
541 | // Rule Normalize-From-Impl (see rustc guide) | |
542 | // | |
0bf4aa26 XL |
543 | // ``` |
544 | // impl<P0..Pn> Trait<A1..An> for A0 { | |
8faf50e0 | 545 | // type AssocType<Pn+1..Pm> = T; |
0bf4aa26 XL |
546 | // } |
547 | // ``` | |
83c7162d | 548 | // |
8faf50e0 | 549 | // FIXME: For the moment, we don't account for where clauses written on the associated |
0731742a | 550 | // ty definition (i.e., in the trait def, as in `type AssocType<T> where T: Sized`). |
83c7162d XL |
551 | // ``` |
552 | // forall<P0..Pm> { | |
553 | // forall<Pn+1..Pm> { | |
554 | // Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T) :- | |
8faf50e0 | 555 | // Implemented(A0: Trait<A1..An>) |
83c7162d XL |
556 | // } |
557 | // } | |
558 | // ``` | |
559 | ||
560 | let item = tcx.associated_item(item_id); | |
561 | debug_assert_eq!(item.kind, ty::AssociatedKind::Type); | |
8faf50e0 XL |
562 | let impl_id = match item.container { |
563 | ty::AssociatedItemContainer::ImplContainer(impl_id) => impl_id, | |
564 | _ => bug!("not an impl container"), | |
83c7162d | 565 | }; |
8faf50e0 | 566 | |
a1dfa0c6 XL |
567 | let impl_bound_vars = Substs::bound_vars_for_item(tcx, impl_id); |
568 | ||
83c7162d | 569 | // `A0 as Trait<A1..An>` |
a1dfa0c6 XL |
570 | let trait_ref = tcx.impl_trait_ref(impl_id) |
571 | .unwrap() | |
572 | .subst(tcx, impl_bound_vars); | |
8faf50e0 | 573 | |
83c7162d XL |
574 | // `T` |
575 | let ty = tcx.type_of(item_id); | |
8faf50e0 | 576 | |
83c7162d | 577 | // `Implemented(A0: Trait<A1..An>)` |
9fa01778 | 578 | let trait_implemented: DomainGoal<'_> = ty::TraitPredicate { trait_ref }.lower(); |
8faf50e0 | 579 | |
83c7162d | 580 | // `<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm>` |
8faf50e0 XL |
581 | let projection_ty = ty::ProjectionTy::from_ref_and_name(tcx, trait_ref, item.ident); |
582 | ||
83c7162d XL |
583 | // `Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T)` |
584 | let normalize_goal = DomainGoal::Normalize(ty::ProjectionPredicate { projection_ty, ty }); | |
8faf50e0 | 585 | |
83c7162d | 586 | // `Normalize(... -> T) :- ...` |
a1dfa0c6 | 587 | let normalize_clause = ProgramClause { |
83c7162d XL |
588 | goal: normalize_goal, |
589 | hypotheses: tcx.mk_goals( | |
a1dfa0c6 | 590 | iter::once(tcx.mk_goal(GoalKind::DomainGoal(trait_implemented))) |
83c7162d | 591 | ), |
0bf4aa26 | 592 | category: ProgramClauseCategory::Other, |
83c7162d | 593 | }; |
a1dfa0c6 XL |
594 | let normalize_clause = Clause::ForAll(ty::Binder::bind(normalize_clause)); |
595 | ||
596 | tcx.mk_clauses(iter::once(normalize_clause)) | |
0531ce1d XL |
597 | } |
598 | ||
599 | pub fn dump_program_clauses<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>) { | |
600 | if !tcx.features().rustc_attrs { | |
601 | return; | |
602 | } | |
603 | ||
604 | let mut visitor = ClauseDumper { tcx }; | |
0731742a | 605 | tcx.hir() |
83c7162d XL |
606 | .krate() |
607 | .visit_all_item_likes(&mut visitor.as_deep_visitor()); | |
0531ce1d XL |
608 | } |
609 | ||
610 | struct ClauseDumper<'a, 'tcx: 'a> { | |
611 | tcx: TyCtxt<'a, 'tcx, 'tcx>, | |
612 | } | |
613 | ||
83c7162d | 614 | impl<'a, 'tcx> ClauseDumper<'a, 'tcx> { |
0531ce1d | 615 | fn process_attrs(&mut self, node_id: ast::NodeId, attrs: &[ast::Attribute]) { |
0731742a | 616 | let def_id = self.tcx.hir().local_def_id(node_id); |
0531ce1d | 617 | for attr in attrs { |
83c7162d XL |
618 | let mut clauses = None; |
619 | ||
0531ce1d | 620 | if attr.check_name("rustc_dump_program_clauses") { |
83c7162d XL |
621 | clauses = Some(self.tcx.program_clauses_for(def_id)); |
622 | } | |
623 | ||
624 | if attr.check_name("rustc_dump_env_program_clauses") { | |
0bf4aa26 | 625 | let environment = self.tcx.environment(def_id); |
0731742a | 626 | clauses = Some(self.tcx.program_clauses_for_env(environment)); |
83c7162d XL |
627 | } |
628 | ||
629 | if let Some(clauses) = clauses { | |
8faf50e0 XL |
630 | let mut err = self |
631 | .tcx | |
83c7162d XL |
632 | .sess |
633 | .struct_span_err(attr.span, "program clause dump"); | |
634 | ||
635 | let mut strings: Vec<_> = clauses | |
636 | .iter() | |
a1dfa0c6 | 637 | .map(|clause| clause.to_string()) |
83c7162d XL |
638 | .collect(); |
639 | ||
640 | strings.sort(); | |
641 | ||
642 | for string in strings { | |
643 | err.note(&string); | |
0531ce1d | 644 | } |
83c7162d XL |
645 | |
646 | err.emit(); | |
0531ce1d XL |
647 | } |
648 | } | |
649 | } | |
650 | } | |
651 | ||
652 | impl<'a, 'tcx> Visitor<'tcx> for ClauseDumper<'a, 'tcx> { | |
653 | fn nested_visit_map<'this>(&'this mut self) -> NestedVisitorMap<'this, 'tcx> { | |
0731742a | 654 | NestedVisitorMap::OnlyBodies(&self.tcx.hir()) |
0531ce1d XL |
655 | } |
656 | ||
657 | fn visit_item(&mut self, item: &'tcx hir::Item) { | |
658 | self.process_attrs(item.id, &item.attrs); | |
659 | intravisit::walk_item(self, item); | |
660 | } | |
661 | ||
662 | fn visit_trait_item(&mut self, trait_item: &'tcx hir::TraitItem) { | |
663 | self.process_attrs(trait_item.id, &trait_item.attrs); | |
664 | intravisit::walk_trait_item(self, trait_item); | |
665 | } | |
666 | ||
667 | fn visit_impl_item(&mut self, impl_item: &'tcx hir::ImplItem) { | |
668 | self.process_attrs(impl_item.id, &impl_item.attrs); | |
669 | intravisit::walk_impl_item(self, impl_item); | |
670 | } | |
671 | ||
672 | fn visit_struct_field(&mut self, s: &'tcx hir::StructField) { | |
673 | self.process_attrs(s.id, &s.attrs); | |
674 | intravisit::walk_struct_field(self, s); | |
675 | } | |
676 | } |