From 913ccc7fb4a987ddd7c591d3c7d75579dc502a95 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Dec 2018 08:07:32 +0100
Subject: [api] Move reduction modules to `tactics`

These modules do actually belong there.

We have to slightly reorganize printers, removing a couple of
duplicated ones in the way.
---
 tactics/genredexpr.ml |  79 ++++++++++++++
 tactics/ppred.ml      |  83 +++++++++++++++
 tactics/ppred.mli     |  19 ++++
 tactics/redexpr.ml    | 278 ++++++++++++++++++++++++++++++++++++++++++++++++++
 tactics/redexpr.mli   |  48 +++++++++
 tactics/redops.ml     |  64 ++++++++++++
 tactics/redops.mli    |  20 ++++
 tactics/tactics.ml    |   2 +-
 tactics/tactics.mllib |   4 +
 9 files changed, 596 insertions(+), 1 deletion(-)
 create mode 100644 tactics/genredexpr.ml
 create mode 100644 tactics/ppred.ml
 create mode 100644 tactics/ppred.mli
 create mode 100644 tactics/redexpr.ml
 create mode 100644 tactics/redexpr.mli
 create mode 100644 tactics/redops.ml
 create mode 100644 tactics/redops.mli

(limited to 'tactics')

diff --git a/tactics/genredexpr.ml b/tactics/genredexpr.ml
new file mode 100644
index 0000000000..8209684c37
--- /dev/null
+++ b/tactics/genredexpr.ml
@@ -0,0 +1,79 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Reduction expressions *)
+
+(** The parsing produces initially a list of [red_atom] *)
+
+type 'a red_atom =
+  | FBeta
+  | FMatch
+  | FFix
+  | FCofix
+  | FZeta
+  | FConst of 'a list
+  | FDeltaBut of 'a list
+
+(** This list of atoms is immediately converted to a [glob_red_flag] *)
+
+type 'a glob_red_flag = {
+  rBeta : bool;
+  rMatch : bool;
+  rFix : bool;
+  rCofix : bool;
+  rZeta : bool;
+  rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*)
+  rConst : 'a list
+}
+
+(** Generic kinds of reductions *)
+
+type ('a,'b,'c) red_expr_gen =
+  | 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
+  | Unfold of 'b Locus.with_occurrences list
+  | Fold of 'a list
+  | Pattern of 'a Locus.with_occurrences list
+  | ExtraRedExpr of string
+  | CbvVm of ('b,'c) Util.union Locus.with_occurrences option
+  | CbvNative of ('b,'c) Util.union Locus.with_occurrences option
+
+type ('a,'b,'c) may_eval =
+  | ConstrTerm of 'a
+  | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
+  | ConstrContext of Names.lident * 'a
+  | ConstrTypeOf of 'a
+
+open Libnames
+open Constrexpr
+
+type r_trm = constr_expr
+type r_pat = constr_pattern_expr
+type r_cst = qualid or_by_notation
+
+type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
+
+let make0 ?dyn name =
+  let wit = Genarg.make0 name in
+  let () = Geninterp.register_val0 wit dyn in
+  wit
+
+type 'a and_short_name = 'a * Names.lident option
+
+let wit_red_expr :
+  ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen,
+   (Genintern.glob_constr_and_expr,Names.evaluable_global_reference and_short_name Locus.or_var,Genintern.glob_constr_pattern_and_expr) red_expr_gen,
+   (EConstr.t,Names.evaluable_global_reference,Pattern.constr_pattern) red_expr_gen)
+    Genarg.genarg_type =
+  make0 "redexpr"
diff --git a/tactics/ppred.ml b/tactics/ppred.ml
new file mode 100644
index 0000000000..dd1bcd4699
--- /dev/null
+++ b/tactics/ppred.ml
@@ -0,0 +1,83 @@
+open Util
+open Pp
+open Locus
+open Genredexpr
+open Pputils
+
+let pr_with_occurrences pr keyword (occs,c) =
+  match occs with
+    | AllOccurrences ->
+      pr c
+    | NoOccurrences ->
+      failwith "pr_with_occurrences: no occurrences"
+    | OnlyOccurrences nl ->
+      hov 1 (pr c ++ spc () ++ keyword "at" ++ spc () ++
+                hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+    | AllOccurrencesBut nl ->
+      hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++
+                hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+
+exception ComplexRedFlag
+
+let pr_short_red_flag pr r =
+  if not r.rBeta ||  not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then
+    raise ComplexRedFlag
+  else if List.is_empty r.rConst then
+    if r.rDelta then mt () else raise ComplexRedFlag
+  else (if r.rDelta then str "-" else mt ()) ++
+          hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")
+
+let pr_red_flag pr r =
+  try pr_short_red_flag pr r
+  with ComplexRedFlag ->
+    (if r.rBeta then pr_arg str "beta" else mt ()) ++
+      (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else
+          (if r.rMatch then pr_arg str "match" else mt ()) ++
+          (if r.rFix then pr_arg str "fix" else mt ()) ++
+          (if r.rCofix then pr_arg str "cofix" else mt ())) ++
+      (if r.rZeta then pr_arg str "zeta" else mt ()) ++
+      (if List.is_empty r.rConst then
+          if r.rDelta then pr_arg str "delta"
+          else mt ()
+        else
+          pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
+            hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
+
+let pr_union pr1 pr2 = function
+  | Inl a -> pr1 a
+  | Inr b -> pr2 b
+
+let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function
+  | Red false -> keyword "red"
+  | Hnf -> keyword "hnf"
+  | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f)
+                    ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+  | Cbv f ->
+    if f.rBeta && f.rMatch && f.rFix && f.rCofix &&
+          f.rZeta && f.rDelta && List.is_empty f.rConst then
+      keyword "compute"
+    else
+      hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f)
+  | Lazy f ->
+    hov 1 (keyword "lazy" ++ pr_red_flag pr_ref f)
+  | Cbn f ->
+    hov 1 (keyword "cbn" ++ pr_red_flag pr_ref f)
+  | Unfold l ->
+    hov 1 (keyword "unfold" ++ spc() ++
+              prlist_with_sep pr_comma (pr_with_occurrences pr_ref keyword) l)
+  | Fold l -> hov 1 (keyword "fold" ++ prlist (pr_arg pr_constr) l)
+  | Pattern l ->
+    hov 1 (keyword "pattern" ++
+              pr_arg (prlist_with_sep pr_comma (pr_with_occurrences pr_constr keyword)) l)
+
+  | Red true ->
+    CErrors.user_err Pp.(str "Shouldn't be accessible from user.")
+  | ExtraRedExpr s ->
+    str s
+  | CbvVm o ->
+    keyword "vm_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+  | CbvNative o ->
+    keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern) keyword) o
+
+let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) =
+  pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma)
diff --git a/tactics/ppred.mli b/tactics/ppred.mli
new file mode 100644
index 0000000000..b3a306a36f
--- /dev/null
+++ b/tactics/ppred.mli
@@ -0,0 +1,19 @@
+open Genredexpr
+
+val pr_with_occurrences :
+  ('a -> Pp.t) -> (string -> Pp.t) -> 'a Locus.with_occurrences -> Pp.t
+
+val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
+val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t
+
+val pr_red_expr :
+  ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) ->
+  (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t
+
+val pr_red_expr_env : Environ.env -> Evd.evar_map ->
+  (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
+  (Environ.env -> Evd.evar_map -> 'a -> Pp.t) *
+  ('b -> Pp.t) *
+  (Environ.env -> Evd.evar_map -> 'c -> Pp.t) ->
+  (string -> Pp.t) ->
+  ('a,'b,'c) red_expr_gen -> Pp.t
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
new file mode 100644
index 0000000000..aabfae444e
--- /dev/null
+++ b/tactics/redexpr.ml
@@ -0,0 +1,278 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Util
+open Names
+open Constr
+open EConstr
+open Declarations
+open Genredexpr
+open Pattern
+open Reductionops
+open Tacred
+open CClosure
+open RedFlags
+open Libobject
+
+(* call by value normalisation function using the virtual machine *)
+let cbv_vm env sigma c =
+  if Coq_config.bytecode_compiler then
+    let ctyp = Retyping.get_type_of env sigma c in
+    Vnorm.cbv_vm env sigma c ctyp
+  else
+    compute env sigma c
+
+let warn_native_compute_disabled =
+  CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler"
+  (fun () ->
+   strbrk "native_compute disabled at configure time; falling back to vm_compute.")
+
+let cbv_native env sigma c =
+  if Coq_config.native_compiler then
+    let ctyp = Retyping.get_type_of env sigma c in
+    Nativenorm.native_norm env sigma c ctyp
+  else
+    (warn_native_compute_disabled ();
+     cbv_vm env sigma c)
+
+let whd_cbn flags env sigma t =
+  let (state,_) =
+    (whd_state_gen ~refold:true ~tactic_mode:true flags env sigma (t,Reductionops.Stack.empty))
+  in
+  Reductionops.Stack.zip ~refold:true sigma state
+
+let strong_cbn flags =
+  strong_with_flags whd_cbn flags
+
+let simplIsCbn = ref (false)
+let () = Goptions.(declare_bool_option {
+  optdepr = false;
+  optname =
+    "Plug the simpl tactic to the new cbn mechanism";
+  optkey = ["SimplIsCbn"];
+  optread = (fun () -> !simplIsCbn);
+  optwrite = (fun a -> simplIsCbn:=a);
+})
+
+let set_strategy_one ref l  =
+  let k =
+    match ref with
+      | EvalConstRef sp -> ConstKey sp
+      | EvalVarRef id -> VarKey id in
+  Global.set_strategy k l;
+  match k,l with
+      ConstKey sp, Conv_oracle.Opaque ->
+        Csymtable.set_opaque_const sp
+    | ConstKey sp, _ ->
+        let cb = Global.lookup_constant sp in
+        (match cb.const_body with
+          | OpaqueDef _ ->
+            user_err ~hdr:"set_transparent_const"
+              (str "Cannot make" ++ spc () ++
+                 Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++
+                 spc () ++ str "transparent because it was declared opaque.");
+          | _ -> Csymtable.set_transparent_const sp)
+    | _ -> ()
+
+let cache_strategy (_,str) =
+  List.iter
+    (fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql)
+    str
+
+let subst_strategy (subs,(local,obj)) =
+  local,
+  List.Smart.map
+    (fun (k,ql as entry) ->
+      let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in
+      if ql==ql' then entry else (k,ql'))
+    obj
+
+
+let map_strategy f l =
+  let l'  = List.fold_right
+    (fun (lev,ql) str ->
+      let ql' = List.fold_right
+        (fun q ql ->
+          match f q with
+              Some q' -> q' :: ql
+            | None -> ql) ql [] in
+      if List.is_empty ql' then str else (lev,ql')::str) l [] in
+  if List.is_empty l' then None else Some (false,l')
+
+let classify_strategy (local,_ as obj) =
+  if local then Dispose else Substitute obj
+
+let disch_ref ref =
+  match ref with
+      EvalConstRef c -> Some ref
+    | EvalVarRef id -> if Lib.is_in_section (GlobRef.VarRef id) then None else Some ref
+
+let discharge_strategy (_,(local,obj)) =
+  if local then None else
+  map_strategy disch_ref obj
+
+type strategy_obj =
+    bool * (Conv_oracle.level * evaluable_global_reference list) list
+
+let inStrategy : strategy_obj -> obj =
+  declare_object {(default_object "STRATEGY") with
+                    cache_function = (fun (_,obj) -> cache_strategy obj);
+                    load_function = (fun _ (_,obj) -> cache_strategy obj);
+                    subst_function = subst_strategy;
+                    discharge_function = discharge_strategy;
+                    classify_function = classify_strategy }
+
+
+let set_strategy local str =
+  Lib.add_anonymous_leaf (inStrategy (local,str))
+
+(* Generic reduction: reduction functions used in reduction tactics *)
+
+type red_expr =
+    (constr, evaluable_global_reference, constr_pattern) red_expr_gen
+
+let make_flag_constant = function
+  | EvalVarRef id -> fVAR id
+  | EvalConstRef sp -> fCONST sp
+
+let make_flag env f =
+  let red = no_red in
+  let red = if f.rBeta then red_add red fBETA else red in
+  let red = if f.rMatch then red_add red fMATCH else red in
+  let red = if f.rFix then red_add red fFIX else red in
+  let red = if f.rCofix then red_add red fCOFIX else red in
+  let red = if f.rZeta then red_add red fZETA else red in
+  let red =
+    if f.rDelta then (* All but rConst *)
+        let red = red_add red fDELTA in
+        let red = red_add_transparent red
+                    (Conv_oracle.get_transp_state (Environ.oracle env)) in
+        List.fold_right
+          (fun v red -> red_sub red (make_flag_constant v))
+          f.rConst red
+    else (* Only rConst *)
+        let red = red_add_transparent (red_add red fDELTA) TransparentState.empty in
+        List.fold_right
+          (fun v red -> red_add red (make_flag_constant v))
+          f.rConst red
+  in red
+
+(* table of custom reductino fonctions, not synchronized,
+   filled via ML calls to [declare_reduction] *)
+let reduction_tab = ref String.Map.empty
+
+(* table of custom reduction expressions, synchronized,
+   filled by command Declare Reduction *)
+let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction"
+
+let declare_reduction s f =
+  if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
+  then user_err ~hdr:"Redexpr.declare_reduction"
+    (str "There is already a reduction expression of name " ++ str s)
+  else reduction_tab := String.Map.add s f !reduction_tab
+
+let check_custom = function
+  | ExtraRedExpr s ->
+      if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab)
+      then user_err ~hdr:"Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s)
+  |_ -> ()
+
+let decl_red_expr s e =
+  if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
+  then user_err ~hdr:"Redexpr.decl_red_expr"
+    (str "There is already a reduction expression of name " ++ str s)
+  else begin
+    check_custom e;
+    red_expr_tab := String.Map.add s e !red_expr_tab
+  end
+
+let out_arg = function
+  | Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
+  | Locus.ArgArg x -> x
+
+let out_with_occurrences (occs,c) =
+  (Locusops.occurrences_map (List.map out_arg) occs, c)
+
+let e_red f env evm c = evm, f env evm c
+
+let head_style = false (* Turn to true to have a semantics where simpl
+   only reduce at the head when an evaluable reference is given, e.g.
+   2+n would just reduce to S(1+n) instead of S(S(n)) *)
+
+let contextualize f g = function
+  | Some (occs,c) ->
+      let l = Locusops.occurrences_map (List.map out_arg) occs in
+      let b,c,h = match c with
+        | Inl r -> true,PRef (global_of_evaluable_reference r),f
+        | Inr c -> false,c,f in
+      e_red (contextually b (l,c) (fun _ -> h))
+  | None -> e_red g
+
+let warn_simpl_unfolding_modifiers =
+  CWarnings.create ~name:"simpl-unfolding-modifiers" ~category:"tactics"
+         (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
+  | 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
+     (contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
+  | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
+  | Cbn f ->
+     (e_red (strong_cbn (make_flag f)), DEFAULTcast)
+  | Lazy f -> (e_red (clos_norm_flags (make_flag 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 "\"")))
+  | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
+  | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
+  in
+    reduction_of_red_expr
+
+let subst_mps subst c =
+  EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
+
+let subst_red_expr subs =
+  Redops.map_red_expr_gen
+    (subst_mps subs)
+    (Mod_subst.subst_evaluable_reference subs)
+    (Patternops.subst_pattern subs)
+
+let inReduction : bool * string * red_expr -> obj =
+  declare_object
+    {(default_object "REDUCTION") with
+       cache_function = (fun (_,(_,s,e)) -> decl_red_expr s e);
+       load_function = (fun _ (_,(_,s,e)) -> decl_red_expr s e);
+       subst_function =
+        (fun (subs,(b,s,e)) -> b,s,subst_red_expr subs e);
+       classify_function =
+        (fun ((b,_,_) as obj) -> if b then Dispose else Substitute obj) }
+
+let declare_red_expr locality s expr =
+    Lib.add_anonymous_leaf (inReduction (locality,s,expr))
diff --git a/tactics/redexpr.mli b/tactics/redexpr.mli
new file mode 100644
index 0000000000..1f65862701
--- /dev/null
+++ b/tactics/redexpr.mli
@@ -0,0 +1,48 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Interpretation layer of redexprs such as hnf, cbv, etc. *)
+
+open Names
+open Constr
+open EConstr
+open Pattern
+open Genredexpr
+open Reductionops
+open Locus
+
+type red_expr =
+    (constr, evaluable_global_reference, constr_pattern) red_expr_gen
+
+val out_with_occurrences : 'a with_occurrences -> occurrences * 'a
+
+val reduction_of_red_expr :
+  Environ.env -> red_expr -> e_reduction_function * cast_kind
+
+(** [true] if we should use the vm to verify the reduction *)
+
+(** Adding a custom reduction (function to be use at the ML level)
+   NB: the effect is permanent. *)
+val declare_reduction : string -> reduction_function -> unit
+
+(** Adding a custom reduction (function to be called a vernac command).
+   The boolean flag is the locality. *)
+val declare_red_expr : bool -> string -> red_expr -> unit
+
+(** Opaque and Transparent commands. *)
+
+(** Sets the expansion strategy of a constant. When the boolean is
+   true, the effect is non-synchronous (i.e. it does not survive
+   section and module closure). *)
+val set_strategy :
+  bool -> (Conv_oracle.level * evaluable_global_reference list) list -> unit
+
+(** call by value normalisation function using the virtual machine *)
+val cbv_vm : reduction_function
diff --git a/tactics/redops.ml b/tactics/redops.ml
new file mode 100644
index 0000000000..6f83ea9a34
--- /dev/null
+++ b/tactics/redops.ml
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Genredexpr
+
+let union_consts l1 l2 = Util.List.union Pervasives.(=) l1 l2 (* FIXME *)
+
+let make_red_flag l =
+  let rec add_flag red = function
+    | [] -> red
+    | FBeta :: lf -> add_flag { red with rBeta = true } lf
+    | FMatch :: lf -> add_flag { red with rMatch = true } lf
+    | FFix :: lf -> add_flag { red with rFix = true } lf
+    | FCofix :: lf -> add_flag { red with rCofix = true } lf
+    | FZeta :: lf -> add_flag { red with rZeta = true } lf
+    | FConst l :: lf ->
+        if red.rDelta then
+          CErrors.user_err Pp.(str
+            "Cannot set both constants to unfold and constants not to unfold");
+        add_flag { red with rConst = union_consts red.rConst l } lf
+    | FDeltaBut l :: lf ->
+        if red.rConst <> [] && not red.rDelta then
+          CErrors.user_err Pp.(str
+            "Cannot set both constants to unfold and constants not to unfold");
+        add_flag
+          { red with rConst = union_consts red.rConst l; rDelta = true }
+          lf
+  in
+  add_flag
+    {rBeta = false; rMatch = false; rFix = false; rCofix = false;
+     rZeta = false; rDelta = false; rConst = []}
+    l
+
+
+let all_flags =
+  {rBeta = true; rMatch = true; rFix = true; rCofix = true;
+   rZeta = true; rDelta = true; rConst = []}
+
+(** Mapping [red_expr_gen] *)
+
+let map_flags f flags =
+  { flags with rConst = List.map f flags.rConst }
+
+let map_occs f (occ,e) = (occ,f e)
+
+let map_red_expr_gen f g h = function
+  | Fold l -> Fold (List.map f l)
+  | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l)
+  | Simpl (flags,occs_o) ->
+     Simpl (map_flags g flags, Option.map (map_occs (Util.map_union g h)) occs_o)
+  | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l)
+  | Cbv flags -> Cbv (map_flags g flags)
+  | Lazy flags -> Lazy (map_flags g flags)
+  | CbvVm occs_o -> CbvVm (Option.map (map_occs (Util.map_union g h)) occs_o)
+  | CbvNative occs_o -> CbvNative (Option.map (map_occs (Util.map_union g h)) occs_o)
+  | Cbn flags -> Cbn (map_flags g flags)
+  | ExtraRedExpr _ | Red _ | Hnf as x -> x
diff --git a/tactics/redops.mli b/tactics/redops.mli
new file mode 100644
index 0000000000..7254f29b25
--- /dev/null
+++ b/tactics/redops.mli
@@ -0,0 +1,20 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Genredexpr
+
+val make_red_flag : 'a red_atom list -> 'a glob_red_flag
+
+val all_flags : 'a glob_red_flag
+
+(** Mapping [red_expr_gen] *)
+
+val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) ->
+  ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b3ea13cf4f..9bd4a29a69 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -889,7 +889,7 @@ let reduce redexp cl =
   let trace env sigma =
     let open Printer in
     let pr = (pr_econstr_env, pr_leconstr_env, pr_evaluable_reference, pr_constr_pattern_env) in
-    Pp.(hov 2 (Pputils.pr_red_expr_env env sigma pr str redexp))
+    Pp.(hov 2 (Ppred.pr_red_expr_env env sigma pr str redexp))
   in
   let trace () =
     let sigma, env = Pfedit.get_current_context () in
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 5afec74fae..1861c5b99b 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -6,6 +6,10 @@ Hipattern
 Ind_tables
 Eqschemes
 Elimschemes
+Genredexpr
+Redops
+Redexpr
+Ppred
 Tactics
 Abstract
 Elim
-- 
cgit v1.2.3