Use Environment instead of ty::ParamEnv in chalk context
This commit is contained in:
parent
cbbd70d4f2
commit
62df973293
11 changed files with 271 additions and 103 deletions
|
|
@ -70,6 +70,7 @@ use rustc_data_structures::stable_hasher::{StableHasher, HashStable};
|
|||
use std::fmt;
|
||||
use std::hash::Hash;
|
||||
use syntax_pos::symbol::InternedString;
|
||||
use traits;
|
||||
use traits::query::{
|
||||
CanonicalProjectionGoal, CanonicalTyGoal, CanonicalTypeOpEqGoal, CanonicalTypeOpSubtypeGoal,
|
||||
CanonicalPredicateGoal, CanonicalTypeOpProvePredicateGoal, CanonicalTypeOpNormalizeGoal,
|
||||
|
|
@ -550,6 +551,7 @@ define_dep_nodes!( <'tcx>
|
|||
[anon] TraitSelect,
|
||||
|
||||
[] ParamEnv(DefId),
|
||||
[] Environment(DefId),
|
||||
[] DescribeDef(DefId),
|
||||
|
||||
// FIXME(mw): DefSpans are not really inputs since they are derived from
|
||||
|
|
@ -669,7 +671,7 @@ define_dep_nodes!( <'tcx>
|
|||
[input] Features,
|
||||
|
||||
[] ProgramClausesFor(DefId),
|
||||
[] ProgramClausesForEnv(ParamEnv<'tcx>),
|
||||
[] ProgramClausesForEnv(traits::Environment<'tcx>),
|
||||
[] WasmImportModuleMap(CrateNum),
|
||||
[] ForeignModules(CrateNum),
|
||||
|
||||
|
|
|
|||
|
|
@ -1418,7 +1418,15 @@ impl_stable_hash_for!(enum traits::QuantifierKind {
|
|||
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
|
||||
|
|
|
|||
|
|
@ -278,6 +278,8 @@ pub type TraitObligations<'tcx> = Vec<TraitObligation<'tcx>>;
|
|||
/// * `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.
|
||||
|
|
@ -378,6 +380,33 @@ pub struct ProgramClause<'tcx> {
|
|||
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)]
|
||||
|
|
@ -1080,6 +1109,7 @@ pub fn provide(providers: &mut ty::query::Providers<'_>) {
|
|||
codegen_fulfill_obligation: codegen::codegen_fulfill_obligation,
|
||||
vtable_methods,
|
||||
substitute_normalize_and_test_predicates,
|
||||
environment,
|
||||
..*providers
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -658,7 +658,43 @@ EnumTypeFoldableImpl! {
|
|||
}
|
||||
}
|
||||
|
||||
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))
|
||||
|
|
|
|||
|
|
@ -12,6 +12,7 @@ use dep_graph::SerializedDepNodeIndex;
|
|||
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,
|
||||
|
|
@ -826,8 +827,14 @@ impl<'tcx> QueryDescription<'tcx> for queries::program_clauses_for<'tcx> {
|
|||
}
|
||||
|
||||
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()
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -12,6 +12,7 @@
|
|||
|
||||
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;
|
||||
|
|
@ -181,6 +182,15 @@ impl<'tcx, T: Key> Key for ty::ParamEnvAnd<'tcx, T> {
|
|||
}
|
||||
}
|
||||
|
||||
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
|
||||
|
|
|
|||
|
|
@ -377,6 +377,8 @@ define_queries! { <'tcx>
|
|||
// 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,
|
||||
|
|
@ -664,7 +666,7 @@ define_queries! { <'tcx>
|
|||
[] fn program_clauses_for: ProgramClausesFor(DefId) -> Clauses<'tcx>,
|
||||
|
||||
[] fn program_clauses_for_env: ProgramClausesForEnv(
|
||||
ty::ParamEnv<'tcx>
|
||||
traits::Environment<'tcx>
|
||||
) -> Clauses<'tcx>,
|
||||
},
|
||||
|
||||
|
|
|
|||
|
|
@ -1156,6 +1156,7 @@ pub fn force_from_dep_node<'a, 'gcx, 'lcx>(tcx: TyCtxt<'a, 'gcx, 'lcx>,
|
|||
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!()); }
|
||||
|
|
|
|||
|
|
@ -23,7 +23,9 @@ use rustc::traits::{
|
|||
Goal,
|
||||
GoalKind,
|
||||
ProgramClause,
|
||||
QuantifierKind
|
||||
QuantifierKind,
|
||||
Environment,
|
||||
InEnvironment,
|
||||
};
|
||||
use rustc::ty::fold::{TypeFoldable, TypeFolder, TypeVisitor};
|
||||
use rustc::ty::subst::Kind;
|
||||
|
|
@ -68,10 +70,10 @@ BraceStructTypeFoldableImpl! {
|
|||
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>>;
|
||||
|
||||
|
|
@ -82,13 +84,13 @@ impl context::Context for ChalkArenas<'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>;
|
||||
|
||||
|
|
@ -105,17 +107,17 @@ impl context::Context for ChalkArenas<'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!()
|
||||
|
|
@ -124,7 +126,10 @@ impl context::AggregateOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
|
|||
|
||||
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!()
|
||||
}
|
||||
|
||||
|
|
@ -142,7 +147,7 @@ impl context::ContextOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
|
|||
/// - 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!()
|
||||
|
|
@ -175,19 +180,19 @@ impl context::ContextOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
|
|||
}
|
||||
|
||||
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
|
||||
}
|
||||
|
||||
|
|
@ -196,8 +201,8 @@ impl context::ContextOps<ChalkArenas<'gcx>> for ChalkContext<'cx, 'gcx> {
|
|||
/// 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
|
||||
}
|
||||
|
||||
|
|
@ -267,10 +272,10 @@ impl context::InferenceTable<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
|||
|
||||
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")
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -279,7 +284,7 @@ impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
|||
{
|
||||
fn resolvent_clause(
|
||||
&mut self,
|
||||
_environment: &ty::ParamEnv<'tcx>,
|
||||
_environment: &Environment<'tcx>,
|
||||
_goal: &DomainGoal<'tcx>,
|
||||
_subst: &CanonicalVarValues<'tcx>,
|
||||
_clause: &ProgramClause<'tcx>,
|
||||
|
|
@ -290,8 +295,8 @@ impl context::ResolventOps<ChalkArenas<'gcx>, ChalkArenas<'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!()
|
||||
|
|
@ -303,8 +308,8 @@ impl context::TruncateOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
|||
{
|
||||
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!
|
||||
}
|
||||
|
||||
|
|
@ -321,7 +326,7 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
|||
{
|
||||
fn program_clauses(
|
||||
&self,
|
||||
_environment: &ty::ParamEnv<'tcx>,
|
||||
_environment: &Environment<'tcx>,
|
||||
goal: &DomainGoal<'tcx>,
|
||||
) -> Vec<ProgramClause<'tcx>> {
|
||||
use rustc::traits::WhereClause::*;
|
||||
|
|
@ -389,8 +394,8 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
|||
|
||||
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)
|
||||
}
|
||||
|
|
@ -412,9 +417,9 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
|||
|
||||
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)
|
||||
|
|
@ -422,14 +427,14 @@ impl context::UnificationOps<ChalkArenas<'gcx>, ChalkArenas<'tcx>>
|
|||
|
||||
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, ()>> {
|
||||
|
|
|
|||
127
src/librustc_traits/lowering/environment.rs
Normal file
127
src/librustc_traits/lowering/environment.rs
Normal file
|
|
@ -0,0 +1,127 @@
|
|||
// 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()
|
||||
);
|
||||
}
|
||||
|
|
@ -8,6 +8,8 @@
|
|||
// 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;
|
||||
|
|
@ -25,8 +27,6 @@ use rustc::traits::{
|
|||
};
|
||||
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;
|
||||
|
|
@ -34,7 +34,7 @@ use std::iter;
|
|||
crate fn provide(p: &mut Providers) {
|
||||
*p = Providers {
|
||||
program_clauses_for,
|
||||
program_clauses_for_env,
|
||||
program_clauses_for_env: environment::program_clauses_for_env,
|
||||
..*p
|
||||
};
|
||||
}
|
||||
|
|
@ -173,66 +173,6 @@ crate fn program_clauses_for<'a, 'tcx>(
|
|||
}
|
||||
}
|
||||
|
||||
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,
|
||||
|
|
@ -595,8 +535,8 @@ impl<'a, 'tcx> ClauseDumper<'a, 'tcx> {
|
|||
}
|
||||
|
||||
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));
|
||||
let environment = self.tcx.environment(def_id);
|
||||
clauses = Some(self.tcx.program_clauses_for_env(environment));
|
||||
}
|
||||
|
||||
if let Some(clauses) = clauses {
|
||||
Loading…
Add table
Add a link
Reference in a new issue