diff --git a/src/librustc/ich/impls_ty.rs b/src/librustc/ich/impls_ty.rs index 04e57883c7753..ad255fb8417f2 100644 --- a/src/librustc/ich/impls_ty.rs +++ b/src/librustc/ich/impls_ty.rs @@ -1382,16 +1382,46 @@ impl_stable_hash_for!(enum infer::canonical::Certainty { Proven, Ambiguous }); -impl<'a, 'tcx> HashStable> for traits::WhereClauseAtom<'tcx> { +impl<'a, 'tcx> HashStable> for traits::WhereClause<'tcx> { fn hash_stable(&self, hcx: &mut StableHashingContext<'a>, hasher: &mut StableHasher) { - 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> for traits::WellFormed<'tcx> { + fn hash_stable(&self, + hcx: &mut StableHashingContext<'a>, + hasher: &mut StableHasher) { + 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> for traits::FromEnv<'tcx> { + fn hash_stable(&self, + hcx: &mut StableHashingContext<'a>, + hasher: &mut StableHasher) { + 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> 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), } } } diff --git a/src/librustc/traits/mod.rs b/src/librustc/traits/mod.rs index 3bd4e11b0e8b9..4e4c60b1c1181 100644 --- a/src/librustc/traits/mod.rs +++ b/src/librustc/traits/mod.rs @@ -269,7 +269,9 @@ pub type PredicateObligations<'tcx> = Vec>; pub type TraitObligations<'tcx> = Vec>; /// The following types: -/// * `WhereClauseAtom` +/// * `WhereClause` +/// * `WellFormed` +/// * `FromEnv` /// * `DomainGoal` /// * `Goal` /// * `Clause` @@ -277,21 +279,31 @@ pub type TraitObligations<'tcx> = Vec>; /// 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>; @@ -314,27 +326,27 @@ pub enum Goal<'tcx> { pub type Goals<'tcx> = &'tcx Slice>; +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> 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)] diff --git a/src/librustc/traits/structural_impls.rs b/src/librustc/traits/structural_impls.rs index d1304a0a3f887..d24c84b2556f8 100644 --- a/src/librustc/traits/structural_impls.rs +++ b/src/librustc/traits/structural_impls.rs @@ -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::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::WhereClauseAtom<'a> { - type Lifted = traits::WhereClauseAtom<'tcx>; - (traits::WhereClauseAtom::Implemented)(trait_ref), - (traits::WhereClauseAtom::ProjectionEq)(projection), + 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), } } diff --git a/src/librustc_traits/chalk_context.rs b/src/librustc_traits/chalk_context.rs index bf26409c3ef5f..a1242621cb18c 100644 --- a/src/librustc_traits/chalk_context.rs +++ b/src/librustc_traits/chalk_context.rs @@ -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<'tcx>> _environment: &ty::ParamEnv<'tcx>, goal: &DomainGoal<'tcx>, ) -> Vec> { - 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<'tcx>> panic!() } - Holds(ProjectionEq(_projection_predicate)) => { + DomainGoal::Holds(ProjectionEq(_projection_predicate)) => { // These come from: panic!() } - WellFormed(Implemented(_trait_predicate)) => { - // These come from -- the trait decl. + DomainGoal::Holds(RegionOutlives(_region_outlives)) => { panic!() } - WellFormed(ProjectionEq(_projection_predicate)) => panic!(), - - FromEnv(Implemented(_trait_predicate)) => panic!(), - - FromEnv(ProjectionEq(_projection_predicate)) => panic!(), + DomainGoal::Holds(TypeOutlives(_type_outlives)) => { + panic!() + } - WellFormedTy(_ty) => panic!(), + DomainGoal::WellFormed(WellFormed::Trait(_trait_predicate)) => { + // These come from -- the trait decl. + panic!() + } - FromEnvTy(_ty) => panic!(), + DomainGoal::WellFormed(WellFormed::Ty(_ty)) => panic!(), - RegionOutlives(_region_outlives) => panic!(), + DomainGoal::FromEnv(FromEnv::Trait(_trait_predicate)) => panic!(), - TypeOutlives(_type_outlives) => panic!(), + DomainGoal::FromEnv(FromEnv::Ty(_ty)) => panic!(), - Normalize(_) => panic!(), + DomainGoal::Normalize(_) => panic!(), } } diff --git a/src/librustc_traits/lowering.rs b/src/librustc_traits/lowering.rs index 32f18a62abe59..0270e970976ea 100644 --- a/src/librustc_traits/lowering.rs +++ b/src/librustc_traits/lowering.rs @@ -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 { - /// 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,36 +36,36 @@ where } } -impl<'tcx> Lower> for ty::TraitPredicate<'tcx> { - fn lower(&self) -> WhereClauseAtom<'tcx> { - WhereClauseAtom::Implemented(*self) +impl<'tcx> Lower> for ty::TraitPredicate<'tcx> { + fn lower(&self) -> WhereClause<'tcx> { + WhereClause::Implemented(*self) } } -impl<'tcx> Lower> for ty::ProjectionPredicate<'tcx> { - fn lower(&self) -> WhereClauseAtom<'tcx> { - WhereClauseAtom::ProjectionEq(*self) +impl<'tcx> Lower> for ty::ProjectionPredicate<'tcx> { + fn lower(&self) -> WhereClause<'tcx> { + WhereClause::ProjectionEq(*self) } } -impl<'tcx, T> Lower> for T -where - T: Lower>, -{ - fn lower(&self) -> DomainGoal<'tcx> { - DomainGoal::Holds(self.lower()) +impl<'tcx> Lower> for ty::RegionOutlivesPredicate<'tcx> { + fn lower(&self) -> WhereClause<'tcx> { + WhereClause::RegionOutlives(*self) } } -impl<'tcx> Lower> for ty::RegionOutlivesPredicate<'tcx> { - fn lower(&self) -> DomainGoal<'tcx> { - DomainGoal::RegionOutlives(*self) +impl<'tcx> Lower> for ty::TypeOutlivesPredicate<'tcx> { + fn lower(&self) -> WhereClause<'tcx> { + WhereClause::TypeOutlives(*self) } } -impl<'tcx> Lower> for ty::TypeOutlivesPredicate<'tcx> { +impl<'tcx, T> Lower> for T +where + T: Lower>, +{ fn lower(&self) -> DomainGoal<'tcx> { - DomainGoal::TypeOutlives(*self) + DomainGoal::Holds(self.lower()) } } @@ -86,15 +86,20 @@ where impl<'tcx> Lower> 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, } } } @@ -127,6 +134,8 @@ crate fn program_clauses_for<'a, 'tcx>( DefPathData::Trait(_) => program_clauses_for_trait(tcx, def_id), DefPathData::Impl => program_clauses_for_impl(tcx, def_id), DefPathData::AssocTypeInImpl(..) => program_clauses_for_associated_type_value(tcx, def_id), + DefPathData::AssocTypeInTrait(..) => program_clauses_for_associated_type_def(tcx, def_id), + DefPathData::TypeNs(..) => program_clauses_for_type_def(tcx, def_id), _ => Slice::empty(), } } @@ -212,16 +221,20 @@ fn program_clauses_for_trait<'a, 'tcx>( substs: Substs::identity_for_item(tcx, def_id), }, }; - // `FromEnv(Self: Trait)` - let from_env = Goal::from(DomainGoal::FromEnv(trait_pred.lower())); + // `Implemented(Self: Trait)` - let impl_trait = DomainGoal::Holds(WhereClauseAtom::Implemented(trait_pred)); + let impl_trait: DomainGoal = trait_pred.lower(); + + // `FromEnv(Self: Trait)` + let from_env_goal = impl_trait.into_from_env_goal().into_goal(); + let hypotheses = tcx.intern_goals(&[from_env_goal]); // `Implemented(Self: Trait) :- FromEnv(Self: Trait)` 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,25 +252,17 @@ 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()) - tcx.mk_clauses(clauses.chain(implied_bound_clauses)) -} + // `FromEnv(WC) :- FromEnv(Self: Trait)` + .map(|wc| wc.map_bound(|goal| ProgramClause { + goal: goal.into_from_env_goal(), + hypotheses, + })) -/// For a given `where_clause`, returns a clause `FromEnv(WC) :- FromEnv(Self: Trait)`. -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)` - let impl_trait = DomainGoal::FromEnv(WhereClauseAtom::Implemented(trait_pred)); - - // `FromEnv(WC) :- FromEnv(Self: Trait)` - Clause::ForAll(where_clause.lower().map_bound(|goal| ProgramClause { - goal: goal.into_from_env_goal(), - hypotheses: tcx.intern_goals(&[Goal::from(impl_trait)]), - })) + .map(Clause::ForAll); + + tcx.mk_clauses(clauses.chain(implied_bound_clauses)) } fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId) -> Clauses<'tcx> { @@ -275,9 +280,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)` let trait_pred = ty::TraitPredicate { trait_ref }.lower(); + // `WC` let where_clauses = tcx.predicates_of(def_id).predicates.lower(); @@ -293,6 +300,72 @@ fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId tcx.intern_clauses(&[Clause::ForAll(ty::Binder::dummy(clause))]) } +pub fn program_clauses_for_type_def<'a, 'tcx>( + tcx: TyCtxt<'a, 'tcx, 'tcx>, + def_id: DefId, +) -> Clauses<'tcx> { + + // Rule WellFormed-Type + // + // `struct Ty where WC1, ..., WCm` + // + // ``` + // forall { + // WellFormed(Ty<...>) :- WC1, ..., WCm` + // } + // ``` + + // `Ty<...>` + let ty = tcx.type_of(def_id); + + // `WC` + let where_clauses = tcx.predicates_of(def_id).predicates.lower(); + + // `WellFormed(Ty<...>) :- WC1, ..., WCm` + let well_formed = ProgramClause { + goal: DomainGoal::WellFormed(WellFormed::Ty(ty)), + hypotheses: tcx.mk_goals( + where_clauses.iter().cloned().map(|wc| Goal::from_poly_domain_goal(wc, tcx)) + ), + }; + + let well_formed_clause = iter::once(Clause::ForAll(ty::Binder::dummy(well_formed))); + + // Rule FromEnv-Type + // + // For each where clause `WC`: + // ``` + // forall { + // FromEnv(WC) :- FromEnv(Ty<...>) + // } + // ``` + + // `FromEnv(Ty<...>)` + let from_env_goal = DomainGoal::FromEnv(FromEnv::Ty(ty)).into_goal(); + let hypotheses = tcx.intern_goals(&[from_env_goal]); + + // For each where clause `WC`: + let from_env_clauses = where_clauses + .into_iter() + + // `FromEnv(WC) :- FromEnv(Ty<...>)` + .map(|wc| wc.map_bound(|goal| ProgramClause { + goal: goal.into_from_env_goal(), + hypotheses, + })) + + .map(Clause::ForAll); + + tcx.mk_clauses(well_formed_clause.chain(from_env_clauses)) +} + +pub fn program_clauses_for_associated_type_def<'a, 'tcx>( + _tcx: TyCtxt<'a, 'tcx, 'tcx>, + _item_id: DefId, +) -> Clauses<'tcx> { + unimplemented!() +} + pub fn program_clauses_for_associated_type_value<'a, 'tcx>( tcx: TyCtxt<'a, 'tcx, 'tcx>, item_id: DefId, @@ -301,45 +374,50 @@ pub fn program_clauses_for_associated_type_value<'a, 'tcx>( // // ```impl Trait for A0 // { - // type AssocType where WC = T; + // type AssocType = 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 where T: Sized`). // ``` // forall { // forall { // Normalize(>::AssocType -> T) :- - // Implemented(A0: Trait) && WC + // Implemented(A0: Trait) // } // } // ``` 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` let trait_ref = tcx.impl_trait_ref(impl_id).unwrap(); + // `T` let ty = tcx.type_of(item_id); + // `Implemented(A0: Trait)` 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) && WC` - let mut where_clauses = vec![trait_implemented]; - where_clauses.extend(item_where_clauses); + + // `Implemented(A0: Trait)` + let hypotheses = vec![trait_implemented]; + // `>::AssocType` let projection_ty = ty::ProjectionTy::from_ref_and_name(tcx, trait_ref, item.name); + // `Normalize(>::AssocType -> 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)), ), diff --git a/src/test/ui/chalkify/lower_struct.rs b/src/test/ui/chalkify/lower_struct.rs new file mode 100644 index 0000000000000..9287555a05684 --- /dev/null +++ b/src/test/ui/chalkify/lower_struct.rs @@ -0,0 +1,18 @@ +// Copyright 2018 The Rust Project Developers. See the COPYRIGHT +// file at the top-level directory of this distribution and at +// http://rust-lang.org/COPYRIGHT. +// +// Licensed under the Apache License, Version 2.0 or the MIT license +// , at your +// option. This file may not be copied, modified, or distributed +// except according to those terms. + +#![feature(rustc_attrs)] + +#[rustc_dump_program_clauses] //~ ERROR program clause dump +struct Foo where Box: Clone { + _x: std::marker::PhantomData, +} + +fn main() { } diff --git a/src/test/ui/chalkify/lower_struct.stderr b/src/test/ui/chalkify/lower_struct.stderr new file mode 100644 index 0000000000000..d6cc9c8e9a401 --- /dev/null +++ b/src/test/ui/chalkify/lower_struct.stderr @@ -0,0 +1,12 @@ +error: program clause dump + --> $DIR/lower_struct.rs:13:1 + | +LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | + = note: FromEnv(T: std::marker::Sized) :- FromEnv(Foo). + = note: FromEnv(std::boxed::Box: std::clone::Clone) :- FromEnv(Foo). + = note: WellFormed(Foo) :- Implemented(T: std::marker::Sized), Implemented(std::boxed::Box: std::clone::Clone). + +error: aborting due to previous error + diff --git a/src/test/ui/chalkify/lower_trait_higher_rank.stderr b/src/test/ui/chalkify/lower_trait_higher_rank.stderr index 7f6f503c6ff72..ea275d647fa7c 100644 --- a/src/test/ui/chalkify/lower_trait_higher_rank.stderr +++ b/src/test/ui/chalkify/lower_trait_higher_rank.stderr @@ -4,10 +4,10 @@ error: program clause dump LL | #[rustc_dump_program_clauses] //~ ERROR program clause dump | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | - = note: FromEnv(>::Output == &'a u8) :- FromEnv(Self: Foo). = note: FromEnv(F: std::marker::Sized) :- FromEnv(Self: Foo). = note: FromEnv(F: std::ops::Fn<(&'a (u8, u16),)>) :- FromEnv(Self: Foo). = note: Implemented(Self: Foo) :- FromEnv(Self: Foo). + = note: ProjectionEq(>::Output == &'a u8) :- FromEnv(Self: Foo). error: aborting due to previous error