@@ -108,6 +108,7 @@ impl<'tcx> IntoFromEnvGoal for DomainGoal<'tcx> {
108108 FromEnv ( ..) |
109109 WellFormedTy ( ..) |
110110 FromEnvTy ( ..) |
111+ Normalize ( ..) |
111112 RegionOutlives ( ..) |
112113 TypeOutlives ( ..) => self ,
113114 }
@@ -118,10 +119,20 @@ crate fn program_clauses_for<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefI
118119 -> Lrc < & ' tcx Slice < Clause < ' tcx > > >
119120{
120121 let node_id = tcx. hir . as_local_node_id ( def_id) . unwrap ( ) ;
121- let item = tcx. hir . expect_item ( node_id) ;
122- match item. node {
123- hir:: ItemTrait ( ..) => program_clauses_for_trait ( tcx, def_id) ,
124- hir:: ItemImpl ( ..) => program_clauses_for_impl ( tcx, def_id) ,
122+ let node = tcx. hir . find ( node_id) . unwrap ( ) ;
123+ match node {
124+ hir:: map:: Node :: NodeItem ( item) => match item. node {
125+ hir:: ItemTrait ( ..) => program_clauses_for_trait ( tcx, def_id) ,
126+ hir:: ItemImpl ( ..) => program_clauses_for_impl ( tcx, def_id) ,
127+ _ => Lrc :: new ( tcx. mk_clauses ( iter:: empty :: < Clause > ( ) ) ) ,
128+ }
129+ hir:: map:: Node :: NodeImplItem ( item) => {
130+ if let hir:: ImplItemKind :: Type ( ..) = item. node {
131+ program_clauses_for_associated_type_value ( tcx, def_id)
132+ } else {
133+ Lrc :: new ( tcx. mk_clauses ( iter:: empty :: < Clause > ( ) ) )
134+ }
135+ } ,
125136
126137 // FIXME: other constructions e.g. traits, associated types...
127138 _ => Lrc :: new ( tcx. mk_clauses ( iter:: empty :: < Clause > ( ) ) ) ,
@@ -233,6 +244,58 @@ fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId
233244 Lrc :: new ( tcx. mk_clauses ( iter:: once ( Clause :: ForAll ( ty:: Binder :: dummy ( clause) ) ) ) )
234245}
235246
247+ pub fn program_clauses_for_associated_type_value < ' a , ' tcx > (
248+ tcx : TyCtxt < ' a , ' tcx , ' tcx > ,
249+ item_id : DefId ,
250+ ) -> Lrc < & ' tcx Slice < Clause < ' tcx > > > {
251+ // Rule Normalize-From-Impl (see rustc guide)
252+ //
253+ // ```impl<P0..Pn> Trait<A1..An> for A0
254+ // {
255+ // type AssocType<Pn+1..Pm> where WC = T;
256+ // }```
257+ //
258+ // ```
259+ // forall<P0..Pm> {
260+ // forall<Pn+1..Pm> {
261+ // Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T) :-
262+ // Implemented(A0: Trait<A1..An>) && WC
263+ // }
264+ // }
265+ // ```
266+
267+ let item = tcx. associated_item ( item_id) ;
268+ debug_assert_eq ! ( item. kind, ty:: AssociatedKind :: Type ) ;
269+ let impl_id = if let ty:: AssociatedItemContainer :: ImplContainer ( impl_id) = item. container {
270+ impl_id
271+ } else {
272+ bug ! ( )
273+ } ;
274+ // `A0 as Trait<A1..An>`
275+ let trait_ref = tcx. impl_trait_ref ( impl_id) . unwrap ( ) ;
276+ // `T`
277+ let ty = tcx. type_of ( item_id) ;
278+ // `Implemented(A0: Trait<A1..An>)`
279+ let trait_implemented = ty:: Binder :: dummy ( ty:: TraitPredicate { trait_ref } . lower ( ) ) ;
280+ // `WC`
281+ let item_where_clauses = tcx. predicates_of ( item_id) . predicates . lower ( ) ;
282+ // `Implemented(A0: Trait<A1..An>) && WC`
283+ let mut where_clauses = vec ! [ trait_implemented] ;
284+ where_clauses. extend ( item_where_clauses) ;
285+ // `<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm>`
286+ let projection_ty = ty:: ProjectionTy :: from_ref_and_name ( tcx, trait_ref, item. name ) ;
287+ // `Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T)`
288+ let normalize_goal = DomainGoal :: Normalize ( ty:: ProjectionPredicate { projection_ty, ty } ) ;
289+ // `Normalize(... -> T) :- ...`
290+ let clause = ProgramClause {
291+ goal : normalize_goal,
292+ hypotheses : tcx. mk_goals (
293+ where_clauses. into_iter ( ) . map ( |wc| Goal :: from_poly_domain_goal ( wc, tcx) )
294+ ) ,
295+ } ;
296+ Lrc :: new ( tcx. mk_clauses ( iter:: once ( Clause :: ForAll ( ty:: Binder :: dummy ( clause) ) ) ) )
297+ }
298+
236299pub fn dump_program_clauses < ' a , ' tcx > ( tcx : TyCtxt < ' a , ' tcx , ' tcx > ) {
237300 if !tcx. features ( ) . rustc_attrs {
238301 return ;
0 commit comments