-
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
Do not flatten matches for C# #5509
Closed
keyboardDrummer
wants to merge
42
commits into
dafny-lang:master
from
keyboardDrummer:noFlattenForCSharp
Closed
Do not flatten matches for C# #5509
keyboardDrummer
wants to merge
42
commits into
dafny-lang:master
from
keyboardDrummer:noFlattenForCSharp
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
… match expressions in an expression context
keyboardDrummer
added
the
run-integration-tests
Forces running the CI for integration tests even if the deep tests fail
label
Jun 3, 2024
keyboardDrummer
added a commit
that referenced
this pull request
Jun 4, 2024
### Description - Split off parts of single pass compiler, which is the refactoring part of #5509 ### How has this been tested? - No additional testing needed <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>
Closing in favor of #5528 |
auto-merge was automatically disabled
June 5, 2024 15:04
Pull request was closed
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
run-integration-tests
Forces running the CI for integration tests even if the deep tests fail
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.
Description
Do not flatten matches for C#. Such flattening can cause the generated code size to be the square of the input code size. Removing the flattening leads to a huge decrease in the size of the generated C# code inside the Dafny codebase. It goes from ~14K lines to ~7K.
The compilation of nested matches is done as follows:
Is roughly compiled into
Caveats
Maintainability
The approach taken to compile unflattened matches is one that could be applied generally, across all compilers, but it was slightly simpler to only apply it to C#, so I've done that for now.
Ideally the transformation would be a Dafny-to-Dafny source transformation, instead of a customization of SinglePassCompiler. However, Dafny does not allow using statements in expression contexts, and this is needed for the transformation. I think it would be good to have an intermediate Dafny that does allow this, similar to what @cpitclaudel 's Dafny-in-Dafny compiler allowed, and then to define the rewrite that this PR introduces using a Dafny source translation.
Improvement
For C# we could generate much nicer code, since C# allows declaring new variables inside expressions using
x is T xAsType
expressions. We could get rid of the nestedif
statements and theunmatched
variable. However, I'll leave this for future work.How has this been tested?
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.