feat(library/tactic): add trace_state_tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/tactic/tactic.cpp

@@ -74,6 +74,16 @@ tactic trace_tactic(char const * msg) {
     return trace_tactic(std::string(msg));
 }
 
+tactic trace_state_tactic() {
+    return mk_tactic1([=](environment const &, io_state const & io, proof_state const & s) -> proof_state {
+            options opts = io.get_options();
+            format fmt   = s.pp(io.get_formatter(), opts);
+            io.get_diagnostic_channel() << mk_pair(fmt, opts) << "\n";
+            io.get_diagnostic_channel().get_stream().flush();
+            return s;
+        });
+}
+
 tactic suppress_trace(tactic const & t) {
     return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq {
             io_state new_io(io);

src/library/tactic/tactic.h

@@ -148,6 +148,10 @@ tactic trace_tactic(char const * msg);
 class sstream;
 tactic trace_tactic(sstream const & msg);
 tactic trace_tactic(std::string const & msg);
+/**
+   \brief Return a tactic that just displays the input state in the diagnostic channel.
+*/
+tactic trace_state_tactic();
 /**
    \brief Create a tactic that applies \c t, but suppressing diagnostic messages.
 */

src/tests/library/tactic/tactic.cpp

@@ -128,10 +128,11 @@ static void tst2() {
     ctx = extend(ctx, "H2", q);
     std::cout << "proof: " << (repeat(conj_tactic()) << assumption_tactic()).solve(env, io, ctx, And(And(p, q), And(p, p)))
               << "\n";
+    std::cout << "-------------\n";
     // Theorem to be proved
     expr F   = Implies(p, Implies(q, And(And(p, q), And(p, p))));
     // Tactic
-    tactic T = repeat(conj_tactic() || imp_tactic()) << assumption_tactic();
+    tactic T = repeat(conj_tactic() || imp_tactic()) << trace_state_tactic() << assumption_tactic();
     // Generate proof using tactic
     expr pr  = T.solve(env, io, context(), F);
     // Print proof