From 358daf3a4e46061fa2a3e7f2b608e5932676dab4 Mon Sep 17 00:00:00 2001
From: James Sully <sullyj3@gmail.com>
Date: Sat, 27 Jul 2024 21:46:43 +1000
Subject: [PATCH] Create TimerOpResult for reporting of results related to
 timers

replace RemoveTimerResult with this

this will also be used for pause/resume timer
---
 src/Sand/Basic.lean      |  2 --
 src/Sand/SandDaemon.lean | 15 ++++++++-------
 2 files changed, 8 insertions(+), 9 deletions(-)

diff --git a/src/Sand/Basic.lean b/src/Sand/Basic.lean
index 295f582..9b67226 100644
--- a/src/Sand/Basic.lean
+++ b/src/Sand/Basic.lean
@@ -94,10 +94,8 @@ inductive Command
 
 -- responses to commands sent from server to client
 inductive CmdResponse
-  -- acknowledgement of `addTimer` and `cancelTimer`
   | ok
   | list (timers : Array Timer)
-  -- response to `cancelTimer` of nonexistent `TimerId`
   | timerNotFound (which : TimerId)
   deriving ToJson, FromJson
 
diff --git a/src/Sand/SandDaemon.lean b/src/Sand/SandDaemon.lean
index 826afeb..5e1969a 100644
--- a/src/Sand/SandDaemon.lean
+++ b/src/Sand/SandDaemon.lean
@@ -29,19 +29,20 @@ def addTimer (state : SanddState) (due : Nat) : BaseIO TimerId := do
   state.timers.atomically <| modify (·.insert id timer)
   return id
 
-inductive RemoveTimerResult
-  | removed
+inductive TimerOpError
   | notFound
 
-def removeTimer (state : SanddState) (id : TimerId) : BaseIO RemoveTimerResult := do
+def TimerOpResult α := Except TimerOpError α
+
+def 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 .removed
+    pure <| .ok ()
   | none => do
-    pure .notFound
+    pure <| .error .notFound
 
 def timerExists (state : SanddState) (id : TimerId) : BaseIO Bool := do
   let timers ← state.timers.atomically get
@@ -120,9 +121,9 @@ def handleClientCmd
     _ ← client.send CmdResponse.ok.serialize
   | .cancelTimer which => do
     match ← state.removeTimer which with
-    | .notFound => do
+    | .error .notFound => do
       _ ← client.send <| (CmdResponse.timerNotFound which).serialize
-    | .removed => do
+    | .ok () => do
       _ ← client.send CmdResponse.ok.serialize
   | .list => do
     let timers ← state.timers.atomically get