Added support for a side effect on constants in reduction functions.

This exports two functions:

- declare_reduction_effect: to declare a hook to be applied when some
  constant are visited during the execution of some reduction functions
  (primarily cbv, but also cbn, simpl, hnf, ...).
- set_reduction_effect: to declare a constant on which a given effect
  hook should be called.

Developed jointly by Thomas Sibut-Pinote and Hugo Herbelin.

Added support for printing effect in functions of tacred.ml.

6 files changed, 162 insertions, 39 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index bcda4ff50..631b5f5aa 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -10,6 +10,16 @@ will fail to compile now. They should switch to `Bytes.t`
 
 * ML API *
 
+Added two functions for declaring hooks to be executed in reduction
+functions when some given constants are traversed:
+
+  declare_reduction_effect: to declare a hook to be applied when some
+  constant are visited during the execution of some reduction functions
+  (primarily cbv).
+
+  set_reduction_effect: to declare a constant on which a given effect
+  hook should be called.
+
 We renamed the following functions:
 
   Context.Rel.Declaration.fold   -> Context.Rel.Declaration.fold_constr
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 077756ac7..69a5e79b4 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -187,7 +187,7 @@ val create_clos_infos :
   ?evars:(existential->constr option) -> reds -> env -> clos_infos
 val oracle_of_infos : clos_infos -> Conv_oracle.oracle
 
-val env_of_infos : clos_infos -> env
+val env_of_infos : 'a infos -> env
 
 val infos_with_reds : clos_infos -> reds -> clos_infos
 
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 782552583..6c2086f3e 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -132,6 +132,7 @@ let mkSTACK = function
   | STACK(0,v0,stk0), stk -> STACK(0,v0,stack_concat stk0 stk)
   | v,stk -> STACK(0,v,stk)
 
+type cbv_infos = { infos : cbv_value infos; sigma : Evd.evar_map }
 
 (* Change: zeta reduction cannot be avoided in CBV *)
 
@@ -189,6 +190,43 @@ let pr_key = function
   | VarKey id -> Names.Id.print id
   | RelKey n -> Pp.(str "REL_" ++ int n)
 
