feat: add bibliography support

DocGen4/Output.lean

@@ -10,6 +10,8 @@ import DocGen4.Output.Index
 import DocGen4.Output.Module
 import DocGen4.Output.NotFound
 import DocGen4.Output.Find
+import DocGen4.Output.References
+import DocGen4.Output.Bibtex
 import DocGen4.Output.SourceLinker
 import DocGen4.Output.Search
 import DocGen4.Output.ToJson
@@ -20,6 +22,21 @@ namespace DocGen4
 
 open Lean IO System Output Process
 
+def collectBackrefs : IO (Array BackrefItem) := do
+  let mut backrefs : Array BackrefItem := #[]
+  for entry in ← System.FilePath.readDir declarationsBasePath do
+    if entry.fileName.startsWith "backrefs-" && entry.fileName.endsWith ".json" then
+      let fileContent ← FS.readFile entry.path
+      match Json.parse fileContent with
+      | .error err =>
+        throw <| IO.userError s!"failed to parse file '{entry.path}' as json: {err}"
+      | .ok jsonContent =>
+        match fromJson? jsonContent with
+        | .error err =>
+          throw <| IO.userError s!"failed to parse file '{entry.path}': {err}"
+        | .ok (arr : Array BackrefItem) => backrefs := backrefs ++ arr
+  return backrefs
+
 def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
   let findBasePath := basePath / "find"
 
@@ -35,6 +52,7 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
   let foundationalTypesHtml := ReaderT.run foundationalTypes config |>.toString
   let navbarHtml := ReaderT.run navbar config |>.toString
   let searchHtml := ReaderT.run search config |>.toString
+  let referencesHtml := ReaderT.run (references (← collectBackrefs)) config |>.toString
   let docGenStatic := #[
     ("style.css", styleCss),
     ("favicon.svg", faviconSvg),
@@ -52,7 +70,8 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
     ("index.html", indexHtml),
     ("foundational_types.html", foundationalTypesHtml),
     ("404.html", notFoundHtml),
-    ("navbar.html", navbarHtml)
+    ("navbar.html", navbarHtml),
+    ("references.html", referencesHtml)
   ]
   for (fileName, content) in docGenStatic do
     FS.writeFile (basePath / fileName) content
@@ -72,14 +91,15 @@ def htmlOutputDeclarationDatas (result : AnalyzerResult) : HtmlT IO Unit := do
 
 def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (sourceUrl? : Option String) : IO Unit := do
   let config : SiteContext := {
-    result := result,
+    result := result
     sourceLinker := SourceLinker.sourceLinker sourceUrl?
+    refsMap := .ofList (baseConfig.refs.map fun x => (x.citekey, x)).toList
   }
 
   FS.createDirAll basePath
   FS.createDirAll declarationsBasePath
 
-  discard <| htmlOutputDeclarationDatas result |>.run config baseConfig
+  discard <| htmlOutputDeclarationDatas result |>.run {} config baseConfig
 
   for (modName, module) in result.moduleInfo.toArray do
     let fileDir := moduleNameToDirectory basePath modName
@@ -90,16 +110,29 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
       depthToRoot := modName.components.dropLast.length
       currentName := some modName
     }
-    let moduleHtml := moduleToHtml module |>.run config baseConfig
+    let (moduleHtml, cfg) := moduleToHtml module |>.run {} config baseConfig
+    if not cfg.errors.isEmpty then
+      throw <| IO.userError s!"There are errors when generating '{filePath}': {cfg.errors}"
     FS.createDirAll fileDir
     FS.writeFile filePath moduleHtml.toString
+    FS.writeFile (declarationsBasePath / s!"backrefs-{module.name}.json") (toString (toJson cfg.backrefs))
 
 def getSimpleBaseContext (hierarchy : Hierarchy) : IO SiteBaseContext := do
-  return {
-    depthToRoot := 0,
-    currentName := none,
-    hierarchy
-  }
+  let contents ← FS.readFile (declarationsBasePath / "references.json") <|> (pure "[]")
+  match Json.parse contents with
+  | .error err =>
+    throw <| IO.userError s!"Failed to parse 'references.json': {err}"
+  | .ok jsonContent =>
+    match fromJson? jsonContent with
+    | .error err =>
+      throw <| IO.userError s!"Failed to parse 'references.json': {err}"
+    | .ok (refs : Array BibItem) =>
+      return {
+        depthToRoot := 0
+        currentName := none
+        hierarchy := hierarchy
+        refs := refs
+      }
 
 def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
   htmlOutputSetup baseConfig

DocGen4/Output/Base.lean

@@ -17,6 +17,32 @@ def basePath := lakeBuildDir / "doc"
 def srcBasePath := basePath / "src"
 def declarationsBasePath := lakeBuildDir / "doc-data"
 
+/-- The structure representing a processed bibitem. -/
+structure BibItem where
+  /-- The cite key as in the bib file. -/
+  citekey : String
+  /-- The tag generated by bib processor, e.g. `[Doe12]`.
+  Should be plain text and should not be escaped. -/
+  tag : String
+  /-- The HTML generated by bib processor, e.g.
+  `John Doe. <i>Test</i>. 2012.`-/
+  html : String
+  /-- The plain text form of `html` field. Should not be escaped. -/
+  plaintext : String
+  deriving FromJson, ToJson
+
+/-- The structure representing a backref item. -/
+structure BackrefItem where
+  /-- The cite key as in the bib file. -/
+  citekey : String
+  /-- The name of the module. -/
+  modName : Name
+  /-- The name of the function, as a string. It is empty if the backref is in modstring. -/
+  funName : String
+  /-- The index of the backref in that module, starting from zero. -/
+  index : Nat
+  deriving FromJson, ToJson, Inhabited
+
 /--
 The context used in the `BaseHtmlM` monad for HTML templating.
 -/
