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) : Async 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 ← liftM (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) : Async Unit

If:

• s is not yet running start it and return an Async computation that will complete once the previously configured duration has elapsed.
• s is already or not anymore running return the same Async computation as the first call to wait.

Equations

• s.wait = Std.Internal.IO.Async.Async.ofPurePromise s.native.next

@[inline]

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

If:

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

Equations

• s.reset = liftM s.native.reset

@[inline]

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

If:

• s is still running this stops s without completing any remaining Async computations that were created through wait. Note that if another Async computation is binding on any of these it will 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.selector (s : Sleep) : Selector Unit

Create a Selector that resolves once s has finished. s only starts when it runs inside of a Selectable.

Equations

• One or more equations did not get rendered due to their size.

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

Return an Async computation that completes after duration.

Equations

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

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

Return a Selector that completes after duration.

Equations

• Std.Internal.IO.Async.Selector.sleep duration = do let sleeper ← Std.Internal.IO.Async.Sleep.mk duration pure sleeper.selector

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) : Async Unit

If:

• i is not yet running start it and return an Async computation that completes 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 Async computation as the last call
  • the tick from the last call of i has finished return a new Async computation that waits for the closest next tick from the time of calling this function.
• i is not running anymore this is a no-op.

Equations

• i.tick = Std.Internal.IO.Async.Async.ofPurePromise i.native.next

@[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 completing any remaining Async computations that were created through tick. Note that if another Async computation is binding on any of these it will hang forever without further intervention.
• i is not yet or not anymore running this is a no-op.

Equations

• i.stop = i.native.stop