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

2 files changed, 25 insertions, 9 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 1aa8997710..84eba701ed 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -200,7 +200,8 @@ type evar_map = {
   univ_cstrs : Univ.universes;
   conv_pbs   : evar_constraint list;
   last_mods  : Evar.Set.t;
-  metas      : clbinding Metamap.t
+  metas      : clbinding Metamap.t;
+  effects    : Declareops.side_effects;
 }
 
 (*** Lifting primitive from EvarMap. ***)
@@ -361,6 +362,7 @@ let empty = {
   conv_pbs   = [];
   last_mods  = Evar.Set.empty;
   metas      = Metamap.empty;
+  effects    = Declareops.no_seff;
 }
 
 let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
@@ -463,6 +465,17 @@ let collect_evars c =
   collrec Evar.Set.empty c
 
 (**********************************************************)
+(* Side effects *)
+
+let emit_side_effects eff evd =
+  { evd with effects = Declareops.union_side_effects eff evd.effects; }
+
+let drop_side_effects evd =
+  { evd with effects = Declareops.no_seff; }
+
+let eval_side_effects evd = evd.effects
+
+(**********************************************************)
 (* Sort variables *)
 
 let new_univ_variable evd =
@@ -659,15 +672,11 @@ type open_constr = evar_map * constr
   type ['a] *)
 type 'a sigma = {
   it : 'a ;
-  eff : Declareops.side_effects;
   sigma : evar_map
 }
 
 let sig_it x = x.it
-let sig_eff x = x.eff
 let sig_sig x = x.sigma
-let emit_side_effects eff x =
-  { x with eff = Declareops.union_side_effects eff x.eff }
 
 (**********************************************************)
 (* Failure explanation *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index a5ff11c7ed..5ef243e136 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -195,6 +195,17 @@ val evar_source : existential_key -> evar_map -> Evar_kinds.t located
 (** Convenience function. Wrapper around {!find} to recover the source of an
     evar in a given evar map. *)
 
+(** {5 Side-effects} *)
+
+val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map
+(** Push a side-effect into the evar map. *)
+
+val eval_side_effects : evar_map -> Declareops.side_effects
+(** Return the effects contained in the evar map. *)
+
+val drop_side_effects : evar_map -> evar_map
+(** This should not be used. For hacking purposes. *)
+
 (** {5 Sort variables}
 
     Evar maps also keep track of the universe constraints defined at a given
@@ -212,8 +223,6 @@ val set_eq_sort : evar_map -> sorts -> sorts -> evar_map
 type 'a sigma = {
   it : 'a ;
   (** The base object. *)
-  eff : Declareops.side_effects;
-  (** Sideffects to be handled by the state machine. *)
   sigma : evar_map
   (** The added unification state. *)
 }
@@ -221,9 +230,7 @@ type 'a sigma = {
     ['a]. *)
 
 val sig_it  : 'a sigma -> 'a
-val sig_eff : 'a sigma -> Declareops.side_effects
 val sig_sig : 'a sigma -> evar_map
-val emit_side_effects : Declareops.side_effects -> 'a sigma -> 'a sigma
 
 (** {5 Meta machinery}