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

No flatten for most backends #5528

Merged
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 May 29, 2024
e77441a
Update codeSize test
keyboardDrummer May 29, 2024
547317f
Split off statement part from SPCG
keyboardDrummer May 29, 2024
55b4cde
Draft of nested match compiler
keyboardDrummer May 30, 2024
b4bc5cf
Save
keyboardDrummer May 30, 2024
f10aa78
Generated code looks good upon visual inspection
keyboardDrummer May 30, 2024
ee9ae6f
Generated code compiles and runs
keyboardDrummer May 30, 2024
069dddb
Move NestedMatch generation to just C#
keyboardDrummer May 30, 2024
da513a0
Attempt at implementation for expressions
keyboardDrummer May 30, 2024
88536c8
Ran formatter
keyboardDrummer May 30, 2024
f13be6e
Fixes
keyboardDrummer May 30, 2024
a61d607
Update C# code generator zo it also uses custom generation for nested…
keyboardDrummer May 30, 2024
846ad62
Regen GeneratedFromDafny code
keyboardDrummer May 30, 2024
85c1b20
Revert "Regen GeneratedFromDafny code"
keyboardDrummer May 30, 2024
3660a37
Fix gen
keyboardDrummer May 30, 2024
26000a5
Fixes for generics
keyboardDrummer May 30, 2024
2805584
Update generated files
keyboardDrummer May 30, 2024
09f39f8
Merge branch 'master' into noFlattenForCSharp
keyboardDrummer May 30, 2024
82a5d71
Fix bug related to disjoint patterns
keyboardDrummer May 31, 2024
c32be6f
Merge branch 'noFlattenForCSharp' of github.com:keyboardDrummer/dafny…
keyboardDrummer May 31, 2024
861cee7
Merge remote-tracking branch 'origin/master' into noFlattenForCSharp
keyboardDrummer May 31, 2024
1e25d7b
Fix literal pattern bug
keyboardDrummer May 31, 2024
6791e43
Remove DatatypeWrapperEraser.IsErasableDatatypeWrapper check
keyboardDrummer May 31, 2024
eedcf47
Ran formatter
keyboardDrummer May 31, 2024
6f981ab
Fix bug in disjunctive assignments
keyboardDrummer May 31, 2024
0bd8c0d
Merge branch 'master' into noFlattenForCSharp
keyboardDrummer May 31, 2024
903f2bf
Trigger CI
keyboardDrummer May 31, 2024
5d9dc07
Merge branch 'noFlattenForCSharp' of github.com:keyboardDrummer/dafny…
keyboardDrummer May 31, 2024
9477c6f
Fixes
keyboardDrummer Jun 1, 2024
b919fa8
Refactoring
keyboardDrummer Jun 1, 2024
c6de95b
Add force integration tests code
keyboardDrummer Jun 3, 2024
0672492
Merge branch 'master' into noFlattenForCSharp
keyboardDrummer Jun 4, 2024
3c86dd7
Convert if else chains to switch
keyboardDrummer Jun 4, 2024
e45420a
Merge commit 'a748799eef1d7~1' into noFlattenForCSharp
keyboardDrummer Jun 5, 2024
b8de307
Merge commit 'a748799eef1d7' into noFlattenForCSharp
keyboardDrummer Jun 5, 2024
f97bf09
Merge remote-tracking branch 'origin/master' into noFlattenForCSharp
keyboardDrummer Jun 5, 2024
75bb47e
Ran formatter
keyboardDrummer Jun 5, 2024
e1bb707
Refactoring
keyboardDrummer Jun 5, 2024
dbcb4a4
Further refactoring
keyboardDrummer Jun 5, 2024
420a13b
Further refactoring
keyboardDrummer Jun 5, 2024
5f860c9
Attempt at using nested matches for all backends
keyboardDrummer Jun 5, 2024
808d090
Use flattened matches for DafnyCodeGenerator
keyboardDrummer Jun 5, 2024
126344a
Reintroduce flattening for Java
keyboardDrummer Jun 5, 2024
a1011f7
Fixes
keyboardDrummer Jun 5, 2024
387b35f
Remove codeSize test
keyboardDrummer Jun 5, 2024
49e0c55
Update expect files
keyboardDrummer Jun 5, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Reintroduce flattening for Java
  • Loading branch information
keyboardDrummer committed Jun 5, 2024
commit 126344a91f64b8f361ba744efe660ee9f8883824
14 changes: 14 additions & 0 deletions Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -4322,5 +4322,19 @@ protected class ClassWriter : IClassWriter {
catchBlock.WriteLine($"dafny.DafnySequence<Character> {haltMessageVarName} = dafny.DafnySequence.asString(e.getMessage());");
TrStmt(recoveryBody, catchBlock);
}

protected override void EmitNestedMatchExpr(NestedMatchExpr match, bool inLetExprBody, ConcreteSyntaxTree output,
ConcreteSyntaxTree wStmts) {
EmitExpr(match.Flattened, inLetExprBody, output, wStmts);
}

protected override void TrOptNestedMatchExpr(NestedMatchExpr match, Type resultType, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts,
bool inLetExprBody, IVariable accumulatorVar) {
TrExprOpt(match.Flattened, resultType, wr, wStmts, inLetExprBody, accumulatorVar);
}

protected override void EmitNestedMatchStmt(NestedMatchStmt match, ConcreteSyntaxTree writer) {
TrStmt(match.Flattened, writer);
}
}
}
Loading