feat: docstring role for module names, plus improved suggestions (#10533)

This PR adds a docstring role for module names, called `module`. It also
improves the suggestions provided for code elements, making them more
relevant and proposing `lit`.

Author: david-christiansen

src/Lean/Elab/DocString.lean

@@ -1198,7 +1198,10 @@ private def sortSuggestions (ss : Array Meta.Hint.Suggestion) : Array Meta.Hint.
   ss.qsort (cmp ·.suggestion ·.suggestion)
 
 open Diff in
-private def mkSuggestion  (ref : Syntax) (hintTitle : MessageData) (newStrings : Array (String × Option String × Option String)) : DocM MessageData := do
+private def mkSuggestion
+    (ref : Syntax) (hintTitle : MessageData)
+    (newStrings : Array (String × Option String × Option String)) :
+    DocM MessageData := do
   match (← read).suggestionMode with
   | .interactive =>
     hintTitle.hint (newStrings.map fun (s, preInfo?, postInfo?) => { suggestion := s, preInfo?, postInfo? }) (ref? := some ref)
@@ -1268,6 +1271,11 @@ public partial def elabInline (stx : TSyntax `inline) : DocM (Inline ElabInline)
                 snd.snd := moreInfo.map withSpace
               }
           let ss := ss.qsort (fun x y => x.1 < y.1)
+          let litSuggestion :=
+            ( "{lit}" ++ str,
+              some "Use the `lit` role:\n",
+              some "\nto mark the code as literal text and disable suggestions" )
+          let ss := ss.push litSuggestion
           let hint ← mkSuggestion stx m!"Insert a role to document it:" ss
           logWarning m!"Code element could be more specific.{hint}"
     return .code s.getString
@@ -1293,7 +1301,7 @@ public partial def elabInline (stx : TSyntax `inline) : DocM (Inline ElabInline)
             continue
           else throw e
         | e => throw e
-    throwErrorAt name "No expander for `{name}`"
+    throwErrorAt name "Unkown role `{name}`"
   | other =>
     throwErrorAt other "Unsupported syntax {other}"
 where
@@ -1359,7 +1367,7 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
             continue
           else throw e
         | e => throw e
-    throwErrorAt name "No directive expander for `{name}`"
+    throwErrorAt name "Unknown directive `{name}`"
   | `(block| ```%$opener | $s ```) =>
     if doc.verso.suggestions.get (← getOptions) then
       if let some ⟨b, e⟩ := opener.getRange? then
@@ -1402,7 +1410,7 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
             continue
           else throw e
         | e => throw e
-    throwErrorAt name "No code block expander for `{name}`"
+    throwErrorAt name "Unknown code block `{name}`"
   | `(block| command{$name $args*}) =>
     let expanders ← commandExpandersFor name
     for (exName, ex) in expanders do
@@ -1421,7 +1429,7 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
             continue
           else throw e
         | e => throw e
-    throwErrorAt name "No document command elaborator for `{name}`"
+    throwErrorAt name "Unknown document command `{name}`"
   | `(block|%%%$_*%%%) =>
     let h ←
       if stx.raw.getRange?.isSome then m!"Remove it".hint #[""] (ref? := stx)

src/Lean/Elab/DocString/Builtin.lean

@@ -106,6 +106,13 @@ structure Data.Syntax where
   stx : Lean.Syntax
 deriving TypeName
 
+/-- The code represents a module name. -/
+structure Data.ModuleName where
+  /-- The module. -/
+  «module» : Name
+deriving TypeName
+
+
 private def onlyCode [Monad m] [MonadError m] (xs : TSyntaxArray `inline) : m StrLit := do
   if h : xs.size = 1 then
     match xs[0] with
@@ -177,6 +184,61 @@ def name (full : Option Ident := none) (scope : DocScope := .local) (xs : TSynta
     }
     return .other { name := ``PostponedCheck, val := .mk val } #[.code s.getString]
 
+private def similarNames (x : Name) (xs : Array Name) : Array Name := Id.run do
+  let s := x.toString
+  let mut threshold := if s.length < 5 then 1 else if s.length < 8 then 2 else 3
+  let mut candidates := #[]
+  for x in xs do
+    if let some d ← levenshtein s x.toString threshold then
+      if d < threshold then threshold := d
+      if d ≤ threshold then candidates := candidates.push (x, d)
+  -- Only keep the smallest distance
+  return candidates.filterMap fun (x, d) => do
+    guard (d ≤ threshold)
+    pure x
+
+/--
+Displays a name, without attempting to elaborate implicit arguments.
+-/
+@[builtin_doc_role]
+def module (checked : flag true) (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
+  let s ← onlyCode xs
+  let x := s.getString.toName
+  let n := mkIdentFrom' s x
+  if checked then
+    let env ← getEnv
+    if x ∉ env.header.moduleNames then
+      let ss := similarNames x env.header.moduleNames
+      let ref ← getRef
+      let unchecked : Option Meta.Hint.Suggestion ←
+        match ref with
+        | `(inline|role{$x +checked}%$tk2[$_]) =>
+          let some b := x.raw.getTailPos?
+            | pure none
+          let some e := tk2.getPos?
+            | pure none
+          pure <| some {
+            span? := some (Syntax.mkStrLit ((← getFileMap).source.extract b e) (info := .synthetic b e)),
+            previewSpan? := some ref,
+            suggestion := "" : Meta.Hint.Suggestion
+          }
+        | `(inline|role{$_}%$tk2[$_]) =>
+          pure <| some {
+            span? := some tk2
+            previewSpan? := some ref,
+            suggestion := " -checked}": Meta.Hint.Suggestion
+          }
+        | _ => pure none
+      let ss := unchecked.toArray ++ ss.map fun x =>
+        { suggestion := x.toString, span? := some n, previewSpan? := some ref }
+      let h ←
+        if ss.isEmpty then pure m!""
+        else m!"Either disable the existence check or use an imported module:".hint ss (ref? := some ref)
+      logErrorAt n m!"Module is not transitively imported by the current module.{h}"
+
+  return .other {name := ``Data.ModuleName, val := .mk (Data.ModuleName.mk x)} #[.code s.getString]
+
+
 private def introduceAntiquotes (stx : Syntax) : DocM Unit :=
   discard <| stx.rewriteBottomUpM fun stx' =>
     match stx' with
@@ -439,15 +501,15 @@ def syntaxCat (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
 
 private partial def onlyIdent : Syntax → Bool
   | .node _ _ args =>
-    let nonEmpty := args.filter isEmpty
+    let nonEmpty := args.filter (!isEmpty ·)
     if h : nonEmpty.size = 1 then onlyIdent nonEmpty[0]
     else false
   | .ident .. => true
   | _ => false
 where
   isEmpty : Syntax → Bool
   | .node _ _ xs =>
-    xs.size = 0 || xs.all isEmpty
+    xs.all isEmpty
   | _ => false
 
 /--
@@ -884,7 +946,7 @@ def suggestName (code : StrLit) : DocM (Array CodeSuggestion) := do
     | _ =>
     if let some (_, []) := (← resolveLocalName stx.getId) then
       suggestions := suggestions.push <| .mk ``name none none
-    else
+    else if stx.getId.components.length == 1 then
       suggestions := suggestions.push <| .mk ``given none none
   return suggestions
 
@@ -912,8 +974,9 @@ def suggestLean (code : StrLit) : DocM (Array CodeSuggestion) := do
         withoutErrToSorry <|
         if stx[1][1].isMissing then pure none
         else some <$> elabType stx[1][1]
-      discard <| withoutErrToSorry <| elabTerm stx[0] ty?
+      let tm ← withoutErrToSorry <| elabTerm stx[0] ty?
     return #[.mk ``lean none none]
+
   catch | _ => return #[]
 
 /--
@@ -1040,3 +1103,15 @@ def suggestSyntax (code : StrLit) : DocM (Array CodeSuggestion) := do
 
   candidates.mapM fun cat => do
     return .mk ``«syntax» (some s!"{cat}") none
+
+/--
+Suggests the `module` role, if applicable.
+-/
+@[builtin_doc_code_suggestions]
+def suggestModule (code : StrLit) : DocM (Array CodeSuggestion) := do
+  let env ← getEnv
+  let moduleNames := env.header.moduleNames
+  let s := code.getString
+  if moduleNames.any (·.toString == s) then
+    return #[.mk ``module none none]
+  else return #[]

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// CI, please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;

tests/lean/run/versoDocs.lean

@@ -368,37 +368,26 @@ Hint: Insert a role to document it:
   • {̲a̲t̲t̲r̲}̲`instance`
   • {̲k̲w̲ ̲(̲o̲f̲ ̲:̲=̲ ̲L̲e̲a̲n̲.̲P̲a̲r̲s̲e̲r̲.̲A̲t̲t̲r̲.̲i̲n̲s̲t̲a̲n̲c̲e̲)̲}̲`instance` (in `attr`)
   • {̲s̲y̲n̲t̲a̲x̲ ̲a̲t̲t̲r̲}̲`instance`
+  • Use the `lit` role:
+    {̲l̲i̲t̲}̲`instance`
+    to mark the code as literal text and disable suggestions
 ---
 warning: Code element could be more specific.
 
 Hint: Insert a role to document it:
   • {̲a̲t̲t̲r̲}̲`term_elab`
   • {̲g̲i̲v̲e̲n̲}̲`term_elab`
-  • {̲l̲e̲a̲n̲}̲`term_elab`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲a̲t̲t̲r̲}̲`term_elab`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`term_elab`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲m̲c̲a̲s̲e̲s̲P̲a̲t̲}̲`term_elab`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲m̲i̲n̲t̲r̲o̲P̲a̲t̲}̲`term_elab`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲m̲r̲e̲f̲i̲n̲e̲P̲a̲t̲}̲`term_elab`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲m̲r̲e̲v̲e̲r̲t̲P̲a̲t̲}̲`term_elab`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲r̲c̲a̲s̲e̲s̲P̲a̲t̲}̲`term_elab`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲r̲i̲n̲t̲r̲o̲P̲a̲t̲}̲`term_elab`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲s̲t̲x̲}̲`term_elab`
+  • Use the `lit` role:
+    {̲l̲i̲t̲}̲`term_elab`
+    to mark the code as literal text and disable suggestions
 ---
 warning: Code element could be more specific.
 
 Hint: Insert a role to document it:
   • {̲g̲i̲v̲e̲n̲}̲`instantiation`
-  • {̲l̲e̲a̲n̲}̲`instantiation`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲a̲t̲t̲r̲}̲`instantiation`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲d̲o̲E̲l̲e̲m̲}̲`instantiation`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲m̲c̲a̲s̲e̲s̲P̲a̲t̲}̲`instantiation`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲m̲i̲n̲t̲r̲o̲P̲a̲t̲}̲`instantiation`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲m̲r̲e̲f̲i̲n̲e̲P̲a̲t̲}̲`instantiation`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲m̲r̲e̲v̲e̲r̲t̲P̲a̲t̲}̲`instantiation`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲r̲c̲a̲s̲e̲s̲P̲a̲t̲}̲`instantiation`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲r̲i̲n̲t̲r̲o̲P̲a̲t̲}̲`instantiation`
-  • {̲s̲y̲n̲t̲a̲x̲ ̲s̲t̲x̲}̲`instantiation`
+  • Use the `lit` role:
+    {̲l̲i̲t̲}̲`instantiation`
+    to mark the code as literal text and disable suggestions
 -/
 #guard_msgs in
 /--
@@ -408,6 +397,59 @@ This is not an attribute: `instantiation`
 -/
 def attrSuggestionTest := ()
 
+/--
+error: Module is not transitively imported by the current module.
+
+Hint: Either disable the existence check or use an imported module:
+  {module ̲-̲c̲h̲e̲c̲k̲e̲d̲}`NonExistent`
+---
+error: Module is not transitively imported by the current module.
+
+Hint: Either disable the existence check or use an imported module:
+  • {module ̲-̲c̲h̲e̲c̲k̲e̲d̲}`Laen.Data.Jsn`
+  • {module}`L̵a̵e̵n̵.̵D̵a̵t̵a̵.̵J̵s̵n̵L̲e̲a̲n̲.̲D̲a̲t̲a̲.̲J̲s̲o̲n̲`
+---
+error: Module is not transitively imported by the current module.
+
+Hint: Either disable the existence check or use an imported module:
+  • {module ̲-̲c̲h̲e̲c̲k̲e̲d̲}`Lean.Data.jso`
+  • {module}`L̵e̵a̵n̵.̵D̵a̵t̵a̵.̵j̵s̵o̵L̲e̲a̲n̲.̲D̲a̲t̲a̲.̲J̲s̲o̲n̲`
+  • {module}`L̵e̵a̵n̵.̵D̵a̵t̵a̵.̵j̵s̵o̵L̲e̲a̲n̲.̲D̲a̲t̲a̲.̲L̲s̲p̲`
+-/
+#guard_msgs in
+/--
+Error, no suggestions:
+{module}`NonExistent`
+
+Error, one suggestions:
+{module}`Laen.Data.Jsn`
+
+No error:
+{module -checked}`NonExistent`
+
+Error, two suggestions:
+{module}`Lean.Data.jso`
+
+No error:
+{module}`Lean.Data.Json`
+-/
+def talksAboutModules := ()
+
+/--
+warning: Code element could be more specific.
+
+Hint: Insert a role to document it:
+  • {̲m̲o̲d̲u̲l̲e̲}̲`Lean.Data.Json.Basic`
+  • Use the `lit` role:
+    {̲l̲i̲t̲}̲`Lean.Data.Json.Basic`
+    to mark the code as literal text and disable suggestions
+-/
+#guard_msgs in
+/--
+`Lean.Data.Json.Basic`
+-/
+def moduleSuggestionTest := ()
+
 /-
 TODO test:
 * Scope rules for all operators