From 71dc1626bddc9c966156cd8894d91845bc9aab9f Mon Sep 17 00:00:00 2001 From: scalexm Date: Wed, 28 Mar 2018 14:13:08 +0200 Subject: [PATCH 1/2] Tweak `Clause` definition and HRTBs --- src/librustc/ich/impls_ty.rs | 12 +++--- src/librustc/traits/mod.rs | 35 +++++++++++++---- src/librustc/traits/structural_impls.rs | 42 ++++++++++++-------- src/librustc_traits/lowering.rs | 52 +++++++++++++------------ 4 files changed, 88 insertions(+), 53 deletions(-) diff --git a/src/librustc/ich/impls_ty.rs b/src/librustc/ich/impls_ty.rs index 9a442e0529938..dfc64dfdb27e9 100644 --- a/src/librustc/ich/impls_ty.rs +++ b/src/librustc/ich/impls_ty.rs @@ -1392,6 +1392,12 @@ impl<'a, 'tcx> HashStable> for traits::Goal<'tcx> { } } +impl_stable_hash_for!( + impl<'tcx> for struct traits::ProgramClause<'tcx> { + goal, hypotheses + } +); + impl<'a, 'tcx> HashStable> for traits::Clause<'tcx> { fn hash_stable(&self, hcx: &mut StableHashingContext<'a>, @@ -1400,11 +1406,7 @@ impl<'a, 'tcx> HashStable> 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), } } diff --git a/src/librustc/traits/mod.rs b/src/librustc/traits/mod.rs index 1d5d3e41c9c9a..33930f4a59992 100644 --- a/src/librustc/traits/mod.rs +++ b/src/librustc/traits/mod.rs @@ -272,6 +272,8 @@ pub enum DomainGoal<'tcx> { TypeOutlives(ty::TypeOutlivesPredicate<'tcx>), } +pub type PolyDomainGoal<'tcx> = ty::Binder>; + #[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)] pub enum QuantifierKind { Universal, @@ -294,9 +296,15 @@ impl<'tcx> From> for Goal<'tcx> { } } -impl<'tcx> From> for Clause<'tcx> { - fn from(domain_goal: DomainGoal<'tcx>) -> Self { - Clause::DomainGoal(domain_goal) +impl<'tcx> From> 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> 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>, DomainGoal<'tcx>), - DomainGoal(DomainGoal<'tcx>), - ForAll(Box>>), + Implies(ProgramClause<'tcx>), + ForAll(ty::Binder>), +} + +/// 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>, } pub type Selection<'tcx> = Vtable<'tcx, PredicateObligation<'tcx>>; diff --git a/src/librustc/traits/structural_impls.rs b/src/librustc/traits/structural_impls.rs index d6e6f0e98adc4..865a9a34aaa25 100644 --- a/src/librustc/traits/structural_impls.rs +++ b/src/librustc/traits/structural_impls.rs @@ -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), } } diff --git a/src/librustc_traits/lowering.rs b/src/librustc_traits/lowering.rs index 1092e826a35f9..4b1983d18d6a5 100644 --- a/src/librustc_traits/lowering.rs +++ b/src/librustc_traits/lowering.rs @@ -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> 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))` 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`. -/// -/// 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> for ty::Binder - where T: Lower> + ty::fold::TypeFoldable<'tcx> + Copy +impl<'tcx, T> Lower> for ty::Binder + where T: Lower> + 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> for ty::Predicate<'tcx> { - fn lower(&self) -> Goal<'tcx> { +impl<'tcx> Lower> for ty::Predicate<'tcx> { + fn lower(&self) -> PolyDomainGoal<'tcx> { use rustc::ty::Predicate::*; match self { @@ -90,7 +81,7 @@ impl<'tcx> Lower> 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)` - let from_env = Goal::DomainGoal(DomainGoal::FromEnv(trait_pred.lower())); + let from_env = DomainGoal::FromEnv(trait_pred.lower()).into(); // `Implemented(Self: Trait)` let impl_trait = DomainGoal::Holds(WhereClauseAtom::Implemented(trait_pred)); // `Implemented(Self: Trait) :- FromEnv(Self: Trait)` - 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) :- 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(); + let program_clause = match clause { + Clause::Implies(program_clause) => program_clause, + Clause::ForAll(program_clause) => program_clause.skip_binder(), + }; + // Skip the top-level binder for a less verbose output + self.tcx.sess.struct_span_err(attr.span, &format!("{}", program_clause)).emit(); } } } From 1074a22905c6c96f2b7013073510d5f57a555436 Mon Sep 17 00:00:00 2001 From: Alexandre Martin Date: Mon, 2 Apr 2018 22:25:22 +0200 Subject: [PATCH 2/2] Fix comment --- src/librustc_traits/lowering.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/librustc_traits/lowering.rs b/src/librustc_traits/lowering.rs index 4b1983d18d6a5..153b2e730337d 100644 --- a/src/librustc_traits/lowering.rs +++ b/src/librustc_traits/lowering.rs @@ -188,11 +188,11 @@ impl<'a, 'tcx> ClauseDumper<'a, 'tcx > { if attr.check_name("rustc_dump_program_clauses") { let clauses = self.tcx.program_clauses_for(def_id); for clause in &*clauses { + // 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(), }; - // Skip the top-level binder for a less verbose output self.tcx.sess.struct_span_err(attr.span, &format!("{}", program_clause)).emit(); } }