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

MVP for chalkification #48985

Merged
merged 6 commits into from
Mar 18, 2018
Merged

MVP for chalkification #48985

merged 6 commits into from
Mar 18, 2018

Conversation

scalexm
Copy link
Member

@scalexm scalexm commented Mar 13, 2018

@rust-highfive rust-highfive added the S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. label Mar 13, 2018
@bors
Copy link
Contributor

bors commented Mar 13, 2018

☔ The latest upstream changes (presumably #48411) made this pull request unmergeable. Please resolve the merge conflicts.

Copy link
Contributor

@nikomatsakis nikomatsakis left a comment

Choose a reason for hiding this comment

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

This looks awesome! I left some suggestions, mostly nits of various kinds. I'm inclined to move forward quickly and do most of our iteration in tree rather than spending too much time in this PR, so we should feel free to mark some items as "follow-up work" (e.g., giving names and comments and things).

@@ -1237,3 +1237,86 @@ for ty::UniverseIndex {
self.depth().hash_stable(hcx, hasher);
}
}

impl<'a, 'tcx> HashStable<StableHashingContext<'a>> for traits::WhereClauseAtom<'tcx> {
Copy link
Contributor

Choose a reason for hiding this comment

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

egads we should really extend the macro here

@@ -242,6 +244,59 @@ pub type Obligations<'tcx, O> = Vec<Obligation<'tcx, O>>;
pub type PredicateObligations<'tcx> = Vec<PredicateObligation<'tcx>>;
pub type TraitObligations<'tcx> = Vec<TraitObligation<'tcx>>;

#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub enum WhereClauseAtom<'tcx> {
Implemented(ty::PolyTraitPredicate<'tcx>),
Copy link
Contributor

Choose a reason for hiding this comment

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

I don't think we want poly trait predicates here. I think we want the binders to be moved out of WhereClauseAtom and into the Goal -- actually, in Chalk we get this mildly wrong, as I'll comment below.

Implies(Vec<DomainGoal<'tcx>>, Box<Goal<'tcx>>),
And(Box<Goal<'tcx>>, Box<Goal<'tcx>>),
Not(Box<Goal<'tcx>>),
Leaf(LeafGoal<'tcx>),
Copy link
Contributor

Choose a reason for hiding this comment

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

I think we should just call this DomainGoal, and forego the Leaf indirection


#[derive(Clone, PartialEq, Eq, Hash, Debug)]
pub enum Goal<'tcx> {
Implies(Vec<DomainGoal<'tcx>>, Box<Goal<'tcx>>),
Copy link
Contributor

Choose a reason for hiding this comment

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

So, this matches chalk, where we make the hypotheses a set of domain goals, but it's not as general as we could do. We really should use Clause<'tcx> here, which would match the following enum:

enum Clause<'tcx> {
    Implies(Vec<Goal<'tcx>>, DomainGoal<'tcx>),
    DomainGoal(DomainGoal<'tcx>),
    ForAll(Box<ty::Binder<Clause<'tcx>>),
}

This matches the definition from Page 7 of "A Proof Procedure for the Logic of Hereditary Harrop Formulas" pretty well. That definition is D = A | G => A | D ^ D | forall x. D -- where D is a clause, G is a goal, and A is a DomainGoal -- but we've moved the "and" case (D ^ D) into the vector. (There are broader definitions as well for clauses, but they can be normalized into this form.)

This would also entail a change to Environment to store these clauses instead of just domain goals.

The reason that this matters is that if we move the binder out of DomainGoal, we need somewhere to put it in the case of a clause!

Copy link
Contributor

Choose a reason for hiding this comment

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

Also, I think we should use interners probably, and hence make this:

type Goal<'tcx> = &'tcx GoalKind<'tcx>;
enum GoalKind<'tcx> {
    Implies(Vec<DomainGoal<'tcx>, Goal<'tcx>),
    ... // as today
}

but we can do that in a follow-up. (We should open a FIXME for it before landing.)

Copy link
Contributor

Choose a reason for hiding this comment

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

I opened rust-lang/chalk#94 to describe the change here in chalk

fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
write!(fmt, "{}", self.consequence)?;
if self.conditions.is_empty() {
write!(fmt, ".")?;
Copy link
Contributor

Choose a reason for hiding this comment

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

Total nit: let's either keep the . on both sides or drop it on both sides. =)

}
}

impl<'tcx> TypeFoldable<'tcx> for traits::WhereClauseAtom<'tcx> {
Copy link
Contributor

Choose a reason for hiding this comment

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

There are pretty decent macros for this... oh, shoot, they are in #48411 -- oh, wait, that just landed =)

You may want to adopt one of these:

rust/src/librustc/macros.rs

Lines 160 to 164 in 8c4ff22

///////////////////////////////////////////////////////////////////////////
// Lift and TypeFoldable macros
//
// When possible, use one of these (relatively) convenient macros to write
// the impls for you.


trait Foo { }

#[rustc_dump_program_clauses] //~ ERROR Implemented(T: Foo) :-
Copy link
Contributor

Choose a reason for hiding this comment

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

This is so nice =) I guess you intentionally omitted the details here? (We see them below in the stderr file...)

Copy link
Member Author

@scalexm scalexm Mar 13, 2018

Choose a reason for hiding this comment

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

Yes I skipped them here because it's a bit verbose :)

fn lower(&self) -> DomainGoal<'tcx> {
use self::Predicate::*;

match *self {
Copy link
Contributor

Choose a reason for hiding this comment

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

Nit; you don't need the *self anymore; you can add the feature(match_default_bindings) instead

let trait_ref = ty::Binder(TraitPredicate { trait_ref }).lower();
let where_clauses = tcx.predicates_of(def_id).predicates.lower();

let clause = ProgramClause {
Copy link
Contributor

Choose a reason for hiding this comment

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

Hmm. So, I think we should go through the rustc-guide reference on this topic and give names to each of these rules. Then we can reference those rules here to allow for easy cross-reference.

Copy link
Contributor

Choose a reason for hiding this comment

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

This can be done later.

use ty::{self, PolyTraitPredicate, TraitPredicate, PolyProjectionPredicate, TyCtxt, Predicate};
use super::{DomainGoal, ProgramClause, WhereClauseAtom};
use rustc_data_structures::sync::Lrc;
use syntax::ast;
Copy link
Contributor

Choose a reason for hiding this comment

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

Nit: let's move this code into librustc_traits now that #48411 has landed

@nikomatsakis
Copy link
Contributor

nikomatsakis commented Mar 13, 2018

ok so I was talking to @scalexm on gitter. We agreed that we can leave most of the changes here for later. Here is the list of thing I wrote, I think:

@nikomatsakis
Copy link
Contributor

@scalexm I'd like to review one last time tomorrow or whatever, but otherwise once nits are fixed I think we should land and then we can open up issues for follow-up work

@scalexm scalexm changed the title [WIP] MVP for chalkification MVP for chalkification Mar 14, 2018
@nikomatsakis
Copy link
Contributor

@bors r+

This is so exciting. 🎉

@bors
Copy link
Contributor

bors commented Mar 15, 2018

📌 Commit 4eaa85d has been approved by nikomatsakis

@bors bors added S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. and removed S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. labels Mar 15, 2018
if let ImplPolarity::Negative = tcx.impl_polarity(def_id) {
return Lrc::new(vec![]);
}

Copy link
Member

Choose a reason for hiding this comment

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

[00:06:08] tidy error: /checkout/src/librustc_traits/lowering.rs:120: trailing whitespace
[00:06:10] some tidy checks failed

@kennytm
Copy link
Member

kennytm commented Mar 15, 2018

@bors r-

Tidy failed.

@bors bors added S-waiting-on-author Status: This is awaiting some action (such as code changes or more information) from the author. and removed S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. labels Mar 15, 2018
@kennytm
Copy link
Member

kennytm commented Mar 15, 2018

@bors r=nikomatsakis

@bors
Copy link
Contributor

bors commented Mar 15, 2018

📌 Commit ef3b4e1 has been approved by nikomatsakis

@bors bors added S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion. and removed S-waiting-on-author Status: This is awaiting some action (such as code changes or more information) from the author. labels Mar 15, 2018
@bors
Copy link
Contributor

bors commented Mar 18, 2018

⌛ Testing commit ef3b4e1 with merge 7c396eb...

bors added a commit that referenced this pull request Mar 18, 2018
@bors
Copy link
Contributor

bors commented Mar 18, 2018

☀️ Test successful - status-appveyor, status-travis
Approved by: nikomatsakis
Pushing 7c396eb to master...

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
S-waiting-on-bors Status: Waiting on bors to run and complete tests. Bors will change the label on completion.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants