Merge pull request #53 from leanprover/structuring

Restructuring and documentation.

DocGen4.lean

@@ -3,10 +3,7 @@ Copyright (c) 2021 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-import DocGen4.Hierarchy
 import DocGen4.Process
 import DocGen4.Load
-import DocGen4.ToHtmlFormat
 import DocGen4.IncludeStr
 import DocGen4.Output
-import DocGen4.Attributes

DocGen4/IncludeStr.lean

@@ -27,6 +27,11 @@ partial def traverseDir (f : FilePath) (p : FilePath → IO Bool) : IO (Option F
 
 syntax (name := includeStr) "include_str" str : term
 
+/--
+Provides a way to include the contents of a file at compile time as a String.
+This is used to include things like the CSS and JS in the binary so we
+don't have to carry them around as files.
+-/
 @[termElab includeStr] def includeStrImpl : TermElab := λ stx expectedType? => do
   let str := stx[1].isStrLit?.get!
   let srcPath := (FilePath.mk (← read).fileName)

DocGen4/Load.lean

@@ -13,6 +13,11 @@ namespace DocGen4
 
 open Lean System Std IO
 
+/--
+Sets up a lake workspace for the current project. Furthermore initialize
+the Lean search path with the path to the proper compiler from lean-toolchain
+as well as all the dependencies.
+-/
 def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × String)) := do
   let (leanInstall?, lakeInstall?) ← Lake.findInstall?
   let res ← StateT.run Lake.Cli.loadWorkspace {leanInstall?, lakeInstall?} |>.toIO'
@@ -28,10 +33,14 @@ def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × Str
     pure $ Except.ok (ws, lean.githash)
   | Except.error rc => pure $ Except.error rc
 
-def load (imports : List Name) : IO AnalyzerResult := do
+/--
+Load a list of modules from the current Lean search path into an `Environment`
+to process for documentation.
+-/
+def load (imports : List Name) : IO Process.AnalyzerResult := do
   let env ← importModules (List.map (Import.mk · false) imports) Options.empty
   -- TODO parameterize maxHeartbeats
   IO.println "Processing modules"
