feat: delab Name.mkStr/Num

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -630,8 +630,25 @@ def delabEqNDRec : Delab := whenPPOption getPPNotation do
   `($h ▸ $m)
 
 @[builtinDelab app.Eq.rec]
-def delabEqRec : Delab := whenPPOption getPPNotation do
+def delabEqRec : Delab :=
   -- relevant signature parts as in `Eq.ndrec`
   delabEqNDRec
 
+def reifyName : Expr → DelabM Name
+  | Expr.const ``Lean.Name.anonymous .. => Name.anonymous
+  | Expr.app (Expr.app (Expr.const ``Lean.Name.mkStr ..) n _) (Expr.lit (Literal.strVal s) _) _ => do
+    (← reifyName n).mkStr s
+  | Expr.app (Expr.app (Expr.const ``Lean.Name.mkNum ..) n _) (Expr.lit (Literal.natVal i) _) _ => do
+    (← reifyName n).mkNum i
+  | _ => failure
+
+@[builtinDelab app.Lean.Name.mkStr]
+def delabNameMkStr : Delab := whenPPOption getPPNotation do
+  let n ← reifyName (← getExpr)
+  -- not guaranteed to be a syntactically valid name, but usually more helpful than the explicit version
+  mkNode ``Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{n}"]
+
+@[builtinDelab app.Lean.Name.mkNum]
+def delabNameMkNum : Delab := delabNameMkStr
+
 end Lean.PrettyPrinter.Delaborator

tests/lean/macroResolveName.lean.expected.out

@@ -1,2 +1,2 @@
-some (Name.mkStr (Name.mkStr Name.anonymous "Lean") "Macro") : Option Name
-[(Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "Nat") "succ", [])] : List (Lean.Name × List ?m)
+some `Lean.Macro : Option Name
+[(`Nat.succ, [])] : List (Lean.Name × List ?m)

tests/lean/namelit.lean

@@ -1,4 +1,4 @@
---
+set_option pp.notation false
 
 #check `foo
 #check `foo.bla

tests/lean/syntaxInNamespacesAndPP.lean.expected.out

@@ -19,6 +19,5 @@ bla true
     [Elab.app.finalize] after etaArgs, true : Bool
 [Elab.command] end 
 def Bla.bla : Lean.ParserDescr :=
-Lean.ParserDescr.node (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "Bla") "bla") 1022
-  (Lean.ParserDescr.binary (Lean.Name.mkStr Lean.Name.anonymous "andthen") (Lean.ParserDescr.symbol "bla")
-    (Lean.ParserDescr.cat (Lean.Name.mkStr Lean.Name.anonymous "term") 0))
+Lean.ParserDescr.node `Bla.bla 1022
+  (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "bla") (Lean.ParserDescr.cat `term 0))