bookshelf-doc/DocGen4/Process/Hierarchy.lean

125 lines
3.9 KiB
Plaintext
Raw Normal View History

2021-12-12 12:28:52 +00:00
/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
2021-12-12 12:20:44 +00:00
import Lean
import Lean.Data.HashMap
2021-12-12 12:20:44 +00:00
def Lean.HashSet.fromArray [BEq α] [Hashable α] (xs : Array α) : Lean.HashSet α :=
xs.foldr (flip .insert) .empty
2021-12-12 12:20:44 +00:00
namespace DocGen4
open Lean Name
2021-12-12 12:20:44 +00:00
def getNLevels (name : Name) (levels: Nat) : Name :=
2022-10-20 17:51:26 +00:00
let components := name.componentsRev
2022-01-15 14:35:52 +00:00
(components.drop (components.length - levels)).reverse.foldl (· ++ ·) Name.anonymous
2021-12-12 12:20:44 +00:00
inductive Hierarchy where
| node (name : Name) (isFile : Bool) (children : RBNode Name (fun _ => Hierarchy)) : Hierarchy
2021-12-12 12:20:44 +00:00
instance : Inhabited Hierarchy := ⟨Hierarchy.node Name.anonymous false RBNode.leaf⟩
2021-12-12 12:20:44 +00:00
abbrev HierarchyMap := RBNode Name (fun _ => Hierarchy)
2021-12-12 12:20:44 +00:00
-- Everything in this namespace is adapted from stdlib's RBNode
namespace HierarchyMap
def toList : HierarchyMap → List (Name × Hierarchy)
| t => t.revFold (fun ps k v => (k, v)::ps) []
def toArray : HierarchyMap → Array (Name × Hierarchy)
| t => t.fold (fun ps k v => ps ++ #[(k, v)] ) #[]
2021-12-12 12:20:44 +00:00
def hForIn [Monad m] (t : HierarchyMap) (init : σ) (f : (Name × Hierarchy) → σ → m (ForInStep σ)) : m σ :=
t.forIn init (fun a b acc => f (a, b) acc)
instance : ForIn m HierarchyMap (Name × Hierarchy) where
forIn := HierarchyMap.hForIn
end HierarchyMap
namespace Hierarchy
def empty (n : Name) (isFile : Bool) : Hierarchy :=
node n isFile RBNode.leaf
2021-12-12 12:20:44 +00:00
def getName : Hierarchy → Name
| node n _ _ => n
2021-12-12 12:20:44 +00:00
def getChildren : Hierarchy → HierarchyMap
| node _ _ c => c
def isFile : Hierarchy → Bool
| node _ f _ => f
2021-12-12 12:20:44 +00:00
2022-07-23 11:01:25 +00:00
partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run do
2021-12-12 12:20:44 +00:00
let hn := h.getName
let mut cs := h.getChildren
if getNumParts hn + 1 == getNumParts n then
2021-12-12 12:20:44 +00:00
match cs.find Name.cmp n with
| none =>
2022-07-23 11:01:25 +00:00
node hn h.isFile (cs.insert Name.cmp n <| empty n true)
| some (node _ true _) => h
| some (node _ false ccs) =>
cs := cs.erase Name.cmp n
2022-07-23 11:01:25 +00:00
node hn h.isFile (cs.insert Name.cmp n <| node n true ccs)
2021-12-12 12:20:44 +00:00
else
let leveledName := getNLevels n (getNumParts hn + 1)
2021-12-12 12:20:44 +00:00
match cs.find Name.cmp leveledName with
| some nextLevel =>
cs := cs.erase Name.cmp leveledName
-- BUG?
2022-07-23 11:01:25 +00:00
node hn h.isFile <| cs.insert Name.cmp leveledName (nextLevel.insert! n)
2021-12-12 12:20:44 +00:00
| none =>
let child := (insert! (empty leveledName false) n)
2022-07-23 11:01:25 +00:00
node hn h.isFile <| cs.insert Name.cmp leveledName child
2021-12-12 12:20:44 +00:00
partial def fromArray (names : Array Name) : Hierarchy :=
names.foldl insert! (empty anonymous false)
2021-12-12 12:20:44 +00:00
def baseDirBlackList : HashSet String :=
HashSet.fromArray #[
"404.html",
2023-06-08 05:52:51 +00:00
"color-scheme.js",
"declaration-data.js",
"declarations",
"find",
"how-about.js",
"index.html",
"search.html",
2022-11-20 12:10:05 +00:00
"foundational_types.html",
"mathjax-config.js",
"navbar.html",
"nav.js",
"search.js",
"src",
"style.css"
]
partial def fromDirectoryAux (dir : System.FilePath) (previous : Name) : IO (Array Name) := 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
2022-07-23 11:01:25 +00:00
children := children.push <| .str previous (entry.fileName.dropRight ".html".length)
return children
def fromDirectory (dir : System.FilePath) : IO Hierarchy := do
let mut children := #[]
for entry in ← System.FilePath.readDir dir do
if baseDirBlackList.contains entry.fileName then
continue
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
2021-12-12 12:20:44 +00:00
end Hierarchy
end DocGen4