From 445040b33fabf57645a92abcf498beb3baa73dd7 Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Wed, 3 May 2023 09:23:18 -0500
Subject: [PATCH] Fix: Formatting for parameter default values

---
 Source/DafnyCore/AST/DafnyAst.cs             |  5 +++++
 Source/DafnyCore/Dafny.atg                   |  4 ++--
 Source/DafnyPipeline.Test/FormatterIssues.cs | 13 +++++++++++++
 docs/dev/news/3944.fix                       |  1 +
 4 files changed, 21 insertions(+), 2 deletions(-)
 create mode 100644 docs/dev/news/3944.fix

diff --git a/Source/DafnyCore/AST/DafnyAst.cs b/Source/DafnyCore/AST/DafnyAst.cs
index 2f52b11b533..c3534fd3f8e 100644
--- a/Source/DafnyCore/AST/DafnyAst.cs
+++ b/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>
diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg
index 98c10719c7e..28bab375efb 100644
--- a/Source/DafnyCore/Dafny.atg
+++ b/Source/DafnyCore/Dafny.atg
@@ -2199,12 +2199,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 }
                     ); .)
     }
   ]
diff --git a/Source/DafnyPipeline.Test/FormatterIssues.cs b/Source/DafnyPipeline.Test/FormatterIssues.cs
index 178c1f51cce..0e9ce803957 100644
--- a/Source/DafnyPipeline.Test/FormatterIssues.cs
+++ b/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(@"
diff --git a/docs/dev/news/3944.fix b/docs/dev/news/3944.fix
new file mode 100644
index 00000000000..8dd5df37f33
--- /dev/null
+++ b/docs/dev/news/3944.fix
@@ -0,0 +1 @@
+Formatting for parameter default values
\ No newline at end of file