From a52047727efb8127cae74c0d010c6f070de46077 Mon Sep 17 00:00:00 2001 From: James Sully Date: Sun, 28 Jul 2024 20:45:24 +1000 Subject: [PATCH] Split CmdResponse into per-command Types --- src/Sand/Basic.lean | 4 +-- src/Sand/Message.lean | 62 ++++++++++++++++++++++++++++++++-------- src/Sand/SandClient.lean | 37 +++++++++--------------- src/Sand/SandDaemon.lean | 40 ++++++++++++-------------- 4 files changed, 85 insertions(+), 58 deletions(-) diff --git a/src/Sand/Basic.lean b/src/Sand/Basic.lean index eabf5de..1e63ade 100644 --- a/src/Sand/Basic.lean +++ b/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)) diff --git a/src/Sand/Message.lean b/src/Sand/Message.lean index da5961a..82a92f6 100644 --- a/src/Sand/Message.lean +++ b/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 diff --git a/src/Sand/SandClient.lean b/src/Sand/SandClient.lean index 89430cd..7df1be8 100644 --- a/src/Sand/SandClient.lean +++ b/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 diff --git a/src/Sand/SandDaemon.lean b/src/Sand/SandDaemon.lean index cd027cf..a507d41 100644 --- a/src/Sand/SandDaemon.lean +++ b/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