-
Notifications
You must be signed in to change notification settings - Fork 260
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
Fix: Ability to use .Key as a constant name in datatypes and classes #4423
Conversation
@@ -6686,10 +6687,11 @@ AND Apply(f,h0,bxs) == Apply(f,h0,bxs) | |||
return predef.ArrayLength; | |||
} else if (f.EnclosingClass is ValuetypeDecl { Name: "real" } && f.Name == "Floor") { | |||
return predef.RealFloor; | |||
} else if (f is SpecialField && !(f is DatatypeDestructor)) { | |||
} else if (f is SpecialField && !(f is DatatypeDestructor || f.EnclosingClass is IndDatatypeDecl or ClassLikeDecl)) { |
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.
You're checking IndDatatypeDecl
instead of DatatypeDecl
. The latter also includes codatatype declarations. Did you intend to make this distinction? I don't quite understand the test, but perhaps you even want TopLevelDeclWithMembers
instead of IndDatatypeDecl or ClassLikeDecl
, which would then also include abstract types and newtypes. I suggest adding test cases for these, too.
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.
Interesting remark. Testing it with co-datatype did not yield any error, but opaque types and newtypes did yield errors.
However, map itself being a ValueTypeDecl, which is a TopLevelDeclWithMembers, I had to make an exclusion check, but it ended up working.
Co-authored-by: Rustan Leino <[email protected]>
…afny-lang#4423) This PR fixes dafny-lang#4394 I added the corresponding test. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Rustan Leino <[email protected]>
…4423) This PR fixes #4394 I added the corresponding test. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Rustan Leino <[email protected]>
This PR fixes #4394
I added the corresponding test.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.