OpenE2K/rust
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Refactor the chalkify lowering process

Browse Source
This commit is contained in:
scalexm 2018-06-04 13:57:56 +02:00
parent 6eafab06cf
commit 0347b32a26
5 changed files with 237 additions and 141 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

45
src/librustc/ich/impls_ty.rs
View File

@ -1382,16 +1382,46 @@ impl_stable_hash_for!(enum infer::canonical::Certainty {
Proven, Ambiguous
});
impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::WhereClauseAtom<'tcx> {
impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::WhereClause<'tcx> {
fn hash_stable<W: StableHasherResult>(&self,
hcx: &mut StableHashingContext<'a>,
hasher: &mut StableHasher<W>) {
use traits::WhereClauseAtom::*;
use traits::WhereClause::*;
mem::discriminant(self).hash_stable(hcx, hasher);
match self {
Implemented(trait_ref) => trait_ref.hash_stable(hcx, hasher),
ProjectionEq(projection) => projection.hash_stable(hcx, hasher),
TypeOutlives(ty_outlives) => ty_outlives.hash_stable(hcx, hasher),
RegionOutlives(region_outlives) => region_outlives.hash_stable(hcx, hasher),
}
}
}
impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::WellFormed<'tcx> {
fn hash_stable<W: StableHasherResult>(&self,
hcx: &mut StableHashingContext<'a>,
hasher: &mut StableHasher<W>) {
use traits::WellFormed::*;
mem::discriminant(self).hash_stable(hcx, hasher);
match self {
Trait(trait_ref) => trait_ref.hash_stable(hcx, hasher),
Ty(ty) => ty.hash_stable(hcx, hasher),
}
}
}
impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::FromEnv<'tcx> {
fn hash_stable<W: StableHasherResult>(&self,
hcx: &mut StableHashingContext<'a>,
hasher: &mut StableHasher<W>) {
use traits::FromEnv::*;
mem::discriminant(self).hash_stable(hcx, hasher);
match self {
Trait(trait_ref) => trait_ref.hash_stable(hcx, hasher),
Ty(ty) => ty.hash_stable(hcx, hasher),
}
}
}
@ -1404,15 +1434,10 @@ impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::DomainGoal<'tcx>
mem::discriminant(self).hash_stable(hcx, hasher);
match self {
Holds(where_clause) |
WellFormed(where_clause) |
FromEnv(where_clause) => where_clause.hash_stable(hcx, hasher),
WellFormedTy(ty) => ty.hash_stable(hcx, hasher),
Holds(wc) => wc.hash_stable(hcx, hasher),
WellFormed(wf) => wf.hash_stable(hcx, hasher),
FromEnv(from_env) => from_env.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),
}
}
}

46
src/librustc/traits/mod.rs
View File

