work towards chalkify-ing the engine #49837

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

src/librustc_driver/driver.rs

+        time(sess,
+             "dumping chalk-like clauses",
+             || rustc_traits::lowering::dump_program_clauses(tcx));
+


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

pub fn check_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

src/librustc_traits/lowering.rs

+        );
+        mem::swap(&mut next_round, &mut last_round);
+    }
+


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> Clone for Vec<T> { ... } // Implemented(Vec<T>: Clone) :- Implemented(T: Clone) (*) fn foo<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 (*) rule let 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

src/librustc/hir/map/definitions.rs

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

src/librustc_traits/lowering.rs

+    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

pub enum Def {

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 e2f3781 Compare 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 d8c6d03 Compare 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 64c0247 Compare 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 2c5fbe2 Compare 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:master Apr 24, 2018

eddyb reviewed Dec 19, 2018

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

work towards chalkify-ing the engine #49837

work towards chalkify-ing the engine #49837

nikomatsakis commented Apr 10, 2018

nikomatsakis commented Apr 10, 2018

nikomatsakis commented Apr 10, 2018

bors commented Apr 10, 2018

scalexm Apr 10, 2018

nikomatsakis Apr 11, 2018

nikomatsakis Apr 11, 2018

scalexm Apr 10, 2018

nikomatsakis Apr 11, 2018

scalexm commented Apr 10, 2018

nikomatsakis commented Apr 11, 2018

nikomatsakis commented Apr 11, 2018

scalexm commented Apr 12, 2018

bors commented Apr 12, 2018

bors commented Apr 12, 2018

nikomatsakis commented Apr 13, 2018

bors commented Apr 13, 2018

nikomatsakis commented Apr 13, 2018

bors commented Apr 13, 2018

bors commented Apr 14, 2018

nikomatsakis commented Apr 23, 2018

bors commented Apr 23, 2018

kennytm commented Apr 24, 2018

bors commented Apr 24, 2018

bors commented Apr 24, 2018

eddyb Dec 19, 2018

eddyb Dec 19, 2018

oli-obk Dec 19, 2018

eddyb Dec 19, 2018

eddyb Dec 19, 2018

oli-obk commented Dec 19, 2018

varkor commented Dec 19, 2018

eddyb commented Jan 30, 2019

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

work towards chalkify-ing the engine #49837

work towards chalkify-ing the engine #49837

Conversation

nikomatsakis commented Apr 10, 2018

nikomatsakis commented Apr 10, 2018

nikomatsakis commented Apr 10, 2018

bors commented Apr 10, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

scalexm commented Apr 10, 2018

nikomatsakis commented Apr 11, 2018

nikomatsakis commented Apr 11, 2018

scalexm commented Apr 12, 2018

bors commented Apr 12, 2018

bors commented Apr 12, 2018

nikomatsakis commented Apr 13, 2018

bors commented Apr 13, 2018

nikomatsakis commented Apr 13, 2018

bors commented Apr 13, 2018

bors commented Apr 14, 2018

nikomatsakis commented Apr 23, 2018

bors commented Apr 23, 2018

kennytm commented Apr 24, 2018

bors commented Apr 24, 2018

bors commented Apr 24, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

oli-obk commented Dec 19, 2018

varkor commented Dec 19, 2018

eddyb commented Jan 30, 2019