From b019faf7baac87af7c8791db80ae4819360f8f0a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 15 Dec 2021 11:59:36 +0100
Subject: [PATCH] feat: An initial list of declarations and their kinds

---
 DocGen4/Output/Module.lean | 26 +++++++++++++++++++++++---
 DocGen4/Process.lean       | 20 ++++++++++++++++++++
 2 files changed, 43 insertions(+), 3 deletions(-)

diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 44438b2..bb4ea87 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -11,11 +11,31 @@ namespace Output
 
 open scoped DocGen4.Jsx
 
+-- TODO: This is a mix of decl.j2 and decl_header.j2, there is tons of stuff still missing
+def docInfoToHtml (doc : DocInfo) : HtmlM Html := do
+  <div «class»="decl" id={doc.getName.toString}>
+    <div «class»={doc.getKind}>
+      <div «class»="gh_link">
+        -- TODO: Put the proper source link
+        <a href="https://github.com">source</a>
+      </div>
+      -- TODO: Attributes
+      -- TODO: Noncomputable, partial etc.
+      <span «class»="decl_kind">{doc.getKind}</span>
+      -- TODO: HTMLify the name etc.
+      {doc.getName.toString}
+      -- TODO: args
+      -- TODO: The actual type information we are here for
+    </div>
+  </div>
+
 def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do
+  -- TODO: Probably some sort of ordering by line number would be cool?
+  -- maybe they should already be ordered in members.
+  let docInfos ← module.members.mapM docInfoToHtml
+  -- TODO: This is missing imports, imported by, source link, list of decls
   templateExtends (baseHtml module.name.toString) $
-    <main>
-      <h1>This is the page of {module.name.toString}</h1>
-    </main>
+    Html.element "main" #[] docInfos
 
 end Output
 end DocGen4
diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index 950beac..b1bc9fc 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -256,6 +256,26 @@ def prettyPrint (i : DocInfo) : CoreM String := do
     let fieldString ← i.fieldInfo.mapM (NameInfo.prettyPrint ∘ FieldInfo.toNameInfo)
     s!"class {←i.toNameInfo.prettyPrint} extends {i.parents}, fields: {fieldString}, instances : {instanceString}, doc string: {i.doc}"
 
+def getName : DocInfo → Name
+| axiomInfo i => i.name
+| theoremInfo i => i.name
+| opaqueInfo i => i.name
+| definitionInfo i => i.name
+| instanceInfo i => i.name
+| inductiveInfo i => i.name
+| structureInfo i => i.name
+| classInfo i => i.name
+
+def getKind : DocInfo → String
+| axiomInfo _ => "axiom"
+| theoremInfo _ => "theorem"
+| opaqueInfo _ => "constant"
+| definitionInfo _ => "def"
+| instanceInfo _ => "instance" -- TODO: This doesnt exist in CSS yet
+| inductiveInfo _ => "inductive"
+| structureInfo _ => "structure"
+| classInfo _ => "class" -- TODO: This is handled as structure right now
+
 end DocInfo
 
 namespace Module