[plugins] Prepare plugin API for functional handling of state.

To this purpose we allow plugins to register functions that will
modify the state.

This is not used yet, but will be used soon when we remove the global
handling of the proof state.

7 files changed, 79 insertions, 51 deletions

diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 850902d6b..8673155e2 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -15,6 +15,7 @@ Command
 Classes
 Record
 Assumptions
+Vernacstate
 Vernacinterp
 Mltop
 Topfmt
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5bcb3b1e1..a71794f5e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1909,7 +1909,7 @@ let vernac_load interp fname =
  * is the outdated/deprecated "Local" attribute of some vernacular commands
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
-let interp ?proof ?loc locality poly c =
+let interp ?proof ?loc locality poly st c =
   vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c);
   match c with
   (* The below vernac are candidates for removal from the main type
@@ -2069,7 +2069,10 @@ let interp ?proof ?loc locality poly c =
   | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
 
   (* Extensions *)
-  | VernacExtend (opn,args) -> Vernacinterp.call ?locality ?loc (opn,args)
+  | VernacExtend (opn,args) ->
+    (* XXX: Here we are returning the state! :) *)
+    let _st : Vernacstate.t = Vernacinterp.call ?locality ?loc (opn,args) st in
+    ()
 
 (* Vernaculars that take a locality flag *)
 let check_vernac_supports_locality c l =
@@ -2147,28 +2150,6 @@ let locate_if_not_already ?loc (e, info) =
 exception HasNotFailed
 exception HasFailed of Pp.t
 
-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 =
@@ -2187,8 +2168,8 @@ let with_fail st b f =
                             (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;
+      Vernacstate.invalidate_cache ();
+      Vernacstate.unfreeze_interp_state st;
       let (e, _) = CErrors.push e in
       match e with
       | HasNotFailed ->
@@ -2230,8 +2211,8 @@ let interp ?(verbosely=true) ?proof st (loc,c) =
         try
           vernac_timeout begin fun () ->
           if verbosely
-            then Flags.verbosely (interp ?proof ?loc locality poly) c
-            else Flags.silently  (interp ?proof ?loc locality poly) c;
+            then Flags.verbosely (interp ?proof ?loc locality poly st) c
+            else Flags.silently  (interp ?proof ?loc locality poly st) c;
           if orig_program_mode || not !Flags.program_mode || isprogcmd then
             Flags.program_mode := orig_program_mode;
 	  ignore (Flags.use_polymorphic_flag ())
@@ -2252,7 +2233,9 @@ let interp ?(verbosely=true) ?proof st (loc,c) =
     if verbosely then Flags.verbosely (aux false) c
     else aux false c
 
+(* XXX: There is a bug here in case of an exception, see @gares
+   comments on the PR *)
 let interp ?verbosely ?proof st cmd =
-  unfreeze_interp_state st;
+  Vernacstate.unfreeze_interp_state st;
   interp ?verbosely ?proof st cmd;
-  freeze_interp_state `No
+  Vernacstate.freeze_interp_state `No
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 56635c801..67001bc24 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -14,21 +14,11 @@ 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 ->
-  interp_state ->
-    Vernacexpr.vernac_expr Loc.located -> interp_state
+  Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> Vernacstate.t
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
@@ -40,7 +30,7 @@ val make_cases : string -> string list list
 
 (* 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 with_fail : Vernacstate.t -> bool -> (unit -> unit) -> unit
 
 val command_focus : unit Proof.focus_kind
 
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index d2687161a..1d024386e 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -11,7 +11,8 @@ open Pp
 open CErrors
 
 type deprecation = bool
-type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit
+type vernac_command = Genarg.raw_generic_argument list -> Loc.t option ->
+  Vernacstate.t -> Vernacstate.t
 
 (* Table of vernac entries *)
 let vernac_tab =
@@ -66,8 +67,9 @@ let call ?locality ?loc (opn,converted_args) =
     let hunk = callback converted_args in
     phase := "Executing command";
     Locality.LocalityFixme.set locality;
-    hunk loc;
-    Locality.LocalityFixme.assert_consumed()
+    let res = hunk loc in
+    Locality.LocalityFixme.assert_consumed ();
+    res
   with
     | Drop -> raise Drop
     | reraise ->
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 84370fdc2..1c66b1c04 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -9,12 +9,16 @@
 (** Interpretation of extended vernac phrases. *)
 
 type deprecation = bool
-type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit
 
-val vinterp_add : deprecation -> Vernacexpr.extend_name ->
-  vernac_command -> unit
-val overwriting_vinterp_add :
-  Vernacexpr.extend_name -> vernac_command -> unit
+type vernac_command = Genarg.raw_generic_argument list -> Loc.t option ->
+  Vernacstate.t -> Vernacstate.t
+
+val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit
+
+val overwriting_vinterp_add : Vernacexpr.extend_name -> vernac_command -> unit
 
 val vinterp_init : unit -> unit
-val call : ?locality:bool -> ?loc:Loc.t -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit
+
+val call : ?locality:bool -> ?loc:Loc.t ->
+  Vernacexpr.extend_name * Genarg.raw_generic_argument list ->
+  Vernacstate.t -> Vernacstate.t
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
new file mode 100644
index 000000000..9802a03ca
--- /dev/null
+++ b/vernac/vernacstate.ml
@@ -0,0 +1,29 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type t = { (* 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)
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
new file mode 100644
index 000000000..63a5b3b1e
--- /dev/null
+++ b/vernac/vernacstate.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type t = { (* 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 -> t
+val unfreeze_interp_state : t -> unit
+
+(* WARNING: Do not use, it will go away in future releases *)
+val invalidate_cache : unit -> unit