Rollup merge of #49497 - scalexm:hrtb, r=nikomatsakis
Chalkify - Tweak `Clause` definition and HRTBs r? @nikomatsakis
This commit is contained in:
commit
72ac3ebf68
4 changed files with 88 additions and 53 deletions
|
@ -1392,6 +1392,12 @@ impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::Goal<'tcx> {
|
|||
}
|
||||
}
|
||||
|
||||
impl_stable_hash_for!(
|
||||
impl<'tcx> for struct traits::ProgramClause<'tcx> {
|
||||
goal, hypotheses
|
||||
}
|
||||
);
|
||||
|
||||
impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::Clause<'tcx> {
|
||||
fn hash_stable<W: StableHasherResult>(&self,
|
||||
hcx: &mut StableHashingContext<'a>,
|
||||
|
@ -1400,11 +1406,7 @@ impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::Clause<'tcx> {
|
|||
|
||||
mem::discriminant(self).hash_stable(hcx, hasher);
|
||||
match self {
|
||||
Implies(hypotheses, goal) => {
|
||||
hypotheses.hash_stable(hcx, hasher);
|
||||
goal.hash_stable(hcx, hasher);
|
||||
}
|
||||
DomainGoal(domain_goal) => domain_goal.hash_stable(hcx, hasher),
|
||||
Implies(clause) => clause.hash_stable(hcx, hasher),
|
||||
ForAll(clause) => clause.hash_stable(hcx, hasher),
|
||||
}
|
||||
}
|
||||
|
|
|
@ -272,6 +272,8 @@ pub enum DomainGoal<'tcx> {
|
|||
TypeOutlives(ty::TypeOutlivesPredicate<'tcx>),
|
||||
}
|
||||
|
||||
pub type PolyDomainGoal<'tcx> = ty::Binder<DomainGoal<'tcx>>;
|
||||
|
||||
#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
|
||||
pub enum QuantifierKind {
|
||||
Universal,
|
||||
|
@ -294,9 +296,15 @@ impl<'tcx> From<DomainGoal<'tcx>> for Goal<'tcx> {
|
|||
}
|
||||
}
|
||||
|
||||
impl<'tcx> From<DomainGoal<'tcx>> for Clause<'tcx> {
|
||||
fn from(domain_goal: DomainGoal<'tcx>) -> Self {
|
||||
Clause::DomainGoal(domain_goal)
|
||||
impl<'tcx> From<PolyDomainGoal<'tcx>> for Goal<'tcx> {
|
||||
fn from(domain_goal: PolyDomainGoal<'tcx>) -> Self {
|
||||
match domain_goal.no_late_bound_regions() {
|
||||
Some(p) => p.into(),
|
||||
None => Goal::Quantified(
|
||||
QuantifierKind::Universal,
|
||||
Box::new(domain_goal.map_bound(|p| p.into()))
|
||||
),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -304,10 +312,23 @@ impl<'tcx> From<DomainGoal<'tcx>> for Clause<'tcx> {
|
|||
/// Harrop Formulas".
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
|
||||
pub enum Clause<'tcx> {
|
||||
// FIXME: again, use interned refs instead of `Box`
|
||||
Implies(Vec<Goal<'tcx>>, DomainGoal<'tcx>),
|
||||
DomainGoal(DomainGoal<'tcx>),
|
||||
ForAll(Box<ty::Binder<Clause<'tcx>>>),
|
||||
Implies(ProgramClause<'tcx>),
|
||||
ForAll(ty::Binder<ProgramClause<'tcx>>),
|
||||
}
|
||||
|
||||
/// A "program clause" has the form `D :- G1, ..., Gn`. It is saying
|
||||
/// that the domain goal `D` is true if `G1...Gn` are provable. This
|
||||
/// is equivalent to the implication `G1..Gn => D`; we usually write
|
||||
/// it with the reverse implication operator `:-` to emphasize the way
|
||||
/// that programs are actually solved (via backchaining, which starts
|
||||
/// with the goal to solve and proceeds from there).
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
|
||||
pub struct ProgramClause<'tcx> {
|
||||
/// This goal will be considered true...
|
||||
pub goal: DomainGoal<'tcx>,
|
||||
|
||||
/// ...if we can prove these hypotheses (there may be no hypotheses at all):
|
||||
pub hypotheses: Vec<Goal<'tcx>>,
|
||||
}
|
||||
|
||||
pub type Selection<'tcx> = Vtable<'tcx, PredicateObligation<'tcx>>;
|
||||
|
|
|
@ -493,25 +493,29 @@ impl<'tcx> fmt::Display for traits::Goal<'tcx> {
|
|||
}
|
||||
}
|
||||
|
||||
impl<'tcx> fmt::Display for traits::ProgramClause<'tcx> {
|
||||
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
|
||||
let traits::ProgramClause { goal, hypotheses } = self;
|
||||
write!(fmt, "{}", goal)?;
|
||||
if !hypotheses.is_empty() {
|
||||
write!(fmt, " :- ")?;
|
||||
for (index, condition) in hypotheses.iter().enumerate() {
|
||||
if index > 0 {
|
||||
write!(fmt, ", ")?;
|
||||
}
|
||||
write!(fmt, "{}", condition)?;
|
||||
}
|
||||
}
|
||||
write!(fmt, ".")
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> fmt::Display for traits::Clause<'tcx> {
|
||||
fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
|
||||
use traits::Clause::*;
|
||||
|
||||
match self {
|
||||
Implies(hypotheses, goal) => {
|
||||
write!(fmt, "{}", goal)?;
|
||||
if !hypotheses.is_empty() {
|
||||
write!(fmt, " :- ")?;
|
||||
for (index, condition) in hypotheses.iter().enumerate() {
|
||||
if index > 0 {
|
||||
write!(fmt, ", ")?;
|
||||
}
|
||||
write!(fmt, "{}", condition)?;
|
||||
}
|
||||
}
|
||||
write!(fmt, ".")
|
||||
}
|
||||
DomainGoal(domain_goal) => write!(fmt, "{}.", domain_goal),
|
||||
Implies(clause) => write!(fmt, "{}", clause),
|
||||
ForAll(clause) => {
|
||||
// FIXME: appropriate binder names
|
||||
write!(fmt, "forall<> {{ {} }}", clause.skip_binder())
|
||||
|
@ -553,10 +557,16 @@ EnumTypeFoldableImpl! {
|
|||
}
|
||||
}
|
||||
|
||||
BraceStructTypeFoldableImpl! {
|
||||
impl<'tcx> TypeFoldable<'tcx> for traits::ProgramClause<'tcx> {
|
||||
goal,
|
||||
hypotheses
|
||||
}
|
||||
}
|
||||
|
||||
EnumTypeFoldableImpl! {
|
||||
impl<'tcx> TypeFoldable<'tcx> for traits::Clause<'tcx> {
|
||||
(traits::Clause::Implies)(hypotheses, goal),
|
||||
(traits::Clause::DomainGoal)(domain_goal),
|
||||
(traits::Clause::Implies)(clause),
|
||||
(traits::Clause::ForAll)(clause),
|
||||
}
|
||||
}
|
||||
|
|
|
@ -13,7 +13,7 @@ use rustc::hir::def_id::DefId;
|
|||
use rustc::hir::intravisit::{self, NestedVisitorMap, Visitor};
|
||||
use rustc::ty::{self, TyCtxt};
|
||||
use rustc::ty::subst::Substs;
|
||||
use rustc::traits::{QuantifierKind, Goal, DomainGoal, Clause, WhereClauseAtom};
|
||||
use rustc::traits::{WhereClauseAtom, PolyDomainGoal, DomainGoal, ProgramClause, Clause};
|
||||
use syntax::ast;
|
||||
use rustc_data_structures::sync::Lrc;
|
||||
|
||||
|
@ -61,28 +61,19 @@ impl<'tcx> Lower<DomainGoal<'tcx>> for ty::TypeOutlivesPredicate<'tcx> {
|
|||
/// `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 goals, e.g. as for the previous example:
|
||||
/// 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))>`.
|
||||
///
|
||||
/// Also, if `self` does not contain generic lifetimes, we can safely drop the binder and we
|
||||
/// can directly lower to a leaf goal instead of a quantified goal.
|
||||
impl<'tcx, T> Lower<Goal<'tcx>> for ty::Binder<T>
|
||||
where T: Lower<DomainGoal<'tcx>> + ty::fold::TypeFoldable<'tcx> + Copy
|
||||
impl<'tcx, T> Lower<PolyDomainGoal<'tcx>> for ty::Binder<T>
|
||||
where T: Lower<DomainGoal<'tcx>> + ty::fold::TypeFoldable<'tcx>
|
||||
{
|
||||
fn lower(&self) -> Goal<'tcx> {
|
||||
match self.no_late_bound_regions() {
|
||||
Some(p) => p.lower().into(),
|
||||
None => Goal::Quantified(
|
||||
QuantifierKind::Universal,
|
||||
Box::new(self.map_bound(|p| p.lower().into()))
|
||||
),
|
||||
}
|
||||
fn lower(&self) -> PolyDomainGoal<'tcx> {
|
||||
self.map_bound_ref(|p| p.lower())
|
||||
}
|
||||
}
|
||||
|
||||
impl<'tcx> Lower<Goal<'tcx>> for ty::Predicate<'tcx> {
|
||||
fn lower(&self) -> Goal<'tcx> {
|
||||
impl<'tcx> Lower<PolyDomainGoal<'tcx>> for ty::Predicate<'tcx> {
|
||||
fn lower(&self) -> PolyDomainGoal<'tcx> {
|
||||
use rustc::ty::Predicate::*;
|
||||
|
||||
match self {
|
||||
|
@ -90,7 +81,7 @@ impl<'tcx> Lower<Goal<'tcx>> for ty::Predicate<'tcx> {
|
|||
RegionOutlives(predicate) => predicate.lower(),
|
||||
TypeOutlives(predicate) => predicate.lower(),
|
||||
Projection(predicate) => predicate.lower(),
|
||||
WellFormed(ty) => DomainGoal::WellFormedTy(*ty).into(),
|
||||
WellFormed(ty) => ty::Binder::dummy(DomainGoal::WellFormedTy(*ty)),
|
||||
ObjectSafe(..) |
|
||||
ClosureKind(..) |
|
||||
Subtype(..) |
|
||||
|
@ -134,13 +125,16 @@ fn program_clauses_for_trait<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefI
|
|||
}
|
||||
};
|
||||
// `FromEnv(Self: Trait<P1..Pn>)`
|
||||
let from_env = Goal::DomainGoal(DomainGoal::FromEnv(trait_pred.lower()));
|
||||
let from_env = DomainGoal::FromEnv(trait_pred.lower()).into();
|
||||
// `Implemented(Self: Trait<P1..Pn>)`
|
||||
let impl_trait = DomainGoal::Holds(WhereClauseAtom::Implemented(trait_pred));
|
||||
|
||||
// `Implemented(Self: Trait<P1..Pn>) :- FromEnv(Self: Trait<P1..Pn>)`
|
||||
let clause = Clause::Implies(vec![from_env], impl_trait);
|
||||
Lrc::new(vec![clause])
|
||||
let clause = ProgramClause {
|
||||
goal: impl_trait,
|
||||
hypotheses: vec![from_env],
|
||||
};
|
||||
Lrc::new(vec![Clause::ForAll(ty::Binder::dummy(clause))])
|
||||
}
|
||||
|
||||
fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId)
|
||||
|
@ -167,8 +161,11 @@ fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId
|
|||
let where_clauses = tcx.predicates_of(def_id).predicates.lower();
|
||||
|
||||
// `Implemented(A0: Trait<A1..An>) :- WC`
|
||||
let clause = Clause::Implies(where_clauses, trait_pred);
|
||||
Lrc::new(vec![clause])
|
||||
let clause = ProgramClause {
|
||||
goal: trait_pred,
|
||||
hypotheses: where_clauses.into_iter().map(|wc| wc.into()).collect()
|
||||
};
|
||||
Lrc::new(vec![Clause::ForAll(ty::Binder::dummy(clause))])
|
||||
}
|
||||
|
||||
pub fn dump_program_clauses<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>) {
|
||||
|
@ -184,14 +181,19 @@ struct ClauseDumper<'a, 'tcx: 'a> {
|
|||
tcx: TyCtxt<'a, 'tcx, 'tcx>,
|
||||
}
|
||||
|
||||
impl <'a, 'tcx> ClauseDumper<'a, '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 {
|
||||
if attr.check_name("rustc_dump_program_clauses") {
|
||||
let clauses = self.tcx.program_clauses_for(def_id);
|
||||
for clause in &*clauses {
|
||||
self.tcx.sess.struct_span_err(attr.span, &format!("{}", clause)).emit();
|
||||
// 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(),
|
||||
};
|
||||
self.tcx.sess.struct_span_err(attr.span, &format!("{}", program_clause)).emit();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue