Skip to content

Commit

Permalink
Create TimerOpResult for reporting of results related to timers
Browse files Browse the repository at this point in the history
replace RemoveTimerResult with this

this will also be used for pause/resume timer
  • Loading branch information
sullyj3 committed Jul 28, 2024
1 parent 0059584 commit 358daf3
Show file tree
Hide file tree
Showing 2 changed files with 8 additions and 9 deletions.
2 changes: 0 additions & 2 deletions src/Sand/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -94,10 +94,8 @@ inductive Command

-- 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

Expand Down
15 changes: 8 additions & 7 deletions src/Sand/SandDaemon.lean
Original file line number Diff line number Diff line change
Expand Up @@ -29,19 +29,20 @@ def addTimer (state : SanddState) (due : Nat) : BaseIO TimerId := do
state.timers.atomically <| modify (·.insert id timer)
return id

inductive RemoveTimerResult
| removed
inductive TimerOpError
| notFound

def removeTimer (state : SanddState) (id : TimerId) : BaseIO RemoveTimerResult := do
def TimerOpResult α := Except TimerOpError α

def removeTimer (state : SanddState) (id : TimerId) : BaseIO (TimerOpResult Unit) := do
let timers ← state.timers.atomically get
-- match timers.findIdx? (λ timer ↦ timer.id == id) with
match timers.find? id with
| some _ => do
state.timers.atomically <| set <| timers.erase id
pure .removed
pure <| .ok ()
| none => do
pure .notFound
pure <| .error .notFound

def timerExists (state : SanddState) (id : TimerId) : BaseIO Bool := do
let timers ← state.timers.atomically get
Expand Down Expand Up @@ -120,9 +121,9 @@ def handleClientCmd
_ ← client.send CmdResponse.ok.serialize
| .cancelTimer which => do
match ← state.removeTimer which with
| .notFound => do
| .error .notFound => do
_ ← client.send <| (CmdResponse.timerNotFound which).serialize
| .removed => do
| .ok () => do
_ ← client.send CmdResponse.ok.serialize
| .list => do
let timers ← state.timers.atomically get
Expand Down

0 comments on commit 358daf3

Please sign in to comment.