Moving printing code for red_expr and may_eval to Pptactic.

4 files changed, 87 insertions, 90 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 69fc30864..4f510f250 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -727,86 +727,6 @@ end) = struct
 
   let pr_binders = pr_undelimited_binders spc (pr ltop)
 
-  let pr_with_occurrences pr (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))
-
-  let pr_red_flag pr r =
-    (if r.rBeta then pr_arg str "beta" else mt ()) ++
-      (if r.rIota then pr_arg str "iota" 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_metaid id = str"?" ++ pr_id id
-
-  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) = function
-    | Red false -> keyword "red"
-    | Hnf -> keyword "hnf"
-    | Simpl o -> keyword "simpl" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
-    | Cbv f ->
-      if f.rBeta && f.rIota && 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) 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)) l)
-
-    | Red true ->
-      error "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)) o
-    | CbvNative o ->
-      keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
-
-  let pr_may_eval test prc prlc pr2 pr3 = function
-    | ConstrEval (r,c) ->
-      hov 0
-        (keyword "eval" ++ brk (1,1) ++
-           pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++
-           keyword "in" ++ spc() ++ prc c)
-    | ConstrContext ((_,id),c) ->
-      hov 0
-        (keyword "context" ++ spc () ++ pr_id id ++ spc () ++
-           str "[" ++ prlc c ++ str "]")
-    | ConstrTypeOf c ->
-      hov 1 (keyword "type of" ++ spc() ++ prc c)
-    | ConstrTerm c when test c ->
-      h 0 (str "(" ++ prc c ++ str ")")
-    | ConstrTerm c ->
-      prc c
-
-  let pr_may_eval a =
-    pr_may_eval (fun _ -> false) a
-
 end
 
 module Tag =
diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli
index 7ac650c98..04415e746 100644
--- a/printing/ppconstrsig.mli
+++ b/printing/ppconstrsig.mli
@@ -30,7 +30,6 @@ module type Pp = sig
   val pr_tight_coma : unit -> std_ppcmds
 
   val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
-  val pr_metaid : Id.t -> std_ppcmds
 
   val pr_lident : Id.t located -> std_ppcmds
   val pr_lname : Name.t located -> std_ppcmds
@@ -47,15 +46,6 @@ module type Pp = sig
   val pr_qualid : qualid -> std_ppcmds
   val pr_patvar : patvar -> std_ppcmds
 
-  val pr_with_occurrences :
-    ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds
-  val pr_red_expr :
-    ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
-    ('a,'b,'c) red_expr_gen -> std_ppcmds
-  val pr_may_eval :
-    ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
-    ('c -> std_ppcmds) -> ('a,'b,'c) may_eval -> std_ppcmds
-
   val pr_glob_sort : glob_sort -> std_ppcmds
   val pr_guard_annot : (constr_expr -> std_ppcmds) ->
     local_binder list ->
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 520905db9..6790be3c6 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -100,6 +100,84 @@ module Make
 
   let keyword x = tag_keyword (str x)
 
+  let pr_with_occurrences pr (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))
+
+  let pr_red_flag pr r =
+    (if r.rBeta then pr_arg str "beta" else mt ()) ++
+      (if r.rIota then pr_arg str "iota" 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) = function
+    | Red false -> keyword "red"
+    | Hnf -> keyword "hnf"
+    | Simpl o -> keyword "simpl" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
+    | Cbv f ->
+      if f.rBeta && f.rIota && 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) 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)) l)
+
+    | Red true ->
+      error "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)) o
+    | CbvNative o ->
+      keyword "native_compute" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
+
+  let pr_may_eval test prc prlc pr2 pr3 = function
+    | ConstrEval (r,c) ->
+      hov 0
+        (keyword "eval" ++ brk (1,1) ++
+           pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++
+           keyword "in" ++ spc() ++ prc c)
+    | ConstrContext ((_,id),c) ->
+      hov 0
+        (keyword "context" ++ spc () ++ pr_id id ++ spc () ++
+           str "[" ++ prlc c ++ str "]")
+    | ConstrTypeOf c ->
+      hov 1 (keyword "type of" ++ spc() ++ prc c)
+    | ConstrTerm c when test c ->
+      h 0 (str "(" ++ prc c ++ str ")")
+    | ConstrTerm c ->
+      prc c
+
+  let pr_may_eval a =
+    pr_may_eval (fun _ -> false) a
+
   let pr_arg pr x = spc () ++ pr x
 
   let pr_or_var pr = function
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index 355055e6d..712158288 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -18,6 +18,15 @@ open Misctypes
 
 module type Pp = sig
 
+  val pr_with_occurrences :
+    ('a -> std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds
+  val pr_red_expr :
+    ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
+    ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds
+  val pr_may_eval :
+    ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+    ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds
+
   val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
   val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
   val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds