feat: allow Verso docstrings to suppose the existence of instances

This PR adds a {givenInstance}`C` role that adds an instance of `C` to
the document's local assumptions.

Author: david-christiansen

src/Lean/Elab/DocString.lean

@@ -86,6 +86,9 @@ structure State where
   -/
   lctx : LocalContext
   /--
+  -/
+  localInstances : LocalInstances
+  /--
   The options.
 
   The `MonadLift TermElabM DocM` instance runs the lifted action with these options, so elaboration
@@ -129,10 +132,10 @@ instance : MonadStateOf State DocM :=
 
 instance : MonadLift TermElabM DocM where
   monadLift act := private DocM.mk fun _ _ st' => do
-    let {openDecls, lctx, options, ..} := (← st'.get)
+    let {openDecls, lctx, options, localInstances, ..} := (← st'.get)
     let v ←
       withTheReader Core.Context (fun ρ => { ρ with openDecls, options }) <|
-      withTheReader Meta.Context (fun ρ => { ρ with lctx }) <|
+      withTheReader Meta.Context (fun ρ => { ρ with lctx, localInstances }) <|
       act
     return v
 
@@ -144,16 +147,19 @@ private builtin_initialize modDocstringStateExt : EnvExtension (Option ModuleDoc
   registerEnvExtension (pure none)
 
 private def getModState
-    [Monad m] [MonadEnv m] [MonadLiftT IO m] [MonadLCtx m]
+    [Monad m] [MonadEnv m] [MonadLiftT IO m] [MonadLiftT MetaM m] [MonadLCtx m]
     [MonadResolveName m] [MonadOptions m] : m ModuleDocstringState := do
   if let some st := modDocstringStateExt.getState (← getEnv) then
     return st
   else
-    let lctx ← getLCtx
+    let scopes := [{header := "", isPublic := true}]
     let openDecls ← getOpenDecls
+    let lctx ← getLCtx
+    let localInstances ← Meta.getLocalInstances
     let options ← getOptions
-    let scopes := [{header := "", isPublic := true}]
-    let st : ModuleDocstringState := { scopes, openDecls, lctx, options, scopedExts := #[] }
+    let scopedExts := #[]
+    let st : ModuleDocstringState :=
+      { scopes, openDecls, lctx, localInstances, options, scopedExts }
     modifyEnv fun env =>
       modDocstringStateExt.setState env st
     return st
@@ -197,7 +203,7 @@ def DocM.exec (declName : Name) (binders : Syntax) (act : DocM α)
       let options ← getOptions
       let scopes := [{header := "", isPublic := true}]
       let ((v, _), _) ← withTheReader Meta.Context (fun ρ => { ρ with localInstances }) <|
-        act.run { suggestionMode } |>.run {} |>.run { scopes, openDecls, lctx, options }
+        act.run { suggestionMode } |>.run {} |>.run { scopes, openDecls, lctx, localInstances, options }
       pure v
     finally
       scopedEnvExtensionsRef.set sc

src/Lean/Elab/DocString/Builtin.lean

@@ -522,7 +522,6 @@ private def givenContents : ParserFn :=
        optionalFn (symbolFn ":" >> termParser.fn)))
     (symbolFn ",")
 
-
 /--
 A metavariable to be discussed in the remainder of the docstring.
 
@@ -612,6 +611,98 @@ def given (type : Option StrLit := none) (typeIsMeta : flag false) («show» : f
         |> Inline.concat
   else return .empty
 
+private def givenInstanceContents : ParserFn :=
+  whitespace >>
+  sepBy1Fn false
+    (nodeFn nullKind
+     (optionalFn (atomicFn (identFn >> symbolFn ":")) >>
+       termParser.fn))
+    (symbolFn ",")
+
+/--
+An instance metavariable to be discussed in the remainder of the docstring.
+
+This is similar to {given}, but the resulting variable is marked for instance synthesis
+(with `BinderInfo.instImplicit`), and the name is optional.
+
+There are two syntaxes that can be used:
+ * `` {givenInstance}`T` `` establishes an unnamed instance of type `T`.
+ * `` {givenInstance}`x : T` `` establishes a named instance `x` of type `T`.
+
+Additionally, the contents of the code literal can be repeated, with comma separators.
+
+If the `show` flag is `false` (default `true`), then the instance is not shown in the docstring.
+-/
+@[builtin_doc_role]
+def givenInstance («show» : flag true) (xs : TSyntaxArray `inline) :
+    DocM (Inline ElabInline) := do
+  let s ← onlyCode xs
+
+  let stxs ← parseStrLit givenInstanceContents s
+  let stxs := stxs.getArgs.mapIdx Prod.mk |>.filterMap fun (n, s) =>
+    if n % 2 = 0 then some s else none
+  let mut lctx ← getLCtx
+  let mut localInstances ← Meta.getLocalInstances
+  let mut instCounter := 0
+  for stx in stxs do
+    let nameColonOpt := stx[0][0]
+    let tyStx := stx[1]
+
+    -- Generate a fresh name if no name is provided
+    let (userName, hasUserName) ←
+      if nameColonOpt.isMissing then
+        instCounter := instCounter + 1
+        pure (Name.mkSimple s!"inst{instCounter}", false)
+      else
+        -- nameColonOpt is `identFn >> symbolFn ":"`, so the identifier is the first child
+        pure (nameColonOpt[0].getId, true)
+
+    let ty' : Expr ← elabType tyStx
+    let class? ← Meta.isClass? ty'
+    let some className := class?
+      | throwError m!"Expected a type class, but got `{.ofExpr ty'}`"
+
+    let fv ← mkFreshFVarId
+    lctx := lctx.mkLocalDecl fv userName ty' BinderInfo.default
+    localInstances := localInstances.push { fvar := .fvar fv, className }
+
+    if hasUserName then
+      addTermInfo' nameColonOpt[0] (.fvar fv)
+        (lctx? := some lctx) (isBinder := true) (expectedType? := some ty')
+
+  modify fun st => { st with lctx, localInstances }
+
+  if «show» then
+    let text ← getFileMap
+    let mut outStrs := #[]
+    let mut failed := false
+    for stx in stxs do
+      let nameColonOpt := stx[0][0]
+      let thisStr ←
+        if let some ⟨b', e'⟩ := stx[1].getRange? then
+          -- Has type annotation
+          if nameColonOpt.isMissing then
+            -- No name, just show type
+            pure <| String.Pos.Raw.extract text.source b' e'
+          else
+            -- Has name and type, nameColonOpt is `identFn >> symbolFn ":"`
+            if let some ⟨b, e⟩ := nameColonOpt[0].getRange? then
+              pure <| s!"{b.extract text.source e} : {b'.extract text.source e'}"
+            else
+              failed := true
+              break
+        else
+          failed := true
+          break
+      outStrs := outStrs.push thisStr
+    if failed then
+      return .code s.getString
+    else
+      return outStrs.map Inline.code
+        |>.toList |>.intersperse (Inline.text ", ") |>.toArray
+        |> Inline.concat
+  else return .empty
+
 
 private def firstToken? (stx : Syntax) : Option Syntax :=
   stx.find? fun

stage0/src/stdlib_flags.h

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

tests/lean/run/versoDocs.lean

@@ -96,6 +96,12 @@ def rot (n : Nat) (xs : Array α) : Array α :=
 #eval rot 5 #[1, 2, 3]
 
 
+/--
+Given {given}`α : Type` and {given}`x : α, y : α` with an instance of {givenInstance}`Add α`,
+{lean}`x + y : α`.
+-/
+def givens := ()
+
 /--
 Given {given}`xs : List α`, finds lists {given}`ys` and {given}`zs` such that {lean}`xs = ys ++ zs`
 and {lean}`∀x ∈ xs, p x` and {lean}`zs.head?.all (¬p ·)`.