[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

4 files changed, 41 insertions, 35 deletions

diff --git a/vernac/command.ml b/vernac/command.ml
index a1a87d54e..f095a5d6c 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -79,7 +79,7 @@ let red_constant_entry n ce sigma = function
         let (_, c) = redfun env sigma c in
         EConstr.Unsafe.to_constr c
       in
-      { ce with const_entry_body = Future.chain ~pure:true proof_out
+      { ce with const_entry_body = Future.chain proof_out
         (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) }
 
 let warn_implicits_in_term =
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index d45665dd4..9ab89c883 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -60,7 +60,7 @@ let adjust_guardness_conditions const = function
   (* Try all combinations... not optimal *)
      let env = Global.env() in
      { const with const_entry_body =
-        Future.chain ~pure:true const.const_entry_body
+        Future.chain const.const_entry_body
         (fun ((body, ctx), eff) ->
           match kind_of_term body with
           | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 7f2985aca..13b6eafc2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2148,23 +2148,42 @@ let locate_if_not_already ?loc (e, info) =
 exception HasNotFailed
 exception HasFailed of Pp.t
 
-let with_fail b f =
-  if not b then f ()
+type interp_state = { (* TODO: inline records in OCaml 4.03 *)
+  system  : States.state;        (* summary + libstack *)
+  proof   : Proof_global.state;  (* proof state *)
+  shallow : bool                 (* is the state trimmed down (libstack) *)
+}
+
+(* Unfortunately we cannot cache here due to some bits in the STM not
+   being fully pure. *)
+let freeze_interp_state marshallable =
+  { system = States.freeze ~marshallable;
+    proof = Proof_global.freeze ~marshallable;
+    shallow = marshallable = `Shallow }
+
+let unfreeze_interp_state { system; proof } =
+  States.unfreeze system;
+  Proof_global.unfreeze proof
+
+(* XXX STATE: this type hints that restoring the state should be the
+   caller's responsibility *)
+let with_fail st b f =
+  if not b
+  then f ()
   else begin try
       (* If the command actually works, ignore its effects on the state.
        * Note that error has to be printed in the right state, hence
        * within the purified function *)
-      Future.purify
-        (fun v ->
-           try f v; raise HasNotFailed
-           with
-           | HasNotFailed as e -> raise e
-           | e ->
-              let e = CErrors.push e in
-              raise (HasFailed (CErrors.iprint
-                (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))))
-        ()
+      try f (); raise HasNotFailed
+      with
+      | HasNotFailed as e -> raise e
+      | e ->
+        let e = CErrors.push e in
+        raise (HasFailed (CErrors.iprint
+                            (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e)))
     with e when CErrors.noncritical e ->
+      (* Restore the previous state *)
+      unfreeze_interp_state st;
       let (e, _) = CErrors.push e in
       match e with
       | HasNotFailed ->
@@ -2175,7 +2194,7 @@ let with_fail b f =
       | _ -> assert false
   end
 
-let interp ?(verbosely=true) ?proof (loc,c) =
+let interp ?(verbosely=true) ?proof st (loc,c) =
   let orig_program_mode = Flags.is_program_mode () in
   let rec aux ?locality ?polymorphism isprogcmd = function
 
@@ -2188,7 +2207,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
     | VernacPolymorphic (b, c) -> user_err Pp.(str "Polymorphism specified twice")
     | VernacLocal _ -> user_err Pp.(str "Locality specified twice")
     | VernacFail v ->
-        with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v)
+        with_fail st true (fun () -> aux ?locality ?polymorphism isprogcmd v)
     | VernacTimeout (n,v) ->
         current_timeout := Some n;
         aux ?locality ?polymorphism isprogcmd v
@@ -2228,21 +2247,7 @@ let interp ?(verbosely=true) ?proof (loc,c) =
     if verbosely then Flags.verbosely (aux false) c
     else aux false c
 
-type interp_state = { (* TODO: inline records in OCaml 4.03 *)
-  system  : States.state;        (* summary + libstack *)
-  proof   : Proof_global.state;  (* proof state *)
-  shallow : bool                 (* is the state trimmed down (libstack) *)
-}
-
-let freeze_interp_state marshallable =
-  { system = States.freeze ~marshallable;
-    proof = Proof_global.freeze ~marshallable;
-    shallow = (marshallable = `Shallow) }
-
-let unfreeze_interp_state { system; proof } =
-  States.unfreeze system; Proof_global.unfreeze proof
-
-let _dummy_interp_state = { system = Obj.magic 0; proof = Obj.magic 0; shallow = false }
-
 let interp ?verbosely ?proof st cmd =
-  interp ?verbosely ?proof cmd; st
+  unfreeze_interp_state st;
+  interp ?verbosely ?proof st cmd;
+  freeze_interp_state `No
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 5559e6b81..56635c801 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -22,7 +22,6 @@ type interp_state = { (* TODO: inline records in OCaml 4.03 *)
 
 val freeze_interp_state : Summary.marshallable -> interp_state
 val unfreeze_interp_state : interp_state -> unit
-val _dummy_interp_state : interp_state
 
 (** The main interpretation function of vernacular expressions *)
 val interp :
@@ -39,7 +38,9 @@ val interp :
 
 val make_cases : string -> string list list
 
-val with_fail : bool -> (unit -> unit) -> unit
+(* XXX STATE: this type hints that restoring the state should be the
+   caller's responsibility *)
+val with_fail : interp_state -> bool -> (unit -> unit) -> unit
 
 val command_focus : unit Proof.focus_kind