bookshelf-doc/DocGen4/Output/Module.lean

217 lines
7.2 KiB
Plaintext
Raw Normal View History

/-
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.Output.Template
import DocGen4.Output.Inductive
import DocGen4.Output.Structure
import DocGen4.Output.Class
import DocGen4.Output.Definition
2022-02-04 21:48:08 +00:00
import DocGen4.Output.Instance
2022-02-06 19:14:36 +00:00
import DocGen4.Output.ClassInductive
2022-02-17 05:47:38 +00:00
import DocGen4.Output.DocString
import DocGen4.Process
2022-02-15 18:19:40 +00:00
import Lean.Data.Xml.Parser
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
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)
| BinderInfo.implicit => ("{", "}", true)
| BinderInfo.strictImplicit => ("⦃", "⦄", true)
| BinderInfo.instImplicit => ("[", "]", true)
let mut nodes := #[Html.text s!"{l}{arg.name.toString} : "]
2023-01-01 18:51:01 +00:00
nodes := nodes.append (← infoFormatToHtml arg.type)
nodes := nodes.push r
let inner := <span class="fn">[nodes]</span>
let html := Html.element "span" false #[("class", "decl_args")] #[inner]
if implicit then
2023-01-01 18:51:01 +00:00
return <span class="impl_arg">{html}</span>
else
2023-01-01 18:51:01 +00:00
return html
/--
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
2022-05-19 09:14:47 +00:00
nodes := nodes.push <span class="decl_extends">extends</span>
let mut parents := #[]
for parent in s.parents do
let link ← declNameToHtmlBreakWithinLink parent
let inner := <span class="fn">{link}</span>
let html:= Html.element "span" false #[("class", "decl_parent")] #[inner]
parents := parents.push html
nodes := nodes.append (parents.toList.intersperse (Html.text ", ")).toArray
2023-01-01 18:51:01 +00:00
return nodes
/--
Render the general header of a declaration containing its declaration type
and name.
-/
def docInfoHeader (doc : DocInfo) : HtmlM Html := do
let mut nodes := #[]
2022-07-23 11:01:25 +00:00
nodes := nodes.push <| Html.element "span" false #[("class", "decl_kind")] #[doc.getKindDescription]
2021-12-17 16:20:44 +00:00
nodes := nodes.push
2022-05-19 09:14:47 +00:00
<span class="decl_name">
{← declNameToHtmlBreakWithinLink doc.getName}
2021-12-17 16:20:44 +00:00
</span>
for arg in doc.getArgs do
2023-01-01 18:51:01 +00:00
nodes := nodes.push (← argToHtml arg)
match doc with
2023-01-01 18:51:01 +00:00
| DocInfo.structureInfo i => nodes := nodes.append (← structureInfoHeader i)
| DocInfo.classInfo i => nodes := nodes.append (← structureInfoHeader i)
| _ => nodes := nodes
nodes := nodes.push <| Html.element "span" true #[("class", "decl_args")] #[" :"]
2023-01-01 18:51:01 +00:00
nodes := nodes.push <div class="decl_type">[← infoFormatToHtml doc.getType]</div>
return <div class="decl_header"> [nodes] </div>
/--
The main entry point for rendering a single declaration inside a given module.
-/
2022-01-09 15:57:19 +00:00
def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
-- basic info like headers, types, structure fields, etc.
2022-02-18 03:28:44 +00:00
let docInfoHtml ← match doc with
| DocInfo.inductiveInfo i => inductiveToHtml i
| DocInfo.structureInfo i => structureToHtml i
| DocInfo.classInfo i => classToHtml i
2022-02-06 19:14:36 +00:00
| DocInfo.classInductiveInfo i => classInductiveToHtml i
| _ => pure #[]
-- rendered doc stirng
2022-02-18 03:28:44 +00:00
let docStringHtml ← match doc.getDocString with
| some s => docStringToHtml s
| none => pure #[]
-- extra information like equations and instances
let extraInfoHtml ← match doc with
2023-01-01 18:51:01 +00:00
| DocInfo.classInfo i => pure #[← classInstancesToHtml i.name]
| DocInfo.definitionInfo i => equationsToHtml i
| DocInfo.instanceInfo i => equationsToHtml i.toDefinitionInfo
2023-01-01 18:51:01 +00:00
| DocInfo.classInductiveInfo i => pure #[← classInstancesToHtml i.name]
| DocInfo.inductiveInfo i => pure #[← instancesForToHtml i.name]
| DocInfo.structureInfo i => pure #[← instancesForToHtml i.name]
| _ => pure #[]
2022-02-13 02:32:53 +00:00
let attrs := doc.getAttrs
let attrsHtml :=
if attrs.size > 0 then
let attrStr := "@[" ++ String.intercalate ", " doc.getAttrs.toList ++ "]"
#[Html.element "div" false #[("class", "attributes")] #[attrStr]]
else
#[]
let leanInkHtml :=
2023-01-01 18:51:01 +00:00
if ← leanInkEnabled? then
#[
<div class="ink_link">
2023-01-01 18:51:01 +00:00
<a href={← declNameToInkLink doc.getName}>ink</a>
</div>
]
else
#[]
2022-02-13 02:32:53 +00:00
2022-02-12 14:09:13 +00:00
pure
2022-05-19 09:14:47 +00:00
<div class="decl" id={doc.getName.toString}>
<div class={doc.getKind}>
<div class="gh_link">
2023-01-01 18:51:01 +00:00
<a href={← getSourceUrl module doc.getDeclarationRange}>source</a>
2022-02-12 14:09:13 +00:00
</div>
[leanInkHtml]
2022-02-13 02:32:53 +00:00
[attrsHtml]
2023-01-01 18:51:01 +00:00
{← docInfoHeader doc}
2022-02-18 03:28:44 +00:00
[docInfoHtml]
[docStringHtml]
[extraInfoHtml]
</div>
</div>
/--
Rendering a module doc string, that is the ones with an ! after the opener
as HTML.
-/
def modDocToHtml (mdoc : ModuleDoc) : HtmlM Html := do
2022-10-20 17:51:26 +00:00
pure
2022-05-19 09:14:47 +00:00
<div class="mod_doc">
2023-01-01 18:51:01 +00:00
[← docStringToHtml mdoc.doc]
2022-02-15 17:06:46 +00:00
</div>
/--
Render a module member, that is either a module doc string or a declaration
as HTML.
-/
2022-02-18 03:28:44 +00:00
def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := do
2022-02-15 17:06:46 +00:00
match member with
| ModuleMember.docInfo d => docInfoToHtml module d
| ModuleMember.modDoc d => modDocToHtml d
2022-02-15 17:06:46 +00:00
2022-01-16 13:22:53 +00:00
def declarationToNavLink (module : Name) : Html :=
2022-05-19 09:14:47 +00:00
<div class="nav_link">
<a class="break_within" href={s!"#{module.toString}"}>
[breakWithin module.toString]
</a>
</div>
/--
Returns the list of all imports this module does.
-/
2022-01-16 13:22:53 +00:00
def getImports (module : Name) : HtmlM (Array Name) := do
let res ← getResult
2023-01-01 18:51:01 +00:00
return res.moduleInfo.find! module |>.imports
2022-01-16 13:22:53 +00:00
/--
Sort the list of all modules this one is importing, linkify it
and return the HTML.
-/
def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
2023-01-01 18:51:01 +00:00
let imports := (← getImports moduleName).qsort Name.lt
imports.mapM (fun i => do return <li>{← moduleToHtmlLink i}</li>)
/--
Render the internal nav bar (the thing on the right on all module pages).
-/
2022-01-09 15:57:19 +00:00
def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
2022-02-12 14:09:13 +00:00
pure
2022-05-19 09:14:47 +00:00
<nav class="internal_nav">
<h3><a class="break_within" href="#top">[breakWithin moduleName.toString]</a></h3>
2023-01-01 18:51:01 +00:00
<p class="gh_nav_link"><a href={← getSourceUrl moduleName none}>source</a></p>
2022-05-19 09:14:47 +00:00
<div class="imports">
2022-02-12 14:09:13 +00:00
<details>
<summary>Imports</summary>
<ul>
2023-01-01 18:51:01 +00:00
[← importsHtml moduleName]
2022-02-12 14:09:13 +00:00
</ul>
</details>
<details>
<summary>Imported by</summary>
2022-07-22 14:56:51 +00:00
<ul id={s!"imported-by-{moduleName}"} class="imported-by-list"> </ul>
2022-02-12 14:09:13 +00:00
</details>
</div>
[members.map declarationToNavLink]
</nav>
/--
The main entry point to rendering the HTML for an entire module.
-/
def moduleToHtml (module : Process.Module) : HtmlM Html := withTheReader SiteBaseContext (setCurrentName module.name) do
2023-02-16 18:51:35 +00:00
let relevantMembers := module.members.filter Process.ModuleMember.shouldRender
let memberDocs ← relevantMembers.mapM (moduleMemberToHtml module.name)
let memberNames := filterDocInfo relevantMembers |>.map DocInfo.getName
2022-07-23 11:01:25 +00:00
templateLiftExtends (baseHtmlGenerator module.name.toString) <| pure #[
2023-01-01 18:51:01 +00:00
← internalNav memberNames module.name,
2022-02-18 04:52:01 +00:00
Html.element "main" false #[] memberDocs
]
end Output
end DocGen4