fixed formatter issue

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -898,7 +898,7 @@ Similar to `delabBinders`, but tracking whether `forallE` is dependent or not.
 See issue #1571
 -/
 private partial def delabForallBinders (delabGroup : Array Syntax → Bool → Syntax → Delab) (curNames : Array Syntax := #[]) (curDep := false) : Delab := do
-  let dep := !(← getExpr).isArrow
+  let dep := !(← getExpr).isArrow || (← getOptionsAtCurrPos).get ppPiBinderNames false
   if !curNames.isEmpty && dep != curDep then
     -- don't group
     delabGroup curNames curDep (← delab)
@@ -926,7 +926,7 @@ def delabForall : Delab := do
     | BinderInfo.instImplicit   => `(bracketedBinderF|[$curNames.back : $stxT])
     | _                         =>
       -- NOTE: non-dependent arrows are available only for the default binder info
-      if dependent || (← getOptionsAtCurrPos).get ppPiBinderNames false then
+      if dependent then
         if prop && !(← getPPOption getPPPiBinderTypes) then
           return ← `(∀ $curNames:ident*, $stxBody)
         else

src/Lean/PrettyPrinter/Formatter.lean

@@ -30,16 +30,18 @@ structure Context where
 
 structure State where
   stxTrav  : Syntax.Traverser
-  -- Textual content of `stack` up to the first whitespace (not enclosed in an escaped ident). We assume that the textual
-  -- content of `stack` is modified only by `pushText` and `pushLine`, so `leadWord` is adjusted there accordingly.
+  /-- Textual content of `stack` up to the first whitespace (not enclosed in an escaped ident). We assume that the textual
+  content of `stack` is modified only by `pushText` and `pushLine`, so `leadWord` is adjusted there accordingly. -/
   leadWord : String := ""
-  -- Whether the generated format begins with the result of an ungrouped category formatter.
+  /-- When the `leadWord` is nonempty, whether it is an identifier. Identifiers get space inserted between them. -/
+  leadWordIdent : Bool := false
+  /-- Whether the generated format begins with the result of an ungrouped category formatter. -/
   isUngrouped : Bool := false
-  -- Whether the resulting format must be grouped when used in a category formatter.
-  -- If the flag is set to false, then categoryParser omits the fill+nest operation.
+  /-- Whether the resulting format must be grouped when used in a category formatter.
+  If the flag is set to false, then categoryParser omits the fill+nest operation. -/
   mustBeGrouped : Bool := true
-  -- Stack of generated Format objects, analogous to the Syntax stack in the parser.
-  -- Note, however, that the stack is reversed because of the right-to-left traversal.
+  /-- Stack of generated Format objects, analogous to the Syntax stack in the parser.
+  Note, however, that the stack is reversed because of the right-to-left traversal. -/
   stack    : Array Format := #[]
 
 end Formatter
@@ -121,7 +123,7 @@ private def push (f : Format) : FormatterM Unit :=
 
 def pushWhitespace (f : Format) : FormatterM Unit := do
   push f
-  modify fun st => { st with leadWord := "", isUngrouped := false }
+  modify fun st => { st with leadWord := "", leadWordIdent := false, isUngrouped := false }
 
 def pushLine : FormatterM Unit :=
   pushWhitespace Format.line
@@ -335,7 +337,7 @@ def parseToken (s : String) : FormatterM ParserState :=
     options := ← getOptions
   } ((← read).table) (Parser.mkParserState s)
 
-def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
+def pushToken (info : SourceInfo) (tk : String) (ident : Bool) : FormatterM Unit := do
   match info with
   | SourceInfo.original _ _ ss _ =>
     -- preserve non-whitespace content (i.e. comments)
@@ -346,23 +348,34 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
         push s!"\n{ss'}"
       else
         push s!"  {ss'}"
-      modify fun st => { st with leadWord := "" }
+      modify fun st => { st with leadWord := "", leadWordIdent := false }
   | _ => pure ()
 
   let st ← get
-  -- If there is no space between `tk` and the next word, see if we would parse more than `tk` as a single token
+  -- If there is no space between `tk` and the next word, see if we should insert a discretionary space.
   if st.leadWord != "" && tk.trimRight == tk then
-    let tk' := tk.trimLeft
-    let t ← parseToken $ tk' ++ st.leadWord
-    if t.pos <= tk'.endPos then
-      -- stopped within `tk` => use it as is, extend `leadWord` if not prefixed by whitespace
+    let insertSpace ← do
+      if ident && st.leadWordIdent then
+        -- Both idents => need space
+        pure true
+      else
+        -- Check if we would parse more than `tk` as a single token
+        let tk' := tk.trimLeft
+        let t ← parseToken $ tk' ++ st.leadWord
+        if t.pos ≤ tk'.endPos then
+          -- stopped within `tk` => use it as is
+          pure false
+        else
+          -- stopped after `tk` => add space
+          pure true
+    if !insertSpace then
+      -- extend `leadWord` if not prefixed by whitespace
       push tk
-      modify fun st => { st with leadWord := if tk.trimLeft == tk then tk ++ st.leadWord else "" }
+      modify fun st => { st with leadWord := if tk.trimLeft == tk then tk ++ st.leadWord else "", leadWordIdent := ident }
     else
-      -- stopped after `tk` => add space
       pushLine
       push tk
-      modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" }
+      modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "", leadWordIdent := ident }
   else
     -- already separated => use `tk` as is
     if st.leadWord == "" then
@@ -372,7 +385,7 @@ def pushToken (info : SourceInfo) (tk : String) : FormatterM Unit := do
       push tk.trimRight
     else
       push tk -- preserve special whitespace for tokens like ":=\n"
-    modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "" }
+    modify fun st => { st with leadWord := if tk.trimLeft == tk then tk else "", leadWordIdent := ident }
 
   match info with
   | SourceInfo.original ss _ _ _ =>
@@ -395,7 +408,7 @@ def symbolNoAntiquot.formatter (sym : String) : Formatter := do
   let stx ← getCur
   if stx.isToken sym then do
     let (Syntax.atom info _) ← pure stx | unreachable!
-    withMaybeTag (getExprPos? stx) (pushToken info sym)
+    withMaybeTag (getExprPos? stx) (pushToken info sym false)
     goLeft
   else do
     trace[PrettyPrinter.format.backtrack] "unexpected syntax '{format stx}', expected symbol '{sym}'"
@@ -410,9 +423,9 @@ def unicodeSymbolNoAntiquot.formatter (sym asciiSym : String) : Formatter := do
   let Syntax.atom info val ← getCur
     | throwError m!"not an atom: {← getCur}"
   if val == sym.trim then
-    pushToken info sym
+    pushToken info sym false
   else
-    pushToken info asciiSym;
+    pushToken info asciiSym false
   goLeft
 
 @[combinator_formatter identNoAntiquot]
@@ -423,14 +436,14 @@ def identNoAntiquot.formatter : Formatter := do
   let id := id.simpMacroScopes
   let table := (← read).table
   let isToken (s : String) : Bool := (table.find? s).isSome
-  withMaybeTag (getExprPos? stx) (pushToken info (id.toString (isToken := isToken)))
+  withMaybeTag (getExprPos? stx) (pushToken info (id.toString (isToken := isToken)) true)
   goLeft
 
 @[combinator_formatter rawIdentNoAntiquot] def rawIdentNoAntiquot.formatter : Formatter := do
   checkKind identKind
   let Syntax.ident info _ id _ ← getCur
     | throwError m!"not an ident: {← getCur}"
-  pushToken info id.toString
+  pushToken info id.toString true
   goLeft
 
 @[combinator_formatter identEq] def identEq.formatter (_id : Name) := rawIdentNoAntiquot.formatter
@@ -441,7 +454,7 @@ def visitAtom (k : SyntaxNodeKind) : Formatter := do
     checkKind k
   let Syntax.atom info val ← pure $ stx.ifNode (fun n => n.getArg 0) (fun _ => stx)
     | throwError m!"not an atom: {stx}"
-  pushToken info val
+  pushToken info val false
   goLeft
 
 @[combinator_formatter charLitNoAntiquot] def charLitNoAntiquot.formatter := visitAtom charLitKind
@@ -490,7 +503,7 @@ def sepByNoAntiquot.formatter (p pSep : Formatter) : Formatter := do
 @[combinator_formatter checkStackTop] def checkStackTop.formatter : Formatter := pure ()
 @[combinator_formatter checkNoWsBefore] def checkNoWsBefore.formatter : Formatter :=
   -- prevent automatic whitespace insertion
-  modify fun st => { st with leadWord := "" }
+  modify fun st => { st with leadWord := "", leadWordIdent := false }
 @[combinator_formatter checkLinebreakBefore] def checkLinebreakBefore.formatter : Formatter := pure ()
 @[combinator_formatter checkTailWs] def checkTailWs.formatter : Formatter := pure ()
 @[combinator_formatter checkColEq] def checkColEq.formatter : Formatter := pure ()

