daemon responds to all client messages, client provides feedback to user

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

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:",

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