diff options
| -rw-r--r-- | dev/printers.mllib | 3 | ||||
| -rw-r--r-- | lib/future.ml | 136 | ||||
| -rw-r--r-- | lib/future.mli | 61 | ||||
| -rw-r--r-- | lib/lib.mllib | 1 |
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 |