src/lake/Lake/Toml/ParserUtil.lean

@@ -161,7 +161,7 @@ open Formatter Syntax.MonadTraverser in
   let .atom info val := stx
     | trace[PrettyPrinter.format.backtrack] "unexpected syntax '{format stx}', expected atom"
       throwBacktrack
-  withMaybeTag (getSyntaxExprPos? stx) (pushToken info val)
+  withMaybeTag (getSyntaxExprPos? stx) (pushToken info val false)
   goLeft
 
 @[combinator_parenthesizer atom]

tests/lean/run/2846.lean

@@ -48,13 +48,23 @@ def foo' (n n : Nat) (a : Fin ((by clear n; exact n) + 1)) : Fin (n + 1) := 0
 
 /-!
 Named argument after inaccessible name, still stays after the colon.
-But, it does not print using named pi notation since this is not a dependent type.
+Prints with named pi notation.
 -/
 def foo'' : String → (needle : String) → String := fun _ yo => yo
 
-/-- info: foo'' : (a✝needle : String) → String -/
+/-- info: foo'' : String → (needle : String) → String -/
 #guard_msgs in #check foo''
 
+/-!
+Named argument after inaccessible name that's still a dependent argument.
+Stays after the colon, and the names are grouped.
+-/
+
+def foo''' : (_ : Nat) → (n : Nat) → Fin (n + by clear n; assumption) := sorry
+
+/-- info: foo''' : (x✝ n : Nat) → Fin (n + x✝) -/
+#guard_msgs in #check foo'''
+
 /-!
 Named argument after inaccessible name, still stays after the colon.
 Here, because it's a dependent type the named pi notation shows the name.

tests/lean/run/4320.lean

@@ -8,7 +8,7 @@ def many_map {α β : Type} (f : α → β) : Many α → Many β
 
 /--
 info: many_map.induct {α β : Type} (f : α → β) (motive : Many α → Prop) (case1 : motive Many.none)
-  (case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) : ∀ (a : Many α), motive a
+  (case2 : ∀ (x : α) (xs : Unit → Many α), motive (xs ()) → motive (Many.more x xs)) : ∀ (a✝ : Many α), motive a✝
 -/
 #guard_msgs in
 #check many_map.induct

tests/lean/run/5424.lean

@@ -1,3 +1,4 @@
+import Lean
 /-!
 # Long runs of identifiers should include line breaks
 -/
@@ -19,3 +20,12 @@ info: foo
   Nat
 -/
 #guard_msgs(whitespace := exact) in #check foo
+
+/-!
+Issue pointed out by Mario: need spaces between `x✝` and `y✝`.
+-/
+/--
+info: def foo✝ (x✝ y✝ : Nat✝) :=
+  x✝
+-/
+#guard_msgs in #eval do Lean.PrettyPrinter.ppCommand (← `(command| def foo (x y : Nat) := x))

tests/lean/run/974.lean

@@ -12,23 +12,22 @@ attribute [simp] Formula.count_quantifiers
 
 /--
 info: Formula.count_quantifiers.eq_1.{u_1} :
-  ∀ (x : Nat) (f₁ f₂ : Formula x), (f₁.imp f₂).count_quantifiers = f₁.count_quantifiers + f₂.count_quantifiers
+  ∀ (x✝ : Nat) (f₁ f₂ : Formula x✝), (f₁.imp f₂).count_quantifiers = f₁.count_quantifiers + f₂.count_quantifiers
 -/
 #guard_msgs in
 #check Formula.count_quantifiers.eq_1
 
 /--
 info: Formula.count_quantifiers.eq_2.{u_1} :
-  ∀ (x : Nat) (f : Formula (x + 1)), f.all.count_quantifiers = f.count_quantifiers + 1
+  ∀ (x✝ : Nat) (f : Formula (x✝ + 1)), f.all.count_quantifiers = f.count_quantifiers + 1
 -/
 #guard_msgs in
 #check Formula.count_quantifiers.eq_2
 
 /--
 info: Formula.count_quantifiers.eq_3.{u_1} :
-  ∀ (x : Nat) (x_1 : Formula x),
-    (∀ (f₁ f₂ : Formula x), x_1 = f₁.imp f₂ → False) →
-      (∀ (f : Formula (x + 1)), x_1 = f.all → False) → x_1.count_quantifiers = 0
+  ∀ (x✝ : Nat) (x✝¹ : Formula x✝) (x_4 : ∀ (f₁ f₂ : Formula x✝), x✝¹ = f₁.imp f₂ → False)
+    (x_5 : ∀ (f : Formula (x✝ + 1)), x✝¹ = f.all → False), x✝¹.count_quantifiers = 0
 -/
 #guard_msgs in
 #check Formula.count_quantifiers.eq_3

tests/lean/run/eqnsPrio.lean

@@ -11,13 +11,15 @@ def foo : Bool → Nat → Nat
   | _, n+1 => foo .false n
 termination_by _ n => n
 
-/-- info: foo.eq_1 : ∀ (x : Bool), foo x 0 = 0 -/
+/-- info: foo.eq_1 : ∀ (x✝ : Bool), foo x✝ 0 = 0 -/
 #guard_msgs in
 #check foo.eq_1
 /-- info: foo.eq_2 (n : Nat) : foo true n.succ = foo true n -/
 #guard_msgs in
 #check foo.eq_2
-/-- info: foo.eq_3 : ∀ (x : Bool) (n : Nat), (x = true → False) → foo x n.succ = foo false n -/
+/--
+info: foo.eq_3 : ∀ (x✝ : Bool) (n : Nat) (x_3 : x✝ = true → False), foo x✝ n.succ = foo false n
+-/
 #guard_msgs in
 #check foo.eq_3
 

tests/lean/run/funind_demo.lean

@@ -9,7 +9,7 @@ def ackermann : Nat → Nat → Nat
 info: ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
   (case2 : ∀ (n : Nat), motive n 1 → motive n.succ 0)
   (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive n.succ m.succ) :
-  ∀ (a a_1 : Nat), motive a a_1
+  ∀ (a✝ a✝¹ : Nat), motive a✝ a✝¹
 -/
 #guard_msgs in
 #check ackermann.induct
@@ -19,7 +19,7 @@ def Tree.rev : Tree → Tree | node ts => .node (ts.attach.map (fun ⟨t, _ht⟩
 
 /--
 info: Tree.rev.induct (motive : Tree → Prop)
-  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) : ∀ (a : Tree), motive a
+  (case1 : ∀ (ts : List Tree), (∀ (t : Tree), t ∈ ts → motive t) → motive (Tree.node ts)) : ∀ (a✝ : Tree), motive a✝
 -/
 #guard_msgs in
 #check Tree.rev.induct

tests/lean/run/funind_fewer_levels.lean

@@ -11,7 +11,7 @@ def foo.{u} : Nat → PUnit.{u}
 
 /--
 info: Structural.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ) :
-  ∀ (a : Nat), motive a
+  ∀ (a✝ : Nat), motive a✝
 -/
 #guard_msgs in
 #check foo.induct
@@ -31,7 +31,7 @@ termination_by xs => xs
 
 /--
 info: WellFounded.foo.induct.{v} {α : Type v} (motive : List α → Prop) (case1 : motive [])
-  (case2 : ∀ (head : α) (xs : List α), motive xs → motive (head :: xs)) : ∀ (a : List α), motive a
+  (case2 : ∀ (head : α) (xs : List α), motive xs → motive (head :: xs)) : ∀ (a✝ : List α), motive a✝
 -/
 #guard_msgs in
 #check foo.induct
@@ -58,7 +58,7 @@ end
 
 /--
 info: Mutual.foo.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ)
-  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : ∀ (a : Nat), motive1 a
+  (case3 : motive2 0) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) : ∀ (a✝ : Nat), motive1 a✝
 -/
 #guard_msgs in
 #check foo.induct

tests/lean/run/funind_proof.lean

@@ -35,7 +35,7 @@ info: Term.replaceConst.induct (a b : String) (motive1 : Term → Prop) (motive2
   (case1 : ∀ (a_1 : String), (a == a_1) = true → motive1 (const a_1))
   (case2 : ∀ (a_1 : String), ¬(a == a_1) = true → motive1 (const a_1))
   (case3 : ∀ (a : String) (cs : List Term), motive2 cs → motive1 (app a cs)) (case4 : motive2 [])
-  (case5 : ∀ (c : Term) (cs : List Term), motive1 c → motive2 cs → motive2 (c :: cs)) : ∀ (a : Term), motive1 a
+  (case5 : ∀ (c : Term) (cs : List Term), motive1 c → motive2 cs → motive2 (c :: cs)) : ∀ (a✝ : Term), motive1 a✝
 -/
 #guard_msgs in
 #check replaceConst.induct

tests/lean/run/funind_structural.lean

@@ -11,7 +11,7 @@ termination_by structural x => x
 
 /--
 info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
-  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) : ∀ (a : Nat), motive a
+  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) : ∀ (a✝ : Nat), motive a✝
 -/
 #guard_msgs in
 #check fib.induct
