Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.

6 files changed, 16 insertions, 17 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 67893e3b78..ae4b2e3363 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -555,6 +555,12 @@ let tclEVARMAP =
 
 let tclENV = Proof.current
 
+let tclEFFECTS eff =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  Proof.get >>= fun initial ->
+  Proof.set (emit_side_effects eff initial)
+
 exception Timeout
 let _ = Errors.register_handler begin function
   | Timeout -> Errors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 7be8f6003b..409bbb76a1 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -234,6 +234,9 @@ val tclEVARMAP : Evd.evar_map tactic
    environment is returned by {!Proofview.Goal.env}. *)
 val tclENV : Environ.env tactic
 
+(* [tclEFFECTS eff] add the effects [eff] to the current state. *)
+val tclEFFECTS : Declareops.side_effects -> unit tactic
+
 (* Shelves all the goals under focus. The goals are placed on the
    shelf for later use (or being solved by side-effects). *)
 val shelve : unit tactic
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 85546619e3..d7f0dd83f4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -343,7 +343,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d
   let type_of_cls = type_of_clause cls gl in
   let dep = dep_proof_ok && dep_fun c type_of_cls in
   let (elim,effs) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
-  Proofview.V82.tactic (Tactics.emit_side_effects effs) <*>
+  Proofview.tclEFFECTS effs <*>
   general_elim_clause with_evars frzevars tac cls c t l
     (match lft2rgt with None -> false | Some b -> b)
     {elimindex = None; elimbody = (elim,NoBindings)}
@@ -861,7 +861,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
   let pf_ty = mkArrow eqn absurd_term in
   let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
   let pf = clenv_value_cast_meta absurd_clause in
-  Proofview.V82.tactic (Tactics.emit_side_effects eff) <*>
+  Proofview.tclEFFECTS eff <*>
   tclTHENS (cut_intro absurd_term)
     [onLastHypId gen_absurdity; (Proofview.V82.tactic (refine pf))]
 
@@ -1231,9 +1231,8 @@ let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) =
     let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
       ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
     let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
-    let sigma = Evd.emit_side_effects eff (Proofview.Goal.sigma gl) in
       (* cut with the good equality and prove the requested goal *)
-    tclTHENS (tclTHEN (Proofview.V82.tclEVARS sigma) (cut (mkApp (ceq,new_eq_args))))
+    tclTHENS (tclTHEN (Proofview.tclEFFECTS eff) (cut (mkApp (ceq,new_eq_args))))
       [tclIDTAC; tclTHEN (Proofview.V82.tactic (apply (
         mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
        ))) (Auto.trivial [] [])
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1f88ed6453..aeac5e2642 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3879,12 +3879,6 @@ let unify ?(state=full_transparent_state) x y gl =
     in tclEVARS evd gl
   with e when Errors.noncritical e -> tclFAIL 0 (str"Not unifiable") gl
 
-let emit_side_effects eff gl =
-(* Declareops.iter_side_effects (fun e ->
-    prerr_endline ("emitting: " ^ Declareops.string_of_side_effect e))
-    eff; *)
-  { it = [gl.it] ; sigma = Evd.emit_side_effects eff gl.sigma; }
-
 module Simple = struct
   (** Simplified version of some of the above tactics *)
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 9f4f0e9ce1..671343b128 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -394,8 +394,6 @@ val declare_intro_decomp_eq :
    (types * constr * constr) ->
    clausenv -> unit Proofview.tactic) -> unit
 
-val emit_side_effects : Declareops.side_effects -> tactic
-
 module Simple : sig
   (** Simplified version of some of the above tactics *)
 
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 94447f0d04..253d218988 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -378,7 +378,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
                        then lb_type_of_p else mkApp (lb_type_of_p,lb_args)
            in
            Tacticals.New.tclTHENLIST [
-             Proofview.V82.tactic (Tactics.emit_side_effects eff);
+             Proofview.tclEFFECTS eff;
              Equality.replace p q ; Proofview.V82.tactic (apply app) ; Auto.default_auto]
   end
 
@@ -448,7 +448,7 @@ let do_replace_bl bl_scheme_key ind aavoid narg lft rgt =
                            then bl_t1 else mkApp (bl_t1,bl_args)
                 in
                 Tacticals.New.tclTHENLIST [
-                  Proofview.V82.tactic (Tactics.emit_side_effects eff) ;
+                  Proofview.tclEFFECTS eff;
                   Equality.replace_by t1 t2
                     (Tacticals.New.tclTHEN (Proofview.V82.tactic (apply app)) (Auto.default_auto)) ;
                   aux q1 q2 ]
@@ -861,10 +861,9 @@ let compute_dec_tact ind lnamesparrec nparrec =
       Proofview.tclZERO (UserError ("",str"Error during the decidability part, leibniz to boolean"++
         str" equality is required."))
   end >>= fun (lbI,eff'') ->
+  let eff = (Declareops.union_side_effects eff'' (Declareops.union_side_effects eff' eff)) in
   Tacticals.New.tclTHENLIST [
-        Proofview.V82.tactic (Tactics.emit_side_effects
-          (Declareops.union_side_effects eff''
-            (Declareops.union_side_effects eff' eff)));
+        Proofview.tclEFFECTS eff;
         intros_using fresh_first_intros;
         intros_using [freshn;freshm];
 	(*we do this so we don't have to prove the same goal twice *)