Merge pull request #33 from xubaiw/docstring

Docstring support

DocGen4/Output.lean

@@ -71,7 +71,7 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do
 
   let mut declList := #[]
   for (_, mod) in result.moduleInfo.toArray do
-    for decl in mod.members do
+    for decl in filterMapDocInfo mod.members do
       let findHtml := ReaderT.run (findRedirectHtml decl.getName) config
       let findDir := basePath / "find" / decl.getName.toString
       FS.createDirAll findDir
@@ -86,6 +86,7 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do
   FS.writeFile (basePath / "404.html") notFoundHtml.toString
   FS.writeFile (basePath / "nav.js") navJs
   FS.writeFile (basePath / "search.js") searchJs
+  FS.writeFile (basePath / "mathjax-config.js") mathjaxConfigJs
   for (module, content) in result.moduleInfo.toArray do
     let moduleHtml := ReaderT.run (moduleToHtml content) config
     let path := moduleNameToFile basePath module

DocGen4/Output/Base.lean

@@ -49,6 +49,7 @@ section Static
   def styleCss : String := include_str "./static/style.css"
   def navJs : String := include_str "./static/nav.js"
   def searchJs : String := include_str "./static/search.js"
+  def mathjaxConfigJs : String := include_str "./static/mathjax-config.js"
 end Static
 
 def declNameToLink (name : Name) : HtmlM String := do

DocGen4/Output/Class.lean

@@ -21,7 +21,7 @@ def classInstancesToHtml (instances : Array Name) : HtmlM Html := do
     </details>
 
 def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do
-  pure $ (←structureToHtml i.toStructureInfo).push (←classInstancesToHtml i.instances)
+  pure $ (←structureToHtml i.toStructureInfo)
 
 end Output
 end DocGen4

DocGen4/Output/ClassInductive.lean

@@ -7,7 +7,7 @@ namespace DocGen4
 namespace Output
 
 def classInductiveToHtml (i : ClassInductiveInfo) : HtmlM (Array Html) := do
-  pure $ (←inductiveToHtml i.toInductiveInfo).push (←classInstancesToHtml i.instances)
+  pure $ (←inductiveToHtml i.toInductiveInfo)
 
 end Output
 end DocGen4

DocGen4/Output/Definition.lean

@@ -1,4 +1,5 @@
 import DocGen4.Output.Template
+import DocGen4.Output.DocString
 
 namespace DocGen4
 namespace Output
@@ -9,23 +10,17 @@ open Lean Widget
 def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
   pure <li «class»="equation">[←infoFormatToHtml c]</li>
 
-def equationsToHtml (i : DefinitionInfo) : HtmlM (Option Html) := do
+def equationsToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
   if let some eqs := i.equations then
     let equationsHtml ← eqs.mapM equationToHtml
-    pure
+    pure #[
       <details>
         <summary>Equations</summary>
         <ul «class»="equations">
           [equationsHtml]
         </ul>
       </details>
-  else
-    pure none
-
-def definitionToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
-  let equationsHtml ← equationsToHtml i
-  if let some equationsHtml := equationsHtml then
-    pure #[equationsHtml]
+    ]
   else
     pure #[]
 

DocGen4/Output/DocString.lean

