fix: parameter references in Verso docstrings (#14198)

This PR fixes a bug where references to parameters by names failed for
unbracketed binders, in the presence of `_` parameters, and in
macro-generated declarations.

Parameters are introduced by walking the declaration's binders, matching
them up to the elaborated type. Cases were missing for bare identifiers
and `_`.

Author: david-christiansen

src/Lean/DocString/Add.lean

@@ -172,6 +172,64 @@ def reportVersoParseFailure
       severity := .error
     }
 
+open Lean.Doc in
+/--
+Elaborates already-parsed Verso `blocks` for the specified declaration with interactive features
+disabled, reporting any elaboration messages at the current reference. When `fileMap?` is provided,
+message positions are interpreted against it.
+-/
+private def execVersoBlocks
+    (declName : Name) (binders : Syntax) (blocks : Array Syntax) (fileMap? : Option FileMap) :
+    TermElabM (Array (Doc.Block ElabInline ElabBlock) × Array (Doc.Part ElabInline ElabBlock Empty)) := do
+  let msgs ← Core.getAndEmptyMessageLog
+  let (val, msgs') ←
+    try
+      let act := (Doc.elabBlocks (blocks.map (⟨·⟩))).exec declName binders (suggestionMode := .batch)
+      let val ←
+        Elab.withEnableInfoTree false <|
+          match fileMap? with
+          | some fileMap => withTheReader Core.Context ({· with fileMap }) act
+          | none => act
+      pure (val, ← Core.getAndEmptyMessageLog)
+    finally
+      Core.setMessageLog msgs
+  for msg in msgs'.toArray do
+    logAt (← getRef) msg.data (severity := msg.severity) (isSilent := msg.isSilent)
+  pure val
+
+open Lean.Doc in
+open Parser in
+/--
+Parses a Verso docstring from its text and elaborates it for the specified declaration. Because the
+text carries no source positions, interactive features are disabled and any messages are reported at
+the current reference.
+
+`binders` should be the syntax of the parameters to the constant that is being documented, as a null
+node that contains a sequence of bracketed binders, or an empty null node when none are available.
+-/
+def versoDocStringOfText
+    (declName : Name) (binders : Syntax) (docComment : String) :
+    TermElabM (Array (Doc.Block ElabInline ElabBlock) × Array (Doc.Part ElabInline ElabBlock Empty)) := do
+  let env ← getEnv
+  let ictx : InputContext := .mk docComment (← getFileName)
+  let text := ictx.fileMap
+  let pmctx : ParserModuleContext := {
+    env,
+    options := ← getOptions,
+    currNamespace := (← getCurrNamespace),
+    openDecls := (← getOpenDecls)
+  }
+  let s := mkParserState docComment
+  -- TODO parse one block at a time for error recovery purposes
+  let s := Doc.Parser.document.run ictx pmctx (getTokenTable env) s
+
+  if !s.allErrors.isEmpty then
+    for (_, _, err) in s.allErrors do
+      logError err.toString
+    return (#[], #[])
+  else
+    execVersoBlocks declName binders s.stxStack.back.getArgs (fileMap? := some text)
+
 open Lean.Doc in
 open Lean.Parser.Command in
 /--
@@ -187,9 +245,24 @@ are available, pass `Syntax.missing` or an empty null node.
 def versoDocString
     (declName : Name) (binders : Syntax) (docComment : TSyntax ``docComment) :
     TermElabM (Array (Doc.Block ElabInline ElabBlock) × Array (Doc.Part ElabInline ElabBlock Empty)) := do
-  if let some stx ← parseVersoDocString docComment then
-    Doc.elabBlocks (stx.getArgs.map (⟨·⟩)) |>.exec declName binders
-  else return (#[], #[])
+  -- A docstring already parsed as Verso, or one re-parsable from its source range, supports
+  -- interactive features. A macro-generated docstring has neither, so fall back to its text.
+  let body := docComment.raw[1]
+  if (body.getPos? (canonicalOnly := true)).isSome then
+    -- Source positions are available, so re-parse from source for interactive features.
+    if let some stx ← parseVersoDocString docComment then
+      Doc.elabBlocks (stx.getArgs.map (⟨·⟩)) |>.exec declName binders
+    else return (#[], #[])
+  else if body.isOfKind ``versoCommentBody then
+    if body[0].isOfKind `Lean.Doc.Syntax.parseFailure then
+      -- The markup failed to parse, so re-parse its text to report the error.
+      versoDocStringOfText declName binders body[0][0].getAtomVal
+    else
+      -- A docstring parsed as Verso by a macro, with positions stripped.
+      execVersoBlocks declName binders body[0].getArgs (fileMap? := none)
+  else
+    -- A plain-text doc comment without source positions; parse and elaborate from its text.
+    versoDocStringOfText declName binders docComment.getDocString
 
 open Lean.Doc Parser in
 open Lean.Parser.Command in
@@ -204,52 +277,15 @@ def versoModDocString
 
 
 
-open Lean.Doc in
-open Parser in
 /--
 Adds a Verso docstring to the specified declaration, which should already be present in the
 environment. The docstring is added from a string value, rather than syntax, which means that the
 interactive features are disabled.
 -/
 def versoDocStringFromString
     (declName : Name) (docComment : String) :
-    TermElabM (Array (Doc.Block ElabInline ElabBlock) × Array (Doc.Part ElabInline ElabBlock Empty)) := do
-
-  let env ← getEnv
-  let ictx : InputContext := .mk docComment (← getFileName)
-  let text := ictx.fileMap
-  let pmctx : ParserModuleContext := {
-    env,
-    options := ← getOptions,
-    currNamespace := (← getCurrNamespace),
-    openDecls := (← getOpenDecls)
-  }
-  let s := mkParserState docComment
-  -- TODO parse one block at a time for error recovery purposes
-  let s := Doc.Parser.document.run ictx pmctx (getTokenTable env) s
-
-  if !s.allErrors.isEmpty then
-    for (pos, _, err) in s.allErrors do
-      logError err.toString
-    return (#[], #[])
-  else
-    let stx := s.stxStack.back
-    let stx := stx.getArgs
-    let msgs ← Core.getAndEmptyMessageLog
-    let (val, msgs') ←
-      try
-        let range? := (← getRef).getRange?
-        let val ←
-          Elab.withEnableInfoTree false <| withTheReader Core.Context ({· with fileMap := text}) <|
-            (Doc.elabBlocks (stx.map (⟨·⟩))).exec declName (mkNullNode #[]) (suggestionMode := .batch)
-        let msgs' ← Core.getAndEmptyMessageLog
-        pure (val, msgs')
-      finally
-        Core.setMessageLog msgs
-    -- Adjust messages to show them at the call site
-    for msg in msgs'.toArray do
-      logAt (← getRef) msg.data (severity := msg.severity)
-    pure val
+    TermElabM (Array (Doc.Block ElabInline ElabBlock) × Array (Doc.Part ElabInline ElabBlock Empty)) :=
+  versoDocStringOfText declName (mkNullNode #[]) docComment
 
 /--
 Adds a Markdown docstring to the environment, validating documentation links.

src/Lean/Elab/DocString.lean

@@ -274,7 +274,12 @@ where
           localInstances := localInstances.push {className := c, fvar := .fvar fv}
 
         if let some (some x') := x then
-          if x'.getId == y then
+          if x'.getKind == ``hole then
+            -- A `_` parameter has no name, so it matches no binder. Drop it from the cursor
+            -- and align the remaining parameters by name; each lifted binder, including
+            -- captured variables, is introduced under its own name below.
+            x := none
+          else if x'.getId == y then
             lctx := lctx.mkLocalDecl fv y ty
             Meta.withLCtx lctx localInstances <|
               addTermInfo' x' (.fvar fv) (lctx? := some lctx) (expectedType? := ty)
@@ -301,7 +306,10 @@ where
     | ``instBinder =>
       let x := binderStx[1][0]
       if x.isMissing then pure #[none] else pure #[some x]
-    | _ => throwErrorAt binderStx "Couldn't interpret binder {binderStx}"
+    | k =>
+      -- A parameter bound by an unbracketed identifier or `_`, as in `def f x` or `where go _`.
+      if k == identKind || k == ``hole then pure #[some binderStx]
+      else throwErrorAt binderStx "Couldn't interpret binder {binderStx}"
   getNames (ids : Syntax) : TermElabM (Array (Option Syntax)) :=
     ids.getArgs.mapM fun x =>
       if x.getKind == identKind || x.getKind == ``hole then
@@ -1209,7 +1217,11 @@ unsafe def roleExpandersForUnsafe (roleName : Ident) :
     let builtins := (← builtinDocRoles.get).get? x |>.getD #[]
     return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ builtins
   else
-    let x := roleName.getId
+    -- Builtin roles are not necessarily in the environment at a
+    -- quotation site, so they aren't in the preresolved list. They
+    -- must also be looked up by their plain name, erasing any macro
+    -- scopes a quotation introduced.
+    let x := roleName.getId.eraseMacroScopes
     let hasBuiltin ← resolveBuiltinDocName (← builtinDocRoles.get) x
     return hasBuiltin.toArray.flatten
 
@@ -1228,7 +1240,7 @@ unsafe def codeBlockExpandersForUnsafe (codeBlockName : Ident) :
     let names' := (← builtinDocCodeBlocks.get).get? x |>.getD #[]
     return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ names'
   else
-    let x := codeBlockName.getId
+    let x := codeBlockName.getId.eraseMacroScopes
     let hasBuiltin ← resolveBuiltinDocName (← builtinDocCodeBlocks.get) x
     return hasBuiltin.toArray.flatten
 
@@ -1247,7 +1259,7 @@ unsafe def directiveExpandersForUnsafe (directiveName : Ident) :
     let names' := (← builtinDocDirectives.get).get? x |>.getD #[]
     return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ names'
   else
-    let x := directiveName.getId
+    let x := directiveName.getId.eraseMacroScopes
     let hasBuiltin ← resolveBuiltinDocName (← builtinDocDirectives.get) x
     return hasBuiltin.toArray.flatten
 
@@ -1265,7 +1277,7 @@ unsafe def commandExpandersForUnsafe (commandName : Ident) :
     let names' := (← builtinDocCommands.get).get? x |>.getD #[]
     return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ names'
   else
-    let x := commandName.getId
+    let x := commandName.getId.eraseMacroScopes
     let hasBuiltin :=
       (← builtinDocCommands.get).get? x <|> (← builtinDocCommands.get).get? (`Lean.Doc ++ x)
     return hasBuiltin.toArray.flatten

src/Lean/Elab/DocString/Builtin.lean

@@ -906,6 +906,20 @@ structure Data.LeanBlock where
 deriving TypeName
 
 
+/--
+Runs `act` with info trees enabled, returning its result together with the info trees it produced.
+The document's prior info trees are restored afterward; the trees from `act` are added to the
+document only when its info trees were already enabled.
+-/
+def withHighlightingInfoTrees (act : DocM α) : DocM (α × PersistentArray InfoTree) := do
+  let enabled := (← getInfoState).enabled
+  let outer ← getResetInfoTrees
+  let a ← withEnableInfoTree true <| withSaveInfoContext act
+  let trees ← getInfoTrees
+  modifyInfoState fun st => { st with trees := if enabled then outer ++ trees else outer }
+  return (a, trees)
+
+
 /--
 Elaborates a sequence of Lean commands as examples.
 
@@ -920,19 +934,24 @@ The flags `error` and `warning` indicate that an error or warning is expected in
 @[builtin_doc_code_block]
 def lean (name : Option Ident := none) (error warning : flag false) («show» : flag true) (code : StrLit) :
     DocM (Block ElabInline ElabBlock) := do
-  let text ← getFileMap
   let env ← getEnv
-  let p := andthenFn whitespace (categoryParserFnImpl `command)
-  -- TODO fallback for non-original syntax
-  let pos := code.raw.getPos? true |>.get!
-  let endPos := code.raw.getTailPos? true |>.get!
-  let endPos := if endPos ≤ text.source.rawEndPos then endPos else text.source.rawEndPos
-  let ictx :=
-    mkInputContext text.source (← getFileName)
-      (endPos := endPos) (endPos_valid := by simp only [endPos]; split <;> simp [*])
+  -- Parse from the file when source positions are available, otherwise from the literal's own
+  -- contents (e.g. for a docstring that came from a macro).
+  let (text, ictx, pos) ←
+    if let some pos := code.raw.getPos? true then
+      let text ← getFileMap
+      let endPos := code.raw.getTailPos? true |>.getD text.source.rawEndPos
+      let endPos := if endPos ≤ text.source.rawEndPos then endPos else text.source.rawEndPos
+      pure (text,
+        mkInputContext text.source (← getFileName)
+          (endPos := endPos) (endPos_valid := by simp only [endPos]; split <;> simp [*]),
+        pos)
+    else
+      let ictx := mkInputContext code.getString (← getFileName)
+      pure (ictx.fileMap, ictx, (0 : String.Pos.Raw))
   let cctx : Command.Context := {fileName := ← getFileName, fileMap := text, snap? := none, cancelTk? := none}
   let scopes := (← get).scopes
-  let (cmds, cmdState, trees) ← withSaveInfoContext do
+  let ((cmds, cmdState), trees) ← withHighlightingInfoTrees do
     let mut cmdState : Command.State := { env, maxRecDepth := ← MonadRecDepth.getMaxRecDepth, scopes }
     let mut pstate : Parser.ModuleParserState := {
       pos
@@ -954,8 +973,7 @@ def lean (name : Option Ident := none) (error warning : flag false) («show» :
 
     for t in cmdState.infoState.trees do
       pushInfoTree t
-    let trees := (← getInfoTrees)
-    pure (cmds, cmdState, trees)
+    pure (cmds, cmdState)
 
   let mut output := #[]
   for msg in cmdState.messages.toArray do
@@ -1098,7 +1116,7 @@ Treats the provided term as Lean syntax in the documentation's scope.
 def leanRole (type : Option StrLit := none) (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
   let s ← onlyCode xs
   let stx ← parseStrLit leanTermContents s
-  withSaveInfoContext do
+  let (_, trees) ← withHighlightingInfoTrees do
     let ty? ←
       withoutErrToSorry <| do
       if stx[1][1].isMissing then -- no colon
@@ -1111,7 +1129,6 @@ def leanRole (type : Option StrLit := none) (xs : TSyntaxArray `inline) : DocM (
           logErrorAt t m!"Ignoring `{s.getString}` in favor of type provided after colon"
         some <$> elabType stx[1][1]
     withoutErrToSorry <| discard <| elabExtraTerm stx[0] ty?
-  let trees := (← getInfoTrees)
   if h : trees.size > 0 then
     let tm := Data.LeanTerm.mk (← highlightSyntax trees stx)
     return .other {val := .mk tm} #[.code s.getString]
@@ -1125,15 +1142,14 @@ Treats the provided term as Lean syntax in the documentation's scope.
 @[builtin_doc_code_block]
 def leanTerm (code : StrLit) : DocM (Block ElabInline ElabBlock) := do
   let stx ← parseStrLit leanTermContents code
-  withSaveInfoContext do
+  let (_, trees) ← withHighlightingInfoTrees do
     let ty? ←
       withoutErrToSorry <|
       if stx[1][1].isMissing then -- no colon
         pure none
       else -- type after colon
         some <$> elabType stx[1][1]
     withoutErrToSorry <| discard <| elabExtraTerm stx[0] ty?
-  let trees := (← getInfoTrees)
   if h : trees.size > 0 then
     let tm := Data.LeanTerm.mk (← highlightSyntax trees stx)
     return .other {val := .mk tm} #[.code code.getString]
@@ -1249,7 +1265,7 @@ def assert' (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
   let lhsStx ← parseStrLit assertTermContents lhsCode
   let rhsStx ← parseStrLit assertTermContents rhsCode
   let tyStx? ← tyCode?.mapM (parseStrLit assertTermContents)
-  withSaveInfoContext do
+  let (_, trees) ← withHighlightingInfoTrees do
     let ty? ← withoutErrToSorry <|
       match tyStx? with
       | some tyStx => some <$> elabType tyStx
@@ -1260,7 +1276,6 @@ def assert' (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
       throwError m!"Expected {lhs} = {rhs}, which is {← Meta.whnf lhs} = {← Meta.whnf rhs}, reducing to {← Meta.reduceAll lhs} = {← Meta.reduceAll rhs} but they are not equal."
   let str := lhsCode.getString ++ " = " ++ rhsCode.getString ++
     (tyCode?.map (" : " ++ ·.getString) |>.getD "")
-  let trees ← getInfoTrees
   if trees.size > 0 then
     let mut code := (← highlightSyntax trees lhsStx) ++ " = " ++ (← highlightSyntax trees rhsStx)
     if let some tyStx := tyStx? then
@@ -1277,14 +1292,13 @@ Asserts that an equality holds.
 def assert (xs : TSyntaxArray `inline) : DocM (Inline ElabInline) := do
   let s ← onlyCode xs
   let stx ← parseStrLit termParser.fn s
-  withSaveInfoContext do
+  let (_, trees) ← withHighlightingInfoTrees do
     let ty ← withoutErrToSorry <| elabType stx
     match_expr (← Meta.whnf ty) with
     | Eq _ lhs rhs =>
       unless (← Meta.isDefEq lhs rhs) do
         throwErrorAt stx m!"Expected {lhs} = {rhs}, but they are not definitionally equal"
     | _ => throwErrorAt stx m!"Expected equality type"
-  let trees ← getInfoTrees
   if trees.size > 0 then
     let tm := Data.LeanTerm.mk (← highlightSyntax trees stx)
     return .other {val := .mk tm} #[.code s.getString]

src/Lean/Elab/DocString/Builtin/Parsing.lean

@@ -23,7 +23,24 @@ private def strLitRange [Monad m] [MonadFileMap m] (s : StrLit) : m Lean.Syntax.
 variable [Monad m] [MonadFileMap m] [MonadEnv m]
 variable [MonadError m] [AddMessageContext m] [MonadLog m] [MonadOptions m]
 
+/--
+Parses a string literal's contents directly from its decoded value rather than from the source file.
+This is used when the literal has no source position, as in a docstring that came from a macro.
+-/
+private def parseFromContents (p : ParserFn) (contents : String) : m Syntax := do
+  let env ← getEnv
+  let ictx := mkInputContext contents (← getFileName)
+  let s := p.run ictx { env, options := ← getOptions } (getTokenTable env) (mkParserState contents)
+  if !s.allErrors.isEmpty then
+    throwError (s.toErrorMsg ictx)
+  else if ictx.atEnd s.pos then
+    pure s.stxStack.back
+  else
+    throwError ((s.mkError "end of input").toErrorMsg ictx)
+
 def parseStrLit (p : ParserFn) (s : StrLit) : m Syntax := do
+  if (s.raw.getPos? (canonicalOnly := true)).isNone then
+    return ← parseFromContents p s.getString
   let text ← getFileMap
   let env ← getEnv
   let ⟨pos, endPos⟩ ← strLitRange s
@@ -43,6 +60,8 @@ def parseStrLit (p : ParserFn) (s : StrLit) : m Syntax := do
     throwError ((s.mkError "end of input").toErrorMsg ictx)
 
 def parseQuotedStrLit (p : ParserFn) (strLit : StrLit) : m Syntax := do
+  if (strLit.raw.getPos? (canonicalOnly := true)).isNone then
+    return ← parseFromContents p strLit.getString
   let text ← getFileMap
   let env ← getEnv
   let ⟨pos, _⟩ ← strLitRange strLit
@@ -100,6 +119,18 @@ where
     return n
 
 def parseStrLit' (p : ParserFn) (s : StrLit) : m (Syntax × Bool) := do
+  if (s.raw.getPos? (canonicalOnly := true)).isNone then
+    let contents := s.getString
+    let env ← getEnv
+    let ictx := mkInputContext contents (← getFileName)
+    let st := p.run ictx { env, options := ← getOptions } (getTokenTable env) (mkParserState contents)
+    let err ←
+      if !st.allErrors.isEmpty then
+        logError (st.toErrorMsg ictx); pure true
+      else if !ictx.atEnd st.pos then
+        logError ((st.mkError "end of input").toErrorMsg ictx); pure true
+      else pure false
+    return (st.stxStack.back, err)
   let text ← getFileMap
   let env ← getEnv
   let endPos := s.raw.getTailPos? true |>.get!