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

handle numeric fields in struct syntax #949

Merged
merged 3 commits into from
Jan 14, 2024
Merged

Conversation

tjhance
Copy link
Collaborator

@tjhance tjhance commented Dec 27, 2023

Did you know you can do:

enum Foo {
    Bar(u32, u32),
    Qux,
}

fn test() {
    let b = Foo::Bar { 1: 30, 0: 20 };
    assert(b.get_Bar_0() == 20);
    assert(b.get_Bar_1() == 30);
}

Well, I didn't! I only realized it because rustc's internal de-sugaring of '?' generates code that uses this form. Then I checked, and it turns out users can write it this way too. This PR handles the numeric identifiers correctly (previously, Verus would panic because it didn't translate the to VIR correctly).

VIR previously had this note for struct-syntax patterns and struct-syntax constructors:

/// For tuple-style variants, the field initializers appear in order and are named "_0", "_1", etc.
/// For struct-style variants, the field initializers may appear in any order.

The "appear in order" part is no longer true as of this PR. It seems nobody was relying on it, anyway, but it would be good for someone other than me to double-check.

fn field<S: Into<String>>(&mut self, raw_id: S) -> Id {
let raw_id = raw_id.into();
let f = || raw_id.clone();
Self::id(&mut self.rename_count, &mut self.field_to_name, IdKind::Field, &raw_id, f)
Copy link
Contributor

@utaal-b utaal-b Jan 7, 2024

Choose a reason for hiding this comment

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

Will this store the name in key_to_name even for numeric fields for which we are not going to use the rename_count in lifetime_emit? Does that matter?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Yes

Copy link
Contributor

Choose a reason for hiding this comment

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

Why is the distinction in lifetime_emit necessary?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I guess it's not necessary, now that I think about it. I guess the original reason I did it was because I didn't think it made sense to use IdKind::Local for field names.

@tjhance tjhance force-pushed the numeric-fields-in-structs branch from 17528d1 to 3a20c67 Compare January 9, 2024 18:54
@tjhance tjhance merged commit 8fdfdb8 into main Jan 14, 2024
5 checks passed
@tjhance tjhance deleted the numeric-fields-in-structs branch January 14, 2024 14:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants