Split CmdResponse into per-command Types

src/Sand/Basic.lean

@@ -35,12 +35,12 @@ inductive TimerState
 inductive TimerStateForClient
  | running (due : Moment)
  | paused (remaining : Duration)
- deriving ToJson, FromJson
+ deriving Repr, ToJson, FromJson
 
 structure TimerInfoForClient where
  id : TimerId
  state : TimerStateForClient
- deriving ToJson, FromJson
+ deriving Repr, ToJson, FromJson
 
 def timersForClient
  (timers : HashMap TimerId (Timer × TimerState))

src/Sand/Message.lean

@@ -1,7 +1,7 @@
 import Lean
 import «Sand».Basic
 
-open Lean (ToJson FromJson toJson)
+open Lean (Json ToJson FromJson toJson fromJson?)
 
 namespace Sand
 
@@ -10,20 +10,58 @@ inductive Command
  | addTimer (duration : Duration)
  | list
  | cancelTimer (which : TimerId)
- | pause (which : TimerId)
- | resume (which : TimerId)
+ | pauseTimer  (which : TimerId)
+ | resumeTimer (which : TimerId)
  deriving Repr, ToJson, FromJson
 
 -- responses to commands sent from server to client
-inductive CmdResponse
+inductive AddTimerResponse
  | ok
- | list (timers : Array TimerInfoForClient)
- | timerNotFound (which : TimerId)
- | noop
- | serviceError (msg : String)
- deriving ToJson, FromJson
-
-def CmdResponse.serialize : CmdResponse → ByteArray :=
- String.toUTF8 ∘ toString ∘ toJson
+ deriving Repr, ToJson, FromJson
+
+inductive ListResponse
+ | ok (timers : Array TimerInfoForClient)
+ deriving Repr, ToJson, FromJson
+
+inductive CancelTimerResponse
+ | ok
+ | timerNotFound
+ deriving Repr, ToJson, FromJson
+
+inductive PauseTimerResponse
+ | ok
+ | timerNotFound
+ | alreadyPaused
+ deriving Repr, ToJson, FromJson
+
+inductive ResumeTimerResponse
+ | ok
+ | timerNotFound
+ | alreadyRunning
+ deriving Repr, ToJson, FromJson
+
+def ResponseFor : Command → Type
+ | .addTimer _ => AddTimerResponse
+ | .list => ListResponse
+ | .cancelTimer _ => CancelTimerResponse
+ | .pauseTimer _ => PauseTimerResponse
+ | .resumeTimer _ => ResumeTimerResponse
+
+def toJsonResponse {cmd : Command} (resp : ResponseFor cmd) : Lean.Json := by
+ cases cmd <;> (
+ simp only [ResponseFor] at resp
+ exact toJson resp
+ )
+
+def serializeResponse {cmd : Command} (resp : ResponseFor cmd) : ByteArray :=
+ String.toUTF8 <| toString <| toJsonResponse resp
+
+def fromJsonResponse? {cmd : Command}
+ (resp : Json) : Except String (ResponseFor cmd) := by
+ cases cmd <;> (
+ simp only [ResponseFor]
+ exact fromJson? resp
+ )
+
 
 end Sand

src/Sand/SandClient.lean

@@ -3,8 +3,7 @@ import «Sand».Basic
 import «Sand».Time
 import «Sand».Message
 
-open Sand (Timer TimerId TimerInfoForClient Command CmdResponse Duration
- Moment instHsubMoments)
+open Sand
 
 def withUnixSocket path (action : Socket → IO a) := do
  let addr := Socket.SockAddrUnix.unix path
@@ -124,10 +123,10 @@ def parseArgs : List String → Option Command
  return .cancelTimer { id := timerId }
  | ["pause", idStr] => do
  let timerId ← idStr.toNat?
- return .pause { id := timerId }
+ return .pauseTimer { id := timerId }
  | ["resume", idStr] => do
  let timerId ← idStr.toNat?
- return .resume { id := timerId }
+ return .resumeTimer { id := timerId }
  | args => do
  let duration ← parseTimer args
  return .addTimer duration
@@ -162,8 +161,8 @@ def handleCmd (server : Socket) (cmd : Command) : IO Unit := do
  -- 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 resp? : Except String (ResponseFor cmd) :=
+ fromJsonResponse? =<< Lean.Json.parse respStr
  let .ok resp := resp? | do
  IO.println "Failed to parse message from server:"
  println! " \"{respStr}\""
@@ -172,38 +171,30 @@ def handleCmd (server : Socket) (cmd : Command) : IO Unit := do
  -- Handle response
  match cmd with
  | Command.addTimer timer => do
