feat: recommended_spelling command (#6869)
This PR adds a `recommended_spelling` command, which can be used for recording the recommended spelling of a notation (for example, that the recommended spelling of `∧` in identifiers is `and`). This information is then appended to the relevant docstrings for easy lookup. The function `Lean.Elab.Term.Doc.allRecommendedSpellings` may be used to obtain a list of all recommended spellings, for example to create a table that is part of a style guide. In the future, it might be desirable to be able to partition such a table into smaller tables by category. This can be added in a future PR. The implementation is heavily inspired by #4490.
This commit is contained in:
Markus Himmel
GitHub
parent
13e2a0291c
commit
0f5dceda4b
7 changed files with 230 additions and 3 deletions
|
|
@ -6,6 +6,7 @@ Authors: Leonardo de Moura
|
|||
prelude
|
||||
import Lean.DocString.Extension
|
||||
import Lean.Parser.Tactic.Doc
|
||||
import Lean.Parser.Term.Doc
|
||||
|
||||
set_option linter.missingDocs true
|
||||
|
||||
|
|
@ -15,6 +16,7 @@ set_option linter.missingDocs true
|
|||
|
||||
namespace Lean
|
||||
open Lean.Parser.Tactic.Doc
|
||||
open Lean.Parser.Term.Doc
|
||||
|
||||
/--
|
||||
Finds the docstring for a name, taking tactic alternate forms and documentation extensions into
|
||||
|
|
@ -26,4 +28,5 @@ including extensions.
|
|||
def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) := do
|
||||
let declName := alternativeOfTactic env declName |>.getD declName
|
||||
let exts := getTacticExtensionString env declName
|
||||
return (← findSimpleDocString? env declName (includeBuiltin := includeBuiltin)).map (· ++ exts)
|
||||
let spellings := getRecommendedSpellingString env declName
|
||||
return (← findSimpleDocString? env declName (includeBuiltin := includeBuiltin)).map (· ++ exts ++ spellings)
|
||||
|
|
|
|||
|
|
@ -54,3 +54,4 @@ import Lean.Elab.CheckTactic
|
|||
import Lean.Elab.MatchExpr
|
||||
import Lean.Elab.Tactic.Doc
|
||||
import Lean.Elab.Time
|
||||
import Lean.Elab.RecommendedSpelling
|
||||
|
|
|
|||
34
src/Lean/Elab/RecommendedSpelling.lean
Normal file
34
src/Lean/Elab/RecommendedSpelling.lean
Normal file
|
|
@ -0,0 +1,34 @@
|
|||
/-
|
||||
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Markus Himmel
|
||||
-/
|
||||
prelude
|
||||
import Lean.Parser.Term.Doc
|
||||
import Lean.Parser.Command
|
||||
import Lean.Elab.Command
|
||||
|
||||
namespace Lean.Elab.Term.Doc
|
||||
open Lean.Parser.Term.Doc
|
||||
open Lean.Elab.Command
|
||||
open Lean.Parser.Command
|
||||
|
||||
@[builtin_command_elab «recommended_spelling»] def elabRecommendedSpelling : CommandElab
|
||||
| `(«recommended_spelling»|$[$docs:docComment]? recommended_spelling $spelling:str for $«notation»:str in [$[$decls:ident],*]) => do
|
||||
let declNames ← liftTermElabM <| decls.mapM (fun decl => realizeGlobalConstNoOverloadWithInfo decl)
|
||||
let recommendedSpelling : RecommendedSpelling := {
|
||||
«notation» := «notation».getString
|
||||
recommendedSpelling := spelling.getString
|
||||
additionalInformation? := docs.map (·.getDocString)
|
||||
}
|
||||
modifyEnv (addRecommendedSpelling · recommendedSpelling declNames)
|
||||
| _ => throwError "Malformed recommended spelling command"
|
||||
|
||||
/-- Returns an array containing all recommended spellings. -/
|
||||
def allRecommendedSpellings : MetaM (Array RecommendedSpelling) := do
|
||||
let all := recommendedSpellingExt.toEnvExtension.getState (← getEnv)
|
||||
|>.importedEntries
|
||||
|>.push (recommendedSpellingExt.exportEntriesFn (recommendedSpellingExt.getState (← getEnv)))
|
||||
return all.flatMap id
|
||||
|
||||
end Lean.Elab.Term.Doc
|
||||
|
|
@ -736,7 +736,7 @@ Documentation can only be added to declarations in the same module.
|
|||
docComment >> "add_decl_doc " >> ident
|
||||
|
||||
/--
|
||||
Register a tactic tag, saving its user-facing name and docstring.
|
||||
Registers a tactic tag, saving its user-facing name and docstring.
|
||||
|
||||
Tactic tags can be used by documentation generation tools to classify related tactics.
|
||||
-/
|
||||
|
|
@ -745,7 +745,7 @@ Tactic tags can be used by documentation generation tools to classify related ta
|
|||
"register_tactic_tag " >> ident >> strLit
|
||||
|
||||
/--
|
||||
Add more documentation as an extension of the documentation for a given tactic.
|
||||
Adds more documentation as an extension of the documentation for a given tactic.
|
||||
|
||||
The extended documentation is placed in the command's docstring. It is shown as part of a bulleted
|
||||
list, so it should be brief.
|
||||
|
|
@ -754,6 +754,47 @@ list, so it should be brief.
|
|||
optional (docComment >> ppLine) >>
|
||||
"tactic_extension " >> ident
|
||||
|
||||
/--
|
||||
Documents a recommended spelling for a notation in identifiers.
|
||||
|
||||
Theorems should generally be systematically named after their statement, rather than creatively.
|
||||
Non-identifier notations should be referred to consistently by their recommended spelling.
|
||||
|
||||
```
|
||||
/-- some additional info -/
|
||||
recommended_spelling "and" for "∧" in [And, «term_∧_»]
|
||||
```
|
||||
|
||||
will do the following:
|
||||
* Adds the sentence "The recommended spelling of `∧` in identifiers is `and` (some additional info)."
|
||||
to the end of the docstring for `And` and for `∧`. If the additional info is more than a single
|
||||
line, it will be placed below the sentence instead of in parentheses.
|
||||
* Registers this information in an environment extension, so that it will later be possible to
|
||||
generate a table with all recommended spellings.
|
||||
|
||||
You can add attach the recommended spelling to as many declarations as you want. It is recommended
|
||||
to attach the recommended spelling to all relevant parsers as well as the declaration the parsers
|
||||
refer to (if such a declaration exists). Note that the `inherit_doc` attribute does *not* copy
|
||||
recommended spellings, so even though the parser for `∧` uses `@[inherit_doc And]`, we have to
|
||||
attach the recommended spelling to both `And` and `«term_∧_»`.
|
||||
|
||||
The `syntax`, `macro`, `elab` and `notation` commands accept a `(name := parserName)` option to
|
||||
assign a name to the created parser so that you do not have to guess the automatically generated
|
||||
name. The `synax`, `macro` and `elab` commands can be hovered to see the name of the parser.
|
||||
|
||||
For complex notations which enclose identifiers, the convention is to use example identifiers rather
|
||||
than other placeholders. This is an example following the convention:
|
||||
```
|
||||
recommended_spelling "singleton" for "[a]" in [List.cons, «term[_]»]
|
||||
```
|
||||
Using `[·]` or `[⋯]` or `[…]` instead of `[a]` would be against the convention. When attaching a
|
||||
recommended spelling to a notation whose docstring already has an example, try to reuse the
|
||||
identifier names chosen in the docstring for consistency.
|
||||
-/
|
||||
@[builtin_command_parser] def «recommended_spelling» := leading_parser
|
||||
optional (docComment >> ppLine) >>
|
||||
"recommended_spelling " >> strLit >> " for " >> strLit >> " in " >>
|
||||
"[" >> sepBy1 ident ", " >> "]"
|
||||
|
||||
/--
|
||||
This is an auxiliary command for generation constructor injectivity theorems for
|
||||
|
|
|
|||
|
|
@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich, Mario Carneiro
|
|||
prelude
|
||||
import Lean.Parser.Attr
|
||||
import Lean.Parser.Level
|
||||
import Lean.Parser.Term.Doc
|
||||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
|
|
|
|||
83
src/Lean/Parser/Term/Doc.lean
Normal file
83
src/Lean/Parser/Term/Doc.lean
Normal file
|
|
@ -0,0 +1,83 @@
|
|||
/-
|
||||
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Markus Himmel
|
||||
-/
|
||||
prelude
|
||||
import Lean.Parser.Extension
|
||||
|
||||
/-! Environment extension to register preferred spellings of notations in identifiers. -/
|
||||
|
||||
set_option linter.missingDocs true
|
||||
|
||||
namespace Lean.Parser.Term.Doc
|
||||
|
||||
/-- Information about how to spell a certain notation for an identifier in declaration names. -/
|
||||
structure RecommendedSpelling where
|
||||
/-- The notation in question. -/
|
||||
«notation» : String
|
||||
/-- The recommended spelling of the notation in identifiers. -/
|
||||
recommendedSpelling : String
|
||||
/-- Additional information. -/
|
||||
additionalInformation? : Option String
|
||||
|
||||
/--
|
||||
Recommended spellings for notations, stored in a way so that the recommended spellings for a given
|
||||
declaration are easily accessible.
|
||||
-/
|
||||
builtin_initialize recommendedSpellingByNameExt
|
||||
: PersistentEnvExtension (Name × Array RecommendedSpelling) (RecommendedSpelling × Array Name)
|
||||
(NameMap (Array RecommendedSpelling)) ←
|
||||
registerPersistentEnvExtension {
|
||||
mkInitial := pure {},
|
||||
addImportedFn := fun _ => pure {},
|
||||
addEntryFn := fun es (rec, xs) => xs.foldl (init := es) fun es x => es.insert x (es.findD x #[] |>.push rec),
|
||||
exportEntriesFn := fun es =>
|
||||
es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
|
||||
}
|
||||
|
||||
/-- Recommended spellings for notations, stored in such a way that it is easy to generate a table
|
||||
containing every recommended spelling exactly once. -/
|
||||
builtin_initialize recommendedSpellingExt
|
||||
: PersistentEnvExtension RecommendedSpelling RecommendedSpelling (Array RecommendedSpelling) ←
|
||||
registerPersistentEnvExtension {
|
||||
mkInitial := pure {},
|
||||
addImportedFn := fun _ => pure {},
|
||||
addEntryFn := Array.push,
|
||||
exportEntriesFn := id
|
||||
}
|
||||
|
||||
/-- Adds a recommended spelling to the environment. -/
|
||||
def addRecommendedSpelling (env : Environment) (rec : RecommendedSpelling) (names : Array Name) : Environment :=
|
||||
let env := recommendedSpellingExt.addEntry env rec
|
||||
recommendedSpellingByNameExt.addEntry env (rec, names)
|
||||
|
||||
/-- Returns the recommended spellings associated with the given declaration name. -/
|
||||
def getRecommendedSpellingsForName (env : Environment) (declName : Name) :
|
||||
Array RecommendedSpelling := Id.run do
|
||||
let mut spellings := #[]
|
||||
for modArr in recommendedSpellingByNameExt.toEnvExtension.getState env |>.importedEntries do
|
||||
if let some (_, strs) := modArr.binSearch (declName, #[]) (Name.quickLt ·.1 ·.1) then
|
||||
spellings := spellings ++ strs
|
||||
if let some strs := recommendedSpellingByNameExt.getState env |>.find? declName then
|
||||
spellings := spellings ++ strs
|
||||
return spellings
|
||||
|
||||
/-- Renders the recommended spellings for the given declaration into a string for appending to
|
||||
the docstring. -/
|
||||
def getRecommendedSpellingString (env : Environment) (declName : Name) : String := Id.run do
|
||||
let spellings := getRecommendedSpellingsForName env declName
|
||||
if spellings.size == 0 then ""
|
||||
else "\n\nConventions for notations in identifiers:\n\n" ++ String.join (spellings.toList.map bullet) |>.trimRight
|
||||
where
|
||||
indentLine (str : String) : String :=
|
||||
(if str.all (·.isWhitespace) then str else " " ++ str) ++ "\n"
|
||||
bullet (spelling : RecommendedSpelling) : String :=
|
||||
let firstLine := s!" * The recommended spelling of `{spelling.«notation»}` in identifiers is `{spelling.recommendedSpelling}`"
|
||||
let additionalInfoLines := spelling.additionalInformation?.map (·.splitOn "\n")
|
||||
match additionalInfoLines with
|
||||
| none | some [] => firstLine ++ ".\n\n"
|
||||
| some [l] => firstLine ++ s!" ({l.trimRight}).\n\n"
|
||||
| some ls => firstLine ++ ".\n\n" ++ String.join (ls.map indentLine) ++ "\n\n"
|
||||
|
||||
end Lean.Parser.Term.Doc
|
||||
64
tests/lean/run/recommendedSpelling.lean
Normal file
64
tests/lean/run/recommendedSpelling.lean
Normal file
|
|
@ -0,0 +1,64 @@
|
|||
import Lean
|
||||
|
||||
/-!
|
||||
Test the `recommended_spelling` command.
|
||||
|
||||
TODO: once we use this command in Init, we can test that recommended spellings from imported
|
||||
modules are reported correctly.
|
||||
-/
|
||||
|
||||
/--
|
||||
Conjuction
|
||||
|
||||
Second line
|
||||
-/
|
||||
inductive MyAnd (P Q : Prop) : Prop where
|
||||
| intro : P → Q → MyAnd P Q
|
||||
|
||||
@[inherit_doc] infixr:35 " ☃ " => MyAnd
|
||||
@[inherit_doc] infixr:35 " ☋ " => MyAnd
|
||||
|
||||
recommended_spelling "snowmand" for "☃" in [MyAnd, «term_☃_»]
|
||||
/-- the preferred notation is `∧`.
|
||||
|
||||
more stuff
|
||||
|
||||
even more stuff
|
||||
|
||||
hello
|
||||
|
||||
-/
|
||||
recommended_spelling "orbitalAnd" for "☋" in [MyAnd, «term_☋_»]
|
||||
/-- Docstring -/
|
||||
recommended_spelling "and" for "something" in [«term_☃_», «term_☋_»]
|
||||
|
||||
def findDocString? (n : Lean.Name) : Lean.MetaM (Option String) := do
|
||||
Lean.findDocString? (← Lean.getEnv) n
|
||||
|
||||
/--
|
||||
info: some
|
||||
"Conjuction\n\nSecond line\n\n\nConventions for notations in identifiers:\n\n * The recommended spelling of `☃` in identifiers is `snowmand`.\n\n * The recommended spelling of `☋` in identifiers is `orbitalAnd`.\n\n the preferred notation is `∧`.\n\n more stuff\n\n even more stuff\n\n hello"
|
||||
-/
|
||||
#guard_msgs in
|
||||
#eval findDocString? `MyAnd
|
||||
|
||||
/--
|
||||
info: some
|
||||
"Conjuction\n\nSecond line\n\n\nConventions for notations in identifiers:\n\n * The recommended spelling of `☃` in identifiers is `snowmand`.\n\n * The recommended spelling of `something` in identifiers is `and` (Docstring)."
|
||||
-/
|
||||
#guard_msgs in
|
||||
#eval findDocString? `«term_☃_»
|
||||
|
||||
/--
|
||||
info: some
|
||||
"Conjuction\n\nSecond line\n\n\nConventions for notations in identifiers:\n\n * The recommended spelling of `☋` in identifiers is `orbitalAnd`.\n\n the preferred notation is `∧`.\n\n more stuff\n\n even more stuff\n\n hello\n\n\n\n\n * The recommended spelling of `something` in identifiers is `and` (Docstring)."
|
||||
-/
|
||||
#guard_msgs in
|
||||
#eval findDocString? `«term_☋_»
|
||||
|
||||
/-- info: 1 -/
|
||||
#guard_msgs in
|
||||
#eval do
|
||||
return (← Lean.Elab.Term.Doc.allRecommendedSpellings)
|
||||
|>.map Lean.Parser.Term.Doc.RecommendedSpelling.«notation»
|
||||
|>.count "☋"
|
||||
Loading…
Add table
Reference in a new issue