Feat code actions forall calc (#6044)

### What was changed?
First, for implicit assertions, if they are surrounded by a declaration
that supports by clause (like AssertStmt or CallStmt), the by clause is
preferred to inserting the assertion before.

![InsertVarByStatement](https://github.com/user-attachments/assets/add8e4c4-f4e1-4818-9374-0c69dd10e387)
And that works also for well-formedness, since well-formedness is now
proved by by-blocks (thanks @keyboardDrummer for that, and @alex-chew
for creating Dafny expressions for well-formedness)

![InsertAssertByPreconditionStatement](https://github.com/user-attachments/assets/7b4fe592-abf6-4b31-9ee3-3cfc75749284)
Moreover, if a by clause already exist, the code action will insert into
it.

![InsertAssertExistingByPreconditionStatement](https://github.com/user-attachments/assets/bce3c787-1655-410d-9dc6-52fe924a976c)

Second, assertion of foralls now support a proof sketch by inserting
forall statement

![InsertForallStatement](https://github.com/user-attachments/assets/c411570d-8f33-463f-ab7a-af093a594a31)

Third, assertions of equalities or equivalence now support a proof
sketch by inserting a calc statement.

![InsertCalcStatement](https://github.com/user-attachments/assets/fb76312a-51b5-4325-a0cd-457ef5dc444e)

![InsertCalcEquivStatement](https://github.com/user-attachments/assets/68d12a15-684a-4f97-bd66-fa86ca8ad348)

The code for inserting such proof sketches has been refactored so that
it will be even more easy to extend in the future.

### How has this been tested?
- Tests were updated for the insertion point (var....by) when possible
and insert there if it already exist.
- Tests were added for foralls, equalities and equivalences, and also
new insertion points

<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>

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<Expression> expressions, [CanBeNull] PrintFlags printFlags = null) {
       Contract.Requires(expressions != null);
       using var wr = new StringWriter();

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;
@@ -108,14 +109,104 @@ 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 for><all i | i % 4 == 1 :: i % 2 == 0(>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 {
+  assert for><all i | i % 4 == 1 :: i % 2 == 0(>Insert a forall statement-> by {
+    forall i: int | i % 4 == 1 ensures i % 2 == 0 {
+      assert i % 2 == 0;
+    }
+  }:::;<)
+  1
+}");
+    }
+
     [Fact]
     public async Task GitIssue4401CorrectInsertionPlace() {
       await TestCodeAction(@"
 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);
+  }:::;<)
+}");
+    }
+
+    [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);
+  <)}
 }");
     }
 
@@ -126,9 +217,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);
+      }:::;<)
     }
   }
 }");
@@ -254,17 +346,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 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 ExplicitDivisionImp() {
+    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 ></ (i + 1) == j;
+  x
+}");
+    }
+
+    [Fact]
+    public async Task ExplicitDivisionImpImpMethod() {
+      await TestCodeAction(@"
+method Foo(b: bool, i: int, j: int)
+{
+  var x := b ==> b ==> (>Insert explicit failing assertion->assert i + 1 != 0;
+                       <)2 ></ (i + 1) == j;
+}");
+    }
+
+    [Fact]
+    public async Task ExplicitDivisionImpMethod() {
       await TestCodeAction(@"
 method Foo(b: bool, i: int, j: int)
 {
@@ -278,28 +403,53 @@ 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 ></ (i + 1) == j ==> b;
+  var x := 2 ></ (i + 1) == j ==> b(>Insert explicit failing assertion-> by {
+    assert i + 1 != 0;
+  }:::;<)
 }");
     }
 
     [Fact]
-    public async Task ExplicitDivisionAnd() {
+    public async Task ExplicitDivisionAndFunction() {
       await TestCodeAction(@"
-method Foo(b: bool, i: int, j: int)
+function Foo(b: bool, i: int, j: int): bool
 {
   var x := b && (>Insert explicit failing assertion->assert i + 1 != 0;
                 <)2 ></ (i + 1) == j;
+  x
 }");
     }
 
+
     [Fact]
-    public async Task ExplicitDivisionAnd2() {
+    public async Task ExplicitDivisionAndMethod() {
       await TestCodeAction(@"
 method Foo(b: bool, i: int, j: int)
+{
+  var x := b && (>Insert explicit failing assertion->assert i + 1 != 0;
+                <)2 ></ (i + 1) == j;
+}");
+    }
+
+    [Fact]
+    public async Task ExplicitDivisionAnd2Function() {
+      await TestCodeAction(@"
+function Foo(b: bool, i: int, j: int): bool
 {
   (>Insert explicit failing assertion->assert i + 1 != 0;
   <)var x := 2 ></ (i + 1) == j && b;
+  x
+}");
+    }
+
+    [Fact]
+    public async Task ExplicitDivisionAnd2Method() {
+      await TestCodeAction(@"
+method Foo(b: bool, i: int, j: int)
+{
+  var x := 2 ></ (i + 1) == j && b(>Insert explicit failing assertion-> by {
+    assert i + 1 != 0;
+  }:::;<)
 }");
     }
 
@@ -319,35 +469,69 @@ 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 ></ (i + 1) == j || b;
+  var x := 2 ></ (i + 1) == j || b(>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 ></ match b case true => 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 ></ match b case true => 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 ></ (i + 1) == j(>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 ></ (i + 1) == j;
+  2
+}");
+    }
+
+    [Fact]
+    public async Task ExplicitDivisionExp2Function() {
+      await TestCodeAction(@"
+function Foo(b: bool, i: int, j: int): bool
+{
+  var x := (>Insert explicit failing assertion->(assert i + 1 != 0;
+            2 / (i + 1) == j):::2 ></ (i + 1) == j<) <== b;
+  x
 }");
     }
 
     [Fact]
-    public async Task ExplicitDivisionExp2() {
+    public async Task ExplicitDivisionExp2Method() {
       await TestCodeAction(@"
 method Foo(b: bool, i: int, j: int)
 {
@@ -357,7 +541,7 @@ method Foo(b: bool, i: int, j: int)
     }
 
     [Fact]
-    public async Task ExplicitDivisionByZeroFunction() {
+    public async Task ExplicitDivisionByZeroIfFunction() {
       await TestCodeAction(@"
 function Foo(i: int): int
 {
@@ -372,7 +556,7 @@ function Foo(i: int): int
 
 
     [Fact]
-    public async Task ExplicitDivisionByZeroFunctionLetExpr() {
+    public async Task ExplicitDivisionByZeroMatchFunctionLetExpr() {
       await TestCodeAction(@"
 function Foo(i: int): int
 {
@@ -410,7 +594,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();
@@ -441,8 +627,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)}");
+        }
       }
     }