structure Std.Internal.IO.Async.Sleep : Type

Sleep can be used to sleep for some duration once. The underlying timer has millisecond resolution.

• ofNative :: (
• native : UV.Timer
• )

@[inline]

def Std.Internal.IO.Async.Sleep.mk (duration : Time.Millisecond.Offset) : IO Sleep

Set up a Sleep that waits for duration milliseconds. This function only initializes but does not yet start the timer.

Equations

• Std.Internal.IO.Async.Sleep.mk duration = do let native ← Std.Internal.UV.Timer.mk (Std.Time.Internal.UnitVal.toInt duration).toNat.toUInt64 false pure { native := native }

@[inline]

def Std.Internal.IO.Async.Sleep.wait (s : Sleep) : IO (AsyncTask Unit)

If:

• s is not yet running start it and return an AsyncTask that will resolve once the previously configured duration has run out.
• s is already or not anymore running return the same AsyncTask as the first call to wait.

Equations

• s.wait = do let promise ← s.native.next pure (Std.Internal.IO.Async.AsyncTask.ofPurePromise promise)

@[inline]

def Std.Internal.IO.Async.Sleep.reset (s : Sleep) : IO Unit

If:

• s is still running the timer restarts counting from now and finishes after duration milliseconds.
• s is not yet or not anymore running this is a no-op.

Equations

• s.reset = s.native.reset

@[inline]

def Std.Internal.IO.Async.Sleep.stop (s : Sleep) : IO Unit

If:

• s is still running this stops s without resolving any remaining AsyncTasks that were created through wait. Note that if another AsyncTask is binding on any of these it is going hang forever without further intervention.
• s is not yet or not anymore running this is a no-op.

Equations

• s.stop = s.native.stop

def Std.Internal.IO.Async.sleep (duration : Time.Millisecond.Offset) : IO (AsyncTask Unit)

Return an AsyncTask that resolves after duration.

Equations

• Std.Internal.IO.Async.sleep duration = do let sleeper ← Std.Internal.IO.Async.Sleep.mk duration sleeper.wait

structure Std.Internal.IO.Async.Interval : Type

Interval can be used to repeatedly wait for some duration like a clock. The underlying timer has millisecond resolution.

• ofNative :: (
• native : UV.Timer
• )

@[inline]

def Std.Internal.IO.Async.Interval.mk (duration : Time.Millisecond.Offset) : autoParam (0 < duration) _auto✝ → IO Interval

Setup up an Interval that waits for duration milliseconds. This function only initializes but does not yet start the timer.

Equations

• Std.Internal.IO.Async.Interval.mk duration x✝ = do let native ← Std.Internal.UV.Timer.mk (Std.Time.Internal.UnitVal.toInt duration).toNat.toUInt64 true pure { native := native }

@[inline]

def Std.Internal.IO.Async.Interval.tick (i : Interval) : IO (AsyncTask Unit)

If:

• i is not yet running start it and return an AsyncTask that resolves right away as the 0th multiple of duration has elapsed.
• i is already running and:
  • the tick from the last call of i has not yet finished return the same AsyncTask as the last call
  • the tick frrom the last call of i has finished return a new AsyncTask that waits for the closest next tick from the time of calling this function.
• i is not running aymore this is a no-op.

Equations

• i.tick = do let promise ← i.native.next pure (Std.Internal.IO.Async.AsyncTask.ofPurePromise promise)

@[inline]

def Std.Internal.IO.Async.Interval.reset (i : Interval) : IO Unit

If:

• Interval.tick was called on i before the timer restarts counting from now and the next tick happens in duration.
• i is not yet or not anymore running this is a no-op.

Equations

• i.reset = i.native.reset

@[inline]

def Std.Internal.IO.Async.Interval.stop (i : Interval) : IO Unit

If:

• i is still running this stops i without resolving any remaing AsyncTask that were created through tick. Note that if another AsyncTask is binding on any of these it is going hang forever without further intervention.
• i is not yet or not anymore running this is a no-op.

Equations

• i.stop = i.native.stop