@@ -0,0 +1,211 @@
+import CMark
+import DocGen4.Output.Template
+import Lean.Data.Parsec
+import Unicode.General.GeneralCategory
+
+open Lean Unicode  Xml Parser Parsec
+
+namespace DocGen4
+namespace Output
+
+/-- Auxiliary function for `splitAround`. -/
+@[specialize] partial def splitAroundAux (s : String) (p : Char → Bool) (b i : String.Pos) (r : List String) : List String :=
+  if s.atEnd i then
+    let r := (s.extract b i)::r
+    r.reverse
+  else
+    let c := s.get i
+    if p c then
+      let i := s.next i
+      splitAroundAux s p i i (c.toString::s.extract b (i-1)::r)
+    else
+      splitAroundAux s p b (s.next i) r
+
+/--
+  Similar to `Stirng.split` in Lean core, but keeps the separater.
+  e.g. `splitAround "a,b,c" (λ c => c = ',') = ["a", ",", "b", ",", "c"]`
+-/
+def splitAround (s : String) (p : Char → Bool) : List String := splitAroundAux s p 0 0 []
+
+instance : Inhabited Element := ⟨"", Std.RBMap.empty, #[]⟩
+
+/-- Parse an array of Xml/Html document from String. -/
+def manyDocument : Parsec (Array Element) := many (prolog *> element <* many Misc) <* eof
+
+/--
+  Generate id for heading elements, with the following rules:
+
+  1. Characters in `letter`, `mark`, `number` and `symbol` unicode categories are preserved.
+  2. Any sequences of Characters in `punctuation`, `separator` and `other` categories are replaced by a single dash.
+  3. Cases (upper and lower) are preserved.
+  4. Xml/Html tags are ignored.
+-/
+partial def xmlGetHeadingId (el : Xml.Element) : String :=
+  elementToPlainText el |> replaceCharSeq unicodeToDrop "-"
+  where
+    elementToPlainText el := match el with 
+    | (Element.Element name attrs contents) => 
+      "".intercalate (contents.toList.map contentToPlainText)
+    contentToPlainText c := match c with
+    | Content.Element el => elementToPlainText el
+    | Content.Comment _ => ""
+    | Content.Character s => s
+    replaceCharSeq pattern replacement s :=
+      s.split pattern
+      |>.filter (!·.isEmpty)
+      |> replacement.intercalate
+    unicodeToDrop (c : Char) : Bool := 
+      charInGeneralCategory c GeneralCategory.punctuation ||
+      charInGeneralCategory c GeneralCategory.separator ||
+      charInGeneralCategory c GeneralCategory.other  
+
+/--
+  This function try to find the given name, both globally and in current module.
+
+  For global search, a precise name is need. If the global search fails, the function
+  tries to find a local one that ends with the given search name.
+-/
+def nameToLink? (s : String) : HtmlM (Option String) := do
+  let res ← getResult
+  if let some name := Lean.Syntax.decodeNameLit ("`" ++ s) then
+    -- with exactly the same name
+    if res.name2ModIdx.contains name then
+      declNameToLink name
+    -- module name
+    else if res.moduleNames.contains name then
+      moduleNameToLink name
+    -- find similar name in the same module
+    else
+      match (← getCurrentName) with
+      | some currentName =>
+        match res.moduleInfo.find! currentName |>.members |> filterMapDocInfo |>.find? (sameEnd ·.getName name) with
+        | some info => 
+          declNameToLink info.getName
+        | _ => pure none
+      | _ => pure none
+  else
+    pure none
+  where
+    -- check if two names have the same ending components
+    sameEnd n1 n2 :=
+      List.zip n1.components' n2.components'
+      |>.all λ ⟨a, b⟩ => a == b
+
+/--
+  Extend links with following rules:
+
+  1. if the link starts with `##`, a name search is used and will panic if not found
+  2. if the link starts with `#`, it's treated as id link, no modification
+  3. if the link starts with `http`, it's an absolute one, no modification
+  4. otherwise it's a relative link, extend it with base url
+-/
+def extendLink (s : String)  : HtmlM String := do
+  -- for intra doc links
+  if s.startsWith "##" then
+    if let some link ← nameToLink? (s.drop 2) then
+      pure link
+    else
+      panic! s!"Cannot find {s.drop 2}, only full name and abbrev in current module is supported"
+  -- for id 
+  else if s.startsWith "#" then
+    pure s
+  -- for absolute and relative urls
+  else if s.startsWith "http" then 
+    pure s
+  else pure ((←getRoot) ++ s)
+
+/-- Add attributes for heading. -/
+def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Element) : HtmlM Element := do
+  match el with
+  | Element.Element name attrs contents => do
+    let id := xmlGetHeadingId el
+    let anchorAttributes := Std.RBMap.empty
+      |>.insert "class" "hover-link"
+      |>.insert "href" s!"#{id}"
+    let anchor := Element.Element "a" anchorAttributes #[Content.Character "#"]
+    let newAttrs := attrs
+      |>.insert "id" id
+      |>.insert "class" "markdown-heading"
+    let newContents := (← 
+      contents.mapM (λ c => match c with
+      | Content.Element e => (modifyElement e).map (Content.Element)
+      | _ => pure c))
+      |>.push (Content.Character " ")
+      |>.push (Content.Element anchor)
+    pure ⟨ name, newAttrs, newContents⟩ 
+
+/-- Extend anchor links. -/
+def extendAnchor (el : Element) : HtmlM Element := do
+  match el with
+  | Element.Element name attrs contents =>
+    let root ← getRoot
+    let newAttrs ← match (attrs.find? "href").map extendLink with
+    | some href => href.map (attrs.insert "href")
+    | none => pure attrs
+    pure ⟨ name, newAttrs, contents⟩
+
+/-- Automatically add intra documentation link for inline code span. -/
+def autoLink (el : Element) : HtmlM Element := do
+  match el with
+  | Element.Element name attrs contents =>
+    let mut newContents := #[]
+    for c in contents do
+      match c with
+      | Content.Character s =>
+        newContents := newContents ++ (← splitAround s unicodeToSplit |>.mapM linkify).join
+      | _ => newContents := newContents.push c
+    pure ⟨ name, attrs, newContents ⟩
+  where
+    linkify s := do
+      let link? ← nameToLink? s
+      match link? with
+      | some link => 
+        let attributes := Std.RBMap.empty.insert "href" link
+        pure [Content.Element $ Element.Element "a" attributes #[Content.Character s]]
+      | none =>
+        let sHead := s.dropRightWhile (λ c => c ≠ '.')
+        let sTail := s.takeRightWhile (λ c => c ≠ '.')
+        let link'? ← nameToLink? sTail
+        match link'? with
+        | some link' => 
+          let attributes := Std.RBMap.empty.insert "href" link'
+          pure [
+            Content.Character sHead,
+            Content.Element $ Element.Element "a" attributes #[Content.Character sTail]
+          ]
+        | none =>
+          pure [Content.Character s]
+    unicodeToSplit (c : Char) : Bool := 
+      charInGeneralCategory c GeneralCategory.separator ||
+      charInGeneralCategory c GeneralCategory.other  
+/-- Core function of modifying the cmark rendered docstring html. -/
+partial def modifyElement (element : Element) : HtmlM Element :=
+  match element with
+  | el@(Element.Element name attrs contents) => do
+    -- add id and class to <h_></h_>
+    if name = "h1" ∨ name = "h2" ∨ name = "h3" ∨ name = "h4" ∨ name = "h5" ∨ name = "h6" then
+      addHeadingAttributes el modifyElement
+    -- extend relative href for <a></a>
+    else if name = "a" then
+      extendAnchor el
+    -- auto link for inline <code></code>
+    else if name = "code" then
+      autoLink el
+    -- recursively modify
+    else
+      let newContents ← contents.mapM λ c => match c with
+        | Content.Element e => (modifyElement e).map Content.Element
+        | _ => pure c
+      pure ⟨ name, attrs, newContents ⟩ 
+
+/-- Convert docstring to Html. -/
+def docStringToHtml (s : String) : HtmlM (Array Html) := do
+  let rendered := CMark.renderHtml s
+  match manyDocument rendered.mkIterator with
+  | Parsec.ParseResult.success _ res => 
+    res.mapM λ x => do
+      pure (Html.text $ toString (← modifyElement x))
+  | _ => pure #[Html.text rendered]
+
+end Output
+end DocGen4

DocGen4/Output/Inductive.lean

@@ -1,4 +1,5 @@
 import DocGen4.Output.Template
+import DocGen4.Output.DocString
 
 namespace DocGen4
 namespace Output
@@ -11,7 +12,8 @@ def ctorToHtml (i : NameInfo) : HtmlM Html := do
   pure <li «class»="constructor" id={name}>{shortName} : [←infoFormatToHtml i.type]</li>
 
 def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do
-  pure #[<ul "class"="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>]
+  let constructorsHtml := <ul "class"="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>
+  pure #[constructorsHtml]
 
 end Output
 end DocGen4

DocGen4/Output/Instance.lean

@@ -4,7 +4,5 @@ import DocGen4.Output.Definition
 namespace DocGen4
 namespace Output
 
-def instanceToHtml (i : InstanceInfo) : HtmlM (Array Html) := definitionToHtml i
-
 end Output
 end DocGen4

DocGen4/Output/Module.lean

@@ -10,6 +10,8 @@ import DocGen4.Output.Class
 import DocGen4.Output.Definition
 import DocGen4.Output.Instance
 import DocGen4.Output.ClassInductive
+import DocGen4.Output.DocString
+import Lean.Data.Xml.Parser
 
 namespace DocGen4
 namespace Output
@@ -72,15 +74,23 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   pure <div «class»="decl_header"> [nodes] </div>
 
 def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
-  let docHtml ← match doc with
+  -- basic info like headers, types, structure fields, etc.
+  let docInfoHtml ← match doc with
   | DocInfo.inductiveInfo i => inductiveToHtml i
   | DocInfo.structureInfo i => structureToHtml i
   | DocInfo.classInfo i => classToHtml i
-  | DocInfo.definitionInfo i => definitionToHtml i
-  | DocInfo.instanceInfo i => instanceToHtml i
   | DocInfo.classInductiveInfo i => classInductiveToHtml i
-  | _ => pure #[]
-
+  | i => pure #[]
+  -- rendered doc stirng
+  let docStringHtml ← match doc.getDocString with
+  | some s => docStringToHtml s
+  | none => pure #[]
+  -- extra information like equations and instances
+  let extraInfoHtml ← match doc with
+  | DocInfo.classInfo i => pure #[←classInstancesToHtml i.instances]
+  | DocInfo.definitionInfo i => equationsToHtml i
+  | DocInfo.classInductiveInfo i => pure #[←classInstancesToHtml i.instances]
+  | i => pure #[]
   let attrs := doc.getAttrs
   let attrsHtml :=
     if attrs.size > 0 then
@@ -97,10 +107,23 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
         </div>
         [attrsHtml]
         {←docInfoHeader doc}
-        [docHtml]
+        [docInfoHtml]
+        [docStringHtml]
+        [extraInfoHtml]
       </div>
     </div>
 
+def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do
+  pure 
+    <div «class»="mod_doc">
+      [←docStringToHtml mdoc.doc]
+    </div>
+
+def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := do
+  match member with
+  | ModuleMember.docInfo d => docInfoToHtml module d
+  | ModuleMember.modDoc d => modDocToHtml module d
+
 def declarationToNavLink (module : Name) : Html :=
   <div «class»="nav_link">
     <a «class»="break_within" href={s!"#{module.toString}"}>{module.toString}</a>
@@ -162,10 +185,11 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
     </nav>
 
 def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do
-  let docInfos ← module.members.mapM (λ i => docInfoToHtml module.name i)
+  let memberDocs ← module.members.mapM (λ i => moduleMemberToHtml module.name i)
+  let memberNames := filterMapDocInfo module.members |>.map DocInfo.getName
   templateExtends (baseHtmlArray module.name.toString) $ pure #[
-    ←internalNav (module.members.map DocInfo.getName) module.name,
-    Html.element "main" false #[] docInfos
+    ←internalNav memberNames module.name,
+    Html.element "main" false #[] memberDocs
   ]
 
 end Output

