Moving side effects into evar_map. There was no reason to keep another

state out of one we were threading all the way along. This should be
safer, as one cannot forego side effects accidentally by manipulating
explicitly the [sigma] container.

Still, this patch raised the issue of badly used evar maps. There
is an ad-hoc workaround (i.e. a hack) in Rewrite to handle the
fact it uses evar maps in an unorthodox way.

Likewise, that mean we have to revert all contrib patches that added
effect threading...

There was also a dubious use of side effects in their toplevel handling,
that duplicates them, leading to the need of a rather unsafe List.uniquize
afterwards. It should be investigaged.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16850 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 27 insertions, 40 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 9467d2d710..625ae74f12 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -27,7 +27,6 @@ type proofview = {
      initial : (Term.constr * Term.types) list;
      solution : Evd.evar_map;
      comb : Goal.goal list;
-     side_effects : Declareops.side_effects
      }
 
 let proofview p =
@@ -40,7 +39,6 @@ let init =
   | [] ->  { initial = [] ; 
 	     solution = Evd.empty ;
              comb = [];
-             side_effects = Declareops.no_seff
 	   }
   | (env,typ)::l -> let { initial = ret ; solution = sol ; comb = comb } =
                            aux l
@@ -52,8 +50,7 @@ let init =
 			 let gl = Goal.build e in
 			 { initial = (econstr,typ)::ret;
 			   solution = new_defs ;
-                           comb = gl::comb;
-                           side_effects = Declareops.no_seff }
+                           comb = gl::comb; }
   in
   fun l -> let v = aux l in
     (* Marks all the goal unresolvable for typeclasses. *)
@@ -69,13 +66,15 @@ let finished = function
   | _  -> false
 
 (* Returns the current value of the proofview partial proofs. *)
-let return { solution=defs; side_effects=eff } c = Evarutil.nf_evar defs c, eff
+let return { solution=defs } = defs
+
+let return_constr { solution = defs } c = Evarutil.nf_evar defs c
 
 let partial_proof pv =
-  List.map fst (List.map (return pv) (List.map fst (initial_goals pv)))
+  List.map (return_constr pv) (List.map fst (initial_goals pv))
 
 let emit_side_effects eff x =
-  { x with side_effects = Declareops.union_side_effects eff x.side_effects }
+  { x with solution = Evd.emit_side_effects eff x.solution }
 
 (* spiwack: this function should probably go in the Util section,
     but I'd rather have Util (or a separate module for lists)
@@ -366,8 +365,8 @@ let rec catchable_exception = function
    [s] to each goal successively and applying [k] to each result. *)
 let list_of_sensitive s k env step =
   Goal.list_map begin fun defs g ->
-    let (a,defs,effs) = Goal.eval s env defs g in
-    (k a) , defs, effs
+    let (a,defs) = Goal.eval s env defs g in
+    (k a) , defs
   end step.comb step.solution
 (* In form of a tactic *)
 let list_of_sensitive s k env =
@@ -376,10 +375,8 @@ let list_of_sensitive s k env =
   let (>>) = Inner.seq in
   Inner.get >>= fun step ->
   try 
-    let (tacs,defs,effs) = list_of_sensitive s k env step in
-    Inner.set { step with solution = defs;
-      side_effects = Declareops.union_side_effects step.side_effects 
-        (Declareops.flatten_side_effects effs) } >>
+    let (tacs,defs) = list_of_sensitive s k env step in
+    Inner.set { step with solution = defs; } >>
     Inner.return tacs
   with e when catchable_exception e ->
     tclZERO e env
@@ -400,23 +397,20 @@ let tclGOALBINDU s k =
 (* No backtracking can happen here, hence, as opposed to the dispatch tacticals,
     everything is done in one step. *)
 let sensitive_on_proofview s env step =
-  let wrap g ((defs, partial_list, partial_eff) as partial_res) = 
+  let wrap g ((defs, partial_list) as partial_res) = 
     match Goal.advance defs g with
     | None -> partial_res
     | Some g ->
-      let { Goal.subgoals = sg } , d', eff = Goal.eval s env defs g in
-      (d', sg::partial_list, eff::partial_eff)
+      let { Goal.subgoals = sg } , d' = Goal.eval s env defs g in
+      (d', sg::partial_list)
   in
-  let ( new_defs , combed_subgoals, side_effects ) = 
-    List.fold_right wrap step.comb (step.solution,[],[])
+  let ( new_defs , combed_subgoals ) = 
+    List.fold_right wrap step.comb (step.solution,[])
   in
   { step with
      solution = new_defs;
-     comb = List.flatten combed_subgoals;
-     side_effects =
-       Declareops.union_side_effects
-         (Declareops.flatten_side_effects side_effects) step.side_effects }
-let tclSENSITIVE s env =
+     comb = List.flatten combed_subgoals; }
+  let tclSENSITIVE s env =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Inner.bind in
   Inner.get >>= fun step ->
@@ -456,25 +450,18 @@ module V82 = struct
     try
       let tac evd gl = 
         let glsigma  =
-          tac { Evd.it = gl ; sigma = evd; eff = Declareops.no_seff }  in
+          tac { Evd.it = gl ; sigma = evd; }  in
         let sigma = glsigma.Evd.sigma in
         let g = glsigma.Evd.it in
-        ( g, sigma, glsigma.Evd.eff )
+        ( g, sigma )
       in
     (* Old style tactics expect the goals normalized with respect to evars. *)
-      let no_side_eff f x y =
-        let a, b = f x y in a, b, Declareops.no_seff in
-      let (initgoals,initevd, eff1) = 
-        Goal.list_map (no_side_eff Goal.V82.nf_evar) ps.comb ps.solution
+      let (initgoals,initevd) =
+        Goal.list_map Goal.V82.nf_evar ps.comb ps.solution
       in
-      let (goalss,evd,eff2) = Goal.list_map tac initgoals initevd in
+      let (goalss,evd) = Goal.list_map tac initgoals initevd in
       let sgs = List.flatten goalss in
-      Inner.set { ps with solution=evd ; comb=sgs; 
-        side_effects =
-          Declareops.union_side_effects ps.side_effects 
-            (Declareops.union_side_effects 
-              (Declareops.flatten_side_effects eff1)
-              (Declareops.flatten_side_effects eff2)) }
+      Inner.set { ps with solution=evd ; comb=sgs; }
     with e when catchable_exception e ->
       tclZERO e env
 
@@ -495,12 +482,12 @@ module V82 = struct
 
   (* Returns the open goals of the proofview together with the evar_map to 
      interprete them. *)
-  let goals { comb = comb ; solution = solution; side_effects=eff } =
-   { Evd.it = comb ; sigma = solution; eff=eff}
+  let goals { comb = comb ; solution = solution; } =
+   { Evd.it = comb ; sigma = solution }
 
-  let top_goals { initial=initial ; solution=solution; side_effects=eff } =
+  let top_goals { initial=initial ; solution=solution; } =
     let goals = List.map (fun (t,_) -> Goal.V82.build (fst (Term.destEvar t))) initial in
-    { Evd.it = goals ; sigma=solution; eff=eff }
+    { Evd.it = goals ; sigma=solution; }
 
   let top_evars { initial=initial } =
     let evars_of_initial (c,_) =