[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

1 files changed, 22 insertions, 60 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))