@@ -25,7 +25,7 @@ termination_by structural x => x
 /--
 info: binary.induct (motive : Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc) (case2 : ∀ (acc : Nat), motive 1 acc)
   (case3 : ∀ (n acc : Nat), motive (n + 1) acc → motive n (binary (n + 1) acc) → motive n.succ.succ acc) :
-  ∀ (a a_1 : Nat), motive a a_1
+  ∀ (a✝ a✝¹ : Nat), motive a✝ a✝¹
 -/
 #guard_msgs in
 #check binary.induct
@@ -41,7 +41,7 @@ termination_by structural _ x => x
 info: binary'.induct (motive : Bool → Nat → Prop) (case1 : ∀ (acc : Bool), motive acc 0)
   (case2 : ∀ (acc : Bool), motive acc 1)
   (case3 : ∀ (acc : Bool) (n : Nat), motive acc (n + 1) → motive (binary' acc (n + 1)) n → motive acc n.succ.succ) :
-  ∀ (a : Bool) (a_1 : Nat), motive a a_1
+  ∀ (a✝ : Bool) (a✝¹ : Nat), motive a✝ a✝¹
 -/
 #guard_msgs in
 #check binary'.induct
@@ -56,7 +56,7 @@ termination_by structural x => x
 info: zip.induct.{u_1, u_2} {α : Type u_1} {β : Type u_2} (motive : List α → List β → Prop)
   (case1 : ∀ (x : List β), motive [] x) (case2 : ∀ (t : List α), (t = [] → False) → motive t [])
   (case3 : ∀ (x : α) (xs : List α) (y : β) (ys : List β), motive xs ys → motive (x :: xs) (y :: ys)) :
-  ∀ (a : List α) (a_1 : List β), motive a a_1
+  ∀ (a✝ : List α) (a✝¹ : List β), motive a✝ a✝¹
 -/
 #guard_msgs in
 #check zip.induct
@@ -94,7 +94,7 @@ info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n
   (case1 : ∀ (x : Bool) (m n : Nat) (x_1 : Finn n), motive x m Finn.fzero x_1)
   (case2 : ∀ (x : Bool) (m n : Nat) (x_1 : Finn n), (x_1 = Finn.fzero → False) → motive x m x_1 Finn.fzero)
   (case3 : ∀ (x : Bool) (m n : Nat) (i j : Finn n), motive (!x) (m + 1) i j → motive x m i.fsucc j.fsucc) (x : Bool)
-  {n : Nat} (m : Nat) : ∀ (a f : Finn n), motive x m a f
+  {n : Nat} (m : Nat) : ∀ (a✝ f : Finn n), motive x m a✝ f
 -/
 #guard_msgs in
 #check Finn.min.induct
@@ -195,7 +195,7 @@ info: TermDenote.Term.denote.induct (motive : {ctx : List Ty} → {ty : Ty} →
   (case6 :
     ∀ (a : List Ty) (ty ty₁ : Ty) (a_1 : Term a ty₁) (b : Term (ty₁ :: a) ty) (env : HList Ty.denote a),
       motive a_1 env → motive b (HList.cons (a_1.denote env) env) → motive (a_1.let b) env)
-  {ctx : List Ty} {ty : Ty} : ∀ (a : Term ctx ty) (a_1 : HList Ty.denote ctx), motive a a_1
+  {ctx : List Ty} {ty : Ty} : ∀ (a✝ : Term ctx ty) (a✝¹ : HList Ty.denote ctx), motive a✝ a✝¹
 -/
 #guard_msgs in
 #check TermDenote.Term.denote.induct

tests/lean/run/funind_structural_mutual.lean

@@ -26,7 +26,7 @@ info: Tree.size.induct.{u_1} {α : Type u_1} (motive_1 : Tree α → Prop) (moti
   (case1 :
     ∀ (a : α) (tsf : Bool → List (Tree α)), motive_2 (tsf true) → motive_2 (tsf false) → motive_1 (Tree.node a tsf))
   (case2 : motive_2 []) (case3 : ∀ (t : Tree α) (ts : List (Tree α)), motive_1 t → motive_2 ts → motive_2 (t :: ts)) :
-  ∀ (a : Tree α), motive_1 a
+  ∀ (a✝ : Tree α), motive_1 a✝
 -/
 #guard_msgs in
 #check Tree.size.induct