From e792e079e2c3aa2361bd2d0bea16cd255c1276b6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 16 Aug 2013 18:34:11 -0700 Subject: [PATCH] Add formatter API Signed-off-by: Leonardo de Moura --- src/exprlib/CMakeLists.txt | 3 +- src/exprlib/formatter.cpp | 34 +++++++++++++++++ src/exprlib/formatter.h | 38 +++++++++++++++++++ src/exprlib/printer.h | 2 +- src/frontend/frontend.cpp | 35 ----------------- src/frontend/operator_info.cpp | 69 +++++++++++++++------------------- src/frontend/operator_info.h | 20 ++++++++++ src/frontend/pp.h | 3 +- src/kernel/object.h | 5 ++- 9 files changed, 132 insertions(+), 77 deletions(-) create mode 100644 src/exprlib/formatter.cpp create mode 100644 src/exprlib/formatter.h diff --git a/src/exprlib/CMakeLists.txt b/src/exprlib/CMakeLists.txt index cff1128fa..902eaffc7 100644 --- a/src/exprlib/CMakeLists.txt +++ b/src/exprlib/CMakeLists.txt @@ -1,2 +1,3 @@ -add_library(exprlib basic_thms.cpp deep_copy.cpp max_sharing.cpp toplevel.cpp printer.cpp) +add_library(exprlib basic_thms.cpp deep_copy.cpp max_sharing.cpp toplevel.cpp printer.cpp + formatter.cpp) target_link_libraries(exprlib ${LEAN_LIBS}) diff --git a/src/exprlib/formatter.cpp b/src/exprlib/formatter.cpp new file mode 100644 index 000000000..d221ef14d --- /dev/null +++ b/src/exprlib/formatter.cpp @@ -0,0 +1,34 @@ +/* +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 +#include "formatter.h" +#include "printer.h" + +namespace lean { +class simple_formatter : public formatter { +public: + virtual format operator()(expr const & e) { + std::ostringstream s; s << e; return format(s.str()); + } + virtual format operator()(context const & c) { + std::ostringstream s; s << c; return format(s.str()); + } + virtual format operator()(context const & c, expr const & e, bool format_ctx) { + std::ostringstream s; + if (format_ctx) + s << c << "|-\n"; + s << mk_pair(e,c); + return format(s.str()); + } + virtual format operator()(environment const & env) { + std::ostringstream s; s << env; return format(s.str()); + } +}; +std::shared_ptr mk_simple_formatter() { + return std::shared_ptr(new simple_formatter()); +} +} diff --git a/src/exprlib/formatter.h b/src/exprlib/formatter.h new file mode 100644 index 000000000..c18e75498 --- /dev/null +++ b/src/exprlib/formatter.h @@ -0,0 +1,38 @@ +/* +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 "context.h" + +namespace lean { +class environment; +/** + \brief API for formatting expressions, contexts and environments. +*/ +class formatter { +public: + virtual ~formatter() {} + /** \brief Format the given expression. */ + virtual format operator()(expr const & e) = 0; + /** \brief Format the given context. */ + virtual format operator()(context const & c) = 0; + /** + \brief Format the given expression with respect to the given + context. + + \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; + /** \brief Format the given environment */ + virtual format operator()(environment const & env) = 0; +}; +/** + \brief Return simple expression formatter that just uses printer module. +*/ +std::shared_ptr mk_simple_formatter(); +} diff --git a/src/exprlib/printer.h b/src/exprlib/printer.h index 701f2fe02..4ad7a0c81 100644 --- a/src/exprlib/printer.h +++ b/src/exprlib/printer.h @@ -12,7 +12,7 @@ Author: Leonardo de Moura namespace lean { std::ostream & operator<<(std::ostream & out, context const & ctx); std::ostream & operator<<(std::ostream & out, expr const & e); -std::ostream & operator<<(std::ostream & out, std::pair const & p); +std::ostream & operator<<(std::ostream & out, std::pair const & p); class environment; std::ostream & operator<<(std::ostream & out, environment const & env); } diff --git a/src/frontend/frontend.cpp b/src/frontend/frontend.cpp index d331a0153..7e6e587c2 100644 --- a/src/frontend/frontend.cpp +++ b/src/frontend/frontend.cpp @@ -14,41 +14,6 @@ Author: Leonardo de Moura #include "pp.h" namespace lean { -/** - \brief Create object for tracking notation/operator declarations. - This object is mainly used for pretty printing. -*/ -class notation_declaration : public neutral_object_cell { - operator_info m_op; - name m_name; -public: - notation_declaration(operator_info const & op, name const & n):m_op(op), m_name(n) {} - virtual ~notation_declaration() {} - static char const * g_keyword; - virtual char const * keyword() const { return g_keyword; } - virtual format pp(environment const &) const { - char const * cmd; - switch (m_op.get_fixity()) { - case fixity::Infix: cmd = "Infix"; break; - case fixity::Infixl: cmd = "Infixl"; break; - case fixity::Infixr: cmd = "Infixr"; break; - case fixity::Prefix: cmd = "Prefix"; break; - case fixity::Postfix: cmd = "Postfix"; break; - case fixity::Mixfixl: cmd = "Mixfixl"; break; - case fixity::Mixfixr: cmd = "Mixfixr"; break; - case fixity::Mixfixc: cmd = "Mixfixc"; break; - } - format r = highlight_command(format(cmd)); - if (m_op.get_precedence() != 0) - r += format{space(), format(m_op.get_precedence())}; - for (auto p : m_op.get_op_name_parts()) - r += format{space(), format(p)}; - r += format{space(), format(m_name)}; - return r; - } -}; -char const * notation_declaration::g_keyword = "Notation"; - /** \brief Implementation of the Lean frontend */ struct frontend::imp { // Remark: only named objects are stored in the dictionary. diff --git a/src/frontend/operator_info.cpp b/src/frontend/operator_info.cpp index c63436621..e5a8351c9 100644 --- a/src/frontend/operator_info.cpp +++ b/src/frontend/operator_info.cpp @@ -101,53 +101,46 @@ operator_info mixfixc(unsigned num_parts, name const * parts, unsigned precedenc lean_assert(num_parts > 1); return operator_info(new operator_info::imp(num_parts, parts, fixity::Mixfixc, precedence)); } -static char const * g_arrow = "\u21a6"; +char const * to_string(fixity f) { + switch (f) { + case fixity::Infix: return "Infix"; + case fixity::Infixl: return "Infixl"; + case fixity::Infixr: return "Infixr"; + case fixity::Prefix: return "Prefix"; + case fixity::Postfix: return "Postfix"; + case fixity::Mixfixl: return "Mixfixl"; + case fixity::Mixfixr: return "Mixfixr"; + case fixity::Mixfixc: return "Mixfixc"; + } + lean_unreachable(); + return 0; +} format pp(operator_info const & o) { format r; - switch (o.get_fixity()) { - case fixity::Infix: r = format("Infix"); break; - case fixity::Infixl: r = format("Infixl"); break; - case fixity::Infixr: r = format("Infixr"); break; - case fixity::Prefix: r = format("Prefix"); break; - case fixity::Postfix: r = format("Postfix"); break; - case fixity::Mixfixl: - case fixity::Mixfixr: - case fixity::Mixfixc: r = format("Mixfix"); break; - } - - r += space(); - + r = format(to_string(o.get_fixity())); if (o.get_precedence() != 0) - r += format{format(o.get_precedence()), space()}; - - switch (o.get_fixity()) { - case fixity::Infix: case fixity::Infixl: case fixity::Infixr: case fixity::Prefix: case fixity::Postfix: - r += pp(o.get_op_name()); break; - case fixity::Mixfixl: - for (auto p : o.get_op_name_parts()) r += format{pp(p), format(" _")}; - break; - case fixity::Mixfixr: - for (auto p : o.get_op_name_parts()) r += format{format("_ "), pp(p)}; - break; - case fixity::Mixfixc: { - bool first = true; - for (auto p : o.get_op_name_parts()) { - if (first) first = false; else r += format(" _ "); - r += pp(p); - } - }} - - list const & l = o.get_internal_names(); - if (!is_nil(l)) { - r += format{space(), format(g_arrow)}; - for (auto n : l) r += format{space(), pp(n)}; - } + r += format{space(), format(o.get_precedence())}; + for (auto p : o.get_op_name_parts()) + r += format{space(), format(p)}; return r; } +char const * notation_declaration::keyword() const { + return to_string(m_op.get_fixity()); +} + std::ostream & operator<<(std::ostream & out, operator_info const & o) { out << pp(o); return out; } + +format pp(notation_declaration const & n) { + return format{pp(n.get_op()), space(), format(n.get_internal_name())}; +} + +std::ostream & operator<<(std::ostream & out, notation_declaration const & n) { + out << pp(n); + return out; +} } diff --git a/src/frontend/operator_info.h b/src/frontend/operator_info.h index 53e3715c4..bfcc195c9 100644 --- a/src/frontend/operator_info.h +++ b/src/frontend/operator_info.h @@ -8,11 +8,13 @@ Author: Leonardo de Moura #include "name.h" #include "list.h" #include "format.h" +#include "object.h" namespace lean { /** \brief Operator fixity. Prefix: ID _ + Infixl: _ ID _ Infixl: _ ID _ (left associative) Infixr: _ ID _ (right associative) Postfix: _ ID @@ -101,4 +103,22 @@ inline operator_info mixfixc(std::initializer_list const & l, unsigned pre format pp(operator_info const & o); std::ostream & operator<<(std::ostream & out, operator_info const & o); + +/** + \brief Create object for tracking notation/operator declarations. + This object is mainly used for recording the declaration. +*/ +class notation_declaration : public neutral_object_cell { + operator_info m_op; + name m_name; +public: + notation_declaration(operator_info const & op, name const & n):m_op(op), m_name(n) {} + virtual ~notation_declaration() {} + virtual char const * keyword() const; + operator_info get_op() const { return m_op; } + name const & get_internal_name() const { return m_name; } +}; + +format pp(notation_declaration const & n); +std::ostream & operator<<(std::ostream & out, notation_declaration const & n); } diff --git a/src/frontend/pp.h b/src/frontend/pp.h index 9539f1b88..3b784981d 100644 --- a/src/frontend/pp.h +++ b/src/frontend/pp.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "context.h" namespace lean { + class frontend; class expr_formatter { public: @@ -28,5 +29,5 @@ public: /** \brief Nest the given format object using the setting provided by get_options. */ format nest(format const & f); }; -std::shared_ptr mk_pp_expr_formatter(frontend const & fe, options const & opts); +std::shared_ptr mk_pp_formatter(frontend const & fe, options const & opts); } diff --git a/src/kernel/object.h b/src/kernel/object.h index 74d0da826..b2497a594 100644 --- a/src/kernel/object.h +++ b/src/kernel/object.h @@ -58,7 +58,8 @@ public: /** \brief Neutral objects are mainly used for bookkeeping in - kernel frontends. + frontends built on top of the kernel. + The kernel does *not* create neutral objects. */ class neutral_object_cell : public object_cell { public: @@ -122,6 +123,8 @@ public: bool is_definition() const { return m_ptr->is_definition(); } bool is_opaque() const { return m_ptr->is_opaque(); } expr const & get_value() const { return m_ptr->get_value(); } + + object_cell const * cell() const { return m_ptr; } }; object mk_uvar_decl(name const & n, level const & l); object mk_definition(name const & n, expr const & t, expr const & v, bool opaque);