Split the intepretation of red_exprs in two phases.

1 files changed, 30 insertions, 16 deletions

diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index a8747e0a7c..7ed7e0f50b 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -129,6 +129,9 @@ let set_strategy local str =
 type red_expr =
     (constr, evaluable_global_reference, constr_pattern) red_expr_gen
 
+type red_expr_val =
+  (constr, evaluable_global_reference, constr_pattern, CClosure.RedFlags.reds) red_expr_gen0
+
 let make_flag_constant = function
   | EvalVarRef id -> fVAR id
   | EvalConstRef sp -> fCONST sp
@@ -221,38 +224,49 @@ let warn_simpl_unfolding_modifiers =
          (fun () ->
           Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.")
 
-let reduction_of_red_expr env =
-  let make_flag = make_flag env in
-  let rec reduction_of_red_expr = function
+let rec eval_red_expr env = function
+| Simpl (f, o) ->
+  let () =
+    if not (simplIsCbn () || List.is_empty f.rConst) then
+      warn_simpl_unfolding_modifiers () in
+  let f = if simplIsCbn () then make_flag env f else CClosure.all (* dummy *) in
+  Simpl (f, o)
+| Cbv f -> Cbv (make_flag env f)
+| Cbn f -> Cbn (make_flag env f)
+| Lazy f -> Lazy (make_flag env f)
+| ExtraRedExpr s ->
+  begin match String.Map.find s !red_expr_tab with
+  | e -> eval_red_expr env e
+  | exception Not_found -> ExtraRedExpr s (* delay to runtime interpretation *)
+  end
+| (Red _ | Hnf | Unfold _ | Fold _ | Pattern _ | CbvVm _ | CbvNative _) as e -> e
+
+let reduction_of_red_expr_val = function
   | Red internal ->
       if internal then (e_red try_red_product,DEFAULTcast)
       else (e_red red_product,DEFAULTcast)
   | Hnf -> (e_red hnf_constr,DEFAULTcast)
   | Simpl (f,o) ->
-     let whd_am = if simplIsCbn () then whd_cbn (make_flag f) else whd_simpl in
-     let am = if simplIsCbn () then strong_cbn (make_flag f) else simpl in
-     let () =
-       if not (simplIsCbn () || List.is_empty f.rConst) then
-         warn_simpl_unfolding_modifiers () in
+     let whd_am = if simplIsCbn () then whd_cbn f else whd_simpl in
+     let am = if simplIsCbn () then strong_cbn f else simpl in
      (contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
-  | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
+  | Cbv f -> (e_red (cbv_norm_flags f),DEFAULTcast)
   | Cbn f ->
-     (e_red (strong_cbn (make_flag f)), DEFAULTcast)
-  | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast)
+     (e_red (strong_cbn f), DEFAULTcast)
+  | Lazy f -> (e_red (clos_norm_flags f),DEFAULTcast)
   | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast)
   | Fold cl -> (e_red (fold_commands cl),DEFAULTcast)
   | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast)
   | ExtraRedExpr s ->
       (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast)
       with Not_found ->
-        (try reduction_of_red_expr (String.Map.find s !red_expr_tab)
-         with Not_found ->
            user_err ~hdr:"Redexpr.reduction_of_red_expr"
-             (str "unknown user-defined reduction \"" ++ str s ++ str "\"")))
+             (str "unknown user-defined reduction \"" ++ str s ++ str "\""))
   | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
   | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
-  in
-    reduction_of_red_expr
+
+let reduction_of_red_expr env r =
+  reduction_of_red_expr_val (eval_red_expr env r)
 
 let subst_mps subst c =
   EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))