Small API encapsulation inside Redexpr.

We move bind_red_expr_occurrences from Tactics to Redexpr, where it
semantically belongs. We also hide it and seal the corresponding evaluated
types.

3 files changed, 73 insertions, 67 deletions

diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index 7ed7e0f50b..9c2df71f82 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -268,6 +268,74 @@ let reduction_of_red_expr_val = function
 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_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 8350a831ca..5f3a7b689b 100644
--- a/tactics/redexpr.mli
+++ b/tactics/redexpr.mli
@@ -21,14 +21,14 @@ open Locus
 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
+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 : red_expr_val -> e_reduction_function * cast_kind
+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 :
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2a855e47af..d787b5eb30 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -634,70 +634,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 *)
@@ -963,14 +903,12 @@ let reduce redexp cl =
   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_val 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_val 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)