[stm] Remove state-handling from Futures.

We make Vernacentries.interp functional wrt state, and thus remove
state-handling from `Future`. Now, a future needs a closure if it
wants to preserve state.

Consequently, `Vernacentries.interp` takes a state, and returns the
new one.

We don't explicitly thread the state in the STM yet, instead, we
recover the state that was used before and pass it explicitly to
`interp`.

I have tested the commit with the files in interactive, but we aware
that some new bugs may appear or old ones be made more apparent.
However, I am confident that this step will improve our understanding
of bugs.

In some cases, we perform a bit more summary wrapping/unwrapping. This
will go away in future commits; informal timings for a full make:

- master:
  real	2m11,027s
  user	8m30,904s
  sys	1m0,000s

- no_futures:
  real	2m8,474s
  user	8m34,380s
  sys	0m59,156s

2 files changed, 31 insertions, 120 deletions

diff --git a/lib/future.ml b/lib/future.ml
index d9463aa0f..09285ea27 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -6,12 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* To deal with side effects we have to save/restore the system state *)
-type freeze
-let freeze = ref (fun () -> assert false : unit -> freeze)
-let unfreeze = ref (fun _ -> () : freeze -> unit)
-let set_freeze f g = freeze := f; unfreeze := g
-
 let not_ready_msg = ref (fun name ->
       Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^
                 "Please wait or pass "^
@@ -30,6 +24,7 @@ let customize_not_here_msg f = not_here_msg := f
 
 exception NotReady of string
 exception NotHere of string
+
 let _ = CErrors.register_handler (function
   | NotReady name -> !not_ready_msg name
   | NotHere name -> !not_here_msg name
@@ -59,7 +54,7 @@ type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computat
 and 'a comp =
   | Delegated of (unit -> unit)
   | Closure of (unit -> 'a)
-  | Val of 'a * freeze option
+  | Val of 'a
   | Exn of Exninfo.iexn  (* Invariant: this exception is always "fixed" as in fix_exn *)
 
 and 'a comput =
@@ -74,7 +69,7 @@ let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x =
   ref (Ongoing (name, CEphemeron.create (uuid, f, Pervasives.ref x)))
 let get x =
   match !x with
-  | Finished v -> unnamed, UUID.invalid, id, ref (Val (v,None))
+  | Finished v -> unnamed, UUID.invalid, id, ref (Val v)
   | Ongoing (name, x) ->
       try let uuid, fix, c = CEphemeron.get x in name, uuid, fix, c
       with CEphemeron.InvalidKey ->
@@ -95,13 +90,13 @@ let is_exn kx = let _, _, _, x = get kx in match !x with
   | Val _ | Closure _ | Delegated _ -> false
 
 let peek_val kx = let _, _, _, x = get kx in match !x with
-  | Val (v, _) -> Some v
+  | Val v -> Some v
   | Exn _ | Closure _ | Delegated _ -> None
 
 let uuid kx = let _, id, _, _ = get kx in id
 
-let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None))
-let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ())))
+let from_val ?(fix_exn=id) v = create fix_exn (Val v)
+let from_here ?(fix_exn=id) v = create fix_exn (Val v)
 
 let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn
 
@@ -110,7 +105,7 @@ let create_delegate ?(blocking=true) ~name fix_exn =
     let _, _, fix_exn, c = get ck in
     assert (match !c with Delegated _ -> true | _ -> false);
     begin match v with
-    | `Val v -> c := Val (v, None)
+    | `Val v -> c := Val v
     | `Exn e -> c := Exn (fix_exn e)
     | `Comp f -> let _, _, _, comp = get f in c := !comp end;
     signal () in
@@ -124,17 +119,16 @@ let create_delegate ?(blocking=true) ~name fix_exn =
   ck, assignement signal ck
 
 (* TODO: get rid of try/catch to be stackless *)
-let rec compute ~pure ck : 'a value =
+let rec compute ck : 'a value =
   let _, _, fix_exn, c = get ck in
   match !c with
-  | Val (x, _) -> `Val x
+  | Val x -> `Val x
   | Exn (e, info) -> `Exn (e, info)
-  | Delegated wait -> wait (); compute ~pure ck
+  | Delegated wait -> wait (); compute ck
   | Closure f ->
       try
         let data = f () in
-        let state = if pure then None else Some (!freeze ()) in
-        c := Val (data, state); `Val data
+        c := Val data; `Val data
       with e ->
         let e = CErrors.push e in
         let e = fix_exn e in
@@ -142,60 +136,30 @@ let rec compute ~pure ck : 'a value =
         | (NotReady _, _) -> `Exn e
         | _ -> c := Exn e; `Exn e
 
-let force ~pure x = match compute ~pure x with
+let force x = match compute x with
   | `Val v -> v
   | `Exn e -> Exninfo.iraise e
 
-let chain ~pure ck f =
+let chain ck f =
   let name, uuid, fix_exn, c = get ck in
   create ~uuid ~name fix_exn (match !c with
-  | Closure _ | Delegated _ -> Closure (fun () -> f (force ~pure ck))
+  | Closure _ | Delegated _ -> Closure (fun () -> f (force ck))
   | Exn _ as x -> x
-  | Val (v, None)   when pure -> Val (f v, None)
-  | Val (v, Some _) when pure -> Val (f v, None)
-  | Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v)
-  | Val (v, None) ->
-      match !ck with
-      | Finished _ -> CErrors.anomaly(Pp.str
-          "Future.chain ~pure:false call on an already joined computation.")
-      | Ongoing _ -> CErrors.anomaly(Pp.strbrk(
-          "Future.chain ~pure:false call on a pure computation. "^
-          "This can happen if the computation was initial created with "^
-          "Future.from_val or if it was Future.chain ~pure:true with a "^
-          "function and later forced.")))
+  | Val v -> Val (f v))
 
 let create fix_exn f = create fix_exn (Closure f)
 
 let replace kx y =
   let _, _, _, x = get kx in
   match !x with
-  | Exn _ -> x := Closure (fun () -> force ~pure:false y)
+  | Exn _ -> x := Closure (fun () -> force y)
   | _ -> CErrors.anomaly
            (Pp.str "A computation can be replaced only if is_exn holds.")
 
-let purify f x =
-  let state = !freeze () in
-  try
-    let v = f x in
-    !unfreeze state;
-    v
-  with e ->
-    let e = CErrors.push e in !unfreeze state; Exninfo.iraise e
-
-let transactify f x =
-  let state = !freeze () in
-  try f x
-  with e ->
-    let e = CErrors.push e in !unfreeze state; Exninfo.iraise e
-
-let purify_future f x = if is_over x then f x else purify f x
-let compute x = purify_future (compute ~pure:false) x
-let force ~pure x = purify_future (force ~pure) x
-let chain ~pure x f =
-  let y = chain ~pure x f in
-  if is_over x then ignore(force ~pure y);
+let chain x f =
+  let y = chain x f in
+  if is_over x then ignore(force y);
   y
-let force x = force ~pure:false x
 
 let join kx =
   let v = force kx in
@@ -205,12 +169,11 @@ let join kx =
 let sink kx = if is_val kx then ignore(join kx)
 
 let split2 x =
-  chain ~pure:true x (fun x -> fst x),
-  chain ~pure:true x (fun x -> snd x)
+  chain x (fun x -> fst x), chain x (fun x -> snd x)
 
 let map2 f x l =
   CList.map_i (fun i y ->
-    let xi = chain ~pure:true x (fun x ->
+    let xi = chain x (fun x ->
         try List.nth x i
         with Failure _ | Invalid_argument _ ->
           CErrors.anomaly (Pp.str "Future.map2 length mismatch.")) in
@@ -226,6 +189,5 @@ let print f kx =
   match !x with
   | Delegated _ -> str "Delegated" ++ uid
   | Closure _ -> str "Closure" ++ uid
-  | Val (x, None) -> str "PureVal" ++ uid ++ spc () ++ hov 0 (f x)
-  | Val (x, Some _) -> str "StateVal" ++ uid ++ spc () ++ hov 0 (f x)
+  | Val x -> str "PureVal" ++ uid ++ spc () ++ hov 0 (f x)
   | Exn (e, _) -> str "Exn"  ++ uid ++ spc () ++ hov 0 (str (Printexc.to_string e))
diff --git a/lib/future.mli b/lib/future.mli
index acfce51a0..853f81cea 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -6,42 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Futures: asynchronous computations with some purity enforcing
+(* Futures: asynchronous computations.
  *
  * 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.
+ * to deal with 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
+ * One difference 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
@@ -113,27 +83,17 @@ val is_exn : 'a computation -> bool
 val peek_val : 'a computation -> 'a option
 val uuid : 'a computation -> UUID.t
 
-(* [chain pure c f] chains computation [c] with [f].
- * [chain] forces immediately the new computation if the old one is_over (Exn or Val).
- * The [pure] parameter is 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.
- *)
-val chain : pure:bool ->
-  'a computation -> ('a -> 'b) -> 'b computation
+(* [chain c f] chains computation [c] with [f].
+ * [chain] is eager, that is to say, it won't suspend the new computation
+ * if the old one is_over (Exn or Val).
+*)
+val chain : '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.
+(* Final call.
  * 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
@@ -148,19 +108,8 @@ val map2 :
   ('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.t) -> 'a computation -> Pp.t
 
-type freeze
-(* 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 -> freeze) -> (freeze -> unit) -> unit
-
 val customize_not_ready_msg : (string -> Pp.t) -> unit
 val customize_not_here_msg : (string -> Pp.t) -> unit