Imported Upstream version 8.5~beta1+dfsg

1 files changed, 162 insertions, 0 deletions

diff --git a/lib/future.mli b/lib/future.mli
new file mode 100644
index 00000000..8a4fa0bd
--- /dev/null
+++ b/lib/future.mli
@@ -0,0 +1,162 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Futures: asynchronous computations with some purity enforcing
+ *
+ * A Future.computation is like a lazy_t but with some extra bells and whistles
+ * to deal with imperative code and eventual delegation to a slave process.
+ *
+ * Example of a simple scenario taken into account:
+ *
+ *   let f = Future.from_here (number_of_constants (Global.env())) in
+ *   let g = Future.chain ~pure:false f (fun n ->
+ *             n = number_of_constants (Global.env())) in
+ *   ...
+ *   Lemmas.save_named ...;
+ *   ...
+ *   let b = Future.force g in
+ *
+ * The Future.computation f holds a (immediate, no lazy here) value.
+ * We then chain to obtain g that (will) hold false if (when it will be
+ * run) the global environment has a different number of constants, true
+ * if nothing changed.
+ * Before forcing g, we add to the global environment one more constant.
+ * When finally we force g.  Its value is going to be *true*.
+ * This because Future.from_here stores in the computation not only the initial
+ * value but the entire system state.  When g is forced the state is restored,
+ * hence Global.env() returns the environment that was actual when f was
+ * created.
+ * Last, forcing g is run protecting the system state, hence when g finishes,
+ * the actual system state is restored.
+ *
+ * If you compare this with lazy_t, you see that the value returned is *false*,
+ * that is counter intuitive and error prone.
+ *
+ * Still not all computations are impure and access/alter the system state.
+ * This class can be optimized by using ~pure:true, but there is no way to
+ * statically check if this flag is misused, hence use it with care.
+ *
+ * Other differences with lazy_t is that a future computation that produces
+ * and exception can be substituted for another computation of the same type.
+ * Moreover a future computation can be delegated to another execution entity
+ * that will be allowed to set the result.  Finally future computations can
+ * always be marshalled: if they were joined before marshalling, they will
+ * hold the computed value (assuming it is itself marshallable), otherwise
+ * they will become invalid and accessing them raises a private exception.
+ *)
+
+(* Each computation has a unique id that is inherited by each offspring
+ * computation (chain, split, map...).  Joined computations lose it.  *)
+module UUID : sig
+  type t
+  val invalid : t
+
+  val compare : t -> t -> int
+  val equal : t -> t -> bool
+end
+
+module UUIDMap : Map.S with type key = UUID.t
+module UUIDSet : Set.S with type elt = UUID.t
+
+exception NotReady
+
+type 'a computation
+type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn ]
+type fix_exn = Exninfo.iexn -> Exninfo.iexn
+
+(* Build a computation, no snapshot of the global state is taken.  If you need
+   to grab a copy of the state start with from_here () and then chain.
+   fix_exn is used to enrich any exception raised
+   by forcing the computations or any computation that is chained after
+   it. It is used by STM to attach errors to their corresponding states,
+   and to communicate to the code catching the exception a valid state id. *)
+val create : fix_exn -> (unit -> 'a) -> 'a computation
+
+(* Usually from_val is used to create "fake" futures, to use the same API
+   as if a real asynchronous computations was there.  In this case fixing
+   the exception is not needed, but *if* the future is chained, the fix_exn
+   argument should really be given *)
+val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation
+
+(* Like from_val, but also takes a snapshot of the global state.  Morally
+   the value is not just the 'a but also the global system state *)
+val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation
+
+(* To get the fix_exn of a computation and build a Tacexpr.declaration_hook.
+ * When a future enters the environment a corresponding hook is run to perform
+ * some work.  If this fails, then its failure has to be annotated with the
+ * same state id that corresponds to the future computation end.  I.e. Qed
+ * is split into two parts, the lazy one (the future) and the eagher one
+ * (the hook), both performing some computations for the same state id. *)
+val fix_exn_of : 'a computation -> fix_exn
+
+(* Run remotely, returns the function to assign.
+   If not blocking (the default) it raises NotReady if forced before the
+   delage assigns it. *)
+type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
+val create_delegate :
+  ?blocking:bool -> fix_exn -> 'a computation * ('a assignement -> unit)
+
+(* Given a computation that is_exn, replace it by another one *)
+val replace : 'a computation -> 'a computation -> unit
+
+(* Inspect a computation *)
+val is_over : 'a computation -> bool
+val is_val : 'a computation -> bool
+val is_exn : 'a computation -> bool
+val peek_val : 'a computation -> 'a option
+val uuid : 'a computation -> UUID.t
+
+(* [chain greedy pure c f] chains computation [c] with [f].
+ * The [greedy] and [pure] parameters are tricky:
+ * [pure]:
+ *   When pure is true, the returned computation will not keep a copy
+ *   of the global state.
+ *   [let c' = chain ~pure:true c f in let c'' = chain ~pure:false c' g in]
+ *   is invalid.  It works if one forces [c''] since the whole computation
+ *   will be executed in one go.  It will not work, and raise an anomaly, if
+ *   one forces c' and then c''.
+ *   [join c; chain ~pure:false c g] is invalid and fails at runtime.
+ *   [force c; chain ~pure:false c g] is correct.
+ * [greedy]:
+ *   The [greedy] parameter forces immediately the new computation if
+ *   the old one is_over (Exn or Val). Defaults to true. *)
+val chain : ?greedy:bool -> pure:bool ->
+  'a computation -> ('a -> 'b) -> 'b computation
+
+(* Forcing a computation *)
+val force : 'a computation -> 'a
+val compute : 'a computation -> 'a value
+
+(* Final call, no more *inpure* chain allowed since the state is lost.
+ * Also the fix_exn function is lost, hence error reporting can be incomplete
+ * in a computation obtained by chaining on a joined future. *)
+val join : 'a computation -> 'a
+
+(* Call this before stocking the future.  If it is_val then it is joined *)
+val sink : 'a computation -> unit
+
+(*** Utility functions ************************************************* ***)
+val split2 : ?greedy:bool ->
+  ('a * 'b) computation -> 'a computation * 'b computation
+val map2 : ?greedy:bool ->
+  ('a computation -> 'b -> 'c) ->
+     'a list computation -> 'b list -> 'c list
+
+(* Once set_freeze is called we can purify a computation *)
+val purify : ('a -> 'b) -> 'a -> 'b
+(* And also let a function alter the state but backtrack if it raises exn *)
+val transactify : ('a -> 'b) -> 'a -> 'b
+
+(** Debug: print a computation given an inner printing function. *)
+val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds
+
+(* These functions are needed to get rid of side effects.
+   Thy are set for the outermos layer of the system, since they have to
+   deal with the whole system state. *)
+val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit