-
Notifications
You must be signed in to change notification settings - Fork 90
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
Recursive priorities (or push-priorities, or leafy priorities) #845
Conversation
7d6c1d1
to
bce64ac
Compare
Add operators to push merge priorities down to the values inside a record in lazy and recursive manner, as initially proposed in the RFC001 on overriding. This PR adds the syntax `| _push_default` and `| _push_force` to metavalues as a temporary, ugly-on-purpose keyword such that bikeshedding can happen later and doesn't block the technical implementation.
bce64ac
to
10fa531
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this looks good, with the obvious caveat that I'm still very new to the codebase. I left some small comments, but neither needs to block the PR.
/// Presence of an annotation `push force` | ||
pub push_force: bool, | ||
/// Presence of an annotation `push default` | ||
pub push_default: bool, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Does it ever make sense for a value to be annotated with both _push_force
and _push_default
? If not, I'm wondering if it could make more sense to model this in a way where it's not possible for both to be true
at the same time, e.g.
pub push_prio: Option<PushPriority>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's indeed fishy semantically, but the thing is that nothing currently prevents the user from doing so:
x | _push_default | _push_force = ...
because annotations are just parsed one by one and combined. In some sense, you can see ExtdAnnot
as an AST for meta-annotation, and the source syntax does allow both to be set, just as they were flags. Once it's actually transformed into a term by attach()
, it does have to chose an actual push_prio
to use.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks ok to me. I second Matthew's comments though.
Closes #279. Implement push priority operators as described in RFC001. The general idea is that:
is equivalent to
The push priority operators are dynamic and not just syntactic sugar. They operate on arbitrary expressions and are thus not limited to record literals. The syntax
_push_default
and_push_force
is temporary (and ugly on purpose), to proceed with the technical implementation without being blocked by bikeshedding considerations, which can happen after, prior to the next release.