Merge PR #13609: Extrude the computation of redexp flags in reduce.

Reviewed-by: herbelin

4 files changed, 117 insertions, 85 deletions

diff --git a/tactics/genredexpr.ml b/tactics/genredexpr.ml
index 1f6b04c1d3..9939490e79 100644
--- a/tactics/genredexpr.ml
+++ b/tactics/genredexpr.ml
@@ -35,13 +35,13 @@ type 'a glob_red_flag = {
 
 (** Generic kinds of reductions *)
 
-type ('a,'b,'c) red_expr_gen =
+type ('a, 'b, 'c, 'flags) red_expr_gen0 =
   | Red of bool
   | Hnf
-  | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option
-  | Cbv of 'b glob_red_flag
-  | Cbn of 'b glob_red_flag
-  | Lazy of 'b glob_red_flag
+  | Simpl of 'flags * ('b, 'c) Util.union Locus.with_occurrences option
+  | Cbv of 'flags
+  | Cbn of 'flags
+  | Lazy of 'flags
   | Unfold of 'b Locus.with_occurrences list
   | Fold of 'a list
   | Pattern of 'a Locus.with_occurrences list
@@ -49,6 +49,9 @@ type ('a,'b,'c) red_expr_gen =
   | CbvVm of ('b,'c) Util.union Locus.with_occurrences option
   | CbvNative of ('b,'c) Util.union Locus.with_occurrences option
 
+type ('a, 'b, 'c) red_expr_gen =
+  ('a, 'b, 'c, 'b glob_red_flag) red_expr_gen0
+
 type ('a,'b,'c) may_eval =
   | ConstrTerm of 'a
   | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index a8747e0a7c..9c2df71f82 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,117 @@ 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)
+
+let reduction_of_red_expr env r =
+  reduction_of_red_expr_val (eval_red_expr env r)
+
+(* Possibly equip a reduction with the occurrences mentioned in an
+   occurrence clause *)
+
+let error_illegal_clause () =
+  CErrors.user_err Pp.(str "\"at\" clause not supported in presence of an occurrence clause.")
+
+let error_illegal_non_atomic_clause () =
+  CErrors.user_err Pp.(str "\"at\" clause not supported in presence of a non atomic \"in\" clause.")
+
+let error_occurrences_not_unsupported () =
+  CErrors.user_err Pp.(str "Occurrences not supported for this reduction tactic.")
+
+let bind_red_expr_occurrences occs nbcl redexp =
+  let open Locus in
+  let has_at_clause = function
+    | Unfold l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
+    | Pattern l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
+    | Simpl (_,Some (occl,_)) -> occl != AllOccurrences
+    | _ -> false in
+  if occs == AllOccurrences then
+    if nbcl > 1 && has_at_clause redexp then
+      error_illegal_non_atomic_clause ()
+    else
+      redexp
+  else
+    match redexp with
+    | Unfold (_::_::_) ->
+        error_illegal_clause ()
+    | Unfold [(occl,c)] ->
+        if occl != AllOccurrences then
+          error_illegal_clause ()
+        else
+          Unfold [(occs,c)]
+    | Pattern (_::_::_) ->
+        error_illegal_clause ()
+    | Pattern [(occl,c)] ->
+        if occl != AllOccurrences then
+          error_illegal_clause ()
+        else
+          Pattern [(occs,c)]
+    | Simpl (f,Some (occl,c)) ->
+        if occl != AllOccurrences then
+          error_illegal_clause ()
+        else
+          Simpl (f,Some (occs,c))
+    | CbvVm (Some (occl,c)) ->
+        if occl != AllOccurrences then
+          error_illegal_clause ()
+        else
+          CbvVm (Some (occs,c))
+    | CbvNative (Some (occl,c)) ->
+        if occl != AllOccurrences then
+          error_illegal_clause ()
+        else
+          CbvNative (Some (occs,c))
+    | Red _ | Hnf | Cbv _ | Lazy _ | Cbn _
+    | ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None ->
+        error_occurrences_not_unsupported ()
+    | Unfold [] | Pattern [] ->
+        assert false
+
+let reduction_of_red_expr_val ?occs r =
+  let r = match occs with
+  | None -> r
+  | Some (occs, nbcl) -> bind_red_expr_occurrences occs nbcl r
   in
-    reduction_of_red_expr
+  reduction_of_red_expr_val r
 
 let subst_mps subst c =
   EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
diff --git a/tactics/redexpr.mli b/tactics/redexpr.mli
index d43785218f..5f3a7b689b 100644
--- a/tactics/redexpr.mli
+++ b/tactics/redexpr.mli
@@ -19,10 +19,18 @@ open Reductionops
 open Locus
 
 type red_expr =
-    (constr, evaluable_global_reference, constr_pattern) red_expr_gen
+  (constr, evaluable_global_reference, constr_pattern) red_expr_gen
+
+type red_expr_val
 
 val out_with_occurrences : 'a with_occurrences -> occurrences * 'a
 
+val eval_red_expr : Environ.env -> red_expr -> red_expr_val
+
+val reduction_of_red_expr_val : ?occs:(Locus.occurrences_expr * int) ->
+  red_expr_val -> e_reduction_function * cast_kind
+
+(** Composition of {!reduction_of_red_expr_val} with {!eval_red_expr} *)
 val reduction_of_red_expr :
   Environ.env -> red_expr -> e_reduction_function * cast_kind
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 528fa65d5a..130e0e97c2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -616,70 +616,10 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where env sigma dec
       in
       (sigma, LocalDef (id,b',ty'))
 
-(* Possibly equip a reduction with the occurrences mentioned in an
-   occurrence clause *)
-
-let error_illegal_clause () =
-  error "\"at\" clause not supported in presence of an occurrence clause."
-
-let error_illegal_non_atomic_clause () =
-  error "\"at\" clause not supported in presence of a non atomic \"in\" clause."
-
-let error_occurrences_not_unsupported () =
-  error "Occurrences not supported for this reduction tactic."
-
 let bind_change_occurrences occs = function
   | None -> None
   | Some c -> Some (Redexpr.out_with_occurrences (occs,c))
 
-let bind_red_expr_occurrences occs nbcl redexp =
-  let has_at_clause = function
-    | Unfold l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
-    | Pattern l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
-    | Simpl (_,Some (occl,_)) -> occl != AllOccurrences
-    | _ -> false in
-  if occs == AllOccurrences then
-    if nbcl > 1 && has_at_clause redexp then
-      error_illegal_non_atomic_clause ()
-    else
-      redexp
-  else
-    match redexp with
-    | Unfold (_::_::_) ->
-        error_illegal_clause ()
-    | Unfold [(occl,c)] ->
-        if occl != AllOccurrences then
-          error_illegal_clause ()
-        else
-          Unfold [(occs,c)]
-    | Pattern (_::_::_) ->
-        error_illegal_clause ()
-    | Pattern [(occl,c)] ->
-        if occl != AllOccurrences then
-          error_illegal_clause ()
-        else
-          Pattern [(occs,c)]
-    | Simpl (f,Some (occl,c)) ->
-        if occl != AllOccurrences then
-          error_illegal_clause ()
-        else
-          Simpl (f,Some (occs,c))
-    | CbvVm (Some (occl,c)) ->
-        if occl != AllOccurrences then
-          error_illegal_clause ()
-        else
-          CbvVm (Some (occs,c))
-    | CbvNative (Some (occl,c)) ->
-        if occl != AllOccurrences then
-          error_illegal_clause ()
-        else
-          CbvNative (Some (occs,c))
-    | Red _ | Hnf | Cbv _ | Lazy _ | Cbn _
-    | ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None ->
-        error_occurrences_not_unsupported ()
-    | Unfold [] | Pattern [] ->
-        assert false
-
 (* The following two tactics apply an arbitrary
    reduction function either to the conclusion or to a
    certain hypothesis *)
@@ -941,17 +881,16 @@ let reduce redexp cl =
   | Red _ | Hnf | CbvVm _ | CbvNative _ -> StableHypConv
   | ExtraRedExpr _ -> StableHypConv (* Should we be that lenient ?*)
   in
+  let redexp = Redexpr.eval_red_expr env redexp in
   begin match cl.concl_occs with
   | NoOccurrences -> Proofview.tclUNIT ()
   | occs ->
-    let redexp = bind_red_expr_occurrences occs nbcl redexp in
-    let redfun = Redexpr.reduction_of_red_expr env redexp in
+    let redfun = Redexpr.reduction_of_red_expr_val ~occs:(occs, nbcl) redexp in
     e_change_in_concl ~check (revert_cast redfun)
   end
   <*>
   let f (id, occs, where) =
-    let redexp = bind_red_expr_occurrences occs nbcl redexp in
-    let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in
+    let (redfun, _) = Redexpr.reduction_of_red_expr_val ~occs:(occs, nbcl) redexp in
     let redfun _ env sigma c = redfun env sigma c in
     let redfun env sigma d = e_pf_change_decl redfun where env sigma d in
     (id, redfun)