@ -269,7 +269,9 @@ pub type PredicateObligations<'tcx> = Vec<PredicateObligation<'tcx>>;
pub type TraitObligations<'tcx> = Vec<TraitObligation<'tcx>>;
/// The following types:
/// * `WhereClauseAtom`
/// * `WhereClause`
/// * `WellFormed`
/// * `FromEnv`
/// * `DomainGoal`
/// * `Goal`
/// * `Clause`
@ -277,21 +279,31 @@ pub type TraitObligations<'tcx> = Vec<TraitObligation<'tcx>>;
/// logic programming clauses. They are part of the interface
/// for the chalk SLG solver.
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub enum WhereClauseAtom<'tcx> {
pub enum WhereClause<'tcx> {
Implemented(ty::TraitPredicate<'tcx>),
ProjectionEq(ty::ProjectionPredicate<'tcx>),
RegionOutlives(ty::RegionOutlivesPredicate<'tcx>),
TypeOutlives(ty::TypeOutlivesPredicate<'tcx>),
}
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub enum WellFormed<'tcx> {
Trait(ty::TraitPredicate<'tcx>),
Ty(Ty<'tcx>),
}
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub enum FromEnv<'tcx> {
Trait(ty::TraitPredicate<'tcx>),
Ty(Ty<'tcx>),
}
#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub enum DomainGoal<'tcx> {
Holds(WhereClauseAtom<'tcx>),
WellFormed(WhereClauseAtom<'tcx>),
FromEnv(WhereClauseAtom<'tcx>),
WellFormedTy(Ty<'tcx>),
Holds(WhereClause<'tcx>),
WellFormed(WellFormed<'tcx>),
FromEnv(FromEnv<'tcx>),
Normalize(ty::ProjectionPredicate<'tcx>),
FromEnvTy(Ty<'tcx>),
RegionOutlives(ty::RegionOutlivesPredicate<'tcx>),
TypeOutlives(ty::TypeOutlivesPredicate<'tcx>),
}
pub type PolyDomainGoal<'tcx> = ty::Binder<DomainGoal<'tcx>>;
@ -314,27 +326,27 @@ pub enum Goal<'tcx> {
pub type Goals<'tcx> = &'tcx Slice<Goal<'tcx>>;
impl<'tcx> DomainGoal<'tcx> {
pub fn into_goal(self) -> Goal<'tcx> {
Goal::DomainGoal(self)
}
}
impl<'tcx> Goal<'tcx> {
pub fn from_poly_domain_goal<'a>(
domain_goal: PolyDomainGoal<'tcx>,
tcx: TyCtxt<'a, 'tcx, 'tcx>,
) -> Goal<'tcx> {
match domain_goal.no_late_bound_regions() {
Some(p) => p.into(),
Some(p) => p.into_goal(),
None => Goal::Quantified(
QuantifierKind::Universal,
domain_goal.map_bound(|p| tcx.mk_goal(Goal::from(p)))
domain_goal.map_bound(|p| tcx.mk_goal(p.into_goal()))
),
}
}
}
impl<'tcx> From<DomainGoal<'tcx>> for Goal<'tcx> {
fn from(domain_goal: DomainGoal<'tcx>) -> Self {
Goal::DomainGoal(domain_goal)
}
}
/// This matches the definition from Page 7 of "A Proof Procedure for the Logic of Hereditary
/// Harrop Formulas".
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]

103
src/librustc/traits/structural_impls.rs
View File

@ -405,13 +405,37 @@ BraceStructTypeFoldableImpl! {
} where T: TypeFoldable<'tcx>
}
impl<'tcx> fmt::Display for traits::WhereClauseAtom<'tcx> {
impl<'tcx> fmt::Display for traits::WhereClause<'tcx> {
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
use traits::WhereClauseAtom::*;
use traits::WhereClause::*;
match self {
Implemented(trait_ref) => write!(fmt, "Implemented({})", trait_ref),
ProjectionEq(projection) => write!(fmt, "ProjectionEq({})", projection),
RegionOutlives(predicate) => write!(fmt, "RegionOutlives({})", predicate),
TypeOutlives(predicate) => write!(fmt, "TypeOutlives({})", predicate),
}
}
}
impl<'tcx> fmt::Display for traits::WellFormed<'tcx> {
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
use traits::WellFormed::*;
match self {
Trait(trait_ref) => write!(fmt, "WellFormed({})", trait_ref),
Ty(ty) => write!(fmt, "WellFormed({})", ty),
}
}
}
impl<'tcx> fmt::Display for traits::FromEnv<'tcx> {
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
use traits::FromEnv::*;
match self {
Trait(trait_ref) => write!(fmt, "FromEnv({})", trait_ref),
Ty(ty) => write!(fmt, "FromEnv({})", ty),
}
}
}
@ -419,19 +443,12 @@ impl<'tcx> fmt::Display for traits::WhereClauseAtom<'tcx> {
impl<'tcx> fmt::Display for traits::DomainGoal<'tcx> {
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
use traits::DomainGoal::*;
use traits::WhereClauseAtom::*;
match self {
Holds(wc) => write!(fmt, "{}", wc),
WellFormed(Implemented(trait_ref)) => write!(fmt, "WellFormed({})", trait_ref),
WellFormed(ProjectionEq(projection)) => write!(fmt, "WellFormed({})", projection),
FromEnv(Implemented(trait_ref)) => write!(fmt, "FromEnv({})", trait_ref),
FromEnv(ProjectionEq(projection)) => write!(fmt, "FromEnv({})", projection),
WellFormedTy(ty) => write!(fmt, "WellFormed({})", ty),
WellFormed(wf) => write!(fmt, "{}", wf),
FromEnv(from_env) => write!(fmt, "{}", from_env),
Normalize(projection) => write!(fmt, "Normalize({})", projection),
FromEnvTy(ty) => write!(fmt, "FromEnv({})", ty),
RegionOutlives(predicate) => write!(fmt, "RegionOutlives({})", predicate),
TypeOutlives(predicate) => write!(fmt, "TypeOutlives({})", predicate),
}
}
}
@ -506,30 +523,60 @@ impl<'tcx> fmt::Display for traits::Clause<'tcx> {
}
EnumTypeFoldableImpl! {
impl<'tcx> TypeFoldable<'tcx> for traits::WhereClauseAtom<'tcx> {
(traits::WhereClauseAtom::Implemented)(trait_ref),
(traits::WhereClauseAtom::ProjectionEq)(projection),
impl<'tcx> TypeFoldable<'tcx> for traits::WhereClause<'tcx> {
(traits::WhereClause::Implemented)(trait_ref),
(traits::WhereClause::ProjectionEq)(projection),
(traits::WhereClause::TypeOutlives)(ty_outlives),
(traits::WhereClause::RegionOutlives)(region_outlives),
}
}
EnumLiftImpl! {
impl<'a, 'tcx> Lift<'tcx> for traits::WhereClauseAtom<'a> {
type Lifted = traits::WhereClauseAtom<'tcx>;
(traits::WhereClauseAtom::Implemented)(trait_ref),
(traits::WhereClauseAtom::ProjectionEq)(projection),
impl<'a, 'tcx> Lift<'tcx> for traits::WhereClause<'a> {
type Lifted = traits::WhereClause<'tcx>;
(traits::WhereClause::Implemented)(trait_ref),
(traits::WhereClause::ProjectionEq)(projection),
(traits::WhereClause::TypeOutlives)(ty_outlives),
(traits::WhereClause::RegionOutlives)(region_outlives),
}
}
EnumTypeFoldableImpl! {
impl<'tcx> TypeFoldable<'tcx> for traits::WellFormed<'tcx> {
(traits::WellFormed::Trait)(trait_ref),
(traits::WellFormed::Ty)(ty),
}
}
EnumLiftImpl! {
impl<'a, 'tcx> Lift<'tcx> for traits::WellFormed<'a> {
type Lifted = traits::WellFormed<'tcx>;
(traits::WellFormed::Trait)(trait_ref),
(traits::WellFormed::Ty)(ty),
}
}
EnumTypeFoldableImpl! {
impl<'tcx> TypeFoldable<'tcx> for traits::FromEnv<'tcx> {
(traits::FromEnv::Trait)(trait_ref),
(traits::FromEnv::Ty)(ty),
}
}
EnumLiftImpl! {
impl<'a, 'tcx> Lift<'tcx> for traits::FromEnv<'a> {
type Lifted = traits::FromEnv<'tcx>;
(traits::FromEnv::Trait)(trait_ref),
(traits::FromEnv::Ty)(ty),
}
}
EnumTypeFoldableImpl! {
impl<'tcx> TypeFoldable<'tcx> for traits::DomainGoal<'tcx> {
(traits::DomainGoal::Holds)(wc),
(traits::DomainGoal::WellFormed)(wc),
(traits::DomainGoal::FromEnv)(wc),
(traits::DomainGoal::WellFormedTy)(ty),
(traits::DomainGoal::WellFormed)(wf),
(traits::DomainGoal::FromEnv)(from_env),
(traits::DomainGoal::Normalize)(projection),
(traits::DomainGoal::FromEnvTy)(ty),
(traits::DomainGoal::RegionOutlives)(predicate),
(traits::DomainGoal::TypeOutlives)(predicate),
}
}
@ -537,13 +584,9 @@ EnumLiftImpl! {
impl<'a, 'tcx> Lift<'tcx> for traits::DomainGoal<'a> {
type Lifted = traits::DomainGoal<'tcx>;
(traits::DomainGoal::Holds)(wc),
(traits::DomainGoal::WellFormed)(wc),
(traits::DomainGoal::FromEnv)(wc),
(traits::DomainGoal::WellFormedTy)(ty),
(traits::DomainGoal::WellFormed)(wf),
(traits::DomainGoal::FromEnv)(from_env),
(traits::DomainGoal::Normalize)(projection),
(traits::DomainGoal::FromEnvTy)(ty),
(traits::DomainGoal::RegionOutlives)(predicate),
(traits::DomainGoal::TypeOutlives)(predicate),
}
}

44
src/librustc_traits/chalk_context.rs
View File

@ -14,7 +14,16 @@ use rustc::infer::canonical::{
Canonical, CanonicalVarValues, Canonicalize, QueryRegionConstraint, QueryResult,
};
use rustc::infer::{InferCtxt, InferOk, LateBoundRegionConversionTime};
use rustc::traits::{DomainGoal, ExClauseFold, ExClauseLift, Goal, ProgramClause, QuantifierKind};
use rustc::traits::{
WellFormed,
FromEnv,
DomainGoal,
ExClauseFold,
ExClauseLift,
Goal,
ProgramClause,
QuantifierKind
};
use rustc::ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
use rustc::ty::subst::Kind;
use rustc::ty::{self, TyCtxt};
@ -314,11 +323,10 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
_environment: &ty::ParamEnv<'tcx>,
goal: &DomainGoal<'tcx>,
) -> Vec<ProgramClause<'tcx>> {
use rustc::traits::DomainGoal::*;
use rustc::traits::WhereClauseAtom::*;
use rustc::traits::WhereClause::*;
match goal {
Holds(Implemented(_trait_predicate)) => {
DomainGoal::Holds(Implemented(_trait_predicate)) => {
// These come from:
//
// - Trait definitions (implied bounds)
@ -326,31 +334,31 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
panic!()
}
Holds(ProjectionEq(_projection_predicate)) => {
DomainGoal::Holds(ProjectionEq(_projection_predicate)) => {
// These come from:
panic!()
}
WellFormed(Implemented(_trait_predicate)) => {
DomainGoal::Holds(RegionOutlives(_region_outlives)) => {
panic!()
}
DomainGoal::Holds(TypeOutlives(_type_outlives)) => {
panic!()
}
DomainGoal::WellFormed(WellFormed::Trait(_trait_predicate)) => {
// These come from -- the trait decl.
panic!()
}
WellFormed(ProjectionEq(_projection_predicate)) => panic!(),
DomainGoal::WellFormed(WellFormed::Ty(_ty)) => panic!(),
FromEnv(Implemented(_trait_predicate)) => panic!(),
DomainGoal::FromEnv(FromEnv::Trait(_trait_predicate)) => panic!(),
FromEnv(ProjectionEq(_projection_predicate)) => panic!(),
DomainGoal::FromEnv(FromEnv::Ty(_ty)) => panic!(),
WellFormedTy(_ty) => panic!(),
FromEnvTy(_ty) => panic!(),
RegionOutlives(_region_outlives) => panic!(),
TypeOutlives(_type_outlives) => panic!(),
Normalize(_) => panic!(),
DomainGoal::Normalize(_) => panic!(),
}
}

140
src/librustc_traits/lowering.rs
View File

@ -13,7 +13,7 @@ use rustc::hir::intravisit::{self, NestedVisitorMap, Visitor};
use rustc::hir::map::definitions::DefPathData;
use rustc::hir::{self, ImplPolarity};
use rustc::traits::{Clause, Clauses, DomainGoal, Goal, PolyDomainGoal, ProgramClause,
WhereClauseAtom};
WhereClause, FromEnv, WellFormed};
use rustc::ty::subst::Substs;
use rustc::ty::{self, Slice, TyCtxt};
use rustc_data_structures::fx::FxHashSet;
@ -23,7 +23,7 @@ use syntax::ast;
use std::iter;
crate trait Lower<T> {
/// Lower a rustc construction (e.g. `ty::TraitPredicate`) to a chalk-like type.
/// Lower a rustc construct (e.g. `ty::TraitPredicate`) to a chalk-like type.
fn lower(&self) -> T;
}
@ -36,39 +36,39 @@ where
}
}
impl<'tcx> Lower<WhereClauseAtom<'tcx>> for ty::TraitPredicate<'tcx> {
fn lower(&self) -> WhereClauseAtom<'tcx> {
WhereClauseAtom::Implemented(*self)
impl<'tcx> Lower<WhereClause<'tcx>> for ty::TraitPredicate<'tcx> {
fn lower(&self) -> WhereClause<'tcx> {
WhereClause::Implemented(*self)
}
}
impl<'tcx> Lower<WhereClauseAtom<'tcx>> for ty::ProjectionPredicate<'tcx> {
fn lower(&self) -> WhereClauseAtom<'tcx> {
WhereClauseAtom::ProjectionEq(*self)
impl<'tcx> Lower<WhereClause<'tcx>> for ty::ProjectionPredicate<'tcx> {
fn lower(&self) -> WhereClause<'tcx> {
WhereClause::ProjectionEq(*self)
}
}
impl<'tcx> Lower<WhereClause<'tcx>> for ty::RegionOutlivesPredicate<'tcx> {
fn lower(&self) -> WhereClause<'tcx> {
WhereClause::RegionOutlives(*self)
}
}
impl<'tcx> Lower<WhereClause<'tcx>> for ty::TypeOutlivesPredicate<'tcx> {
fn lower(&self) -> WhereClause<'tcx> {
WhereClause::TypeOutlives(*self)
}
}
impl<'tcx, T> Lower<DomainGoal<'tcx>> for T
where
T: Lower<WhereClauseAtom<'tcx>>,
T: Lower<WhereClause<'tcx>>,
{
fn lower(&self) -> DomainGoal<'tcx> {
DomainGoal::Holds(self.lower())
}
}
impl<'tcx> Lower<DomainGoal<'tcx>> for ty::RegionOutlivesPredicate<'tcx> {
fn lower(&self) -> DomainGoal<'tcx> {
DomainGoal::RegionOutlives(*self)
}
}
impl<'tcx> Lower<DomainGoal<'tcx>> for ty::TypeOutlivesPredicate<'tcx> {
fn lower(&self) -> DomainGoal<'tcx> {
DomainGoal::TypeOutlives(*self)
}
}
/// `ty::Binder` is used for wrapping a rustc construction possibly containing generic
/// lifetimes, e.g. `for<'a> T: Fn(&'a i32)`. Instead of representing higher-ranked things
/// in that leaf-form (i.e. `Holds(Implemented(Binder<TraitPredicate>))` in the previous
@ -86,15 +86,20 @@ where
impl<'tcx> Lower<PolyDomainGoal<'tcx>> for ty::Predicate<'tcx> {
fn lower(&self) -> PolyDomainGoal<'tcx> {
use rustc::ty::Predicate::*;
use rustc::ty::Predicate;
match self {
Trait(predicate) => predicate.lower(),
RegionOutlives(predicate) => predicate.lower(),
TypeOutlives(predicate) => predicate.lower(),
Projection(predicate) => predicate.lower(),
WellFormed(ty) => ty::Binder::dummy(DomainGoal::WellFormedTy(*ty)),
ObjectSafe(..) | ClosureKind(..) | Subtype(..) | ConstEvaluatable(..) => {
Predicate::Trait(predicate) => predicate.lower(),
Predicate::RegionOutlives(predicate) => predicate.lower(),
Predicate::TypeOutlives(predicate) => predicate.lower(),
Predicate::Projection(predicate) => predicate.lower(),
Predicate::WellFormed(ty) => ty::Binder::dummy(
DomainGoal::WellFormed(WellFormed::Ty(*ty))
),
Predicate::ObjectSafe(..) |
Predicate::ClosureKind(..) |
Predicate::Subtype(..) |
Predicate::ConstEvaluatable(..) => {
unimplemented!()
}
}
@ -110,11 +115,13 @@ trait IntoFromEnvGoal {
impl<'tcx> IntoFromEnvGoal for DomainGoal<'tcx> {
fn into_from_env_goal(self) -> DomainGoal<'tcx> {
use self::DomainGoal::*;
use self::WhereClause::*;
match self {
Holds(wc_atom) => FromEnv(wc_atom),
WellFormed(..) | FromEnv(..) | WellFormedTy(..) | FromEnvTy(..) | Normalize(..)
| RegionOutlives(..) | TypeOutlives(..) => self,
DomainGoal::Holds(Implemented(trait_ref)) => DomainGoal::FromEnv(
FromEnv::Trait(trait_ref)
),
other => other,
}
}
}
@ -212,16 +219,20 @@ fn program_clauses_for_trait<'a, 'tcx>(
substs: Substs::identity_for_item(tcx, def_id),
},
};
// `FromEnv(Self: Trait<P1..Pn>)`
let from_env = Goal::from(DomainGoal::FromEnv(trait_pred.lower()));
// `Implemented(Self: Trait<P1..Pn>)`
let impl_trait = DomainGoal::Holds(WhereClauseAtom::Implemented(trait_pred));
let impl_trait: DomainGoal = trait_pred.lower();
// `FromEnv(Self: Trait<P1..Pn>)`
let from_env = impl_trait.into_from_env_goal().into_goal();
// `Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)`
let hypotheses = tcx.intern_goals(&[from_env]);
let implemented_from_env = ProgramClause {
goal: impl_trait,
hypotheses: tcx.intern_goals(&[from_env]),
hypotheses,
};
let clauses = iter::once(Clause::ForAll(ty::Binder::dummy(implemented_from_env)));
// Rule Implied-Bound-From-Trait
@ -239,27 +250,19 @@ fn program_clauses_for_trait<'a, 'tcx>(
let where_clauses = &tcx.predicates_of(def_id).predicates;
let implied_bound_clauses = where_clauses[1..]
.into_iter()
.map(|wc| implied_bound_from_trait(tcx, trait_pred, wc));
.map(|wc| wc.lower())
// `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`
.map(|wc| wc.map_bound(|goal| ProgramClause {
goal: goal.into_from_env_goal(),
hypotheses,
}))
.map(Clause::ForAll);
tcx.mk_clauses(clauses.chain(implied_bound_clauses))
}
/// For a given `where_clause`, returns a clause `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`.
fn implied_bound_from_trait<'a, 'tcx>(
tcx: TyCtxt<'a, 'tcx, 'tcx>,
trait_pred: ty::TraitPredicate<'tcx>,
where_clause: &ty::Predicate<'tcx>,
) -> Clause<'tcx> {
// `FromEnv(Self: Trait<P1..Pn>)`
let impl_trait = DomainGoal::FromEnv(WhereClauseAtom::Implemented(trait_pred));
// `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`
Clause::ForAll(where_clause.lower().map_bound(|goal| ProgramClause {
goal: goal.into_from_env_goal(),
hypotheses: tcx.intern_goals(&[Goal::from(impl_trait)]),
}))
}
fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId) -> Clauses<'tcx> {
if let ImplPolarity::Negative = tcx.impl_polarity(def_id) {
return Slice::empty();
@ -275,9 +278,11 @@ fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId
// }
// ```
let trait_ref = tcx.impl_trait_ref(def_id).unwrap();
let trait_ref = tcx.impl_trait_ref(def_id).expect("not an impl");
// `Implemented(A0: Trait<A1..An>)`
let trait_pred = ty::TraitPredicate { trait_ref }.lower();
// `WC`
let where_clauses = tcx.predicates_of(def_id).predicates.lower();
@ -301,45 +306,48 @@ pub fn program_clauses_for_associated_type_value<'a, 'tcx>(
//
// ```impl<P0..Pn> Trait<A1..An> for A0
// {
// type AssocType<Pn+1..Pm> where WC = T;
// type AssocType<Pn+1..Pm> = T;
// }```
//
// ```
// forall<P0..Pm> {
// forall<Pn+1..Pm> {
// Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T) :-
// Implemented(A0: Trait<A1..An>) && WC
// Implemented(A0: Trait<A1..An>)
// }
// }
// ```
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!()
let impl_id = match item.container {
ty::AssociatedItemContainer::ImplContainer(impl_id) => impl_id,
_ => bug!("not an impl container"),
};
// `A0 as Trait<A1..An>`
let trait_ref = tcx.impl_trait_ref(impl_id).unwrap();
// `T`
let ty = tcx.type_of(item_id);
// `Implemented(A0: Trait<A1..An>)`
let trait_implemented = ty::Binder::dummy(ty::TraitPredicate { trait_ref }.lower());
// `WC`
let item_where_clauses = tcx.predicates_of(item_id).predicates.lower();
// `Implemented(A0: Trait<A1..An>) && WC`
let mut where_clauses = vec![trait_implemented];
where_clauses.extend(item_where_clauses);
// `Implemented(A0: Trait<A1..An>)`
let hypotheses = vec![trait_implemented];
// `<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) :- ...`
let clause = ProgramClause {
goal: normalize_goal,
hypotheses: tcx.mk_goals(
where_clauses
hypotheses
.into_iter()
.map(|wc| Goal::from_poly_domain_goal(wc, tcx)),
),