From 4fa2468a85a5bf69c690d94089625015731ffe60 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 20 Aug 2013 12:19:28 -0700 Subject: [PATCH] Add output_channel and state abstractions Signed-off-by: Leonardo de Moura --- src/exprlib/CMakeLists.txt | 2 +- src/exprlib/formatter.cpp | 10 ++--- src/exprlib/formatter.h | 21 ++++----- src/exprlib/state.cpp | 40 ++++++++++++++++++ src/exprlib/state.h | 72 +++++++++++++++++++++++++++++++ src/frontend/frontend.cpp | 15 ++++++- src/frontend/frontend.h | 12 ++++++ src/frontend/pp.cpp | 87 +++++++++++++++++++------------------- src/frontend/pp.h | 2 +- src/tests/frontend/pp.cpp | 14 +++++- src/util/output_channel.h | 50 ++++++++++++++++++++++ 11 files changed, 260 insertions(+), 65 deletions(-) create mode 100644 src/exprlib/state.cpp create mode 100644 src/exprlib/state.h create mode 100644 src/util/output_channel.h diff --git a/src/exprlib/CMakeLists.txt b/src/exprlib/CMakeLists.txt index f7da763eb..f5d1802f7 100644 --- a/src/exprlib/CMakeLists.txt +++ b/src/exprlib/CMakeLists.txt @@ -1,3 +1,3 @@ add_library(exprlib basic_thms.cpp deep_copy.cpp max_sharing.cpp toplevel.cpp printer.cpp - formatter.cpp context_to_lambda.cpp) + formatter.cpp context_to_lambda.cpp state.cpp) target_link_libraries(exprlib ${LEAN_LIBS}) diff --git a/src/exprlib/formatter.cpp b/src/exprlib/formatter.cpp index 38b42194f..03a70f65a 100644 --- a/src/exprlib/formatter.cpp +++ b/src/exprlib/formatter.cpp @@ -11,23 +11,23 @@ Author: Leonardo de Moura namespace lean { class simple_formatter_cell : public formatter_cell { public: - virtual format operator()(expr const & e) { + virtual format operator()(expr const & e, options const & opts) { std::ostringstream s; s << e; return format(s.str()); } - virtual format operator()(context const & c) { + virtual format operator()(context const & c, options const & opts) { std::ostringstream s; s << c; return format(s.str()); } - virtual format operator()(context const & c, expr const & e, bool format_ctx) { + virtual format operator()(context const & c, expr const & e, bool format_ctx, options const & opts) { std::ostringstream s; if (format_ctx) s << c << "|-\n"; s << mk_pair(e,c); return format(s.str()); } - virtual format operator()(object const & obj) { + virtual format operator()(object const & obj, options const & opts) { std::ostringstream s; s << obj; return format(s.str()); } - virtual format operator()(environment const & env) { + virtual format operator()(environment const & env, options const & opts) { std::ostringstream s; s << env; return format(s.str()); } }; diff --git a/src/exprlib/formatter.h b/src/exprlib/formatter.h index c4901f8f7..519bfa3da 100644 --- a/src/exprlib/formatter.h +++ b/src/exprlib/formatter.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include "context.h" +#include "options.h" namespace lean { class environment; @@ -18,9 +19,9 @@ class formatter_cell { public: virtual ~formatter_cell() {} /** \brief Format the given expression. */ - virtual format operator()(expr const & e) = 0; + virtual format operator()(expr const & e, options const & opts) = 0; /** \brief Format the given context. */ - virtual format operator()(context const & c) = 0; + virtual format operator()(context const & c, options const & opts) = 0; /** \brief Format the given expression with respect to the given context. @@ -28,11 +29,11 @@ public: \remark If format_ctx == false, then the context is not formatted. It just provides names for the free variables */ - virtual format operator()(context const & c, expr const & e, bool format_ctx = false) = 0; + virtual format operator()(context const & c, expr const & e, bool format_ctx, options const & opts) = 0; /** \brief Format the given object */ - virtual format operator()(object const & obj) = 0; + virtual format operator()(object const & obj, options const & opts) = 0; /** \brief Format the given environment */ - virtual format operator()(environment const & env) = 0; + virtual format operator()(environment const & env, options const & opts) = 0; }; class formatter { @@ -40,11 +41,11 @@ class formatter { public: formatter(formatter_cell * c):m_cell(c) {} formatter(std::shared_ptr const & c):m_cell(c) {} - format operator()(expr const & e) { return (*m_cell)(e); } - format operator()(context const & c) { return (*m_cell)(c); } - format operator()(context const & c, expr const & e, bool format_ctx = false) { return (*m_cell)(c, e, format_ctx); } - format operator()(object const & obj) { return (*m_cell)(obj); } - format operator()(environment const & env) { return (*m_cell)(env); } + format operator()(expr const & e, options const & opts = options()) { return (*m_cell)(e, opts); } + format operator()(context const & c, options const & opts = options()) { return (*m_cell)(c, opts); } + format operator()(context const & c, expr const & e, bool format_ctx = false, options const & opts = options()) { return (*m_cell)(c, e, format_ctx, opts); } + format operator()(object const & obj, options const & opts = options()) { return (*m_cell)(obj, opts); } + format operator()(environment const & env, options const & opts = options()) { return (*m_cell)(env, opts); } }; formatter mk_simple_formatter(); diff --git a/src/exprlib/state.cpp b/src/exprlib/state.cpp new file mode 100644 index 000000000..5334abfeb --- /dev/null +++ b/src/exprlib/state.cpp @@ -0,0 +1,40 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "state.h" + +namespace lean { +state::state(): + m_formatter(mk_simple_formatter()), + m_regular_channel(new stdout_channel()), + m_diagnostic_channel(new stderr_channel()) { +} + +state::state(options const & opts, formatter const & fmt): + m_options(opts), + m_formatter(fmt), + m_regular_channel(new stdout_channel()), + m_diagnostic_channel(new stderr_channel()) { +} + +state::~state() {} + +void state::set_regular_channel(std::shared_ptr const & out) { + m_regular_channel = out; +} + +void state::set_diagnostic_channel(std::shared_ptr const & out) { + m_diagnostic_channel = out; +} + +void state::set_options(options const & opts) { + m_options = opts; +} + +void state::set_formatter(formatter const & f) { + m_formatter = f; +} +} diff --git a/src/exprlib/state.h b/src/exprlib/state.h new file mode 100644 index 000000000..6e204ad45 --- /dev/null +++ b/src/exprlib/state.h @@ -0,0 +1,72 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "output_channel.h" +#include "formatter.h" +#include "options.h" + +namespace lean { +/** + \brief State provided to internal lean procedures that need to: + 1- Access user defined options + 2- Produce verbosity messages + 3- Output results + 4- Produce formatted output +*/ +class state { + options m_options; + formatter m_formatter; + std::shared_ptr m_regular_channel; + std::shared_ptr m_diagnostic_channel; +public: + state(); + state(options const & opts, formatter const & fmt); + ~state(); + + options get_options() const { return m_options; } + formatter get_formatter() const { return m_formatter; } + output_channel & get_regular_channel() const { return *m_regular_channel; } + output_channel & get_diagnostic_channel() const { return *m_diagnostic_channel; } + + void set_regular_channel(std::shared_ptr const & out); + void set_diagnostic_channel(std::shared_ptr const & out); + void set_options(options const & opts); + void set_formatter(formatter const & f); +}; + +struct regular { + state const & m_state; + regular(state const & s):m_state(s) {} +}; + +struct diagnostic { + state const & m_state; + diagnostic(state const & s):m_state(s) {} +}; + +template +inline regular const & operator<<(regular const & out, T const & t) { + out.m_state.get_regular_channel().get_stream() << t; + return out; +} + +template +inline diagnostic const & operator<<(diagnostic const & out, T const & t) { + out.m_state.get_diagnostic_channel().get_stream() << t; + return out; +} + +inline regular const & operator<<(regular const & out, expr const & e) { + out.m_state.get_regular_channel().get_stream() << out.m_state.get_formatter()(e, out.m_state.get_options()); + return out; +} + +inline diagnostic const & operator<<(diagnostic const & out, expr const & e) { + out.m_state.get_diagnostic_channel().get_stream() << out.m_state.get_formatter()(e, out.m_state.get_options()); + return out; +} +} diff --git a/src/frontend/frontend.cpp b/src/frontend/frontend.cpp index 672dd2dbf..a8e58de74 100644 --- a/src/frontend/frontend.cpp +++ b/src/frontend/frontend.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "operator_info.h" #include "toplevel.h" #include "builtin_notation.h" +#include "state.h" #include "pp.h" namespace lean { @@ -27,6 +28,7 @@ struct frontend::imp { operator_table m_led; // led table for Pratt's parser expr_to_operator m_expr_to_operator; // map denotations to operators (this is used for pretty printing) implicit_table m_implicit_table; // track the number of implicit arguments for a symbol. + state m_state; bool has_children() const { return m_num_children > 0; } void inc_children() { m_num_children++; } @@ -168,7 +170,8 @@ struct frontend::imp { explicit imp(std::shared_ptr const & parent): m_num_children(0), m_parent(parent), - m_env(m_parent->m_env.mk_child()) { + m_env(m_parent->m_env.mk_child()), + m_state(m_parent->m_state) { m_parent->inc_children(); } @@ -181,8 +184,11 @@ struct frontend::imp { frontend::frontend():m_imp(new imp(*this)) { init_builtin_notation(*this); init_toplevel(m_imp->m_env); + m_imp->m_state.set_formatter(mk_pp_formatter(*this)); +} +frontend::frontend(imp * new_ptr):m_imp(new_ptr) { + m_imp->m_state.set_formatter(mk_pp_formatter(*this)); } -frontend::frontend(imp * new_ptr):m_imp(new_ptr) {} frontend::frontend(std::shared_ptr const & ptr):m_imp(ptr) {} frontend::~frontend() {} @@ -223,4 +229,9 @@ void frontend::add_mixfixc(unsigned sz, name const * opns, unsigned p, expr cons operator_info frontend::find_op_for(expr const & n) const { return m_imp->find_op_for(n); } operator_info frontend::find_nud(name const & n) const { return m_imp->find_nud(n); } operator_info frontend::find_led(name const & n) const { return m_imp->find_led(n); } + +state const & frontend::get_state() const { return m_imp->m_state; } +void frontend::set_options(options const & opts) { return m_imp->m_state.set_options(opts); } +void frontend::set_regular_channel(std::shared_ptr const & out) { return m_imp->m_state.set_regular_channel(out); } +void frontend::set_diagnostic_channel(std::shared_ptr const & out) { return m_imp->m_state.set_diagnostic_channel(out); } } diff --git a/src/frontend/frontend.h b/src/frontend/frontend.h index 79a31602f..09a3e06e0 100644 --- a/src/frontend/frontend.h +++ b/src/frontend/frontend.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include #include "environment.h" #include "operator_info.h" +#include "state.h" namespace lean { /** @@ -113,5 +114,16 @@ public: */ operator_info find_led(name const & n) const; /*@}*/ + + /** + @name State management. + */ + /*@{*/ + state const & get_state() const; + operator state const &() const { return get_state(); } + void set_options(options const & opts); + void set_regular_channel(std::shared_ptr const & out); + void set_diagnostic_channel(std::shared_ptr const & out); + /*@}*/ }; } diff --git a/src/frontend/pp.cpp b/src/frontend/pp.cpp index 6e2059131..5cfe913b2 100644 --- a/src/frontend/pp.cpp +++ b/src/frontend/pp.cpp @@ -793,23 +793,22 @@ public: class pp_formatter_cell : public formatter_cell { frontend m_frontend; - options m_options; - unsigned m_indent; - format pp(expr const & e) { - return pp_fn(m_frontend, m_options)(e); + format pp(expr const & e, options const & opts) { + return pp_fn(m_frontend, opts)(e); } - format pp(context const & c, expr const & e, bool include_e) { + format pp(context const & c, expr const & e, bool include_e, options const & opts) { + unsigned indent = get_pp_indent(opts); format r; bool first = true; expr c2 = context_to_lambda(c, e); while (is_fake_context(c2)) { name n1 = get_unused_name(c2); - format entry = format{format(n1), space(), colon(), space(), pp(fake_context_domain(c2))}; + format entry = format{format(n1), space(), colon(), space(), pp(fake_context_domain(c2), opts)}; expr val = fake_context_value(c2); if (val) - entry += format{space(), g_assign_fmt, nest(m_indent, format{line(), pp(val)})}; + entry += format{space(), g_assign_fmt, nest(indent, format{line(), pp(val, opts)})}; if (first) { r = group(entry); first = false; @@ -820,77 +819,77 @@ class pp_formatter_cell : public formatter_cell { } if (include_e) { if (first) - r += format{line(), pp(c2)}; + r += format{line(), pp(c2, opts)}; else - r = pp(c2); + r = pp(c2, opts); } else { return r; } return r; } - format pp_definition(char const * kwd, name const & n, expr const & t, expr const & v) { + format pp_definition(char const * kwd, name const & n, expr const & t, expr const & v, options const & opts) { + unsigned indent = get_pp_indent(opts); format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(), - pp(t), space(), g_assign_fmt, line(), pp(v)}; - return group(nest(m_indent, def)); + pp(t, opts), space(), g_assign_fmt, line(), pp(v, opts)}; + return group(nest(indent, def)); } - format pp_compact_definition(char const * kwd, name const & n, expr const & t, expr const & v) { + format pp_compact_definition(char const * kwd, name const & n, expr const & t, expr const & v, options const & opts) { expr it1 = t; expr it2 = v; while (is_pi(it1) && is_lambda(it2)) { if (abst_domain(it1) != abst_domain(it2)) - return pp_definition(kwd, n, t, v); + return pp_definition(kwd, n, t, v, opts); it1 = abst_body(it1); it2 = abst_body(it2); } if (!is_lambda(v) || is_pi(it1)) { - return pp_definition(kwd, n, t, v); + return pp_definition(kwd, n, t, v, opts); } else { + lean_assert(is_lambda(v)); - format def = pp_fn(m_frontend, m_options).pp_definition(v, t); + format def = pp_fn(m_frontend, opts).pp_definition(v, t); return format{highlight_command(format(kwd)), space(), format(n), def}; } } - format pp_uvar_decl(object const & obj) { + format pp_uvar_decl(object const & obj, options const & opts) { return format{highlight_command(format(obj.keyword())), space(), format(obj.get_name()), space(), format("\u2265"), space(), ::lean::pp(obj.get_cnstr_level())}; } - format pp_postulate(object const & obj) { - return format{highlight_command(format(obj.keyword())), space(), format(obj.get_name()), space(), colon(), space(), pp(obj.get_type())}; + format pp_postulate(object const & obj, options const & opts) { + return format{highlight_command(format(obj.keyword())), space(), format(obj.get_name()), space(), colon(), space(), pp(obj.get_type(), opts)}; } - format pp_definition(object const & obj) { - return pp_compact_definition(obj.keyword(), obj.get_name(), obj.get_type(), obj.get_value()); + format pp_definition(object const & obj, options const & opts) { + return pp_compact_definition(obj.keyword(), obj.get_name(), obj.get_type(), obj.get_value(), opts); } - format pp_notation_decl(object const & obj) { + format pp_notation_decl(object const & obj, options const & opts) { notation_declaration const & n = *(static_cast(obj.cell())); - return format{::lean::pp(n.get_op()), space(), colon(), space(), pp(n.get_expr())}; + return format{::lean::pp(n.get_op()), space(), colon(), space(), pp(n.get_expr(), opts)}; } public: - pp_formatter_cell(frontend const & fe, options const & opts): - m_frontend(fe), - m_options(opts) { - m_indent = get_pp_indent(opts); + pp_formatter_cell(frontend const & fe): + m_frontend(fe) { } virtual ~pp_formatter_cell() { } - virtual format operator()(expr const & e) { - return pp(e); + virtual format operator()(expr const & e, options const & opts) { + return pp(e, opts); } - virtual format operator()(context const & c) { - return pp(c, Type(), false); + virtual format operator()(context const & c, options const & opts) { + return pp(c, Type(), false, opts); } - virtual format operator()(context const & c, expr const & e, bool format_ctx) { + virtual format operator()(context const & c, expr const & e, bool format_ctx, options const & opts) { if (format_ctx) { - return pp(c, e, true); + return pp(c, e, true, opts); } else { expr c2 = context_to_lambda(c, e); while (is_fake_context(c2)) { @@ -898,20 +897,20 @@ public: name n1 = get_unused_name(rest); c2 = instantiate_with_closed(rest, mk_constant(n1)); } - return pp(c2); + return pp(c2, opts); } } - virtual format operator()(object const & obj) { + virtual format operator()(object const & obj, options const & opts) { switch (obj.kind()) { - case object_kind::UVarDeclaration: return pp_uvar_decl(obj); - case object_kind::Postulate: return pp_postulate(obj); - case object_kind::Definition: return pp_definition(obj); + case object_kind::UVarDeclaration: return pp_uvar_decl(obj, opts); + case object_kind::Postulate: return pp_postulate(obj, opts); + case object_kind::Definition: return pp_definition(obj, opts); case object_kind::Neutral: if (dynamic_cast(obj.cell())) { // If the object is not notation, then the object was // created in different frontend, and we ignore it. - return pp_notation_decl(obj); + return pp_notation_decl(obj, opts); } else { return format("Unknown neutral object"); } @@ -920,25 +919,25 @@ public: return format(); } - virtual format operator()(environment const & env) { + virtual format operator()(environment const & env, options const & opts) { format r; bool first = true; std::for_each(env.begin_objects(), env.end_objects(), [&](object const & obj) { if (first) first = false; else r += line(); - r += operator()(obj); + r += operator()(obj, opts); }); return r; } }; -formatter mk_pp_formatter(frontend const & fe, options const & opts) { - return formatter(new pp_formatter_cell(fe, opts)); +formatter mk_pp_formatter(frontend const & fe) { + return formatter(new pp_formatter_cell(fe)); } std::ostream & operator<<(std::ostream & out, frontend const & fe) { - formatter fmt = mk_pp_formatter(fe, options()); + formatter fmt = mk_pp_formatter(fe); out << fmt(fe.get_environment()); return out; } diff --git a/src/frontend/pp.h b/src/frontend/pp.h index 2414600ef..ccb124af4 100644 --- a/src/frontend/pp.h +++ b/src/frontend/pp.h @@ -11,6 +11,6 @@ Author: Leonardo de Moura namespace lean { class frontend; -formatter mk_pp_formatter(frontend const & fe, options const & opts = options()); +formatter mk_pp_formatter(frontend const & fe); std::ostream & operator<<(std::ostream & out, frontend const & fe); } diff --git a/src/tests/frontend/pp.cpp b/src/tests/frontend/pp.cpp index c7371643c..756440c06 100644 --- a/src/tests/frontend/pp.cpp +++ b/src/tests/frontend/pp.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include "frontend.h" #include "printer.h" #include "abstract.h" +#include "builtin.h" #include "pp.h" #include "test.h" using namespace lean; @@ -36,8 +37,8 @@ static void tst2() { expr t = Fun({a, Type()}, mk_shared_expr(10)); expr g = Const("g"); std::cout << fmt(g(t, t, t)) << std::endl; - formatter fmt2 = mk_pp_formatter(f, options({"pp", "alias_min_weight"}, 100)); - std::cout << fmt2(g(t, t, t)) << std::endl; + formatter fmt2 = mk_pp_formatter(f); + std::cout << fmt2(g(t, t, t), options({"pp", "alias_min_weight"}, 100)) << std::endl; } static void tst3() { @@ -56,9 +57,18 @@ static void tst3() { std::cout << fmt(g(d, c, b, t)) << "\n"; } +static void tst4() { + frontend f; + state const & s = f.get_state(); + regular(s) << And(Const("a"), Const("b")) << "\n"; + regular(f) << And(Const("a"), Const("b")) << "\n"; + diagnostic(f) << And(Const("a"), Const("b")) << "\n"; +} + int main() { tst1(); tst2(); tst3(); + tst4(); return has_violations() ? 1 : 0; } diff --git a/src/util/output_channel.h b/src/util/output_channel.h new file mode 100644 index 000000000..dfb67c9c9 --- /dev/null +++ b/src/util/output_channel.h @@ -0,0 +1,50 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include + +namespace lean { +/** + \brief Wrapper for std::ostream. + The idea is to be able to have an output stream that can be + "reassigned". + + std::unique_ptr out; + out = new stdout_channel(); + (*out) << "writting to standard output"; + out = new stderr_channel(); + (*out) << "writting to standard input"; + out = new file_output_channel("file.txt"); + (*out) << "writting to file"; +*/ +class output_channel { +public: + virtual ~output_channel() {} + virtual std::ostream & get_stream() = 0; +}; +class stdout_channel : public output_channel { +public: + virtual std::ostream & get_stream() { return std::cout; } +}; +class stderr_channel : public output_channel { +public: + virtual std::ostream & get_stream() { return std::cerr; } +}; +class file_output_channel : public output_channel { + std::ofstream m_out; +public: + file_output_channel(char const * fname):m_out(fname) {} + virtual ~file_output_channel() {} + virtual std::ostream & get_stream() { return m_out; } +}; +template +output_channel & operator<<(output_channel & out, T const & v) { + out.get_stream() << v; + return out; +} +}