From 0f5dceda4b6ac42f214f4918321ad050abc79891 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Mon, 3 Feb 2025 12:15:52 +0100 Subject: [PATCH] feat: `recommended_spelling` command (#6869) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- src/Lean/DocString.lean | 5 +- src/Lean/Elab.lean | 1 + src/Lean/Elab/RecommendedSpelling.lean | 34 ++++++++++ src/Lean/Parser/Command.lean | 45 +++++++++++++- src/Lean/Parser/Term.lean | 1 + src/Lean/Parser/Term/Doc.lean | 83 +++++++++++++++++++++++++ tests/lean/run/recommendedSpelling.lean | 64 +++++++++++++++++++ 7 files changed, 230 insertions(+), 3 deletions(-) create mode 100644 src/Lean/Elab/RecommendedSpelling.lean create mode 100644 src/Lean/Parser/Term/Doc.lean create mode 100644 tests/lean/run/recommendedSpelling.lean diff --git a/src/Lean/DocString.lean b/src/Lean/DocString.lean index d288228209..15c0fb12b2 100644 --- a/src/Lean/DocString.lean +++ b/src/Lean/DocString.lean @@ -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) diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean index 9f0ee92028..8f72567832 100644 --- a/src/Lean/Elab.lean +++ b/src/Lean/Elab.lean @@ -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 diff --git a/src/Lean/Elab/RecommendedSpelling.lean b/src/Lean/Elab/RecommendedSpelling.lean new file mode 100644 index 0000000000..5657f30239 --- /dev/null +++ b/src/Lean/Elab/RecommendedSpelling.lean @@ -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 diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 73a94a5b0f..2a3808a841 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -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 diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 639b534e76..7014ff76c7 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -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 diff --git a/src/Lean/Parser/Term/Doc.lean b/src/Lean/Parser/Term/Doc.lean new file mode 100644 index 0000000000..d4305fdd27 --- /dev/null +++ b/src/Lean/Parser/Term/Doc.lean @@ -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 diff --git a/tests/lean/run/recommendedSpelling.lean b/tests/lean/run/recommendedSpelling.lean new file mode 100644 index 0000000000..d62ba1d476 --- /dev/null +++ b/tests/lean/run/recommendedSpelling.lean @@ -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 "☋"