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