Stream: wg-traits

Topic: chalk #80 smarter subgoal selection


Keith Yeung (Dec 11 2018 at 06:33, on Zulip):

I'm currently looking into this issue; though I haven't really read all of the documentation about how chalk works, i _think_ i have a good enough model of how prolog works, e.g. how it recursively applies rules in order to get to the final goal and backtracks if it went to the wrong direction

Keith Yeung (Dec 11 2018 at 06:35, on Zulip):

oh, looks like i was basically describing the pursue_strand function's objective!

Keith Yeung (Dec 11 2018 at 07:59, on Zulip):

i'm thinking of replacing the Vec<Literal<C>> into a BinaryHeap<Literal<C>>, so we can have insertion sort, and we can just pop the first one off the heap

Keith Yeung (Dec 11 2018 at 08:31, on Zulip):

hmm, it looks like we need to rearchitect a couple of things too, since SelectedSubgoal stores an index to the subgoal: Vec<Literal<C>> as defined on the X-clause

Keith Yeung (Dec 11 2018 at 08:32, on Zulip):

and I instead want SelectedSubgoal to store the Literal<C> directly so it manages the ownership

Keith Yeung (Dec 11 2018 at 09:14, on Zulip):

ok, that doesn't seem easy, because there seems to be two Context type parameters that I need to be aware of: C and I

Keith Yeung (Dec 11 2018 at 09:16, on Zulip):

I need some way of converting a Literal<C> to a Literal<I>, and vice-versa

Keith Yeung (Dec 12 2018 at 19:34, on Zulip):

I'm now abandoning the idea of using a BinaryHeap, because there doesn't seem to be a clean way to interchange the Literal between contexts

nikomatsakis (Dec 13 2018 at 17:43, on Zulip):

hey @Keith Yeung =)

Keith Yeung (Dec 13 2018 at 18:03, on Zulip):

Hi

Keith Yeung (Dec 13 2018 at 18:46, on Zulip):

I instead now iterate over the vec of subgoals and use max() to determine the greatest (least amount of effort) subgoal

Keith Yeung (Dec 13 2018 at 18:47, on Zulip):

And manually implementing PartialOrd and Ord in a way that makes sense

nikomatsakis (Dec 13 2018 at 19:02, on Zulip):

I see

nikomatsakis (Dec 13 2018 at 19:02, on Zulip):

I am hoping that as we push chalk forward we'll have some "real world" data to help us out here

Keith Yeung (Dec 13 2018 at 19:36, on Zulip):

so, i have some (probably wrong) heuristics for this:

Keith Yeung (Dec 13 2018 at 19:38, on Zulip):

looking at the variants of the Goal enum, I've put CannotProve as the greatest, because there is basically no calculation involved with that goal

Keith Yeung (Dec 13 2018 at 19:41, on Zulip):

then it's Leaf > Not > Quantified > And > Implies

Keith Yeung (Dec 13 2018 at 19:41, on Zulip):

the way i reached this order is just by counting the number of goals that each variant contains

Keith Yeung (Dec 13 2018 at 19:43, on Zulip):

that perhaps may not be the best way, and we might want to reorder And, Not and Quantified to be higher if the operation to separate them into individual Leaf goals is not that expensive

Keith Yeung (Dec 13 2018 at 19:43, on Zulip):

i do however think there should be an extensive way of ordering the Leaf goals

Keith Yeung (Dec 17 2018 at 02:07, on Zulip):

opened a PR here https://github.com/rust-lang-nursery/chalk/pull/193

Keith Yeung (Dec 17 2018 at 02:07, on Zulip):

i'd still like to know if there's a way to benchmark these changes

nikomatsakis (Dec 17 2018 at 15:30, on Zulip):

cool

Keith Yeung (Jan 08 2019 at 22:10, on Zulip):

@nikomatsakis I believe you mentioned that you want to try a different approach instead?

nikomatsakis (Jan 14 2019 at 19:41, on Zulip):

@Keith Yeung yeah sorry I didn't get back to you

nikomatsakis (Jan 14 2019 at 19:41, on Zulip):

maybe we can chat about this in a bit more depth after the meeting? (e.g., in ~20 minutes, or whenever that comes?) turns out my usual call in that slot got canceled

Keith Yeung (Jan 14 2019 at 19:45, on Zulip):

sure thing, i should still be available

nikomatsakis (Jan 14 2019 at 19:59, on Zulip):

OK @Keith Yeung

nikomatsakis (Jan 14 2019 at 19:59, on Zulip):

first off left me review the PR :)

nikomatsakis (Jan 14 2019 at 19:59, on Zulip):

Ah, right, so if I recall the PR worked by giving things an order

nikomatsakis (Jan 14 2019 at 19:59, on Zulip):

but I'd sort of prefer to make this more customizable

nikomatsakis (Jan 14 2019 at 20:01, on Zulip):

one simple option would be to add a callback that can be used here, when selecting the subgoal_index

nikomatsakis (Jan 14 2019 at 20:01, on Zulip):

something that takes &strand.ex_clause and returns a subgoal index

Keith Yeung (Jan 14 2019 at 20:01, on Zulip):

i briefly entertained the idea of giving subgoals a score

nikomatsakis (Jan 14 2019 at 20:02, on Zulip):

it seems like it's not necessary for us to be able to independently decide the priority of a subgoal without reference to other subgoals

Keith Yeung (Jan 14 2019 at 20:02, on Zulip):

but that scoring system can quickly become really complex

nikomatsakis (Jan 14 2019 at 20:02, on Zulip):

we basically just want to know "what to do next"

nikomatsakis (Jan 14 2019 at 20:02, on Zulip):

although in fact I imagine that the implementations often will have a fixed scheme

nikomatsakis (Jan 14 2019 at 20:03, on Zulip):

i.e., I think that rustc will deprioritize certain traits and built-in impls and things, particularly when there are unresolved inference variables within

Keith Yeung (Jan 14 2019 at 20:03, on Zulip):

hmm... looks like we need a way to peek deeply into the structure of a subgoal

nikomatsakis (Jan 14 2019 at 20:04, on Zulip):

hmm

nikomatsakis (Jan 14 2019 at 20:05, on Zulip):

well

nikomatsakis (Jan 14 2019 at 20:05, on Zulip):

I think the context will know all the types it needs

nikomatsakis (Jan 14 2019 at 20:05, on Zulip):

that is, we will be giving it a ExClause

nikomatsakis (Jan 14 2019 at 20:06, on Zulip):

the subgoals therein are a list of Literal

nikomatsakis (Jan 14 2019 at 20:06, on Zulip):
pub enum Literal<C: Context> {
    // FIXME: pub b/c fold
    Positive(C::GoalInEnvironment),
    Negative(C::GoalInEnvironment),
}
nikomatsakis (Jan 14 2019 at 20:06, on Zulip):

looks like I intended for this stuff to be private, but it ain't

nikomatsakis (Jan 14 2019 at 20:06, on Zulip):

anyway, the C::GoalInEnvironment is something that the context knows

nikomatsakis (Jan 14 2019 at 20:07, on Zulip):

e.g., here is the definition in rustc

nikomatsakis (Jan 14 2019 at 20:07, on Zulip):

so it ought to be able to figure out which thing it wants to pick

Keith Yeung (Jan 14 2019 at 20:08, on Zulip):

i see, looks like we need some more helper methods/functions in the Context to let us decide what should be evaluated next

Keith Yeung (Jan 14 2019 at 20:09, on Zulip):

rather than having the bulk of the logic placed in logic.rs

nikomatsakis (Jan 14 2019 at 20:12, on Zulip):

I think .. probably just one method

nikomatsakis (Jan 14 2019 at 20:12, on Zulip):

but that is what I had in mind, yeah

nikomatsakis (Jan 14 2019 at 20:12, on Zulip):

I'm trying to decide in which trait it belongs =)

nikomatsakis (Jan 14 2019 at 20:14, on Zulip):

I think either probably the InferenceTable trait

nikomatsakis (Jan 14 2019 at 20:14, on Zulip):

or else a new trait analogous to TruncateOps and UnificationOps

nikomatsakis (Jan 14 2019 at 20:14, on Zulip):

i.e., SelectionOps

nikomatsakis (Jan 14 2019 at 20:18, on Zulip):

@Keith Yeung summarized here

nikomatsakis (Jan 14 2019 at 20:18, on Zulip):

sound good?

nikomatsakis (Jan 14 2019 at 20:18, on Zulip):

Once this lands, next step will be to configure the rustc side :)

Keith Yeung (Jan 14 2019 at 20:19, on Zulip):

yeah, let's see what i can come up with

Last update: Nov 18 2019 at 01:00UTC