Merge PR #7889: Cleanup reduction effects: they only work on constants.

4 files changed, 17 insertions, 20 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 3758008189..da6e26cc4b 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -280,8 +280,9 @@ let rec norm_head info env t stack =
   | Var id -> norm_head_ref 0 info env stack (VarKey id)
 
   | Const sp ->
-      Reductionops.reduction_effect_hook (env_of_infos info.infos) info.sigma t (lazy (reify_stack t stack));
-      norm_head_ref 0 info env stack (ConstKey sp)
+    Reductionops.reduction_effect_hook (env_of_infos info.infos) info.sigma
+      (fst sp) (lazy (reify_stack t stack));
+    norm_head_ref 0 info env stack (ConstKey sp)
 
   | LetIn (_, b, _, c) ->
       (* zeta means letin are contracted; delta without zeta means we *)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 63c7ab3c69..ba40262815 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -47,29 +47,28 @@ open Libobject
 type effect_name = string
 
 (** create a persistent set to store effect functions *)
-module ConstrMap = Map.Make (Constr)
 
 (* Table bindings a constant to an effect *)
-let constant_effect_table = Summary.ref ~name:"reduction-side-effect" ConstrMap.empty
+let constant_effect_table = Summary.ref ~name:"reduction-side-effect" Cmap.empty
 
 (* Table bindings function key to effective functions *)
 let effect_table = Summary.ref ~name:"reduction-function-effect" String.Map.empty
 
 (** a test to know whether a constant is actually the effect function *)
-let reduction_effect_hook env sigma termkey c =
+let reduction_effect_hook env sigma con c =
   try
-    let funkey = ConstrMap.find termkey !constant_effect_table in
+    let funkey = Cmap.find con !constant_effect_table in
     let effect = String.Map.find funkey !effect_table in
     effect env sigma (Lazy.force c)
   with Not_found -> ()
 
-let cache_reduction_effect (_,(termkey,funkey)) =
-  constant_effect_table := ConstrMap.add termkey funkey !constant_effect_table
+let cache_reduction_effect (_,(con,funkey)) =
+  constant_effect_table := Cmap.add con funkey !constant_effect_table
 
-let subst_reduction_effect (subst,(termkey,funkey)) =
-  (subst_mps subst termkey,funkey)
+let subst_reduction_effect (subst,(con,funkey)) =
+  (subst_constant subst con,funkey)
 
-let inReductionEffect : Constr.constr * string -> obj =
+let inReductionEffect : Constant.t * string -> obj =
   declare_object {(default_object "REDUCTION-EFFECT") with
     cache_function = cache_reduction_effect;
     open_function = (fun i o -> if Int.equal i 1 then cache_reduction_effect o);
@@ -83,8 +82,7 @@ let declare_reduction_effect funkey f =
 
 (** A function to set the value of the print function *)
 let set_reduction_effect x funkey =
-  let termkey = UnivGen.constr_of_global x in
-  Lib.add_anonymous_leaf (inReductionEffect (termkey,funkey))
+  Lib.add_anonymous_leaf (inReductionEffect (x,funkey))
 
 
 (** Machinery to custom the behavior of the reduction *)
@@ -872,7 +870,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
       | Some body -> whrec cst_l (body, stack)
       | None -> fold ())
     | Const (c,u as const) ->
-      reduction_effect_hook env sigma (EConstr.to_constr sigma x)
+      reduction_effect_hook env sigma c
          (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,stack))));
       if CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) then
        let u' = EInstance.kind sigma u in
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index b44c642d43..07eeec9276 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -41,10 +41,10 @@ val declare_reduction_effect : effect_name ->
   (Environ.env -> Evd.evar_map -> Constr.constr -> unit) -> unit
 
 (* [set_reduction_effect cst name] declares effect [name] to be called when [cst] is found *)
-val set_reduction_effect : GlobRef.t -> effect_name -> unit
+val set_reduction_effect : Constant.t -> effect_name -> unit
 
 (* [effect_hook env sigma key term] apply effect associated to [key] on [term] *)
-val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constr.constr ->
+val reduction_effect_hook : Environ.env -> Evd.evar_map -> Constant.t ->
   Constr.constr Lazy.t -> unit
 
 (** {6 Machinery about a stack of unfolded constant }
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 599a0f8162..8911a2f343 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -539,7 +539,7 @@ let reduce_mind_case_use_function func env sigma mia =
 let match_eval_ref env sigma constr stack =
   match EConstr.kind sigma constr with
   | Const (sp, u) ->
-     reduction_effect_hook env sigma (EConstr.to_constr sigma constr)
+     reduction_effect_hook env sigma sp
         (lazy (EConstr.to_constr sigma (applist (constr,stack))));
      if is_evaluable env (EvalConstRef sp) then Some (EvalConst sp, u) else None
   | Var id when is_evaluable env (EvalVarRef id) -> Some (EvalVar id, EInstance.empty)
@@ -550,7 +550,7 @@ let match_eval_ref env sigma constr stack =
 let match_eval_ref_value env sigma constr stack =
   match EConstr.kind sigma constr with
   | Const (sp, u) ->
-     reduction_effect_hook env sigma (EConstr.to_constr sigma constr)
+     reduction_effect_hook env sigma sp
         (lazy (EConstr.to_constr sigma (applist (constr,stack))));
     if is_evaluable env (EvalConstRef sp) then
       let u = EInstance.kind sigma u in
@@ -558,8 +558,6 @@ let match_eval_ref_value env sigma constr stack =
     else
       None
   | Proj (p, c) when not (Projection.unfolded p) ->
-     reduction_effect_hook env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma constr)
-        (lazy (EConstr.to_constr sigma (applist (constr,stack))));
      if is_evaluable env (EvalConstRef (Projection.constant p)) then
        Some (mkProj (Projection.unfold p, c))
      else None