-  Prod.fst <$> Meta.MetaM.toIO process { maxHeartbeats := 100000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {}
+  Prod.fst <$> Meta.MetaM.toIO Process.process { maxHeartbeats := 100000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {}
 
 end DocGen4

DocGen4/Output.lean

@@ -12,74 +12,16 @@ import DocGen4.Output.Module
 import DocGen4.Output.NotFound
 import DocGen4.Output.Find
 import DocGen4.Output.Semantic
+import DocGen4.Output.SourceLinker
 
 namespace DocGen4
 
-open Lean Std IO System Output
+open Lean IO System Output Process
 
-
+/--
-/-
+The main entrypoint for outputting the documentation HTML based on an
-Three link types from git supported:
+`AnalyzerResult`.
-- https://github.com/org/repo
-- https://github.com/org/repo.git
-- git@github.com:org/repo.git
-TODO: This function is quite brittle and very github specific, we can
-probably do better.
 -/
-def getGithubBaseUrl (gitUrl : String) : String := Id.run do
-  let mut url := gitUrl
-  if url.startsWith "git@" then
-    url := url.drop 15
-    url := url.dropRight 4
-    pure s!"https://github.com/{url}"
-  else if url.endsWith ".git" then
-    pure $ url.dropRight 4
-  else
-    pure url
-
-def getProjectGithubUrl : IO String := do
-  let out ← IO.Process.output {cmd := "git", args := #["remote", "get-url", "origin"]}
-  if out.exitCode != 0 then
-    throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
-  pure out.stdout.trimRight
-
-def getProjectCommit : IO String := do
-  let out ← IO.Process.output {cmd := "git", args := #["rev-parse", "HEAD"]}
-  if out.exitCode != 0 then
-    throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
-  pure out.stdout.trimRight
-
-def sourceLinker (ws : Lake.Workspace) (leanHash : String): IO (Name → Option DeclarationRange → String) := do
-  -- Compute a map from package names to source URL
-  let mut gitMap := Std.mkHashMap
-  let projectBaseUrl := getGithubBaseUrl (←getProjectGithubUrl)
-  let projectCommit ← getProjectCommit
-  gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit)
-  for pkg in ws.packageArray do
-    for dep in pkg.dependencies do
-      let value := match dep.src with
-        | Lake.Source.git url commit => (getGithubBaseUrl url, commit)
-        -- TODO: What do we do here if linking a source is not possible?
-        | _ => ("https://example.com", "master")
-      gitMap := gitMap.insert dep.name value
-
-  pure $ λ module range =>
-    let parts := module.components.map Name.toString
-    let path := (parts.intersperse "/").foldl (· ++ ·) ""
-    let root := module.getRoot
-    let basic := if root == `Lean ∨ root == `Init ∨ root == `Std then
-      s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"
-    else
-      match ws.packageForModule? module with
-      | some pkg =>
-        let (baseUrl, commit) := gitMap.find! pkg.name
-        s!"{baseUrl}/blob/{commit}/{path}.lean"
-      | none => "https://example.com"
-
-    match range with
-    | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}"
-    | none => basic
-
 def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String) : IO Unit := do
   let config : SiteContext := { depthToRoot := 0, result := result, currentName := none, sourceLinker := ←sourceLinker ws leanHash}
   let basePath := FilePath.mk "." / "build" / "doc"

DocGen4/Output/Base.lean

@@ -5,18 +5,33 @@ Authors: Henrik Böving
 -/
 import DocGen4.Process
 import DocGen4.IncludeStr
-import DocGen4.ToHtmlFormat
+import DocGen4.Output.ToHtmlFormat
 
-namespace DocGen4
+namespace DocGen4.Output
-namespace Output
 
 open scoped DocGen4.Jsx
-open Lean System Widget Elab
+open Lean System Widget Elab Process
 
+/--
+The context used in the `HtmlM` monad for HTML templating.
+-/
 structure SiteContext where
+  /--
+  The full analysis result from the Process module.
+  -/
   result : AnalyzerResult
+  /--
+  How far away we are from the page root, used for relative links to the root.
+  -/
   depthToRoot: Nat
+  /--
+  The name of the current module if there is one, there exist a few
+  pages that don't have a module name.
+  -/
   currentName : Option Name
+  /--
+  A function to link declaration names to their source URLs, usually Github ones.
+  -/
   sourceLinker : Name → Option DeclarationRange → String
 
 def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := some name}
@@ -24,6 +39,9 @@ def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName :=
 abbrev HtmlT := ReaderT SiteContext
 abbrev HtmlM := HtmlT Id
 
+/--
+Obtains the root URL as a relative one to the current depth.
+-/
 def getRoot : HtmlM String := do
   let rec go: Nat -> String
   | 0 => "./"
@@ -35,22 +53,46 @@ def getResult : HtmlM AnalyzerResult := do pure (←read).result
 def getCurrentName : HtmlM (Option Name) := do pure (←read).currentName
 def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do pure $ (←read).sourceLinker module range
 
+/--
+If a template is meant to be extended because it for example only provides the
+header but no real content this is the way to fill the template with content.
+-/
 def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β :=
   new >>= base
 
+/--
+Returns the doc-gen4 link to a module name.
+-/
 def moduleNameToLink (n : Name) : HtmlM String := do
   let parts := n.components.map Name.toString
   pure $ (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
 
+/--
+Returns the HTML doc-gen4 link to a module name.
+-/
+def moduleToHtmlLink (module : Name) : HtmlM Html := do
+  pure <a href={←moduleNameToLink module}>{module.toString}</a>
+
+/--
+Returns the path to the HTML file that contains information about a module.
+-/
 def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath :=
   let parts := n.components.map Name.toString
   FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html"
 
+/--
+Returns the directory of the HTML file that contains information about a module.
+-/
 def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
   let parts := n.components.dropLast.map Name.toString
   basePath / parts.foldl (· / ·) (FilePath.mk ".")
 
+
 section Static
+/-!
+The following section contains all the statically included files that
+are used in documentation generation, notably JS and CSS ones.
+-/
   def styleCss : String := include_str "../../static/style.css"
   def declarationDataCenterJs : String := include_str "../../static/declaration-data.js"
   def navJs : String := include_str "../../static/nav.js"
@@ -60,11 +102,41 @@ section Static
   def mathjaxConfigJs : String := include_str "../../static/mathjax-config.js"
 end Static
 
+/--
+Returns the doc-gen4 link to a declaration name.
+-/
 def declNameToLink (name : Name) : HtmlM String := do
   let res ← getResult
   let module := res.moduleNames[res.name2ModIdx.find! name]
   pure $ (←moduleNameToLink module) ++ "#" ++ name.toString
 
+/--
+Returns the HTML doc-gen4 link to a declaration name.
+-/
+def declNameToHtmlLink (name : Name) : HtmlM Html := do
+  let link ← declNameToLink name
+  pure <a href={←declNameToLink name}>{name.toString}</a>
+
+/--
+Returns the HTML doc-gen4 link to a declaration name with "break_within"
+set as class.
+-/
+def declNameToHtmlBreakWithinLink (name : Name) : HtmlM Html := do
+  let link ← declNameToLink name
+  pure <a class="break_within" href={←declNameToLink name}>{name.toString}</a>
+
+/--
+In Lean syntax declarations the following pattern is quite common:
+```
+syntax term " + " term : term
+```
+that is, we place spaces around the operator in the middle. When the
+`InfoTree` framework provides us with information about what source token
+corresponds to which identifier it will thus say that `" + "` corresponds to
+`HAdd.hadd`. This is however not the way we want this to be linked, in the HTML
+only `+` should be linked, taking care of this is what this function is
+responsible for.
+-/
 def splitWhitespaces (s : String) : (String × String × String) := Id.run do
   let front := "".pushn ' ' $ s.offsetOfPos (s.find (!Char.isWhitespace ·))
   let mut s := s.trimLeft
@@ -72,6 +144,11 @@ def splitWhitespaces (s : String) : (String × String × String) := Id.run do
   s := s.trimRight
   (front, s, back)
 
+/--
+Turns a `CodeWithInfos` object, that is basically a Lean syntax tree with
+information about what the identifiers mean, into an HTML object that links
+to as much information as possible.
+-/
 partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
   match i with
   | TaggedText.text t => pure #[Html.escape t]
@@ -93,5 +170,4 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
          pure #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
     | _ => pure #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
 
-end Output
+end DocGen4.Output
-end DocGen4

DocGen4/Output/Class.lean

@@ -1,5 +1,6 @@
 import DocGen4.Output.Template
 import DocGen4.Output.Structure
+import DocGen4.Process
 
 namespace DocGen4
 namespace Output
@@ -8,7 +9,7 @@ open scoped DocGen4.Jsx
 open Lean
 
 def classInstanceToHtml (name : Name) : HtmlM Html := do
-  pure <li><a href={←declNameToLink name}>{name.toString}</a></li>
+  pure <li>{←declNameToHtmlLink name}</li>
 
 def classInstancesToHtml (instances : Array Name) : HtmlM Html := do
   let instancesHtml ← instances.mapM classInstanceToHtml
@@ -20,7 +21,7 @@ def classInstancesToHtml (instances : Array Name) : HtmlM Html := do
         </ul>
     </details>
 
-def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do
+def classToHtml (i : Process.ClassInfo) : HtmlM (Array Html) := do
   pure $ (←structureToHtml i.toStructureInfo)
 
 end Output

DocGen4/Output/ClassInductive.lean

@@ -1,12 +1,13 @@
 import DocGen4.Output.Template
 import DocGen4.Output.Class
 import DocGen4.Output.Inductive
+import DocGen4.Process
 
 
 namespace DocGen4
 namespace Output
 
-def classInductiveToHtml (i : ClassInductiveInfo) : HtmlM (Array Html) := do
+def classInductiveToHtml (i : Process.ClassInductiveInfo) : HtmlM (Array Html) := do
   pure $ (←inductiveToHtml i.toInductiveInfo)
 
 end Output

DocGen4/Output/Definition.lean

@@ -1,5 +1,6 @@
 import DocGen4.Output.Template
 import DocGen4.Output.DocString
+import DocGen4.Process
 
 namespace DocGen4
 namespace Output
@@ -7,13 +8,19 @@ namespace Output
 open scoped DocGen4.Jsx
 open Lean Widget
 
-/- This is basically an arbitrary number that seems to work okay. -/
+/-- This is basically an arbitrary number that seems to work okay. -/
 def equationLimit : Nat := 200
 
 def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
   pure <li class="equation">[←infoFormatToHtml c]</li>
 
-def equationsToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
+/--
+Attempt to render all `simp` equations for this definition. At a size
+defined in `equationLimit` we stop trying since they:
+- are too ugly to read most of the time
+- take too long
+-/
+def equationsToHtml (i : Process.DefinitionInfo) : HtmlM (Array Html) := do
   if let some eqs := i.equations then
     let equationsHtml ← eqs.mapM equationToHtml
     let filteredEquationsHtml := equationsHtml.filter (λ eq => eq.textLength < equationLimit)

DocGen4/Output/DocString.lean

@@ -3,7 +3,7 @@ import DocGen4.Output.Template
 import Lean.Data.Parsec
 import Unicode.General.GeneralCategory
 
-open Lean Unicode  Xml Parser Parsec
+open Lean Unicode  Xml Parser Parsec DocGen4.Process
 
 namespace DocGen4
 namespace Output

DocGen4/Output/Index.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-import DocGen4.ToHtmlFormat
+import DocGen4.Output.ToHtmlFormat
 import DocGen4.Output.Template
 
 namespace DocGen4

DocGen4/Output/Inductive.lean

@@ -1,17 +1,18 @@
 import DocGen4.Output.Template
 import DocGen4.Output.DocString
+import DocGen4.Process
 
 namespace DocGen4
 namespace Output
 
 open scoped DocGen4.Jsx
 
-def ctorToHtml (i : NameInfo) : HtmlM Html := do
+def ctorToHtml (i : Process.NameInfo) : HtmlM Html := do
   let shortName := i.name.components'.head!.toString
   let name := i.name.toString
   pure <li class="constructor" id={name}>{shortName} : [←infoFormatToHtml i.type]</li>
 
-def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do
+def inductiveToHtml (i : Process.InductiveInfo) : HtmlM (Array Html) := do
   let constructorsHtml := <ul class="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>
   pure #[constructorsHtml]
 

DocGen4/Output/Module.lean

@@ -11,14 +11,19 @@ import DocGen4.Output.Definition
 import DocGen4.Output.Instance
 import DocGen4.Output.ClassInductive
 import DocGen4.Output.DocString
+import DocGen4.Process
 import Lean.Data.Xml.Parser
 
 namespace DocGen4
 namespace Output
 
 open scoped DocGen4.Jsx
-open Lean
+open Lean Process
 
+/--
+Render an `Arg` as HTML, adding opacity effects etc. depending on what
+type of binder it has.
+-/
 def argToHtml (arg : Arg) : HtmlM Html := do
   let (l, r, implicit) := match arg.binderInfo with
   | BinderInfo.default => ("(", ")", false)
@@ -37,19 +42,27 @@ def argToHtml (arg : Arg) : HtmlM Html := do
   else
     pure html
 
-def structureInfoHeader (s : StructureInfo) : HtmlM (Array Html) := do
+/--
+Render the structures this structure extends from as HTML so it can be
+added to the top level.
+-/
+def structureInfoHeader (s : Process.StructureInfo) : HtmlM (Array Html) := do
   let mut nodes := #[]
   if s.parents.size > 0 then
     nodes := nodes.push <span class="decl_extends">extends</span>
     let mut parents := #[]
     for parent in s.parents do
-      let link := <a class="break_within" href={←declNameToLink parent}>{parent.toString}</a>
+      let link ← declNameToHtmlBreakWithinLink parent
       let inner := Html.element "span" true #[("class", "fn")] #[link]
       let html:= Html.element "span" false #[("class", "decl_parent")] #[inner]
       parents := parents.push html
     nodes := nodes.append (parents.toList.intersperse (Html.text ", ")).toArray
   pure nodes
 
+/--
+Render the general header of a declaration containing its declaration type
+and name.
+-/
 def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   let mut nodes := #[]
   nodes := nodes.push <span class="decl_kind">{doc.getKindDescription}</span>
@@ -63,7 +76,6 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   for arg in doc.getArgs do
     nodes := nodes.push (←argToHtml arg)
 
-  -- TODO: dedup this
   match doc with
   | DocInfo.structureInfo i => nodes := nodes.append (←structureInfoHeader i)
   | DocInfo.classInfo i => nodes := nodes.append (←structureInfoHeader i.toStructureInfo)
@@ -73,6 +85,9 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType)
   pure <div class="decl_header"> [nodes] </div>
 
+/--
+The main entry point for rendering a single declaration inside a given module.
+-/
 def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
   -- basic info like headers, types, structure fields, etc.
   let docInfoHtml ← match doc with
@@ -114,12 +129,20 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
       </div>
     </div>
 
+/--
+Rendering a module doc string, that is the ones with an ! after the opener
+as HTML.
+-/
 def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do
   pure 
     <div class="mod_doc">
       [←docStringToHtml mdoc.doc]
     </div>
 
+/--
+Render a module member, that is either a module doc string or a declaration
+as HTML.
+-/
 def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := do
   match member with
   | ModuleMember.docInfo d => docInfoToHtml module d
@@ -130,10 +153,9 @@ def declarationToNavLink (module : Name) : Html :=
     <a class="break_within" href={s!"#{module.toString}"}>{module.toString}</a>
   </div>
 
--- TODO: Similar functions are used all over the place, we should dedup them
+/--
-def moduleToNavLink (module : Name) : HtmlM Html := do
+Returns the list of all imports this module does.
-  pure <a href={←moduleNameToLink module}>{module.toString}</a>
+-/
-
 def getImports (module : Name) : HtmlM (Array Name) := do
   let res ← getResult
   let some idx := res.moduleNames.findIdx? (. == module) | unreachable!
@@ -144,6 +166,17 @@ def getImports (module : Name) : HtmlM (Array Name) := do
       imports := imports.push (res.moduleNames.get! i)
   pure imports
 
+/--
+Sort the list of all modules this one is importing, linkify it
+and return the HTML.
+-/
+def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
+  let imports := (←getImports moduleName) |>.qsort Name.lt
+  imports.mapM (λ i => do pure <li>{←moduleToHtmlLink i}</li>)
+
+/--
+Returns a list of all modules this module is imported by.
+-/
 def getImportedBy (module : Name) : HtmlM (Array Name) := do
   let res ← getResult
   let some idx := res.moduleNames.findIdx? (. == module) | unreachable!
@@ -154,15 +187,17 @@ def getImportedBy (module : Name) : HtmlM (Array Name) := do
       impBy := impBy.push (res.moduleNames.get! i)
   pure impBy
 
+/--
+Sort the list of all modules this one is imported by, linkify it
+and return the HTML.
+-/
 def importedByHtml (moduleName : Name) : HtmlM (Array Html) := do
   let imports := (←getImportedBy moduleName) |>.qsort Name.lt
-  imports.mapM (λ i => do pure <li>{←moduleToNavLink i}</li>)
+  imports.mapM (λ i => do pure <li>{←moduleToHtmlLink i}</li>)
-
-
-def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
-  let imports := (←getImports moduleName) |>.qsort Name.lt
-  imports.mapM (λ i => do pure <li>{←moduleToNavLink i}</li>)
 
+/--
+Render the internal nav bar (the thing on the right on all module pages).
+-/
 def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
   pure
     <nav class="internal_nav">
@@ -185,10 +220,13 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
       [members.map declarationToNavLink]
     </nav>
 
-def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do
+/--
+The main entry point to rendering the HTML for an entire module.
+-/
+def moduleToHtml (module : Process.Module) : HtmlM Html := withReader (setCurrentName module.name) do
   let memberDocs ← module.members.mapM (λ i => moduleMemberToHtml module.name i)
   let memberNames := filterMapDocInfo module.members |>.map DocInfo.getName
-  templateExtends (baseHtmlArray module.name.toString) $ pure #[
+  templateExtends (baseHtmlGenerator module.name.toString) $ pure #[
     ←internalNav memberNames module.name,
     Html.element "main" false #[] memberDocs
   ]

DocGen4/Output/Navbar.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 import Lean
-import DocGen4.ToHtmlFormat
+import DocGen4.Output.ToHtmlFormat
 import DocGen4.Output.Base
 
 namespace DocGen4
@@ -15,9 +15,12 @@ open scoped DocGen4.Jsx
 
 def moduleListFile (file : Name) : HtmlM Html := do
   pure <div class={if (← getCurrentName) == file then "nav_link visible" else "nav_link"}>
-    <a href={← moduleNameToLink file}>{file.toString}</a>
+    {←moduleToHtmlLink file}
   </div>
 
+/--
+Build the HTML tree representing the module hierarchy.
+-/
 partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
   let children := Array.mk (h.getChildren.toList.map Prod.snd)
   let dirs := children.filter (λ c => c.getChildren.toList.length != 0)
@@ -31,7 +34,7 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
       [if (←getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>
       {
         if (←getResult).moduleInfo.contains h.getName then
-          Html.element "summary" true #[] #[<a "href"={← moduleNameToLink h.getName}>{h.getName.toString}</a>]
+          Html.element "summary" true #[] #[←moduleToHtmlLink h.getName]
         else
           <summary>{h.getName.toString}</summary>
       }
@@ -39,6 +42,9 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
       [fileNodes]
     </details>
 
+/--
+Return a list of top level modules, linkified and rendered as HTML
+-/
 def moduleList : HtmlM Html := do
   let hierarchy := (←getResult).hierarchy
   let mut list := Array.empty
@@ -46,6 +52,9 @@ def moduleList : HtmlM Html := do
     list := list.push $ ←moduleListDir cs
   pure <div class="module_list">[list]</div>
 
+/--
+The main entry point to rendering the navbar on the left hand side.
+-/
 def navbar : HtmlM Html := do
   pure
     <nav class="nav">

DocGen4/Output/NotFound.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-import DocGen4.ToHtmlFormat
+import DocGen4.Output.ToHtmlFormat
 import DocGen4.Output.Template
 
 namespace DocGen4
@@ -11,6 +11,9 @@ namespace Output
 
 open scoped DocGen4.Jsx
 
+/--
+Render the 404 page.
+-/
 def notFound : HtmlM Html := do templateExtends (baseHtml "404") $ pure $
   <main>
     <h1>404 Not Found</h1>

DocGen4/Output/Semantic.lean

@@ -1,8 +1,9 @@
 import DocGen4.Output.Template
 import DocGen4.Output.DocString
+import DocGen4.Process
 import Lean.Data.Xml
 
-open Lean Xml
+open Lean Xml DocGen4.Process
 
 namespace DocGen4
 namespace Output

DocGen4/Output/SourceLinker.lean

@@ -0,0 +1,88 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+import Lake
+
+namespace DocGen4.Output
+
+open Lean
+
+/--
+Turns a Github git remote URL into an HTTPS Github URL.
+Three link types from git supported:
+- https://github.com/org/repo
+- https://github.com/org/repo.git
+- git@github.com:org/repo.git
+
+TODO: This function is quite brittle and very Github specific, we can
+probably do better.
+-/
+def getGithubBaseUrl (gitUrl : String) : String := Id.run do
+  let mut url := gitUrl
+  if url.startsWith "git@" then
+    url := url.drop 15
+    url := url.dropRight 4
+    pure s!"https://github.com/{url}"
+  else if url.endsWith ".git" then
+    pure $ url.dropRight 4
+  else
+    pure url
+
+/--
+Obtain the Github URL of a project by parsing the origin remote.
+-/
+def getProjectGithubUrl : IO String := do
+  let out ← IO.Process.output {cmd := "git", args := #["remote", "get-url", "origin"]}
+  if out.exitCode != 0 then
+    throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
+  pure out.stdout.trimRight
+
+/--
+Obtain the git commit hash of the project that is currently getting analyzed.
+-/
+def getProjectCommit : IO String := do
+  let out ← IO.Process.output {cmd := "git", args := #["rev-parse", "HEAD"]}
+  if out.exitCode != 0 then
+    throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
+  pure out.stdout.trimRight
+
+/--
+Given a lake workspace with all the dependencies as well as the hash of the
+compiler release to work with this provides a function to turn names of
+declarations into (optionally positional) Github URLs.
+-/
+def sourceLinker (ws : Lake.Workspace) (leanHash : String): IO (Name → Option DeclarationRange → String) := do
+  -- Compute a map from package names to source URL
+  let mut gitMap := Std.mkHashMap
+  let projectBaseUrl := getGithubBaseUrl (←getProjectGithubUrl)
+  let projectCommit ← getProjectCommit
+  gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit)
+  for pkg in ws.packageArray do
+    for dep in pkg.dependencies do
+      let value := match dep.src with
+        | Lake.Source.git url commit => (getGithubBaseUrl url, commit)
+        -- TODO: What do we do here if linking a source is not possible?
+        | _ => ("https://example.com", "master")
+      gitMap := gitMap.insert dep.name value
+
+  pure $ λ module range =>
+    let parts := module.components.map Name.toString
+    let path := (parts.intersperse "/").foldl (· ++ ·) ""
+    let root := module.getRoot
+    let basic := if root == `Lean ∨ root == `Init ∨ root == `Std then
+      s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"
+    else
+      match ws.packageForModule? module with
+      | some pkg =>
+        let (baseUrl, commit) := gitMap.find! pkg.name
+        s!"{baseUrl}/blob/{commit}/{path}.lean"
+      | none => "https://example.com"
+
+    match range with
+    | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}"
+    | none => basic
+
+end DocGen4.Output

DocGen4/Output/Structure.lean

@@ -1,5 +1,6 @@
 import DocGen4.Output.Template
 import DocGen4.Output.DocString
+import DocGen4.Process
 
 namespace DocGen4
 namespace Output
@@ -7,7 +8,10 @@ namespace Output
 open scoped DocGen4.Jsx
 open Lean
 
-def fieldToHtml (f : NameInfo) : HtmlM Html := do
+/--
+Render a single field consisting of its documentation, its name and its type as HTML.
+-/
+def fieldToHtml (f : Process.NameInfo) : HtmlM Html := do
   let shortName := f.name.components'.head!.toString
   let name := f.name.toString
   if let some doc := f.doc then
@@ -23,7 +27,10 @@ def fieldToHtml (f : NameInfo) : HtmlM Html := do
         <div class="structure_field_info">{s!"{shortName} "} : [←infoFormatToHtml f.type]</div>
       </li>
 
-def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
+/--
+Render all information about a structure as HTML.
+-/
+def structureToHtml (i : Process.StructureInfo) : HtmlM (Array Html) := do
   let structureHtml :=
     if Name.isSuffixOf `mk i.ctor.name then
       (<ul class="structure_fields" id={i.ctor.name.toString}>

DocGen4/Output/Template.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-import DocGen4.ToHtmlFormat
+import DocGen4.Output.ToHtmlFormat
 import DocGen4.Output.Navbar
 
 namespace DocGen4
@@ -11,7 +11,10 @@ namespace Output
 
 open scoped DocGen4.Jsx
 
-def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
+/--
+The HTML template used for all pages.
+-/
+def baseHtmlGenerator (title : String) (site : Array Html) : HtmlM Html := do
   pure
     <html lang="en">
       <head>
@@ -60,8 +63,10 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
 
     </html>
 
-
+/--
-def baseHtml (title : String) (site : Html) : HtmlM Html := baseHtmlArray title #[site]
+A comfortability wrapper around `baseHtmlGenerator`.
+-/
+def baseHtml (title : String) (site : Html) : HtmlM Html := baseHtmlGenerator title #[site]
 
 end Output
 end DocGen4

DocGen4/Process.lean

@@ -4,533 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 
-import Lean
+import DocGen4.Process.Analyze
-import Lean.PrettyPrinter
+import DocGen4.Process.Attributes
-import Std.Data.HashMap
+import DocGen4.Process.AxiomInfo
-import Lean.Meta.SynthInstance
+import DocGen4.Process.Base
-
+import DocGen4.Process.ClassInfo
-import DocGen4.Hierarchy
+import DocGen4.Process.DefinitionInfo
-import DocGen4.Attributes
+import DocGen4.Process.DocInfo
-
+import DocGen4.Process.Hierarchy
-namespace DocGen4
+import DocGen4.Process.InductiveInfo
-
+import DocGen4.Process.InstanceInfo
-open Lean Meta PrettyPrinter Std Widget
+import DocGen4.Process.NameInfo
-
+import DocGen4.Process.OpaqueInfo
-structure NameInfo where
+import DocGen4.Process.StructureInfo
-  name  : Name
+import DocGen4.Process.TheoremInfo
-  type : CodeWithInfos
-  doc : Option String
-  deriving Inhabited
-
-structure Arg where
-  name : Name
-  type : CodeWithInfos
-  binderInfo : BinderInfo
-
-structure Info extends NameInfo where
-  args : Array Arg
-  declarationRange : DeclarationRange
-  attrs : Array String
-  deriving Inhabited
-
-structure AxiomInfo extends Info where
-  isUnsafe : Bool
-  deriving Inhabited
-
-structure TheoremInfo extends Info
-  deriving Inhabited
-
-structure OpaqueInfo extends Info where
-  value : CodeWithInfos
-  -- A value of partial is interpreted as this constant being part of a partial def
-  -- since the actual definition for a partial def is hidden behind an inaccessible value
-  unsafeInformation : DefinitionSafety
-  deriving Inhabited
-
-structure DefinitionInfo extends Info where
-  -- partial defs are handled by OpaqueInfo
-  isUnsafe : Bool
-  hints : ReducibilityHints
-  equations : Option (Array CodeWithInfos)
-  isNonComputable : Bool
-  deriving Inhabited
-
-abbrev InstanceInfo := DefinitionInfo
-
-structure InductiveInfo extends Info where
-  ctors : List NameInfo   -- List of all constructors and their type for this inductive datatype
-  isUnsafe : Bool
-  deriving Inhabited
-
-structure StructureInfo extends Info where
-  fieldInfo : Array NameInfo
-  parents : Array Name
-  ctor : NameInfo
-  deriving Inhabited
-
-structure ClassInfo extends StructureInfo where
-  instances : Array Name
-  deriving Inhabited
-
-structure ClassInductiveInfo extends InductiveInfo where
-  instances : Array Name
-  deriving Inhabited
-
-inductive DocInfo where
-| axiomInfo (info : AxiomInfo) : DocInfo
-| theoremInfo (info : TheoremInfo) : DocInfo
-| opaqueInfo (info : OpaqueInfo) : DocInfo
-| definitionInfo (info : DefinitionInfo) : DocInfo
-| instanceInfo (info : InstanceInfo) : DocInfo
-| inductiveInfo (info : InductiveInfo) : DocInfo
-| structureInfo (info : StructureInfo) : DocInfo
-| classInfo (info : ClassInfo) : DocInfo
-| classInductiveInfo (info : ClassInductiveInfo) : DocInfo
-  deriving Inhabited
-
-namespace DocInfo
-
-def getDeclarationRange : DocInfo → DeclarationRange
-| axiomInfo i => i.declarationRange
-| theoremInfo i => i.declarationRange
-| opaqueInfo i => i.declarationRange
-| definitionInfo i => i.declarationRange
-| instanceInfo i => i.declarationRange
-| inductiveInfo i => i.declarationRange
-| structureInfo i => i.declarationRange
-| classInfo i => i.declarationRange
-| classInductiveInfo i => i.declarationRange
-
-end DocInfo
-
-inductive ModuleMember where
-| docInfo (info : DocInfo) : ModuleMember
-| modDoc (doc : ModuleDoc) : ModuleMember
-deriving Inhabited
-
-structure Module where
-  name : Name
-  -- Sorted according to their line numbers
-  members : Array ModuleMember
-  deriving Inhabited
-
-partial def typeToArgsType (e : Expr) : (Array (Name × Expr × BinderInfo) × Expr) :=
-  let helper := λ name type body data =>
-    -- Once we hit a name with a macro scope we stop traversing the expression
-    -- and print what is left after the : instead. The only exception
-    -- to this is instances since these almost never have a name
-    -- but should still be printed as arguments instead of after the :.
-    if name.hasMacroScopes ∧ ¬data.binderInfo.isInstImplicit then
-      (#[], e)
-    else
-      let name := name.eraseMacroScopes
-      let arg := (name, type, data.binderInfo)
-      let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
-      (#[arg] ++ args, final)
-
-  match e.consumeMData with
-  | Expr.lam name type body data => helper name type body data
-  | Expr.forallE name type body data => helper name type body data
-  | _ => (#[], e)
-
-def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
-  let (fmt, infos) ← formatInfos expr
-  let tt := TaggedText.prettyTagged fmt
-  let ctx := {
-    env := ← getEnv
-    mctx := ← getMCtx
-    options := ← getOptions
-    currNamespace := ← getCurrNamespace
-    openDecls := ← getOpenDecls
-    fileMap := default,
-    ngen := ← getNGen
-  }
-  pure $ tagExprInfos ctx infos tt
-
-def NameInfo.ofTypedName (n : Name) (t : Expr) : MetaM NameInfo := do
-  let env ← getEnv
-  pure { name := n, type := ←prettyPrintTerm t, doc := ←findDocString? env n}
-
-def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
-  let env ← getEnv
-  let (args, type) := typeToArgsType v.type
-  let args ← args.mapM (λ (n, e, b) => do pure $ Arg.mk n (←prettyPrintTerm e) b)
-  let doc ← findDocString? env v.name
-  let nameInfo ← NameInfo.ofTypedName v.name type
-  match ←findDeclarationRanges? v.name with
-  -- TODO: Maybe selection range is more relevant? Figure this out in the future
-  | some range => pure $ Info.mk nameInfo args range.range (←getAllAttributes v.name)
-  | none => panic! s!"{v.name} is a declaration without position"
-
-def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do
-  let info ← Info.ofConstantVal v.toConstantVal
-  pure $ AxiomInfo.mk info v.isUnsafe
-
-def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do
-  let info ← Info.ofConstantVal v.toConstantVal
-  pure $ TheoremInfo.mk info
-
-def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
-  let info ← Info.ofConstantVal v.toConstantVal
-  let t ← prettyPrintTerm v.value
-  let env ← getEnv
-  let isPartial := env.find? (Compiler.mkUnsafeRecName v.name) |>.isSome
-  if isPartial then
-    pure $ OpaqueInfo.mk info t DefinitionSafety.partial
-  else
-    let safety := if v.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe
-    pure $ OpaqueInfo.mk info t safety
-
-def isInstance (declName : Name) : MetaM Bool := do
-  pure $ (instanceExtension.getState (←getEnv)).instanceNames.contains declName
-
-partial def stripArgs (e : Expr) : Expr :=
-  match e.consumeMData with
-  | Expr.lam name type body data =>
-    let name := name.eraseMacroScopes
-    stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩))
-  | Expr.forallE name type body data =>
-    let name := name.eraseMacroScopes
-    stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩))
-  | _ => e
-
-def processEq (eq : Name) : MetaM CodeWithInfos := do
-  let type ← (mkConstWithFreshMVarLevels eq >>= inferType)
-  let final := stripArgs type
-  prettyPrintTerm final
-
-def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
-  let env ← getEnv
-  withOptions (tactic.hygienic.set . false) do
-    lambdaTelescope v.value fun xs body => do
-      let us := v.levelParams.map mkLevelParam
-      let type ← mkEq (mkAppN (Lean.mkConst v.name us) xs) body
-      let type ← mkForallFVars xs type
-      pure type
-
-def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
-  let info ← Info.ofConstantVal v.toConstantVal
-  let isUnsafe := v.safety == DefinitionSafety.unsafe
-  let isNonComput := isNoncomputable (←getEnv) v.name
-  try
-    let eqs? ← getEqnsFor? v.name
-    match eqs? with
-    | some eqs =>
-      let prettyEqs ← eqs.mapM processEq
-      pure $ DefinitionInfo.mk info isUnsafe v.hints prettyEqs isNonComput
-    | none =>
-      let eq ← prettyPrintTerm $ stripArgs (←valueToEq v)
-      pure $ DefinitionInfo.mk info isUnsafe v.hints (some #[eq]) isNonComput
-  catch err =>
-    IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}"
-    pure $ DefinitionInfo.mk info isUnsafe v.hints none isNonComput
-
-def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
-  let info ← DefinitionInfo.ofDefinitionVal v
-  let some className := getClassName (←getEnv) v.type | unreachable!
-  if let some instAttr ← getDefaultInstance v.name className then
-    pure { info with attrs := info.attrs.push instAttr }
-  else
-    pure info
-
-def getConstructorType (ctor : Name) : MetaM Expr := do
-  let env ← getEnv
-  match env.find? ctor with
-  | some (ConstantInfo.ctorInfo i) => pure i.type
-  | _ => panic! s!"Constructor {ctor} was requested but does not exist"
-
-def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
-  let info ← Info.ofConstantVal v.toConstantVal
-  let env ← getEnv
-  let ctors ← v.ctors.mapM (λ name => do NameInfo.ofTypedName name (←getConstructorType name))
-  pure $ InductiveInfo.mk info ctors v.isUnsafe
-
-def dropArgs (type : Expr) (n : Nat) : (Expr × List (Name × Expr)) :=
-  match type, n with
-  | e, 0 => (e, [])
-  | Expr.forallE name type body _, x + 1 =>
-    let body := body.instantiate1 $ mkFVar ⟨name⟩
-    let next := dropArgs body x
-    { next with snd := (name, type) :: next.snd}
-  | e, x + 1 => panic! s!"No forallE left"
-
-def getFieldTypes (struct : Name) (ctor : ConstructorVal) (parents : Nat) : MetaM (Array NameInfo) := do
-  let type := ctor.type
-  let (fieldFunction, params) := dropArgs type (ctor.numParams + parents)
-  let (_, fields) := dropArgs fieldFunction (ctor.numFields - parents)
-  let mut fieldInfos := #[]
-  for (name, type) in fields do
-    fieldInfos := fieldInfos.push $ ←NameInfo.ofTypedName (struct.append name) type
-  pure $ fieldInfos
-
-def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
-  let info ← Info.ofConstantVal v.toConstantVal
-  let env ← getEnv
-  let parents := getParentStructures env v.name
-  let ctor := getStructureCtor env v.name
-  match getStructureInfo? env v.name with
-  | some i =>
-    if i.fieldNames.size - parents.size > 0 then
-      pure $ StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents (←NameInfo.ofTypedName ctor.name ctor.type)
-    else
-      pure $ StructureInfo.mk info #[] parents (←NameInfo.ofTypedName ctor.name ctor.type)
-  | none => panic! s!"{v.name} is not a structure"
-
-def getInstances (className : Name) : MetaM (Array Name) := do
-  let fn ← mkConstWithFreshMVarLevels className
-  let (xs, _, _) ← forallMetaTelescopeReducing (← inferType fn)
-  let insts ← SynthInstance.getInstances (mkAppN fn xs)
-  pure $ insts.map Expr.constName!
-
-def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
-  let sinfo ← StructureInfo.ofInductiveVal v
-  pure $ ClassInfo.mk sinfo (←getInstances v.name)
-
-def ClassInductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInductiveInfo := do
-  let info ← InductiveInfo.ofInductiveVal v
-  pure $ ClassInductiveInfo.mk info (←getInstances v.name)
-
-namespace DocInfo
-
-def isBlackListed (declName : Name) : MetaM Bool := do
-  match ←findDeclarationRanges? declName with
-  | some _ =>
-    let env ← getEnv
-    pure (declName.isInternal)
-    <||> (pure $ isAuxRecursor env declName)
-    <||> (pure $ isNoConfusion env declName)
-    <||> isRec declName
-    <||> isMatcher declName
-  -- TODO: Evaluate whether filtering out declarations without range is sensible
-  | none => pure true
-
--- TODO: Is this actually the best way?
-def isProjFn (declName : Name) : MetaM Bool := do
-  let env ← getEnv
-  match declName with
-  | Name.str parent name _ =>
-    if isStructure env parent then
-      match getStructureInfo? env parent with
-      | some i =>
-        match i.fieldNames.find? (· == name) with
-        | some _ => pure true
-        | none => pure false
-      | none => panic! s!"{parent} is not a structure"
-    else
-      pure false
-  | _ => pure false
-
-def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, info) => do
-  if (←isBlackListed name) then
-    return none
-  match info with
-  | ConstantInfo.axiomInfo i => pure <| some <| axiomInfo (←AxiomInfo.ofAxiomVal i)
-  | ConstantInfo.thmInfo i => pure <| some <| theoremInfo (←TheoremInfo.ofTheoremVal i)
-  | ConstantInfo.opaqueInfo i => pure <| some <| opaqueInfo (←OpaqueInfo.ofOpaqueVal i)
-  | ConstantInfo.defnInfo i =>
-    if ← (isProjFn i.name) then
-      pure none
-    else
-      if (←isInstance i.name) then
-        let info ← InstanceInfo.ofDefinitionVal i
-        pure <| some <| instanceInfo info
-      else
-        let info ← DefinitionInfo.ofDefinitionVal i
-        pure <| some <| definitionInfo  info
-  | ConstantInfo.inductInfo i =>
-    let env ← getEnv
-    if isStructure env i.name then
-      if isClass env i.name then
-        pure <| some <| classInfo (←ClassInfo.ofInductiveVal i)
-      else
-        pure <| some <| structureInfo (←StructureInfo.ofInductiveVal i)
-    else
-      if isClass env i.name then
-        pure <| some <| classInductiveInfo (←ClassInductiveInfo.ofInductiveVal i)
-      else
-        pure <| some <| inductiveInfo (←InductiveInfo.ofInductiveVal i)
-  -- we ignore these for now
-  | ConstantInfo.ctorInfo i => pure none
-  | ConstantInfo.recInfo i => pure none
-  | ConstantInfo.quotInfo i => pure none
-
-def getName : DocInfo → Name
-| axiomInfo i => i.name
-| theoremInfo i => i.name
-| opaqueInfo i => i.name
-| definitionInfo i => i.name
-| instanceInfo i => i.name
-| inductiveInfo i => i.name
-| structureInfo i => i.name
-| classInfo i => i.name
-| classInductiveInfo i => i.name
-
-def getKind : DocInfo → String
-| axiomInfo _ => "axiom"
-| theoremInfo _ => "theorem"
-| opaqueInfo _ => "constant"
-| definitionInfo _ => "def"
-| instanceInfo _ => "instance"
-| inductiveInfo _ => "inductive"
-| structureInfo _ => "structure"
-| classInfo _ => "class"
-| classInductiveInfo _ => "class"
-
-def getKindDescription : DocInfo → String
-| axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom"
-| theoremInfo _ => "theorem"
-| opaqueInfo i =>
-  match i.unsafeInformation with
-  | DefinitionSafety.safe => "constant"
-  | DefinitionSafety.unsafe => "unsafe constant"
-  | DefinitionSafety.partial => "partial def"
-| definitionInfo i => Id.run do
-  if i.hints.isAbbrev then
-    pure "abbrev"
-  else
-    let mut modifiers := #[]
-    if i.isUnsafe then
-      modifiers := modifiers.push "unsafe"
-    if i.isNonComputable then
-      modifiers := modifiers.push "noncomputable"
-
-    modifiers := modifiers.push "def"
-    pure $ String.intercalate " " modifiers.toList
-| instanceInfo i => Id.run do
-  let mut modifiers := #[]
-  if i.isUnsafe then
-    modifiers := modifiers.push "unsafe"
-  if i.isNonComputable then
-    modifiers := modifiers.push "noncomputable"
-
-  modifiers := modifiers.push "instance"
-  pure $ String.intercalate " " modifiers.toList
-| inductiveInfo i => if i.isUnsafe then "unsafe inductive" else "inductive"
-| structureInfo _ => "structure"
-| classInfo _ => "class"
-| classInductiveInfo _ => "class inductive"
-
-def getType : DocInfo → CodeWithInfos
-| axiomInfo i => i.type
-| theoremInfo i => i.type
-| opaqueInfo i => i.type
-| definitionInfo i => i.type
-| instanceInfo i => i.type
-| inductiveInfo i => i.type
-| structureInfo i => i.type
-| classInfo i => i.type
-| classInductiveInfo i => i.type
-
-def getArgs : DocInfo → Array Arg
-| axiomInfo i => i.args
-| theoremInfo i => i.args
-| opaqueInfo i => i.args
-| definitionInfo i => i.args
-| instanceInfo i => i.args
-| inductiveInfo i => i.args
-| structureInfo i => i.args
-| classInfo i => i.args
-| classInductiveInfo i => i.args
-
-def getAttrs : DocInfo → Array String
-| axiomInfo i => i.attrs
-| theoremInfo i => i.attrs
-| opaqueInfo i => i.attrs
-| definitionInfo i => i.attrs
-| instanceInfo i => i.attrs
-| inductiveInfo i => i.attrs
-| structureInfo i => i.attrs
-| classInfo i => i.attrs
-| classInductiveInfo i => i.attrs
-
-def getDocString : DocInfo → Option String
-| axiomInfo i => i.doc
-| theoremInfo i => i.doc
-| opaqueInfo i => i.doc
-| definitionInfo i => i.doc
-| instanceInfo i => i.doc
-| inductiveInfo i => i.doc
-| structureInfo i => i.doc
-| classInfo i => i.doc
-| classInductiveInfo i => i.doc
-
-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
-  moduleInfo : HashMap Name Module
-  hierarchy : Hierarchy
-  -- Indexed by ModIdx
-  importAdj : Array (Array Bool)
-  deriving Inhabited
-
-deriving instance Inhabited for ModuleDoc
-
-def process : MetaM AnalyzerResult := do
-  let env ← getEnv
-  let mut res := mkHashMap env.header.moduleNames.size
-  for module in env.header.moduleNames do
-    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
-      let analysis := Prod.fst <$> Meta.MetaM.toIO (DocInfo.ofConstant cinfo) { maxHeartbeats := 5000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {}
-      if let some dinfo ← analysis then
-        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 (ModuleMember.docInfo dinfo)}
-    catch e =>
-      IO.println s!"WARNING: Failed to obtain information for: {cinfo.fst}: {←e.toMessageData.toString}"
-
-  -- TODO: This is definitely not the most efficient way to store this data
-  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 ModuleMember.order}
-    let some modIdx := env.getModuleIdx? moduleName | unreachable!
-    let moduleData := env.header.moduleData.get! modIdx
-    for imp in moduleData.imports do
-      let some importIdx := env.getModuleIdx? imp.module | unreachable!
-      adj := adj.set! modIdx (adj.get! modIdx |>.set! importIdx true)
-
-  pure {
-    name2ModIdx := env.const2ModIdx,
-    moduleNames := env.header.moduleNames,
-    moduleInfo := res,
-    hierarchy := Hierarchy.fromArray env.header.moduleNames,
-    importAdj := adj
-  }
-
-end DocGen4

DocGen4/Process/Analyze.lean

@@ -0,0 +1,140 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+
+import Lean
+import Std.Data.HashMap
+
+import DocGen4.Process.Base
+import DocGen4.Process.Hierarchy
+import DocGen4.Process.DocInfo
+
+namespace DocGen4.Process
+
+open Lean Meta Std
+
+/--
+Member of a module, either a declaration or some module doc string.
+-/
+inductive ModuleMember where
+| docInfo (info : DocInfo) : ModuleMember
+| modDoc (doc : ModuleDoc) : ModuleMember
+deriving Inhabited
+
+/--
+A Lean module.
+-/
+structure Module where
+  /--
+  Name of the module.
+  -/
+  name : Name
+  /--
+  All members of the module, sorted according to their line numbers.
+  -/
+  members : Array ModuleMember
+  deriving Inhabited
+
+/--
+The result of running a full doc-gen analysis on a project.
+-/
+structure AnalyzerResult where
+  /--
+  The map from module names to indices of the `moduleNames` array.
+  -/
+  name2ModIdx : HashMap Name ModuleIdx
+  /--
+  The list of all modules, accessible nicely via `name2ModIdx`.
+  -/
+  moduleNames : Array Name
+  /--
+  A map from module names to information about these modules.
+  -/
+  moduleInfo : HashMap Name Module
+  /--
+  The module hierarchy as a tree structure.
+  -/
+  hierarchy : Hierarchy
+  /--
+  An adjacency matrix for the import relation between modules, indexed
+  my the values in `name2ModIdx`.
+  -/
+  importAdj : Array (Array Bool)
+  deriving Inhabited
+
+namespace ModuleMember
+
+def getDeclarationRange : ModuleMember → DeclarationRange
+| docInfo i => i.getDeclarationRange
+| modDoc i => i.declarationRange
+
+/--
+An order for module members, based on their declaration range.
+-/
+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
+
+/--
+Run the doc-gen analysis on all modules that are loaded into the `Environment`
+of this `MetaM` run.
+-/
+def process : MetaM AnalyzerResult := do
+  let env ← getEnv
+  let mut res := mkHashMap env.header.moduleNames.size
+  for module in env.header.moduleNames do
+    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
+      let analysis := Prod.fst <$> Meta.MetaM.toIO (DocInfo.ofConstant cinfo) { maxHeartbeats := 5000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {}
+      if let some dinfo ← analysis then
+        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 (ModuleMember.docInfo dinfo)}
+    catch e =>
+      IO.println s!"WARNING: Failed to obtain information for: {cinfo.fst}: {←e.toMessageData.toString}"
+
+  -- TODO: This is definitely not the most efficient way to store this data
+  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 ModuleMember.order}
+    let some modIdx := env.getModuleIdx? moduleName | unreachable!
+    let moduleData := env.header.moduleData.get! modIdx
+    for imp in moduleData.imports do
+      let some importIdx := env.getModuleIdx? imp.module | unreachable!
+      adj := adj.set! modIdx (adj.get! modIdx |>.set! importIdx true)
+
+  pure {
+    name2ModIdx := env.const2ModIdx,
+    moduleNames := env.header.moduleNames,
+    moduleInfo := res,
+    hierarchy := Hierarchy.fromArray env.header.moduleNames,
+    importAdj := adj
+  }
+
+def filterMapDocInfo (ms : Array ModuleMember) : Array DocInfo :=
+  ms.filterMap filter
+  where
+    filter : ModuleMember → Option DocInfo
+    | ModuleMember.docInfo i => some i
+    | _ => none
+
+end DocGen4.Process

DocGen4/Process/Attributes.lean

@@ -3,17 +3,31 @@ import Lean
 namespace DocGen4
 
 open Lean Meta
-
 -- The following is probably completely overengineered but I love it
+
+/--
+Captures the notion of a value based attributes, `attrKind` is things like
+`EnumAttributes`.
+-/
 class ValueAttr (attrKind : Type → Type) where
+  /--
+  Given a certain value based attribute, an `Environment` and the `Name` of
+  a declaration returns the value of the attribute on this declaration if present.
+  -/
   getValue {α : Type} [Inhabited α] [ToString α] : attrKind α → Environment → Name → Option String
 
+/--
+Contains a specific attribute declaration of a certain attribute kind (enum based, parametric etc.).
+-/
 structure ValueAttrWrapper (attrKind : Type → Type) [ValueAttr attrKind] where
   {α : Type}
   attr : attrKind α
   [str : ToString α]
   [inhab : Inhabited α]
 
+/--
+Obtain the value of an enum attribute for a certain name.
+-/
 def enumGetValue {α : Type} [Inhabited α] [ToString α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option String := OptionM.run do
   let val ← EnumAttributes.getValue attr env decl
   some (toString val)
@@ -21,6 +35,9 @@ def enumGetValue {α : Type} [Inhabited α] [ToString α] (attr : EnumAttributes
 instance : ValueAttr EnumAttributes where
   getValue := enumGetValue
 
+/--
+Obtain the value of a parametric attribute for a certain name.
+-/
 def parametricGetValue {α : Type} [Inhabited α] [ToString α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option String := OptionM.run do
   let val ← ParametricAttribute.getParam attr env decl
   some (attr.attr.name.toString ++ " " ++ toString val)
@@ -31,6 +48,9 @@ instance : ValueAttr ParametricAttribute where
 abbrev EnumAttrWrapper := ValueAttrWrapper EnumAttributes
 abbrev ParametricAttrWrapper := ValueAttrWrapper ParametricAttribute
 
+/--
+The list of all tag based attributes doc-gen knows about and can recover.
+-/
 def tagAttributes : Array TagAttribute :=
   #[IR.UnboxResult.unboxAttr, neverExtractAttr, Elab.Term.elabWithoutExpectedTypeAttr,
     SynthInstance.inferTCGoalsRLAttr, matchPatternAttr]
@@ -54,6 +74,9 @@ instance : ToString SpecializeAttributeKind where
     | SpecializeAttributeKind.specialize => "specialize"
     | SpecializeAttributeKind.nospecialize => "nospecialize"
 
+/--
+The list of all enum based attributes doc-gen knows about and can recover.
+-/
 def enumAttributes : Array EnumAttrWrapper := #[⟨Compiler.inlineAttrs⟩, ⟨Compiler.specializeAttrs⟩]
 
 instance : ToString ExternEntry where
@@ -70,6 +93,10 @@ instance : ToString ExternEntry where
 instance : ToString ExternAttrData where
   toString data := (data.arity?.map toString |>.getD "") ++ " " ++ String.intercalate " " (data.entries.map toString)
 
+/--
+The list of all parametric attributes (that is, attributes with any kind of information attached)
+doc-gen knows about and can recover.
+-/
 def parametricAttributes : Array ParametricAttrWrapper := #[⟨externAttr⟩, ⟨Compiler.implementedByAttr⟩, ⟨exportAttr⟩]
 
 def getTags (decl : Name) : MetaM (Array String) := do
@@ -114,6 +141,10 @@ def hasCsimp (decl : Name) : MetaM (Option String) := do
     else
       none
 
+/--
+The list of custom attributes, that don't fit in the parametric or enum
+attribute kinds, doc-gen konws about and can recover.
+-/
 def customAttrs := #[hasSimp, hasCsimp]
 
 def getCustomAttrs (decl : Name) : MetaM (Array String) := do
@@ -123,6 +154,10 @@ def getCustomAttrs (decl : Name) : MetaM (Array String) := do
       values := values.push value
   pure values
 
+/--
+The main entry point for recovering all attribute values for a given
+declaration.
+-/
 def getAllAttributes (decl : Name) : MetaM (Array String) := do
   let tags ← getTags decl
   let enums ← getEnumValues decl

DocGen4/Process/AxiomInfo.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.NameInfo
+
+namespace DocGen4.Process
+
+open Lean Meta
+
+def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do
+  let info ← Info.ofConstantVal v.toConstantVal
+  pure $ AxiomInfo.mk info v.isUnsafe
+
+end DocGen4.Process

DocGen4/Process/Base.lean

@@ -0,0 +1,186 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+
+import Lean
+
+namespace DocGen4.Process
+open Lean Widget Meta
+
+/--
+Stores information about a typed name.
+-/
+structure NameInfo where
+  /--
+  The name that has this info attached.
+  -/
+  name  : Name
+  /--
+  The pretty printed type of this name.
+  -/
+  type : CodeWithInfos
+  /--
+  The doc string of the name if it exists.
+  -/
+  doc : Option String
+  deriving Inhabited
+
+/--
+An argument to a declaration, e.g. the `(x : Nat)` in `def foo (x : Nat) := x`.
+-/
+structure Arg where
+  /--
+  The name of the argument.
+  -/
+  name : Name
+  /--
+  The pretty printed type of the argument.
+  -/
+  type : CodeWithInfos
+  /--
+  What kind of binder was used for the argument.
+  -/
+  binderInfo : BinderInfo
+
+/--
+A base structure for information about a declaration.
+-/
+structure Info extends NameInfo where
+  /--
+  The list of arguments to the declaration.
+  -/
+  args : Array Arg
+  /--
+  In which lines the declaration was created.
+  -/
+  declarationRange : DeclarationRange
+  /--
+  A list of (known) attributes that are attached to the declaration.
+  -/
+  attrs : Array String
+  deriving Inhabited
+
+/--
+Information about an `axiom` declaration.
+-/
+structure AxiomInfo extends Info where
+  isUnsafe : Bool
+  deriving Inhabited
+
+/--
+Information about a `theorem` declaration.
+-/
+structure TheoremInfo extends Info
+  deriving Inhabited
+
+/--
+Information about a `constant` declaration.
+-/
+structure OpaqueInfo extends Info where
+  /--
+  The pretty printed value of the declaration.
+  -/
+  value : CodeWithInfos
+  /--
+  A value of partial is interpreted as this constant being part of a partial def
+  since the actual definition for a partial def is hidden behind an inaccessible value.
+  -/
+  unsafeInformation : DefinitionSafety
+  deriving Inhabited
+
+/--
+Information about a `def` declaration, note that partial defs are handled by `OpaqueInfo`.
+-/
+structure DefinitionInfo extends Info where
+  isUnsafe : Bool
+  hints : ReducibilityHints
+  equations : Option (Array CodeWithInfos)
+  isNonComputable : Bool
+  deriving Inhabited
+
+/--
+Information about an `instance` declaration.
+-/
+abbrev InstanceInfo := DefinitionInfo
+
+/--
+Information about an `inductive` declaration
+-/
+structure InductiveInfo extends Info where
+  /--
+  List of all constructors of this inductive type.
+  -/
+  ctors : List NameInfo
+  isUnsafe : Bool
+  deriving Inhabited
+
+/--
+Information about a `structure` declaration.
+-/
+structure StructureInfo extends Info where
+  /--
+  Information about all the fields of the structure.
+  -/
+  fieldInfo : Array NameInfo
+  /--
+  All the structures this one inherited from.
+  -/
+  parents : Array Name
+  /--
+  The constructor of the structure.
+  -/
+  ctor : NameInfo
+  deriving Inhabited
+
+/--
+Information about a `class` declaration.
+-/
+structure ClassInfo extends StructureInfo where
+  instances : Array Name
+  deriving Inhabited
+
+/--
+Information about a `class inductive` declaration.
+-/
+structure ClassInductiveInfo extends InductiveInfo where
+  instances : Array Name
+  deriving Inhabited
+
+/--
+A general type for informations about declarations.
+-/
+inductive DocInfo where
+| axiomInfo (info : AxiomInfo) : DocInfo
+| theoremInfo (info : TheoremInfo) : DocInfo
+| opaqueInfo (info : OpaqueInfo) : DocInfo
+| definitionInfo (info : DefinitionInfo) : DocInfo
+| instanceInfo (info : InstanceInfo) : DocInfo
+| inductiveInfo (info : InductiveInfo) : DocInfo
+| structureInfo (info : StructureInfo) : DocInfo
+| classInfo (info : ClassInfo) : DocInfo
+| classInductiveInfo (info : ClassInductiveInfo) : DocInfo
+  deriving Inhabited
+
+/--
+Turns an `Expr` into a pretty printed `CodeWithInfos`.
+-/
+def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
+  let (fmt, infos) ← formatInfos expr
+  let tt := TaggedText.prettyTagged fmt
+  let ctx := {
+    env := ← getEnv
+    mctx := ← getMCtx
+    options := ← getOptions
+    currNamespace := ← getCurrNamespace
+    openDecls := ← getOpenDecls
+    fileMap := default,
+    ngen := ← getNGen
+  }
+  pure $ tagExprInfos ctx infos tt
+
+def isInstance (declName : Name) : MetaM Bool := do
+  pure $ (instanceExtension.getState (←getEnv)).instanceNames.contains declName
+
+end DocGen4.Process

DocGen4/Process/ClassInfo.lean

@@ -0,0 +1,32 @@
+
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.NameInfo
+import DocGen4.Process.StructureInfo
+import DocGen4.Process.InductiveInfo
+
+namespace DocGen4.Process
+
+open Lean Meta 
+
+def getInstances (className : Name) : MetaM (Array Name) := do
+  let fn ← mkConstWithFreshMVarLevels className
+  let (xs, _, _) ← forallMetaTelescopeReducing (← inferType fn)
+  let insts ← SynthInstance.getInstances (mkAppN fn xs)
+  pure $ insts.map Expr.constName!
+
+def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
+  let sinfo ← StructureInfo.ofInductiveVal v
+  pure $ ClassInfo.mk sinfo (←getInstances v.name)
+
+def ClassInductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInductiveInfo := do
+  let info ← InductiveInfo.ofInductiveVal v
+  pure $ ClassInductiveInfo.mk info (←getInstances v.name)
+
+end DocGen4.Process

DocGen4/Process/DefinitionInfo.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.NameInfo
+
+namespace DocGen4.Process
+
+open Lean Meta Widget
+
+partial def stripArgs (e : Expr) : Expr :=
+  match e.consumeMData with
+  | Expr.lam name type body data =>
+    let name := name.eraseMacroScopes
+    stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩))
+  | Expr.forallE name type body data =>
+    let name := name.eraseMacroScopes
+    stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩))
+  | _ => e
+
+def processEq (eq : Name) : MetaM CodeWithInfos := do
+  let type ← (mkConstWithFreshMVarLevels eq >>= inferType)
+  let final := stripArgs type
+  prettyPrintTerm final
+
+def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
+  let env ← getEnv
+  withOptions (tactic.hygienic.set . false) do
+    lambdaTelescope v.value fun xs body => do
+      let us := v.levelParams.map mkLevelParam
+      let type ← mkEq (mkAppN (Lean.mkConst v.name us) xs) body
+      let type ← mkForallFVars xs type
+      pure type
+
+def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
+  let info ← Info.ofConstantVal v.toConstantVal
+  let isUnsafe := v.safety == DefinitionSafety.unsafe
+  let isNonComput := isNoncomputable (←getEnv) v.name
+  try
+    let eqs? ← getEqnsFor? v.name
+    match eqs? with
+    | some eqs =>
+      let prettyEqs ← eqs.mapM processEq
+      pure $ DefinitionInfo.mk info isUnsafe v.hints prettyEqs isNonComput
+    | none =>
+      let eq ← prettyPrintTerm $ stripArgs (←valueToEq v)
+      pure $ DefinitionInfo.mk info isUnsafe v.hints (some #[eq]) isNonComput
+  catch err =>
+    IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}"
+    pure $ DefinitionInfo.mk info isUnsafe v.hints none isNonComput
+
+
+end DocGen4.Process

DocGen4/Process/DocInfo.lean

@@ -0,0 +1,199 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.AxiomInfo
+import DocGen4.Process.TheoremInfo
+import DocGen4.Process.OpaqueInfo
+import DocGen4.Process.InstanceInfo
+import DocGen4.Process.DefinitionInfo
+import DocGen4.Process.ClassInfo
+import DocGen4.Process.StructureInfo
+import DocGen4.Process.InductiveInfo
+
+
+namespace DocGen4.Process
+namespace DocInfo
+
+open Lean Meta Widget
+
+def getDeclarationRange : DocInfo → DeclarationRange
+| axiomInfo i => i.declarationRange
+| theoremInfo i => i.declarationRange
+| opaqueInfo i => i.declarationRange
+| definitionInfo i => i.declarationRange
+| instanceInfo i => i.declarationRange
+| inductiveInfo i => i.declarationRange
+| structureInfo i => i.declarationRange
+| classInfo i => i.declarationRange
+| classInductiveInfo i => i.declarationRange
+
+def getName : DocInfo → Name
+| axiomInfo i => i.name
+| theoremInfo i => i.name
+| opaqueInfo i => i.name
+| definitionInfo i => i.name
+| instanceInfo i => i.name
+| inductiveInfo i => i.name
+| structureInfo i => i.name
+| classInfo i => i.name
+| classInductiveInfo i => i.name
+
+def getKind : DocInfo → String
+| axiomInfo _ => "axiom"
+| theoremInfo _ => "theorem"
+| opaqueInfo _ => "constant"
+| definitionInfo _ => "def"
+| instanceInfo _ => "instance"
+| inductiveInfo _ => "inductive"
+| structureInfo _ => "structure"
+| classInfo _ => "class"
+| classInductiveInfo _ => "class"
+
+def getType : DocInfo → CodeWithInfos
+| axiomInfo i => i.type
+| theoremInfo i => i.type
+| opaqueInfo i => i.type
+| definitionInfo i => i.type
+| instanceInfo i => i.type
+| inductiveInfo i => i.type
+| structureInfo i => i.type
+| classInfo i => i.type
+| classInductiveInfo i => i.type
+
+def getArgs : DocInfo → Array Arg
+| axiomInfo i => i.args
+| theoremInfo i => i.args
+| opaqueInfo i => i.args
+| definitionInfo i => i.args
+| instanceInfo i => i.args
+| inductiveInfo i => i.args
+| structureInfo i => i.args
+| classInfo i => i.args
+| classInductiveInfo i => i.args
+
+def getAttrs : DocInfo → Array String
+| axiomInfo i => i.attrs
+| theoremInfo i => i.attrs
+| opaqueInfo i => i.attrs
+| definitionInfo i => i.attrs
+| instanceInfo i => i.attrs
+| inductiveInfo i => i.attrs
+| structureInfo i => i.attrs
+| classInfo i => i.attrs
+| classInductiveInfo i => i.attrs
+
+def getDocString : DocInfo → Option String
+| axiomInfo i => i.doc
+| theoremInfo i => i.doc
+| opaqueInfo i => i.doc
+| definitionInfo i => i.doc
+| instanceInfo i => i.doc
+| inductiveInfo i => i.doc
+| structureInfo i => i.doc
+| classInfo i => i.doc
+| classInductiveInfo i => i.doc
+
+def isBlackListed (declName : Name) : MetaM Bool := do
+  match ←findDeclarationRanges? declName with
+  | some _ =>
+    let env ← getEnv
+    pure (declName.isInternal)
+    <||> (pure $ isAuxRecursor env declName)
+    <||> (pure $ isNoConfusion env declName)
+    <||> isRec declName
+    <||> isMatcher declName
+  -- TODO: Evaluate whether filtering out declarations without range is sensible
+  | none => pure true
+
+-- TODO: Is this actually the best way?
+def isProjFn (declName : Name) : MetaM Bool := do
+  let env ← getEnv
+  match declName with
+  | Name.str parent name _ =>
+    if isStructure env parent then
+      match getStructureInfo? env parent with
+      | some i =>
+        match i.fieldNames.find? (· == name) with
+        | some _ => pure true
+        | none => pure false
+      | none => panic! s!"{parent} is not a structure"
+    else
+      pure false
+  | _ => pure false
+
+def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, info) => do
+  if (←isBlackListed name) then
+    return none
+  match info with
+  | ConstantInfo.axiomInfo i => pure <| some <| axiomInfo (←AxiomInfo.ofAxiomVal i)
+  | ConstantInfo.thmInfo i => pure <| some <| theoremInfo (←TheoremInfo.ofTheoremVal i)
+  | ConstantInfo.opaqueInfo i => pure <| some <| opaqueInfo (←OpaqueInfo.ofOpaqueVal i)
+  | ConstantInfo.defnInfo i =>
+    if ← (isProjFn i.name) then
+      pure none
+    else
+      if (←isInstance i.name) then
+        let info ← InstanceInfo.ofDefinitionVal i
+        pure <| some <| instanceInfo info
+      else
+        let info ← DefinitionInfo.ofDefinitionVal i
+        pure <| some <| definitionInfo  info
+  | ConstantInfo.inductInfo i =>
+    let env ← getEnv
+    if isStructure env i.name then
+      if isClass env i.name then
+        pure <| some <| classInfo (←ClassInfo.ofInductiveVal i)
+      else
+        pure <| some <| structureInfo (←StructureInfo.ofInductiveVal i)
+    else
+      if isClass env i.name then
+        pure <| some <| classInductiveInfo (←ClassInductiveInfo.ofInductiveVal i)
+      else
+        pure <| some <| inductiveInfo (←InductiveInfo.ofInductiveVal i)
+  -- we ignore these for now
+  | ConstantInfo.ctorInfo i => pure none
+  | ConstantInfo.recInfo i => pure none
+  | ConstantInfo.quotInfo i => pure none
+
+def getKindDescription : DocInfo → String
+| axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom"
+| theoremInfo _ => "theorem"
+| opaqueInfo i =>
+  match i.unsafeInformation with
+  | DefinitionSafety.safe => "constant"
+  | DefinitionSafety.unsafe => "unsafe constant"
+  | DefinitionSafety.partial => "partial def"
+| definitionInfo i => Id.run do
+  if i.hints.isAbbrev then
+    pure "abbrev"
+  else
+    let mut modifiers := #[]
+    if i.isUnsafe then
+      modifiers := modifiers.push "unsafe"
+    if i.isNonComputable then
+      modifiers := modifiers.push "noncomputable"
+
+    modifiers := modifiers.push "def"
+    pure $ String.intercalate " " modifiers.toList
+| instanceInfo i => Id.run do
+  let mut modifiers := #[]
+  if i.isUnsafe then
+    modifiers := modifiers.push "unsafe"
+  if i.isNonComputable then
+    modifiers := modifiers.push "noncomputable"
+
+  modifiers := modifiers.push "instance"
+  pure $ String.intercalate " " modifiers.toList
+| inductiveInfo i => if i.isUnsafe then "unsafe inductive" else "inductive"
+| structureInfo _ => "structure"
+| classInfo _ => "class"
+| classInductiveInfo _ => "class inductive"
+
+end DocInfo
+
+end DocGen4.Process

DocGen4/Process/InductiveInfo.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.NameInfo
+
+namespace DocGen4.Process
+
+open Lean Meta 
+
+def getConstructorType (ctor : Name) : MetaM Expr := do
+  let env ← getEnv
+  match env.find? ctor with
+  | some (ConstantInfo.ctorInfo i) => pure i.type
+  | _ => panic! s!"Constructor {ctor} was requested but does not exist"
+
+def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
+  let info ← Info.ofConstantVal v.toConstantVal
+  let env ← getEnv
+  let ctors ← v.ctors.mapM (λ name => do NameInfo.ofTypedName name (←getConstructorType name))
+  pure $ InductiveInfo.mk info ctors v.isUnsafe
+
+end DocGen4.Process

DocGen4/Process/InstanceInfo.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.NameInfo
+import DocGen4.Process.DefinitionInfo
+
+namespace DocGen4.Process
+
+open Lean Meta 
+
+def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
+  let info ← DefinitionInfo.ofDefinitionVal v
+  let some className := getClassName (←getEnv) v.type | unreachable!
+  if let some instAttr ← getDefaultInstance v.name className then
+    pure { info with attrs := info.attrs.push instAttr }
+  else
+    pure info
+
+end DocGen4.Process

DocGen4/Process/NameInfo.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.Attributes
+
+namespace DocGen4.Process
+open Lean Meta
+
+def NameInfo.ofTypedName (n : Name) (t : Expr) : MetaM NameInfo := do
+  let env ← getEnv
+  pure { name := n, type := ←prettyPrintTerm t, doc := ←findDocString? env n}
+
+partial def typeToArgsType (e : Expr) : (Array (Name × Expr × BinderInfo) × Expr) :=
+  let helper := λ name type body data =>
+    -- Once we hit a name with a macro scope we stop traversing the expression
+    -- and print what is left after the : instead. The only exception
+    -- to this is instances since these almost never have a name
+    -- but should still be printed as arguments instead of after the :.
+    if name.hasMacroScopes ∧ ¬data.binderInfo.isInstImplicit then
+      (#[], e)
+    else
+      let name := name.eraseMacroScopes
+      let arg := (name, type, data.binderInfo)
+      let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
+      (#[arg] ++ args, final)
+  match e.consumeMData with
+  | Expr.lam name type body data => helper name type body data
+  | Expr.forallE name type body data => helper name type body data
+  | _ => (#[], e)
+
+def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
+  let env ← getEnv
+  let (args, type) := typeToArgsType v.type
+  let args ← args.mapM (λ (n, e, b) => do pure $ Arg.mk n (←prettyPrintTerm e) b)
+  let doc ← findDocString? env v.name
+  let nameInfo ← NameInfo.ofTypedName v.name type
+  match ←findDeclarationRanges? v.name with
+  -- TODO: Maybe selection range is more relevant? Figure this out in the future
+  | some range => pure $ Info.mk nameInfo args range.range (←getAllAttributes v.name)
+  | none => panic! s!"{v.name} is a declaration without position"
+
+end DocGen4.Process

DocGen4/Process/OpaqueInfo.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.NameInfo
+
+namespace DocGen4.Process
+
+open Lean Meta
+
+def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
+  let info ← Info.ofConstantVal v.toConstantVal
+  let t ← prettyPrintTerm v.value
+  let env ← getEnv
+  let isPartial := env.find? (Compiler.mkUnsafeRecName v.name) |>.isSome
+  if isPartial then
+    pure $ OpaqueInfo.mk info t DefinitionSafety.partial
+  else
+    let safety := if v.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe
+    pure $ OpaqueInfo.mk info t safety
+
+end DocGen4.Process

DocGen4/Process/StructureInfo.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.NameInfo
+
+namespace DocGen4.Process
+
+open Lean Meta 
+
+-- TODO: replace with Leos variant from Zulip
+def dropArgs (type : Expr) (n : Nat) : (Expr × List (Name × Expr)) :=
+  match type, n with
+  | e, 0 => (e, [])
+  | Expr.forallE name type body _, x + 1 =>
+    let body := body.instantiate1 $ mkFVar ⟨name⟩
+    let next := dropArgs body x
+    { next with snd := (name, type) :: next.snd}
+  | e, x + 1 => panic! s!"No forallE left"
+
+def getFieldTypes (struct : Name) (ctor : ConstructorVal) (parents : Nat) : MetaM (Array NameInfo) := do
+  let type := ctor.type
+  let (fieldFunction, params) := dropArgs type (ctor.numParams + parents)
+  let (_, fields) := dropArgs fieldFunction (ctor.numFields - parents)
+  let mut fieldInfos := #[]
+  for (name, type) in fields do
+    fieldInfos := fieldInfos.push $ ←NameInfo.ofTypedName (struct.append name) type
+  pure $ fieldInfos
+
+def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
+  let info ← Info.ofConstantVal v.toConstantVal
+  let env ← getEnv
+  let parents := getParentStructures env v.name
+  let ctor := getStructureCtor env v.name
+  match getStructureInfo? env v.name with
+  | some i =>
+    if i.fieldNames.size - parents.size > 0 then
+      pure $ StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents (←NameInfo.ofTypedName ctor.name ctor.type)
+    else
+      pure $ StructureInfo.mk info #[] parents (←NameInfo.ofTypedName ctor.name ctor.type)
+  | none => panic! s!"{v.name} is not a structure"
+
+end DocGen4.Process

DocGen4/Process/TheoremInfo.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2022 Henrik Böving. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+import Lean
+
+import DocGen4.Process.Base
+import DocGen4.Process.NameInfo
+
+namespace DocGen4.Process
+
+open Lean Meta
+
+def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do
+  let info ← Info.ofConstantVal v.toConstantVal
+  pure $ TheoremInfo.mk info
+
+end DocGen4.Process