Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Chalkify - Tweak Clause definition and HRTBs #49497

Merged
merged 2 commits into from
Apr 5, 2018
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 7 additions & 5 deletions src/librustc/ich/impls_ty.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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>,
Expand All @@ -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),
}
}
Expand Down
35 changes: 28 additions & 7 deletions src/librustc/traits/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -294,20 +296,39 @@ 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()))
),
}
}
}

/// This matches the definition from Page 7 of "A Proof Procedure for the Logic of Hereditary
/// 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).
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for this!

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(Actually @nikomatsakis’s comment from his chalkify-engine branch :p)

#[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>>;
Expand Down
42 changes: 26 additions & 16 deletions src/librustc/traits/structural_impls.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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())
Expand Down Expand Up @@ -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),
}
}
52 changes: 27 additions & 25 deletions src/librustc_traits/lowering.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down Expand Up @@ -61,36 +61,27 @@ 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 {
Trait(predicate) => predicate.lower(),
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(..) |
Expand Down Expand Up @@ -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))])
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This could still be a Clause::Implies, no?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In chalk, clauses which come from the program are always fully quantified so as to account for generic parameters, e.g.:

impl<T> Foo for T {}

would lower to the following clause:

forall<T> { T: Foo }

In rustc, there is no concept of « quantified by type », only by lifetime (and quantification by lifetime is only used for higher ranked types like in for<‘a> fn(&’a i32)).

So the binder in front of the clause is indeed not useful for the moment, but you can view it as just a placeholder until rustc binders are reworked in order to account for types.

}

fn program_clauses_for_impl<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>, def_id: DefId)
Expand All @@ -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))])
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also could be Clause::Implies

}

pub fn dump_program_clauses<'a, 'tcx>(tcx: TyCtxt<'a, 'tcx, 'tcx>) {
Expand All @@ -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();
}
}
}
Expand Down