Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

perf: use a better data structure for the index #269

Merged
merged 1 commit into from
Jan 13, 2025
Merged

perf: use a better data structure for the index #269

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 12 additions & 10 deletions src/verso-manual/VersoManual/Index.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,18 +73,16 @@ end Index


structure Index where
entries : HashSet (Index.Entry × InternalId) := {}
see : HashSet Index.See := {}
entries : Array (Index.Entry × InternalId) := #[]
see : Array Index.See := {}

instance : ToJson Index where
toJson | ⟨entries, see⟩ => ToJson.toJson (entries.toArray.qsort cmpEntry, see.toArray.qsort (· < ·))
where
cmpEntry | (e1, id1), (e2, id2) => e1 < e2 || (e1 == e2 && id1 < id2)
toJson | ⟨entries, see⟩ => ToJson.toJson (entries, see)

instance : FromJson Index where
fromJson? v := do
let ((entries : Array _), (sees : Array _)) ← FromJson.fromJson? v
pure ⟨HashSet.insertMany {} entries, HashSet.insertMany {} sees⟩
pure ⟨entries, sees⟩

def Inline.index : Inline where
name := `Verso.Genre.Manual.index
Expand All @@ -101,8 +99,12 @@ def Index.addEntry [Monad m] [MonadState TraverseState m] [MonadLiftT IO m] [Mon
let ist : Option (Except String Index) := (← get).get? indexState
match ist with
| some (.error err) => logError err
| some (.ok v) => modify (·.set indexState {v with entries := v.entries.insert (entry, id)})
| none => modify (·.set indexState {entries := (HashSet.empty.insert (entry, id)) : Index})
| some (.ok v) =>
modify fun i =>
i.set indexState {v with entries := v.entries.binInsert cmpEntry (entry, id)}
| none => modify (·.set indexState {entries := #[(entry, id)] : Index})
where
cmpEntry | (e1, id1), (e2, id2) => e1 < e2 || (e1 == e2 && id1 < id2)

@[inline_extension index]
def index.descr : InlineDescr where
Expand Down Expand Up @@ -150,8 +152,8 @@ def see.descr : InlineDescr where
let ist : Option (Except String Index) := (← get).get? indexState
match ist with
| some (.error err) => logError err; return none
| some (.ok v) => modify (·.set indexState {v with see := v.see.insert see})
| none => modify (·.set indexState {entries := {}, see := (HashSet.empty.insert see) : Index})
| some (.ok v) => modify (·.set indexState {v with see := v.see.binInsert (· < ·) see})
| none => modify (·.set indexState {entries := {}, see := #[see] : Index})
pure none
toTeX :=
some <| fun _ _ _ _ => do
Expand Down
Loading