-
Notifications
You must be signed in to change notification settings - Fork 254
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
No flatten for most backends #5528
Merged
keyboardDrummer
merged 46 commits into
dafny-lang:master
from
keyboardDrummer:noFlattenForAllBackends
Jun 5, 2024
Merged
Changes from 1 commit
Commits
Show all changes
46 commits
Select commit
Hold shift + click to select a range
97d81e2
Add patterns/codeSize test
keyboardDrummer e77441a
Update codeSize test
keyboardDrummer 547317f
Split off statement part from SPCG
keyboardDrummer 55b4cde
Draft of nested match compiler
keyboardDrummer b4bc5cf
Save
keyboardDrummer f10aa78
Generated code looks good upon visual inspection
keyboardDrummer ee9ae6f
Generated code compiles and runs
keyboardDrummer 069dddb
Move NestedMatch generation to just C#
keyboardDrummer da513a0
Attempt at implementation for expressions
keyboardDrummer 88536c8
Ran formatter
keyboardDrummer f13be6e
Fixes
keyboardDrummer a61d607
Update C# code generator zo it also uses custom generation for nested…
keyboardDrummer 846ad62
Regen GeneratedFromDafny code
keyboardDrummer 85c1b20
Revert "Regen GeneratedFromDafny code"
keyboardDrummer 3660a37
Fix gen
keyboardDrummer 26000a5
Fixes for generics
keyboardDrummer 2805584
Update generated files
keyboardDrummer 09f39f8
Merge branch 'master' into noFlattenForCSharp
keyboardDrummer 82a5d71
Fix bug related to disjoint patterns
keyboardDrummer c32be6f
Merge branch 'noFlattenForCSharp' of github.com:keyboardDrummer/dafny…
keyboardDrummer 861cee7
Merge remote-tracking branch 'origin/master' into noFlattenForCSharp
keyboardDrummer 1e25d7b
Fix literal pattern bug
keyboardDrummer 6791e43
Remove DatatypeWrapperEraser.IsErasableDatatypeWrapper check
keyboardDrummer eedcf47
Ran formatter
keyboardDrummer 6f981ab
Fix bug in disjunctive assignments
keyboardDrummer 0bd8c0d
Merge branch 'master' into noFlattenForCSharp
keyboardDrummer 903f2bf
Trigger CI
keyboardDrummer 5d9dc07
Merge branch 'noFlattenForCSharp' of github.com:keyboardDrummer/dafny…
keyboardDrummer 9477c6f
Fixes
keyboardDrummer b919fa8
Refactoring
keyboardDrummer c6de95b
Add force integration tests code
keyboardDrummer 0672492
Merge branch 'master' into noFlattenForCSharp
keyboardDrummer 3c86dd7
Convert if else chains to switch
keyboardDrummer e45420a
Merge commit 'a748799eef1d7~1' into noFlattenForCSharp
keyboardDrummer b8de307
Merge commit 'a748799eef1d7' into noFlattenForCSharp
keyboardDrummer f97bf09
Merge remote-tracking branch 'origin/master' into noFlattenForCSharp
keyboardDrummer 75bb47e
Ran formatter
keyboardDrummer e1bb707
Refactoring
keyboardDrummer dbcb4a4
Further refactoring
keyboardDrummer 420a13b
Further refactoring
keyboardDrummer 5f860c9
Attempt at using nested matches for all backends
keyboardDrummer 808d090
Use flattened matches for DafnyCodeGenerator
keyboardDrummer 126344a
Reintroduce flattening for Java
keyboardDrummer a1011f7
Fixes
keyboardDrummer 387b35f
Remove codeSize test
keyboardDrummer 49e0c55
Update expect files
keyboardDrummer File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Ran formatter
- Loading branch information
commit 88536c86b1bbaff45414fd287553b626f1dbb5d9
There are no files selected for viewing
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
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
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
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -17,7 +17,7 @@ | |
using static Microsoft.Dafny.GeneratorErrors; | ||
|
||
namespace Microsoft.Dafny.Compilers { | ||
public abstract partial class SinglePassCodeGenerator { | ||
public abstract partial class SinglePassCodeGenerator { | ||
protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts = null) { | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Applied a resharper refactoring to turn the if's into a switch statement. No actual changes to this method except for NestedMatchStmt, which now calls into a method. |
||
Contract.Requires(stmt != null); | ||
Contract.Requires(wr != null); | ||
|
@@ -442,8 +442,7 @@ public abstract partial class SinglePassCodeGenerator { | |
} | ||
} | ||
|
||
private void EmitMatchStmt(ConcreteSyntaxTree wr, MatchStmt s) | ||
{ | ||
private void EmitMatchStmt(ConcreteSyntaxTree wr, MatchStmt s) { | ||
// Type source = e; | ||
// if (source.is_Ctor0) { | ||
// FormalType f0 = ((Dt_Ctor0)source._D).a0; | ||
|
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
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
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.
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.
Applied a resharper refactoring to turn the if's into a switch statement. No actual changes to this method except for NestedMatchExpr, which now calls into a method.