r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

feat: instances from JSON

main
Henrik Böving 2022-07-22 16:15:37 +02:00
parent bb9b55ef2c
commit 2ffff99f90
7 changed files with 46 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
DocGen4/Output.lean
View File

@ -45,6 +45,7 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
("search.js", searchJs),
("mathjax-config.js", mathjaxConfigJs),
("instances.js", instancesJs),
("importedBy.js", importedByJs),
("index.html", indexHtml),
("404.html", notFoundHtml),
("navbar.html", navbarHtml)

1
DocGen4/Output/Base.lean
View File

@ -133,6 +133,7 @@ are used in documentation generation, notably JS and CSS ones.
def howAboutJs : String := include_str "../../static/how-about.js"
def searchJs : String := include_str "../../static/search.js"
def instancesJs : String := include_str "../../static/instances.js"
def importedByJs : String := include_str "../../static/importedBy.js"
def findJs : String := include_str "../../static/find/find.js"
def mathjaxConfigJs : String := include_str "../../static/mathjax-config.js"

2
DocGen4/Output/Class.lean
View File

@ -15,7 +15,7 @@ def classInstancesToHtml (className : Name) : HtmlM Html := do
pure
<details «class»="instances">
<summary>Instances</summary>
<ul id={s!"instances-list-{className}"}></ul>
<ul id={s!"instances-list-{className}"} class="instances-list"></ul>
</details>
def classToHtml (i : Process.ClassInfo) : HtmlM (Array Html) := do

2
DocGen4/Output/Template.lean
View File

@ -29,6 +29,8 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d
<script type="module" src={s!"{←getRoot}nav.js"}></script>
<script type="module" src={s!"{←getRoot}search.js"}></script>
<script type="module" src={s!"{←getRoot}how-about.js"}></script>
<script type="module" src={s!"{←getRoot}instances.js"}></script>
<script type="module" src={s!"{←getRoot}importedBy.js"}></script>
</head>
<body>

6
DocGen4/Process/ClassInfo.lean
View File

@ -15,12 +15,6 @@ 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
StructureInfo.ofInductiveVal v

21
static/declaration-data.js
View File

@ -78,6 +78,27 @@ export class DeclarationDataCenter {
return getMatches(this.declarationData.declarations, pattern);
}
}
/**
* Search for all instances of a certain typeclass
* @returns {Array<String>}
*/
instancesForClass(className) {
const instances = this.declarationData.instances[className];
if (!instances) {
return [];
} else {
return instances;
}
}
/**
* Analogous to Lean declNameToLink
* @returns {String}
*/
declNameToLink(declName) {
return this.declarationData.declarations[declName].docLink;
}
}
function isSeparater(char) {

20
static/instances.js Normal file
View File

@ -0,0 +1,20 @@
import { DeclarationDataCenter } from "./declaration-data.js";
annotateInstances();
async function annotateInstances() {
const dataCenter = await DeclarationDataCenter.init();
const instanceLists = [...(document.querySelectorAll(".instances-list"))];
for (const instanceList of instanceLists) {
const className = instanceList.id.slice("instances-list-".length);
const instances = dataCenter.instancesForClass(className);
var innerHTML = "";
for(var instance of instances) {
// TODO: probably fix site root
const instanceLink = dataCenter.declNameToLink(instance);
innerHTML += `<li><a href="${SITE_ROOT}${instanceLink}">${instance}</a></li>`
}
instanceList.innerHTML = innerHTML;
}
}