use std::fmt;
use std::hash::Hash;
use syntax_pos::symbol::InternedString;
+use traits;
use traits::query::{
CanonicalProjectionGoal, CanonicalTyGoal, CanonicalTypeOpEqGoal, CanonicalTypeOpSubtypeGoal,
CanonicalPredicateGoal, CanonicalTypeOpProvePredicateGoal, CanonicalTypeOpNormalizeGoal,
[anon] TraitSelect,
[] ParamEnv(DefId),
+ [] Environment(DefId),
[] DescribeDef(DefId),
// FIXME(mw): DefSpans are not really inputs since they are derived from
[input] Features,
[] ProgramClausesFor(DefId),
- [] ProgramClausesForEnv(ParamEnv<'tcx>),
+ [] ProgramClausesForEnv(traits::Environment<'tcx>),
[] WasmImportModuleMap(CrateNum),
[] ForeignModules(CrateNum),
Existential
});
+<<<<<<< HEAD
impl_stable_hash_for!(struct ty::subst::UserSubsts<'tcx> { substs, user_self_ty });
impl_stable_hash_for!(struct ty::subst::UserSelfTy<'tcx> { impl_def_id, self_ty });
+=======
+impl_stable_hash_for!(
+ impl<'tcx> for struct traits::Environment<'tcx> {
+ clauses,
+ }
+);
+>>>>>>> Use `Environment` instead of `ty::ParamEnv` in chalk context
/// * `DomainGoal`
/// * `Goal`
/// * `Clause`
+/// * `Environment`
+/// * `InEnvironment`
/// are used for representing the trait system in the form of
/// logic programming clauses. They are part of the interface
/// for the chalk SLG solver.
pub hypotheses: Goals<'tcx>,
}
+/// A set of clauses that we assume to be true.
+#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
+pub struct Environment<'tcx> {
+ pub clauses: Clauses<'tcx>,
+}
+
+impl Environment<'tcx> {
+ pub fn with<G>(self, goal: G) -> InEnvironment<'tcx, G> {
+ InEnvironment {
+ environment: self,
+ goal,
+ }
+ }
+}
+
+/// Something (usually a goal), along with an environment.
+#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
+pub struct InEnvironment<'tcx, G> {
+ pub environment: Environment<'tcx>,
+ pub goal: G,
+}
+
+/// Compute the environment of the given item.
+fn environment<'a, 'tcx>(_tcx: TyCtxt<'a, 'tcx, 'tcx>, _def_id: DefId) -> Environment<'tcx> {
+ panic!()
+}
+
pub type Selection<'tcx> = Vtable<'tcx, PredicateObligation<'tcx>>;
#[derive(Clone,Debug)]
codegen_fulfill_obligation: codegen::codegen_fulfill_obligation,
vtable_methods,
substitute_normalize_and_test_predicates,
+ environment,
..*providers
};
}
}
}
-impl<'tcx> TypeFoldable<'tcx> for &'tcx ty::List<traits::Clause<'tcx>> {
+BraceStructTypeFoldableImpl! {
+ impl<'tcx> TypeFoldable<'tcx> for traits::Environment<'tcx> { clauses }
+}
+
+BraceStructTypeFoldableImpl! {
+ impl<'tcx, G> TypeFoldable<'tcx> for traits::InEnvironment<'tcx, G> {
+ environment,
+ goal
+ } where G: TypeFoldable<'tcx>
+}
+
+impl<'a, 'tcx> Lift<'tcx> for traits::Environment<'a> {
+ type Lifted = traits::Environment<'tcx>;
+ fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<Self::Lifted> {
+ tcx.lift(&self.clauses).map(|clauses| {
+ traits::Environment {
+ clauses,
+ }
+ })
+ }
+}
+
+impl<'a, 'tcx, G: Lift<'tcx>> Lift<'tcx> for traits::InEnvironment<'a, G> {
+ type Lifted = traits::InEnvironment<'tcx, G::Lifted>;
+ fn lift_to_tcx<'b, 'gcx>(&self, tcx: TyCtxt<'b, 'gcx, 'tcx>) -> Option<Self::Lifted> {
+ tcx.lift(&self.environment).and_then(|environment| {
+ tcx.lift(&self.goal).map(|goal| {
+ traits::InEnvironment {
+ environment,
+ goal,
+ }
+ })
+ })
+ }
+}
+
+impl<'tcx> TypeFoldable<'tcx> for traits::Clauses<'tcx> {
fn super_fold_with<'gcx: 'tcx, F: TypeFolder<'gcx, 'tcx>>(&self, folder: &mut F) -> Self {
let v = self.iter()
.map(|t| t.fold_with(folder))
use dep_graph::DepNode;
use hir::def_id::{CrateNum, DefId, DefIndex};
use mir::interpret::GlobalId;
+use traits;
use traits::query::{
CanonicalPredicateGoal, CanonicalProjectionGoal, CanonicalTyGoal, CanonicalTypeOpEqGoal,
CanonicalTypeOpNormalizeGoal, CanonicalTypeOpProvePredicateGoal, CanonicalTypeOpSubtypeGoal,
}
impl<'tcx> QueryDescription<'tcx> for queries::program_clauses_for_env<'tcx> {
- fn describe(_tcx: TyCtxt<'_, '_, '_>, _: ty::ParamEnv<'tcx>) -> Cow<'static, str> {
- "generating chalk-style clauses for param env".into()
+ fn describe(_tcx: TyCtxt<'_, '_, '_>, _: traits::Environment<'tcx>) -> Cow<'static, str> {
+ "generating chalk-style clauses for environment".into()
+ }
+}
+
+impl<'tcx> QueryDescription<'tcx> for queries::environment<'tcx> {
+ fn describe(_tcx: TyCtxt<'_, '_, '_>, _: DefId) -> Cow<'static, str> {
+ "return a chalk-style environment".into()
}
}
use infer::canonical::Canonical;
use hir::def_id::{CrateNum, DefId, LOCAL_CRATE, DefIndex};
+use traits;
use ty::{self, Ty, TyCtxt};
use ty::subst::Substs;
use ty::fast_reject::SimplifiedType;
}
}
+impl<'tcx> Key for traits::Environment<'tcx> {
+ fn query_crate(&self) -> CrateNum {
+ LOCAL_CRATE
+ }
+ fn default_span(&self, _: TyCtxt<'_, '_, '_>) -> Span {
+ DUMMY_SP
+ }
+}
+
impl Key for InternedString {
fn query_crate(&self) -> CrateNum {
LOCAL_CRATE
// might want to use `reveal_all()` method to change modes.
[] fn param_env: ParamEnv(DefId) -> ty::ParamEnv<'tcx>,
+ [] fn environment: Environment(DefId) -> traits::Environment<'tcx>,
+
// Trait selection queries. These are best used by invoking `ty.moves_by_default()`,
// `ty.is_copy()`, etc, since that will prune the environment where possible.
[] fn is_copy_raw: is_copy_dep_node(ty::ParamEnvAnd<'tcx, Ty<'tcx>>) -> bool,
[] fn program_clauses_for: ProgramClausesFor(DefId) -> Clauses<'tcx>,
[] fn program_clauses_for_env: ProgramClausesForEnv(
- ty::ParamEnv<'tcx>
+ traits::Environment<'tcx>
) -> Clauses<'tcx>,
},
DepKind::CheckMatch => { force!(check_match, def_id!()); }
DepKind::ParamEnv => { force!(param_env, def_id!()); }
+ DepKind::Environment => { force!(environment, def_id!()); }
DepKind::DescribeDef => { force!(describe_def, def_id!()); }
DepKind::DefSpan => { force!(def_span, def_id!()); }
DepKind::LookupStability => { force!(lookup_stability, def_id!()); }
Goal,
GoalKind,
ProgramClause,
- QuantifierKind
+ QuantifierKind,
+ Environment,
+ InEnvironment,
};
use rustc::ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
use rustc::ty::subst::Kind;
impl context::Context for ChalkArenas<'tcx> {
type CanonicalExClause = Canonical<'tcx, ExClause<Self>>;
- type CanonicalGoalInEnvironment = Canonical<'tcx, ty::ParamEnvAnd<'tcx, Goal<'tcx>>>;
+ type CanonicalGoalInEnvironment = Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>;
// u-canonicalization not yet implemented
- type UCanonicalGoalInEnvironment = Canonical<'tcx, ty::ParamEnvAnd<'tcx, Goal<'tcx>>>;
+ type UCanonicalGoalInEnvironment = Canonical<'tcx, InEnvironment<'tcx, Goal<'tcx>>>;
type CanonicalConstrainedSubst = Canonical<'tcx, ConstrainedSubst<'tcx>>;
type InferenceNormalizedSubst = CanonicalVarValues<'tcx>;
- type GoalInEnvironment = ty::ParamEnvAnd<'tcx, Goal<'tcx>>;
+ type GoalInEnvironment = InEnvironment<'tcx, Goal<'tcx>>;
type RegionConstraint = QueryRegionConstraint<'tcx>;
type Substitution = CanonicalVarValues<'tcx>;
- type Environment = ty::ParamEnv<'tcx>;
+ type Environment = Environment<'tcx>;
type Goal = Goal<'tcx>;
type UnificationResult = InferOk<'tcx, ()>;
fn goal_in_environment(
- env: &ty::ParamEnv<'tcx>,
+ env: &Environment<'tcx>,
goal: Goal<'tcx>,
- ) -> ty::ParamEnvAnd<'tcx, Goal<'tcx>> {
- env.and(goal)
+ ) -> InEnvironment<'tcx, Goal<'tcx>> {
+ env.with(goal)
}
}
impl context::AggregateOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
fn make_solution(
&self,
- _root_goal: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
+ _root_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
_simplified_answers: impl context::AnswerStream<ChalkArenas<'gcx>>,
) -> Option<Canonical<'gcx, QueryResponse<'gcx, ()>>> {
unimplemented!()
impl context::ContextOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
/// True if this is a coinductive goal -- e.g., proving an auto trait.
- fn is_coinductive(&self, _goal: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>) -> bool {
+ fn is_coinductive(
+ &self,
+ _goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>
+ ) -> bool {
unimplemented!()
}
/// - the environment and goal found by substitution `S` into `arg`
fn instantiate_ucanonical_goal<R>(
&self,
- _arg: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
+ _arg: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
_op: impl context::WithInstantiatedUCanonicalGoal<ChalkArenas<'gcx>, Output = R>,
) -> R {
unimplemented!()
}
fn canonical(
- u_canon: &'a Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
- ) -> &'a Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
+ u_canon: &'a Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
+ ) -> &'a Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>> {
u_canon
}
fn is_trivial_substitution(
- _u_canon: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
+ _u_canon: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
_canonical_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
) -> bool {
unimplemented!()
}
- fn num_universes(_: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>) -> usize {
+ fn num_universes(_: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>) -> usize {
0 // FIXME
}
/// but for the universes of universally quantified names.
fn map_goal_from_canonical(
_map: &UniverseMap,
- value: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
- ) -> Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
+ value: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
+ ) -> Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>> {
*value // FIXME universe maps not implemented yet
}
fn add_clauses(
&mut self,
- _env: &ty::ParamEnv<'tcx>,
+ _env: &Environment<'tcx>,
_clauses: Vec<ProgramClause<'tcx>>,
- ) -> ty::ParamEnv<'tcx> {
- panic!("FIXME no method to add clauses to ParamEnv yet")
+ ) -> Environment<'tcx> {
+ panic!("FIXME no method to add clauses to Environment yet")
}
}
{
fn resolvent_clause(
&mut self,
- _environment: &ty::ParamEnv<'tcx>,
+ _environment: &Environment<'tcx>,
_goal: &DomainGoal<'tcx>,
_subst: &CanonicalVarValues<'tcx>,
_clause: &ProgramClause<'tcx>,
fn apply_answer_subst(
&mut self,
_ex_clause: ChalkExClause<'tcx>,
- _selected_goal: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
- _answer_table_goal: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
+ _selected_goal: &InEnvironment<'tcx, Goal<'tcx>>,
+ _answer_table_goal: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
_canonical_answer_subst: &Canonical<'gcx, ConstrainedSubst<'gcx>>,
) -> chalk_engine::fallible::Fallible<ChalkExClause<'tcx>> {
panic!()
{
fn truncate_goal(
&mut self,
- subgoal: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
- ) -> Option<ty::ParamEnvAnd<'tcx, Goal<'tcx>>> {
+ subgoal: &InEnvironment<'tcx, Goal<'tcx>>,
+ ) -> Option<InEnvironment<'tcx, Goal<'tcx>>> {
Some(*subgoal) // FIXME we should truncate at some point!
}
{
fn program_clauses(
&self,
- _environment: &ty::ParamEnv<'tcx>,
+ _environment: &Environment<'tcx>,
goal: &DomainGoal<'tcx>,
) -> Vec<ProgramClause<'tcx>> {
use rustc::traits::WhereClause::*;
fn canonicalize_goal(
&mut self,
- value: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
- ) -> Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>> {
+ value: &InEnvironment<'tcx, Goal<'tcx>>,
+ ) -> Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>> {
let mut _orig_values = OriginalQueryValues::default();
self.infcx.canonicalize_query(value, &mut _orig_values)
}
fn u_canonicalize_goal(
&mut self,
- value: &Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
+ value: &Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
) -> (
- Canonical<'gcx, ty::ParamEnvAnd<'gcx, Goal<'gcx>>>,
+ Canonical<'gcx, InEnvironment<'gcx, Goal<'gcx>>>,
UniverseMap,
) {
(value.clone(), UniverseMap)
fn invert_goal(
&mut self,
- _value: &ty::ParamEnvAnd<'tcx, Goal<'tcx>>,
- ) -> Option<ty::ParamEnvAnd<'tcx, Goal<'tcx>>> {
+ _value: &InEnvironment<'tcx, Goal<'tcx>>,
+ ) -> Option<InEnvironment<'tcx, Goal<'tcx>>> {
panic!("goal inversion not yet implemented")
}
fn unify_parameters(
&mut self,
- _environment: &ty::ParamEnv<'tcx>,
+ _environment: &Environment<'tcx>,
_a: &Kind<'tcx>,
_b: &Kind<'tcx>,
) -> ChalkEngineFallible<InferOk<'tcx, ()>> {
+++ /dev/null
-// 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 <LICENSE-APACHE or
-// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
-// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
-// option. This file may not be copied, modified, or distributed
-// except according to those terms.
-
-use rustc::hir::def_id::DefId;
-use rustc::hir::intravisit::{self, NestedVisitorMap, Visitor};
-use rustc::hir::map::definitions::DefPathData;
-use rustc::hir::{self, ImplPolarity};
-use rustc::traits::{
- Clause,
- Clauses,
- DomainGoal,
- FromEnv,
- GoalKind,
- PolyDomainGoal,
- ProgramClause,
- WellFormed,
- WhereClause,
-};
-use rustc::ty::query::Providers;
-use rustc::ty::{self, List, TyCtxt};
-use rustc_data_structures::fx::FxHashSet;
-use std::mem;
-use syntax::ast;
-
-use std::iter;
-
-crate fn provide(p: &mut Providers) {
- *p = Providers {
- program_clauses_for,
- program_clauses_for_env,
- ..*p
- };
-}
-
-crate trait Lower<T> {
- /// Lower a rustc construct (e.g. `ty::TraitPredicate`) to a chalk-like type.
- fn lower(&self) -> T;
-}
-
-impl<T, U> Lower<Vec<U>> for Vec<T>
-where
- T: Lower<U>,
-{
- fn lower(&self) -> Vec<U> {
- self.iter().map(|item| item.lower()).collect()
- }
-}
-
-impl<'tcx> Lower<WhereClause<'tcx>> for ty::TraitPredicate<'tcx> {
- fn lower(&self) -> WhereClause<'tcx> {
- WhereClause::Implemented(*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<WhereClause<'tcx>>,
-{
- fn lower(&self) -> DomainGoal<'tcx> {
- DomainGoal::Holds(self.lower())
- }
-}
-
-/// `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
-/// example), we model them with quantified domain goals, e.g. as for the previous example:
-/// `forall<'a> { T: Fn(&'a i32) }` which corresponds to something like
-/// `Binder<Holds(Implemented(TraitPredicate))>`.
-impl<'tcx, T> Lower<PolyDomainGoal<'tcx>> for ty::Binder<T>
-where
- T: Lower<DomainGoal<'tcx>> + ty::fold::TypeFoldable<'tcx>,
-{
- fn lower(&self) -> PolyDomainGoal<'tcx> {
- self.map_bound_ref(|p| p.lower())
- }
-}
-
-impl<'tcx> Lower<PolyDomainGoal<'tcx>> for ty::Predicate<'tcx> {
- fn lower(&self) -> PolyDomainGoal<'tcx> {
- use rustc::ty::Predicate;
-
- match self {
- 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!(),
- }
- }
-}
-
-/// Used for implied bounds related rules (see rustc guide).
-trait IntoFromEnvGoal {
- /// Transforms an existing goal into a `FromEnv` goal.
- fn into_from_env_goal(self) -> Self;
-}
-
-/// Used for well-formedness related rules (see rustc guide).
-trait IntoWellFormedGoal {
- /// Transforms an existing goal into a `WellFormed` goal.
- fn into_well_formed_goal(self) -> Self;
-}
-
-impl<'tcx> IntoFromEnvGoal for DomainGoal<'tcx> {
- fn into_from_env_goal(self) -> DomainGoal<'tcx> {
- use self::WhereClause::*;
-
- match self {
- DomainGoal::Holds(Implemented(trait_ref)) => {
- DomainGoal::FromEnv(FromEnv::Trait(trait_ref))
- }
- other => other,
- }
- }
-}
-
-impl<'tcx> IntoWellFormedGoal for DomainGoal<'tcx> {
- fn into_well_formed_goal(self) -> DomainGoal<'tcx> {
- use self::WhereClause::*;
-
- match self {
- DomainGoal::Holds(Implemented(trait_ref)) => {
- DomainGoal::WellFormed(WellFormed::Trait(trait_ref))
- }
- other => other,
- }
- }
-}
-
-crate fn program_clauses_for<'a, 'tcx>(
- tcx: TyCtxt<'a, 'tcx, 'tcx>,
- def_id: DefId,
-) -> Clauses<'tcx> {
- match tcx.def_key(def_id).disambiguated_data.data {
- 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),
- _ => List::empty(),
- }
-}
-
-crate fn program_clauses_for_env<'a, 'tcx>(
- tcx: TyCtxt<'a, 'tcx, 'tcx>,
- param_env: ty::ParamEnv<'tcx>,
-) -> Clauses<'tcx> {
- debug!("program_clauses_for_env(param_env={:?})", param_env);
-
- let mut last_round = FxHashSet();
- last_round.extend(
- param_env
- .caller_bounds
- .iter()
- .flat_map(|&p| predicate_def_id(p)),
- );
-
- let mut closure = last_round.clone();
- let mut next_round = FxHashSet();
- while !last_round.is_empty() {
- next_round.extend(
- last_round
- .drain()
- .flat_map(|def_id| {
- tcx.predicates_of(def_id)
- .instantiate_identity(tcx)
- .predicates
- })
- .flat_map(|p| predicate_def_id(p))
- .filter(|&def_id| closure.insert(def_id)),
- );
- mem::swap(&mut next_round, &mut last_round);
- }
-
- debug!("program_clauses_for_env: closure = {:#?}", closure);
-
- return tcx.mk_clauses(
- closure
- .into_iter()
- .flat_map(|def_id| tcx.program_clauses_for(def_id).iter().cloned()),
- );
-
- /// Given that `predicate` is in the environment, returns the
- /// def-id of something (e.g., a trait, associated item, etc)
- /// whose predicates can also be assumed to be true. We will
- /// compute the transitive closure of such things.
- fn predicate_def_id<'tcx>(predicate: ty::Predicate<'tcx>) -> Option<DefId> {
- match predicate {
- ty::Predicate::Trait(predicate) => Some(predicate.def_id()),
-
- ty::Predicate::Projection(projection) => Some(projection.item_def_id()),
-
- ty::Predicate::WellFormed(..)
- | ty::Predicate::RegionOutlives(..)
- | ty::Predicate::TypeOutlives(..)
- | ty::Predicate::ObjectSafe(..)
- | ty::Predicate::ClosureKind(..)
- | ty::Predicate::Subtype(..)
- | ty::Predicate::ConstEvaluatable(..) => None,
- }
- }
-}
-
-fn program_clauses_for_trait<'a, 'tcx>(
- tcx: TyCtxt<'a, 'tcx, 'tcx>,
- def_id: DefId,
-) -> Clauses<'tcx> {
- // `trait Trait<P1..Pn> where WC { .. } // P0 == Self`
-
- // Rule Implemented-From-Env (see rustc guide)
- //
- // ```
- // forall<Self, P1..Pn> {
- // Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)
- // }
- // ```
-
- // `Self: Trait<P1..Pn>`
- let trait_pred = ty::TraitPredicate {
- trait_ref: ty::TraitRef::identity(tcx, def_id),
- };
-
- // `Implemented(Self: Trait<P1..Pn>)`
- let impl_trait: DomainGoal = trait_pred.lower();
-
- // `FromEnv(Self: Trait<P1..Pn>)`
- let from_env_goal = tcx.mk_goal(impl_trait.into_from_env_goal().into_goal());
- let hypotheses = tcx.intern_goals(&[from_env_goal]);
-
- // `Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)`
- let implemented_from_env = ProgramClause {
- goal: impl_trait,
- hypotheses,
- };
-
- let clauses = iter::once(Clause::ForAll(ty::Binder::dummy(implemented_from_env)));
-
- let where_clauses = &tcx.predicates_defined_on(def_id).predicates
- .into_iter()
- .map(|(wc, _)| wc.lower())
- .collect::<Vec<_>>();
-
- // Rule Implied-Bound-From-Trait
- //
- // For each where clause WC:
- // ```
- // forall<Self, P1..Pn> {
- // FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn)
- // }
- // ```
-
- // `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`, for each where clause WC
- let implied_bound_clauses = where_clauses
- .iter()
- .cloned()
-
- // `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`
- .map(|wc| wc.map_bound(|goal| ProgramClause {
- goal: goal.into_from_env_goal(),
- hypotheses,
- }))
- .map(Clause::ForAll);
-
- // Rule WellFormed-TraitRef
- //
- // Here `WC` denotes the set of all where clauses:
- // ```
- // forall<Self, P1..Pn> {
- // WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)
- // }
- // ```
-
- // `Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)`
- let wf_conditions = iter::once(ty::Binder::dummy(trait_pred.lower()))
- .chain(
- where_clauses
- .into_iter()
- .map(|wc| wc.map_bound(|goal| goal.into_well_formed_goal()))
- );
-
- // `WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)`
- let wf_clause = ProgramClause {
- goal: DomainGoal::WellFormed(WellFormed::Trait(trait_pred)),
- hypotheses: tcx.mk_goals(
- wf_conditions.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
- ),
- };
- let wf_clause = iter::once(Clause::ForAll(ty::Binder::dummy(wf_clause)));
-
- tcx.mk_clauses(
- clauses
- .chain(implied_bound_clauses)
- .chain(wf_clause)
- )
-}
-
-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 List::empty();
- }
-
- // Rule Implemented-From-Impl (see rustc guide)
- //
- // `impl<P0..Pn> Trait<A1..An> for A0 where WC { .. }`
- //
- // ```
- // forall<P0..Pn> {
- // Implemented(A0: Trait<A1..An>) :- WC
- // }
- // ```
-
- 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
- .into_iter()
- .map(|(wc, _)| wc.lower());
-
- // `Implemented(A0: Trait<A1..An>) :- WC`
- let clause = ProgramClause {
- goal: trait_pred,
- hypotheses: tcx.mk_goals(
- where_clauses
- .map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
- ),
- };
- tcx.mk_clauses(iter::once(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<P1..Pn> where WC1, ..., WCm`
- //
- // ```
- // forall<P1..Pn> {
- // WellFormed(Ty<...>) :- WC1, ..., WCm`
- // }
- // ```
-
- // `Ty<...>`
- let ty = tcx.type_of(def_id);
-
- // `WC`
- let where_clauses = tcx.predicates_of(def_id).predicates
- .into_iter()
- .map(|(wc, _)| wc.lower())
- .collect::<Vec<_>>();
-
- // `WellFormed(Ty<...>) :- WC1, ..., WCm`
- let well_formed = ProgramClause {
- goal: DomainGoal::WellFormed(WellFormed::Ty(ty)),
- hypotheses: tcx.mk_goals(
- where_clauses
- .iter()
- .cloned()
- .map(|wc| tcx.mk_goal(GoalKind::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<P1..Pn> {
- // FromEnv(WC) :- FromEnv(Ty<...>)
- // }
- // ```
-
- // `FromEnv(Ty<...>)`
- let from_env_goal = tcx.mk_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> {
- // 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>(
- tcx: TyCtxt<'a, 'tcx, 'tcx>,
- item_id: DefId,
-) -> Clauses<'tcx> {
- // Rule Normalize-From-Impl (see rustc guide)
- //
- // ```
- // 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`).
- // ```
- // forall<P0..Pm> {
- // forall<Pn+1..Pm> {
- // Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T) :-
- // Implemented(A0: Trait<A1..An>)
- // }
- // }
- // ```
-
- let item = tcx.associated_item(item_id);
- debug_assert_eq!(item.kind, ty::AssociatedKind::Type);
- 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());
-
- // `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.ident);
-
- // `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(
- hypotheses
- .into_iter()
- .map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
- ),
- };
- tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::dummy(clause))))
-}
-
-pub fn dump_program_clauses<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>) {
- if !tcx.features().rustc_attrs {
- return;
- }
-
- let mut visitor = ClauseDumper { tcx };
- tcx.hir
- .krate()
- .visit_all_item_likes(&mut visitor.as_deep_visitor());
-}
-
-struct ClauseDumper<'a, 'tcx: 'a> {
- tcx: TyCtxt<'a, 'tcx, 'tcx>,
-}
-
-impl<'a, 'tcx> ClauseDumper<'a, 'tcx> {
- fn process_attrs(&mut self, node_id: ast::NodeId, attrs: &[ast::Attribute]) {
- let def_id = self.tcx.hir.local_def_id(node_id);
- for attr in attrs {
- let mut clauses = None;
-
- if attr.check_name("rustc_dump_program_clauses") {
- clauses = Some(self.tcx.program_clauses_for(def_id));
- }
-
- if attr.check_name("rustc_dump_env_program_clauses") {
- let param_env = self.tcx.param_env(def_id);
- clauses = Some(self.tcx.program_clauses_for_env(param_env));
- }
-
- if let Some(clauses) = clauses {
- let mut err = self
- .tcx
- .sess
- .struct_span_err(attr.span, "program clause dump");
-
- let mut strings: Vec<_> = clauses
- .iter()
- .map(|clause| {
- // Skip the top-level binder for a less verbose output
- let program_clause = match clause {
- Clause::Implies(program_clause) => program_clause,
- Clause::ForAll(program_clause) => program_clause.skip_binder(),
- };
- program_clause.to_string()
- })
- .collect();
-
- strings.sort();
-
- for string in strings {
- err.note(&string);
- }
-
- err.emit();
- }
- }
- }
-}
-
-impl<'a, 'tcx> Visitor<'tcx> for ClauseDumper<'a, 'tcx> {
- fn nested_visit_map<'this>(&'this mut self) -> NestedVisitorMap<'this, 'tcx> {
- NestedVisitorMap::OnlyBodies(&self.tcx.hir)
- }
-
- fn visit_item(&mut self, item: &'tcx hir::Item) {
- self.process_attrs(item.id, &item.attrs);
- intravisit::walk_item(self, item);
- }
-
- fn visit_trait_item(&mut self, trait_item: &'tcx hir::TraitItem) {
- self.process_attrs(trait_item.id, &trait_item.attrs);
- intravisit::walk_trait_item(self, trait_item);
- }
-
- fn visit_impl_item(&mut self, impl_item: &'tcx hir::ImplItem) {
- self.process_attrs(impl_item.id, &impl_item.attrs);
- intravisit::walk_impl_item(self, impl_item);
- }
-
- fn visit_struct_field(&mut self, s: &'tcx hir::StructField) {
- self.process_attrs(s.id, &s.attrs);
- intravisit::walk_struct_field(self, s);
- }
-}
--- /dev/null
+// 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 <LICENSE-APACHE or
+// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
+// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
+// option. This file may not be copied, modified, or distributed
+// except according to those terms.
+
+use rustc::traits::{
+ Clause,
+ Clauses,
+ DomainGoal,
+ FromEnv,
+ Goal,
+ ProgramClause,
+ Environment,
+};
+use rustc::ty::{TyCtxt, Ty};
+use rustc_data_structures::fx::FxHashSet;
+
+struct ClauseVisitor<'set, 'a, 'tcx: 'a> {
+ tcx: TyCtxt<'a, 'tcx, 'tcx>,
+ round: &'set mut FxHashSet<Clause<'tcx>>,
+}
+
+impl ClauseVisitor<'set, 'a, 'tcx> {
+ fn new(tcx: TyCtxt<'a, 'tcx, 'tcx>, round: &'set mut FxHashSet<Clause<'tcx>>) -> Self {
+ ClauseVisitor {
+ tcx,
+ round,
+ }
+ }
+
+ fn visit_ty(&mut self, _ty: Ty<'tcx>) {
+
+ }
+
+ fn visit_from_env(&mut self, from_env: FromEnv<'tcx>) {
+ match from_env {
+ FromEnv::Trait(predicate) => {
+ self.round.extend(
+ self.tcx.program_clauses_for(predicate.def_id())
+ .iter()
+ .cloned()
+ );
+ }
+
+ FromEnv::Ty(ty) => self.visit_ty(ty),
+ }
+ }
+
+ fn visit_domain_goal(&mut self, domain_goal: DomainGoal<'tcx>) {
+ if let DomainGoal::FromEnv(from_env) = domain_goal {
+ self.visit_from_env(from_env);
+ }
+ }
+
+ fn visit_goal(&mut self, goal: Goal<'tcx>) {
+ match goal {
+ Goal::Implies(clauses, goal) => {
+ for clause in clauses {
+ self.visit_clause(*clause);
+ }
+ self.visit_goal(*goal);
+ }
+
+ Goal::And(goal1, goal2) => {
+ self.visit_goal(*goal1);
+ self.visit_goal(*goal2);
+ }
+
+ Goal::Not(goal) => self.visit_goal(*goal),
+ Goal::DomainGoal(domain_goal) => self.visit_domain_goal(domain_goal),
+ Goal::Quantified(_, goal) => self.visit_goal(**goal.skip_binder()),
+ Goal::CannotProve => (),
+ }
+ }
+
+ fn visit_program_clause(&mut self, clause: ProgramClause<'tcx>) {
+ self.visit_domain_goal(clause.goal);
+ for goal in clause.hypotheses {
+ self.visit_goal(*goal);
+ }
+ }
+
+ fn visit_clause(&mut self, clause: Clause<'tcx>) {
+ match clause {
+ Clause::Implies(clause) => self.visit_program_clause(clause),
+ Clause::ForAll(clause) => self.visit_program_clause(*clause.skip_binder()),
+ }
+ }
+}
+
+crate fn program_clauses_for_env<'a, 'tcx>(
+ tcx: TyCtxt<'a, 'tcx, 'tcx>,
+ environment: Environment<'tcx>,
+) -> Clauses<'tcx> {
+ debug!("program_clauses_for_env(environment={:?})", environment);
+
+ let mut last_round = FxHashSet();
+ {
+ let mut visitor = ClauseVisitor::new(tcx, &mut last_round);
+ for clause in environment.clauses {
+ visitor.visit_clause(*clause);
+ }
+ }
+
+ let mut closure = last_round.clone();
+ let mut next_round = FxHashSet();
+ while !last_round.is_empty() {
+ let mut visitor = ClauseVisitor::new(tcx, &mut next_round);
+ for clause in last_round {
+ visitor.visit_clause(clause);
+ }
+ last_round = next_round.drain()
+ .filter(|&clause| closure.insert(clause))
+ .collect();
+ }
+
+ debug!("program_clauses_for_env: closure = {:#?}", closure);
+
+ return tcx.mk_clauses(
+ closure.into_iter()
+ );
+}
--- /dev/null
+// 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 <LICENSE-APACHE or
+// http://www.apache.org/licenses/LICENSE-2.0> or the MIT license
+// <LICENSE-MIT or http://opensource.org/licenses/MIT>, at your
+// option. This file may not be copied, modified, or distributed
+// except according to those terms.
+
+mod environment;
+
+use rustc::hir::def_id::DefId;
+use rustc::hir::intravisit::{self, NestedVisitorMap, Visitor};
+use rustc::hir::map::definitions::DefPathData;
+use rustc::hir::{self, ImplPolarity};
+use rustc::traits::{
+ Clause,
+ Clauses,
+ DomainGoal,
+ FromEnv,
+ GoalKind,
+ PolyDomainGoal,
+ ProgramClause,
+ WellFormed,
+ WhereClause,
+};
+use rustc::ty::query::Providers;
+use rustc::ty::{self, List, TyCtxt};
+use syntax::ast;
+
+use std::iter;
+
+crate fn provide(p: &mut Providers) {
+ *p = Providers {
+ program_clauses_for,
+ program_clauses_for_env: environment::program_clauses_for_env,
+ ..*p
+ };
+}
+
+crate trait Lower<T> {
+ /// Lower a rustc construct (e.g. `ty::TraitPredicate`) to a chalk-like type.
+ fn lower(&self) -> T;
+}
+
+impl<T, U> Lower<Vec<U>> for Vec<T>
+where
+ T: Lower<U>,
+{
+ fn lower(&self) -> Vec<U> {
+ self.iter().map(|item| item.lower()).collect()
+ }
+}
+
+impl<'tcx> Lower<WhereClause<'tcx>> for ty::TraitPredicate<'tcx> {
+ fn lower(&self) -> WhereClause<'tcx> {
+ WhereClause::Implemented(*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<WhereClause<'tcx>>,
+{
+ fn lower(&self) -> DomainGoal<'tcx> {
+ DomainGoal::Holds(self.lower())
+ }
+}
+
+/// `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
+/// example), we model them with quantified domain goals, e.g. as for the previous example:
+/// `forall<'a> { T: Fn(&'a i32) }` which corresponds to something like
+/// `Binder<Holds(Implemented(TraitPredicate))>`.
+impl<'tcx, T> Lower<PolyDomainGoal<'tcx>> for ty::Binder<T>
+where
+ T: Lower<DomainGoal<'tcx>> + ty::fold::TypeFoldable<'tcx>,
+{
+ fn lower(&self) -> PolyDomainGoal<'tcx> {
+ self.map_bound_ref(|p| p.lower())
+ }
+}
+
+impl<'tcx> Lower<PolyDomainGoal<'tcx>> for ty::Predicate<'tcx> {
+ fn lower(&self) -> PolyDomainGoal<'tcx> {
+ use rustc::ty::Predicate;
+
+ match self {
+ 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!(),
+ }
+ }
+}
+
+/// Used for implied bounds related rules (see rustc guide).
+trait IntoFromEnvGoal {
+ /// Transforms an existing goal into a `FromEnv` goal.
+ fn into_from_env_goal(self) -> Self;
+}
+
+/// Used for well-formedness related rules (see rustc guide).
+trait IntoWellFormedGoal {
+ /// Transforms an existing goal into a `WellFormed` goal.
+ fn into_well_formed_goal(self) -> Self;
+}
+
+impl<'tcx> IntoFromEnvGoal for DomainGoal<'tcx> {
+ fn into_from_env_goal(self) -> DomainGoal<'tcx> {
+ use self::WhereClause::*;
+
+ match self {
+ DomainGoal::Holds(Implemented(trait_ref)) => {
+ DomainGoal::FromEnv(FromEnv::Trait(trait_ref))
+ }
+ other => other,
+ }
+ }
+}
+
+impl<'tcx> IntoWellFormedGoal for DomainGoal<'tcx> {
+ fn into_well_formed_goal(self) -> DomainGoal<'tcx> {
+ use self::WhereClause::*;
+
+ match self {
+ DomainGoal::Holds(Implemented(trait_ref)) => {
+ DomainGoal::WellFormed(WellFormed::Trait(trait_ref))
+ }
+ other => other,
+ }
+ }
+}
+
+crate fn program_clauses_for<'a, 'tcx>(
+ tcx: TyCtxt<'a, 'tcx, 'tcx>,
+ def_id: DefId,
+) -> Clauses<'tcx> {
+ match tcx.def_key(def_id).disambiguated_data.data {
+ 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),
+ _ => List::empty(),
+ }
+}
+
+fn program_clauses_for_trait<'a, 'tcx>(
+ tcx: TyCtxt<'a, 'tcx, 'tcx>,
+ def_id: DefId,
+) -> Clauses<'tcx> {
+ // `trait Trait<P1..Pn> where WC { .. } // P0 == Self`
+
+ // Rule Implemented-From-Env (see rustc guide)
+ //
+ // ```
+ // forall<Self, P1..Pn> {
+ // Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)
+ // }
+ // ```
+
+ // `Self: Trait<P1..Pn>`
+ let trait_pred = ty::TraitPredicate {
+ trait_ref: ty::TraitRef::identity(tcx, def_id),
+ };
+
+ // `Implemented(Self: Trait<P1..Pn>)`
+ let impl_trait: DomainGoal = trait_pred.lower();
+
+ // `FromEnv(Self: Trait<P1..Pn>)`
+ let from_env_goal = tcx.mk_goal(impl_trait.into_from_env_goal().into_goal());
+ let hypotheses = tcx.intern_goals(&[from_env_goal]);
+
+ // `Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)`
+ let implemented_from_env = ProgramClause {
+ goal: impl_trait,
+ hypotheses,
+ };
+
+ let clauses = iter::once(Clause::ForAll(ty::Binder::dummy(implemented_from_env)));
+
+ let where_clauses = &tcx.predicates_defined_on(def_id).predicates
+ .into_iter()
+ .map(|(wc, _)| wc.lower())
+ .collect::<Vec<_>>();
+
+ // Rule Implied-Bound-From-Trait
+ //
+ // For each where clause WC:
+ // ```
+ // forall<Self, P1..Pn> {
+ // FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn)
+ // }
+ // ```
+
+ // `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`, for each where clause WC
+ let implied_bound_clauses = where_clauses
+ .iter()
+ .cloned()
+
+ // `FromEnv(WC) :- FromEnv(Self: Trait<P1..Pn>)`
+ .map(|wc| wc.map_bound(|goal| ProgramClause {
+ goal: goal.into_from_env_goal(),
+ hypotheses,
+ }))
+ .map(Clause::ForAll);
+
+ // Rule WellFormed-TraitRef
+ //
+ // Here `WC` denotes the set of all where clauses:
+ // ```
+ // forall<Self, P1..Pn> {
+ // WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)
+ // }
+ // ```
+
+ // `Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)`
+ let wf_conditions = iter::once(ty::Binder::dummy(trait_pred.lower()))
+ .chain(
+ where_clauses
+ .into_iter()
+ .map(|wc| wc.map_bound(|goal| goal.into_well_formed_goal()))
+ );
+
+ // `WellFormed(Self: Trait<P1..Pn>) :- Implemented(Self: Trait<P1..Pn>) && WellFormed(WC)`
+ let wf_clause = ProgramClause {
+ goal: DomainGoal::WellFormed(WellFormed::Trait(trait_pred)),
+ hypotheses: tcx.mk_goals(
+ wf_conditions.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
+ ),
+ };
+ let wf_clause = iter::once(Clause::ForAll(ty::Binder::dummy(wf_clause)));
+
+ tcx.mk_clauses(
+ clauses
+ .chain(implied_bound_clauses)
+ .chain(wf_clause)
+ )
+}
+
+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 List::empty();
+ }
+
+ // Rule Implemented-From-Impl (see rustc guide)
+ //
+ // `impl<P0..Pn> Trait<A1..An> for A0 where WC { .. }`
+ //
+ // ```
+ // forall<P0..Pn> {
+ // Implemented(A0: Trait<A1..An>) :- WC
+ // }
+ // ```
+
+ 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
+ .into_iter()
+ .map(|(wc, _)| wc.lower());
+
+ // `Implemented(A0: Trait<A1..An>) :- WC`
+ let clause = ProgramClause {
+ goal: trait_pred,
+ hypotheses: tcx.mk_goals(
+ where_clauses
+ .map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
+ ),
+ };
+ tcx.mk_clauses(iter::once(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<P1..Pn> where WC1, ..., WCm`
+ //
+ // ```
+ // forall<P1..Pn> {
+ // WellFormed(Ty<...>) :- WC1, ..., WCm`
+ // }
+ // ```
+
+ // `Ty<...>`
+ let ty = tcx.type_of(def_id);
+
+ // `WC`
+ let where_clauses = tcx.predicates_of(def_id).predicates
+ .into_iter()
+ .map(|(wc, _)| wc.lower())
+ .collect::<Vec<_>>();
+
+ // `WellFormed(Ty<...>) :- WC1, ..., WCm`
+ let well_formed = ProgramClause {
+ goal: DomainGoal::WellFormed(WellFormed::Ty(ty)),
+ hypotheses: tcx.mk_goals(
+ where_clauses
+ .iter()
+ .cloned()
+ .map(|wc| tcx.mk_goal(GoalKind::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<P1..Pn> {
+ // FromEnv(WC) :- FromEnv(Ty<...>)
+ // }
+ // ```
+
+ // `FromEnv(Ty<...>)`
+ let from_env_goal = tcx.mk_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> {
+ // 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>(
+ tcx: TyCtxt<'a, 'tcx, 'tcx>,
+ item_id: DefId,
+) -> Clauses<'tcx> {
+ // Rule Normalize-From-Impl (see rustc guide)
+ //
+ // ```
+ // 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`).
+ // ```
+ // forall<P0..Pm> {
+ // forall<Pn+1..Pm> {
+ // Normalize(<A0 as Trait<A1..An>>::AssocType<Pn+1..Pm> -> T) :-
+ // Implemented(A0: Trait<A1..An>)
+ // }
+ // }
+ // ```
+
+ let item = tcx.associated_item(item_id);
+ debug_assert_eq!(item.kind, ty::AssociatedKind::Type);
+ 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());
+
+ // `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.ident);
+
+ // `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(
+ hypotheses
+ .into_iter()
+ .map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
+ ),
+ };
+ tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::dummy(clause))))
+}
+
+pub fn dump_program_clauses<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>) {
+ if !tcx.features().rustc_attrs {
+ return;
+ }
+
+ let mut visitor = ClauseDumper { tcx };
+ tcx.hir
+ .krate()
+ .visit_all_item_likes(&mut visitor.as_deep_visitor());
+}
+
+struct ClauseDumper<'a, 'tcx: 'a> {
+ tcx: TyCtxt<'a, 'tcx, 'tcx>,
+}
+
+impl<'a, 'tcx> ClauseDumper<'a, 'tcx> {
+ fn process_attrs(&mut self, node_id: ast::NodeId, attrs: &[ast::Attribute]) {
+ let def_id = self.tcx.hir.local_def_id(node_id);
+ for attr in attrs {
+ let mut clauses = None;
+
+ if attr.check_name("rustc_dump_program_clauses") {
+ clauses = Some(self.tcx.program_clauses_for(def_id));
+ }
+
+ if attr.check_name("rustc_dump_env_program_clauses") {
+ let environment = self.tcx.environment(def_id);
+ clauses = Some(self.tcx.program_clauses_for_env(environment));
+ }
+
+ if let Some(clauses) = clauses {
+ let mut err = self
+ .tcx
+ .sess
+ .struct_span_err(attr.span, "program clause dump");
+
+ let mut strings: Vec<_> = clauses
+ .iter()
+ .map(|clause| {
+ // Skip the top-level binder for a less verbose output
+ let program_clause = match clause {
+ Clause::Implies(program_clause) => program_clause,
+ Clause::ForAll(program_clause) => program_clause.skip_binder(),
+ };
+ program_clause.to_string()
+ })
+ .collect();
+
+ strings.sort();
+
+ for string in strings {
+ err.note(&string);
+ }
+
+ err.emit();
+ }
+ }
+ }
+}
+
+impl<'a, 'tcx> Visitor<'tcx> for ClauseDumper<'a, 'tcx> {
+ fn nested_visit_map<'this>(&'this mut self) -> NestedVisitorMap<'this, 'tcx> {
+ NestedVisitorMap::OnlyBodies(&self.tcx.hir)
+ }
+
+ fn visit_item(&mut self, item: &'tcx hir::Item) {
+ self.process_attrs(item.id, &item.attrs);
+ intravisit::walk_item(self, item);
+ }
+
+ fn visit_trait_item(&mut self, trait_item: &'tcx hir::TraitItem) {
+ self.process_attrs(trait_item.id, &trait_item.attrs);
+ intravisit::walk_trait_item(self, trait_item);
+ }
+
+ fn visit_impl_item(&mut self, impl_item: &'tcx hir::ImplItem) {
+ self.process_attrs(impl_item.id, &impl_item.attrs);
+ intravisit::walk_impl_item(self, impl_item);
+ }
+
+ fn visit_struct_field(&mut self, s: &'tcx hir::StructField) {
+ self.process_attrs(s.id, &s.attrs);
+ intravisit::walk_struct_field(self, s);
+ }
+}
projects / rust.git / commitdiff