finish timer pause/resume

src/Sand/Basic.lean

@@ -1,8 +1,13 @@
 import Lean
 import Socket
+import Batteries
 
 open Lean (ToJson FromJson toJson)
 open System (FilePath)
+open Batteries (HashMap)
+
+def Batteries.HashMap.values [BEq α] [Hashable α] (hashMap : HashMap α β) : Array β :=
+ hashMap.toArray |>.map Prod.snd
 
 namespace Sand
 
@@ -68,6 +73,34 @@ structure Timer where
  due : Nat
  deriving Repr, ToJson, FromJson
 
+-- TODO this data model needs improvement
+-- currently paused timers retain their outdated due times while they're paused
+inductive TimerState
+ | paused (remaining : Duration)
+ | running (task : Task (Except IO.Error Unit))
+
+
+-- TODO filthy hack.
+-- revisit after reworking timer data model
+inductive TimerStateForClient
+ | running (due : Nat)
+ | paused (remaining : Duration)
+ deriving ToJson, FromJson
+
+structure TimerInfoForClient where
+ id : TimerId
+ state : TimerStateForClient
+ deriving ToJson, FromJson
+
+def timersForClient
+ (timers : HashMap Nat (Timer × TimerState))
+ : Array TimerInfoForClient :=
+ timers.values.map λ (timer, timerstate) ↦
+ let state : TimerStateForClient := match timerstate with
+ | TimerState.running _ => .running timer.due
+ | .paused remaining => .paused remaining
+ { id := timer.id, state }
+
 def nullStdioConfig : IO.Process.StdioConfig := ⟨.null, .null, .null⟩
 def SimpleChild : Type := IO.Process.Child nullStdioConfig
 
@@ -97,8 +130,9 @@ inductive Command
 -- responses to commands sent from server to client
 inductive CmdResponse
  | ok
- | list (timers : Array Timer)
+ | list (timers : Array TimerInfoForClient)
  | timerNotFound (which : TimerId)
+ | noop
  deriving ToJson, FromJson
 
 def CmdResponse.serialize : CmdResponse → ByteArray :=

src/Sand/SandClient.lean

@@ -1,7 +1,7 @@
 import Socket
 import «Sand».Basic
 
-open Sand (Timer Command CmdResponse Duration)
+open Sand (Timer TimerId TimerInfoForClient Command CmdResponse Duration)
 
 def withUnixSocket path (action : Socket → IO a) := do
  let addr := Socket.SockAddrUnix.unix path
@@ -125,14 +125,18 @@ def parseArgs : List String → Option Command
 
 def unlines := String.intercalate "\n"
 
-def showTimer (now : Nat) : Timer → String
- | {id, due} =>
- let remaining : Duration := ⟨due - now⟩
- let formatted := remaining.formatColonSeparated
-
- s!"#{repr id} | {formatted} remaining"
-
-def showTimers (timers : List Timer) (now : Nat) : String :=
+def showTimer (now : Nat) : TimerInfoForClient → String
+ | {id, state} =>
+ match state with
+ | .running due =>
+ let remaining : Duration := ⟨due - now⟩
+ let formatted := remaining.formatColonSeparated
+ s!"#{repr id} | {formatted} remaining"
+ | .paused remaining =>
+ let formatted := remaining.formatColonSeparated
+ s!"#{repr id} | {formatted} remaining (PAUSED)"
+
+def showTimers (timers : List TimerInfoForClient) (now : Nat) : String :=
  if timers.isEmpty then
  "No running timers."
  else
@@ -161,27 +165,40 @@ def handleCmd (server : Socket) (cmd : Command) : IO Unit := do
  | Command.addTimer timer => do
  let .ok := resp | unexpectedResponse respStr
  println! "Timer created for {timer.formatColonSeparated}."
- | Command.cancelTimer timerId => do
- match resp with
+ | Command.cancelTimer timerId => match resp with
  | .ok =>
  println! "Timer #{repr timerId} cancelled."
- | .timerNotFound timerId => do
- println! "Timer with id \"{repr timerId}\" not found."
- IO.Process.exit 1
+ | .timerNotFound timerId => timerNotFound timerId
  | _ => unexpectedResponse respStr
  | Command.list => do
  let .list timers := resp | unexpectedResponse respStr
  let now ← IO.monoMsNow
  IO.println <| showTimers timers.data now