+let rec reify_stack t = function
+  | TOP -> t
+  | APP (args,st) ->
+      reify_stack (mkApp(t,Array.map reify_value args)) st
+  | CASE (ty,br,ci,env,st) ->
+      reify_stack
+        (mkCase (ci, ty, t,br))
+        st
+  | PROJ (p, pinfo, st) ->
+       reify_stack (mkProj (p, t)) st
+
+and reify_value = function (* reduction under binders *)
+  | VAL (n,t) -> lift n t
+  | STACK (0,v,stk) ->
+      reify_stack (reify_value v) stk
+  | STACK (n,v,stk) ->
+      lift n (reify_stack (reify_value v) stk)
+  | CBN(t,env) ->
+    t
+      (* map_constr_with_binders subs_lift (cbv_norm_term) env t *)
+  | LAM (n,ctxt,b,env) ->
+      List.fold_left (fun c (n,t)  -> Term.mkLambda (n, t, c)) b ctxt
+  | FIXP ((lij,(names,lty,bds)),env,args) ->
+      mkApp
+        (mkFix (lij,
+		(names,
+		 lty,
+		 bds)),
+         Array.map reify_value args)
+  | COFIXP ((j,(names,lty,bds)),env,args) ->
+      mkApp
+        (mkCoFix (j,
+		  (names,lty,bds)),
+         Array.map reify_value args)
+  | CONSTR (c,args) ->
+      mkApp(mkConstructU c, Array.map reify_value args)
+
 (* The main recursive functions
  *
  * Go under applications and cases/projections (pushed in the stack), 
@@ -213,12 +251,12 @@ let rec norm_head info env t stack =
   
   | Proj (p, c) -> 
     let p' =
-      if red_set (info_flags info) (fCONST (Projection.constant p)) 
-      	&& red_set (info_flags info) fBETA 
+      if red_set (info_flags info.infos) (fCONST (Projection.constant p)) 
+      	&& red_set (info_flags info.infos) fBETA 
       then Projection.unfold p
       else p
     in 
-    let pinfo = Environ.lookup_projection p (info_env info) in
+    let pinfo = Environ.lookup_projection p (info_env info.infos) in
       norm_head info env c (PROJ (p', pinfo, stack))
 	
   (* constants, axioms
@@ -233,14 +271,16 @@ let rec norm_head info env t stack =
 
   | Var id -> norm_head_ref 0 info env stack (VarKey id)
 
-  | Const sp -> norm_head_ref 0 info env stack (ConstKey sp)
+  | 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)
 
   | LetIn (_, b, _, c) ->
       (* zeta means letin are contracted; delta without zeta means we *)
       (* allow bindings but leave let's in place *)
-      if red_set (info_flags info) fZETA then
+      if red_set (info_flags info.infos) fZETA then
         (* New rule: for Cbv, Delta does not apply to locally bound variables
-           or red_set (info_flags info) fDELTA
+           or red_set (info_flags info.infos) fDELTA
          *)
 	let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in
         norm_head info env' c stack
@@ -248,7 +288,7 @@ let rec norm_head info env t stack =
 	(CBN(t,env), stack) (* Should we consider a commutative cut ? *)
 
   | Evar ev ->
-      (match evar_value info.i_cache ev with
+      (match evar_value info.infos.i_cache ev with
           Some c -> norm_head info env c stack
         | None -> (VAL(0, t), stack))
 
@@ -265,8 +305,8 @@ let rec norm_head info env t stack =
   | Prod _ -> (CBN(t,env), stack)
 
 and norm_head_ref k info env stack normt =
-  if red_set_ref (info_flags info) normt then
-    match ref_value_cache info normt with
+  if red_set_ref (info_flags info.infos) normt then
+    match ref_value_cache info.infos normt with
       | Some body ->
          if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt);
          strip_appl (shift_value k body) stack
@@ -291,7 +331,7 @@ and cbv_stack_term info stack env t =
 and cbv_stack_value info env = function
   (* a lambda meets an application -> BETA *)
   | (LAM (nlams,ctxt,b,env), APP (args, stk))
-      when red_set (info_flags info) fBETA ->
+      when red_set (info_flags info.infos) fBETA ->
     let nargs = Array.length args in
       if nargs == nlams then
           cbv_stack_term info stk (subs_cons(args,env)) b
@@ -305,31 +345,31 @@ and cbv_stack_value info env = function
 
     (* a Fix applied enough -> IOTA *)
     | (FIXP(fix,env,[||]), stk)
-        when fixp_reducible (info_flags info) fix stk ->
+        when fixp_reducible (info_flags info.infos) fix stk ->
         let (envf,redfix) = contract_fixp env fix in
         cbv_stack_term info stk envf redfix
 
     (* constructor guard satisfied or Cofix in a Case -> IOTA *)
     | (COFIXP(cofix,env,[||]), stk)
-        when cofixp_reducible (info_flags info) cofix stk->
+        when cofixp_reducible (info_flags info.infos) cofix stk->
         let (envf,redfix) = contract_cofixp env cofix in
         cbv_stack_term info stk envf redfix
 
     (* constructor in a Case -> IOTA *)
     | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,ci,env,stk)))
-            when red_set (info_flags info) fMATCH ->
+            when red_set (info_flags info.infos) fMATCH ->
 	let cargs =
           Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in
         cbv_stack_term info (stack_app cargs stk) env br.(n-1)
 
     (* constructor of arity 0 in a Case -> IOTA *)
     | (CONSTR(((_,n),u),[||]), CASE(_,br,_,env,stk))
-            when red_set (info_flags info) fMATCH ->
+            when red_set (info_flags info.infos) fMATCH ->
                     cbv_stack_term info stk env br.(n-1)
 
     (* constructor in a Projection -> IOTA *)
     | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk)))
-        when red_set (info_flags info) fMATCH && Projection.unfolded p ->
+        when red_set (info_flags info.infos) fMATCH && Projection.unfolded p ->
       let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in
 	cbv_stack_value info env (strip_appl arg stk)
 
@@ -337,7 +377,7 @@ and cbv_stack_value info env = function
     | (FIXP(fix,env,[||]), APP(appl,TOP)) -> FIXP(fix,env,appl)
     | (COFIXP(cofix,env,[||]), APP(appl,TOP)) -> COFIXP(cofix,env,appl)
     | (CONSTR(c,[||]), APP(appl,TOP)) -> CONSTR(c,appl)
-      
+
     (* definitely a value *)
     | (head,stk) -> mkSTACK(head, stk)
 
@@ -400,12 +440,11 @@ let cbv_norm infos constr =
   let constr = EConstr.Unsafe.to_constr constr in
   EConstr.of_constr (with_stats (lazy (cbv_norm_term infos (subs_id 0) constr)))
 
-type cbv_infos = cbv_value infos
-
 (* constant bodies are normalized at the first expansion *)
 let create_cbv_infos flgs env sigma =
-  create
-    (fun old_info c -> cbv_stack_term old_info TOP (subs_id 0) c)
+  let infos = create
+    (fun old_info c -> cbv_stack_term { infos = old_info; sigma } TOP (subs_id 0) c)
     flgs
     env
-    (Reductionops.safe_evar_value sigma)
+    (Reductionops.safe_evar_value sigma) in
+  { infos; sigma }
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 5a2328aaa..463a8bda4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -40,6 +40,54 @@ let _ = Goptions.declare_bool_option {
 let get_refolding_in_reduction () = !refolding_in_reduction
 let set_refolding_in_reduction = (:=) refolding_in_reduction
 
+(** Support for reduction effects *)
+
+open Mod_subst
+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
+
+(* 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 =
+  try
+    let funkey = ConstrMap.find termkey !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 subst_reduction_effect (subst,(termkey,funkey)) =
+  (subst_mps subst termkey,funkey)
+
+let inReductionEffect : Constr.constr * 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);
+    subst_function = subst_reduction_effect;
+    classify_function = (fun o -> Substitute o) }
+
+let declare_reduction_effect funkey f =
+  if String.Map.mem funkey !effect_table then
+    CErrors.anomaly Pp.(str "Cannot redeclare effect function " ++ qstring funkey ++ str ".");
+  effect_table := String.Map.add funkey f !effect_table
+
+(** A function to set the value of the print function *)
+let set_reduction_effect x funkey =
+  let termkey = Universes.constr_of_global x in
+  Lib.add_anonymous_leaf (inReductionEffect (termkey,funkey))
+
+
 (** Machinery to custom the behavior of the reduction *)
 module ReductionBehaviour = struct
   open Globnames
@@ -859,9 +907,12 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
       (match safe_meta_value sigma ev with
       | Some body -> whrec cst_l (EConstr.of_constr body, stack)
       | None -> fold ())
