work towards chalkify-ing the engine by nikomatsakis · Pull Request #49837 · rust-lang/rust

nikomatsakis · 2018-04-10T10:02:13Z

This work towards creating a "all program clauses needed for this goal" query

r? @scalexm

nikomatsakis · 2018-04-10T10:02:48Z

D'oh, have to rebase =)

nikomatsakis · 2018-04-10T10:03:23Z

@bors delegate=scalexm

bors · 2018-04-10T10:03:24Z

✌️ @scalexm can now approve this pull request

scalexm · 2018-04-10T22:53:32Z

I must admit that when writing this code, I just put the compiler pass at the end of the function without thinking too much about it. What's the precise reason for preferring it to be placed before "death checking" etc?

ah, it's a subtle thing. when you invoke check_name to test the name of an attribute, you also implicitly mark the attribute as "used" (at least by default):
rust/src/libsyntax/attr.rs
Lines 208 to 214 in 43e994c
pubfncheck_name(&self,name:&str) -> bool{
let matches = self.path == name;
if matches {
mark_used(self);
}
matches
}
this info is then used by the "unused attribute" lint. Since we were running this pass before the lint fired, that info was not available when the unused attribute lint executed, producing lint warnings of "unused attribute" in some cases (only the new tests).

that whole scheme needs to be rewritten for the query system at some point...

scalexm · 2018-04-10T23:19:52Z

I think this is good, we should be able to retrieve all the clauses that are of interest to us. One point though, we will want to run this algorithm not only for our environment, but also for goals we want to prove, e.g.:
impl<T:Clone>CloneforVec<T>{ ... }// Implemented(Vec<T>: Clone) :- Implemented(T: Clone) (*)fnfoo<T:Clone>(a:Vec<T>){// it doesn't seem like the `T: Clone` in the environment will enable us to reach// the (*) rule above// We must prove `Implemented(Vec<T>: Clone)` here: if we run the transitive// closure algorithm for this goal, we will reach the (*) rulelet b = a.clone();}
so could we just change the name program_clauses_for_env to something more general? Like program_clauses_for_goals?

I was debating about this-- specifically, what the key for the query should be, and how we should cache this information. I was sort of assuming that there would be some higher-level procedure that was, given a goal and its environment, assembling the full set of clauses (and caching the result, no doubt). Therefore, I figured this "for-env" query would just be a small part of it.

scalexm · 2018-04-10T23:21:30Z

this is cool 👍🏻

nikomatsakis · 2018-04-11T08:24:13Z

I'll try to rebase today.

nikomatsakis · 2018-04-11T22:07:01Z

rebased

scalexm · 2018-04-12T14:41:58Z

@bors r+

bors · 2018-04-12T14:41:59Z

📌 Commit e2f3781 has been approved by scalexm

bors · 2018-04-12T19:04:07Z

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

nikomatsakis · 2018-04-13T00:22:55Z

Rebased. However, the final results look a bit funny:

error: program clause dump
--> $DIR/lower_env1.rs:18:1
|
LL | #[rustc_dump_env_program_clauses] //~ ERROR program clause dump
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= note: Implemented(Self: std::marker::Sized) :- FromEnv(Self: std::marker::Sized).
= note: Implemented(Self: Bar) :- FromEnv(Self: Bar).
= note: FromEnv(Self: Bar) :- FromEnv(Self: Bar).
= note: Implemented(Self: Foo) :- FromEnv(Self: Foo).
error: aborting due to previous error

In particular:

 = note: FromEnv(Self: Bar) :- FromEnv(Self: Bar).

but I don't think that is a problem that is due to this PR... I didn't investigate yet.

bors · 2018-04-13T15:58:18Z

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

nikomatsakis · 2018-04-13T21:48:07Z

@bors r=scalexm

bors · 2018-04-13T21:48:07Z

📌 Commit 64c0247 has been approved by scalexm

bors · 2018-04-14T16:10:20Z

⌛ Testing commit 64c0247972adfae02d6a58d08d6e57e577b310aa with merge 04de83c7b7e488cfb82d61f022588551550dcd4d...

Chalk wants to be able to pass these constraints around. Also, the form we were using in our existing queries was not as general as we are going to need.

(rather than issuing multiple errors) Also, reorder so that the annotations are considered "used" when the lint runs.

This computes the transitive closure of traits that appear in the environment and then appends their clauses. It needs some work, but it's in the right direction.

Also, introduce `Clauses` and `Goals` type alises for readability.

nikomatsakis · 2018-04-23T17:50:39Z

@bors r=scalexm

bors · 2018-04-23T17:50:40Z

📌 Commit 2c5fbe2 has been approved by scalexm

kennytm · 2018-04-24T03:58:04Z

@bors p=3

bors · 2018-04-24T08:32:59Z

⌛ Testing commit 2c5fbe2 with merge 898c9f7...

@scalexm

work towards chalkify-ing the engine This work towards creating a "all program clauses needed for this goal" query r? @scalexm

bors · 2018-04-24T10:44:16Z

☀️ Test successful - status-appveyor, status-travis
Approved by: scalexm
Pushing 898c9f7 to master...

eddyb · 2018-12-19T01:14:16Z

+ /// An associated type **declaration** (i.e., in a trait)
+ AssocTypeInTrait(InternedString),
+ /// An associated type **value** (i.e., in an impl)
+ AssocTypeInImpl(InternedString),


Why was this split done? Also, why "declaration vs value" and not "declaration vs definition"?

eddyb · 2018-12-19T01:17:01Z

