michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/io_state): simplify regular/diagnostic

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-10 13:09:35 -08:00
parent 6b1b6c7bd1
commit c0b9c7ffc4
6 changed files with 46 additions and 88 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/frontends/lean/operator_info.cpp
View file

@ -184,13 +184,8 @@ std::ostream & operator<<(std::ostream & out, operator_info const & o) {
return out; return out;
} }
regular const & operator<<(regular const & out, operator_info const & o) { io_state_stream const & operator<<(io_state_stream const & out, operator_info const & o) {
out.m_io_state.get_regular_channel().get_stream() << mk_pair(pp(o), out.m_io_state.get_options()); out.get_stream() << mk_pair(pp(o), out.get_options());
return out;
}
diagnostic const & operator<<(diagnostic const & out, operator_info const & o) {
out.m_io_state.get_diagnostic_channel().get_stream() << mk_pair(pp(o), out.m_io_state.get_options());
return out; return out;
} }
} }

3
src/frontends/lean/operator_info.h
View file

@ -111,8 +111,7 @@ inline operator_info mixfixo(std::initializer_list<name> const & l, unsigned pre
format pp(operator_info const & o); format pp(operator_info const & o);
std::ostream & operator<<(std::ostream & out, operator_info const & o); std::ostream & operator<<(std::ostream & out, operator_info const & o);
regular const & operator<<(regular const & out, operator_info const & o); io_state_stream const & operator<<(io_state_stream const & out, operator_info const & o);
diagnostic const & operator<<(diagnostic const & out, operator_info const & o);
/** /**
\brief Create object for tracking notation/operator declarations. \brief Create object for tracking notation/operator declarations.

53
src/library/io_state.cpp
View file

@ -42,57 +42,26 @@ void io_state::set_formatter(formatter const & f) {
m_formatter = f; m_formatter = f;
} }
void regular::flush() { io_state_stream const & operator<<(io_state_stream const & out, endl_class) {
m_io_state.get_regular_channel().get_stream().flush(); out.get_stream() << std::endl;
}
void diagnostic::flush() {
m_io_state.get_diagnostic_channel().get_stream().flush();
}
regular const & operator<<(regular const & out, endl_class) {
out.m_io_state.get_regular_channel().get_stream() << std::endl;
return out; return out;
} }
diagnostic const & operator<<(diagnostic const & out, endl_class) { io_state_stream const & operator<<(io_state_stream const & out, expr const & e) {
out.m_io_state.get_diagnostic_channel().get_stream() << std::endl; options const & opts = out.get_options();
out.get_stream() << mk_pair(out.get_formatter()(e, opts), opts);
return out; return out;
} }
regular const & operator<<(regular const & out, expr const & e) { io_state_stream const & operator<<(io_state_stream const & out, object const & obj) {
options const & opts = out.m_io_state.get_options(); options const & opts = out.get_options();
out.m_io_state.get_regular_channel().get_stream() << mk_pair(out.m_io_state.get_formatter()(e, opts), opts); out.get_stream() << mk_pair(out.get_formatter()(obj, opts), opts);
return out; return out;
} }
diagnostic const & operator<<(diagnostic const & out, expr const & e) { io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex) {
options const & opts = out.m_io_state.get_options(); options const & opts = out.get_options();
out.m_io_state.get_diagnostic_channel().get_stream() << mk_pair(out.m_io_state.get_formatter()(e, opts), opts); out.get_stream() << mk_pair(ex.pp(out.get_formatter(), opts), opts);
return out;
}
regular const & operator<<(regular const & out, object const & obj) {
options const & opts = out.m_io_state.get_options();
out.m_io_state.get_regular_channel().get_stream() << mk_pair(out.m_io_state.get_formatter()(obj, opts), opts);
return out;
}
diagnostic const & operator<<(diagnostic const & out, object const & obj) {
options const & opts = out.m_io_state.get_options();
out.m_io_state.get_diagnostic_channel().get_stream() << mk_pair(out.m_io_state.get_formatter()(obj, opts), opts);
return out;
}
regular const & operator<<(regular const & out, kernel_exception const & ex) {
options const & opts = out.m_io_state.get_options();
out.m_io_state.get_regular_channel().get_stream() << mk_pair(ex.pp(out.m_io_state.get_formatter(), opts), opts);
return out;
}
diagnostic const & operator<<(diagnostic const & out, kernel_exception const & ex) {
options const & opts = out.m_io_state.get_options();
out.m_io_state.get_diagnostic_channel().get_stream() << mk_pair(ex.pp(out.m_io_state.get_formatter(), opts), opts);
return out; return out;
} }

54
src/library/io_state.h
View file

@ -41,24 +41,38 @@ public:
} }
}; };
/**
\brief Base class for \c regular and \c diagnostic wrapper classes.
*/
class io_state_stream {
protected:
io_state const & m_io_state;
public:
io_state_stream(io_state const & s):m_io_state(s) {}
virtual std::ostream & get_stream() const = 0;
void flush() { get_stream().flush(); }
formatter get_formatter() const { return m_io_state.get_formatter(); }
options get_options() const { return m_io_state.get_options(); }
};
/** /**
\brief Wrapper for the io_state object that provides access to the \brief Wrapper for the io_state object that provides access to the
io_state's regular channel io_state's regular channel
*/ */
struct regular { class regular : public io_state_stream {
io_state const & m_io_state; public:
regular(io_state const & s):m_io_state(s) {} regular(io_state const & s):io_state_stream(s) {}
void flush(); std::ostream & get_stream() const { return m_io_state.get_regular_channel().get_stream(); }
}; };
/** /**
\brief Wrapper for the io_state object that provides access to the \brief Wrapper for the io_state object that provides access to the
io_state's diagnostic channel io_state's diagnostic channel
*/ */
struct diagnostic { class diagnostic : public io_state_stream {
io_state const & m_io_state; public:
diagnostic(io_state const & s):m_io_state(s) {} diagnostic(io_state const & s):io_state_stream(s) {}
void flush(); std::ostream & get_stream() const { return m_io_state.get_diagnostic_channel().get_stream(); }
}; };
// hack for using std::endl with channels // hack for using std::endl with channels
@ -67,24 +81,12 @@ const endl_class endl;
class kernel_exception; class kernel_exception;
regular const & operator<<(regular const & out, endl_class); io_state_stream const & operator<<(io_state_stream const & out, endl_class);
diagnostic const & operator<<(diagnostic const & out, endl_class); io_state_stream const & operator<<(io_state_stream const & out, expr const & e);
regular const & operator<<(regular const & out, expr const & e); io_state_stream const & operator<<(io_state_stream const & out, object const & obj);
diagnostic const & operator<<(diagnostic const & out, expr const & e); io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex);
regular const & operator<<(regular const & out, object const & obj); template<typename T> io_state_stream const & operator<<(io_state_stream const & out, T const & t) {
diagnostic const & operator<<(diagnostic const & out, object const & obj); out.get_stream() << t;
regular const & operator<<(regular const & out, kernel_exception const & ex);
diagnostic const & operator<<(diagnostic const & out, kernel_exception const & ex);
template<typename T>
inline regular const & operator<<(regular const & out, T const & t) {
out.m_io_state.get_regular_channel().get_stream() << t;
return out;
}
template<typename T>
inline diagnostic const & operator<<(diagnostic const & out, T const & t) {
out.m_io_state.get_diagnostic_channel().get_stream() << t;
return out; return out;
} }

