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;
+ }
+}