Implement Chalk lowering rule Normalize-From-Impl

This commit is contained in:
Fabian Zaiser 2018-04-03 17:53:13 +02:00
parent 7360d6dd67
commit 5a73fd5e1f
6 changed files with 81 additions and 5 deletions

View File

@ -1388,6 +1388,7 @@ impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::DomainGoal<'tcx>
FromEnv(where_clause) => where_clause.hash_stable(hcx, hasher),
WellFormedTy(ty) => ty.hash_stable(hcx, hasher),
Normalize(projection) => projection.hash_stable(hcx, hasher),
FromEnvTy(ty) => ty.hash_stable(hcx, hasher),
RegionOutlives(predicate) => predicate.hash_stable(hcx, hasher),
TypeOutlives(predicate) => predicate.hash_stable(hcx, hasher),

View File

@ -266,6 +266,7 @@ pub enum DomainGoal<'tcx> {
WellFormed(WhereClauseAtom<'tcx>),
FromEnv(WhereClauseAtom<'tcx>),
WellFormedTy(Ty<'tcx>),
Normalize(ty::ProjectionPredicate<'tcx>),
FromEnvTy(Ty<'tcx>),
RegionOutlives(ty::RegionOutlivesPredicate<'tcx>),
TypeOutlives(ty::TypeOutlivesPredicate<'tcx>),

View File

@ -450,6 +450,7 @@ impl<'tcx> fmt::Display for traits::DomainGoal<'tcx> {
FromEnv(Implemented(trait_ref)) => write!(fmt, "FromEnv({})", trait_ref),
FromEnv(ProjectionEq(projection)) => write!(fmt, "FromEnv({})", projection),
WellFormedTy(ty) => write!(fmt, "WellFormed({})", ty),
Normalize(projection) => write!(fmt, "Normalize({})", projection),
FromEnvTy(ty) => write!(fmt, "FromEnv({})", ty),
RegionOutlives(predicate) => write!(fmt, "RegionOutlives({})", predicate),
TypeOutlives(predicate) => write!(fmt, "TypeOutlives({})", predicate),
@ -538,6 +539,7 @@ EnumTypeFoldableImpl! {
(traits::DomainGoal::WellFormed)(wc),
(traits::DomainGoal::FromEnv)(wc),
(traits::DomainGoal::WellFormedTy)(ty),
(traits::DomainGoal::Normalize)(projection),
(traits::DomainGoal::FromEnvTy)(ty),
(traits::DomainGoal::RegionOutlives)(predicate),
(traits::DomainGoal::TypeOutlives)(predicate),

View File

@ -118,10 +118,20 @@ crate fn program_clauses_for<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefI
-> Lrc<&'tcx Slice<Clause<'tcx>>>
{
let node_id = tcx.hir.as_local_node_id(def_id).unwrap();
let item = tcx.hir.expect_item(node_id);
match item.node {
hir::ItemTrait(..) => program_clauses_for_trait(tcx, def_id),
hir::ItemImpl(..) => program_clauses_for_impl(tcx, def_id),
let node = tcx.hir.find(node_id).unwrap();
match node {
hir::map::Node::NodeItem(item) => match item.node {
hir::ItemTrait(..) => program_clauses_for_trait(tcx, def_id),
hir::ItemImpl(..) => program_clauses_for_impl(tcx, def_id),
_ => Lrc::new(vec![]),
}
hir::map::Node::NodeImplItem(item) => {
if let hir::ImplItemKind::Type(..) = item.node {
program_clauses_for_associated_type(tcx, def_id)
} else {
Lrc::new(vec![])
}
},
// FIXME: other constructions e.g. traits, associated types...
_ => Lrc::new(tcx.mk_clauses(iter::empty::<Clause>())),
@ -233,6 +243,53 @@ fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId
Lrc::new(tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::dummy(clause)))))
}
pub fn program_clauses_for_associated_type<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, item_id: DefId)
-> Lrc<Vec<Clause<'tcx>>> {
// Rule Normalize-From-Impl (see rustc guide)
//
// ```impl<P0..Pn> Trait<A1..An> for A0
// where WC
// {
// type AssocType<Pn+1..Pm> where WC1 = T;
// }```
//
// ```
// forall<P0..Pm> {
// forall<Pn+1..Pm> {
// Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T) :-
// WC && WC1
// }
// }
// ```
let item = tcx.associated_item(item_id);
debug_assert_eq!(item.kind, ty::AssociatedKind::Type);
let impl_id = if let ty::AssociatedItemContainer::ImplContainer(impl_id) = item.container {
impl_id
} else {
bug!()
};
// `A0 as Trait<A1..An>`
let trait_ref = tcx.impl_trait_ref(impl_id).unwrap();
// `T`
let ty = tcx.type_of(item_id);
// `WC`
let impl_where_clauses = tcx.predicates_of(impl_id).predicates.lower();
// `WC1`
let item_where_clauses = tcx.predicates_of(item_id).predicates.lower();
// `WC && WC1`
let mut where_clauses = vec![];
where_clauses.extend(impl_where_clauses);
where_clauses.extend(item_where_clauses);
// `<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm>`
let projection_ty = ty::ProjectionTy::from_ref_and_name(tcx, trait_ref, item.name);
// `Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T)`
let normalize_goal = DomainGoal::Normalize(ty::ProjectionPredicate { projection_ty, ty });
// `Normalize(... -> T) :- WC && WC1`
let clause = Clause::Implies(where_clauses, normalize_goal);
Lrc::new(vec![clause])
}
pub fn dump_program_clauses<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>) {
if !tcx.features().rustc_attrs {
return;

View File

@ -15,6 +15,15 @@ trait Foo { }
#[rustc_dump_program_clauses] //~ ERROR Implemented(T: Foo) :-
impl<T: 'static> Foo for T where T: Iterator<Item = i32> { }
trait Bar {
type Assoc;
}
impl<T> Bar for T where T: Iterator<Item = i32> {
#[rustc_dump_program_clauses] //~ ERROR Normalize(<T as Bar>::Assoc == std::vec::Vec<T>) :-
type Assoc = Vec<T>;
}
fn main() {
println!("hello");
}

View File

@ -4,5 +4,11 @@ error: Implemented(T: Foo) :- ProjectionEq(<T as std::iter::Iterator>::Item == i
LL | #[rustc_dump_program_clauses] //~ ERROR Implemented(T: Foo) :-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
error: aborting due to previous error
error: Normalize(<T as Bar>::Assoc == std::vec::Vec<T>) :- ProjectionEq(<T as std::iter::Iterator>::Item == i32), Implemented(T: std::iter::Iterator), Implemented(T: std::marker::Sized).
--> $DIR/lower_impl.rs:23:5
|
LL | #[rustc_dump_program_clauses] //~ ERROR Normalize(<T as Bar>::Assoc == std::vec::Vec<T>) :-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
error: aborting due to 2 previous errors