Adding a monotonic variant of Goal.enter and Goal.nf_enter.

2 files changed, 76 insertions, 25 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index bc2cc3e913..da9c4da9f9 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -892,17 +892,9 @@ end
 
 module UnsafeRepr = Proof.Unsafe
 
-(** {7 Notations} *)
-
-module Notations = struct
-  let (>>=) = tclBIND
-  let (<*>) = tclTHEN
-  let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
-end
-
-open Notations
-
-
+let (>>=) = tclBIND
+let (<*>) = tclTHEN
+let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
 
 (** {6 Goal-dependent tactics} *)
 
@@ -982,6 +974,43 @@ module Goal = struct
     end
     end
 
+  type 'a enter =
+    { enter : 'r. 'a t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
+
+  let s_enter f =
+    InfoL.tag (Info.Dispatch) begin
+    iter_goal begin fun goal ->
+      Env.get >>= fun env ->
+      tclEVARMAP >>= fun sigma ->
+      try
+        let gl = gmake env sigma goal in
+        let sigma = Sigma.Unsafe.of_evar_map sigma in
+        let Sigma (tac, sigma, _) = f.enter gl sigma in
+        let sigma = Sigma.to_evar_map sigma in
+        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac)
+      with e when catchable_exception e ->
+        let (e, info) = Errors.push e in
+        tclZERO ~info e
+    end
+    end
+
+  let nf_s_enter f =
+    InfoL.tag (Info.Dispatch) begin
+    iter_goal begin fun goal ->
+      Env.get >>= fun env ->
+      tclEVARMAP >>= fun sigma ->
+      try
+        let (gl, sigma) = nf_gmake env sigma goal in
+        let sigma = Sigma.Unsafe.of_evar_map sigma in
+        let Sigma (tac, sigma, _) = f.enter gl sigma in
+        let sigma = Sigma.to_evar_map sigma in
+        tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) tac)
+      with e when catchable_exception e ->
+        let (e, info) = Errors.push e in
+        tclZERO ~info e
+    end
+    end
+
   let goals =
     Env.get >>= fun env ->
     Pv.get >>= fun step ->
@@ -1218,3 +1247,13 @@ module V82 = struct
       let (e, info) = Errors.push e in tclZERO ~info e
 
 end
+
+(** {7 Notations} *)
+
+module Notations = struct
+  let (>>=) = tclBIND
+  let (<*>) = tclTHEN
+  let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
+  type 'a enter = 'a Goal.enter =
+    { enter : 'r. 'a Goal.t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
+end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 04ca01ec4d..b565589eb7 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -414,20 +414,6 @@ sig
   val make : ('a, state, state, iexn) Logic_monad.BackState.t -> 'a tactic
 end
 
-(** {7 Notations} *)
-
-module Notations : sig
-
-  (** {!tclBIND} *)
-  val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
-  (** {!tclTHEN} *)
-  val (<*>) : unit tactic -> 'a tactic -> 'a tactic
-  (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *)
-  val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
-
-end
-
-
 (** {6 Goal-dependent tactics} *)
 
 module Goal : sig
@@ -468,6 +454,17 @@ module Goal : sig
   (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
   val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
 
+  type 'a enter =
+    { enter : 'r. 'a t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
+
+  (** A variant of {!enter} allows to work with a monotonic state. The evarmap
+      returned by the argument is put back into the current state before firing
+      the returned tactic. *)
+  val s_enter : [ `LZ ] enter -> unit tactic
+
+  (** Like {!s_enter}, but normalizes the goal beforehand. *)
+  val nf_s_enter : [ `NF ] enter -> unit tactic
+
   (** Recover the list of current goals under focus, without evar-normalization *)
   val goals : [ `LZ ] t tactic list tactic
 
@@ -583,3 +580,18 @@ module V82 : sig
      the monad. *)
   val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic
 end
+
+(** {7 Notations} *)
+
+module Notations : sig
+
+  (** {!tclBIND} *)
+  val (>>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
+  (** {!tclTHEN} *)
+  val (<*>) : unit tactic -> 'a tactic -> 'a tactic
+  (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *)
+  val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
+
+  type 'a enter = 'a Goal.enter =
+    { enter : 'r. 'a Goal.t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
+end