Module Interactive_background_thread.Fut

type nonrec backtrace = Imandra_thread_util.Fut.backtrace
type nonrec exn_with_bt_opt = Imandra_thread_util.Fut.exn_with_bt_opt
include Imandra_thread_util.Fut.S0 with type 'a t = 'a Imandra_thread_util.Fut.t

The type of futures values of type 'a

val pp : 'a CCFormat.printer -> 'a t CCFormat.printer
val is_done : _ t -> bool

is_done fut is true iff state fut is not Fut_wait. In other words, the future has resolved to a value or an exception.

val return : 'a -> 'a t

Future that just contains a value

val fail : exn -> 'a t

Future that just contains a failure

val fail_with_backtrace : exn -> Imandra_thread_util.Fut.backtrace -> 'a t

Future that just contains a failure and backtrace

val fail_with_bt_opt : exn -> Imandra_thread_util.Fut.backtrace option -> 'a t
val error : ?process:string -> ?kind:Imandra_util.Error.kind -> loc:Imandra_util.Iloc.t -> string -> _ t

Interface to Error.error

val errorf : ?process:string -> ?kind:Imandra_util.Error.kind -> loc:Imandra_util.Iloc.t -> ( 'a, Stdlib.Format.formatter, unit, 'b t ) Stdlib.format4 -> 'a

Interface to Error.error

val return_res : ( 'a, Imandra_thread_util.Fut.exn_with_bt_opt ) Stdlib.result -> 'a t
val wait_block : 'a t -> 'a

Block the current thread until the future is resolved.

  • raises an

    exception e if the future was resolved with set_exn or created with fail

val wait_block_catch : 'a t -> ( 'a, Imandra_thread_util.Fut.exn_with_bt_opt ) Stdlib.result

Block the current thread until the future is resolved, like wait. Catches exceptions into a result.

val wait_block_poll : 'a t -> 'a

Wait in an active poll, so as to still catch signals and check other things.

val ignore : _ t -> unit
exception Already_set
type 'a promise

One shot setter for a future

val make : unit -> 'a t * 'a promise

Create a couple of future/promise, so we can fill the future by calling the promise exactly once

val set_done : 'a promise -> 'a -> unit

Set the result of this future to Fut_done x

  • raises Already_set

    if future is already resolved

val set_exn : _ promise -> exn -> unit

Set the result of this future to Fut_exn e

  • raises Already_set

    if future is already resolved

val set_exn_with_backtrace : _ promise -> exn -> Stdlib.Printexc.raw_backtrace -> unit
val set_result_no_bt : 'a promise -> ( 'a, exn ) Stdlib.result -> unit

Set the result of this future.

  • raises Already_set

    if future is already resolved

val set_result : 'a promise -> ( 'a, exn_with_bt_opt ) Stdlib.result -> unit

Set the result of this future.

  • raises Already_set

    if future is already resolved

val interrupt : _ t -> unit

If future is not resolved yet, interrupt it, set the state to Fut_exn Sys.Break

val interrupted : _ t -> bool

Fast check for interruption

val interrupted_promise : _ promise -> bool
val on_completion : f:( ( 'a, exn_with_bt_opt ) Stdlib.result -> unit ) -> 'a t -> unit

Run callback on completion

val both : 'a t -> 'b t -> ('a * 'b) t

Wait until both futures resolve, and return the tuple of their results

val delay : ( unit -> 'a t ) -> 'a t

delay ~f is the same as f, but forces the computation of f to run on the executor rather than right now. It can be useful for some recursive functions, or to avoid doing too much work upfront.

val map : f:( 'a -> 'b ) -> 'a t -> 'b t
val map_err : f:( ( 'a, exn_with_bt_opt ) Stdlib.result -> 'b ) -> 'a t -> 'b t
val flat_map : f:( 'a -> 'b t ) -> 'a t -> 'b t
val flat_map_err : f:( ( 'a, exn_with_bt_opt ) Stdlib.result -> 'b t ) -> 'a t -> 'b t
val map2 : f:( 'a -> 'b -> 'c ) -> 'a t -> 'b t -> 'c t

Wait until both futures resolve, and return the tuple of their results

val app : ( 'a -> 'b ) t -> 'a t -> 'b t

Applicative

val choice : 'a t -> 'a t -> 'a t

choice a b returns the result of the first of a,b to complete, whether it fails or succeeds.

val all_list : 'a t list -> 'a list t

Wait for all elements of the list

val iter_l : f:( 'a -> unit t ) -> 'a list -> unit t
val map_l : f:( 'a -> 'b t ) -> 'a list -> 'b list t

Map over a list

val wait_l : _ t list -> unit t

wait for all futures to terminate

val spawn : name:string -> ( unit -> 'a ) -> 'a t

Spawn in a new task

val spawn1 : name:string -> ( 'a -> 'b ) -> 'a -> 'b t

Spawn in a new task

val spawn2 : name:string -> ( 'a -> 'b -> 'c ) -> 'a -> 'b -> 'c t

Spawn in a new task

module Barrier : sig ... end
module Infix : sig ... end
include module type of Infix
val (>|=) : 'a t -> ( 'a -> 'b ) -> 'b t
val (>>=) : 'a t -> ( 'a -> 'b t ) -> 'b t
val let+ : 'a t -> ( 'a -> 'b ) -> 'b t
val let+? : 'a t -> ( ( 'a, exn_with_bt_opt ) Stdlib.result -> 'b ) -> 'b t
val and+ : 'a t -> 'b t -> ('a * 'b) t
val let* : 'a t -> ( 'a -> 'b t ) -> 'b t
val let*? : 'a t -> ( ( 'a, exn_with_bt_opt ) Stdlib.result -> 'b t ) -> 'b t
val (<*>) : ( 'a -> 'b ) t -> 'a t -> 'b t