-    | Const (c,u as const) when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) ->
-        let u' = EInstance.kind sigma u in
-       (match constant_opt_value_in env (fst const, u') with
+    | Const (c,u as const) ->
+      reduction_effect_hook env sigma (EConstr.to_constr sigma x)
+         (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
+       (match constant_opt_value_in env (c, u') with
 	| None -> fold ()
 	| Some body ->
           let body = EConstr.of_constr body in
@@ -901,7 +952,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 		    | Some (bef,arg,s') ->
 		      whrec Cst_stack.empty 
 			(arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s')
-       )
+       ) else fold ()
     | Proj (p, c) when CClosure.RedFlags.red_projection flags p ->
       (let pb = lookup_projection p env in
        let kn = Projection.constant p in
@@ -1035,7 +1086,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
 	|_ -> fold ()
       else fold ()
 
-    | Rel _ | Var _ | Const _ | LetIn _ | Proj _ -> fold ()
+    | Rel _ | Var _ | LetIn _ | Proj _ -> fold ()
     | Sort _ | Ind _ | Prod _ -> fold ()
   in
   fun xs ->
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index af8048156..944f3b568 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -34,6 +34,22 @@ end
 val get_refolding_in_reduction : unit -> bool
 val set_refolding_in_reduction : bool -> unit
 
+(** {6 Support for reduction effects } *)
+
+type effect_name = string
+
+(* [declare_reduction_effect name f] declares [f] under key [name];
+   [name] must be a unique in "world". *)
+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 : Globnames.global_reference -> 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 ->
+  Constr.constr Lazy.t -> unit
+
 (** {6 Machinery about a stack of unfolded constant }
 
     cst applied to params must convertible to term of the state applied to args
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 3d41d2ddd..be7148509 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -538,20 +538,27 @@ let reduce_mind_case_use_function func env sigma mia =
     | _ -> assert false
 
 
-let match_eval_ref env sigma constr = 
+let match_eval_ref env sigma constr stack =
   match EConstr.kind sigma constr with
-  | Const (sp, u) when is_evaluable env (EvalConstRef sp) ->
-      Some (EvalConst sp, u)
+  | Const (sp, u) ->
+     reduction_effect_hook env sigma (EConstr.to_constr sigma constr)
+        (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)
   | Rel i -> Some (EvalRel i, EInstance.empty)
   | Evar ev -> Some (EvalEvar ev, EInstance.empty)
   | _ -> None
 
-let match_eval_ref_value env sigma constr = 
+let match_eval_ref_value env sigma constr stack =
   match EConstr.kind sigma constr with
-  | Const (sp, u) when is_evaluable env (EvalConstRef sp) ->
-    let u = EInstance.kind sigma u in
-    Some (EConstr.of_constr (constant_value_in env (sp, u)))
+  | Const (sp, u) ->
+     reduction_effect_hook env sigma (EConstr.to_constr sigma constr)
+        (lazy (EConstr.to_constr sigma (applist (constr,stack))));
+    if is_evaluable env (EvalConstRef sp) then
+      let u = EInstance.kind sigma u in
+      Some (EConstr.of_constr (constant_value_in env (sp, u)))
+    else
+      None
   | Var id when is_evaluable env (EvalVarRef id) -> 
      env |> lookup_named id |> NamedDecl.get_value
   | Rel n ->
@@ -561,7 +568,7 @@ let match_eval_ref_value env sigma constr =
 let special_red_case env sigma whfun (ci, p, c, lf) =
   let rec redrec s =
     let (constr, cargs) = whfun s in
-    match match_eval_ref env sigma constr with
+    match match_eval_ref env sigma constr cargs with
     | Some (ref, u) ->
       (match reference_opt_value env sigma ref u with
       | None -> raise Redelimination
@@ -776,7 +783,7 @@ and whd_simpl_stack env sigma =
 	 with Redelimination -> s')
 	  
       | _ -> 
-        match match_eval_ref env sigma x with
+        match match_eval_ref env sigma x stack with
 	| Some (ref, u) ->
           (try
 	     let sapp, nocase = red_elim_const env sigma ref u stack in
@@ -798,7 +805,7 @@ and whd_simpl_stack env sigma =
 and whd_construct_stack env sigma s =
   let (constr, cargs as s') = whd_simpl_stack env sigma s in
   if reducible_mind_case sigma constr then s'
-  else match match_eval_ref env sigma constr with
+  else match match_eval_ref env sigma constr cargs with
   | Some (ref, u) ->
     (match reference_opt_value env sigma ref u with
     | None -> raise Redelimination
@@ -846,7 +853,7 @@ let try_red_product env sigma c =
 	  | Reduced s -> simpfun (applist s)
 	  | NotReducible -> raise Redelimination)
       | _ -> 
-        (match match_eval_ref env sigma x with
+        (match match_eval_ref env sigma x [] with
         | Some (ref, u) ->
           (* TO DO: re-fold fixpoints after expansion *)
           (* to get true one-step reductions *)
@@ -927,7 +934,7 @@ let whd_simpl_stack =
 let whd_simpl_orelse_delta_but_fix env sigma c =
   let rec redrec s =
     let (constr, stack as s') = whd_simpl_stack env sigma s in
-    match match_eval_ref_value env sigma constr with
+    match match_eval_ref_value env sigma constr stack with
     | Some c ->
       (match EConstr.kind sigma (snd (decompose_lam sigma c)) with
       | CoFix _ | Fix _ -> s'