[←docStringToHtml mdoc.doc]
@@ -156,7 +156,7 @@ as HTML.
def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := do
match member with
| ModuleMember.docInfo d => docInfoToHtml module d
- | ModuleMember.modDoc d => modDocToHtml module d
+ | ModuleMember.modDoc d => modDocToHtml d
def declarationToNavLink (module : Name) : Html :=
@@ -168,13 +168,7 @@ Returns the list of all imports this module does.
-/
def getImports (module : Name) : HtmlM (Array Name) := do
let res ← getResult
- let some idx := res.moduleNames.findIdx? (. == module) | unreachable!
- let adj := res.importAdj.get! idx
- let mut imports := #[]
- for i in [:adj.size] do
- if adj.get! i then
- imports := imports.push (res.moduleNames.get! i)
- pure imports
+ pure $ res.moduleInfo.find! module |>.imports
/--
Sort the list of all modules this one is importing, linkify it
@@ -184,27 +178,6 @@ def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
let imports := (←getImports moduleName) |>.qsort Name.lt
imports.mapM (λ i => do pure
{←moduleToHtmlLink i})
-/--
-Returns a list of all modules this module is imported by.
--/
-def getImportedBy (module : Name) : HtmlM (Array Name) := do
- let res ← getResult
- let some idx := res.moduleNames.findIdx? (. == module) | unreachable!
- let adj := res.importAdj
- let mut impBy := #[]
- for i in [:adj.size] do
- if adj.get! i |>.get! idx then
- impBy := impBy.push (res.moduleNames.get! i)
- pure impBy
-
-/--
-Sort the list of all modules this one is imported by, linkify it
-and return the HTML.
--/
-def importedByHtml (moduleName : Name) : HtmlM (Array Html) := do
- let imports := (←getImportedBy moduleName) |>.qsort Name.lt
- imports.mapM (λ i => do pure
{←moduleToHtmlLink i})
-
/--
Render the internal nav bar (the thing on the right on all module pages).
-/
@@ -222,9 +195,7 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
Imported by
-
- [←importedByHtml moduleName]
-
+
[members.map declarationToNavLink]
diff --git a/DocGen4/Output/ToJson.lean b/DocGen4/Output/ToJson.lean
new file mode 100644
index 0000000..7d0a06c
--- /dev/null
+++ b/DocGen4/Output/ToJson.lean
@@ -0,0 +1,52 @@
+import Lean
+import DocGen4.Process
+import DocGen4.Output.Base
+import Std.Data.RBMap
+
+namespace DocGen4.Output
+
+open Lean Std
+
+structure JsonDeclaration where
+ name : String
+ doc : String
+ docLink : String
+ sourceLink : String
+ deriving FromJson, ToJson
+
+structure JsonInstance where
+ name : String
+ className : String
+ deriving FromJson, ToJson
+
+structure JsonModule where
+ name : String
+ declarations : List JsonDeclaration
+ instances : Array JsonInstance
+ imports : Array String
+ deriving FromJson, ToJson
+
+def DocInfo.toJson (module : Name) (info : Process.DocInfo) : HtmlM JsonDeclaration := do
+ let name := info.getName.toString
+ let doc := info.getDocString.getD ""
+ let docLink ← declNameToLink info.getName
+ let sourceLink ← getSourceUrl module info.getDeclarationRange
+ pure { name, doc, docLink, sourceLink }
+
+def Process.Module.toJson (module : Process.Module) : HtmlM Json := do
+ let mut jsonDecls := []
+ let mut instances := #[]
+ let declInfo := Process.filterMapDocInfo module.members
+ 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.instClass.toString}
+ let jsonMod : JsonModule := {
+ name := module.name.toString,
+ declarations := jsonDecls,
+ instances := instances
+ imports := module.imports.map Name.toString
+ }
+ pure $ ToJson.toJson jsonMod
+
+end DocGen4.Output
diff --git a/DocGen4/Process/Analyze.lean b/DocGen4/Process/Analyze.lean
index 77469af..35c4563 100644
--- a/DocGen4/Process/Analyze.lean
+++ b/DocGen4/Process/Analyze.lean
@@ -36,6 +36,7 @@ structure Module where
All members of the module, sorted according to their line numbers.
-/
members : Array ModuleMember
+ imports : Array Name
deriving Inhabited
/--
@@ -54,11 +55,6 @@ structure AnalyzerResult where
A map from module names to information about these modules.
-/
moduleInfo : HashMap Name Module
- /--
- An adjacency matrix for the import relation between modules, indexed
- my the values in `name2ModIdx`.
- -/
- importAdj : Array (Array Bool)
deriving Inhabited
namespace ModuleMember
@@ -105,20 +101,11 @@ def getAllModuleDocs (relevantModules : Array Name) : MetaM (HashMap Name Module
let mut res := mkHashMap relevantModules.size
for module in relevantModules do
let modDocs := getModuleDoc? env module |>.getD #[] |>.map .modDoc
- res := res.insert module (Module.mk module modDocs)
- pure res
-
--- TODO: This is definitely not the most efficient way to store this data
-def buildImportAdjMatrix (allModules : Array Name) : MetaM (Array (Array Bool)) := do
- let env ← getEnv
- let mut adj := Array.mkArray allModules.size (Array.mkArray allModules.size false)
- for moduleName in allModules do
- let some modIdx := env.getModuleIdx? moduleName | unreachable!
+ let some modIdx := env.getModuleIdx? module | unreachable!
let moduleData := env.header.moduleData.get! modIdx
- for imp in moduleData.imports do
- let some importIdx := env.getModuleIdx? imp.module | unreachable!
- adj := adj.set! modIdx (adj.get! modIdx |>.set! importIdx true)
- pure adj
+ let imports := moduleData.imports.map Import.module
+ res := res.insert module $ Module.mk module modDocs imports
+ pure res
/--
Run the doc-gen analysis on all modules that are loaded into the `Environment`
@@ -154,8 +141,6 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
catch e =>
IO.println s!"WARNING: Failed to obtain information for: {name}: {←e.toMessageData.toString}"
- let adj ← buildImportAdjMatrix allModules
-
-- TODO: This could probably be faster if we did sorted insert above instead
for (moduleName, module) in res.toArray do
res := res.insert moduleName {module with members := module.members.qsort ModuleMember.order}
@@ -165,7 +150,6 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do
name2ModIdx := env.const2ModIdx,
moduleNames := allModules,
moduleInfo := res,
- importAdj := adj
}
pure (analysis, hierarchy)
diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean
index ee02fac..6a6b550 100644
--- a/DocGen4/Process/Base.lean
+++ b/DocGen4/Process/Base.lean
@@ -103,7 +103,9 @@ structure DefinitionInfo extends Info where
/--
Information about an `instance` declaration.
-/
-abbrev InstanceInfo := DefinitionInfo
+structure InstanceInfo extends DefinitionInfo where
+ instClass : Name
+ deriving Inhabited
/--
Information about an `inductive` declaration
@@ -137,16 +139,12 @@ structure StructureInfo extends Info where
/--
Information about a `class` declaration.
-/
-structure ClassInfo extends StructureInfo where
- instances : Array Name
- deriving Inhabited
+abbrev ClassInfo := StructureInfo
/--
Information about a `class inductive` declaration.
-/
-structure ClassInductiveInfo extends InductiveInfo where
- instances : Array Name
- deriving Inhabited
+abbrev ClassInductiveInfo := InductiveInfo
/--
A general type for informations about declarations.
diff --git a/DocGen4/Process/ClassInfo.lean b/DocGen4/Process/ClassInfo.lean
index 0d6df44..8e469be 100644
--- a/DocGen4/Process/ClassInfo.lean
+++ b/DocGen4/Process/ClassInfo.lean
@@ -22,11 +22,9 @@ def getInstances (className : Name) : MetaM (Array Name) := do
pure $ insts.map Expr.constName!
def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
- let sinfo ← StructureInfo.ofInductiveVal v
- pure $ ClassInfo.mk sinfo (←getInstances v.name)
+ StructureInfo.ofInductiveVal v
def ClassInductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInductiveInfo := do
- let info ← InductiveInfo.ofInductiveVal v
- pure $ ClassInductiveInfo.mk info (←getInstances v.name)
+ InductiveInfo.ofInductiveVal v
end DocGen4.Process
diff --git a/DocGen4/Process/InstanceInfo.lean b/DocGen4/Process/InstanceInfo.lean
index 23c603b..c4c4a07 100644
--- a/DocGen4/Process/InstanceInfo.lean
+++ b/DocGen4/Process/InstanceInfo.lean
@@ -17,8 +17,8 @@ def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
let info ← DefinitionInfo.ofDefinitionVal v
let some className := getClassName (←getEnv) v.type | unreachable!
if let some instAttr ← getDefaultInstance v.name className then
- pure { info with attrs := info.attrs.push instAttr }
+ pure $ InstanceInfo.mk { info with attrs := info.attrs.push instAttr } className
else
- pure info
+ pure $ InstanceInfo.mk info className
end DocGen4.Process
diff --git a/static/declaration-data.js b/static/declaration-data.js
index 6a74bee..7eb691d 100644
--- a/static/declaration-data.js
+++ b/static/declaration-data.js
@@ -8,16 +8,6 @@ const CACHE_DB_NAME = "declaration-data";
const CACHE_DB_VERSION = 1;
const CACHE_DB_KEY = "DECLARATIONS_KEY";
-async function fetchModuleData(module) {
- const moduleDataUrl = new URL(
- `${SITE_ROOT}/declarations/declaration-data-${module}.bmp`,
- window.location
- );
- const moduleData = await fetch(moduleDataUrl);
- const moduleDataJson = await moduleData.json();
- return moduleDataJson;
-}
-
/**
* The DeclarationDataCenter is used for declaration searching.
*
@@ -65,25 +55,7 @@ export class DeclarationDataCenter {
} else {
// undefined. then fetch the data from the server.
const dataListRes = await fetch(dataListUrl);
- const dataListJson = await dataListRes.json();
-
- // TODO: this is probably kind of inefficient
- const dataJsonUnflattened = await Promise.all(dataListJson.map(fetchModuleData));
-
- const dataJson = dataJsonUnflattened.flat();
- // the data is a map of name (original case) to declaration data.
- const data = new Map(
- dataJson.map(({ name, doc, docLink, sourceLink }) => [
- name,
- {
- name,
- lowerName: name.toLowerCase(),
- lowerDoc: doc.toLowerCase(),
- docLink,
- sourceLink,
- },
- ])
- );
+ const data = await dataListRes.json();
await cacheDeclarationData(data);
DeclarationDataCenter.singleton = new DeclarationDataCenter(data);
}
@@ -100,10 +72,10 @@ export class DeclarationDataCenter {
return [];
}
if (strict) {
- let decl = this.declarationData.get(pattern);
+ let decl = this.declarationData.declarations[pattern];
return decl ? [decl] : [];
} else {
- return getMatches(this.declarationData, pattern);
+ return getMatches(this.declarationData.declarations, pattern);
}
}
}
@@ -141,13 +113,14 @@ function getMatches(declarations, pattern, maxResults = 30) {
const lowerPats = pattern.toLowerCase().split(/\s/g);
const patNoSpaces = pattern.replace(/\s/g, "");
const results = [];
- for (const {
+ for (const [_, {
name,
- lowerName,
- lowerDoc,
+ doc,
docLink,
sourceLink,
- } of declarations.values()) {
+ }] of Object.entries(declarations)) {
+ const lowerName = name.toLowerCase();
+ const lowerDoc = doc.toLowerCase();
let err = matchCaseSensitive(name, lowerName, patNoSpaces);
// match all words as substrings of docstring
if (