wip: heuristically render Markdown in docstrings

doc/UsersGuide/Basic.lean

@@ -53,6 +53,16 @@ results in
 
 {docstring List.forM}
 
+## More Docstring Examples
+
+{docstring String}
+
+{docstring Subtype}
+
+{docstring OfNat}
+
+{docstring Monad}
+
 # Index
 %%%
 number := false

src/verso-manual/VersoManual.lean

@@ -285,7 +285,7 @@ def page (toc : List Html.Toc) (path : Path) (textTitle : String) (htmlTitle con
     (extraJsFiles := config.extraJs.toArray ++ state.extraJsFiles.map ("/-verso-js/" ++ ·.1))
 
 def Config.relativize (config : Config) (path : Path) (html : Html) : Html :=
-  if let some _ := config.baseURL then
+  if config.baseURL.isSome then
     -- Make all absolute URLS be relative to the site root, because that'll make them `base`-relative
     Html.relativize #[] html
   else

src/verso-manual/VersoManual/Docstring.lean

@@ -352,6 +352,14 @@ def docstring (name : Name) (declType : Docstring.DeclType) (signature : Option
   name := `Verso.Genre.Manual.Block.docstring
   data := ToJson.toJson (name, declType, signature)
 
+def docstringSection (header : String) : Block where
+  name := `Verso.Genre.Manual.Block.docstringSection
+  data := ToJson.toJson header
+
+def internalSignature (name : Highlighted) (signature : Option Highlighted) : Block where
+  name := `Verso.Genre.Manual.Block.internalSignature
+  data := ToJson.toJson (name, signature)
+
 end Block
 
 
@@ -470,6 +478,21 @@ def docstringStyle := r#"
   padding-right: 1rem;
 }
 
+.namedocs .subdocs .name-and-type {
+  font-size: 1rem;
+  margin-left: 0;
+  margin-top: 0;
+  margin-right: 0;
+  margin-bottom: 0.5rem;
+}
+
+.namedocs .subdocs .docs {
+  margin-left: 1.5rem;
+  margin-top: 0;
+  margin-right: 0;
+  margin-bottom: 0.5rem;
+}
+
 .namedocs:has(input[data-parent-idx]) tr[data-inherited-from] {
   transition-property: opacity, display;
   transition-duration: 0.4s;
@@ -498,6 +521,46 @@ where
 "
 
 
+open Verso.Genre.Manual.Markdown in
+@[block_extension Block.docstringSection]
+def docstringSection.descr : BlockDescr where
+  traverse _ _ _ := pure none
+  toTeX := none
+  toHtml := some fun _goI goB _id info contents =>
+    open Verso.Doc.Html HtmlT in
+    open Verso.Output Html in do
+      let .ok header := FromJson.fromJson? (α := String) info
+        | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize docstring section data while generating HTML"; pure .empty
+      return {{
+        <h1>{{header}}</h1>
+        {{← contents.mapM goB}}
+      }}
+
+open Verso.Genre.Manual.Markdown in
+@[block_extension Block.internalSignature]
+def internalSignature.descr : BlockDescr where
+  traverse _ _ _ := pure none
+  toTeX := some fun _goI goB _id _ contents => contents.mapM goB -- TODO
+  toHtml := some fun _goI goB _id info contents =>
+    open Verso.Doc.Html HtmlT in
+    open Verso.Output Html in do
+      let .ok (name, signature) := FromJson.fromJson? (α := Highlighted × Option Highlighted) info
+        | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize docstring section data while generating HTML"; pure .empty
+      return {{
+        <section class="subdocs">
+          <pre class="name-and-type hl lean">
+            {{← name.toHtml}}
+            {{← if let some s := signature then do
+                  pure {{" : " {{← s.toHtml}} }}
+                else pure .empty}}
+          </pre>
+          <div class="docs">
+            {{← contents.mapM goB}}
+          </div>
+        </section>
+      }}
+
+
 open Verso.Genre.Manual.Markdown in
 @[block_extension Block.docstring]
 def docstring.descr : BlockDescr where
@@ -601,22 +664,8 @@ where
               }}
             </ul>
           }}
-      let ctorRow ←
-        if isPrivateName ctor.name then
-          pure Html.empty
-        else pure {{
-            <h1>{{if isClass then "Instance Constructor" else "Constructor"}}</h1>
-            <table>
-              <tr><td><code class="hl lean inline">{{← ctor.hlName.toHtml}}</code></td></tr>
-              {{ ← if let some d := ctor.docstring? then do
-                  pure {{<tr><td>{{← md2html goB d}}</td></tr>}}
-                else pure Html.empty
-              }}
-            </table>
-          }}
       let infos := infos.filter (·.subobject?.isNone)
       pure {{
-        {{ ctorRow }}
         {{ parentRow }}
         <h1>{{if isClass then "Methods" else "Fields"}}</h1>
         <table class={{if isClass then "methods" else "fields"}}>
@@ -700,22 +749,132 @@ where
     }
     modify (·.saveDomainObject docstringDomain name.toString id)
 
-
 open Verso.Doc.Elab
 
+def leanFromMarkdown := ()
+
+def Inline.leanFromMarkdown (hls : Highlighted) : Inline where
+  name := ``Verso.Genre.Manual.leanFromMarkdown
+  data := ToJson.toJson hls
+
+
+@[inline_extension leanFromMarkdown]
+def leanFromMarkdown.inlinedescr : InlineDescr where
+  traverse id data _ := pure none
+  toTeX :=
+    some <| fun go _ _ content => do
+      pure <| .seq <| ← content.mapM fun b => do
+        pure <| .seq #[← go b, .raw "\n"]
+  extraCss := [highlightingStyle]
+  extraJs := [highlightingJs]
+  extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)]
+  extraCssFiles := [("tippy-border.css", tippy.border.css)]
+  toHtml :=
+    open Verso.Output Html in
+    open Verso.Doc.Html in
+    some <| fun _ _ data _ => do
+      match FromJson.fromJson? data with
+      | .error err =>
+        HtmlT.logError <| "Couldn't deserialize Lean code while rendering inline HTML: " ++ err
+        pure .empty
+      | .ok (hl : Highlighted) =>
+        hl.inlineHtml "docstring-examples"
+
+open Lean Elab Term in
+def tryElabInlineCodeTerm (decl : Name) (str : String) : DocElabM Term := do
+  dbg_trace "HELLO! {decl} |{str}|"
+
+  match Parser.runParserCategory (← getEnv) `term str s!"<docstring of {decl}>" with
+  | .error e => throw (.error (← getRef) e)
+  | .ok stx =>
+    dbg_trace "PARSED |{stx}|"
+    let (newMsgs, tree) ← do
+      let initMsgs ← Core.getMessageLog
+      try
+        Core.resetMessageLog
+        -- TODO open decls/current namespace
+        let tree' ←  fun _ => do
+          dbg_trace "Gonna elab..."
+          let e ← Elab.Term.elabTerm (catchExPostpone := true) stx none
+          dbg_trace "ELAB'ED! |{e}|"
+          Term.synthesizeSyntheticMVarsNoPostponing
+          let e' ← Term.levelMVarToParam (← instantiateMVars e)
+          Term.synthesizeSyntheticMVarsNoPostponing
+          let e' ← instantiateMVars e'
+          dbg_trace "ELAB'ED MORE! |{e'}|"
+          let ctx := PartialContextInfo.commandCtx {
+            env := ← getEnv, fileMap := ← getFileMap, mctx := ← getMCtx, currNamespace := ← getCurrNamespace,
+            openDecls := ← getOpenDecls, options := ← getOptions, ngen := ← getNGen
+          }
+          pure <| InfoTree.context ctx (.node (Info.ofCommandInfo ⟨`Verso.Genre.Manual.docstring, (← getRef)⟩) (← getInfoState).trees)
+        pure (← Core.getMessageLog, tree')
+      finally
+        Core.setMessageLog initMsgs
+    if newMsgs.hasErrors then
+      for msg in newMsgs.errorsToWarnings.toArray do
+        logMessage msg
+
+    let hls := (← highlight stx #[] (PersistentArray.empty.push tree))
+
+    logInfoAt (← getRef) stx
+
+    ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)])
+
+
+open Lean Elab Term in
+def tryElabInlineCodeName (_decl : Name) (str : String) : DocElabM Term := do
+  let str := str.trim
+  let x := str.toName
+  if x.toString == str then
+    let stx := mkIdent x
+    let n ← realizeGlobalConstNoOverload stx
+    let hl : Highlighted ← constTok n str
+    ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hl)) #[Verso.Doc.Inline.code $(quote str)])
+  else
+    throwError "Not a name: '{str}'"
+where
+  constTok {m} [Monad m] [MonadEnv m] [MonadLiftT MetaM m] [MonadLiftT IO m]
+      (name : Name) (str : String) :
+      m Highlighted := do
+    let docs ← findDocString? (← getEnv) name
+    let sig := toString (← (PrettyPrinter.ppSignature name)).1
+    pure <| .token ⟨.const name sig docs false, str⟩
+
+open Lean Elab Term in
+def tryElabInlineCode (decl : Name) (str : String) : DocElabM Term := do
+  -- This brings the parameters into scope, so the term elaboration version catches them!
+  Meta.forallTelescopeReducing (← getConstInfo decl).type fun _ _ =>
+    try
+      tryElabInlineCodeName decl str <|>
+      tryElabInlineCodeTerm decl str
+    catch
+      | .error ref e =>
+        logWarningAt ref e
+        ``(Verso.Doc.Inline.code $(quote str))
+      | e =>
+        logWarning m!"Internal exception uncaught: {e.toMessageData}"
+        ``(Verso.Doc.Inline.code $(quote str))
+
+def blockFromMarkdownWithLean (name : Name) (b : MD4Lean.Block) : DocElabM Term :=
+  Markdown.blockFromMarkdown b
+    (handleHeaders := Markdown.strongEmphHeaders)
+    (elabInlineCode := tryElabInlineCode name)
+
 @[block_role_expander docstring]
 def docstring : BlockRoleExpander
   | args, #[] => do
     match args with
     | #[.anon (.name x)] =>
       let name ← Elab.realizeGlobalConstNoOverloadWithInfo x
       Doc.PointOfInterest.save (← getRef) name.toString (detail? := some "Documentation")
-      let blockStx ← match ← Lean.findDocString? (← getEnv) name with
-      | none => logWarningAt x m!"No docs found for '{x}'"; pure #[]
-      | some docs =>
-        let some ast := MD4Lean.parse docs
-          | throwErrorAt x "Failed to parse docstring as Markdown"
-        ast.blocks.mapM (Markdown.blockFromMarkdown · Markdown.strongEmphHeaders)
+      let blockStx ←
+        match ← Lean.findDocString? (← getEnv) name with
+        | none => logWarningAt x m!"No docs found for '{x}'"; pure #[]
+        | some docs =>
+          let some ast := MD4Lean.parse docs
+            | throwErrorAt x "Failed to parse docstring as Markdown"
+
+          ast.blocks.mapM (blockFromMarkdownWithLean name)
 
       if Lean.Linter.isDeprecated (← getEnv) name then
         logInfoAt x m!"'{x}' is deprecated"
@@ -735,9 +894,25 @@ def docstring : BlockRoleExpander
       }
       let sig := Lean.Widget.tagCodeInfos ctx infos tt
       let signature ← some <$> renderTagged none sig ⟨{}, false⟩
-      pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstring $(quote name) $(quote declType) $(quote signature)) #[$blockStx,*])]
+      let extras ← getExtras declType
+      pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstring $(quote name) $(quote declType) $(quote signature)) #[$blockStx,*, $extras,*])]
     | _ => throwError "Expected exactly one positional argument that is a name"
   | _, more => throwErrorAt more[0]! "Unexpected block argument"
+where
+  getExtras (declType : Block.Docstring.DeclType) : DocElabM (Array Term) :=
+    match declType with
+    | .structure (isClass := isClass) (constructor := constructor) .. => do
+      let header := if isClass then "Instance Constructor" else "Constructor"
+      let sigDesc ←
+        if let some docs := constructor.docstring? then
+          let some mdAst := MD4Lean.parse docs
+            | throwError "Failed to parse docstring as Markdown"
+          mdAst.blocks.mapM (blockFromMarkdownWithLean constructor.name)
+        else pure #[]
+      let sig ← `(Verso.Doc.Block.other (Verso.Genre.Manual.Block.internalSignature $(quote constructor.hlName) none) #[$sigDesc,*])
+      pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$sig])]
+    | _ => pure #[]
+
 
 def Block.optionDocs (name : Name) (defaultValue : Option Highlighted) : Block where
   name := `Verso.Genre.Manual.optionDocs
@@ -783,7 +958,7 @@ def optionDocs : BlockRoleExpander
     Doc.PointOfInterest.save x optDecl.declName.toString
     let some mdAst := MD4Lean.parse optDecl.descr
       | throwErrorAt x "Failed to parse docstring as Markdown"
-    let contents ← mdAst.blocks.mapM (Markdown.blockFromMarkdown · Markdown.strongEmphHeaders)
+    let contents ← mdAst.blocks.mapM (blockFromMarkdownWithLean x.getId)
     pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.optionDocs $(quote x.getId) $(quote <| highlightDataValue optDecl.defValue)) #[$contents,*])]
 
   | _, more => throwErrorAt more[0]! "Unexpected block argument"