feat: instances for

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

DocGen4/Output/Class.lean

@@ -8,9 +8,6 @@ namespace Output
 open scoped DocGen4.Jsx
 open Lean
 
---def classInstanceToHtml (name : Name) : HtmlM Html := do
---  pure <li>{←declNameToHtmlLink name}</li>
-
 def classInstancesToHtml (className : Name) : HtmlM Html := do
   pure
     <details «class»="instances">

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
+    <details «class»="instances">
+        <summary>Instances For</summary>
+        <ul id={s!"instances-for-list-{typeName}"} class="instances-for-list"></ul>
+    </details>
 
 def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
   let shortName := c.name.components'.head!.toString

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 :=

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

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
 
 /--

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

static/declaration-data.js

@@ -92,6 +92,19 @@ export class DeclarationDataCenter {
     }
   }
 
+  /**
+   * Search for all instances that involve a certain type
+   * @returns {Array<String>}
+   */
+  instancesForType(typeName) {
+    const instances = this.declarationData.instancesFor[typeName];
+    if (!instances) {
+      return [];
+    } else {
+      return instances;
+    }
+  }
+
   /**
    * Analogous to Lean declNameToLink
    * @returns {String}

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 += `<li><a href="${SITE_ROOT}${instanceLink}">${instance}</a></li>`
     }
-    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 += `<li><a href="${SITE_ROOT}${instanceLink}">${instance}</a></li>`
+    }
+    instanceForList.innerHTML = innerHTML;
   }
 }