Fix: Reveal statements can now invoke instance functions statically #4180
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
MikaelMayer
requested changes
Jun 14, 2023
| @@ -47,6 +47,16 @@ | |||
| <Content Include="..\..\node_modules\**\*.*" LinkBase="TestFiles\LitTests\LitTest\node_modules"> | |||
| <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory> | |||
| </Content> | |||
| <Content Update="..\..\Test\git-issues\github-issue-4176.dfy"> | |||
There was a problem hiding this comment.
Please remove this change. We don't need this here, tests are discovered automatically. It was probably added by Rider.
… addition to IntegrationTests.csproj
MikaelMayer
previously approved these changes
Jun 14, 2023
There was a problem hiding this comment.
This is a great fix that surely @atomb will appreciate too ! Looking forward to the test suite passing.
|
Still two more tests failing! But you are making great progress! |
|
Oh, this is great! Requiring |
MikaelMayer
reviewed
Jun 20, 2023
There was a problem hiding this comment.
Great fine tuning to ensure all tests pass !
One last thing: it's a feature, so please add an entry in docs/dev/reveal-opaque-instance-functions.feat with a line like "It's now possible to reveal an instance function of a class by a static reveal, without the need of an object of that class"
MikaelMayer
approved these changes
Jun 20, 2023
MikaelMayer
changed the title
RustanLeino
added a commit
to RustanLeino/dafny
that referenced
this pull request
Sep 13, 2023
Evidently, this was fixed by dafny-lang#4180
RustanLeino
added a commit
that referenced
this pull request
Sep 13, 2023
Evidently, this was fixed by #4180 <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>
keyboardDrummer
pushed a commit
to keyboardDrummer/dafny
that referenced
this pull request
Sep 15, 2023
Evidently, this was fixed by dafny-lang#4180 <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>
keyboardDrummer
pushed a commit
that referenced
this pull request
Sep 15, 2023
Evidently, this was fixed by #4180 <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>
keyboardDrummer
pushed a commit
that referenced
this pull request
Sep 19, 2023
Evidently, this was fixed by #4180 <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>
keyboardDrummer
pushed a commit
that referenced
this pull request
Sep 19, 2023
Evidently, this was fixed by #4180 <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>
RustanLeino
added a commit
that referenced
this pull request
Nov 2, 2023
PR #4180 introduced the ability to `reveal` an instance function in a static context. In the recent PR #4498, this has been implemented to put the instance function itself, without a receiver argument, into an attribute. The recent PR then special-cases the resolution of that attribute. I would call that a hack. This PR mimics that hack for the new resolver. That makes `git-issue-4315.dfy` (see Issue #4315) pass with both resolvers. The hack introduced in this PR and in #4498 is not a great idea, because a use of `this` is placed into the AST in a context where there is no `this`. If (rather, when) this gets fixed, it should be fixed in both resolvers. ### How has this been tested? Test `git-issues/git-issue-4315.dfy` has been converted to run with both the old and new resolver. <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>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Fixes #4176 by making generated reveal lemmas be static.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.