DocGen4/Output/Structure.lean

@@ -1,4 +1,5 @@
 import DocGen4.Output.Template
+import DocGen4.Output.DocString
 
 namespace DocGen4
 namespace Output
@@ -12,21 +13,21 @@ def fieldToHtml (f : NameInfo) : HtmlM Html := do
   pure <li «class»="structure_field" id={name}>{s!"{shortName} "} : [←infoFormatToHtml f.type]</li>
 
 def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
-  if Name.isSuffixOf `mk i.ctor.name then
-    pure #[
-      <ul «class»="structure_fields" id={i.ctor.name.toString}>
+  let structureHtml :=
+    if Name.isSuffixOf `mk i.ctor.name then
+      (<ul «class»="structure_fields" id={i.ctor.name.toString}>
         [←i.fieldInfo.mapM fieldToHtml]
-      </ul>]
-  else
-    let ctorShortName := i.ctor.name.components'.head!.toString
-    pure #[
-      <ul «class»="structure_ext">
+      </ul>)
+    else
+      let ctorShortName := i.ctor.name.components'.head!.toString
+      (<ul «class»="structure_ext">
         <li id={i.ctor.name.toString} «class»="structure_ext_ctor">{s!"{ctorShortName} "} :: (</li>
         <ul «class»="structure_ext_fields">
           [←i.fieldInfo.mapM fieldToHtml]
         </ul>
         <li «class»="structure_ext_ctor">)</li>
-      </ul>]
+      </ul>)
+  pure #[structureHtml]
 
 end Output
 end DocGen4