- let .ok := resp | unexpectedResponse respStr
+ let .ok := resp
  println! "Timer created for {timer.formatColonSeparated}."
  | Command.cancelTimer timerId => match resp with
  | .ok =>
  println! "Timer #{repr timerId.id} cancelled."
- | .timerNotFound timerId => timerNotFound timerId
- | _ => unexpectedResponse respStr
+ | .timerNotFound => timerNotFound timerId
  | Command.list => do
- let .list timers := resp | unexpectedResponse respStr
+ let .ok timers := resp
  let now ← Moment.mk <$> IO.monoMsNow
  IO.println <| showTimers timers.data now
- | Command.pause which => match resp with
+ | Command.pauseTimer which => match resp with
  | .ok =>
  println! "Timer #{repr which.id} paused."
- | .timerNotFound timerId => timerNotFound timerId
- | .noop =>
+ | .timerNotFound => timerNotFound which
+ | .alreadyPaused =>
  println! "Timer {repr which.id} is already paused."
- | _ => unexpectedResponse respStr
- | Command.resume which => match resp with
+ | Command.resumeTimer which => match resp with
  | .ok =>
  println! "Timer #{repr which.id} resumed."
- | .timerNotFound timerId => timerNotFound timerId
- | .noop =>
+ | .timerNotFound => timerNotFound which
+ | .alreadyRunning =>
  println! "Timer {repr which.id} is already running."
- | _ => unexpectedResponse respStr
 
  where
- unexpectedResponse {α : Type} (resp : String) : IO α := do
- IO.println "Unexpected response from server:"
- println! " \"{resp}\""
- IO.Process.exit 1
-
  timerNotFound (timerId : TimerId) := do
  println! "Timer with id \"{repr timerId.id}\" not found."
  IO.Process.exit 1

src/Sand/SandDaemon.lean

@@ -8,10 +8,7 @@ open Lean (Json ToJson FromJson toJson fromJson?)
 
 open Batteries (HashMap)
 
-open Sand (
- Timer TimerId TimerState TimerInfoForClient Command CmdResponse Duration
- Moment
- )
+open Sand
 
 inductive TimerOpError
  | notFound
@@ -168,37 +165,38 @@ def addTimer (duration : Duration) : CmdHandlerT IO Unit := do
 
  (SanddState.addTimer timerDue).liftBaseIO
 
-def handleClientCmd (cmd : Command) : CmdHandlerT IO CmdResponse := do
+def handleClientCmd (cmd : Command) : CmdHandlerT IO (ResponseFor cmd) := do
  let env@{state, client, clientConnectedTime} ← read
  match cmd with
  | .addTimer durationMs => do
  _ ← IO.asTask <| (addTimer durationMs).run env
- return CmdResponse.ok
+ return .ok
  | .cancelTimer which => do
  match ← (SanddState.removeTimer which).liftBaseIO with
  | .error .notFound => do
- return CmdResponse.timerNotFound which
+ return .timerNotFound
  -- TODO yuck
  | .error err@(.noop) => do
  let errMsg := s!"BUG: Unexpected error \"{repr err}\" from removeTimer."
  IO.eprintln errMsg
- return .serviceError errMsg
- | .ok () => pure CmdResponse.ok
+ IO.Process.exit 1
+ | .ok () => pure .ok
  | .list => do
  let timers ← state.timers.atomically get
- return CmdResponse.list <| Sand.timersForClient timers
- | .pause which => do
+ return .ok <| Sand.timersForClient timers
+ | .pauseTimer which => do
  let result ← (SanddState.pauseTimer which).run {state, client, clientConnectedTime}
- return responseForResult which result
- | .resume which => do
+ return match result with
+ | .ok () => .ok
+ | .error .notFound => .timerNotFound
+ | .error .noop => .alreadyPaused
+
+ | .resumeTimer which => do
  let result ← (SanddState.resumeTimer which).liftBaseIO
- return responseForResult which result
- where
- responseForResult (timerId : TimerId) result :=
- match result with
- | .ok () => CmdResponse.ok
- | .error .notFound => CmdResponse.timerNotFound timerId
- | .error .noop => CmdResponse.noop
+ return match result with
+ | .ok () => .ok
+ | .error .notFound => .timerNotFound
+ | .error .noop => .alreadyRunning
 
 def handleClient : CmdHandlerT IO Unit := do
  let {client, ..} ← read
@@ -212,7 +210,7 @@ def handleClient : CmdHandlerT IO Unit := do
  _ ← Sand.notify errMsg
 
  let resp ← handleClientCmd cmd
- _ ← client.send resp.serialize
+ _ ← client.send <| serializeResponse resp
 
 partial def forever (act : IO α) : IO β := act *> forever act