From 561a0476201bb03b7d0049795db8a6baf4936f7e Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 27 Apr 2023 13:21:08 -0500 Subject: [PATCH 1/3] Fix: Format for comprehension expressions --- .../AST/Expressions/ComprehensionExpr.cs | 1 + .../DafnyCore/AST/Expressions/Expressions.cs | 33 +++++++- Source/DafnyPipeline.Test/FormatterIssues.cs | 77 +++++++++++++++++++ docs/dev/news/3912.fix | 1 + 4 files changed, 111 insertions(+), 1 deletion(-) create mode 100644 docs/dev/news/3912.fix diff --git a/Source/DafnyCore/AST/Expressions/ComprehensionExpr.cs b/Source/DafnyCore/AST/Expressions/ComprehensionExpr.cs index deac60672cc..d509d13cec1 100644 --- a/Source/DafnyCore/AST/Expressions/ComprehensionExpr.cs +++ b/Source/DafnyCore/AST/Expressions/ComprehensionExpr.cs @@ -473,6 +473,7 @@ public virtual bool SetIndent(int indentBefore, TokenNewIndentCollector formatte indentBefore = formatter.ReduceBlockiness ? indentBefore : formatter.GetNewTokenVisualIndent(token, indentBefore); assignOpIndent = formatter.ReduceBlockiness ? indentBefore + formatter.SpaceTab : indentBefore; formatter.SetOpeningIndentedRegion(token, indentBefore); + break; } case ":=": diff --git a/Source/DafnyCore/AST/Expressions/Expressions.cs b/Source/DafnyCore/AST/Expressions/Expressions.cs index a2dde9c9525..8d9ce288500 100644 --- a/Source/DafnyCore/AST/Expressions/Expressions.cs +++ b/Source/DafnyCore/AST/Expressions/Expressions.cs @@ -5,6 +5,7 @@ using System.Numerics; using System.Linq; using System.Diagnostics; +using System.Reflection.Emit; using System.Security.AccessControl; using Microsoft.Boogie; @@ -2258,7 +2259,10 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { formatter.SetIndentations(ownedTokens[0], formatter.binOpIndent, formatter.binOpIndent, formatter.binOpArgIndent); } else { var startToken = this.StartToken; - var newIndent = formatter.GetNewTokenVisualIndent(startToken, formatter.GetIndentInlineOrAbove(startToken)); + var newIndent = + ownedTokens[0].val == "," ? + formatter.GetIndentInlineOrAbove(startToken) + : formatter.GetNewTokenVisualIndent(startToken, formatter.GetIndentInlineOrAbove(startToken)); formatter.SetIndentations(ownedTokens[0], newIndent, newIndent, newIndent); } } @@ -2323,6 +2327,33 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { formatter.Visit(E1, item2Indent); formatter.SetIndentations(EndToken, below: indent); return false; + } else if (Op is Opcode.In or Opcode.NotIn) { + var itemIndent = formatter.GetNewTokenVisualIndent( + E0.StartToken, indent); + var item2Indent = itemIndent + formatter.SpaceTab; + formatter.Visit(E0, itemIndent); + foreach (var token in this.OwnedTokens) { + switch (token.val) { + case "<": { + if (token.Prev.line != token.line) { + itemIndent = formatter.GetNewTokenVisualIndent(token, indent); + } + + break; + } + case "in": + case "-": { + if (TokenNewIndentCollector.IsFollowedByNewline(token)) { + formatter.SetOpeningIndentedRegion(token, itemIndent); + } else { + formatter.SetAlign(itemIndent, token, out item2Indent, out _); + } + break; + } + } + } + formatter.Visit(E1, item2Indent); + return false; } else { foreach (var token in OwnedTokens) { formatter.SetIndentations(token, indent, indent, indent); diff --git a/Source/DafnyPipeline.Test/FormatterIssues.cs b/Source/DafnyPipeline.Test/FormatterIssues.cs index 178c1f51cce..2372fd18f42 100644 --- a/Source/DafnyPipeline.Test/FormatterIssues.cs +++ b/Source/DafnyPipeline.Test/FormatterIssues.cs @@ -4,6 +4,83 @@ namespace DafnyPipeline.Test; [Collection("Singleton Test Collection - FormatterForTopLevelDeclarations")] public class FormatterIssues : FormatterBaseTest { + [Fact] + public void GitIssue3912FormatterCollectionArrow() { + FormatterWorksFor(@" +const i := + a in + B + // Previously it was not indented + C + + D && + b in + B + + C +"); + } + + [Fact] + public void GitIssue3912FormatterCollectionArrowA() { + FormatterWorksFor(@" +const newline := + set + i <- + PartA + + PartB + + PartC, + j <- + PartD + :: + f(i,j) + +const sameline := + set i <- + PartA + + PartB + + PartC, + j <- + PartD + :: + f(i,j) + +"); + } + + [Fact] + public void GitIssue3912FormatterCollectionArrowB() { + FormatterWorksFor(@" +const newlineOp := + set + i + <- + PartA + + PartB + + PartC, + j + <- + PartD + :: + f(i,j) + +"); + } + + [Fact] + public void GitIssue3912FormatterCollectionArrowC() { + FormatterWorksFor(@" +const sameLineOp := + set i + <- + PartA + + PartB + + PartC, + j + <- PartD + + PartE + :: + f(i,j) +"); + } + [Fact] public void GitIssue3790DafnyFormatterProducesIncorrectIndentation() { FormatterWorksFor(@" diff --git a/docs/dev/news/3912.fix b/docs/dev/news/3912.fix new file mode 100644 index 00000000000..b6f48a2d3fd --- /dev/null +++ b/docs/dev/news/3912.fix @@ -0,0 +1 @@ +Format for comprehension expressions \ No newline at end of file From fa854e7e67e0574366430830f35cd5e255e73baa Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 27 Apr 2023 13:24:34 -0500 Subject: [PATCH 2/3] added comment --- Source/DafnyCore/AST/Expressions/Expressions.cs | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/DafnyCore/AST/Expressions/Expressions.cs b/Source/DafnyCore/AST/Expressions/Expressions.cs index 8d9ce288500..6a34d502972 100644 --- a/Source/DafnyCore/AST/Expressions/Expressions.cs +++ b/Source/DafnyCore/AST/Expressions/Expressions.cs @@ -2259,6 +2259,7 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { formatter.SetIndentations(ownedTokens[0], formatter.binOpIndent, formatter.binOpIndent, formatter.binOpArgIndent); } else { var startToken = this.StartToken; + //"," in a comprehension is an "&&", except that it should not try to keep a visual indentation between components. var newIndent = ownedTokens[0].val == "," ? formatter.GetIndentInlineOrAbove(startToken) From 0359477bb5f42e2a8dd9e84eb760d54a1159c011 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Mon, 8 May 2023 14:40:16 -0500 Subject: [PATCH 3/3] Update FormatterIssues.cs --- Source/DafnyPipeline.Test/FormatterIssues.cs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Source/DafnyPipeline.Test/FormatterIssues.cs b/Source/DafnyPipeline.Test/FormatterIssues.cs index c0c8154c136..41c2a2489c9 100644 --- a/Source/DafnyPipeline.Test/FormatterIssues.cs +++ b/Source/DafnyPipeline.Test/FormatterIssues.cs @@ -81,6 +81,7 @@ set i "); } + [Fact] public void GitIssue3960FormattingIssueForallStatements() { FormatterWorksFor(@" lemma Lemma() @@ -126,4 +127,4 @@ public void FormatterWorksForEmptyDocument() { FormatterWorksFor(@" ", null, true); } -} \ No newline at end of file +}