From d2594669faf269133c57b15b25d5266b15e88296 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 13 Dec 2021 20:47:52 +0100
Subject: [PATCH] feat: Revamp the hierarchy mechanism

Previously the hierarchy mechanism wouldn't show modules in files that
have names, equal to some directory with submodules.
---
 DocGen4/Hierarchy.lean | 38 ++++++++++++++++++++++++--------------
 DocGen4/Output.lean    | 30 +++++++++++++++---------------
 2 files changed, 39 insertions(+), 29 deletions(-)

diff --git a/DocGen4/Hierarchy.lean b/DocGen4/Hierarchy.lean
index 9f8a0d4..205fec0 100644
--- a/DocGen4/Hierarchy.lean
+++ b/DocGen4/Hierarchy.lean
@@ -21,9 +21,9 @@ def getNLevels (name : Name) (levels: Nat) : Name :=
     components := name.components'
 
 inductive Hierarchy where
-| node : Name → RBNode Name (λ _ => Hierarchy) → Hierarchy
+| node (name : Name) (isFile : Bool) (children : RBNode Name (λ _ => Hierarchy)) : Hierarchy
 
-instance : Inhabited Hierarchy := ⟨Hierarchy.node Name.anonymous RBNode.leaf⟩
+instance : Inhabited Hierarchy := ⟨Hierarchy.node Name.anonymous false RBNode.leaf⟩
 
 abbrev HierarchyMap := RBNode Name (λ _ => Hierarchy)
 
@@ -43,35 +43,45 @@ end HierarchyMap
 
 namespace Hierarchy
 
-def empty (n : Name) : Hierarchy := node n RBNode.leaf
+def empty (n : Name) (isFile : Bool) : Hierarchy :=
+  node n isFile RBNode.leaf
 
 def getName : Hierarchy → Name
-| node n _ => n
+| node n _ _ => n
 
 def getChildren : Hierarchy → HierarchyMap
-| node _ c => c
+| node _ _ c => c
+
+def isFile : Hierarchy → Bool
+| node _ f _ => f
 
 partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run $ do
   let hn := h.getName
   let mut cs := h.getChildren
-  if getDepth hn ≥ getDepth n then
-    panic! "Invalid insert"
-  else if getDepth hn + 1 == getDepth n then
+
+  assert! getDepth hn ≤ getDepth n
+
+  if getDepth hn + 1 == getDepth n then
     match cs.find Name.cmp n with
     | none =>
-      node hn (cs.insert Name.cmp n $ empty n)
-    | some _ => h
+      node hn h.isFile (cs.insert Name.cmp n $ empty n true)
+    | some (node _ true _) => h
+    | some hierarchy@(node _ false ccs) =>
+        cs := cs.erase Name.cmp n
+        node hn h.isFile (cs.insert Name.cmp n $ node n true ccs)
   else
     let leveledName := getNLevels n (getDepth hn + 1)
     match cs.find Name.cmp leveledName with
     | some nextLevel =>
       cs := cs.erase Name.cmp leveledName
-      node hn $ cs.insert Name.cmp leveledName (nextLevel.insert! n)
+      -- BUG?
+      node hn h.isFile $ cs.insert Name.cmp leveledName (nextLevel.insert! n)
     | none =>
-      let child := (insert! (empty leveledName) n)
-      node hn $ cs.insert Name.cmp leveledName child
+      let child := (insert! (empty leveledName false) n)
+      node hn h.isFile $ cs.insert Name.cmp leveledName child
 
-partial def fromArray (names : Array Name) : Hierarchy := names.foldl insert! (empty anonymous)
+partial def fromArray (names : Array Name) : Hierarchy :=
+  names.foldl insert! (empty anonymous false)
 
 end Hierarchy
 end DocGen4
diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 4d92118..3be747c 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -37,27 +37,27 @@ def nameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
   where
     parts := n.components.dropLast.map Name.toString
 
-partial def moduleListAux (h : Hierarchy) : HtmlM Html := do
-  if h.getChildren.toList.length == 0 then
-    <div «class»="nav_link visible">
-      <a href={s!"{←getRoot}{nameToUrl h.getName}"}>{h.getName.toString}</a>
-    </div>
-  else
-    let children := Array.mk (h.getChildren.toList.map Prod.snd)
-    -- TODO: Is having no children really the correct criterium for a clickable module?
-    let (dirs, files) := children.partition (λ c => c.getChildren.toList.length != 0)
-    let nodes := (←(dirs.mapM moduleListAux)) ++ (←(files.mapM moduleListAux))
-    return <details «class»="nav_sect" «data-path»={←nameToUrl h.getName}>
-      <summary>{h.getName.toString}</summary>
-      [nodes]
-    </details>  
+def moduleListFile (file : Name) : HtmlM Html := do
+  <div «class»="nav_link">
+    <a href={s!"{←getRoot}{nameToUrl file}"}>{file.toString}</a>
+  </div>
+
+partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
+  let children := Array.mk (h.getChildren.toList.map Prod.snd)
+  let dirs := children.filter (λ c => c.getChildren.toList.length != 0)
+  let files := children.filter Hierarchy.isFile |>.map Hierarchy.getName
+  return <details «class»="nav_sect" «data-path»={nameToUrl h.getName}>
+    <summary>{h.getName.toString}</summary>
+    [(←(dirs.mapM moduleListDir))]
+    [(←(files.mapM moduleListFile))]
+  </details>
 
 def moduleList : HtmlM (Array Html) := do
   let hierarchy := (←getResult).hierarchy
   let mut list := Array.empty
   for (n, cs) in hierarchy.getChildren do
     list := list.push <h4>{n.toString}</h4>
-    list := list.push $ ←moduleListAux cs
+    list := list.push $ ←moduleListDir cs
   list
 
 def navbar : HtmlM Html := do