+ match tcx.def_key(def_id).disambiguated_data.data {
+ DefPathData::Trait(_) => program_clauses_for_trait(tcx, def_id),
+ DefPathData::Impl => program_clauses_for_impl(tcx, def_id),
+ DefPathData::AssocTypeInImpl(..) => program_clauses_for_associated_type_value(tcx, def_id),


I'm not sure I approve of using DefPathData outside of path-specific logic.
Maybe we need a new enum that's something in between DefPathData and Def?
"DefKind" comes to mind as a possible name.
cc @oli-obk @varkor

we already have
rust/src/librustc/hir/def.rs
Line 46 in 059e6a6
pubenumDef{

By "something in between DefPathData and Def" I meant "not Def itself" - ideally, a plain enum with no DefIds.

Oh and Def should probably be renamed to Res(olution), as it's too specific to name resolution to deserve a more general name.

oli-obk · 2018-12-19T13:44:20Z

So... We could make Def a struct Def { kind: DefKind, id: Option<DefId> } ?

varkor · 2018-12-19T14:01:46Z

The variants of Def aren't quite so homogeneous (e.g. SelfTy(Option<DefId>, Option<DefId>), StructCtor(DefId, CtorKind), etc.), so I'm not sure it'd make such a clean refactoring. It would probably end up duplicating the Def enum and stripping out the unnecessary data.

eddyb · 2019-01-30T10:33:30Z

@oli-obk @varkor My preferred solution would be to have Res::Def(DefKind, DefId) (if we even want to bother with duplicating the DefKind there instead of having a map/query from DefId to DefKind)

That is, Def would become Res, it would keep all of its variants which don't just refer to definitions (in the sense of having a DefId), e.g. SelfTy, Local, etc. and gain a new Def(DefKind, DefId) variant.

rust-highfive assigned scalexm Apr 10, 2018

rust-highfive added the S-waiting-on-review Status: Awaiting review from the assignee but also interested parties. label Apr 10, 2018

scalexm reviewed Apr 10, 2018
View reviewed changes

nikomatsakis force-pushed the chalkify-engine branch from 05a7d9e to e2f3781Compare April 11, 2018 22:06

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 12, 2018

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 Apr 12, 2018

nikomatsakis force-pushed the chalkify-engine branch 2 times, most recently from a61da9a to d8c6d03Compare April 13, 2018 00:21

rust-lang deleted a comment from rust-highfive Apr 13, 2018

nikomatsakis force-pushed the chalkify-engine branch 2 times, most recently from 72869cb to 64c0247Compare April 13, 2018 20:28

rust-lang deleted a comment from rust-highfive Apr 13, 2018

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 Apr 13, 2018

nikomatsakis added 8 commits April 23, 2018 13:28

create a QueryRegionConstraint type
c8a5285
Chalk wants to be able to pass these constraints around. Also, the form we were using in our existing queries was not as general as we are going to need.

add Goal::CannotProve and extract ProgramClause struct
cfbf62f

introduce new DefPathData variants for traits, assoc types
09bd6f3

rustfmt lowering.rs
94639ca

in unit tests, use note to dump multiple program clauses
7173fd7
(rather than issuing multiple errors) Also, reorder so that the annotations are considered "used" when the lint runs.

first draft of program_clauses_for_env
294cae2
This computes the transitive closure of traits that appear in the environment and then appends their clauses. It needs some work, but it's in the right direction.

eliminate the Lrc of a slice and just return the slice
7fa3c8f
Also, introduce `Clauses` and `Goals` type alises for readability.

sort strings on output
2c5fbe2

nikomatsakis force-pushed the chalkify-engine branch from a85943c to 2c5fbe2Compare April 23, 2018 17:28

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 Apr 23, 2018

bors added a commit that referenced this pull request Apr 24, 2018
Auto merge of#49837- nikomatsakis:chalkify-engine, r=scalexm
898c9f7
work towards chalkify-ing the engine This work towards creating a "all program clauses needed for this goal" query r? @scalexm

bors mentioned this pull request Apr 24, 2018
[WIP] Move Self: Trait predicate to trait items instead of the trait itself #50183
Closed

bors merged commit 2c5fbe2 into rust-lang:masterApr 24, 2018

eddyb reviewed Dec 19, 2018
View reviewed changes

	pubfncheck_name(&self,name:&str) -> bool{
	let matches = self.path == name;
	if matches {
	mark_used(self);
	}
	matches
	}

Uh oh!

Uh oh!

Conversation

nikomatsakis commented Apr 10, 2018

Uh oh!

nikomatsakis commented Apr 10, 2018

Uh oh!

nikomatsakis commented Apr 10, 2018

Uh oh!

bors commented Apr 10, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

scalexm commented Apr 10, 2018

Uh oh!

nikomatsakis commented Apr 11, 2018

Uh oh!

nikomatsakis commented Apr 11, 2018

Uh oh!

scalexm commented Apr 12, 2018

Uh oh!

bors commented Apr 12, 2018

Uh oh!

bors commented Apr 12, 2018

Uh oh!

nikomatsakis commented Apr 13, 2018

Uh oh!

bors commented Apr 13, 2018

Uh oh!

nikomatsakis commented Apr 13, 2018

Uh oh!

bors commented Apr 13, 2018

Uh oh!

bors commented Apr 14, 2018

Uh oh!

nikomatsakis commented Apr 23, 2018

Uh oh!

bors commented Apr 23, 2018

Uh oh!

kennytm commented Apr 24, 2018

Uh oh!

bors commented Apr 24, 2018

Uh oh!

bors commented Apr 24, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

oli-obk commented Dec 19, 2018

Uh oh!

varkor commented Dec 19, 2018

Uh oh!

eddyb commented Jan 30, 2019

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants