From 5f31e938c1bf5bb2d6d2d29b26ea932ade115357 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sat, 10 Aug 2024 09:54:39 -0700
Subject: [PATCH] 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 |  6 ++++
 tests/lean/run/delabApp.lean                  | 34 +++++++++++++++++++
 2 files changed, 40 insertions(+)

diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index 3c5ca19fc23c..bf0de8759ebd 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/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
diff --git a/tests/lean/run/delabApp.lean b/tests/lean/run/delabApp.lean
index 4c96e3486558..4d640dedf054 100644
--- a/tests/lean/run/delabApp.lean
+++ b/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)