Fix: Formatting for parameter default values (#3946)

This PR fixes #3944. I first recreated the issue with a test, and then
fixed it.
It turned out, formals had a field "DefaultValue" which was never
considered as a child, so its tokens were considered to be part of the
declaration, which messed up indentation.
The fix was to ensure Formals now take the default value also in their
range, and also in their children.

Source/DafnyCore/AST/DafnyAst.cs

@@ -651,6 +651,11 @@ public bool HasName {
       sanitizedName ??= SanitizeName(Name); // No unique-ification
     public override string CompileName =>
       compileName ??= SanitizeName(NameForCompilation);
+
+    public override IEnumerable<Node> Children =>
+      DefaultValue != null ? new List<Node>() { DefaultValue } : Enumerable.Empty<Node>();
+
+    public override IEnumerable<Node> PreResolveChildren => Children;
   }
 
   /// <summary>

Source/DafnyCore/Dafny.atg

@@ -2200,12 +2200,12 @@ Formals<.bool incoming, bool allowGhostKeyword, bool allowNewKeyword, bool allow
     GIdentType<allowGhostKeyword, allowNewKeyword, incoming, allowOlderKeyword, out range, out name, out ty, out isGhost, out isOld, out isNameOnly, out isOlder>
     ParameterDefaultValue<incoming, out defaultValue>
                  (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, isOld, isNameOnly, isOlder)
-                        { RangeToken = range, IsTypeExplicit = ty != null }
+                        { RangeToken = defaultValue != null ? new RangeToken(range.StartToken, defaultValue.EndToken) : range, IsTypeExplicit = ty != null }
                     ); .)
     { "," GIdentType<allowGhostKeyword, allowNewKeyword, incoming, allowOlderKeyword, out range, out name, out ty, out isGhost, out isOld, out isNameOnly, out isOlder>
     ParameterDefaultValue<incoming, out defaultValue>
                  (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, isOld, isNameOnly, isOlder)
-                        { RangeToken = range, IsTypeExplicit = ty != null }
+                        { RangeToken = defaultValue != null ? new RangeToken(range.StartToken, defaultValue.EndToken) : range, IsTypeExplicit = ty != null }
                     ); .)
     }
   ]

Source/DafnyPipeline.Test/FormatterIssues.cs

@@ -4,6 +4,19 @@ namespace DafnyPipeline.Test;
 
 [Collection("Singleton Test Collection - FormatterForTopLevelDeclarations")]
 public class FormatterIssues : FormatterBaseTest {
+  [Fact]
+  public void GitIssue3944FormatterArgumentsDefaultValue() {
+    FormatterWorksFor(@"
+function Example(
+  newNames : map<string, string> := map[],
+  a: int
+) : bool
+{
+  true
+}
+");
+  }
+
   [Fact]
   public void GitIssue3790DafnyFormatterProducesIncorrectIndentation() {
     FormatterWorksFor(@"

docs/dev/news/3944.fix

@@ -0,0 +1 @@
+Formatting for parameter default values