diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index db7510698..fac4e17cd 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/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; } } diff --git a/src/library/io_state_stream.cpp b/src/library/io_state_stream.cpp index 3a8fcf234..867827de2 100644 --- a/src/library/io_state_stream.cpp +++ b/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; +} } diff --git a/src/library/io_state_stream.h b/src/library/io_state_stream.h index aa355b6f8..e44d7dd6d 100644 --- a/src/library/io_state_stream.h +++ b/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 io_state_stream const & operator<<(io_state_stream const & out, T const & t) { out.get_stream() << t; return out; diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 0dac3d90c..12851193a 100644 --- a/src/library/tactic/proof_state.cpp +++ b/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 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(goal const & g)> f) { return map_filter(s.get_goals(), [=](goal const & in, goal & out) -> bool { check_interrupted(); @@ -71,12 +80,6 @@ goals map_goals(proof_state const & s, std::function(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[] = { diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 999d377f0..b033531b6 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include +#include #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 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(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) diff --git a/src/library/tactic/trace_tactic.cpp b/src/library/tactic/trace_tactic.cpp index 8fe79cec3..2a379d156 100644 --- a/src/library/tactic/trace_tactic.cpp +++ b/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 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 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; });