diff --git a/src/Sand/SandDaemon.lean b/src/Sand/SandDaemon.lean index 3613ff3..9f3bfa2 100644 --- a/src/Sand/SandDaemon.lean +++ b/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 diff --git a/src/Sand/Timers.lean b/src/Sand/Timers.lean index 672116a..49b75c0 100644 --- a/src/Sand/Timers.lean +++ b/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