Future library to represent pure computations

Since the whole system is imperative, futures are run protecting
the global state, and the final state is also saved to let the user
freely chain futures.

Futures can represent local (lazy) computations or remote ones
(delegated).  Delegating a future lets a third party assign its
value at some poit in the future; in the meanwhile accessing the
future value raises an exception.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16669 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 201 insertions, 0 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index c3d3ce709..37ee00517 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -35,6 +35,8 @@ Rtree
 Heap
 Dnet
 Genarg
+Stateid
+Future
 
 Names
 Univ
@@ -49,6 +51,7 @@ Cbytecodes
 Copcodes
 Cemitcodes
 Nativevalues
+Future
 Lazyconstr
 Declareops
 Retroknowledge
diff --git a/lib/future.ml b/lib/future.ml
new file mode 100644
index 000000000..b1b960718
--- /dev/null
+++ b/lib/future.ml
@@ -0,0 +1,136 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* to avoid side effects *)
+let freeze = ref (fun () -> assert false : unit -> Dyn.t)
+let unfreeze = ref (fun _ -> () : Dyn.t -> unit)
+let set_freeze f g = freeze := f; unfreeze := g
+
+exception NotReady
+exception NotHere
+let _ = Errors.register_handler (function
+  | NotReady ->
+      Pp.strbrk("The value you are asking for is not ready yet. " ^
+                "Please wait or pass "^
+                "the \"-coq-slaves off\" option to CoqIDE to disable"^
+                "asynchronous script processing.")
+  | NotHere ->
+      Pp.strbrk("The value you are asking for is not available "^
+                "in this process. If you really need this, pass "^
+                "the \"-coq-slaves off\" option to CoqIDE to disable"^
+                "asynchronous script processing.")
+  | _ -> raise Errors.Unhandled)
+
+(* Val is not necessarily a final state, so the
+   computation restarts from the state stocked into Val *)
+type 'a comp =
+  | Closure of (unit -> 'a)
+  | Val of 'a * Dyn.t option
+  | Exn of exn
+  | Delegated
+  | Dropped
+
+type 'a computation = 'a comp ref
+
+type 'a value = [ `Val of 'a | `Exn of exn ]
+
+let is_over x = match !x with
+  | Val _ | Exn _ -> true
+  | Closure _ | Delegated | Dropped -> false
+
+let is_val x = match !x with
+  | Val _ -> true
+  | Exn _ | Closure _ | Delegated | Dropped -> false
+
+let peek_val x = match !x with
+  | Val (v, _) -> Some v
+  | Exn _ | Closure _ | Delegated | Dropped -> None
+
+let from_val v = ref (Val (v, None))
+let from_here v = ref (Val (v, Some (!freeze ())))
+let proj = function
+  | `Val (x, _ ) -> `Val x
+  | `Exn e -> `Exn e
+
+let create f = ref (Closure f)
+
+let create_delegate () =
+  let c = ref Delegated in
+  c, (function `Val v -> c := Val (v, None) | `Exn e -> c := Exn e)
+
+(* TODO: get rid of try/catch *)
+let compute ~pure c : 'a value = match !c with
+  | Val (x, _) -> `Val x
+  | Exn e -> `Exn e
+  | Delegated -> `Exn NotReady
+  | Dropped -> `Exn NotHere
+  | Closure f ->
+      try
+        let data = f () in
+        let state = if pure then None else Some (!freeze ()) in
+        c := Val (data, state); `Val data
+      with
+      | NotReady as e -> let e = Errors.push e in `Exn e
+      | e -> let e = Errors.push e in c := Exn e; `Exn e
+
+let force ~pure x = match compute ~pure x with
+  | `Val v -> v
+  | `Exn e -> raise e
+
+let drop c = match !c with Closure _ | Val (_,Some _) -> ref Dropped | _ -> c
+
+let chain ?(id="none") ?(pure=false) c f = ref (match !c with
+  | Closure _ | Delegated | Dropped -> Closure (fun () -> f (force ~pure c))
+  | Exn _ as x -> x
+  | Val (v, None) -> Closure (fun () -> f v)
+  | Val (v, Some _) when pure ->  Closure (fun () -> f v)
+  | Val (v, Some state) ->
+       prerr_endline ("Future: restarting (check if optimizable): " ^ id);
+       Closure (fun () -> !unfreeze state; f v))
+
+let create_here f = chain ~pure:false (from_here ()) f
+
+let purify f x =
+  let state = !freeze () in
+  try
+    let v = f x in
+    !unfreeze state;
+    v
+  with e -> let e = Errors.push e in !unfreeze state; raise e
+
+let purify_future f x =
+  match !x with
+  | Val _ | Exn _ | Delegated | Dropped -> f x
+  | Closure _ -> purify f x
+
+let compute x = purify_future (compute ~pure:false) x
+let force x = purify_future (force ~pure:false) x
+
+let join x =
+  let v = force x in
+  (x := match !x with
+       | Val (x,_) -> Val (x, None)
+       | Exn _ | Delegated | Dropped | Closure _ -> assert false);
+  v
+
+let split2 x =
+  chain ~pure:true x (fun x -> fst x),
+  chain ~pure:true x (fun x -> snd x)
+
+let split3 x =
+  chain ~pure:true x (fun x -> Util.pi1 x),
+  chain ~pure:true x (fun x -> Util.pi2 x),
+  chain ~pure:true x (fun x -> Util.pi3 x)
+
+let map2 f x l =
+  CList.map_i (fun i y ->
+    let xi = chain ~pure:true x (fun x ->
+        try List.nth x i
+        with Failure _ | Invalid_argument _ ->
+          Errors.anomaly (Pp.str "Future.map2 length mismatch")) in
+    f xi y) 0 l
diff --git a/lib/future.mli b/lib/future.mli
new file mode 100644
index 000000000..3da0e2fdc
--- /dev/null
+++ b/lib/future.mli
@@ -0,0 +1,61 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Futures: for now lazy computations with some purity enforcing *)
+(* TODO: it may be worth separating in the type pure and inpure computations *)
+
+exception NotReady
+
+type 'a computation
+type 'a value = [ `Val of 'a | `Exn of exn ]
+
+(* Build a computation *)
+val create : (unit -> 'a) -> 'a computation
+val from_val : 'a -> 'a computation
+
+(* Run remotely, returns the function to assign *)
+val create_delegate : unit -> 'a computation * ('a value -> unit)
+
+(* Variants to stock a copy of the current environment *)
+val create_here : (unit -> 'a) -> 'a computation
+val from_here : 'a -> 'a computation
+
+(* Inspect a computation *)
+val is_over : 'a computation -> bool
+val is_val : 'a computation -> bool
+val peek_val : 'a computation -> 'a option
+
+(* Chain computations.
+   Note that in [chain c f], f will execute in an environment modified by c
+   unless ~pure:true *)
+val chain :
+  ?id:string -> ?pure:bool -> 'a computation -> ('a -> 'b) -> 'b computation
+
+(* Forcing a computation *)
+val force : 'a computation -> 'a
+val compute : 'a computation -> 'a value
+
+val drop : 'a computation -> 'a computation
+
+(* Final call, no more impure chain allowed since the state is lost *)
+val join : 'a computation -> 'a
+
+(* Utility *)
+val split2 : ('a * 'b) computation -> 'a computation * 'b computation
+val split3 :
+  ('a * 'b * 'c) computation -> 'a computation * 'b computation * 'c computation
+val map2 :
+  ('a computation -> 'b -> 'c) ->
+     'a list computation -> 'b list -> 'c list
+
+(* These functions are needed to get rid of side effects *)
+val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit
+
+(* Once set_freeze is called we can purify a computation *)
+val purify : ('a -> 'b) -> 'a -> 'b
+
diff --git a/lib/lib.mllib b/lib/lib.mllib
index f28b49a4f..fec18486f 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -17,3 +17,4 @@ Heap
 Dnet
 Unionfind
 Genarg
+Future