Merge PR #1095: [stm] Remove state handling from Futures

4 files changed, 60 insertions, 18 deletions

diff --git a/vernac/command.ml b/vernac/command.ml
index a1a87d54e0..f095a5d6cf 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 d45665dd4c..9ab89c8832 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 66427b7093..b7a8612148 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2148,23 +2148,48 @@ 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) *)
+}
+
+let s_cache = ref (States.freeze ~marshallable:`No)
+let s_proof = ref (Proof_global.freeze ~marshallable:`No)
+
+let invalidate_cache () =
+  s_cache := Obj.magic 0;
+  s_proof := Obj.magic 0
+
+let freeze_interp_state marshallable =
+  { system = (s_cache := States.freeze ~marshallable; !s_cache);
+    proof  = (s_proof := Proof_global.freeze ~marshallable; !s_proof);
+    shallow = marshallable = `Shallow }
+
+let unfreeze_interp_state { system; proof } =
+  if (!s_cache != system) then (s_cache := system; States.unfreeze system);
+  if (!s_proof != proof)  then (s_proof := proof;  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 XXX Careful here with the cache! *)
+      invalidate_cache ();
+      unfreeze_interp_state st;
       let (e, _) = CErrors.push e in
       match e with
       | HasNotFailed ->
@@ -2175,7 +2200,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 +2213,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
@@ -2227,3 +2252,8 @@ let interp ?(verbosely=true) ?proof (loc,c) =
   in
     if verbosely then Flags.verbosely (aux false) c
     else aux false c
+
+let interp ?verbosely ?proof st cmd =
+  unfreeze_interp_state st;
+  interp ?verbosely ?proof st cmd;
+  freeze_interp_state `No
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index a09011d245..56635c8011 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -14,11 +14,21 @@ val dump_global : Libnames.reference or_by_notation -> unit
 val vernac_require :
   Libnames.reference option -> bool option -> Libnames.reference list -> unit
 
+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) *)
+}
+
+val freeze_interp_state : Summary.marshallable -> interp_state
+val unfreeze_interp_state : interp_state -> unit
+
 (** The main interpretation function of vernacular expressions *)
 val interp :
   ?verbosely:bool ->
   ?proof:Proof_global.closed_proof ->
-    Vernacexpr.vernac_expr Loc.located -> unit
+  interp_state ->
+    Vernacexpr.vernac_expr Loc.located -> interp_state
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
@@ -28,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