- | Command.pause which => sorry
- | Command.resume which => sorry
+ | Command.pause which => match resp with
+ | .ok =>
+ println! "Timer #{repr which} paused."
+ | .timerNotFound timerId => timerNotFound timerId
+ | .noop =>
+ println! "Timer {repr which} is already paused."
+ | _ => unexpectedResponse respStr
+ | Command.resume which => match resp with
+ | .ok =>
+ println! "Timer #{repr which} resumed."
+ | .timerNotFound timerId => timerNotFound timerId
+ | .noop =>
+ println! "Timer {repr which} 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}\" not found."
+ IO.Process.exit 1
+
 def usage : String := unlines [
  "Usage:",
  "",

src/Sand/SandDaemon.lean

@@ -2,27 +2,20 @@ import «Sand».Basic
 import Batteries
 
 open System (FilePath)
-open Lean (Json toJson fromJson?)
+open Lean (Json ToJson FromJson toJson fromJson?)
 
 open Batteries (HashMap)
 
-open Sand (Timer TimerId Command CmdResponse Duration)
-
-def Batteries.HashMap.values [BEq α] [Hashable α] (hashMap : HashMap α β) : Array β :=
- hashMap.toArray |>.map Prod.snd
+open Sand (Timer TimerId TimerState TimerInfoForClient Command CmdResponse Duration)
 
 inductive TimerOpError
  | notFound
+ -- returned when calling pause on a paused timer, or resume on a running timer
+ | noop
+ deriving Repr
 
 def TimerOpResult α := Except TimerOpError α
 
-def SanddState.pauseTimer (state : SanddState) (timerId : TimerId)
- : BaseIO (TimerOpResult Unit) := sorry
-
-def SanddState.resumeTimer (state : SanddState) (timerId : TimerId)
- : BaseIO (TimerOpResult Unit) := sorry
-
-
 private def xdgDataHome : OptionT BaseIO FilePath :=
  xdgDataHomeEnv <|> dataHomeDefault
  where
@@ -43,14 +36,26 @@ def playTimerSound : IO Unit := do
  -- todo choose most appropriate media player, possibly record a dependency for package
  _ ← Sand.runCmdSimple "paplay" #[soundPath.toString]
 
-inductive TimerState
- | paused (remaining : Duration)
- | running (task : Task (Except IO.Error Unit))
-
 structure SanddState where
  nextTimerId : IO.Mutex Nat
  timers : IO.Mutex (HashMap Nat (Timer × TimerState))
 
+def SanddState.pauseTimer
+ (state : SanddState) (timerId : TimerId) (clientConnectedTime : Nat)
+ : BaseIO (TimerOpResult Unit) := state.timers.atomically do
+ let timers ← get
+ let some (timer, timerstate) := timers.find? timerId | do
+ return .error .notFound
+ match timerstate with
+ | .paused _ => return .error .noop
+ | .running task => do
+ IO.cancel task
+ let remaining := ⟨timer.due - clientConnectedTime⟩
+ let newTimerstate := .paused remaining
+ let newTimers := timers.insert timerId (timer, newTimerstate)
+ set newTimers
+ return .ok ()
+
 def SanddState.removeTimer (state : SanddState) (id : TimerId) : BaseIO (TimerOpResult Unit) := do
  state.timers.atomically do
  let timers ← get
@@ -89,6 +94,22 @@ partial def countdown
  IO.sleep (remaining_ms/2).toUInt32
  loop
 
+def SanddState.resumeTimer
+ (state : SanddState) (timerId : TimerId) (clientConnectedTime : Nat)
+ : BaseIO (TimerOpResult Unit) := state.timers.atomically do
+ let timers ← get
+ let some (timer, timerstate) := timers.find? timerId | do
+ return .error .notFound
+ match timerstate with
+ | .running _ => return .error .noop
+ | .paused remaining => do
+ let newDueTime := clientConnectedTime + remaining.millis
+ let countdownTask ← IO.asTask <| countdown state timerId newDueTime
+ let newTimerstate := .running countdownTask
+ let newTimer := {timer with due := newDueTime}
+ set <| timers.insert timerId (newTimer, newTimerstate)
+ return .ok ()
+
 def SanddState.initial : IO SanddState := do
  return {
  nextTimerId := (← IO.Mutex.new 1),
@@ -130,13 +151,35 @@ def handleClientCmd
  match ← state.removeTimer which with
  | .error .notFound => do
  _ ← client.send <| (CmdResponse.timerNotFound which).serialize
+ -- TODO yuck
+ | .error err@(.noop) => do
+ IO.eprintln s!"BUG: Unexpected error \"{repr err}\" from removeTimer."
  | .ok () => do
  _ ← client.send CmdResponse.ok.serialize
  | .list => do
  let timers ← state.timers.atomically get
- _ ← client.send <| (CmdResponse.list <| timers.values.map Prod.fst).serialize
- | .pause which => sorry
- | .resume which => sorry
+
+ _ ← client.send <| (CmdResponse.list <| Sand.timersForClient timers).serialize
+
+ -- TODO factor repetition
+ | .pause which => do
+ let result ← state.pauseTimer which clientConnectedTime
+ match result with
+ | .ok () => do
+ _ ← client.send CmdResponse.ok.serialize
+ | .error .notFound => do
+ _ ← client.send (CmdResponse.timerNotFound which).serialize
+ | .error .noop => do
+ _ ← client.send CmdResponse.noop.serialize
+ | .resume which => do
+ let result ← state.resumeTimer which clientConnectedTime
+ match result with
+ | .ok () => do
+ _ ← client.send CmdResponse.ok.serialize
+ | .error .notFound => do
+ _ ← client.send (CmdResponse.timerNotFound which).serialize
+ | .error .noop => do
+ _ ← client.send CmdResponse.noop.serialize
 
 def handleClient
  (client : Socket)