structure Std.Async.Sleep : Type

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

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

@[inline]

def Std.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.Async.Sleep.mk duration = do let native ← liftM (Std.Internal.UV.Timer.mk (Std.Async.timeoutOf✝ duration) false) pure { native := native }

@[inline]

def Std.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 running, or finished after completing, return the same Async computation as the last call to wait. A select that checks s before it completes restarts it, and the computations from earlier calls then fail.
• s was stopped with stop before completing, return an Async computation that fails.

Equations

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

@[inline]

def Std.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.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. Those computations fail once the last reference to their promise is dropped, rather than producing a value.
• s is not yet or not anymore running this is a no-op.

Equations

• s.stop = s.native.stop

def Std.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. Every select or Selectable.tryOne that checks s before it has finished starts it again from duration, so a Sleep that is checked more often than duration never finishes.

Equations

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

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

Return an Async computation that completes after duration.

Equations

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

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

Return a Selector that completes after duration.

Equations

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

structure Std.Async.Interval : Type

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

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

@[inline]

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

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

Equations

• Std.Async.Interval.mk duration x✝ = do let native ← Std.Internal.UV.Timer.mk (Std.Async.timeoutOf✝ duration) true pure { native := native }

@[inline]

def Std.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, the returned Async computation fails, as stop dropped the promise it would have completed.

Equations

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

@[inline]

def Std.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.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. Those computations fail once the last reference to their promise is dropped, rather than producing a value.
• i is not yet or not anymore running this is a no-op.

Equations

• i.stop = i.native.stop