From 463c65408e5ad397002f919d2e2ea1e71b55a5a1 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 9 Jan 2025 10:04:45 -0600 Subject: [PATCH 1/6] Feat: Support for code actions to insert calc and forall statements --- .../DafnyCore/AST/Grammar/Printer/Printer.cs | 8 + .../CodeActions/CodeActionsTest.cs | 173 ++++++++++++-- ...licitFailingAssertionCodeActionProvider.cs | 213 ++++++++++++++---- .../Plugins/DafnyCodeActionProvider.cs | 4 + 4 files changed, 339 insertions(+), 59 deletions(-) diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs index 5d61f3aebb..5a90611bf4 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs @@ -79,6 +79,14 @@ public static string ExprToString(DafnyOptions options, Expression expr, [CanBeN return wr.ToString(); } + public static string ForallExprRangeToString(DafnyOptions options, ForallExpr expr, + [CanBeNull] PrintFlags printFlags = null) { + using var wr = new StringWriter(); + var pr = new Printer(wr, options, printFlags: printFlags); + pr.PrintQuantifierDomain(expr.BoundVars, expr.Attributes, expr.Range); + return wr.ToString(); + } + public static string ExprListToString(DafnyOptions options, List expressions, [CanBeNull] PrintFlags printFlags = null) { Contract.Requires(expressions != null); using var wr = new StringWriter(); diff --git a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs index bd28edcf2a..4925840ab2 100644 --- a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs +++ b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs @@ -5,6 +5,7 @@ using System.Linq; using System.Text.RegularExpressions; using System.Threading.Tasks; +using Castle.Core.Internal; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; using Xunit.Abstractions; @@ -93,6 +94,44 @@ method Dac(c: L) }"); } + [Fact] + public async Task TestCalcIntroduction() { + await TestCodeAction(@" +method Test() { + assert 1 =><= 2(>Insert a calc statement-> by { + calc { + 1; + 2; + } + }:::;<) +}"); + } + + [Fact] + public async Task TestCalcIntroductionEquiv() { + await TestCodeAction(@" +method Test() { + assert true <=><=> false(>Insert a calc statement-> by { + calc <==> { + true; + false; + } + }:::;<) +}"); + } + + [Fact] + public async Task TestForallIntroduction() { + await TestCodeAction(@" +method Test() { + assert forall i | i % 4 == 1 :: i % 2 == 0(>Insert a calc statement-> by { + forall i | i % 4 == 1 ensures i % 2 == 0 { + assert i % 2 == 0; + } + }:::;<) +}"); + } + [Fact] public async Task GitIssue4401CorrectInsertionPlace() { await TestCodeAction(@" @@ -239,17 +278,50 @@ match e } [Fact] - public async Task ExplicitDivisionByZero() { + public async Task ExplicitDivisionByZeroFunction() { await TestCodeAction(@" -method Foo(i: int) +function Foo(i: int): int { (>Insert explicit failing assertion->assert i + 1 != 0; <)var x := 2>< / (i + 1); + x }"); } [Fact] - public async Task ExplicitDivisionImp() { + public async Task ExplicitDivisionByZeroMethod() { + await TestCodeAction(@" +method Foo(i: int) +{ + var x := 2>< / (i + 1)(>Insert explicit failing assertion-> by { + assert i + 1 != 0; + }:::;<) +}"); + } + + [Fact] + public async Task ExplicitDivisionImpFunction() { + await TestCodeAction(@" +function Foo(b: bool, i: int, j: int): bool +{ + var x := b ==> (>Insert explicit failing assertion->assert i + 1 != 0; + <)2 > b ==> (>Insert explicit failing assertion->assert i + 1 != 0; + <)2 >Insert explicit failing assertion->assert i + 1 != 0; <)2 >Insert explicit failing assertion-> by { + assert i + 1 != 0; + }:::;<) +}"); + } + + [Fact] + public async Task ExplicitDivisionAnd2Function() { + await TestCodeAction(@" +function Foo(b: bool, i: int, j: int): int { (>Insert explicit failing assertion->assert i + 1 != 0; <)var x := 2 >Insert explicit failing assertion-> by { + assert i + 1 != 0; + }:::;<) }"); } @@ -304,45 +401,80 @@ public async Task ExplicitDivisionOr2() { await TestCodeAction(@" method Foo(b: bool, i: int, j: int) { - (>Insert explicit failing assertion->assert i + 1 != 0; - <)var x := 2 >Insert explicit failing assertion-> by { + assert i + 1 != 0; + }:::;<) }"); } - - [Fact] public async Task ExplicitDivisionAddParentheses() { await TestCodeAction(@" method Foo(b: bool, i: int, j: int) +{ + var x := 2 > i + 1 case false => i - 1(>Insert explicit failing assertion-> by { + assert (match b case true => i + 1 case false => i - 1) != 0; + }:::;<) +}"); + } + + [Fact] + public async Task ExplicitDivisionAddParentheses2() { + await TestCodeAction(@" +function Foo(b: bool, i: int, j: int): int { (>Insert explicit failing assertion->assert (match b case true => i + 1 case false => i - 1) != 0; <)var x := 2 > i + 1 case false => i - 1; + x }"); } [Fact] - public async Task ExplicitDivisionExp() { + public async Task ExplicitDivisionExpMethod() { await TestCodeAction(@" method Foo(b: bool, i: int, j: int) +{ + var x := b <== 2 >Insert explicit failing assertion-> by { + assert i + 1 != 0; + }:::;<) +}"); + } + + [Fact] + public async Task ExplicitDivisionExpFunction() { + await TestCodeAction(@" +function Foo(b: bool, i: int, j: int): int { (>Insert explicit failing assertion->assert i + 1 != 0; <)var x := b <== 2 >Insert explicit failing assertion->(assert i + 1 != 0; 2 / (i + 1) == j):::2 >Insert explicit failing assertion-> by { + assert i + 1 != 0; + }:::;<) +}"); + } + + [Fact] + public async Task ExplicitDivisionByZeroIfFunction() { await TestCodeAction(@" function Foo(i: int): int { @@ -357,7 +489,7 @@ function Foo(i: int): int [Fact] - public async Task ExplicitDivisionByZeroFunctionLetExpr() { + public async Task ExplicitDivisionByZeroMatchFunctionLetExpr() { await TestCodeAction(@" function Foo(i: int): int { @@ -409,8 +541,13 @@ private async Task TestCodeAction(string source) { } } - Assert.True(found, - $"Did not find the code action '{expectedTitle}'. Available were:{string.Join(",", otherTitles)}"); + if (otherTitles.IsNullOrEmpty()) { + // Parsing gone wrong, we display diagnostics + Assert.True(false, output + "\n" + string.Join("\n", diagnostics.Select(d => d.ToString()))); + } else { + Assert.True(found, + $"Did not find the code action '{expectedTitle}'. Available were:{string.Join(",", otherTitles)}"); + } } } diff --git a/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs b/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs index 3f67298ffb..e7c54ada2c 100644 --- a/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs +++ b/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs @@ -39,41 +39,21 @@ public ImplicitFailingAssertionCodeActionProvider(ILogger 0 ? new List { node } : null; } + + public static INode? GetInsertionNode(Node program, Range selection, out List? nodesTillFailure, out bool needsIsolation) + { + nodesTillFailure = FindInnermostNodeIntersecting(program, selection); - class ExplicitAssertionDafnyCodeAction : DafnyCodeAction { - private readonly DafnyOptions options; - private readonly Expression failingImplicitAssertion; - private readonly Node program; - private readonly Range selection; + needsIsolation = false; - public ExplicitAssertionDafnyCodeAction( - DafnyOptions options, - Node program, - Expression failingImplicitAssertion, - Range selection - ) : base("Insert explicit failing assertion") { - this.options = options; - this.failingImplicitAssertion = failingImplicitAssertion; - this.program = program; - this.selection = selection; - } - - public override IEnumerable GetEdits() { - var nodesTillFailure = FindInnermostNodeIntersecting(program, selection); - - var suggestedEdits = new List(); - var needsIsolation = false; - if (nodesTillFailure == null) { - return suggestedEdits.ToArray(); - } - - INode? insertionNode = null; + INode? insertionNode = null; + if (nodesTillFailure != null) { for (var i = 0; i < nodesTillFailure.Count; i++) { var node = nodesTillFailure[i]; var nextNode = i < nodesTillFailure.Count - 1 ? nodesTillFailure[i + 1] : null; if (node is Statement or LetExpr && ((node is AssignStatement or AssignSuchThatStmt && nextNode is not VarDeclStmt) || - (node is not AssignStatement && nextNode is not VarDeclStmt && nextNode is not AssignSuchThatStmt))) { + (node is not AssignStatement && nextNode is not VarDeclStmt && nextNode is not AssignSuchThatStmt))) { insertionNode = node; break; } @@ -96,20 +76,151 @@ public override IEnumerable GetEdits() { } insertionNode ??= nodesTillFailure[0]; + } else { + insertionNode = null; + } + + return insertionNode; + } + abstract class StatementInsertingCodeAction : DafnyCodeAction { + protected readonly DafnyOptions options; + protected readonly Expression failingImplicitAssertion; + protected readonly Node program; + protected readonly Range selection; + + public StatementInsertingCodeAction( + DafnyOptions options, + Node program, + Expression failingImplicitAssertion, + Range selection, + string message + ) : base(message) { + this.options = options; + this.failingImplicitAssertion = failingImplicitAssertion; + this.program = program; + this.selection = selection; + } + + public override IEnumerable GetEdits() { + var insertionNode = GetInsertionNode(program, selection, out var nodesTillFailure, out var needsIsolation); + if (insertionNode == null || nodesTillFailure == null) { + return new DafnyCodeActionEdit[]{}; + } + + var i = nodesTillFailure.FindLastIndex(node => node is AssertStmt or VarDeclStmt or CallStmt); + INode? possibleByBlocks = null; + if (i != -1 && i + 1 <= nodesTillFailure.Count && insertionNode == nodesTillFailure[i + 1]) { + possibleByBlocks = nodesTillFailure[i]; + } + if (possibleByBlocks?.EndToken is {val: ";" } endToken) { + // We can insert a by block to keep the proof limited + var start = possibleByBlocks.StartToken; + var indentation = IndentationFormatter.Whitespace(Math.Max(start.col - 1, 0)); + var indentation2 = indentation + " "; + var block = " by {\n" + + indentation2 + GetStatementToInsert(indentation2) + "\n" + + indentation + "}"; + return ReplaceWith(endToken, block); + } else {// TODO: If there is already a by block, can we insert into it? + var start = insertionNode.StartToken; + var indentation = IndentationFormatter.Whitespace(Math.Max(start.col - 1 + (needsIsolation ? 1 : 0), 0)); + var assertStr = GetStatementToInsert(indentation) + "\n" + indentation; + return PrefixWithStatement(insertionNode, needsIsolation, assertStr); + } + } + + /// Helper for subclasses to print an expression + protected string S(Expression e) { + return Printer.ExprToString(options, e, new PrintFlags(UseOriginalDafnyNames: true)); + } + + /// Emit code editing instructions to insert the given statement before the given insertion node + /// Wraps everything with parentheses if it requires isolationn, which is the case in expressions notably + protected static IEnumerable PrefixWithStatement(INode insertionNode, bool needsIsolation, string statement) { var start = insertionNode.StartToken; - var assertStr = $"{(needsIsolation ? "(" : "")}assert {Printer.ExprToString(options, failingImplicitAssertion, new PrintFlags(UseOriginalDafnyNames: true))};\n" + - IndentationFormatter.Whitespace(Math.Max(start.col - 1 + (needsIsolation ? 1 : 0), 0)); - suggestedEdits.Add( - new DafnyCodeActionEdit( - InsertBefore(start), assertStr)); + if (needsIsolation) { + statement = "(" + statement; + } + var suggestedEdits = new List { + new ( + InsertBefore(start), statement) + }; if (needsIsolation) { suggestedEdits.Add(new DafnyCodeActionEdit( - InsertAfter(insertionNode.EndToken), ")")); + InsertAfter(insertionNode.EndToken), ")")); } return suggestedEdits.ToArray(); } + + /// Emit code editing instructions to insert the given statement before the given insertion node + /// Wraps everything with parentheses if it requires isolationn, which is the case in expressions notably + protected static IEnumerable ReplaceWith(Token tokenToReplace, string block) { + var suggestedEdits = new List { + new (Replace(tokenToReplace), block) + }; + + return suggestedEdits.ToArray(); + } + + + protected abstract string GetStatementToInsert(string indentation); + } + + class ExplicitAssertionDafnyCodeAction : StatementInsertingCodeAction { + public ExplicitAssertionDafnyCodeAction( + DafnyOptions options, + Node program, + Expression failingImplicitAssertion, + Range selection + ) : base(options, program, failingImplicitAssertion, selection, "Insert explicit failing assertion") { + } + + protected override string GetStatementToInsert(string indentation) { + return $"assert {S(failingImplicitAssertion)};"; + } + } + + class BinaryExprToCalcStatementCodeAction : StatementInsertingCodeAction { + private readonly BinaryExpr failingExplicit; + + public BinaryExprToCalcStatementCodeAction( + DafnyOptions options, + Node program, + BinaryExpr failingExplicit, + Range selection + ) : base(options, program, failingExplicit, selection, "Insert a calc statement") { + this.failingExplicit = failingExplicit; + } + + protected override string GetStatementToInsert(string i) { + var op = failingExplicit.Op is BinaryExpr.Opcode.Iff ? "<==> " : ""; + return /* + */$"calc {op}{{\n"+ + $"{i} {S(failingExplicit.E0)};\n"+ + $"{i} {S(failingExplicit.E1)};\n"+ + $"{i}}}"; + } + } + + class ForallExprStatementCodeAction : StatementInsertingCodeAction { + private readonly ForallExpr failingExplicit; + + public ForallExprStatementCodeAction( + DafnyOptions options, + Node program, + ForallExpr failingExplicit, + Range selection + ) : base(options, program, failingExplicit, selection, "Insert a calc statement") { + this.failingExplicit = failingExplicit; + } + + protected override string GetStatementToInsert(string i) { + return "forall " + Printer.ForallExprRangeToString(options, failingExplicit) + " ensures " + S(failingExplicit.Term) + " {\n" + + $"{i} assert {S(failingExplicit.Term)};\n"+ + $"{i}}}"; + } } protected override IEnumerable? GetDafnyCodeActions(IDafnyCodeActionInput input, @@ -119,22 +230,42 @@ public override IEnumerable GetEdits() { } var failingExpressions = new List() { }; + var failingEqualities = new List() { }; + var failingForalls = new List() { }; input.VerificationTree?.Visit(tree => { if (tree is AssertionVerificationTree assertTree && assertTree.Finished && - assertTree.Range.Intersects(selection) && - assertTree.StatusVerification is GutterVerificationStatus.Error or GutterVerificationStatus.Inconclusive && - assertTree.GetAssertion()?.Description is ProofObligationDescription description && - description.GetAssertedExpr(options) is { } assertedExpr) { - failingExpressions.Add(assertedExpr); + assertTree.Range.Intersects(selection) && + assertTree.StatusVerification is GutterVerificationStatus.Error or GutterVerificationStatus.Inconclusive && + assertTree.GetAssertion()?.Description is ProofObligationDescription description && + description.GetAssertedExpr(options) is { } assertedExpr) { + if (description.IsImplicit) { + failingExpressions.Add(assertedExpr); + } else { + switch (assertedExpr) + { + case BinaryExpr { Op: BinaryExpr.Opcode.Eq or BinaryExpr.Opcode.Iff } binExpr: + failingEqualities.Add(binExpr); + break; + case ForallExpr forallExpr: + failingForalls.Add(forallExpr); + break; + } + } } }); - if (failingExpressions.Count == 0) { + if (failingExpressions.Count == 0 && failingEqualities.Count == 0) { return null; } - return failingExpressions.Select(failingExpression => + IEnumerable explicitAssertions = failingExpressions.Select(failingExpression => new ExplicitAssertionDafnyCodeAction(options, input.Program, failingExpression, selection) ); + IEnumerable suggestedCalcStatements = failingEqualities.Select(failingEquality => + new BinaryExprToCalcStatementCodeAction(options, input.Program, failingEquality, selection)); + IEnumerable suggestedForallStatements = failingForalls.Select(failingForall => + new ForallExprStatementCodeAction(options, input.Program, failingForall, selection)); + + return explicitAssertions.Concat(suggestedCalcStatements).Concat(suggestedForallStatements); } } \ No newline at end of file diff --git a/Source/DafnyLanguageServer/Plugins/DafnyCodeActionProvider.cs b/Source/DafnyLanguageServer/Plugins/DafnyCodeActionProvider.cs index 2160c09437..9faee207aa 100644 --- a/Source/DafnyLanguageServer/Plugins/DafnyCodeActionProvider.cs +++ b/Source/DafnyLanguageServer/Plugins/DafnyCodeActionProvider.cs @@ -37,6 +37,10 @@ public abstract class DafnyCodeActionProvider { protected static SourceOrigin InsertBefore(Token tok) { return new SourceOrigin(tok, null); } + + protected static SourceOrigin Replace(Token tok) { + return new SourceOrigin(tok, tok); + } protected static SourceOrigin InsertAfter(IOrigin tok) { return new SourceOrigin(new Token(tok.line, tok.col + tok.val.Length) { pos = tok.pos + tok.val.Length, From bb5ad21a321ca30e377a27169a34e13a0dbd148a Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 9 Jan 2025 16:02:54 -0600 Subject: [PATCH 2/6] Fixed insertion mechanism. --- .../CodeActions/CodeActionsTest.cs | 35 ++++++++---- ...licitFailingAssertionCodeActionProvider.cs | 57 ++++++++----------- 2 files changed, 48 insertions(+), 44 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs index 4925840ab2..8fbeb60218 100644 --- a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs +++ b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs @@ -124,22 +124,35 @@ method Test() { public async Task TestForallIntroduction() { await TestCodeAction(@" method Test() { - assert forall i | i % 4 == 1 :: i % 2 == 0(>Insert a calc statement-> by { - forall i | i % 4 == 1 ensures i % 2 == 0 { + assert for>Insert a forall statement-> by { + forall i: int | i % 4 == 1 ensures i % 2 == 0 { assert i % 2 == 0; } }:::;<) }"); } + [Fact] + public async Task TestForallIntroductionFunction() { + await TestCodeAction(@" +function Test(): int { + (>Insert a forall statement->forall i | i % 4 == 1 ensures i % 2 == 0 { + assert i % 2 == 0; + } + <)assert for>Insert explicit failing assertion-> - assert exists x: int :: P(x);<) - var x :><| P(x); +method Test() { + var x :><| P(x)(>Insert explicit failing assertion-> by { + assert exists x: int :: P(x); + }:::;<) }"); } @@ -150,9 +163,10 @@ module Test { class TheTest { predicate P(i: int) - method Test() {(>Insert explicit failing assertion-> - assert exists x: int :: P(x);<) - var x :><| P(x); + method Test() { + var x :><| P(x)(>Insert explicit failing assertion-> by { + assert exists x: int :: P(x); + }:::;<) } } }"); @@ -335,8 +349,9 @@ public async Task ExplicitDivisionImp2() { await TestCodeAction(@" method Foo(b: bool, i: int, j: int) { - (>Insert explicit failing assertion->assert i + 1 != 0; - <)var x := 2 > b; + var x := 2 > b(>Insert explicit failing assertion-> by { + assert i + 1 != 0; + }:::;<) }"); } diff --git a/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs b/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs index e7c54ada2c..c61f6411e2 100644 --- a/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs +++ b/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs @@ -40,17 +40,17 @@ public ImplicitFailingAssertionCodeActionProvider(ILogger 0 ? new List { node } : null; } - public static INode? GetInsertionNode(Node program, Range selection, out List? nodesTillFailure, out bool needsIsolation) + public static INode? GetInsertionNode(Node program, Range selection, out List? nodesSinceFailure, out bool needsIsolation) { - nodesTillFailure = FindInnermostNodeIntersecting(program, selection); + nodesSinceFailure = FindInnermostNodeIntersecting(program, selection); needsIsolation = false; INode? insertionNode = null; - if (nodesTillFailure != null) { - for (var i = 0; i < nodesTillFailure.Count; i++) { - var node = nodesTillFailure[i]; - var nextNode = i < nodesTillFailure.Count - 1 ? nodesTillFailure[i + 1] : null; + if (nodesSinceFailure != null) { + for (var i = 0; i < nodesSinceFailure.Count; i++) { + var node = nodesSinceFailure[i]; + var nextNode = i < nodesSinceFailure.Count - 1 ? nodesSinceFailure[i + 1] : null; if (node is Statement or LetExpr && ((node is AssignStatement or AssignSuchThatStmt && nextNode is not VarDeclStmt) || (node is not AssignStatement && nextNode is not VarDeclStmt && nextNode is not AssignSuchThatStmt))) { @@ -59,7 +59,7 @@ public ImplicitFailingAssertionCodeActionProvider(ILogger GetEdits() { return new DafnyCodeActionEdit[]{}; } - var i = nodesTillFailure.FindLastIndex(node => node is AssertStmt or VarDeclStmt or CallStmt); - INode? possibleByBlocks = null; - if (i != -1 && i + 1 <= nodesTillFailure.Count && insertionNode == nodesTillFailure[i + 1]) { - possibleByBlocks = nodesTillFailure[i]; - } - if (possibleByBlocks?.EndToken is {val: ";" } endToken) { + if (insertionNode is AssertStmt or VarDeclStmt or CallStmt && insertionNode.EndToken is {val: ";" } endToken) { // We can insert a by block to keep the proof limited - var start = possibleByBlocks.StartToken; + var start = insertionNode.StartToken; var indentation = IndentationFormatter.Whitespace(Math.Max(start.col - 1, 0)); var indentation2 = indentation + " "; var block = " by {\n" + @@ -212,7 +207,7 @@ public ForallExprStatementCodeAction( Node program, ForallExpr failingExplicit, Range selection - ) : base(options, program, failingExplicit, selection, "Insert a calc statement") { + ) : base(options, program, failingExplicit, selection, "Insert a forall statement") { this.failingExplicit = failingExplicit; } @@ -229,9 +224,8 @@ protected override string GetStatementToInsert(string i) { return null; } - var failingExpressions = new List() { }; - var failingEqualities = new List() { }; - var failingForalls = new List() { }; + var implicitlyFailing = new List() { }; + var explicitlyFailing = new List() { }; input.VerificationTree?.Visit(tree => { if (tree is AssertionVerificationTree assertTree && assertTree.Finished && @@ -240,32 +234,27 @@ assertTree.StatusVerification is GutterVerificationStatus.Error or GutterVerific assertTree.GetAssertion()?.Description is ProofObligationDescription description && description.GetAssertedExpr(options) is { } assertedExpr) { if (description.IsImplicit) { - failingExpressions.Add(assertedExpr); + implicitlyFailing.Add(assertedExpr); } else { - switch (assertedExpr) - { - case BinaryExpr { Op: BinaryExpr.Opcode.Eq or BinaryExpr.Opcode.Iff } binExpr: - failingEqualities.Add(binExpr); - break; - case ForallExpr forallExpr: - failingForalls.Add(forallExpr); - break; - } + explicitlyFailing.Add(assertedExpr); } } }); - if (failingExpressions.Count == 0 && failingEqualities.Count == 0) { + if (implicitlyFailing.Count == 0 && explicitlyFailing.Count == 0) { return null; } - IEnumerable explicitAssertions = failingExpressions.Select(failingExpression => + IEnumerable suggestedExplicitAssertions = implicitlyFailing.Select(failingExpression => new ExplicitAssertionDafnyCodeAction(options, input.Program, failingExpression, selection) ); - IEnumerable suggestedCalcStatements = failingEqualities.Select(failingEquality => + IEnumerable suggestedCalcStatements = + explicitlyFailing.OfType().Where(b => b.Op is BinaryExpr.Opcode.Eq or BinaryExpr.Opcode.Iff ).Select(failingEquality => new BinaryExprToCalcStatementCodeAction(options, input.Program, failingEquality, selection)); - IEnumerable suggestedForallStatements = failingForalls.Select(failingForall => + IEnumerable suggestedForallStatements = explicitlyFailing + .OfType() + .Select(failingForall => new ForallExprStatementCodeAction(options, input.Program, failingForall, selection)); - return explicitAssertions.Concat(suggestedCalcStatements).Concat(suggestedForallStatements); + return suggestedExplicitAssertions.Concat(suggestedCalcStatements).Concat(suggestedForallStatements); } } \ No newline at end of file From 1ccd1620aae07516f9499a1cdb3a0ab29ffad8b2 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 10 Jan 2025 18:58:12 -0600 Subject: [PATCH 3/6] formatting --- .../CodeActions/CodeActionsTest.cs | 4 +-- ...licitFailingAssertionCodeActionProvider.cs | 29 +++++++++---------- 2 files changed, 16 insertions(+), 17 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs index 8fbeb60218..d90cbd36cd 100644 --- a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs +++ b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs @@ -365,8 +365,8 @@ function Foo(b: bool, i: int, j: int): int x }"); } - - + + [Fact] public async Task ExplicitDivisionAndMethod() { await TestCodeAction(@" diff --git a/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs b/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs index c61f6411e2..ccf9887335 100644 --- a/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs +++ b/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs @@ -39,9 +39,8 @@ public ImplicitFailingAssertionCodeActionProvider(ILogger 0 ? new List { node } : null; } - - public static INode? GetInsertionNode(Node program, Range selection, out List? nodesSinceFailure, out bool needsIsolation) - { + + public static INode? GetInsertionNode(Node program, Range selection, out List? nodesSinceFailure, out bool needsIsolation) { nodesSinceFailure = FindInnermostNodeIntersecting(program, selection); needsIsolation = false; @@ -105,10 +104,10 @@ string message public override IEnumerable GetEdits() { var insertionNode = GetInsertionNode(program, selection, out var nodesTillFailure, out var needsIsolation); if (insertionNode == null || nodesTillFailure == null) { - return new DafnyCodeActionEdit[]{}; + return new DafnyCodeActionEdit[] { }; } - if (insertionNode is AssertStmt or VarDeclStmt or CallStmt && insertionNode.EndToken is {val: ";" } endToken) { + if (insertionNode is AssertStmt or VarDeclStmt or CallStmt && insertionNode.EndToken is { val: ";" } endToken) { // We can insert a by block to keep the proof limited var start = insertionNode.StartToken; var indentation = IndentationFormatter.Whitespace(Math.Max(start.col - 1, 0)); @@ -129,7 +128,7 @@ public override IEnumerable GetEdits() { protected string S(Expression e) { return Printer.ExprToString(options, e, new PrintFlags(UseOriginalDafnyNames: true)); } - + /// Emit code editing instructions to insert the given statement before the given insertion node /// Wraps everything with parentheses if it requires isolationn, which is the case in expressions notably protected static IEnumerable PrefixWithStatement(INode insertionNode, bool needsIsolation, string statement) { @@ -158,7 +157,7 @@ protected static IEnumerable ReplaceWith(Token tokenToRepla return suggestedEdits.ToArray(); } - + protected abstract string GetStatementToInsert(string indentation); } @@ -171,7 +170,7 @@ public ExplicitAssertionDafnyCodeAction( Range selection ) : base(options, program, failingImplicitAssertion, selection, "Insert explicit failing assertion") { } - + protected override string GetStatementToInsert(string indentation) { return $"assert {S(failingImplicitAssertion)};"; } @@ -192,13 +191,13 @@ Range selection protected override string GetStatementToInsert(string i) { var op = failingExplicit.Op is BinaryExpr.Opcode.Iff ? "<==> " : ""; return /* - */$"calc {op}{{\n"+ - $"{i} {S(failingExplicit.E0)};\n"+ - $"{i} {S(failingExplicit.E1)};\n"+ + */$"calc {op}{{\n" + + $"{i} {S(failingExplicit.E0)};\n" + + $"{i} {S(failingExplicit.E1)};\n" + $"{i}}}"; } } - + class ForallExprStatementCodeAction : StatementInsertingCodeAction { private readonly ForallExpr failingExplicit; @@ -213,7 +212,7 @@ Range selection protected override string GetStatementToInsert(string i) { return "forall " + Printer.ForallExprRangeToString(options, failingExplicit) + " ensures " + S(failingExplicit.Term) + " {\n" + - $"{i} assert {S(failingExplicit.Term)};\n"+ + $"{i} assert {S(failingExplicit.Term)};\n" + $"{i}}}"; } } @@ -247,8 +246,8 @@ assertTree.StatusVerification is GutterVerificationStatus.Error or GutterVerific IEnumerable suggestedExplicitAssertions = implicitlyFailing.Select(failingExpression => new ExplicitAssertionDafnyCodeAction(options, input.Program, failingExpression, selection) ); - IEnumerable suggestedCalcStatements = - explicitlyFailing.OfType().Where(b => b.Op is BinaryExpr.Opcode.Eq or BinaryExpr.Opcode.Iff ).Select(failingEquality => + IEnumerable suggestedCalcStatements = + explicitlyFailing.OfType().Where(b => b.Op is BinaryExpr.Opcode.Eq or BinaryExpr.Opcode.Iff).Select(failingEquality => new BinaryExprToCalcStatementCodeAction(options, input.Program, failingEquality, selection)); IEnumerable suggestedForallStatements = explicitlyFailing .OfType() From f950860e36b7879aaeec825b98f257a08a6c8e44 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 10 Jan 2025 21:37:14 -0600 Subject: [PATCH 4/6] Support for inserting into preexisting by clauses --- .../CodeActions/CodeActionsTest.cs | 42 ++++++++++++++++++- ...licitFailingAssertionCodeActionProvider.cs | 23 ++++++---- 2 files changed, 57 insertions(+), 8 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs index d90cbd36cd..4b2cf7b918 100644 --- a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs +++ b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs @@ -156,6 +156,44 @@ method Test() { }"); } + [Fact] + public async Task InsertIntoByStatement() { + await TestCodeAction(@" +predicate P(i: int) + +function Test(i: int): int + requires P(i) { + i +} + +method TestMethod() { + assert Test><(1) == 1 by { + (>Insert explicit failing assertion->assert P(1); + <)calc { + 1; + 1; + } + } +}"); + } + + [Fact] + public async Task InsertIntoEmptyByStatement() { + await TestCodeAction(@" +predicate P(i: int) + +function Test(i: int): int + requires P(i) { + i +} + +method TestMethod() { + assert Test><(1) == 1 by { + (>Insert explicit failing assertion-> assert P(1); + <)} +}"); + } + [Fact] public async Task GitIssue4401CorrectInsertionPlaceModule() { await TestCodeAction(@" @@ -525,7 +563,9 @@ private async Task TestCodeAction(string source) { out var ranges); var documentItem = await CreateOpenAndWaitForResolve(output); var diagnostics = await GetLastDiagnostics(documentItem); - Assert.Equal(ranges.Count, diagnostics.Length); + if (ranges.Count != diagnostics.Length) { + Assert.True(ranges.Count == diagnostics.Length, string.Join("\n", diagnostics.Select(d => d.ToString()))); + } if (positions.Count != ranges.Count) { positions = ranges.Select(r => r.Range.Start).ToList(); diff --git a/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs b/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs index ccf9887335..35bb6e604d 100644 --- a/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs +++ b/Source/DafnyLanguageServer/Language/ImplicitFailingAssertionCodeActionProvider.cs @@ -116,11 +116,22 @@ public override IEnumerable GetEdits() { indentation2 + GetStatementToInsert(indentation2) + "\n" + indentation + "}"; return ReplaceWith(endToken, block); - } else {// TODO: If there is already a by block, can we insert into it? + } else if (insertionNode is AssertStmt or VarDeclStmt or CallStmt && insertionNode.OwnedTokens.FirstOrDefault(t => t.val == "by") is { Next: { val: "{" } braceToken } byToken) { + var start = braceToken.Next; + var isEmptyBy = start.Next is { val: "}" }; + var innerCol = isEmptyBy ? start.col + 1 : start.col - 1; + var indentation = IndentationFormatter.Whitespace(Math.Max(innerCol, 0)); + var indentationStart = IndentationFormatter.Whitespace(Math.Max(start.col - 1, 0)); + var assertStr = GetStatementToInsert(indentation) + "\n" + indentationStart; + if (isEmptyBy) { + assertStr = " " + assertStr; + } + return PrefixWithStatement(start, start, false, assertStr); + } else { var start = insertionNode.StartToken; var indentation = IndentationFormatter.Whitespace(Math.Max(start.col - 1 + (needsIsolation ? 1 : 0), 0)); var assertStr = GetStatementToInsert(indentation) + "\n" + indentation; - return PrefixWithStatement(insertionNode, needsIsolation, assertStr); + return PrefixWithStatement(insertionNode.StartToken, insertionNode.EndToken, needsIsolation, assertStr); } } @@ -131,18 +142,16 @@ protected string S(Expression e) { /// Emit code editing instructions to insert the given statement before the given insertion node /// Wraps everything with parentheses if it requires isolationn, which is the case in expressions notably - protected static IEnumerable PrefixWithStatement(INode insertionNode, bool needsIsolation, string statement) { - var start = insertionNode.StartToken; + protected static IEnumerable PrefixWithStatement(Token start, Token end, bool needsIsolation, string statement) { if (needsIsolation) { statement = "(" + statement; } var suggestedEdits = new List { - new ( - InsertBefore(start), statement) + new (InsertBefore(start), statement) }; if (needsIsolation) { suggestedEdits.Add(new DafnyCodeActionEdit( - InsertAfter(insertionNode.EndToken), ")")); + InsertAfter(end), ")")); } return suggestedEdits.ToArray(); From e2b6c045dea2b6729712e5011d07f46f8689f93c Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 10 Jan 2025 21:58:08 -0600 Subject: [PATCH 5/6] Fixed tests --- .../CodeActions/CodeActionsTest.cs | 25 +++++++++---------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs index 4b2cf7b918..a93189153d 100644 --- a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs +++ b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs @@ -136,11 +136,12 @@ method Test() { public async Task TestForallIntroductionFunction() { await TestCodeAction(@" function Test(): int { - (>Insert a forall statement->forall i | i % 4 == 1 ensures i % 2 == 0 { - assert i % 2 == 0; + assert for>Insert a forall statement-> by { + forall i: int | i % 4 == 1 ensures i % 2 == 0 { + assert i % 2 == 0; + } } - <)assert for>Insert explicit failing assertion->assert i + 1 != 0; <)2 >Insert explicit failing assertion-> by { - assert i + 1 != 0; - }:::;<) + var x := b && (>Insert explicit failing assertion->assert i + 1 != 0; + <)2 >Insert explicit failing assertion->assert i + 1 != 0; <)var x := 2 >Insert explicit failing assertion->(assert i + 1 != 0; 2 / (i + 1) == j):::2 >Insert explicit failing assertion-> by { - assert i + 1 != 0; - }:::;<) + var x := (>Insert explicit failing assertion->(assert i + 1 != 0; + 2 / (i + 1) == j):::2 > Date: Mon, 13 Jan 2025 05:19:38 -0600 Subject: [PATCH 6/6] Fixed last CI test --- .../DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs index a93189153d..f1d2352731 100644 --- a/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs +++ b/Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs @@ -140,8 +140,8 @@ function Test(): int { forall i: int | i % 4 == 1 ensures i % 2 == 0 { assert i % 2 == 0; } - } - :::;<)1 + }:::;<) + 1 }"); }