feat: @[app_delab] (#4976)

Adds `@[app_delab ident]` as a macro for `@[delab app.ident]`. Resolves
the identifier when expanding the macro, saving needing to use the fully
qualified identifiers that `@[delab]` requires. Also, unlike `@[delab]`,
throws an error if the identifier cannot be resolved.

Closes #4899

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -123,6 +123,12 @@ unsafe def mkDelabAttribute : IO (KeyedDeclsAttribute Delab) :=
   } `Lean.PrettyPrinter.Delaborator.delabAttribute
 @[builtin_init mkDelabAttribute] opaque delabAttribute : KeyedDeclsAttribute Delab
 
+macro "app_delab" id:ident : attr => do
+  match ← Macro.resolveGlobalName id.getId with
+  | [] => Macro.throwErrorAt id s!"unknown declaration '{id.getId}'"
+  | [(c, [])] => `(attr| delab $(mkIdentFrom (canonical := true) id (`app ++ c)))
+  | _ => Macro.throwErrorAt id s!"ambiguous declaration '{id.getId}'"
+
 def getExprKind : DelabM Name := do
   let e ← getExpr
   pure $ match e with

tests/lean/run/delabApp.lean

@@ -1,3 +1,4 @@
+import Lean
 /-!
 # Testing features of the app delaborator, including overapplication
 -/
@@ -77,3 +78,36 @@ def g (a : Nat) (b := 1) (c := 2) (d := 3) := a + b + c + d
 -- Both the `start` and `stop` arguments are omitted.
 /-- info: fun a => Array.foldl (fun x y => x + y) 0 a : Array Nat → Nat -/
 #guard_msgs in #check fun (a : Array Nat) => a.foldl (fun x y => x + y) 0
+
+
+/-!
+Testing overriding the app delaborator with an `@[app_delab]`
+-/
+
+def myFun (x : Nat) : Nat := x
+
+/-- info: myFun 2 : Nat -/
+#guard_msgs in #check myFun 2
+
+open Lean PrettyPrinter Delaborator in
+@[app_delab myFun] def delabMyFun : Delab := withOverApp 0 `(id)
+
+/-- info: id✝ 2 : Nat -/
+#guard_msgs in #check myFun 2
+
+/-!
+Testing `@[app_delab]` error conditions.
+-/
+
+/-- error: unknown declaration 'noSuchFunction' -/
+#guard_msgs in
+open Lean PrettyPrinter Delaborator in
+@[app_delab noSuchFunction] def delabErr1 : Delab := withOverApp 0 `(id)
+
+def A.f := 0
+def B.f := 0
+open A B
+/-- error: ambiguous declaration 'f' -/
+#guard_msgs in
+open Lean PrettyPrinter Delaborator in
+@[app_delab f] def delabErr2 : Delab := withOverApp 0 `(id)