From 2ffff99f90ec0a10b289b0faefe463c6661f88e9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 22 Jul 2022 16:15:37 +0200 Subject: [PATCH] feat: instances from JSON --- DocGen4/Output.lean | 1 + DocGen4/Output/Base.lean | 1 + DocGen4/Output/Class.lean | 2 +- DocGen4/Output/Template.lean | 2 ++ DocGen4/Process/ClassInfo.lean | 6 ------ static/declaration-data.js | 21 +++++++++++++++++++++ static/instances.js | 20 ++++++++++++++++++++ 7 files changed, 46 insertions(+), 7 deletions(-) create mode 100644 static/instances.js diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 5b52815..0b93e63 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -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) diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 119cca7..eedc683 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -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" diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean index 86d1f52..3ce2225 100644 --- a/DocGen4/Output/Class.lean +++ b/DocGen4/Output/Class.lean @@ -15,7 +15,7 @@ def classInstancesToHtml (className : Name) : HtmlM Html := do pure
Instances - +
def classToHtml (i : Process.ClassInfo) : HtmlM (Array Html) := do diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean index 23b5b9e..e569983 100644 --- a/DocGen4/Output/Template.lean +++ b/DocGen4/Output/Template.lean @@ -29,6 +29,8 @@ def baseHtmlGenerator (title : String) (site : Array Html) : BaseHtmlM Html := d + + diff --git a/DocGen4/Process/ClassInfo.lean b/DocGen4/Process/ClassInfo.lean index 8e469be..0c29db7 100644 --- a/DocGen4/Process/ClassInfo.lean +++ b/DocGen4/Process/ClassInfo.lean @@ -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 diff --git a/static/declaration-data.js b/static/declaration-data.js index 7eb691d..1b3167e 100644 --- a/static/declaration-data.js +++ b/static/declaration-data.js @@ -78,6 +78,27 @@ export class DeclarationDataCenter { return getMatches(this.declarationData.declarations, pattern); } } + + /** + * Search for all instances of a certain typeclass + * @returns {Array} + */ + 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) { diff --git a/static/instances.js b/static/instances.js new file mode 100644 index 0000000..983311c --- /dev/null +++ b/static/instances.js @@ -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 += `
  • ${instance}
    • ` + } + instanceList.innerHTML = innerHTML; + } +}