@@ -12,8 +12,10 @@ use rustc::hir::def_id::DefId;
1212use rustc:: hir:: intravisit:: { self , NestedVisitorMap , Visitor } ;
1313use rustc:: hir:: map:: definitions:: DefPathData ;
1414use rustc:: hir:: { self , ImplPolarity } ;
15- use rustc:: traits:: { Clause , Clauses , DomainGoal , Goal , PolyDomainGoal , ProgramClause ,
16- WhereClause , FromEnv , WellFormed } ;
15+ use rustc:: traits:: {
16+ Clause , Clauses , DomainGoal , FromEnv , Goal , PolyDomainGoal , ProgramClause , WellFormed ,
17+ WhereClause ,
18+ } ;
1719use rustc:: ty:: query:: Providers ;
1820use rustc:: ty:: { self , Slice , TyCtxt } ;
1921use rustc_data_structures:: fx:: FxHashSet ;
@@ -101,34 +103,50 @@ impl<'tcx> Lower<PolyDomainGoal<'tcx>> for ty::Predicate<'tcx> {
101103 Predicate :: RegionOutlives ( predicate) => predicate. lower ( ) ,
102104 Predicate :: TypeOutlives ( predicate) => predicate. lower ( ) ,
103105 Predicate :: Projection ( predicate) => predicate. lower ( ) ,
104- Predicate :: WellFormed ( ty) => ty:: Binder :: dummy (
105- DomainGoal :: WellFormed ( WellFormed :: Ty ( * ty) )
106- ) ,
107- Predicate :: ObjectSafe ( ..) |
108- Predicate :: ClosureKind ( ..) |
109- Predicate :: Subtype ( ..) |
110- Predicate :: ConstEvaluatable ( ..) => {
111- unimplemented ! ( )
106+ Predicate :: WellFormed ( ty) => {
107+ ty:: Binder :: dummy ( DomainGoal :: WellFormed ( WellFormed :: Ty ( * ty) ) )
112108 }
109+ Predicate :: ObjectSafe ( ..)
110+ | Predicate :: ClosureKind ( ..)
111+ | Predicate :: Subtype ( ..)
112+ | Predicate :: ConstEvaluatable ( ..) => unimplemented ! ( ) ,
113113 }
114114 }
115115}
116116
117- /// Transforms an existing goal into a FromEnv goal.
118- ///
119- /// Used for lowered where clauses (see rustc guide).
117+ /// Used for implied bounds related rules (see rustc guide).
120118trait IntoFromEnvGoal {
119+ /// Transforms an existing goal into a `FromEnv` goal.
121120 fn into_from_env_goal ( self ) -> Self ;
122121}
123122
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+
124129impl < ' tcx > IntoFromEnvGoal for DomainGoal < ' tcx > {
125130 fn into_from_env_goal ( self ) -> DomainGoal < ' tcx > {
126131 use self :: WhereClause :: * ;
127132
128133 match self {
129- DomainGoal :: Holds ( Implemented ( trait_ref) ) => DomainGoal :: FromEnv (
130- FromEnv :: Trait ( trait_ref)
131- ) ,
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+
146+ match self {
147+ DomainGoal :: Holds ( Implemented ( trait_ref) ) => {
148+ DomainGoal :: WellFormed ( WellFormed :: Trait ( trait_ref) )
149+ }
132150 other => other,
133151 }
134152 }
@@ -230,7 +248,7 @@ fn program_clauses_for_trait<'a, 'tcx>(
230248 // `Implemented(Self: Trait<P1..Pn>)`
231249 let impl_trait: DomainGoal = trait_pred. lower ( ) ;
232250
233- // `FromEnv(Self: Trait<P1..Pn>)`
251+ // `FromEnv(Self: Trait<P1..Pn>)`
234252 let from_env_goal = impl_trait. into_from_env_goal ( ) . into_goal ( ) ;
235253 let hypotheses = tcx. intern_goals ( & [ from_env_goal] ) ;
236254
@@ -242,6 +260,8 @@ fn program_clauses_for_trait<'a, 'tcx>(
242260
243261 let clauses = iter:: once ( Clause :: ForAll ( ty:: Binder :: dummy ( implemented_from_env) ) ) ;
244262
263+ let where_clauses = & tcx. predicates_defined_on ( def_id) . predicates ;
264+
245265 // Rule Implied-Bound-From-Trait
246266 //
247267 // For each where clause WC:
@@ -252,7 +272,6 @@ fn program_clauses_for_trait<'a, 'tcx>(
252272 // ```
253273
254274 // `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`, for each where clause WC
255- let where_clauses = & tcx. predicates_defined_on ( def_id) . predicates ;
256275 let implied_bound_clauses = where_clauses
257276 . into_iter ( )
258277 . map ( |wc| wc. lower ( ) )
@@ -262,10 +281,40 @@ fn program_clauses_for_trait<'a, 'tcx>(
262281 goal : goal. into_from_env_goal ( ) ,
263282 hypotheses,
264283 } ) )
265-
266284 . map ( Clause :: ForAll ) ;
267285
268- tcx. mk_clauses ( clauses. chain ( implied_bound_clauses) )
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+ ) ;
303+
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+ )
269318}
270319
271320fn program_clauses_for_impl < ' a , ' tcx > ( tcx : TyCtxt < ' a , ' tcx , ' tcx > , def_id : DefId ) -> Clauses < ' tcx > {
@@ -307,7 +356,6 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
307356 tcx : TyCtxt < ' a , ' tcx , ' tcx > ,
308357 def_id : DefId ,
309358) -> Clauses < ' tcx > {
310-
311359 // Rule WellFormed-Type
312360 //
313361 // `struct Ty<P1..Pn> where WC1, ..., WCm`
@@ -328,7 +376,10 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
328376 let well_formed = ProgramClause {
329377 goal : DomainGoal :: WellFormed ( WellFormed :: Ty ( ty) ) ,
330378 hypotheses : tcx. mk_goals (
331- where_clauses. iter ( ) . cloned ( ) . map ( |wc| Goal :: from_poly_domain_goal ( wc, tcx) )
379+ where_clauses
380+ . iter ( )
381+ . cloned ( )
382+ . map ( |wc| Goal :: from_poly_domain_goal ( wc, tcx) ) ,
332383 ) ,
333384 } ;
334385
@@ -459,7 +510,8 @@ impl<'a, 'tcx> ClauseDumper<'a, 'tcx> {
459510 }
460511
461512 if let Some ( clauses) = clauses {
462- let mut err = self . tcx
513+ let mut err = self
514+ . tcx
463515 . sess
464516 . struct_span_err ( attr. span , "program clause dump" ) ;
465517
0 commit comments