DocGen4/Output/Template.lean

@@ -50,6 +50,10 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
       -- TODO Add more js stuff
       <script src={s!"{←getRoot}nav.js"}></script>
       <script src={s!"{←getRoot}search.js"}></script>
+      -- mathjax
+      <script src={s!"{←getRoot}mathjax-config.js"}></script>
+      <script src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
+      <script src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
       </body>
     </html>
 

DocGen4/Process.lean

@@ -101,16 +101,17 @@ def getDeclarationRange : DocInfo → DeclarationRange
 | classInfo i => i.declarationRange
 | classInductiveInfo i => i.declarationRange
 
-def lineOrder (l r : DocInfo) : Bool :=
-  l.getDeclarationRange.pos.line < r.getDeclarationRange.pos.line
-
 end DocInfo
 
+inductive ModuleMember where
+| docInfo (info : DocInfo) : ModuleMember
+| modDoc (doc : ModuleDoc) : ModuleMember
+deriving Inhabited
+
 structure Module where
   name : Name
-  doc : Option String
   -- Sorted according to their line numbers
-  members : Array DocInfo
+  members : Array ModuleMember
   deriving Inhabited
 
 partial def typeToArgsType (e : Expr) : (Array (Name × Expr × BinderInfo) × Expr) :=
@@ -451,6 +452,32 @@ def getDocString : DocInfo → Option String
 
 end DocInfo
 
