Skip to content

Commit

Permalink
Fix formatting of var by statements (#5927)
Browse files Browse the repository at this point in the history
### Description
- Fix formatting of var by statements

### How has this been tested?
- Added a XUnit 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>
  • Loading branch information
keyboardDrummer authored Nov 22, 2024
1 parent 0becbbf commit 7cab063
Show file tree
Hide file tree
Showing 4 changed files with 39 additions and 5 deletions.
9 changes: 8 additions & 1 deletion Source/DafnyCore/AST/Statements/BlockByProofStmt.cs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,8 @@

namespace Microsoft.Dafny;

public class BlockByProofStmt : Statement, ICanResolveNewAndOld, ICanPrint, ICloneable<Statement> {
public class BlockByProofStmt : Statement, ICanResolveNewAndOld, ICanPrint,
ICloneable<Statement>, ICanFormat {

public Statement Body { get; }
public BlockStmt Proof { get; }
Expand Down Expand Up @@ -59,4 +60,10 @@ public override void ResolveGhostness(ModuleResolver resolver, ErrorReporter rep

Proof.ResolveGhostness(resolver, reporter, true, codeContext, "a by block", allowAssumptionVariables, inConstructorInitializationPhase);
}

public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
formatter.SetStatementIndentation(Body);
Proof.SetIndent(indentBefore, formatter);
return false;
}
}
8 changes: 4 additions & 4 deletions Source/DafnyCore/AST/Statements/BlockStmt.cs
Original file line number Diff line number Diff line change
Expand Up @@ -61,12 +61,12 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
}
}

foreach (var blockStmtBody in Body) {
if (blockStmtBody is not BlockStmt && OwnedTokens.Any()) {
formatter.SetIndentations(blockStmtBody.StartToken, innerBlockIndent, innerBlockIndent);
foreach (var childStatement in Body) {
if (childStatement is not BlockStmt or BlockByProofStmt && OwnedTokens.Any()) {
formatter.SetIndentations(childStatement.StartToken, innerBlockIndent, innerBlockIndent);
}

formatter.Visit(blockStmtBody, indentBefore + formatter.SpaceTab);
formatter.Visit(childStatement, indentBefore + formatter.SpaceTab);
}

return false;
Expand Down
26 changes: 26 additions & 0 deletions Source/DafnyPipeline.Test/FormatterForStatements.cs
Original file line number Diff line number Diff line change
Expand Up @@ -232,6 +232,32 @@ modify ... {
");
}

[Fact]
public async Task FormatterWorksForReveal() {
await FormatterWorksFor(@"
method Foo() {
var x := 3 by {
reveal p.q;
}
x := 4 by {
reveal p.q;
}
match foo {
case Some(x) => {
reveal x.y;
a := b(
c,
d
);
}
case None => {
a := e;
}
}
}
");
}

[Fact]
public async Task FormatterWorksForDividedBlockStmt() {
await FormatterWorksFor(@"
Expand Down
1 change: 1 addition & 0 deletions docs/dev/news/5927.fix
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Fix formatting of var by statements

0 comments on commit 7cab063

Please sign in to comment.