Add chalk rules related to associated type defs

* Rule ProjectionEq-Skolemize
* Rule WellFormed-AssocTy
* Rule Implied-Trait-From-AssocTy
This commit is contained in:
scalexm 2018-10-08 12:54:56 +02:00
parent 663002f222
commit 96ff827395
3 changed files with 106 additions and 19 deletions

View File

@ -362,7 +362,7 @@ fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId
.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
),
};
tcx.intern_clauses(&[Clause::ForAll(ty::Binder::dummy(clause))])
tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::dummy(clause))))
}
pub fn program_clauses_for_type_def<'a, 'tcx>(
@ -430,10 +430,86 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
}
pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
_tcx: TyCtxt<'a, 'tcx, 'tcx>,
_item_id: DefId,
tcx: TyCtxt<'a, 'tcx, 'tcx>,
item_id: DefId,
) -> Clauses<'tcx> {
unimplemented!()
// Rule ProjectionEq-Skolemize
//
// ```
// trait Trait<P1..Pn> {
// type AssocType<Pn+1..Pm>;
// }
// ```
//
// `ProjectionEq` can succeed by skolemizing, see "associated type"
// chapter for more:
// ```
// forall<Self, P1..Pn, Pn+1..Pm> {
// ProjectionEq(
// <Self as Trait<P1..Pn>>::AssocType<Pn+1..Pm> =
// (Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>
// )
// }
// ```
let item = tcx.associated_item(item_id);
debug_assert_eq!(item.kind, ty::AssociatedKind::Type);
let trait_id = match item.container {
ty::AssociatedItemContainer::TraitContainer(trait_id) => trait_id,
_ => bug!("not an trait container"),
};
let trait_ref = ty::TraitRef::identity(tcx, trait_id);
let projection_ty = ty::ProjectionTy::from_ref_and_name(tcx, trait_ref, item.ident);
let placeholder_ty = tcx.mk_ty(ty::UnnormalizedProjection(projection_ty));
let projection_eq = WhereClause::ProjectionEq(ty::ProjectionPredicate {
projection_ty,
ty: placeholder_ty,
});
let projection_eq_clause = ProgramClause {
goal: DomainGoal::Holds(projection_eq),
hypotheses: &ty::List::empty(),
};
// Rule WellFormed-AssocTy
// ```
// forall<Self, P1..Pn, Pn+1..Pm> {
// WellFormed((Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>)
// :- Implemented(Self: Trait<P1..Pn>)
// }
// ```
let trait_predicate = ty::TraitPredicate { trait_ref };
let hypothesis = tcx.mk_goal(
DomainGoal::Holds(WhereClause::Implemented(trait_predicate)).into_goal()
);
let wf_clause = ProgramClause {
goal: DomainGoal::WellFormed(WellFormed::Ty(placeholder_ty)),
hypotheses: tcx.mk_goals(iter::once(hypothesis)),
};
// Rule Implied-Trait-From-AssocTy
// ```
// forall<Self, P1..Pn, Pn+1..Pm> {
// FromEnv(Self: Trait<P1..Pn>)
// :- FromEnv((Trait::AssocType)<Self, P1..Pn, Pn+1..Pm>)
// }
// ```
let hypothesis = tcx.mk_goal(
DomainGoal::FromEnv(FromEnv::Ty(placeholder_ty)).into_goal()
);
let from_env_clause = ProgramClause {
goal: DomainGoal::FromEnv(FromEnv::Trait(trait_predicate)),
hypotheses: tcx.mk_goals(iter::once(hypothesis)),
};
let clauses = iter::once(projection_eq_clause)
.chain(iter::once(wf_clause))
.chain(iter::once(from_env_clause));
let clauses = clauses.map(|clause| Clause::ForAll(ty::Binder::dummy(clause)));
tcx.mk_clauses(clauses)
}
pub fn program_clauses_for_associated_type_value<'a, 'tcx>(
@ -442,10 +518,11 @@ pub fn program_clauses_for_associated_type_value<'a, 'tcx>(
) -> Clauses<'tcx> {
// Rule Normalize-From-Impl (see rustc guide)
//
// ```impl<P0..Pn> Trait<A1..An> for A0
// {
// ```
// impl<P0..Pn> Trait<A1..An> for A0 {
// type AssocType<Pn+1..Pm> = T;
// }```
// }
// ```
//
// FIXME: For the moment, we don't account for where clauses written on the associated
// ty definition (i.e. in the trait def, as in `type AssocType<T> where T: Sized`).
@ -492,7 +569,7 @@ pub fn program_clauses_for_associated_type_value<'a, 'tcx>(
.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
),
};
tcx.intern_clauses(&[Clause::ForAll(ty::Binder::dummy(clause))])
tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::dummy(clause))))
}
pub fn dump_program_clauses<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>) {

View File

@ -10,11 +10,12 @@
#![feature(rustc_attrs)]
trait Bar { }
#[rustc_dump_program_clauses] //~ ERROR program clause dump
trait Foo<S, T, U> {
fn s(_: S) -> S;
fn t(_: T) -> T;
fn u(_: U) -> U;
trait Foo<S, T: ?Sized> {
#[rustc_dump_program_clauses] //~ ERROR program clause dump
type Assoc: Bar + ?Sized;
}
fn main() {

View File

@ -1,14 +1,23 @@
error: program clause dump
--> $DIR/lower_trait.rs:13:1
--> $DIR/lower_trait.rs:15:1
|
LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= note: FromEnv(S: std::marker::Sized) :- FromEnv(Self: Foo<S, T, U>).
= note: FromEnv(T: std::marker::Sized) :- FromEnv(Self: Foo<S, T, U>).
= note: FromEnv(U: std::marker::Sized) :- FromEnv(Self: Foo<S, T, U>).
= note: Implemented(Self: Foo<S, T, U>) :- FromEnv(Self: Foo<S, T, U>).
= note: WellFormed(Self: Foo<S, T, U>) :- Implemented(Self: Foo<S, T, U>), WellFormed(S: std::marker::Sized), WellFormed(T: std::marker::Sized), WellFormed(U: std::marker::Sized).
= note: FromEnv(<Self as Foo<S, T>>::Assoc: Bar) :- FromEnv(Self: Foo<S, T>).
= note: FromEnv(S: std::marker::Sized) :- FromEnv(Self: Foo<S, T>).
= note: Implemented(Self: Foo<S, T>) :- FromEnv(Self: Foo<S, T>).
= note: WellFormed(Self: Foo<S, T>) :- Implemented(Self: Foo<S, T>), WellFormed(S: std::marker::Sized), WellFormed(<Self as Foo<S, T>>::Assoc: Bar).
error: aborting due to previous error
error: program clause dump
--> $DIR/lower_trait.rs:17:5
|
LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= note: FromEnv(Self: Foo<S, T>) :- FromEnv(Unnormalized(<Self as Foo<S, T>>::Assoc)).
= note: ProjectionEq(<Self as Foo<S, T>>::Assoc == Unnormalized(<Self as Foo<S, T>>::Assoc)).
= note: WellFormed(Unnormalized(<Self as Foo<S, T>>::Assoc)) :- Implemented(Self: Foo<S, T>).
error: aborting due to 2 previous errors