From c2edae92c8632b8525ffd34ed518a523d81be956 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 3 Jul 2024 00:45:34 -0700
Subject: [PATCH] fix: make sure syntax nodes always run their formatters
 (#4631)

Now syntax nodes have their formatters run even if the parsers they wrap
are all arity zero. This fixes an issue where if `ppSpace` appears in a
`macro`/`elab` then it does not format with a space due to the fact that
macro argument processing wraps this as `group(ppSpace)`, and `ppSpace`
has arity zero.

Implementation note: the fix is to make the `visitArgs` formatter
combinator always visit the last child, even if it does not exist (in
which case the visited node will be `Syntax.missing`). To compensate,
parser combinators like many and optional need to be sure to keep track
of whether there any children. Only optional's needed to be modified.

Closes #4561
---
 src/Lean/PrettyPrinter/Formatter.lean | 14 +++++---
 tests/lean/run/4561.lean              | 50 +++++++++++++++++++++++++++
 2 files changed, 59 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/4561.lean

diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 7566236190..0f186bddf6 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -129,11 +129,13 @@ def pushLine : FormatterM Unit :=
 def pushAlign (force : Bool) : FormatterM Unit :=
   pushWhitespace (.align force)
 
-/-- Execute `x` at the right-most child of the current node, if any, then advance to the left. -/
+/--
+Execute `x` at the right-most child of the current node, if any, then advance to the left.
+Runs `x` even if there are no children, in which case the current syntax node will be `.missing`.
+-/
 def visitArgs (x : FormatterM Unit) : FormatterM Unit := do
   let stx ← getCur
-  if stx.getArgs.size > 0 then
-    goDown (stx.getArgs.size - 1) *> x <* goUp
+  goDown (stx.getArgs.size - 1) *> x <* goUp
   goLeft
 
 /-- Execute `x`, pass array of generated Format objects to `fn`, and push result. -/
@@ -454,7 +456,9 @@ def manyNoAntiquot.formatter (p : Formatter) : Formatter := do
 @[combinator_formatter many1NoAntiquot] def many1NoAntiquot.formatter (p : Formatter) : Formatter := manyNoAntiquot.formatter p
 
 @[combinator_formatter optionalNoAntiquot]
-def optionalNoAntiquot.formatter (p : Formatter) : Formatter := visitArgs p
+def optionalNoAntiquot.formatter (p : Formatter) : Formatter := do
+  let stx ← getCur
+  visitArgs <| unless stx.getArgs.isEmpty do p
 
 @[combinator_formatter many1Unbox]
 def many1Unbox.formatter (p : Formatter) : Formatter := do
@@ -467,7 +471,7 @@ def many1Unbox.formatter (p : Formatter) : Formatter := do
 @[combinator_formatter sepByNoAntiquot]
 def sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter := do
   let stx ← getCur
-  visitArgs <| (List.range stx.getArgs.size).reverse.forM fun i => if i % 2 == 0 then p else pSep
+  visitArgs <| stx.getArgs.size.forRevM fun i => if i % 2 == 0 then p else pSep
 
 @[combinator_formatter sepBy1NoAntiquot] def sepBy1NoAntiquot.formatter := sepByNoAntiquot.formatter
 
diff --git a/tests/lean/run/4561.lean b/tests/lean/run/4561.lean
new file mode 100644
index 0000000000..a95ce5e930
--- /dev/null
+++ b/tests/lean/run/4561.lean
@@ -0,0 +1,50 @@
+import Lean.Elab.Command
+/-!
+# 4561: group(ppSpace) was not pretty printing with a space
+-/
+
+/-!
+Example from the issue. Here, ppSpace is wrapped in a group due to macro argument handling.
+-/
+macro (name := useSyntax) "use0" ppSpace arg:term : tactic => `(tactic| sorry)
+
+/-- info: use0 .succ✝ 0 -/
+#guard_msgs in
+run_cmd do
+  Lean.logInfo <| ← `(tactic| use0 .succ 0)
+
+/-!
+Version of this using `syntax` to test it without macro argument handling.
+-/
+
+syntax "use1" ppSpace term,+ : tactic
+syntax "use2" group(ppSpace) term,+ : tactic
+
+/--
+info: use1 .succ✝ 0
+---
+info: use2 .succ✝ 0
+-/
+#guard_msgs in
+run_cmd Lean.Elab.Command.liftTermElabM do
+  Lean.logInfo <| ← `(tactic| use1 .succ 0)
+  Lean.logInfo <| ← `(tactic| use2 .succ 0)
+
+/-!
+Check that fix even works inside other nodes.
+-/
+
+syntax myPPSpace := ppSpace
+
+syntax "use3" myPPSpace term,+ : tactic
+syntax "use4" group(myPPSpace) term,+ : tactic
+
+/--
+info: use3 .succ✝ 0
+---
+info: use4 .succ✝ 0
+-/
+#guard_msgs in
+run_cmd Lean.Elab.Command.liftTermElabM do
+  Lean.logInfo <| ← `(tactic| use3 .succ 0)
+  Lean.logInfo <| ← `(tactic| use4 .succ 0)