12
src/library/tactic/proof_state.cpp
View file

@ -100,15 +100,9 @@ proof_state to_proof_state(environment const & env, context const & ctx, expr co
return proof_state(goals(mk_pair(g_main, g)), metavar_env(), pr_builder, cex_builder); return proof_state(goals(mk_pair(g_main, g)), metavar_env(), pr_builder, cex_builder);
} }
regular const & operator<<(regular const & out, proof_state & s) { io_state_stream const & operator<<(io_state_stream const & out, proof_state & s) {
options const & opts = out.m_io_state.get_options(); options const & opts = out.get_options();
out.m_io_state.get_regular_channel().get_stream() << mk_pair(s.pp(out.m_io_state.get_formatter(), opts), opts); out.get_stream() << mk_pair(s.pp(out.get_formatter(), opts), opts);
return out;
}
diagnostic const & operator<<(diagnostic const & out, proof_state & s) {
options const & opts = out.m_io_state.get_options();
out.m_io_state.get_diagnostic_channel().get_stream() << mk_pair(s.pp(out.m_io_state.get_formatter(), opts), opts);
return out; return out;
} }

3
src/library/tactic/proof_state.h
View file

@ -118,8 +118,7 @@ goals map_goals(proof_state const & s, F && f) {
}); });
} }
regular const & operator<<(regular const & out, proof_state & s); io_state_stream const & operator<<(io_state_stream const & out, proof_state & s);
diagnostic const & operator<<(diagnostic const & out, proof_state & s);
UDATA_DEFS_CORE(goals) UDATA_DEFS_CORE(goals)
UDATA_DEFS(proof_state) UDATA_DEFS(proof_state)