@@ -114,15 +114,16 @@ impl<'tcx> Lower<PolyDomainGoal<'tcx>> for ty::Predicate<'tcx> {
114
114
}
115
115
}
116
116
117
- /// Used for lowered where clauses (see rustc guide).
117
+ /// Used for implied bounds related rules (see rustc guide).
118
118
trait IntoFromEnvGoal {
119
- // Transforms an existing goal into a FromEnv goal.
119
+ /// Transforms an existing goal into a ` FromEnv` goal.
120
120
fn into_from_env_goal ( self ) -> Self ;
121
121
}
122
122
123
+ /// Used for well-formedness related rules (see rustc guide).
123
124
trait IntoWellFormedGoal {
124
- // Transforms an existing goal into a WellFormed goal.
125
- fn into_wellformed_goal ( self ) -> Self ;
125
+ /// Transforms an existing goal into a ` WellFormed` goal.
126
+ fn into_well_formed_goal ( self ) -> Self ;
126
127
}
127
128
128
129
impl < ' tcx > IntoFromEnvGoal for DomainGoal < ' tcx > {
@@ -139,7 +140,7 @@ impl<'tcx> IntoFromEnvGoal for DomainGoal<'tcx> {
139
140
}
140
141
141
142
impl < ' tcx > IntoWellFormedGoal for DomainGoal < ' tcx > {
142
- fn into_wellformed_goal ( self ) -> DomainGoal < ' tcx > {
143
+ fn into_well_formed_goal ( self ) -> DomainGoal < ' tcx > {
143
144
use self :: WhereClause :: * ;
144
145
145
146
match self {
@@ -284,34 +285,35 @@ fn program_clauses_for_trait<'a, 'tcx>(
284
285
285
286
// Rule WellFormed-TraitRef
286
287
//
287
- // For each where clause WC:
288
+ // Here `WC` denotes the set of all where clauses:
289
+ // ```
288
290
// forall<Self, P1..Pn> {
289
291
// WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)
290
292
// }
293
+ // ```
291
294
292
- //Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)
293
- let mut extend_where_clauses = vec ! [ ty:: Binder :: dummy( trait_pred. lower( ) ) ] ;
294
- extend_where_clauses. extend (
295
- where_clauses
296
- . into_iter ( )
297
- . map ( |wc| wc. lower ( ) . map_bound ( |wc| wc. into_wellformed_goal ( ) ) ) ,
298
- ) ;
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
+ ) ;
299
303
300
- // WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)
301
- let clause = ProgramClause {
304
+ // ` WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)`
305
+ let wf_clause = ProgramClause {
302
306
goal : DomainGoal :: WellFormed ( WellFormed :: Trait ( trait_pred) ) ,
303
307
hypotheses : tcx. mk_goals (
304
- extend_where_clauses
305
- . into_iter ( )
306
- . map ( |wc| Goal :: from_poly_domain_goal ( wc, tcx) ) ,
308
+ wf_conditions. map ( |wc| Goal :: from_poly_domain_goal ( wc, tcx) ) ,
307
309
) ,
308
310
} ;
309
- let wellformed_clauses = iter:: once ( Clause :: ForAll ( ty:: Binder :: dummy ( clause ) ) ) ;
311
+ let wf_clause = iter:: once ( Clause :: ForAll ( ty:: Binder :: dummy ( wf_clause ) ) ) ;
310
312
311
313
tcx. mk_clauses (
312
314
clauses
313
315
. chain ( implied_bound_clauses)
314
- . chain ( wellformed_clauses ) ,
316
+ . chain ( wf_clause )
315
317
)
316
318
}
317
319
0 commit comments