diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 07b1229..5016b3b 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -127,6 +127,7 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
let mut allInstances : HashMap String (Array String) := .empty
let mut importedBy : HashMap String (Array String) := .empty
let mut allModules : List (String × Json) := []
+ let mut instancesFor : HashMap String (Array String) := .empty
for entry in ←System.FilePath.readDir declarationsBasePath do
if entry.fileName.startsWith "declaration-data-" && entry.fileName.endsWith ".bmp" then
let fileContent ← FS.readFile entry.path
@@ -138,6 +139,10 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
let mut insts := allInstances.findD inst.className #[]
insts := insts.push inst.name
allInstances := allInstances.insert inst.className insts
+ for typeName in inst.typeNames do
+ let mut instsFor := instancesFor.findD typeName #[]
+ instsFor := instsFor.push inst.name
+ instancesFor := instancesFor.insert typeName instsFor
for imp in module.imports do
let mut impBy := importedBy.findD imp #[]
impBy := impBy.push module.name
@@ -145,11 +150,14 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
let postProcessInstances := allInstances.toList.map (λ(k, v) => (k, toJson v))
let postProcessImportedBy := importedBy.toList.map (λ(k, v) => (k, toJson v))
+ let postProcessInstancesFor := instancesFor.toList.map (λ(k, v) => (k, toJson v))
+
let finalJson := Json.mkObj [
("declarations", Json.mkObj allDecls),
("instances", Json.mkObj postProcessInstances),
("importedBy", Json.mkObj postProcessImportedBy),
- ("modules", Json.mkObj allModules)
+ ("modules", Json.mkObj allModules),
+ ("instancesFor", Json.mkObj postProcessInstancesFor)
]
-- The root JSON for find
FS.writeFile (declarationsBasePath / "declaration-data.bmp") finalJson.compress
diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean
index 3ce2225..521afc3 100644
--- a/DocGen4/Output/Class.lean
+++ b/DocGen4/Output/Class.lean
@@ -8,9 +8,6 @@ namespace Output
open scoped DocGen4.Jsx
open Lean
---def classInstanceToHtml (name : Name) : HtmlM Html := do
--- pure
{←declNameToHtmlLink name}
-
def classInstancesToHtml (className : Name) : HtmlM Html := do
pure
diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
index 47dbcaa..fdf5fdd 100644
--- a/DocGen4/Output/Inductive.lean
+++ b/DocGen4/Output/Inductive.lean
@@ -6,6 +6,14 @@ namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
+open Lean
+
+def instancesForToHtml (typeName : Name) : HtmlM Html := do
+ pure
+
+ Instances For
+
+
def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
let shortName := c.name.components'.head!.toString
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 278c929..97414d5 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -106,6 +106,8 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
| DocInfo.definitionInfo i => equationsToHtml i
| DocInfo.instanceInfo i => equationsToHtml i.toDefinitionInfo
| DocInfo.classInductiveInfo i => pure #[←classInstancesToHtml i.name]
+ | DocInfo.inductiveInfo i => pure #[←instancesForToHtml i.name]
+ | DocInfo.structureInfo i => pure #[←instancesForToHtml i.name]
| _ => pure #[]
let attrs := doc.getAttrs
let attrsHtml :=
diff --git a/DocGen4/Output/ToJson.lean b/DocGen4/Output/ToJson.lean
index 67a37c7..25e8b9c 100644
--- a/DocGen4/Output/ToJson.lean
+++ b/DocGen4/Output/ToJson.lean
@@ -17,6 +17,7 @@ structure JsonDeclaration where
structure JsonInstance where
name : String
className : String
+ typeNames : Array String
deriving FromJson, ToJson
structure JsonModule where
@@ -40,11 +41,15 @@ def Process.Module.toJson (module : Process.Module) : HtmlM Json := do
for decl in declInfo do
jsonDecls := (←DocInfo.toJson module.name decl) :: jsonDecls
if let .instanceInfo i := decl then
- instances := instances.push { name := i.name.toString, className := i.className.toString}
+ instances := instances.push {
+ name := i.name.toString,
+ className := i.className.toString
+ typeNames := i.typeNames.map Name.toString
+ }
let jsonMod : JsonModule := {
name := module.name.toString,
declarations := jsonDecls,
- instances := instances
+ instances,
imports := module.imports.map Name.toString
}
pure <| ToJson.toJson jsonMod
diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean
index 487f687..d7bcb1b 100644
--- a/DocGen4/Process/Base.lean
+++ b/DocGen4/Process/Base.lean
@@ -105,6 +105,7 @@ Information about an `instance` declaration.
-/
structure InstanceInfo extends DefinitionInfo where
className : Name
+ typeNames : Array Name
deriving Inhabited
/--
diff --git a/DocGen4/Process/InstanceInfo.lean b/DocGen4/Process/InstanceInfo.lean
index ac4e275..dbccd67 100644
--- a/DocGen4/Process/InstanceInfo.lean
+++ b/DocGen4/Process/InstanceInfo.lean
@@ -11,7 +11,17 @@ import DocGen4.Process.DefinitionInfo
namespace DocGen4.Process
-open Lean Meta
+open Lean Meta
+
+def getInstanceTypes (typ : Expr) : MetaM (Array Name) := do
+ let (_, _, tail) ← forallMetaTelescopeReducing typ
+ let args := tail.getAppArgs
+ let (_, bar) ← args.mapM (Expr.forEach · findName) |>.run .empty
+ pure bar
+where
+ findName : Expr → StateRefT (Array Name) MetaM Unit
+ | .const name _ => do set <| (←get).push name
+ | _ => pure ()
def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
let mut info ← DefinitionInfo.ofDefinitionVal v
@@ -19,10 +29,12 @@ def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
if let some instAttr ← getDefaultInstance v.name className then
info := { info with attrs := info.attrs.push instAttr }
+ let typeNames ← getInstanceTypes v.type
pure {
toDefinitionInfo := info,
- className
+ className,
+ typeNames
}
end DocGen4.Process
diff --git a/static/declaration-data.js b/static/declaration-data.js
index a12d4f1..953edf2 100644
--- a/static/declaration-data.js
+++ b/static/declaration-data.js
@@ -92,6 +92,19 @@ export class DeclarationDataCenter {
}
}
+ /**
+ * Search for all instances that involve a certain type
+ * @returns {Array}
+ */
+ instancesForType(typeName) {
+ const instances = this.declarationData.instancesFor[typeName];
+ if (!instances) {
+ return [];
+ } else {
+ return instances;
+ }
+ }
+
/**
* Analogous to Lean declNameToLink
* @returns {String}
diff --git a/static/instances.js b/static/instances.js
index cc7d113..fa73c5c 100644
--- a/static/instances.js
+++ b/static/instances.js
@@ -1,19 +1,36 @@
import { DeclarationDataCenter } from "./declaration-data.js";
annotateInstances();
+annotateInstancesFor()
async function annotateInstances() {
const dataCenter = await DeclarationDataCenter.init();
- const instanceLists = [...(document.querySelectorAll(".instances-list"))];
+ const instanceForLists = [...(document.querySelectorAll(".instances-list"))];
- for (const instanceList of instanceLists) {
- const className = instanceList.id.slice("instances-list-".length);
+ for (const instanceForList of instanceForLists) {
+ const className = instanceForList.id.slice("instances-list-".length);
const instances = dataCenter.instancesForClass(className);
var innerHTML = "";
for(var instance of instances) {
const instanceLink = dataCenter.declNameToLink(instance);
innerHTML += `${instance}`
}
- instanceList.innerHTML = innerHTML;
+ instanceForList.innerHTML = innerHTML;
+ }
+}
+
+async function annotateInstancesFor() {
+ const dataCenter = await DeclarationDataCenter.init();
+ const instanceForLists = [...(document.querySelectorAll(".instances-for-list"))];
+
+ for (const instanceForList of instanceForLists) {
+ const typeName = instanceForList.id.slice("instances-for-list-".length);
+ const instances = dataCenter.instancesForType(typeName);
+ var innerHTML = "";
+ for(var instance of instances) {
+ const instanceLink = dataCenter.declNameToLink(instance);
+ innerHTML += `${instance}`
+ }
+ instanceForList.innerHTML = innerHTML;
}
}