feat: @[builtin_doc] attribute (part 1)

leanprover · Apr 15, 2024 · 6ab7804 · 6ab7804
1 parent 23aacde
commit 6ab7804
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 10 deletions.
diff --git a/src/Lean/BuiltinDocAttr.lean b/src/Lean/BuiltinDocAttr.lean
@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Compiler.InitAttr
+import Lean.DocString
+
+namespace Lean
+
+def declareBuiltinDocStringAndRanges (declName : Name) : AttrM Unit := do
+  if let some doc ← findDocString? (← getEnv) declName (includeBuiltin := false) then
+    declareBuiltin (declName ++ `docString) (mkAppN (mkConst ``addBuiltinDocString) #[toExpr declName, toExpr doc])
+  if let some declRanges ← findDeclarationRanges? declName then
+    declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges])
+
+builtin_initialize
+  registerBuiltinAttribute {
+    name  := `builtin_doc
+    descr := "make the docs and location of this declaration available as a builtin"
+    add   := fun decl stx _ => do
+      Attribute.Builtin.ensureNoArgs stx
+      declareBuiltinDocStringAndRanges decl
+  }
+
+end Lean
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
@@ -114,10 +114,7 @@ unsafe def mkElabAttribute (γ) (attrBuiltinName attrName : Name) (parserNamespa
       return kind
     onAdded       := fun builtin declName => do
       if builtin then
-        if let some doc ← findDocString? (← getEnv) declName (includeBuiltin := false) then
-          declareBuiltin (declName ++ `docString) (mkAppN (mkConst ``addBuiltinDocString) #[toExpr declName, toExpr doc])
-        if let some declRanges ← findDeclarationRanges? declName then
-          declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges])
+        declareBuiltinDocStringAndRanges declName
   } attrDeclName
 
 unsafe def mkMacroAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute Macro) :=

diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
@@ -5,9 +5,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
 import Lean.Parser.Basic
-import Lean.Compiler.InitAttr
 import Lean.ScopedEnvExtension
-import Lean.DocString
+import Lean.BuiltinDocAttr
 
 /-! Extensible parsing via attributes -/
 
@@ -488,10 +487,7 @@ private def BuiltinParserAttribute.add (attrName : Name) (catName : Name)
   | Expr.const `Lean.Parser.Parser _ =>
     declareLeadingBuiltinParser catName declName prio
   | _ => throwError "unexpected parser type at '{declName}' (`Parser` or `TrailingParser` expected)"
-  if let some doc ← findDocString? (← getEnv) declName (includeBuiltin := false) then
-    declareBuiltin (declName ++ `docString) (mkAppN (mkConst ``addBuiltinDocString) #[toExpr declName, toExpr doc])
-  if let some declRanges ← findDeclarationRanges? declName then
-    declareBuiltin (declName ++ `declRange) (mkAppN (mkConst ``addBuiltinDeclarationRanges) #[toExpr declName, toExpr declRanges])
+  declareBuiltinDocStringAndRanges declName
   runParserAttributeHooks catName declName (builtin := true)
 
 /--