[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.

4 files changed, 20 insertions, 123 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 6d53349fa1..26202ef4ca 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -14,7 +14,6 @@ open Util
 open Pp
 open CAst
 open Names
-open Nameops
 open Libnames
 open Pputils
 open Ppextend
@@ -230,20 +229,6 @@ let tag_var = tag Tag.variable
     | { CAst.v = CHole (_,IntroAnonymous,_) } -> mt ()
     | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
 
-  let pr_lident {loc; v=id} =
-    match loc with
-    | None     -> pr_id id
-    | Some loc -> let (b,_) = Loc.unloc loc in
-                  pr_located pr_id (Some (Loc.make_loc (b,b + String.length (Id.to_string id))), id)
-
-  let pr_lname = function
-    | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id)
-    | x -> pr_ast Name.print x
-
-  let pr_or_var pr = function
-    | Locus.ArgArg x -> pr x
-    | Locus.ArgVar id -> pr_lident id
-
   let pr_prim_token = function
     | Numeral (n,s) -> str (if s then n else "-"^n)
     | String s -> qs s
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index e7f71849a5..1cb3aa6d7a 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -21,11 +21,6 @@ val prec_less : precedence -> tolerability -> bool
 
 val pr_tight_coma : unit -> Pp.t
 
-val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t
-
-val pr_lident : lident -> Pp.t
-val pr_lname : lname -> Pp.t
-
 val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t
 val pr_com_at : int -> Pp.t
 val pr_sep_com :
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 59e5f68f22..e6daf9544c 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -12,7 +12,6 @@ open Util
 open Pp
 open Genarg
 open Locus
-open Genredexpr
 
 let beautify_comments = ref []
 
@@ -39,91 +38,25 @@ let pr_located pr (loc, x) =
 
 let pr_ast pr { CAst.loc; v } = pr_located pr (loc, v)
 
-let pr_or_var pr = function
-  | ArgArg x -> pr x
-  | ArgVar {CAst.v=s} -> Names.Id.print s
-
-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)
+let pr_lident { CAst.loc; v=id } =
+  let open Names.Id in
+  match loc with
+  | None     -> print id
+  | Some loc -> let (b,_) = Loc.unloc loc in
+    pr_located print
+      (Some (Loc.make_loc (b,b + String.length (to_string id))), id)
 
-  | 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_lname = let open Names in function
+  | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id)
+  | x -> pr_ast Name.print x
 
-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)
+let pr_or_var pr = function
+  | ArgArg x -> pr x
+  | ArgVar id -> pr_lident id
 
-let pr_or_by_notation f = let open Constrexpr in function
-  | {CAst.loc; v=AN v} -> f v
-  | {CAst.loc; v=ByNotation (s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
+let pr_or_by_notation f = let open Constrexpr in CAst.with_val (function
+    | AN v -> f v
+    | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc)
 
 let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
 
diff --git a/printing/pputils.mli b/printing/pputils.mli
index 5b1969e232..ea554355bc 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -8,33 +8,17 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Names
 open Genarg
-open Locus
-open Genredexpr
 
 val pr_located : ('a -> Pp.t) -> 'a Loc.located -> Pp.t
 val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t
 (** Prints an object surrounded by its commented location *)
 
-val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t
+val pr_lident : lident -> Pp.t
+val pr_lname : lname -> Pp.t
+val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t
 val pr_or_by_notation : ('a -> Pp.t) -> 'a Constrexpr.or_by_notation -> Pp.t
-val pr_with_occurrences :
-  ('a -> Pp.t) -> (string -> Pp.t) -> 'a 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
 
 val pr_raw_generic : Environ.env -> rlevel generic_argument -> Pp.t
 val pr_glb_generic : Environ.env -> glevel generic_argument -> Pp.t