+namespace ModuleMember
+
+def getDeclarationRange : ModuleMember → DeclarationRange
+| docInfo i => i.getDeclarationRange
+| modDoc i => i.declarationRange
+
+def order (l r : ModuleMember) : Bool :=
+  Position.lt l.getDeclarationRange.pos r.getDeclarationRange.pos
+
+def getName : ModuleMember → Name
+| docInfo i => i.getName
+| modDoc i => Name.anonymous
+
+def getDocString : ModuleMember → Option String
+| docInfo i => i.getDocString
+| modDoc i => i.doc
+
+end ModuleMember
+
+def filterMapDocInfo (ms : Array ModuleMember) : Array DocInfo :=
+  ms.filterMap filter
+  where
+    filter : ModuleMember → Option DocInfo
+    | ModuleMember.docInfo i => some i
+    | _ => none
+
 structure AnalyzerResult where
   name2ModIdx : HashMap Name ModuleIdx
   moduleNames : Array Name
@@ -466,13 +493,11 @@ def process : MetaM AnalyzerResult := do
   let env ← getEnv
   let mut res := mkHashMap env.header.moduleNames.size
   for module in env.header.moduleNames do
-    -- TODO: Check why modules can have multiple doc strings and add that later on
-    let moduleDoc := match getModuleDoc? env module with
-    | none => none
-    | some #[] => none
-    | some doc => (doc.get! 0).doc
-
-    res := res.insert module (Module.mk module moduleDoc #[])
+    let modDocs := match getModuleDoc? env module with
+    | none => #[]
+    | some ds => ds
+    |>.map (λ doc => ModuleMember.modDoc doc)
+    res := res.insert module (Module.mk module modDocs)
 
   for cinfo in env.constants.toList do
     try
@@ -481,7 +506,7 @@ def process : MetaM AnalyzerResult := do
         let some modidx := env.getModuleIdxFor? dinfo.getName | unreachable!
         let moduleName := env.allImportedModuleNames.get! modidx
         let module := res.find! moduleName
-        res := res.insert moduleName {module with members := module.members.push dinfo}
+        res := res.insert moduleName {module with members := module.members.push (ModuleMember.docInfo dinfo)}
     catch e =>
       IO.println s!"WARNING: Failed to obtain information for: {cinfo.fst}: {←e.toMessageData.toString}"
 
@@ -489,7 +514,7 @@ def process : MetaM AnalyzerResult := do
   let mut adj := Array.mkArray res.size (Array.mkArray res.size false)
   -- TODO: This could probably be faster if we did an insertion sort above instead
   for (moduleName, module) in res.toArray do
-    res := res.insert moduleName {module with members := module.members.qsort DocInfo.lineOrder}
+    res := res.insert moduleName {module with members := module.members.qsort ModuleMember.order}
     let some modIdx := env.getModuleIdx? moduleName | unreachable!
     let moduleData := env.header.moduleData.get! modIdx
     for imp in moduleData.imports do

lakefile.lean

@@ -4,4 +4,14 @@ open Lake DSL
 package «doc-gen4» {
   -- add configuration options here
   supportInterpreter := true
+  dependencies := #[
+    {
+      name := `CMark
+      src := Source.git "https://github.com/xubaiw/CMark.lean" "0c59e4fa0f8864502dc9e661d437be842d29d708"
+    },
+    {
+      name := `Unicode
+      src := Source.git "https://github.com/xubaiw/Unicode.lean" "3b7b85472d42854a474099928a3423bb97d4fa64"
+    }
+  ]
 }

static/mathjax-config.js

@@ -0,0 +1,17 @@
+MathJax = {
+    tex: {
+        inlineMath: [['$', '$']],
+        displayMath: [['$$', '$$']]
+    },
+    options: {
+        skipHtmlTags: [
+            'script', 'noscript', 'style', 'textarea', 'pre',
+            'code', 'annotation', 'annotation-xml',
+            'decl', 'decl_meta', 'attributes', 'decl_args', 'decl_header', 'decl_name',
+            'decl_type', 'equation', 'equations', 'structure_field', 'structure_fields',
+            'constructor', 'constructors', 'instances'
+        ],
+        ignoreHtmlClass: 'tex2jax_ignore',
+        processHtmlClass: 'tex2jax_process',
+    },
+};