From cda229ac1229df1ed959003cfcb3dc1a18da26ff Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Thu, 14 Dec 2023 16:55:32 -0700 Subject: [PATCH] Add nameext to distinguish PDF and HTML files. --- DocGen4/Output/Base.lean | 8 +++++ DocGen4/Output/Navbar.lean | 27 +++++++++------ DocGen4/Process.lean | 1 + DocGen4/Process/Hierarchy.lean | 62 ++++++++++++++++++++-------------- DocGen4/Process/NameExt.lean | 48 ++++++++++++++++++++++++++ 5 files changed, 111 insertions(+), 35 deletions(-) create mode 100644 DocGen4/Process/NameExt.lean diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index e6c4074..6d7593f 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -97,6 +97,7 @@ def templateExtends {α β} {m} [Bind m] (base : α → m β) (new : m α) : m def templateLiftExtends {α β} {m n} [Bind m] [MonadLift n m] (base : α → n β) (new : m α) : m β := new >>= (monadLift ∘ base) + /-- Returns the doc-gen4 link to a module name. -/ @@ -104,6 +105,13 @@ def moduleNameToLink (n : Name) : BaseHtmlM String := do let parts := n.components.map Name.toString return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" +/- +Returns the doc-gen4 link to a module `NameExt`. +-/ +def moduleNameExtToLink (n : NameExt) : BaseHtmlM String := do + let parts := n.name.components.map Name.toString + return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ "." ++ n.ext.toString + /-- Returns the HTML doc-gen4 link to a module name. -/ diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 33f06f7..dd7ad7e 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -13,9 +13,14 @@ namespace Output open Lean open scoped DocGen4.Jsx -def moduleListFile (file : Name) : BaseHtmlM Html := do - return
- {file.getString!} +def moduleListFile (file : NameExt) : BaseHtmlM Html := do + let contents := + if file.ext == .pdf then + {s!"🗎 {file.getString!} (pdf)"} + else + {file.getString!} + return
+ {contents}
/-- @@ -23,11 +28,14 @@ Build the HTML tree representing the module hierarchy. -/ partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do let children := Array.mk (h.getChildren.toList.map Prod.snd) - let dirs := children.filter (fun c => c.getChildren.toList.length != 0) - let files := children.filter (fun c => Hierarchy.isFile c && c.getChildren.toList.length = 0) - |>.map Hierarchy.getName - let dirNodes ← dirs.mapM moduleListDir - let fileNodes ← files.mapM moduleListFile + let nodes ← children.mapM (fun c => + if c.getChildren.toList.length != 0 then + moduleListDir c + else if Hierarchy.isFile c && c.getChildren.toList.length = 0 then + moduleListFile (Hierarchy.getNameExt c) + else + pure "" + ) let moduleLink ← moduleNameToLink h.getName let summary := if h.isFile then @@ -38,8 +46,7 @@ partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do pure
{summary} - [dirNodes] - [fileNodes] + [nodes]
/-- diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean index 0c1d9e6..dd6a317 100644 --- a/DocGen4/Process.lean +++ b/DocGen4/Process.lean @@ -14,6 +14,7 @@ import DocGen4.Process.DocInfo import DocGen4.Process.Hierarchy import DocGen4.Process.InductiveInfo import DocGen4.Process.InstanceInfo +import DocGen4.Process.NameExt import DocGen4.Process.NameInfo import DocGen4.Process.OpaqueInfo import DocGen4.Process.StructureInfo diff --git a/DocGen4/Process/Hierarchy.lean b/DocGen4/Process/Hierarchy.lean index 9502078..3d1b703 100644 --- a/DocGen4/Process/Hierarchy.lean +++ b/DocGen4/Process/Hierarchy.lean @@ -6,6 +6,8 @@ Authors: Henrik Böving import Lean import Lean.Data.HashMap +import DocGen4.Process.NameExt + def Lean.HashSet.fromArray [BEq α] [Hashable α] (xs : Array α) : Lean.HashSet α := xs.foldr (flip .insert) .empty @@ -18,35 +20,38 @@ def getNLevels (name : Name) (levels: Nat) : Name := (components.drop (components.length - levels)).reverse.foldl (· ++ ·) Name.anonymous inductive Hierarchy where -| node (name : Name) (isFile : Bool) (children : RBNode Name (fun _ => Hierarchy)) : Hierarchy +| node (name : NameExt) (isFile : Bool) (children : RBNode NameExt (fun _ => Hierarchy)) : Hierarchy -instance : Inhabited Hierarchy := ⟨Hierarchy.node Name.anonymous false RBNode.leaf⟩ +instance : Inhabited Hierarchy := ⟨Hierarchy.node ⟨anonymous, .html⟩ false RBNode.leaf⟩ -abbrev HierarchyMap := RBNode Name (fun _ => Hierarchy) +abbrev HierarchyMap := RBNode NameExt (fun _ => Hierarchy) -- Everything in this namespace is adapted from stdlib's RBNode namespace HierarchyMap -def toList : HierarchyMap → List (Name × Hierarchy) +def toList : HierarchyMap → List (NameExt × Hierarchy) | t => t.revFold (fun ps k v => (k, v)::ps) [] -def toArray : HierarchyMap → Array (Name × Hierarchy) +def toArray : HierarchyMap → Array (NameExt × Hierarchy) | t => t.fold (fun ps k v => ps ++ #[(k, v)] ) #[] -def hForIn [Monad m] (t : HierarchyMap) (init : σ) (f : (Name × Hierarchy) → σ → m (ForInStep σ)) : m σ := +def hForIn [Monad m] (t : HierarchyMap) (init : σ) (f : (NameExt × Hierarchy) → σ → m (ForInStep σ)) : m σ := t.forIn init (fun a b acc => f (a, b) acc) -instance : ForIn m HierarchyMap (Name × Hierarchy) where +instance : ForIn m HierarchyMap (NameExt × Hierarchy) where forIn := HierarchyMap.hForIn end HierarchyMap namespace Hierarchy -def empty (n : Name) (isFile : Bool) : Hierarchy := +def empty (n : NameExt) (isFile : Bool) : Hierarchy := node n isFile RBNode.leaf def getName : Hierarchy → Name +| node n _ _ => n.name + +def getNameExt : Hierarchy → NameExt | node n _ _ => n def getChildren : Hierarchy → HierarchyMap @@ -55,31 +60,34 @@ def getChildren : Hierarchy → HierarchyMap def isFile : Hierarchy → Bool | node _ f _ => f -partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run do - let hn := h.getName +partial def insert! (h : Hierarchy) (n : NameExt) : Hierarchy := Id.run do + let hn := h.getNameExt let mut cs := h.getChildren - if getNumParts hn + 1 == getNumParts n then - match cs.find Name.cmp n with + if getNumParts hn.name + 1 == getNumParts n.name then + match cs.find NameExt.cmp n with | none => - node hn h.isFile (cs.insert Name.cmp n <| empty n true) + node hn h.isFile (cs.insert NameExt.cmp n <| empty n true) | some (node _ true _) => h | some (node _ false ccs) => - cs := cs.erase Name.cmp n - node hn h.isFile (cs.insert Name.cmp n <| node n true ccs) + cs := cs.erase NameExt.cmp n + node hn h.isFile (cs.insert NameExt.cmp n <| node n true ccs) else - let leveledName := getNLevels n (getNumParts hn + 1) - match cs.find Name.cmp leveledName with + let leveledName := ⟨getNLevels n.name (getNumParts hn.name + 1), .html⟩ + match cs.find NameExt.cmp leveledName with | some nextLevel => - cs := cs.erase Name.cmp leveledName + cs := cs.erase NameExt.cmp leveledName -- BUG? - node hn h.isFile <| cs.insert Name.cmp leveledName (nextLevel.insert! n) + node hn h.isFile <| cs.insert NameExt.cmp leveledName (nextLevel.insert! n) | none => let child := (insert! (empty leveledName false) n) - node hn h.isFile <| cs.insert Name.cmp leveledName child + node hn h.isFile <| cs.insert NameExt.cmp leveledName child partial def fromArray (names : Array Name) : Hierarchy := - names.foldl insert! (empty anonymous false) + (names.map (fun n => NameExt.mk n .html)).foldl insert! (empty ⟨anonymous, .html⟩ false) + +partial def fromArrayExt (names : Array NameExt) : Hierarchy := + names.foldl insert! (empty ⟨anonymous, .html⟩ false) def baseDirBlackList : HashSet String := HashSet.fromArray #[ @@ -102,13 +110,15 @@ def baseDirBlackList : HashSet String := "style.css" ] -partial def fromDirectoryAux (dir : System.FilePath) (previous : Name) : IO (Array Name) := do +partial def fromDirectoryAux (dir : System.FilePath) (previous : Name) : IO (Array NameExt) := do let mut children := #[] for entry in ← System.FilePath.readDir dir do if ← entry.path.isDir then children := children ++ (← fromDirectoryAux entry.path (.str previous entry.fileName)) else if entry.path.extension = some "html" then - children := children.push <| .str previous (entry.fileName.dropRight ".html".length) + children := children.push <| ⟨.str previous (entry.fileName.dropRight ".html".length), .html⟩ + else if entry.path.extension = some "pdf" then + children := children.push <| ⟨.str previous (entry.fileName.dropRight ".pdf".length), .pdf⟩ return children def fromDirectory (dir : System.FilePath) : IO Hierarchy := do @@ -119,8 +129,10 @@ def fromDirectory (dir : System.FilePath) : IO Hierarchy := do else if ← entry.path.isDir then children := children ++ (← fromDirectoryAux entry.path (.mkSimple entry.fileName)) else if entry.path.extension = some "html" then - children := children.push <| .mkSimple (entry.fileName.dropRight ".html".length) - return Hierarchy.fromArray children + children := children.push <| ⟨.mkSimple (entry.fileName.dropRight ".html".length), .html⟩ + else if entry.path.extension = some "pdf" then + children := children.push <| ⟨.mkSimple (entry.fileName.dropRight ".pdf".length), .pdf⟩ + return Hierarchy.fromArrayExt children end Hierarchy end DocGen4 diff --git a/DocGen4/Process/NameExt.lean b/DocGen4/Process/NameExt.lean new file mode 100644 index 0000000..d1be339 --- /dev/null +++ b/DocGen4/Process/NameExt.lean @@ -0,0 +1,48 @@ +/- +A generalization of `Lean.Name` that includes a file extension. +-/ +import Lean + +open Lean Name + +inductive Extension where +| html +| pdf +deriving Repr + +namespace Extension + +def cmp : Extension → Extension → Ordering + | html, html => Ordering.eq + | html, _ => Ordering.lt + | pdf, pdf => Ordering.eq + | pdf, _ => Ordering.gt + +instance : BEq Extension where + beq e1 e2 := + match cmp e1 e2 with + | Ordering.eq => true + | _ => false + +def toString : Extension → String + | html => "html" + | pdf => "pdf" + +end Extension + +structure NameExt where + name : Name + ext : Extension + +namespace NameExt + +def cmp (n₁ n₂ : NameExt) : Ordering := + match Name.cmp n₁.name n₂.name with + | Ordering.eq => Extension.cmp n₁.ext n₂.ext + | ord => ord + +def getString! : NameExt → String + | ⟨str _ s, _⟩ => s + | _ => unreachable! + +end NameExt