3 use rustc::hir::def_id::DefId;
4 use rustc::hir::intravisit::{self, NestedVisitorMap, Visitor};
5 use rustc::hir::map::definitions::DefPathData;
6 use rustc::hir::{self, ImplPolarity};
15 ProgramClauseCategory,
19 use rustc::ty::query::Providers;
20 use rustc::ty::{self, List, TyCtxt};
21 use rustc::ty::subst::{Subst, InternalSubsts};
26 crate fn provide(p: &mut Providers<'_>) {
29 program_clauses_for_env: environment::program_clauses_for_env,
30 environment: environment::environment,
35 crate trait Lower<T> {
36 /// Lower a rustc construct (e.g., `ty::TraitPredicate`) to a chalk-like type.
40 impl<T, U> Lower<Vec<U>> for Vec<T>
44 fn lower(&self) -> Vec<U> {
45 self.iter().map(|item| item.lower()).collect()
49 impl<'tcx> Lower<WhereClause<'tcx>> for ty::TraitPredicate<'tcx> {
50 fn lower(&self) -> WhereClause<'tcx> {
51 WhereClause::Implemented(*self)
55 impl<'tcx> Lower<WhereClause<'tcx>> for ty::ProjectionPredicate<'tcx> {
56 fn lower(&self) -> WhereClause<'tcx> {
57 WhereClause::ProjectionEq(*self)
61 impl<'tcx> Lower<WhereClause<'tcx>> for ty::RegionOutlivesPredicate<'tcx> {
62 fn lower(&self) -> WhereClause<'tcx> {
63 WhereClause::RegionOutlives(*self)
67 impl<'tcx> Lower<WhereClause<'tcx>> for ty::TypeOutlivesPredicate<'tcx> {
68 fn lower(&self) -> WhereClause<'tcx> {
69 WhereClause::TypeOutlives(*self)
73 impl<'tcx, T> Lower<DomainGoal<'tcx>> for T
75 T: Lower<WhereClause<'tcx>>,
77 fn lower(&self) -> DomainGoal<'tcx> {
78 DomainGoal::Holds(self.lower())
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
85 /// example), we model them with quantified domain goals, e.g., as for the previous example:
86 /// `forall<'a> { T: Fn(&'a i32) }` which corresponds to something like
87 /// `Binder<Holds(Implemented(TraitPredicate))>`.
88 impl<'tcx, T> Lower<PolyDomainGoal<'tcx>> for ty::Binder<T>
90 T: Lower<DomainGoal<'tcx>> + ty::fold::TypeFoldable<'tcx>,
92 fn lower(&self) -> PolyDomainGoal<'tcx> {
93 self.map_bound_ref(|p| p.lower())
97 impl<'tcx> Lower<PolyDomainGoal<'tcx>> for ty::Predicate<'tcx> {
98 fn lower(&self) -> PolyDomainGoal<'tcx> {
99 use rustc::ty::Predicate;
102 Predicate::Trait(predicate) => predicate.lower(),
103 Predicate::RegionOutlives(predicate) => predicate.lower(),
104 Predicate::TypeOutlives(predicate) => predicate.lower(),
105 Predicate::Projection(predicate) => predicate.lower(),
107 Predicate::WellFormed(..) |
108 Predicate::ObjectSafe(..) |
109 Predicate::ClosureKind(..) |
110 Predicate::Subtype(..) |
111 Predicate::ConstEvaluatable(..) => {
112 bug!("unexpected predicate {}", self)
118 /// Used for implied bounds related rules (see rustc guide).
119 trait IntoFromEnvGoal {
120 /// Transforms an existing goal into a `FromEnv` goal.
121 fn into_from_env_goal(self) -> Self;
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;
130 impl<'tcx> IntoFromEnvGoal for DomainGoal<'tcx> {
131 fn into_from_env_goal(self) -> DomainGoal<'tcx> {
132 use self::WhereClause::*;
135 DomainGoal::Holds(Implemented(trait_ref)) => {
136 DomainGoal::FromEnv(FromEnv::Trait(trait_ref))
143 impl<'tcx> IntoWellFormedGoal for DomainGoal<'tcx> {
144 fn into_well_formed_goal(self) -> DomainGoal<'tcx> {
145 use self::WhereClause::*;
148 DomainGoal::Holds(Implemented(trait_ref)) => {
149 DomainGoal::WellFormed(WellFormed::Trait(trait_ref))
156 crate fn program_clauses_for<'a, 'tcx>(
157 tcx: TyCtxt<'a, 'tcx, 'tcx>,
160 match tcx.def_key(def_id).disambiguated_data.data {
161 DefPathData::Trait(_) |
162 DefPathData::TraitAlias(_) => program_clauses_for_trait(tcx, def_id),
163 DefPathData::Impl => program_clauses_for_impl(tcx, def_id),
164 DefPathData::AssocTypeInImpl(..) => program_clauses_for_associated_type_value(tcx, def_id),
165 DefPathData::AssocTypeInTrait(..) => program_clauses_for_associated_type_def(tcx, def_id),
166 DefPathData::TypeNs(..) => program_clauses_for_type_def(tcx, def_id),
171 fn program_clauses_for_trait<'a, 'tcx>(
172 tcx: TyCtxt<'a, 'tcx, 'tcx>,
175 // `trait Trait<P1..Pn> where WC { .. } // P0 == Self`
177 // Rule Implemented-From-Env (see rustc guide)
180 // forall<Self, P1..Pn> {
181 // Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)
185 let bound_vars = InternalSubsts::bound_vars_for_item(tcx, def_id);
187 // `Self: Trait<P1..Pn>`
188 let trait_pred = ty::TraitPredicate {
189 trait_ref: ty::TraitRef {
195 // `Implemented(Self: Trait<P1..Pn>)`
196 let impl_trait: DomainGoal<'_> = trait_pred.lower();
198 // `FromEnv(Self: Trait<P1..Pn>)`
199 let from_env_goal = tcx.mk_goal(impl_trait.into_from_env_goal().into_goal());
200 let hypotheses = tcx.intern_goals(&[from_env_goal]);
202 // `Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)`
203 let implemented_from_env = ProgramClause {
206 category: ProgramClauseCategory::ImpliedBound,
209 let implemented_from_env = Clause::ForAll(ty::Binder::bind(implemented_from_env));
211 let predicates = &tcx.predicates_defined_on(def_id).predicates;
212 let where_clauses = &predicates
214 .map(|(wc, _)| wc.lower())
215 .collect::<Vec<_>>();
217 // Rule Implied-Bound-From-Trait
219 // For each where clause WC:
221 // forall<Self, P1..Pn> {
222 // FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn)
226 // `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`, for each where clause WC
227 let implied_bound_clauses = where_clauses
231 // `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`
233 // we move binders to the left
234 wc.map_bound(|goal| ProgramClause {
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`
240 // index (no def-id).
241 goal: goal.subst(tcx, bound_vars).into_from_env_goal(),
244 category: ProgramClauseCategory::ImpliedBound,
247 .map(Clause::ForAll);
249 // Rule WellFormed-TraitRef
251 // Here `WC` denotes the set of all where clauses:
253 // forall<Self, P1..Pn> {
254 // WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)
259 let wf_conditions = where_clauses
261 .map(|wc| wc.map_bound(|goal| goal.into_well_formed_goal()));
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(
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)))
271 category: ProgramClauseCategory::WellFormed,
273 let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
276 iter::once(implemented_from_env)
277 .chain(implied_bound_clauses)
278 .chain(iter::once(wf_clause))
282 fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId) -> Clauses<'tcx> {
283 if let ImplPolarity::Negative = tcx.impl_polarity(def_id) {
284 return List::empty();
287 // Rule Implemented-From-Impl (see rustc guide)
289 // `impl<P0..Pn> Trait<A1..An> for A0 where WC { .. }`
293 // Implemented(A0: Trait<A1..An>) :- WC
297 let bound_vars = InternalSubsts::bound_vars_for_item(tcx, def_id);
299 let trait_ref = tcx.impl_trait_ref(def_id)
300 .expect("not an impl")
301 .subst(tcx, bound_vars);
303 // `Implemented(A0: Trait<A1..An>)`
304 let trait_pred = ty::TraitPredicate { trait_ref }.lower();
307 let predicates = &tcx.predicates_of(def_id).predicates;
308 let where_clauses = predicates
310 .map(|(wc, _)| wc.lower())
311 .map(|wc| wc.subst(tcx, bound_vars));
313 // `Implemented(A0: Trait<A1..An>) :- WC`
314 let clause = ProgramClause {
316 hypotheses: tcx.mk_goals(
318 .map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
320 category: ProgramClauseCategory::Other,
322 tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::bind(clause))))
325 pub fn program_clauses_for_type_def<'a, 'tcx>(
326 tcx: TyCtxt<'a, 'tcx, 'tcx>,
329 // Rule WellFormed-Type
331 // `struct Ty<P1..Pn> where WC1, ..., WCm`
335 // WellFormed(Ty<...>) :- WC1, ..., WCm`
339 let bound_vars = InternalSubsts::bound_vars_for_item(tcx, def_id);
342 let ty = tcx.type_of(def_id).subst(tcx, bound_vars);
345 let where_clauses = tcx.predicates_of(def_id).predicates
347 .map(|(wc, _)| wc.lower())
348 .collect::<Vec<_>>();
350 // `WellFormed(Ty<...>) :- WC1, ..., WCm`
351 let well_formed_clause = ProgramClause {
352 goal: DomainGoal::WellFormed(WellFormed::Ty(ty)),
353 hypotheses: tcx.mk_goals(
356 .map(|wc| wc.subst(tcx, bound_vars))
357 .map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
359 category: ProgramClauseCategory::WellFormed,
361 let well_formed_clause = Clause::ForAll(ty::Binder::bind(well_formed_clause));
363 // Rule Implied-Bound-From-Type
365 // For each where clause `WC`:
368 // FromEnv(WC) :- FromEnv(Ty<...>)
372 // `FromEnv(Ty<...>)`
373 let from_env_goal = tcx.mk_goal(DomainGoal::FromEnv(FromEnv::Ty(ty)).into_goal());
374 let hypotheses = tcx.intern_goals(&[from_env_goal]);
376 // For each where clause `WC`:
377 let from_env_clauses = where_clauses
380 // `FromEnv(WC) :- FromEnv(Ty<...>)`
382 // move the binders to the left
383 wc.map_bound(|goal| ProgramClause {
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(),
390 category: ProgramClauseCategory::ImpliedBound,
394 .map(Clause::ForAll);
396 tcx.mk_clauses(iter::once(well_formed_clause).chain(from_env_clauses))
399 pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
400 tcx: TyCtxt<'a, 'tcx, 'tcx>,
403 // Rule ProjectionEq-Placeholder
406 // trait Trait<P1..Pn> {
407 // type AssocType<Pn+1..Pm>;
411 // `ProjectionEq` can succeed by skolemizing, see "associated type"
414 // forall<Self, P1..Pn, Pn+1..Pm> {
416 // <Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> =
417 // (Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>
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"),
429 let trait_bound_vars = InternalSubsts::bound_vars_for_item(tcx, trait_id);
430 let trait_ref = ty::TraitRef {
432 substs: trait_bound_vars,
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 {
442 let projection_eq_clause = ProgramClause {
443 goal: DomainGoal::Holds(projection_eq),
444 hypotheses: ty::List::empty(),
445 category: ProgramClauseCategory::Other,
447 let projection_eq_clause = Clause::ForAll(ty::Binder::bind(projection_eq_clause));
449 // Rule WellFormed-AssocTy
451 // forall<Self, P1..Pn, Pn+1..Pm> {
452 // WellFormed((Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>)
453 // :- Implemented(Self: Trait<P1..Pn>)
457 let trait_predicate = ty::TraitPredicate { trait_ref };
458 let hypothesis = tcx.mk_goal(
459 DomainGoal::Holds(WhereClause::Implemented(trait_predicate)).into_goal()
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,
467 let wf_clause = Clause::ForAll(ty::Binder::bind(wf_clause));
469 // Rule Implied-Trait-From-AssocTy
471 // forall<Self, P1..Pn, Pn+1..Pm> {
472 // FromEnv(Self: Trait<P1..Pn>)
473 // :- FromEnv((Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>)
477 let hypothesis = tcx.mk_goal(
478 DomainGoal::FromEnv(FromEnv::Ty(placeholder_ty)).into_goal()
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,
486 let from_env_clause = Clause::ForAll(ty::Binder::bind(from_env_clause));
488 // Rule ProjectionEq-Normalize
490 // ProjectionEq can succeed by normalizing:
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)
498 let offset = tcx.generics_of(trait_id).params
503 // Add a new type param after the existing ones (`U` in the comment above).
504 let ty_var = ty::Bound(
506 ty::BoundVar::from_u32(offset + 1).into()
509 // `ProjectionEq(<Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> = U)`
510 let projection = ty::ProjectionPredicate {
512 ty: tcx.mk_ty(ty_var),
515 // `Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> U)`
516 let hypothesis = tcx.mk_goal(
517 DomainGoal::Normalize(projection).into_goal()
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,
527 let normalize_clause = Clause::ForAll(ty::Binder::bind(normalize_clause));
529 let clauses = iter::once(projection_eq_clause)
530 .chain(iter::once(wf_clause))
531 .chain(iter::once(from_env_clause))
532 .chain(iter::once(normalize_clause));
534 tcx.mk_clauses(clauses)
537 pub fn program_clauses_for_associated_type_value<'a, 'tcx>(
538 tcx: TyCtxt<'a, 'tcx, 'tcx>,
541 // Rule Normalize-From-Impl (see rustc guide)
544 // impl<P0..Pn> Trait<A1..An> for A0 {
545 // type AssocType<Pn+1..Pm> = T;
549 // FIXME: For the moment, we don't account for where clauses written on the associated
550 // ty definition (i.e., in the trait def, as in `type AssocType<T> where T: Sized`).
553 // forall<Pn+1..Pm> {
554 // Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T) :-
555 // Implemented(A0: Trait<A1..An>)
560 let item = tcx.associated_item(item_id);
561 debug_assert_eq!(item.kind, ty::AssociatedKind::Type);
562 let impl_id = match item.container {
563 ty::AssociatedItemContainer::ImplContainer(impl_id) => impl_id,
564 _ => bug!("not an impl container"),
567 let impl_bound_vars = InternalSubsts::bound_vars_for_item(tcx, impl_id);
569 // `A0 as Trait<A1..An>`
570 let trait_ref = tcx.impl_trait_ref(impl_id)
572 .subst(tcx, impl_bound_vars);
575 let ty = tcx.type_of(item_id);
577 // `Implemented(A0: Trait<A1..An>)`
578 let trait_implemented: DomainGoal<'_> = ty::TraitPredicate { trait_ref }.lower();
580 // `<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm>`
581 let projection_ty = ty::ProjectionTy::from_ref_and_name(tcx, trait_ref, item.ident);
583 // `Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T)`
584 let normalize_goal = DomainGoal::Normalize(ty::ProjectionPredicate { projection_ty, ty });
586 // `Normalize(... -> T) :- ...`
587 let normalize_clause = ProgramClause {
588 goal: normalize_goal,
589 hypotheses: tcx.mk_goals(
590 iter::once(tcx.mk_goal(GoalKind::DomainGoal(trait_implemented)))
592 category: ProgramClauseCategory::Other,
594 let normalize_clause = Clause::ForAll(ty::Binder::bind(normalize_clause));
596 tcx.mk_clauses(iter::once(normalize_clause))
599 pub fn dump_program_clauses<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>) {
600 if !tcx.features().rustc_attrs {
604 let mut visitor = ClauseDumper { tcx };
607 .visit_all_item_likes(&mut visitor.as_deep_visitor());
610 struct ClauseDumper<'a, 'tcx: 'a> {
611 tcx: TyCtxt<'a, 'tcx, 'tcx>,
614 impl<'a, 'tcx> ClauseDumper<'a, 'tcx> {
615 fn process_attrs(&mut self, hir_id: hir::HirId, attrs: &[ast::Attribute]) {
616 let def_id = self.tcx.hir().local_def_id_from_hir_id(hir_id);
618 let mut clauses = None;
620 if attr.check_name("rustc_dump_program_clauses") {
621 clauses = Some(self.tcx.program_clauses_for(def_id));
624 if attr.check_name("rustc_dump_env_program_clauses") {
625 let environment = self.tcx.environment(def_id);
626 clauses = Some(self.tcx.program_clauses_for_env(environment));
629 if let Some(clauses) = clauses {
633 .struct_span_err(attr.span, "program clause dump");
635 let mut strings: Vec<_> = clauses
637 .map(|clause| clause.to_string())
642 for string in strings {
652 impl<'a, 'tcx> Visitor<'tcx> for ClauseDumper<'a, 'tcx> {
653 fn nested_visit_map<'this>(&'this mut self) -> NestedVisitorMap<'this, 'tcx> {
654 NestedVisitorMap::OnlyBodies(&self.tcx.hir())
657 fn visit_item(&mut self, item: &'tcx hir::Item) {
658 self.process_attrs(item.hir_id, &item.attrs);
659 intravisit::walk_item(self, item);
662 fn visit_trait_item(&mut self, trait_item: &'tcx hir::TraitItem) {
663 self.process_attrs(trait_item.hir_id, &trait_item.attrs);
664 intravisit::walk_trait_item(self, trait_item);
667 fn visit_impl_item(&mut self, impl_item: &'tcx hir::ImplItem) {
668 self.process_attrs(impl_item.hir_id, &impl_item.attrs);
669 intravisit::walk_impl_item(self, impl_item);
672 fn visit_struct_field(&mut self, s: &'tcx hir::StructField) {
673 self.process_attrs(s.hir_id, &s.attrs);
674 intravisit::walk_struct_field(self, s);