fix(library/tactic): pretty printer for proof states

src/frontends/lean/elaborator.cpp

@@ -942,7 +942,7 @@ void elaborator::display_unsolved_proof_state(expr const & mvar, proof_state con
         auto out = regular(env(), ios());
         flycheck_error err(out);
         display_error_pos(out, pip(), pos);
-        out << " " << msg << "\n" << ps << endl;
+        out << " " << msg << "\n" << ps.pp(env(), ios()) << endl;
     }
 }
 

src/library/io_state_stream.cpp

@@ -23,4 +23,10 @@ io_state_stream const & operator<<(io_state_stream const & out, kernel_exception
     out.get_stream() << mk_pair(ex.pp(out.get_formatter()), opts);
     return out;
 }
+
+io_state_stream const & operator<<(io_state_stream const & out, format const & f) {
+    options const & opts = out.get_options();
+    out.get_stream() << mk_pair(f, opts);
+    return out;
+}
 }

src/library/io_state_stream.h

@@ -41,6 +41,7 @@ class kernel_exception;
 io_state_stream const & operator<<(io_state_stream const & out, endl_class);
 io_state_stream const & operator<<(io_state_stream const & out, expr const & e);
 io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex);
+io_state_stream const & operator<<(io_state_stream const & out, format const & f);
 template<typename T> io_state_stream const & operator<<(io_state_stream const & out, T const & t) {
     out.get_stream() << t;
     return out;

src/library/tactic/proof_state.cpp

@@ -39,14 +39,14 @@ proof_state::proof_state(goals const & gs, substitution const & s, name_generato
     }
 }
 
-format proof_state::pp(formatter const & fmt) const {
-    options const & opts = fmt.get_options();
+format proof_state::pp_core(std::function<formatter()> const & mk_fmt, options const & opts) const {
     bool show_goal_names = get_proof_state_goal_names(opts);
     unsigned indent      = get_pp_indent(opts);
     format r;
     bool first = true;
 
     for (auto const & g : get_goals()) {
+        formatter fmt = mk_fmt();
         if (first) first = false; else r += line() + line();
         if (show_goal_names) {
             r += group(format(g.get_name()) + colon() + nest(indent, line() + g.pp(fmt, m_subst)));
@@ -58,6 +58,15 @@ format proof_state::pp(formatter const & fmt) const {
     return r;
 }
 
+format proof_state::pp(formatter const & fmt) const {
+    return pp_core([&]() { return fmt; }, fmt.get_options());
+}
+
+format proof_state::pp(environment const & env, io_state const & ios) const {
+    return pp_core([&]() { return ios.get_formatter_factory()(env, ios.get_options()); },
+                   ios.get_options());
+}
+
 goals map_goals(proof_state const & s, std::function<optional<goal>(goal const & g)> f) {
     return map_filter<goal>(s.get_goals(), [=](goal const & in, goal & out) -> bool {
             check_interrupted();
@@ -71,12 +80,6 @@ goals map_goals(proof_state const & s, std::function<optional<goal>(goal const &
         });
 }
 
-io_state_stream const & operator<<(io_state_stream const & out, proof_state const & s) {
-    options const & opts = out.get_options();
-    out.get_stream() << mk_pair(s.pp(out.get_formatter()), opts);
-    return out;
-}
-
 proof_state to_proof_state(expr const & meta, expr const & type, substitution const & subst, name_generator ngen,
                            bool relax_main_opaque) {
     return proof_state(goals(goal(meta, type)), subst, ngen, constraints(), relax_main_opaque);
@@ -187,9 +190,8 @@ static int to_proof_state(lua_State * L) {
 static int proof_state_tostring(lua_State * L) {
     std::ostringstream out;
     proof_state & s = to_proof_state(L, 1);
-    formatter fmt   = mk_formatter(L);
     options opts    = get_global_options(L);
-    out << mk_pair(s.pp(fmt), opts);
+    out << mk_pair(s.pp(get_global_environment(L), get_io_state(L)), opts);
     lua_pushstring(L, out.str().c_str());
     return 1;
 }
@@ -202,9 +204,9 @@ static int proof_state_pp(lua_State * L) {
     int nargs = lua_gettop(L);
     proof_state & s = to_proof_state(L, 1);
     if (nargs == 1)
-        return push_format(L, s.pp(mk_formatter(L)));
+        return push_format(L, s.pp(get_global_environment(L), get_io_state(L)));
     else
-        return push_format(L, s.pp(to_formatter(L, 2)));
+        return push_format(L, s.pp(to_environment(L, 1), to_io_state(L, 2)));
 }
 
 static const struct luaL_Reg proof_state_m[] = {

src/library/tactic/proof_state.h

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <utility>
 #include <algorithm>
+#include <functional>
 #include "util/lua.h"
 #include "util/optional.h"
 #include "util/name_set.h"
@@ -21,6 +22,9 @@ class proof_state {
     name_generator   m_ngen;
     constraints      m_postponed;
     bool             m_relax_main_opaque;
+
+    format pp_core(std::function<formatter()> const & mk_fmt, options const & opts) const;
+
 public:
     proof_state(goals const & gs, substitution const & s, name_generator const & ngen, constraints const & postponed,
                 bool relax_main_opaque);
@@ -48,6 +52,13 @@ public:
 
     /** \brief Return true iff this state does not have any goals left */
     bool is_final_state() const { return empty(m_goals); }
+
+    /** \remark This pretty printing method creates a fresh formatter object for each goal.
+        Some format objects "purify" local constant names by renaming.
+        The local constants in different goals are independent of each other.
+        So, this trick/hack avoids "unwanted purification".
+    */
+    format pp(environment const & env, io_state const & ios) const;
     format pp(formatter const & fmt) const;
 };
 
@@ -59,7 +70,6 @@ proof_state to_proof_state(expr const & meta, expr const & type, substitution co
 proof_state to_proof_state(expr const & meta, expr const & type, name_generator ngen, bool relax_main_opaque);
 
 goals map_goals(proof_state const & s, std::function<optional<goal>(goal const & g)> f);
-io_state_stream const & operator<<(io_state_stream const & out, proof_state const & s);
 
 UDATA_DEFS_CORE(goals)
 UDATA_DEFS(proof_state)

src/library/tactic/trace_tactic.cpp

@@ -32,7 +32,7 @@ tactic trace_tactic(char const * msg) {
 tactic trace_state_tactic(std::string const & fname, pair<unsigned, unsigned> const & pos) {
     return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state {
             diagnostic(env, ios) << fname << ":" << pos.first << ":" << pos.second << ": proof state\n"
-                                 << s << endl;
+                                 << s.pp(env, ios) << endl;
             ios.get_diagnostic_channel().get_stream().flush();
             return s;
         });
@@ -40,7 +40,7 @@ tactic trace_state_tactic(std::string const & fname, pair<unsigned, unsigned> co
 
 tactic trace_state_tactic() {
     return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state {
-            diagnostic(env, ios) << "proof state\n" << s << endl;
+            diagnostic(env, ios) << "proof state\n" << s.pp(env, ios) << endl;
             ios.get_diagnostic_channel().get_stream().flush();
             return s;
         });