Merge create Moment type

src/Sand/Basic.lean

@@ -6,6 +6,7 @@ import «Sand».Time
 open Lean (ToJson FromJson toJson)
 open System (FilePath)
 open Batteries (HashMap)
+open Sand (Moment)
 
 def Batteries.HashMap.values [BEq α] [Hashable α] (hashMap : HashMap α β) : Array β :=
  hashMap.toArray |>.map Prod.snd
@@ -20,7 +21,7 @@ def TimerId.fromNat (n : Nat) : TimerId := ⟨n⟩
 
 structure Timer where
  id : TimerId
- due : Nat
+ due : Moment
  deriving Repr, ToJson, FromJson
 
 -- TODO this data model needs improvement
@@ -29,11 +30,10 @@ 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)
+ | running (due : Moment)
  | paused (remaining : Duration)
  deriving ToJson, FromJson
 

src/Sand/SandClient.lean

@@ -2,7 +2,8 @@ import Socket
 import «Sand».Basic
 import «Sand».Time
 
-open Sand (Timer TimerId TimerInfoForClient Command CmdResponse Duration)
+open Sand (Timer TimerId TimerInfoForClient Command CmdResponse Duration
+ Moment instHsubMoments)
 
 def withUnixSocket path (action : Socket → IO a) := do
  let addr := Socket.SockAddrUnix.unix path
@@ -132,18 +133,18 @@ def parseArgs : List String → Option Command
 
 def unlines := String.intercalate "\n"
 
-def showTimer (now : Nat) : TimerInfoForClient → String
+def showTimer (now : Moment) : TimerInfoForClient → String
  | {id, state} =>
  match state with
  | .running due =>
- let remaining : Duration := ⟨due - now⟩
+ 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 :=
+def showTimers (timers : List TimerInfoForClient) (now : Moment) : String :=
  if timers.isEmpty then
  "No running timers."
  else
@@ -179,7 +180,7 @@ def handleCmd (server : Socket) (cmd : Command) : IO Unit := do
  | _ => unexpectedResponse respStr
  | Command.list => do
  let .list timers := resp | unexpectedResponse respStr
- let now ← IO.monoMsNow
+ let now ← Moment.mk <$> IO.monoMsNow
  IO.println <| showTimers timers.data now
  | Command.pause which => match resp with
  | .ok =>

src/Sand/SandDaemon.lean

@@ -7,7 +7,10 @@ open Lean (Json ToJson FromJson toJson fromJson?)
 
 open Batteries (HashMap)
 
-open Sand (Timer TimerId TimerState TimerInfoForClient Command CmdResponse Duration)
+open Sand (
+ Timer TimerId TimerState TimerInfoForClient Command CmdResponse Duration
+ Moment
+ )
 
 inductive TimerOpError
  | notFound
@@ -45,7 +48,7 @@ structure SanddState where
  timers : IO.Mutex Timers
 
 def SanddState.pauseTimer
- (state : SanddState) (timerId : TimerId) (clientConnectedTime : Nat)
+ (state : SanddState) (timerId : TimerId) (clientConnectedTime : Moment)
  : BaseIO (TimerOpResult Unit) := state.timers.atomically do
  let timers ← get
  let some (timer, timerstate) := timers.find? timerId | do
@@ -54,7 +57,7 @@ def SanddState.pauseTimer
  | .paused _ => return .error .noop
  | .running task => do
  IO.cancel task
- let remaining := ⟨timer.due - clientConnectedTime⟩
+ let remaining : Duration := timer.due - clientConnectedTime
  let newTimerstate := .paused remaining
  let newTimers : Timers := timers.insert timerId (timer, newTimerstate)
  set newTimers
@@ -83,32 +86,33 @@ def SanddState.timerExists (state : SanddState) (id : TimerId) : BaseIO Bool :=
 -- strategy aims to be exactly on time (to the millisecond), while avoiding a
 -- long busy wait which consumes too much cpu.
 partial def countdown
- (state : SanddState) (id : TimerId) (due : Nat) : IO Unit := loop
+ (state : SanddState) (id : TimerId) (due : Moment) : IO Unit := loop
  where
  loop := do
- let remaining_ms := due - (← IO.monoMsNow)
+ let now ← Moment.mk <$> IO.monoMsNow
+ let remaining := due - now
  -- This task will be cancelled if the timer is cancelled or paused.
  -- in case of resumed, a new separate task will be spawned.
  if ← IO.checkCanceled then return
- if remaining_ms == 0 then
+ if remaining.millis == 0 then
  _ ← Sand.notify s!"Time's up!"
  playTimerSound
  _ ← state.removeTimer id
  return
- if remaining_ms > 30 then
- IO.sleep (remaining_ms/2).toUInt32
+ if remaining.millis > 30 then
+ IO.sleep (remaining.millis/2).toUInt32
  loop
 
 def SanddState.resumeTimer
- (state : SanddState) (timerId : TimerId) (clientConnectedTime : Nat)
+ (state : SanddState) (timerId : TimerId) (clientConnectedTime : Moment)
  : 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 newDueTime : Moment := clientConnectedTime + remaining
  let countdownTask ← IO.asTask <| countdown state timerId newDueTime
  let newTimerstate := .running countdownTask
  let newTimer := {timer with due := newDueTime}
@@ -122,7 +126,7 @@ def SanddState.initial : IO SanddState := do
  timers := (← IO.Mutex.new ∅)
  }
 
-def SanddState.addTimer (state : SanddState) (due : Nat) : BaseIO Unit := do
+def SanddState.addTimer (state : SanddState) (due : Moment) : BaseIO Unit := do
  let id : TimerId ←
  TimerId.mk <$> state.nextTimerId.atomically (getModify Nat.succ)
  let timer : Timer := ⟨id, due⟩
@@ -133,7 +137,7 @@ partial def busyWaitTil (due : Nat) : IO Unit := do
  while (← IO.monoMsNow) < due do
  pure ()
 
-def addTimer (state : SanddState) (startTime : Nat) (duration : Duration) : IO Unit := do
+def addTimer (state : SanddState) (startTime : Moment) (duration : Duration) : IO Unit := do
  -- run timer
  let msg := s!"Starting timer for {duration.formatColonSeparated}"
 
@@ -143,12 +147,12 @@ def addTimer (state : SanddState) (startTime : Nat) (duration : Duration) : IO U
  -- TODO: problem with this approach - time spent suspended is not counted.
  -- eg if I set a 1 minute timer, then suspend at 30s, the timer will
  -- go off 30s after wake.{}
- let timerDue := startTime + duration.millis
+ let timerDue := startTime + duration
 
  state.addTimer timerDue
 
 def handleClientCmd
- (client : Socket) (state : SanddState) (clientConnectedTime : Nat)
+ (client : Socket) (state : SanddState) (clientConnectedTime : Moment)
  : Command → IO Unit
 
  | .addTimer durationMs => do
@@ -196,7 +200,7 @@ def handleClient
  -- IO.monoMsNow is an ffi call to `std::chrono::steady_clock::now()`
  -- Technically this clock is not guaranteed to be the same between
  -- processes, but it seems to be in practice on linux
- let clientConnectedTime ← IO.monoMsNow
+ let clientConnectedTime ← Moment.mk <$> IO.monoMsNow
 
  -- receive and parse message
  let bytes ← client.recv (maxBytes := 1024)

src/Sand/Time.lean

@@ -4,13 +4,23 @@ open Lean (ToJson FromJson toJson)
 
 namespace Sand
 
+structure Moment where
+ millis : Nat
+ deriving Repr, ToJson, FromJson, BEq
+
 structure Duration where
  millis : Nat
  deriving Repr, ToJson, FromJson, BEq
 
 instance : Add Duration where
  add d1 d2 := { millis := d1.millis + d2.millis }
 
+instance : HAdd Moment Duration Moment where
+ hAdd mom dur := {millis := mom.millis + dur.millis : Moment}
+
+instance instHsubMoments : HSub Moment Moment Duration where
+ hSub m1 m2 := { millis := m1.millis - m2.millis }
+
 namespace Duration
 
 def fromSeconds (seconds : Nat) : Duration := { millis := 1000 * seconds }