@@ -35,9 +61,13 @@ structure SiteBaseContext where
   pages that don't have a module name.
   -/
   currentName : Option Name
+  /--
+  The list of references, as an array.
+  -/
+  refs : Array BibItem
 
 /--
-The context used in the `HtmlM` monad for HTML templating.
+The read-only context used in the `HtmlM` monad for HTML templating.
 -/
 structure SiteContext where
   /--
@@ -48,27 +78,61 @@ structure SiteContext where
   A function to link declaration names to their source URLs, usually Github ones.
   -/
   sourceLinker : Name → Option DeclarationRange → String
+  /--
+  The references as a map.
+  -/
+  refsMap : HashMap String BibItem
+
+/--
+The writable state used in the `HtmlM` monad for HTML templating.
+-/
+structure SiteState where
+  /--
+  The list of back references, as an array.
+  -/
+  backrefs : Array BackrefItem := #[]
+  /--
+  The errors occurred during the process.
+  -/
+  errors : String := ""
 
 def setCurrentName (name : Name) (ctx : SiteBaseContext) := {ctx with currentName := some name}
 
 abbrev BaseHtmlT := ReaderT SiteBaseContext
 abbrev BaseHtmlM := BaseHtmlT Id
 
-abbrev HtmlT (m) := ReaderT SiteContext (BaseHtmlT m)
+abbrev HtmlT (m) := StateT SiteState <| ReaderT SiteContext <| BaseHtmlT m
 abbrev HtmlM := HtmlT Id
 
-def HtmlT.run (x : HtmlT m α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : m α :=
-  ReaderT.run x ctx |>.run baseCtx
+def HtmlT.run (x : HtmlT m α) (state : SiteState) (ctx : SiteContext)
+    (baseCtx : SiteBaseContext) : m (α × SiteState) :=
+  StateT.run x state |>.run ctx |>.run baseCtx
 
-def HtmlM.run (x : HtmlM α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : α :=
-  ReaderT.run x ctx |>.run baseCtx |>.run
+def HtmlM.run (x : HtmlM α) (state : SiteState) (ctx : SiteContext)
+    (baseCtx : SiteBaseContext) : α × SiteState :=
+  StateT.run x state |>.run ctx |>.run baseCtx |>.run
 
 instance [Monad m] : MonadLift HtmlM (HtmlT m) where
-  monadLift x := do return x.run (← readThe SiteContext) (← readThe SiteBaseContext)
+  monadLift x := do return (x.run (← getThe SiteState) (← readThe SiteContext) (← readThe SiteBaseContext)).1
 
 instance [Monad m] : MonadLift BaseHtmlM (BaseHtmlT m) where
   monadLift x := do return x.run (← readThe SiteBaseContext)
 
+/-- Add a backref of the given `citekey` and `funName` to current document, and returns it. -/
+def addBackref (citekey funName : String) : HtmlM BackrefItem := do
+  let newBackref : BackrefItem := {
+    citekey := citekey
+    modName := (← readThe SiteBaseContext).currentName.get!
+    funName := funName
+    index := (← get).backrefs.size
+  }
+  modify fun cfg => { cfg with backrefs := cfg.backrefs.push newBackref }
+  pure newBackref
+
+/-- Add an error message to errors of current document. -/
+def addError (err : String) : HtmlM Unit := do
+  modify fun cfg => { cfg with errors := cfg.errors ++ err ++ "\n" }
+
 /--
 Obtains the root URL as a relative one to the current depth.
 -/

DocGen4/Output/Bibtex.lean

@@ -0,0 +1,42 @@
+import DocGen4.Output.References
+import BibtexQuery.Parser
+import BibtexQuery.Format
+
+/-!
+
+# bib file processor using `BibtexQuery`
+
+This file contains functions for bib file processor using
+pure Lean library `BibtexQuery`.
+
+The main function is `DocGen4.Bibtex.process`.
+
+-/
+
+open Lean Xml DocGen4 Output BibtexQuery
+
+namespace DocGen4.Bibtex
+
+/-- Process the contents of bib file. -/
+def process' (contents : String) : Except String (Array BibItem) := do
+  match BibtexQuery.Parser.bibtexFile contents.iter with
+  | .success _ arr =>
+    let arr ← arr.toArray.filterMapM ProcessedEntry.ofEntry
+    return arr |> sortEntry |> deduplicateTag |>.map fun x =>
+      let html := Formatter.format x
+      {
+        citekey := x.name
+        tag := x.tag
+        html := html.map cToStringEscaped |>.toList |> String.join
+        plaintext := html.map cToPlaintext |>.toList |> String.join
+      }
+  | .error it err =>
+    throw s!"failed to parse bib file at pos {it.2}: {err}"
+
+/-- Process the contents of bib file. -/
+def process (contents : String) : IO (Array BibItem) := do
+  match process' contents with
+  | .ok ret => return ret
+  | .error err => throw <| IO.userError err
+
+end DocGen4.Bibtex