From 619377d3d2193ebcd5f6dd8465e0d752d91bdfff Mon Sep 17 00:00:00 2001
From: James Sully <sullyj3@gmail.com>
Date: Sun, 28 Jul 2024 03:28:14 +1000
Subject: [PATCH] store countdown Task with its associated Timer in
 state.timers (WIP)

This will enable cancelling that task when the timer is cancelled or paused
Also reorder all the functions to allow this
---
 src/Sand/SandDaemon.lean | 74 +++++++++++++++++++++-------------------
 1 file changed, 38 insertions(+), 36 deletions(-)

diff --git a/src/Sand/SandDaemon.lean b/src/Sand/SandDaemon.lean
index 6bed708..9402851 100644
--- a/src/Sand/SandDaemon.lean
+++ b/src/Sand/SandDaemon.lean
@@ -11,23 +11,6 @@ open Sand (Timer TimerId Command CmdResponse Duration)
 def Batteries.HashMap.values [BEq α] [Hashable α] (hashMap : HashMap α β) : Array β :=
   hashMap.toArray |>.map Prod.snd
 
-structure SanddState where
-  nextTimerId : IO.Mutex Nat
-  timers : IO.Mutex (HashMap Nat Timer)
-
-def SanddState.initial : IO SanddState := do
-  return {
-    nextTimerId := (← IO.Mutex.new 1),
-    timers := (← IO.Mutex.new ∅)
-  }
-
-def SanddState.addTimer (state : SanddState) (due : Nat) : BaseIO TimerId := do
-  let id : TimerId ← state.nextTimerId.atomically (getModify Nat.succ)
-  let timer : Timer := ⟨id, due⟩
-  state.timers.atomically <| modify (·.insert id timer)
-  return id
-
-
 inductive TimerOpError
   | notFound
 
@@ -39,19 +22,6 @@ def SanddState.pauseTimer (state : SanddState) (timerId : TimerId)
 def SanddState.resumeTimer (state : SanddState) (timerId : TimerId)
   : BaseIO (TimerOpResult Unit) := sorry
 
-def SanddState.removeTimer (state : SanddState) (id : TimerId) : BaseIO (TimerOpResult Unit) := do
-  let timers ← state.timers.atomically get
-  -- match timers.findIdx? (λ timer ↦ timer.id == id) with
-  match timers.find? id with
-  | some _ => do
-    state.timers.atomically <| set <| timers.erase id
-    pure <| .ok ()
-  | none => do
-    pure <| .error .notFound
-
-def SanddState.timerExists (state : SanddState) (id : TimerId) : BaseIO Bool := do
-  let timers ← state.timers.atomically get
-  return timers.find? id |>.isSome
 
 private def xdgDataHome : OptionT BaseIO FilePath :=
   xdgDataHomeEnv <|> dataHomeDefault
@@ -73,9 +43,24 @@ def playTimerSound : IO Unit := do
   -- todo choose most appropriate media player, possibly record a dependency for package
   _ ← Sand.runCmdSimple "paplay" #[soundPath.toString]
 
-partial def busyWaitTil (due : Nat) : IO Unit := do
-  while (← IO.monoMsNow) < due do
-    pure ()
+structure SanddState where
+  nextTimerId : IO.Mutex Nat
+  timers : IO.Mutex (HashMap Nat (Timer × Task (Except IO.Error Unit)))
+
+def SanddState.removeTimer (state : SanddState) (id : TimerId) : BaseIO (TimerOpResult Unit) := do
+  let timers ← state.timers.atomically get
+  -- match timers.findIdx? (λ timer ↦ timer.id == id) with
+  match timers.find? id with
+  | some _ => do
+    -- TODO cancel the task instead.
+    state.timers.atomically <| set <| timers.erase id
+    pure <| .ok ()
+  | none => do
+    pure <| .error .notFound
+
+def SanddState.timerExists (state : SanddState) (id : TimerId) : BaseIO Bool := do
+  let timers ← state.timers.atomically get
+  return timers.find? id |>.isSome
 
 -- IO.sleep isn't guaranteed to be on time, I find it's usually about 10ms late
 -- this strategy aims to be exactly on time (to the millisecond), while
@@ -97,9 +82,27 @@ partial def countdown
       IO.sleep (remaining_ms/2).toUInt32
 
     -- continue counting down if the timer hasn't been canceled
+    -- TODO check for task cancellation instead
     if (← state.timerExists id) then
       loop
 
+
+def SanddState.initial : IO SanddState := do
+  return {
+    nextTimerId := (← IO.Mutex.new 1),
+    timers := (← IO.Mutex.new ∅)
+  }
+
+def SanddState.addTimer (state : SanddState) (due : Nat) : BaseIO Unit := do
+  let id : TimerId ← state.nextTimerId.atomically (getModify Nat.succ)
+  let timer : Timer := ⟨id, due⟩
+  let countdownTask ← IO.asTask <| countdown state id due
+  state.timers.atomically <| modify (·.insert id (timer, countdownTask))
+
+partial def busyWaitTil (due : Nat) : IO Unit := do
+  while (← IO.monoMsNow) < due do
+    pure ()
+
 def addTimer (state : SanddState) (startTime : Nat) (duration : Duration) : IO Unit := do
   -- run timer
   let msg := s!"Starting timer for {duration.formatColonSeparated}"
@@ -112,8 +115,7 @@ def addTimer (state : SanddState) (startTime : Nat) (duration : Duration) : IO U
   -- go off 30s after wake.{}
   let timerDue := startTime + duration.millis
 
-  let timerId ← state.addTimer timerDue
-  countdown state timerId timerDue
+  state.addTimer timerDue
 
 def handleClientCmd
   (client : Socket) (state : SanddState) (clientConnectedTime : Nat)
@@ -130,7 +132,7 @@ def handleClientCmd
       _ ← client.send CmdResponse.ok.serialize
   | .list => do
     let timers ← state.timers.atomically get
-    _ ← client.send <| (CmdResponse.list timers.values).serialize
+    _ ← client.send <| (CmdResponse.list <| timers.values.map Prod.fst).serialize
   | .pause which => sorry
   | .resume which => sorry