From 614c836385c10dfe4d24d5a0a425eb44be6954f0 Mon Sep 17 00:00:00 2001
From: James Sully <sullyj3@gmail.com>
Date: Sat, 27 Jul 2024 19:27:46 +1000
Subject: [PATCH] daemon responds to all client messages, client provides
 feedback to user

---
 src/Sand/Basic.lean      | 15 +++++++++++-
 src/Sand/SandClient.lean | 51 ++++++++++++++++++++++++++++------------
 src/Sand/SandDaemon.lean | 44 +++++++++++++++++-----------------
 3 files changed, 71 insertions(+), 39 deletions(-)

diff --git a/src/Sand/Basic.lean b/src/Sand/Basic.lean
index d3df3aa..295f582 100644
--- a/src/Sand/Basic.lean
+++ b/src/Sand/Basic.lean
@@ -1,7 +1,7 @@
 import Lean
 import Socket
 
-open Lean (ToJson FromJson)
+open Lean (ToJson FromJson toJson)
 open System (FilePath)
 
 namespace Sand
@@ -92,4 +92,17 @@ inductive Command
   | cancelTimer (which : TimerId)
   deriving Repr, ToJson, FromJson
 
+-- 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
+
+def CmdResponse.serialize : CmdResponse → ByteArray :=
+  String.toUTF8 ∘ toString ∘ toJson
+
+
 end Sand
diff --git a/src/Sand/SandClient.lean b/src/Sand/SandClient.lean
index 9e6d19a..31f4845 100644
--- a/src/Sand/SandClient.lean
+++ b/src/Sand/SandClient.lean
@@ -1,7 +1,7 @@
 import Socket
 import «Sand».Basic
 
-open Sand (Timer Command Duration)
+open Sand (Timer Command CmdResponse Duration)
 
 def withUnixSocket path (action : Socket → IO a) := do
   let addr := Socket.SockAddrUnix.unix path
@@ -139,25 +139,46 @@ def showTimers (timers : List Timer) (now : Nat) : String :=
     unlines <| List.map (showTimer now) <| timers
 
 open Lean (fromJson? toJson) in
-def handleCmd (sock : Socket) (cmd : Command) : IO Unit := do
+def handleCmd (server : Socket) (cmd : Command) : IO Unit := do
   let msg : String := toString <| toJson cmd
-  let _nBytes ← sock.send msg.toUTF8
+  let _nBytes ← server.send msg.toUTF8
+
+  -- TODO: need a way to recv with timeout in case of daemon failure
+  -- TODO: think more about receive buffer size.
+  --   in particular, list response can be arbitrarily long
+  --   we should handle that correctly without allocating such a large
+  --   buffer in the common case
+  let respStr ← String.fromUTF8! <$> server.recv 10240
+  let resp? : Except String CmdResponse :=
+    fromJson? =<< Lean.Json.parse respStr
+  let .ok resp := resp? | do
+    IO.println "Failed to parse message from server:"
+    println! "    \"{respStr}\""
+    IO.Process.exit 1
 
+  -- Handle response
   match cmd with
-  | Command.addTimer _ => pure ()
-  | Command.cancelTimer _ => pure ()
+  | Command.addTimer timer => do
+    let .ok := resp | unexpectedResponse respStr
+    println! "Timer created for {timer.formatColonSeparated}."
+  | Command.cancelTimer timerId => do
+    match resp with
+    | .ok =>
+      println! "Timer #{repr timerId} cancelled."
+    | .timerNotFound timerId => do
+      println! "Timer with id \"{repr timerId}\" not found."
+      IO.Process.exit 1
+    | _ => unexpectedResponse respStr
   | Command.list => do
-    let resp ← sock.recv 10240
-
-    let timers? : Except String (List Timer) := do
-      let json ← Lean.Json.parse <| String.fromUTF8! resp
-      fromJson? json
-
-    let .ok timers := timers? | do
-      println! "failed to parse message from server. exiting"
-
+    let .list timers := resp | unexpectedResponse respStr
     let now ← IO.monoMsNow
-    IO.println <| showTimers timers now
+    IO.println <| showTimers timers.data now
+
+  where
+  unexpectedResponse {α : Type} (resp : String) : IO α := do
+    IO.println "Unexpected response from server:"
+    println! "    \"{resp}\""
+    IO.Process.exit 1
 
 def usage : String := unlines [
     "Usage:",
diff --git a/src/Sand/SandDaemon.lean b/src/Sand/SandDaemon.lean
index b506e52..826afeb 100644
--- a/src/Sand/SandDaemon.lean
+++ b/src/Sand/SandDaemon.lean
@@ -6,7 +6,10 @@ open Lean (Json toJson fromJson?)
 
 open Batteries (HashMap)
 
-open Sand (Timer TimerId Command Duration)
+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
@@ -108,19 +111,22 @@ def addTimer (state : SanddState) (startTime : Nat) (duration : Duration) : IO U
   let timerId ← state.addTimer timerDue
   countdown state timerId timerDue
 
+def handleClientCmd
+  (client : Socket) (state : SanddState) (clientConnectedTime : Nat)
+  : Command → IO Unit
 
-def serializeTimers (timers : HashMap Nat Timer) : ByteArray :=
-  timers
-    |>.toArray
-    |>.map Prod.snd -- get values
-    |> toJson
-    |> toString
-    |>.toUTF8
-
-def list (state : SanddState) (client : Socket) : IO Unit := do
-  let timers ← state.timers.atomically get
-  _ ← client.send <| serializeTimers timers
-
+  | .addTimer durationMs => do
+    _ ← IO.asTask <| addTimer state clientConnectedTime durationMs
+    _ ← client.send CmdResponse.ok.serialize
+  | .cancelTimer which => do
+    match ← state.removeTimer which with
+    | .notFound => do
+      _ ← client.send <| (CmdResponse.timerNotFound which).serialize
+    | .removed => do
+      _ ← client.send CmdResponse.ok.serialize
+  | .list => do
+    let timers ← state.timers.atomically get
+    _ ← client.send <| (CmdResponse.list timers.values).serialize
 
 def handleClient
   (client : Socket)
@@ -130,7 +136,7 @@ def handleClient
   -- IO.monoMsNow is an ffi call to `std::chrono::steady_clock::now()`
   -- Technically this clock is not guaranteed to be the same between
   -- processes, but it seems to be in practice on linux
-  let startTime ← IO.monoMsNow
+  let clientConnectedTime ← IO.monoMsNow
 
   -- receive and parse message
   let bytes ← client.recv (maxBytes := 1024)
@@ -141,15 +147,7 @@ def handleClient
     IO.eprintln errMsg
     _ ← Sand.notify errMsg
 
-  match cmd with
-  | .addTimer durationMs => addTimer state startTime durationMs
-  | .cancelTimer which => do
-    match ← state.removeTimer which with
-    | .notFound => do
-      -- TODO tell client it doesn't exist
-      pure ()
-    | .removed => pure ()
-  | .list => list state client
+  handleClientCmd client state clientConnectedTime cmd
 
 partial def forever (act : IO α) : IO β := act *> forever act