def Std.Internal.UV.Timer : Type

Timers are used to generate IO.Promises that resolve after some time.

A Timer can be in one of 3 states:

• Right after construction it's initial.
• While it is ticking it's running.
• If it has stopped for some reason it's finished.

This together with whether it was set up as repeating with Timer.new determines the behavior of all functions on Timers.

Equations

• Std.Internal.UV.Timer = Std.Internal.UV.TimerImpl✝.type

instance Std.Internal.UV.instNonemptyTimer : Nonempty Timer

@[extern lean_uv_timer_mk]

opaque Std.Internal.UV.Timer.mk (timeout : UInt64) (repeating : Bool) : IO Timer

This creates a Timer in the initial state and doesn't run it yet.

• If repeating is false this constructs a timer that resolves once after timeout milliseconds, counting from when it's run.
• If repeating is true this constructs a timer that resolves after multiples of timeout milliseconds, counting from when it's run. Note that this includes the 0th multiple right after starting the timer. A timeout of 0 ticks every millisecond, and reset then delays the next tick by 1 millisecond. A running repeating timer is kept alive while a promise from next is pending, and otherwise stops once nothing references it.

@[extern lean_uv_timer_next]

opaque Std.Internal.UV.Timer.next (timer : Timer) : IO (IO.Promise Unit)

This function has different behavior depending on the state and configuration of the Timer:

• if repeating is false and:
  • it is initial, run it and return a new IO.Promise that is set to resolve once timeout milliseconds have elapsed. After this IO.Promise is resolved the Timer is finished.
  • it is running, or finished after firing, return the same IO.Promise that the last call to next returned.
  • it was stopped with stop before firing, return a new IO.Promise that is never resolved.
• if repeating is true and:
  • it is initial, run it and return a new IO.Promise that resolves right away (as it is the 0th multiple of timeout).
  • it is running, check whether the last returned IO.Promise is already resolved:
    • If it is, return a new IO.Promise that resolves upon finishing the next cycle
    • If it is not, return the last IO.Promise This ensures that the returned IO.Promise resolves at the next repetition of the timer.
  • if it is finished, return a new IO.Promise that is never resolved, as stop dropped the last one.

A promise from next may also be resolved by the code holding it; the timer then treats it as fulfilled when it fires.

@[extern lean_uv_timer_reset]

opaque Std.Internal.UV.Timer.reset (timer : Timer) : IO Unit

This function has different behavior depending on the state and configuration of the Timer:

• If it is initial or finished this is a no-op.
• If it is running and repeating is false this will delay the resolution of the timer until timeout milliseconds after the call of this function.
• Delay the resolution of the next tick of the timer until timeout milliseconds after the call of this function, then continue normal ticking behavior from there.

@[extern lean_uv_timer_stop]

opaque Std.Internal.UV.Timer.stop (timer : Timer) : IO Unit

This function has different behavior depending on the state of the Timer:

• If it is initial or finished this is a no-op.
• If it is running the execution of the timer is stopped, it is put into the finished state and the promise generated by the next function is dropped.

@[extern lean_uv_timer_cancel]

opaque Std.Internal.UV.Timer.cancel (timer : Timer) : IO Unit

This function has different behavior depending on the state of the Timer:

• If it is initial or finished this is a no-op.
• If it is running, the promise generated by the next function is dropped.
  • If repeating is false then it sets the timer to the initial state.
  • If repeating is true the timer keeps ticking, and ticks before the next call to next are dropped.