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.

1 files changed, 19 insertions, 12 deletions

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'