Module Imandra_thread_util.Fut

Concurrent Futures

Our notion of concurrency is organized around 'aFut.t, which is a value that will resolve into a 'a in the future. This is (mostly) monadic and applicative, and the use of "let operators" should make it reasonably ergonomic.

The notion of 'aFut.t is shared, but most combinators are in the functor Fut.Make which depends on an executor (to specify where the combinator code runs).

type backtrace = Stdlib.Printexc.raw_backtrace
type exn_with_bt_opt = exn * backtrace option
type 'a listener
type 'a fut_state = private
| Fut_wait of {
mutable listen : 'a listener list;
}
| Fut_done of 'a
| Fut_exn of exn * backtrace option
module type S0 = sig ... end
include S0
type 'a t

The type of futures values of type 'a

val pp : 'a CCFormat.printer -> 'a t CCFormat.printer
val state : 'a t -> 'a fut_state
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 -> backtrace -> 'a t

Future that just contains a failure and backtrace

val fail_with_bt_opt : exn -> 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, 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, 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
module type EXECUTOR = sig ... end
module type S = sig ... end
module Make (_ : EXECUTOR) : S
val unwrap_ : ( 'a, exn_with_bt_opt ) Stdlib.result -> 'a

Unwrap result by raising in case of error