Fix bug #5116: [Print Ltac] should be able to print strategies.

3 files changed, 48 insertions, 2 deletions

diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index 82b79c883..28078efd6 100644
--- a/ltac/g_rewrite.ml4
+++ b/ltac/g_rewrite.ml4
@@ -63,8 +63,17 @@ let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c
 let subst_strategy s str = str
 
 let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
-let pr_raw_strategy _ _ _ (s : raw_strategy) = Pp.str "<strategy>"
-let pr_glob_strategy _ _ _ (s : glob_strategy) = Pp.str "<strategy>"
+let pr_raw_strategy prc prlc _ (s : raw_strategy) =
+  let prr = Pptactic.pr_red_expr (prc, prlc, Pptactic.pr_or_by_notation Libnames.pr_reference, prc) in
+  Rewrite.pr_strategy prc prr s
+let pr_glob_strategy prc prlc _ (s : glob_strategy) =
+  let prr = Pptactic.pr_red_expr
+    (Ppconstr.pr_constr_expr,
+    Ppconstr.pr_lconstr_expr,
+    Pptactic.pr_or_by_notation Libnames.pr_reference,
+    Ppconstr.pr_constr_expr)
+  in
+  Rewrite.pr_strategy prc prr s
 
 ARGUMENT EXTEND rewstrategy
     PRINTED BY pr_strategy
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 69f45e1ae..4d7c5d0e4 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1700,6 +1700,40 @@ let rec map_strategy (f : 'a -> 'a2) (g : 'b -> 'b2) : ('a,'b) strategy_ast -> (
   | StratEval r -> StratEval (g r)
   | StratFold c -> StratFold (f c)
 
+let pr_ustrategy = function
+| Subterms -> str "subterms"
+| Subterm -> str "subterm"
+| Innermost -> str "innermost"
+| Outermost -> str "outermost"
+| Bottomup -> str "bottomup"
+| Topdown -> str "topdown"
+| Progress -> str "progress"
+| Try -> str "try"
+| Any -> str "any"
+| Repeat -> str "repeat"
+
+let paren p = str "(" ++ p ++ str ")"
+
+let rec pr_strategy prc prr = function
+| StratId -> str "id"
+| StratFail -> str "fail"
+| StratRefl -> str "refl"
+| StratUnary (s, str) ->
+  pr_ustrategy s ++ spc () ++ paren (pr_strategy prc prr str)
+| StratBinary (Choice, str1, str2) ->
+  str "choice" ++ spc () ++ paren (pr_strategy prc prr str1) ++ spc () ++
+    paren (pr_strategy prc prr str2)
+| StratBinary (Compose, str1, str2) ->
+  pr_strategy prc prr str1 ++ str ";" ++ spc () ++ pr_strategy prc prr str2
+| StratConstr (c, true) -> prc c
+| StratConstr (c, false) -> str "<-" ++ spc () ++ prc c
+| StratTerms cl -> str "terms" ++ spc () ++ pr_sequence prc cl
+| StratHints (old, id) ->
+  let cmd = if old then "old_hints" else "hints" in
+  str cmd ++ spc () ++ str id
+| StratEval r -> str "eval" ++ spc () ++ prr r
+| StratFold c -> str "fold" ++ spc () ++ prc c
+
 let rec strategy_of_ast = function
   | StratId -> Strategies.id
   | StratFail -> Strategies.fail
diff --git a/ltac/rewrite.mli b/ltac/rewrite.mli
index f448c8543..35c448351 100644
--- a/ltac/rewrite.mli
+++ b/ltac/rewrite.mli
@@ -62,6 +62,9 @@ val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strat
 val map_strategy : ('a -> 'b) -> ('c -> 'd) ->
   ('a, 'c) strategy_ast -> ('b, 'd) strategy_ast
 
+val pr_strategy : ('a -> Pp.std_ppcmds) -> ('b -> Pp.std_ppcmds) ->
+  ('a, 'b) strategy_ast -> Pp.std_ppcmds
+
 (** Entry point for user-level "rewrite_strat" *)
 val cl_rewrite_clause_strat : strategy -> Id.t option -> unit Proofview.tactic