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

Conversation

scalexm
Copy link
Member

@scalexm scalexm commented Mar 30, 2018

@shepmaster shepmaster added the S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. label Mar 30, 2018
Copy link
Member

@tmandry tmandry left a comment

Choose a reason for hiding this comment

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

PolyDomainGoal definitely seems like a good approach from my experience with #49435. I'll try rebasing on your branch.

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.

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

Clause::Implies(program_clause) => program_clause,
Clause::ForAll(program_clause) => program_clause.skip_binder(),
};
// Skip the top-level binder for a less verbose output
Copy link
Member

Choose a reason for hiding this comment

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

very nit, but it seems like this comment is describing the let program_clause = match ... more so than the code below it

Copy link
Member Author

Choose a reason for hiding this comment

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

Yeah definitely, I’ll fix that :)

/// 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)

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.

Did you want to fix tmandry's nit?

@scalexm
Copy link
Member Author

scalexm commented Apr 2, 2018

@nikomatsakis done ✅

@nikomatsakis
Copy link
Contributor

@bors r+

@bors
Copy link
Contributor

bors commented Apr 4, 2018

📌 Commit 1074a22 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 Apr 4, 2018
alexcrichton added a commit to alexcrichton/rust that referenced this pull request Apr 5, 2018
Chalkify - Tweak `Clause` definition and HRTBs

r? @nikomatsakis
bors added a commit that referenced this pull request Apr 5, 2018
Rollup of 8 pull requests

Successful merges:

 - #49045 (Make queries thread safe)
 - #49350 (Expand macros in `extern {}` blocks)
 - #49497 (Chalkify - Tweak `Clause` definition and HRTBs)
 - #49597 (proc_macro: Reorganize public API)
 - #49686 (typos)
- #49621
- #49697
- #49705

Failed merges:
@alexcrichton alexcrichton merged commit 1074a22 into rust-lang:master Apr 5, 2018
@scalexm scalexm deleted the hrtb branch October 22, 2018 12:20
@tmandry tmandry added the WG-traits Working group: Traits, https://internals.rust-lang.org/t/announcing-traits-working-group/6804 label May 24, 2023
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. WG-traits Working group: Traits, https://internals.rust-lang.org/t/announcing-traits-working-group/6804
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants