From ae4b0c3b7535c9fb1eedc05eecf754cc7eae6d4d Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 17 Dec 2024 17:08:37 +0100 Subject: [PATCH] wip: further docstring heuristics progress --- src/verso-manual/VersoManual/Docstring.lean | 270 ++++++++++++-------- 1 file changed, 160 insertions(+), 110 deletions(-) diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean index 86c6e20..9ba9c9d 100644 --- a/src/verso-manual/VersoManual/Docstring.lean +++ b/src/verso-manual/VersoManual/Docstring.lean @@ -147,6 +147,22 @@ structure FieldInfo where docString? : Option String deriving Inhabited, Repr, ToJson, FromJson +open Syntax (mkCApp) in +open BinderInfo in +instance : Quote BinderInfo where + quote + | .default => mkCApp ``BinderInfo.default #[] + | .implicit => mkCApp ``implicit #[] + | .instImplicit => mkCApp ``instImplicit #[] + | .strictImplicit => mkCApp ``strictImplicit #[] + +open Syntax (mkCApp) in +instance : Quote FieldInfo where + quote + | ⟨fieldName, fieldFrom, type, projFn, subobject?, binderInfo, autoParam, docString⟩ => + mkCApp ``FieldInfo.mk #[quote fieldName, quote fieldFrom, quote type, quote projFn, quote subobject?, quote binderInfo, quote autoParam, quote docString] + + open Syntax (mkCApp) in instance : Quote BinderInfo where quote @@ -360,6 +376,15 @@ def internalSignature (name : Highlighted) (signature : Option Highlighted) : Bl name := `Verso.Genre.Manual.Block.internalSignature data := ToJson.toJson (name, signature) +def fieldSignature (name : Highlighted) (signature : Highlighted) (inheritedFrom : Option Nat) (inheritance : Array Highlighted) : Block where + name := `Verso.Genre.Manual.Block.fieldSignature + data := ToJson.toJson (name, signature, inheritedFrom, inheritance) + +def inheritance (within : Name) (inheritance : Array Block.Docstring.ParentInfo) : Block where + name := `Verso.Genre.Manual.Block.inheritance + data := ToJson.toJson (within, inheritance) + + end Block @@ -442,7 +467,7 @@ def docstringStyle := r#" .namedocs .methods td, .namedocs .fields td { vertical-align: top; } -.namedocs .inheritance td { +.namedocs .inheritance { vertical-align: top; font-size: smaller; font-family: var(--verso-structure-font-family); @@ -493,7 +518,7 @@ def docstringStyle := r#" margin-bottom: 0.5rem; } -.namedocs:has(input[data-parent-idx]) tr[data-inherited-from] { +.namedocs:has(input[data-parent-idx]) [data-inherited-from] { transition-property: opacity, display; transition-duration: 0.4s; transition-behavior: allow-discrete; @@ -506,26 +531,25 @@ def docstringStyle := r#" str where mkFilterRule (i : Nat) : String := - ".namedocs:has(input[data-parent-idx=\"" ++ toString i ++ "\"]) tr[data-inherited-from=\"" ++ toString i ++ "\"] { + ".namedocs:has(input[data-parent-idx=\"" ++ toString i ++ "\"]) [data-inherited-from=\"" ++ toString i ++ "\"] { display: none; opacity: 0; } -.namedocs:has(input[data-parent-idx=\"" ++ toString i ++ "\"]:checked) tr[data-inherited-from=\"" ++ toString i ++"\"] { +.namedocs:has(input[data-parent-idx=\"" ++ toString i ++ "\"]:checked) [data-inherited-from=\"" ++ toString i ++"\"] { display: table-row; transform: none; opacity: 1; } -.namedocs:has(input[data-parent-idx=\"" ++ toString i ++ "\"]:checked):has(tr.inheritance[data-inherited-from=\"" ++ toString i ++"\"] .parent:hover) tr[data-inherited-from]:not([data-inherited-from=\"" ++ toString i ++"\"]) { +.namedocs:has(input[data-parent-idx=\"" ++ toString i ++ "\"]:checked):has(.inheritance[data-inherited-from=\"" ++ toString i ++"\"]:hover) [data-inherited-from]:not([data-inherited-from=\"" ++ toString i ++"\"]) { opacity: 0.5; } " -open Verso.Genre.Manual.Markdown in @[block_extension Block.docstringSection] def docstringSection.descr : BlockDescr where traverse _ _ _ := pure none - toTeX := none + toTeX := some fun _goI goB _id _info contents => contents.mapM goB toHtml := some fun _goI goB _id info contents => open Verso.Doc.Html HtmlT in open Verso.Output Html in do @@ -536,7 +560,6 @@ def docstringSection.descr : BlockDescr where {{← contents.mapM goB}} }} -open Verso.Genre.Manual.Markdown in @[block_extension Block.internalSignature] def internalSignature.descr : BlockDescr where traverse _ _ _ := pure none @@ -561,6 +584,65 @@ def internalSignature.descr : BlockDescr where }} + +@[block_extension Block.inheritance] +def inheritance.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, parents) := FromJson.fromJson? (α := Name × Array Block.Docstring.ParentInfo) info + | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize docstring structure inheritance data while generating HTML"; pure .empty + let parentRow ← do + if parents.isEmpty then pure .empty + else pure {{ + + }} + + +@[block_extension Block.fieldSignature] +def fieldSignature.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, inheritedFrom, parents) := FromJson.fromJson? (α := Highlighted × Highlighted × Option Nat × Array Highlighted) info + | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize docstring section data while generating HTML"; pure .empty + let inheritedAttr : Array (String × String) := + inheritedFrom.map (fun i => #[("data-inherited-from", toString i)]) |>.getD #[] + return {{ +
+ 
+            {{← name.toHtml}} " : " {{ ← signature.toHtml}}
+
+ {{← if inheritedFrom.isSome then do + pure {{ +
+ "Inherited from " +
    + {{ ← parents.mapM fun p => do + pure {{
  1. {{ ← p.toHtml }}
    2. }} + }} +
+
}} + else pure .empty}} +
+ {{← contents.mapM goB}} +
+
+ }} + open Verso.Genre.Manual.Markdown in @[block_extension Block.docstring] def docstring.descr : BlockDescr where @@ -646,75 +728,6 @@ where | .error e => HtmlT.logError e; pure <| Html.text true str | .ok blks => blks.mapM goB moreDeclHtml name (goB) - | .structure isClass ctor _ infos parents ancestors => - open Verso.Doc.Html in - open Verso.Output Html in do - let parentRow ← do - if parents.isEmpty then pure .empty - else pure {{ -

"Extends"

- - }} - let infos := infos.filter (·.subobject?.isNone) - pure {{ - {{ parentRow }} -

{{if isClass then "Methods" else "Fields"}}

- - {{← infos.mapM fun i => do - let inheritedAttrVal : Option String := - i.fieldFrom.head?.bind (fun n => parents.findIdx? (·.name == n.name)) |>.map toString - let inheritedAttr : Array (String × String) := inheritedAttrVal.map (fun i => #[("data-inherited-from", i)]) |>.getD #[] - - let inheritedRow : Html ← - if i.fieldFrom.isEmpty then pure Html.empty - else - pure {{ - - - - - }} - - let docRow : Html ← - if let some doc := i.docString? then do - let doc ← md2html goB doc - pure {{ - - - - - }} - else - pure Html.empty - - pure <| {{ - - - - - - }} ++ inheritedRow ++ docRow - }} -
- "Inherited from " -
    - {{ ← i.fieldFrom.mapM fun p => do - pure {{
  1. {{ ← p.hlName.toHtml }}
    2. }} - }} -
-
{{ doc }} -
{{← i.fieldName.toHtml}}" : "{{← i.type.toHtml }}
- }} - | .inductive ctors _ _ => open Verso.Doc.Html in open Verso.Output Html in do @@ -773,7 +786,7 @@ def leanFromMarkdown.inlinedescr : InlineDescr where open Verso.Output Html in open Verso.Doc.Html in some <| fun _ _ data _ => do - match FromJson.fromJson? data with + match FromJson.fromJson? (α := Highlighted) data with | .error err => HtmlT.logError <| "Couldn't deserialize Lean code while rendering inline HTML: " ++ err pure .empty @@ -781,19 +794,21 @@ def leanFromMarkdown.inlinedescr : InlineDescr where 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!"" with +def tryElabInlineCodeTerm (str : String) : DocElabM Term := do + let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos + let src := + if let some ⟨line, col⟩ := loc then s!"" + else s!"" + match Parser.runParserCategory (← getEnv) `term str src with | .error e => throw (.error (← getRef) e) | .ok stx => dbg_trace "PARSED |{stx}|" - let (newMsgs, tree) ← do + let (newMsgs, tree, e) ← do let initMsgs ← Core.getMessageLog try Core.resetMessageLog -- TODO open decls/current namespace - let tree' ← fun _ => do + let (tree', e') ← fun _ => do dbg_trace "Gonna elab..." let e ← Elab.Term.elabTerm (catchExPostpone := true) stx none dbg_trace "ELAB'ED! |{e}|" @@ -806,28 +821,29 @@ def tryElabInlineCodeTerm (decl : Name) (str : String) : DocElabM Term := do 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') + pure (InfoTree.context ctx (.node (Info.ofCommandInfo ⟨`Verso.Genre.Manual.docstring, (← getRef)⟩) (← getInfoState).trees), e') + pure (← Core.getMessageLog, tree', e') finally Core.setMessageLog initMsgs if newMsgs.hasErrors then for msg in newMsgs.errorsToWarnings.toArray do logMessage msg + throwError m!"Didn't elaborate {stx} as term" let hls := (← highlight stx #[] (PersistentArray.empty.push tree)) - logInfoAt (← getRef) stx - + logInfoAt (← getRef) m!"Elaborated {stx} -> {e}" ``(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 +def tryElabInlineCodeName (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 + dbg_trace "NAME {n} worked for {str}" let hl : Highlighted ← constTok n str ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hl)) #[Verso.Doc.Inline.code $(quote str)]) else @@ -841,12 +857,16 @@ where 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 _ _ => +def tryElabInlineCode (decls : List Name) (str : String) : DocElabM Term := do + match decls with + | decl :: decls => + -- This brings the parameters into scope, so the term elaboration version catches them! + Meta.forallTelescopeReducing (← getConstInfo decl).type fun _ _ => + tryElabInlineCode decls str + | [] => try - tryElabInlineCodeName decl str <|> - tryElabInlineCodeTerm decl str + tryElabInlineCodeName str <|> + tryElabInlineCodeTerm str catch | .error ref e => logWarningAt ref e @@ -855,10 +875,15 @@ def tryElabInlineCode (decl : Name) (str : String) : DocElabM Term := do logWarning m!"Internal exception uncaught: {e.toMessageData}" ``(Verso.Doc.Inline.code $(quote str)) -def blockFromMarkdownWithLean (name : Name) (b : MD4Lean.Block) : DocElabM Term := +/-- +Heuristically elaborate Lean fragments in Markdown code. The provided names are used as signatures, +from left to right, with the names bound by the signature being available in the local scope in +which the Lean fragments are elaborated. +-/ +def blockFromMarkdownWithLean (names : List Name) (b : MD4Lean.Block) : DocElabM Term := Markdown.blockFromMarkdown b (handleHeaders := Markdown.strongEmphHeaders) - (elabInlineCode := tryElabInlineCode name) + (elabInlineCode := tryElabInlineCode names) @[block_role_expander docstring] def docstring : BlockRoleExpander @@ -874,7 +899,7 @@ def docstring : BlockRoleExpander let some ast := MD4Lean.parse docs | throwErrorAt x "Failed to parse docstring as Markdown" - ast.blocks.mapM (blockFromMarkdownWithLean name) + ast.blocks.mapM (blockFromMarkdownWithLean [name]) if Lean.Linter.isDeprecated (← getEnv) name then logInfoAt x m!"'{x}' is deprecated" @@ -894,23 +919,48 @@ def docstring : BlockRoleExpander } let sig := Lean.Widget.tagCodeInfos ctx infos tt let signature ← some <$> renderTagged none sig ⟨{}, false⟩ - let extras ← getExtras declType + let extras ← getExtras name 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) := + getExtras (name : Name) (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])] + | .structure (isClass := isClass) (constructor := constructor) (fieldInfo := fieldInfo) (parents := parents) .. => do + let ctorRow : Term ← 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 [name, constructor.name]) + else pure #[] + let sig ← `(Verso.Doc.Block.other (Verso.Genre.Manual.Block.internalSignature $(quote constructor.hlName) none) #[$sigDesc,*]) + ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$sig]) + let parentsRow : Option Term ← do + if parents.isEmpty then pure none + else + let header := "Extends" + let inh ← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.inheritance $(quote name) $(quote parents)) #[]) + some <$> ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$inh]) + + + let fieldsRow : Term ← do + let header := if isClass then "Methods" else "Fields" + let fieldInfo := fieldInfo.filter (·.subobject?.isNone) + let fieldSigs : Array Term ← fieldInfo.mapM fun i => do + let inheritedFrom : Option Nat := + i.fieldFrom.head?.bind (fun n => parents.findIdx? (·.name == n.name)) + let sigDesc : Array Term ← + if let some docs := i.docString? then + let some mdAst := MD4Lean.parse docs + | throwError "Failed to parse docstring as Markdown" + mdAst.blocks.mapM (blockFromMarkdownWithLean [name, constructor.name]) + else + pure (#[] : Array Term) + ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.fieldSignature $(quote i.fieldName) $(quote i.type) $(quote inheritedFrom) $(quote <| parents.map (·.parent))) #[$sigDesc,*]) + ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$fieldSigs,*]) + pure <| #[ctorRow] ++ parentsRow.toArray ++ [fieldsRow] | _ => pure #[] @@ -958,7 +1008,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 (blockFromMarkdownWithLean x.getId) + let contents ← mdAst.blocks.mapM (blockFromMarkdownWithLean []) 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"