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)