make Timers abstract

src/Sand/SandDaemon.lean

@@ -155,7 +155,7 @@ def handleClientCmd (cmd : Command) : CmdHandlerT IO (ResponseFor cmd) := do
  | .cancelTimer which => removeTimer which
  | .list => do
  let timers ← state.timers.atomically get
- return .ok <| Sand.timersForClient timers
+ return .ok timers.forClient
  | .pauseTimer which => pauseTimer which
  | .resumeTimer which => resumeTimer which
 

src/Sand/Timers.lean

@@ -33,12 +33,24 @@ def timerForClient (id : TimerId) (timer : Timer) : TimerInfoForClient :=
  | .paused remaining => .paused remaining
  { id, state }
 
-def timersForClient
- (timers : HashMap TimerId Timer)
- : Array TimerInfoForClient := timers.toArray.map (λ (a, b) ↦ timerForClient a b)
 
--- TODO make abstract to allow switching representations more easily
-def Timers := HashMap TimerId Timer
- deriving EmptyCollection
+structure Timers where
+ timers : HashMap TimerId Timer
 
-def Timers.erase : Timers → TimerId → Timers := HashMap.erase
+instance : EmptyCollection Timers where
+ emptyCollection := ⟨∅⟩
+
+namespace Timers
+def erase : Timers → TimerId → Timers
+ | ⟨timers⟩, id => ⟨timers.erase id⟩
+
+def find? : Timers → TimerId → Option Timer
+ | ⟨timers⟩ => timers.find?
+
+def insert : Timers → TimerId → Timer → Timers
+ | ⟨timers⟩, k, v => ⟨timers.insert k v⟩
+
+def forClient : Timers → Array TimerInfoForClient
+ | ⟨timers⟩ => timers.toArray.map (λ (a, b) ↦ timerForClient a b)
+
+end Timers