]>
Commit | Line | Data |
---|---|---|
0531ce1d XL |
1 | // Copyright 2018 The Rust Project Developers. See the COPYRIGHT |
2 | // file at the top-level directory of this distribution and at | |
3 | // http://rust-lang.org/COPYRIGHT. | |
4 | // | |
5 | // Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or | |
6 | // http://www.apache.org/licenses/LICENSE-2.0> or the MIT license | |
7 | // <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your | |
8 | // option. This file may not be copied, modified, or distributed | |
9 | // except according to those terms. | |
10 | ||
0531ce1d XL |
11 | use rustc::hir::def_id::DefId; |
12 | use rustc::hir::intravisit::{self, NestedVisitorMap, Visitor}; | |
83c7162d XL |
13 | use rustc::hir::map::definitions::DefPathData; |
14 | use rustc::hir::{self, ImplPolarity}; | |
8faf50e0 XL |
15 | use rustc::traits::{ |
16 | Clause, Clauses, DomainGoal, FromEnv, Goal, PolyDomainGoal, ProgramClause, WellFormed, | |
17 | WhereClause, | |
18 | }; | |
19 | use rustc::ty::query::Providers; | |
b7449926 | 20 | use rustc::ty::{self, List, TyCtxt}; |
83c7162d XL |
21 | use rustc_data_structures::fx::FxHashSet; |
22 | use std::mem; | |
0531ce1d | 23 | use syntax::ast; |
83c7162d XL |
24 | |
25 | use std::iter; | |
0531ce1d | 26 | |
8faf50e0 XL |
27 | crate fn provide(p: &mut Providers) { |
28 | *p = Providers { | |
29 | program_clauses_for, | |
30 | program_clauses_for_env, | |
31 | ..*p | |
32 | }; | |
33 | } | |
34 | ||
94b46f34 | 35 | crate trait Lower<T> { |
8faf50e0 | 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 | |
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 | |
83c7162d | 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(), | |
106 | Predicate::WellFormed(ty) => { | |
107 | ty::Binder::dummy(DomainGoal::WellFormed(WellFormed::Ty(*ty))) | |
83c7162d | 108 | } |
8faf50e0 XL |
109 | Predicate::ObjectSafe(..) |
110 | | Predicate::ClosureKind(..) | |
111 | | Predicate::Subtype(..) | |
112 | | Predicate::ConstEvaluatable(..) => unimplemented!(), | |
0531ce1d XL |
113 | } |
114 | } | |
115 | } | |
116 | ||
8faf50e0 | 117 | /// Used for implied bounds related rules (see rustc guide). |
83c7162d | 118 | trait IntoFromEnvGoal { |
8faf50e0 | 119 | /// Transforms an existing goal into a `FromEnv` goal. |
83c7162d XL |
120 | fn into_from_env_goal(self) -> Self; |
121 | } | |
0531ce1d | 122 | |
8faf50e0 XL |
123 | /// Used for well-formedness related rules (see rustc guide). |
124 | trait IntoWellFormedGoal { | |
125 | /// Transforms an existing goal into a `WellFormed` goal. | |
126 | fn into_well_formed_goal(self) -> Self; | |
127 | } | |
128 | ||
83c7162d XL |
129 | impl<'tcx> IntoFromEnvGoal for DomainGoal<'tcx> { |
130 | fn into_from_env_goal(self) -> DomainGoal<'tcx> { | |
8faf50e0 XL |
131 | use self::WhereClause::*; |
132 | ||
133 | match self { | |
134 | DomainGoal::Holds(Implemented(trait_ref)) => { | |
135 | DomainGoal::FromEnv(FromEnv::Trait(trait_ref)) | |
136 | } | |
137 | other => other, | |
138 | } | |
139 | } | |
140 | } | |
141 | ||
142 | impl<'tcx> IntoWellFormedGoal for DomainGoal<'tcx> { | |
143 | fn into_well_formed_goal(self) -> DomainGoal<'tcx> { | |
144 | use self::WhereClause::*; | |
145 | ||
83c7162d | 146 | match self { |
8faf50e0 XL |
147 | DomainGoal::Holds(Implemented(trait_ref)) => { |
148 | DomainGoal::WellFormed(WellFormed::Trait(trait_ref)) | |
149 | } | |
150 | other => other, | |
83c7162d | 151 | } |
0531ce1d XL |
152 | } |
153 | } | |
154 | ||
83c7162d XL |
155 | crate fn program_clauses_for<'a, 'tcx>( |
156 | tcx: TyCtxt<'a, 'tcx, 'tcx>, | |
157 | def_id: DefId, | |
158 | ) -> Clauses<'tcx> { | |
159 | match tcx.def_key(def_id).disambiguated_data.data { | |
160 | DefPathData::Trait(_) => program_clauses_for_trait(tcx, def_id), | |
161 | DefPathData::Impl => program_clauses_for_impl(tcx, def_id), | |
162 | DefPathData::AssocTypeInImpl(..) => program_clauses_for_associated_type_value(tcx, def_id), | |
8faf50e0 XL |
163 | DefPathData::AssocTypeInTrait(..) => program_clauses_for_associated_type_def(tcx, def_id), |
164 | DefPathData::TypeNs(..) => program_clauses_for_type_def(tcx, def_id), | |
b7449926 | 165 | _ => List::empty(), |
83c7162d XL |
166 | } |
167 | } | |
168 | ||
169 | crate fn program_clauses_for_env<'a, 'tcx>( | |
170 | tcx: TyCtxt<'a, 'tcx, 'tcx>, | |
171 | param_env: ty::ParamEnv<'tcx>, | |
172 | ) -> Clauses<'tcx> { | |
173 | debug!("program_clauses_for_env(param_env={:?})", param_env); | |
174 | ||
175 | let mut last_round = FxHashSet(); | |
176 | last_round.extend( | |
177 | param_env | |
178 | .caller_bounds | |
179 | .iter() | |
180 | .flat_map(|&p| predicate_def_id(p)), | |
181 | ); | |
182 | ||
183 | let mut closure = last_round.clone(); | |
184 | let mut next_round = FxHashSet(); | |
185 | while !last_round.is_empty() { | |
186 | next_round.extend( | |
187 | last_round | |
188 | .drain() | |
189 | .flat_map(|def_id| { | |
190 | tcx.predicates_of(def_id) | |
191 | .instantiate_identity(tcx) | |
192 | .predicates | |
193 | }) | |
194 | .flat_map(|p| predicate_def_id(p)) | |
195 | .filter(|&def_id| closure.insert(def_id)), | |
196 | ); | |
197 | mem::swap(&mut next_round, &mut last_round); | |
198 | } | |
199 | ||
200 | debug!("program_clauses_for_env: closure = {:#?}", closure); | |
201 | ||
202 | return tcx.mk_clauses( | |
203 | closure | |
204 | .into_iter() | |
205 | .flat_map(|def_id| tcx.program_clauses_for(def_id).iter().cloned()), | |
206 | ); | |
207 | ||
208 | /// Given that `predicate` is in the environment, returns the | |
209 | /// def-id of something (e.g., a trait, associated item, etc) | |
210 | /// whose predicates can also be assumed to be true. We will | |
211 | /// compute the transitive closure of such things. | |
212 | fn predicate_def_id<'tcx>(predicate: ty::Predicate<'tcx>) -> Option<DefId> { | |
213 | match predicate { | |
214 | ty::Predicate::Trait(predicate) => Some(predicate.def_id()), | |
215 | ||
216 | ty::Predicate::Projection(projection) => Some(projection.item_def_id()), | |
217 | ||
218 | ty::Predicate::WellFormed(..) | |
219 | | ty::Predicate::RegionOutlives(..) | |
220 | | ty::Predicate::TypeOutlives(..) | |
221 | | ty::Predicate::ObjectSafe(..) | |
222 | | ty::Predicate::ClosureKind(..) | |
223 | | ty::Predicate::Subtype(..) | |
224 | | ty::Predicate::ConstEvaluatable(..) => None, | |
225 | } | |
226 | } | |
227 | } | |
228 | ||
229 | fn program_clauses_for_trait<'a, 'tcx>( | |
230 | tcx: TyCtxt<'a, 'tcx, 'tcx>, | |
231 | def_id: DefId, | |
232 | ) -> Clauses<'tcx> { | |
0531ce1d | 233 | // `trait Trait<P1..Pn> where WC { .. } // P0 == Self` |
83c7162d XL |
234 | |
235 | // Rule Implemented-From-Env (see rustc guide) | |
0531ce1d XL |
236 | // |
237 | // ``` | |
238 | // forall<Self, P1..Pn> { | |
239 | // Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>) | |
240 | // } | |
241 | // ``` | |
242 | ||
243 | // `Self: Trait<P1..Pn>` | |
244 | let trait_pred = ty::TraitPredicate { | |
8faf50e0 | 245 | trait_ref: ty::TraitRef::identity(tcx, def_id), |
0531ce1d | 246 | }; |
8faf50e0 | 247 | |
0531ce1d | 248 | // `Implemented(Self: Trait<P1..Pn>)` |
8faf50e0 XL |
249 | let impl_trait: DomainGoal = trait_pred.lower(); |
250 | ||
251 | // `FromEnv(Self: Trait<P1..Pn>)` | |
252 | let from_env_goal = impl_trait.into_from_env_goal().into_goal(); | |
253 | let hypotheses = tcx.intern_goals(&[from_env_goal]); | |
0531ce1d XL |
254 | |
255 | // `Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)` | |
83c7162d XL |
256 | let implemented_from_env = ProgramClause { |
257 | goal: impl_trait, | |
8faf50e0 | 258 | hypotheses, |
83c7162d | 259 | }; |
8faf50e0 | 260 | |
83c7162d XL |
261 | let clauses = iter::once(Clause::ForAll(ty::Binder::dummy(implemented_from_env))); |
262 | ||
8faf50e0 XL |
263 | let where_clauses = &tcx.predicates_defined_on(def_id).predicates; |
264 | ||
83c7162d XL |
265 | // Rule Implied-Bound-From-Trait |
266 | // | |
267 | // For each where clause WC: | |
268 | // ``` | |
269 | // forall<Self, P1..Pn> { | |
270 | // FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn) | |
271 | // } | |
272 | // ``` | |
273 | ||
274 | // `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`, for each where clause WC | |
8faf50e0 | 275 | let implied_bound_clauses = where_clauses |
83c7162d | 276 | .into_iter() |
8faf50e0 | 277 | .map(|wc| wc.lower()) |
83c7162d | 278 | |
8faf50e0 XL |
279 | // `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)` |
280 | .map(|wc| wc.map_bound(|goal| ProgramClause { | |
281 | goal: goal.into_from_env_goal(), | |
282 | hypotheses, | |
283 | })) | |
284 | .map(Clause::ForAll); | |
0531ce1d | 285 | |
8faf50e0 XL |
286 | // Rule WellFormed-TraitRef |
287 | // | |
288 | // Here `WC` denotes the set of all where clauses: | |
289 | // ``` | |
290 | // forall<Self, P1..Pn> { | |
291 | // WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC) | |
292 | // } | |
293 | // ``` | |
294 | ||
295 | // `Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)` | |
296 | let wf_conditions = iter::once(ty::Binder::dummy(trait_pred.lower())) | |
297 | .chain( | |
298 | where_clauses | |
299 | .into_iter() | |
300 | .map(|wc| wc.lower()) | |
301 | .map(|wc| wc.map_bound(|goal| goal.into_well_formed_goal())) | |
302 | ); | |
83c7162d | 303 | |
8faf50e0 XL |
304 | // `WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)` |
305 | let wf_clause = ProgramClause { | |
306 | goal: DomainGoal::WellFormed(WellFormed::Trait(trait_pred)), | |
307 | hypotheses: tcx.mk_goals( | |
308 | wf_conditions.map(|wc| Goal::from_poly_domain_goal(wc, tcx)), | |
309 | ), | |
310 | }; | |
311 | let wf_clause = iter::once(Clause::ForAll(ty::Binder::dummy(wf_clause))); | |
312 | ||
313 | tcx.mk_clauses( | |
314 | clauses | |
315 | .chain(implied_bound_clauses) | |
316 | .chain(wf_clause) | |
317 | ) | |
83c7162d XL |
318 | } |
319 | ||
320 | fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId) -> Clauses<'tcx> { | |
0531ce1d | 321 | if let ImplPolarity::Negative = tcx.impl_polarity(def_id) { |
b7449926 | 322 | return List::empty(); |
0531ce1d XL |
323 | } |
324 | ||
325 | // Rule Implemented-From-Impl (see rustc guide) | |
326 | // | |
327 | // `impl<P0..Pn> Trait<A1..An> for A0 where WC { .. }` | |
328 | // | |
329 | // ``` | |
330 | // forall<P0..Pn> { | |
331 | // Implemented(A0: Trait<A1..An>) :- WC | |
332 | // } | |
333 | // ``` | |
334 | ||
8faf50e0 XL |
335 | let trait_ref = tcx.impl_trait_ref(def_id).expect("not an impl"); |
336 | ||
0531ce1d XL |
337 | // `Implemented(A0: Trait<A1..An>)` |
338 | let trait_pred = ty::TraitPredicate { trait_ref }.lower(); | |
8faf50e0 | 339 | |
83c7162d | 340 | // `WC` |
0531ce1d XL |
341 | let where_clauses = tcx.predicates_of(def_id).predicates.lower(); |
342 | ||
83c7162d XL |
343 | // `Implemented(A0: Trait<A1..An>) :- WC` |
344 | let clause = ProgramClause { | |
345 | goal: trait_pred, | |
346 | hypotheses: tcx.mk_goals( | |
347 | where_clauses | |
348 | .into_iter() | |
349 | .map(|wc| Goal::from_poly_domain_goal(wc, tcx)), | |
350 | ), | |
351 | }; | |
94b46f34 | 352 | tcx.intern_clauses(&[Clause::ForAll(ty::Binder::dummy(clause))]) |
83c7162d XL |
353 | } |
354 | ||
8faf50e0 XL |
355 | pub fn program_clauses_for_type_def<'a, 'tcx>( |
356 | tcx: TyCtxt<'a, 'tcx, 'tcx>, | |
357 | def_id: DefId, | |
358 | ) -> Clauses<'tcx> { | |
359 | // Rule WellFormed-Type | |
360 | // | |
361 | // `struct Ty<P1..Pn> where WC1, ..., WCm` | |
362 | // | |
363 | // ``` | |
364 | // forall<P1..Pn> { | |
365 | // WellFormed(Ty<...>) :- WC1, ..., WCm` | |
366 | // } | |
367 | // ``` | |
368 | ||
369 | // `Ty<...>` | |
370 | let ty = tcx.type_of(def_id); | |
371 | ||
372 | // `WC` | |
373 | let where_clauses = tcx.predicates_of(def_id).predicates.lower(); | |
374 | ||
375 | // `WellFormed(Ty<...>) :- WC1, ..., WCm` | |
376 | let well_formed = ProgramClause { | |
377 | goal: DomainGoal::WellFormed(WellFormed::Ty(ty)), | |
378 | hypotheses: tcx.mk_goals( | |
379 | where_clauses | |
380 | .iter() | |
381 | .cloned() | |
382 | .map(|wc| Goal::from_poly_domain_goal(wc, tcx)), | |
383 | ), | |
384 | }; | |
385 | ||
386 | let well_formed_clause = iter::once(Clause::ForAll(ty::Binder::dummy(well_formed))); | |
387 | ||
388 | // Rule FromEnv-Type | |
389 | // | |
390 | // For each where clause `WC`: | |
391 | // ``` | |
392 | // forall<P1..Pn> { | |
393 | // FromEnv(WC) :- FromEnv(Ty<...>) | |
394 | // } | |
395 | // ``` | |
396 | ||
397 | // `FromEnv(Ty<...>)` | |
398 | let from_env_goal = DomainGoal::FromEnv(FromEnv::Ty(ty)).into_goal(); | |
399 | let hypotheses = tcx.intern_goals(&[from_env_goal]); | |
400 | ||
401 | // For each where clause `WC`: | |
402 | let from_env_clauses = where_clauses | |
403 | .into_iter() | |
404 | ||
405 | // `FromEnv(WC) :- FromEnv(Ty<...>)` | |
406 | .map(|wc| wc.map_bound(|goal| ProgramClause { | |
407 | goal: goal.into_from_env_goal(), | |
408 | hypotheses, | |
409 | })) | |
410 | ||
411 | .map(Clause::ForAll); | |
412 | ||
413 | tcx.mk_clauses(well_formed_clause.chain(from_env_clauses)) | |
414 | } | |
415 | ||
416 | pub fn program_clauses_for_associated_type_def<'a, 'tcx>( | |
417 | _tcx: TyCtxt<'a, 'tcx, 'tcx>, | |
418 | _item_id: DefId, | |
419 | ) -> Clauses<'tcx> { | |
420 | unimplemented!() | |
421 | } | |
422 | ||
83c7162d XL |
423 | pub fn program_clauses_for_associated_type_value<'a, 'tcx>( |
424 | tcx: TyCtxt<'a, 'tcx, 'tcx>, | |
425 | item_id: DefId, | |
426 | ) -> Clauses<'tcx> { | |
427 | // Rule Normalize-From-Impl (see rustc guide) | |
428 | // | |
429 | // ```impl<P0..Pn> Trait<A1..An> for A0 | |
430 | // { | |
8faf50e0 | 431 | // type AssocType<Pn+1..Pm> = T; |
83c7162d XL |
432 | // }``` |
433 | // | |
8faf50e0 XL |
434 | // FIXME: For the moment, we don't account for where clauses written on the associated |
435 | // ty definition (i.e. in the trait def, as in `type AssocType<T> where T: Sized`). | |
83c7162d XL |
436 | // ``` |
437 | // forall<P0..Pm> { | |
438 | // forall<Pn+1..Pm> { | |
439 | // Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T) :- | |
8faf50e0 | 440 | // Implemented(A0: Trait<A1..An>) |
83c7162d XL |
441 | // } |
442 | // } | |
443 | // ``` | |
444 | ||
445 | let item = tcx.associated_item(item_id); | |
446 | debug_assert_eq!(item.kind, ty::AssociatedKind::Type); | |
8faf50e0 XL |
447 | let impl_id = match item.container { |
448 | ty::AssociatedItemContainer::ImplContainer(impl_id) => impl_id, | |
449 | _ => bug!("not an impl container"), | |
83c7162d | 450 | }; |
8faf50e0 | 451 | |
83c7162d XL |
452 | // `A0 as Trait<A1..An>` |
453 | let trait_ref = tcx.impl_trait_ref(impl_id).unwrap(); | |
8faf50e0 | 454 | |
83c7162d XL |
455 | // `T` |
456 | let ty = tcx.type_of(item_id); | |
8faf50e0 | 457 | |
83c7162d XL |
458 | // `Implemented(A0: Trait<A1..An>)` |
459 | let trait_implemented = ty::Binder::dummy(ty::TraitPredicate { trait_ref }.lower()); | |
8faf50e0 XL |
460 | |
461 | // `Implemented(A0: Trait<A1..An>)` | |
462 | let hypotheses = vec![trait_implemented]; | |
463 | ||
83c7162d | 464 | // `<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm>` |
8faf50e0 XL |
465 | let projection_ty = ty::ProjectionTy::from_ref_and_name(tcx, trait_ref, item.ident); |
466 | ||
83c7162d XL |
467 | // `Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T)` |
468 | let normalize_goal = DomainGoal::Normalize(ty::ProjectionPredicate { projection_ty, ty }); | |
8faf50e0 | 469 | |
83c7162d XL |
470 | // `Normalize(... -> T) :- ...` |
471 | let clause = ProgramClause { | |
472 | goal: normalize_goal, | |
473 | hypotheses: tcx.mk_goals( | |
8faf50e0 | 474 | hypotheses |
83c7162d XL |
475 | .into_iter() |
476 | .map(|wc| Goal::from_poly_domain_goal(wc, tcx)), | |
477 | ), | |
478 | }; | |
94b46f34 | 479 | tcx.intern_clauses(&[Clause::ForAll(ty::Binder::dummy(clause))]) |
0531ce1d XL |
480 | } |
481 | ||
482 | pub fn dump_program_clauses<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>) { | |
483 | if !tcx.features().rustc_attrs { | |
484 | return; | |
485 | } | |
486 | ||
487 | let mut visitor = ClauseDumper { tcx }; | |
83c7162d XL |
488 | tcx.hir |
489 | .krate() | |
490 | .visit_all_item_likes(&mut visitor.as_deep_visitor()); | |
0531ce1d XL |
491 | } |
492 | ||
493 | struct ClauseDumper<'a, 'tcx: 'a> { | |
494 | tcx: TyCtxt<'a, 'tcx, 'tcx>, | |
495 | } | |
496 | ||
83c7162d | 497 | impl<'a, 'tcx> ClauseDumper<'a, 'tcx> { |
0531ce1d XL |
498 | fn process_attrs(&mut self, node_id: ast::NodeId, attrs: &[ast::Attribute]) { |
499 | let def_id = self.tcx.hir.local_def_id(node_id); | |
500 | for attr in attrs { | |
83c7162d XL |
501 | let mut clauses = None; |
502 | ||
0531ce1d | 503 | if attr.check_name("rustc_dump_program_clauses") { |
83c7162d XL |
504 | clauses = Some(self.tcx.program_clauses_for(def_id)); |
505 | } | |
506 | ||
507 | if attr.check_name("rustc_dump_env_program_clauses") { | |
508 | let param_env = self.tcx.param_env(def_id); | |
509 | clauses = Some(self.tcx.program_clauses_for_env(param_env)); | |
510 | } | |
511 | ||
512 | if let Some(clauses) = clauses { | |
8faf50e0 XL |
513 | let mut err = self |
514 | .tcx | |
83c7162d XL |
515 | .sess |
516 | .struct_span_err(attr.span, "program clause dump"); | |
517 | ||
518 | let mut strings: Vec<_> = clauses | |
519 | .iter() | |
520 | .map(|clause| { | |
521 | // Skip the top-level binder for a less verbose output | |
522 | let program_clause = match clause { | |
523 | Clause::Implies(program_clause) => program_clause, | |
524 | Clause::ForAll(program_clause) => program_clause.skip_binder(), | |
525 | }; | |
8faf50e0 | 526 | program_clause.to_string() |
83c7162d XL |
527 | }) |
528 | .collect(); | |
529 | ||
530 | strings.sort(); | |
531 | ||
532 | for string in strings { | |
533 | err.note(&string); | |
0531ce1d | 534 | } |
83c7162d XL |
535 | |
536 | err.emit(); | |
0531ce1d XL |
537 | } |
538 | } | |
539 | } | |
540 | } | |
541 | ||
542 | impl<'a, 'tcx> Visitor<'tcx> for ClauseDumper<'a, 'tcx> { | |
543 | fn nested_visit_map<'this>(&'this mut self) -> NestedVisitorMap<'this, 'tcx> { | |
544 | NestedVisitorMap::OnlyBodies(&self.tcx.hir) | |
545 | } | |
546 | ||
547 | fn visit_item(&mut self, item: &'tcx hir::Item) { | |
548 | self.process_attrs(item.id, &item.attrs); | |
549 | intravisit::walk_item(self, item); | |
550 | } | |
551 | ||
552 | fn visit_trait_item(&mut self, trait_item: &'tcx hir::TraitItem) { | |
553 | self.process_attrs(trait_item.id, &trait_item.attrs); | |
554 | intravisit::walk_trait_item(self, trait_item); | |
555 | } | |
556 | ||
557 | fn visit_impl_item(&mut self, impl_item: &'tcx hir::ImplItem) { | |
558 | self.process_attrs(impl_item.id, &impl_item.attrs); | |
559 | intravisit::walk_impl_item(self, impl_item); | |
560 | } | |
561 | ||
562 | fn visit_struct_field(&mut self, s: &'tcx hir::StructField) { | |
563 | self.process_attrs(s.id, &s.attrs); | |
564 | intravisit::walk_struct_field(self, s); | |
565 | } | |
566 | } |