Merge pull request #16 from sullyj3/cancellation

Cancellation

src/Sand/Basic.lean

@@ -89,6 +89,7 @@ def notify (message : String) : IO SimpleChild :=
 inductive Command
  | addTimer (duration : Duration)
  | list
+ | cancelTimer (which : TimerId)
  deriving Repr, ToJson, FromJson
 
 end Sand

src/Sand/SandClient.lean

@@ -116,6 +116,9 @@ def parseArgs : List String → Option Command
  | [] => none
  | ["list"] => some .list
  | ["ls"] => some .list
+ | ["cancel", idStr] => do
+ let timerId ← idStr.toNat?
+ return .cancelTimer timerId
  | args => do
  let duration ← parseTimer args
  return .addTimer duration
@@ -142,6 +145,7 @@ def handleCmd (sock : Socket) (cmd : Command) : IO Unit := do
 
  match cmd with
  | Command.addTimer _ => pure ()
+ | Command.cancelTimer _ => pure ()
  | Command.list => do
  let resp ← sock.recv 10240
 

src/Sand/SandDaemon.lean

@@ -22,12 +22,22 @@ def addTimer (state : SanddState) (due : Nat) : BaseIO TimerId := do
  state.timers.atomically <| modify (·.push timer)
  return id
 
--- No-op if timer with TimerId `id` doesn't exist,
-def removeTimer (state : SanddState) (id : TimerId) : BaseIO Unit := do
- state.timers.atomically <| modify λ timers ↦
- match timers.findIdx? (λ timer ↦ timer.id == id) with
- | some idx => timers.eraseIdx idx
- | none => timers
+inductive RemoveTimerResult
+ | removed
+ | notFound
+
+def removeTimer (state : SanddState) (id : TimerId) : BaseIO RemoveTimerResult := do
+ let timers ← state.timers.atomically get
+ match timers.findIdx? (λ timer ↦ timer.id == id) with
+ | some idx => do
+ state.timers.atomically <| set <| timers.eraseIdx idx
+ pure .removed
+ | none => do
+ pure .notFound
+
+def timerExists (state : SanddState) (id : TimerId) : BaseIO Bool := do
+ let timers ← state.timers.atomically get
+ return timers.find? (·.id == id) |>.isSome
 
 end SanddState
 
@@ -58,15 +68,25 @@ partial def busyWaitTil (due : Nat) : IO Unit := do
 -- IO.sleep isn't guaranteed to be on time, I find it's usually about 10ms late
 -- this strategy aims to be exactly on time (to the millisecond), while
 -- avoiding a long busy wait which consumes too much cpu.
-partial def waitTil (due : Nat) : IO Unit := do
- let remaining_ms := due - (← IO.monoMsNow)
- -- We sleep while there's enough time left that we can afford to be inaccurate
- if remaining_ms > 50 then do
- IO.sleep (remaining_ms/2).toUInt32
- waitTil due
- -- then busy wait when we need to be on time
- else do
- busyWaitTil due
+partial def countdown
+ (state : SanddState) (id : TimerId) (due : Nat) : IO Unit := loop
+ where
+ loop := do
+ let remaining_ms := due - (← IO.monoMsNow)
+ if remaining_ms == 0 then
+ _ ← Sand.notify s!"Time's up!"
+ playTimerSound
+ _ ← state.removeTimer id
+ return
+
+ -- We repeatedly sleep while there's enough time left that we can afford to
+ -- be inaccurate, and spin once we're close to the due time.
+ if remaining_ms > 30 then
+ IO.sleep (remaining_ms/2).toUInt32
+
+ -- continue counting down if the timer hasn't been canceled
+ if (← state.timerExists id) then
+ loop
 
 def addTimer (state : SanddState) (startTime : Nat) (duration : Duration) : IO Unit := do
  -- run timer
@@ -80,16 +100,9 @@ def addTimer (state : SanddState) (startTime : Nat) (duration : Duration) : IO U
  -- go off 30s after wake.
  let timerDue := startTime + duration.millis
 
- let addTimerTask : Task TimerId ← BaseIO.asTask <|
- state.addTimer timerDue
-
- waitTil timerDue
- _ ← Sand.notify s!"Time's up!"
-
- playTimerSound
+ let timerId ← state.addTimer timerDue
+ countdown state timerId timerDue
 
- let timerId := addTimerTask.get
- state.removeTimer timerId
 
 def serializeTimers (timers : Array Timer) : ByteArray :=
  String.toUTF8 <| toString <| toJson timers
@@ -120,6 +133,12 @@ def handleClient
 
  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
 
 partial def forever (act : IO α) : IO β := act *> forever act