Categorize chalk clauses
This commit is contained in:
parent
e1926080db
commit
a1931d31f7
5 changed files with 55 additions and 8 deletions
|
@ -1395,10 +1395,16 @@ impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::Goal<'tcx> {
|
||||||
|
|
||||||
impl_stable_hash_for!(
|
impl_stable_hash_for!(
|
||||||
impl<'tcx> for struct traits::ProgramClause<'tcx> {
|
impl<'tcx> for struct traits::ProgramClause<'tcx> {
|
||||||
goal, hypotheses
|
goal, hypotheses, category
|
||||||
}
|
}
|
||||||
);
|
);
|
||||||
|
|
||||||
|
impl_stable_hash_for!(enum traits::ProgramClauseCategory {
|
||||||
|
ImpliedBound,
|
||||||
|
WellFormed,
|
||||||
|
Other,
|
||||||
|
});
|
||||||
|
|
||||||
impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::Clause<'tcx> {
|
impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::Clause<'tcx> {
|
||||||
fn hash_stable<W: StableHasherResult>(&self,
|
fn hash_stable<W: StableHasherResult>(&self,
|
||||||
hcx: &mut StableHashingContext<'a>,
|
hcx: &mut StableHashingContext<'a>,
|
||||||
|
|
|
@ -341,7 +341,8 @@ impl<'tcx> DomainGoal<'tcx> {
|
||||||
pub fn into_program_clause(self) -> ProgramClause<'tcx> {
|
pub fn into_program_clause(self) -> ProgramClause<'tcx> {
|
||||||
ProgramClause {
|
ProgramClause {
|
||||||
goal: self,
|
goal: self,
|
||||||
hypotheses: &ty::List::empty(),
|
hypotheses: ty::List::empty(),
|
||||||
|
category: ProgramClauseCategory::Other,
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -369,6 +370,15 @@ pub enum Clause<'tcx> {
|
||||||
ForAll(ty::Binder<ProgramClause<'tcx>>),
|
ForAll(ty::Binder<ProgramClause<'tcx>>),
|
||||||
}
|
}
|
||||||
|
|
||||||
|
impl Clause<'tcx> {
|
||||||
|
pub fn category(self) -> ProgramClauseCategory {
|
||||||
|
match self {
|
||||||
|
Clause::Implies(clause) => clause.category,
|
||||||
|
Clause::ForAll(clause) => clause.skip_binder().category,
|
||||||
|
}
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
/// Multiple clauses.
|
/// Multiple clauses.
|
||||||
pub type Clauses<'tcx> = &'tcx List<Clause<'tcx>>;
|
pub type Clauses<'tcx> = &'tcx List<Clause<'tcx>>;
|
||||||
|
|
||||||
|
@ -385,6 +395,16 @@ pub struct ProgramClause<'tcx> {
|
||||||
|
|
||||||
/// ...if we can prove these hypotheses (there may be no hypotheses at all):
|
/// ...if we can prove these hypotheses (there may be no hypotheses at all):
|
||||||
pub hypotheses: Goals<'tcx>,
|
pub hypotheses: Goals<'tcx>,
|
||||||
|
|
||||||
|
/// Useful for filtering clauses.
|
||||||
|
pub category: ProgramClauseCategory,
|
||||||
|
}
|
||||||
|
|
||||||
|
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
|
||||||
|
pub enum ProgramClauseCategory {
|
||||||
|
ImpliedBound,
|
||||||
|
WellFormed,
|
||||||
|
Other,
|
||||||
}
|
}
|
||||||
|
|
||||||
/// A set of clauses that we assume to be true.
|
/// A set of clauses that we assume to be true.
|
||||||
|
|
|
@ -496,7 +496,7 @@ impl<'tcx> fmt::Display for traits::Goal<'tcx> {
|
||||||
|
|
||||||
impl<'tcx> fmt::Display for traits::ProgramClause<'tcx> {
|
impl<'tcx> fmt::Display for traits::ProgramClause<'tcx> {
|
||||||
fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
|
fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||||
let traits::ProgramClause { goal, hypotheses } = self;
|
let traits::ProgramClause { goal, hypotheses, .. } = self;
|
||||||
write!(fmt, "{}", goal)?;
|
write!(fmt, "{}", goal)?;
|
||||||
if !hypotheses.is_empty() {
|
if !hypotheses.is_empty() {
|
||||||
write!(fmt, " :- ")?;
|
write!(fmt, " :- ")?;
|
||||||
|
@ -647,10 +647,15 @@ impl<'tcx> TypeFoldable<'tcx> for traits::Goal<'tcx> {
|
||||||
BraceStructTypeFoldableImpl! {
|
BraceStructTypeFoldableImpl! {
|
||||||
impl<'tcx> TypeFoldable<'tcx> for traits::ProgramClause<'tcx> {
|
impl<'tcx> TypeFoldable<'tcx> for traits::ProgramClause<'tcx> {
|
||||||
goal,
|
goal,
|
||||||
hypotheses
|
hypotheses,
|
||||||
|
category,
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
CloneTypeFoldableAndLiftImpls! {
|
||||||
|
traits::ProgramClauseCategory,
|
||||||
|
}
|
||||||
|
|
||||||
EnumTypeFoldableImpl! {
|
EnumTypeFoldableImpl! {
|
||||||
impl<'tcx> TypeFoldable<'tcx> for traits::Clause<'tcx> {
|
impl<'tcx> TypeFoldable<'tcx> for traits::Clause<'tcx> {
|
||||||
(traits::Clause::Implies)(clause),
|
(traits::Clause::Implies)(clause),
|
||||||
|
|
|
@ -14,6 +14,7 @@ use rustc::traits::{
|
||||||
DomainGoal,
|
DomainGoal,
|
||||||
FromEnv,
|
FromEnv,
|
||||||
ProgramClause,
|
ProgramClause,
|
||||||
|
ProgramClauseCategory,
|
||||||
Environment,
|
Environment,
|
||||||
};
|
};
|
||||||
use rustc::ty::{self, TyCtxt, Ty};
|
use rustc::ty::{self, TyCtxt, Ty};
|
||||||
|
@ -39,6 +40,7 @@ impl ClauseVisitor<'set, 'a, 'tcx> {
|
||||||
self.round.extend(
|
self.round.extend(
|
||||||
self.tcx.program_clauses_for(data.item_def_id)
|
self.tcx.program_clauses_for(data.item_def_id)
|
||||||
.iter()
|
.iter()
|
||||||
|
.filter(|c| c.category() == ProgramClauseCategory::ImpliedBound)
|
||||||
.cloned()
|
.cloned()
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
@ -56,6 +58,7 @@ impl ClauseVisitor<'set, 'a, 'tcx> {
|
||||||
self.round.extend(
|
self.round.extend(
|
||||||
self.tcx.program_clauses_for(def.did)
|
self.tcx.program_clauses_for(def.did)
|
||||||
.iter()
|
.iter()
|
||||||
|
.filter(|c| c.category() == ProgramClauseCategory::ImpliedBound)
|
||||||
.cloned()
|
.cloned()
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
@ -68,6 +71,7 @@ impl ClauseVisitor<'set, 'a, 'tcx> {
|
||||||
self.round.extend(
|
self.round.extend(
|
||||||
self.tcx.program_clauses_for(def_id)
|
self.tcx.program_clauses_for(def_id)
|
||||||
.iter()
|
.iter()
|
||||||
|
.filter(|c| c.category() == ProgramClauseCategory::ImpliedBound)
|
||||||
.cloned()
|
.cloned()
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
@ -98,6 +102,7 @@ impl ClauseVisitor<'set, 'a, 'tcx> {
|
||||||
self.round.extend(
|
self.round.extend(
|
||||||
self.tcx.program_clauses_for(predicate.def_id())
|
self.tcx.program_clauses_for(predicate.def_id())
|
||||||
.iter()
|
.iter()
|
||||||
|
.filter(|c| c.category() == ProgramClauseCategory::ImpliedBound)
|
||||||
.cloned()
|
.cloned()
|
||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
@ -176,7 +181,7 @@ crate fn environment<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId) -> En
|
||||||
// Compute the bounds on `Self` and the type parameters.
|
// Compute the bounds on `Self` and the type parameters.
|
||||||
let ty::InstantiatedPredicates { predicates } =
|
let ty::InstantiatedPredicates { predicates } =
|
||||||
tcx.predicates_of(def_id).instantiate_identity(tcx);
|
tcx.predicates_of(def_id).instantiate_identity(tcx);
|
||||||
|
|
||||||
let clauses = predicates.into_iter()
|
let clauses = predicates.into_iter()
|
||||||
.map(|predicate| predicate.lower())
|
.map(|predicate| predicate.lower())
|
||||||
.map(|domain_goal| domain_goal.map_bound(|bound| bound.into_from_env_goal()))
|
.map(|domain_goal| domain_goal.map_bound(|bound| bound.into_from_env_goal()))
|
||||||
|
@ -185,7 +190,7 @@ crate fn environment<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId) -> En
|
||||||
// `ForAll` because each `domain_goal` is a `PolyDomainGoal` and
|
// `ForAll` because each `domain_goal` is a `PolyDomainGoal` and
|
||||||
// could bound lifetimes.
|
// could bound lifetimes.
|
||||||
.map(Clause::ForAll);
|
.map(Clause::ForAll);
|
||||||
|
|
||||||
let node_id = tcx.hir.as_local_node_id(def_id).unwrap();
|
let node_id = tcx.hir.as_local_node_id(def_id).unwrap();
|
||||||
let node = tcx.hir.get(node_id);
|
let node = tcx.hir.get(node_id);
|
||||||
|
|
||||||
|
@ -243,7 +248,7 @@ crate fn environment<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId) -> En
|
||||||
.map(|domain_goal| domain_goal.into_program_clause())
|
.map(|domain_goal| domain_goal.into_program_clause())
|
||||||
.map(Clause::Implies)
|
.map(Clause::Implies)
|
||||||
);
|
);
|
||||||
|
|
||||||
Environment {
|
Environment {
|
||||||
clauses: tcx.mk_clauses(clauses),
|
clauses: tcx.mk_clauses(clauses),
|
||||||
}
|
}
|
||||||
|
|
|
@ -22,6 +22,7 @@ use rustc::traits::{
|
||||||
GoalKind,
|
GoalKind,
|
||||||
PolyDomainGoal,
|
PolyDomainGoal,
|
||||||
ProgramClause,
|
ProgramClause,
|
||||||
|
ProgramClauseCategory,
|
||||||
WellFormed,
|
WellFormed,
|
||||||
WhereClause,
|
WhereClause,
|
||||||
};
|
};
|
||||||
|
@ -204,6 +205,7 @@ fn program_clauses_for_trait<'a, 'tcx>(
|
||||||
let implemented_from_env = ProgramClause {
|
let implemented_from_env = ProgramClause {
|
||||||
goal: impl_trait,
|
goal: impl_trait,
|
||||||
hypotheses,
|
hypotheses,
|
||||||
|
category: ProgramClauseCategory::ImpliedBound,
|
||||||
};
|
};
|
||||||
|
|
||||||
let clauses = iter::once(Clause::ForAll(ty::Binder::dummy(implemented_from_env)));
|
let clauses = iter::once(Clause::ForAll(ty::Binder::dummy(implemented_from_env)));
|
||||||
|
@ -231,6 +233,7 @@ fn program_clauses_for_trait<'a, 'tcx>(
|
||||||
.map(|wc| wc.map_bound(|goal| ProgramClause {
|
.map(|wc| wc.map_bound(|goal| ProgramClause {
|
||||||
goal: goal.into_from_env_goal(),
|
goal: goal.into_from_env_goal(),
|
||||||
hypotheses,
|
hypotheses,
|
||||||
|
category: ProgramClauseCategory::ImpliedBound,
|
||||||
}))
|
}))
|
||||||
.map(Clause::ForAll);
|
.map(Clause::ForAll);
|
||||||
|
|
||||||
|
@ -257,6 +260,7 @@ fn program_clauses_for_trait<'a, 'tcx>(
|
||||||
hypotheses: tcx.mk_goals(
|
hypotheses: tcx.mk_goals(
|
||||||
wf_conditions.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
|
wf_conditions.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
|
||||||
),
|
),
|
||||||
|
category: ProgramClauseCategory::WellFormed,
|
||||||
};
|
};
|
||||||
let wf_clause = iter::once(Clause::ForAll(ty::Binder::dummy(wf_clause)));
|
let wf_clause = iter::once(Clause::ForAll(ty::Binder::dummy(wf_clause)));
|
||||||
|
|
||||||
|
@ -299,6 +303,7 @@ fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId
|
||||||
where_clauses
|
where_clauses
|
||||||
.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
|
.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
|
||||||
),
|
),
|
||||||
|
category: ProgramClauseCategory::Other,
|
||||||
};
|
};
|
||||||
tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::dummy(clause))))
|
tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::dummy(clause))))
|
||||||
}
|
}
|
||||||
|
@ -335,6 +340,7 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
|
||||||
.cloned()
|
.cloned()
|
||||||
.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
|
.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
|
||||||
),
|
),
|
||||||
|
category: ProgramClauseCategory::WellFormed,
|
||||||
};
|
};
|
||||||
|
|
||||||
let well_formed_clause = iter::once(Clause::ForAll(ty::Binder::dummy(well_formed)));
|
let well_formed_clause = iter::once(Clause::ForAll(ty::Binder::dummy(well_formed)));
|
||||||
|
@ -360,6 +366,7 @@ pub fn program_clauses_for_type_def<'a, 'tcx>(
|
||||||
.map(|wc| wc.map_bound(|goal| ProgramClause {
|
.map(|wc| wc.map_bound(|goal| ProgramClause {
|
||||||
goal: goal.into_from_env_goal(),
|
goal: goal.into_from_env_goal(),
|
||||||
hypotheses,
|
hypotheses,
|
||||||
|
category: ProgramClauseCategory::ImpliedBound,
|
||||||
}))
|
}))
|
||||||
|
|
||||||
.map(Clause::ForAll);
|
.map(Clause::ForAll);
|
||||||
|
@ -407,7 +414,8 @@ pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
|
||||||
|
|
||||||
let projection_eq_clause = ProgramClause {
|
let projection_eq_clause = ProgramClause {
|
||||||
goal: DomainGoal::Holds(projection_eq),
|
goal: DomainGoal::Holds(projection_eq),
|
||||||
hypotheses: &ty::List::empty(),
|
hypotheses: ty::List::empty(),
|
||||||
|
category: ProgramClauseCategory::Other,
|
||||||
};
|
};
|
||||||
|
|
||||||
// Rule WellFormed-AssocTy
|
// Rule WellFormed-AssocTy
|
||||||
|
@ -425,6 +433,7 @@ pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
|
||||||
let wf_clause = ProgramClause {
|
let wf_clause = ProgramClause {
|
||||||
goal: DomainGoal::WellFormed(WellFormed::Ty(placeholder_ty)),
|
goal: DomainGoal::WellFormed(WellFormed::Ty(placeholder_ty)),
|
||||||
hypotheses: tcx.mk_goals(iter::once(hypothesis)),
|
hypotheses: tcx.mk_goals(iter::once(hypothesis)),
|
||||||
|
category: ProgramClauseCategory::Other,
|
||||||
};
|
};
|
||||||
|
|
||||||
// Rule Implied-Trait-From-AssocTy
|
// Rule Implied-Trait-From-AssocTy
|
||||||
|
@ -441,6 +450,7 @@ pub fn program_clauses_for_associated_type_def<'a, 'tcx>(
|
||||||
let from_env_clause = ProgramClause {
|
let from_env_clause = ProgramClause {
|
||||||
goal: DomainGoal::FromEnv(FromEnv::Trait(trait_predicate)),
|
goal: DomainGoal::FromEnv(FromEnv::Trait(trait_predicate)),
|
||||||
hypotheses: tcx.mk_goals(iter::once(hypothesis)),
|
hypotheses: tcx.mk_goals(iter::once(hypothesis)),
|
||||||
|
category: ProgramClauseCategory::ImpliedBound,
|
||||||
};
|
};
|
||||||
|
|
||||||
let clauses = iter::once(projection_eq_clause)
|
let clauses = iter::once(projection_eq_clause)
|
||||||
|
@ -506,6 +516,7 @@ pub fn program_clauses_for_associated_type_value<'a, 'tcx>(
|
||||||
.into_iter()
|
.into_iter()
|
||||||
.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
|
.map(|wc| tcx.mk_goal(GoalKind::from_poly_domain_goal(wc, tcx))),
|
||||||
),
|
),
|
||||||
|
category: ProgramClauseCategory::Other,
|
||||||
};
|
};
|
||||||
tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::dummy(clause))))
|
tcx.mk_clauses(iter::once(Clause::ForAll(ty::Binder::dummy(clause))))
|
||||||
}
|
}
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue