From e5fe016a4486134e5547d8259657677cb901f501 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Aug 2013 18:35:49 -0700 Subject: [PATCH] Add pretty printer for s-expressions and options Signed-off-by: Leonardo de Moura --- src/tests/util/options.cpp | 12 ++++ src/tests/util/sexpr.cpp | 12 +++- src/util/format.cpp | 116 +++++++++++++++++++++++++++++++++++-- src/util/format.h | 21 ++++++- src/util/name.cpp | 21 ++++++- src/util/name.h | 12 +++- src/util/options.cpp | 38 ++++++++---- src/util/options.h | 4 ++ src/util/sexpr_funcs.h | 2 +- 9 files changed, 214 insertions(+), 24 deletions(-) diff --git a/src/tests/util/options.cpp b/src/tests/util/options.cpp index a621fba8e..edeb27867 100644 --- a/src/tests/util/options.cpp +++ b/src/tests/util/options.cpp @@ -17,8 +17,20 @@ static void tst1() { std::cout << opt << "\n"; } +static void tst2() { + options opt; + opt = update(opt, name{"test", "foo"}, 10); + opt = update(opt, name{"color"}, 20); + opt = update(opt, name{"ratio"}, 10.5); + sexpr s{1, 2, 3, 4, 5, 6, 7, 8, 9, 10}; + opt = update(opt, name{"sp", "order"}, sexpr{s, s, s, s, s, s}); + opt = update(opt, name{"test", "long", "names", "with", "several", "parts"}, true); + std::cout << pp(opt) << "\n"; +} + int main() { continue_on_violation(true); tst1(); + tst2(); return has_violations() ? 1 : 0; } diff --git a/src/tests/util/sexpr.cpp b/src/tests/util/sexpr.cpp index ee5a2f521..623a53b40 100644 --- a/src/tests/util/sexpr.cpp +++ b/src/tests/util/sexpr.cpp @@ -10,6 +10,8 @@ Author: Leonardo de Moura #include "mpq.h" #include "name.h" #include "test.h" +#include "format.h" +#include "options.h" using namespace lean; static void tst1() { @@ -116,7 +118,7 @@ static void tst2() { static void tst3() { int sum = 0; - foreach(sexpr{0, 1, 2, 3, 4}, + for_each(sexpr{0, 1, 2, 3, 4}, [&](sexpr const & e) { sum += to_int(e); }); lean_assert(sum == 10); } @@ -162,6 +164,13 @@ static void tst6() { lean_assert(s.str() == "\"str with \\\"quote\\\"\""); } +static void tst7() { + sexpr s = sexpr{ sexpr(1,2), sexpr(2,3), sexpr(0,1) }; + std::cout << pp(sexpr{s, s, s, s, s}) << "\n"; + std::cout << pp(sexpr{sexpr(name{"test","name"}), sexpr(10), sexpr(10.20)}) << "\n"; + std::cout << pp(sexpr{sexpr(name{"test","name"}), sexpr(10), sexpr(10.20)}, options(name{"name","separator"}, "-->")) << "\n"; +} + int main() { continue_on_violation(true); tst1(); @@ -170,5 +179,6 @@ int main() { tst4(); tst5(); tst6(); + tst7(); return has_violations() ? 1 : 0; } diff --git a/src/util/format.cpp b/src/util/format.cpp index 3dddda8a0..8ff7d96bd 100644 --- a/src/util/format.cpp +++ b/src/util/format.cpp @@ -4,12 +4,23 @@ Author: Soonho Kong */ +#include #include "sexpr.h" #include "format.h" +#include "escaped.h" #include "sexpr_funcs.h" +#include "options.h" + +#ifndef LEAN_DEFAULT_INDENTATION +#define LEAN_DEFAULT_INDENTATION 4 +#endif + +#ifndef LEAN_DEFAULT_WIDTH +#define LEAN_DEFAULT_WIDTH 120 +#endif namespace lean { -static int default_width = 78; +static int default_width = LEAN_DEFAULT_WIDTH; std::ostream & layout(std::ostream & out, sexpr const & s) { lean_assert(!is_nil(s)); switch (format::sexpr_kind(s)) { @@ -53,7 +64,7 @@ std::ostream & layout(std::ostream & out, sexpr const & s) { } std::ostream & layout_list(std::ostream & out, sexpr const & s) { - foreach(s, [&out](sexpr const & s) { + for_each(s, [&out](sexpr const & s) { layout(out, s); }); return out; @@ -68,10 +79,35 @@ format nest(int i, format const & f) { format highlight(format const & f, format::format_color const c) { return format(format::sexpr_highlight(f.m_value, c)); } -format line() { +// Commonly used format objects +format mk_line() { return format(format::sexpr_line()); } - +static format g_line(mk_line()); +static format g_space(" "); +static format g_lp("("); +static format g_rp(")"); +static format g_comma(","); +static format g_dot("."); +format const & line() { + return g_line; +} +format const & space() { + return g_space; +} +format const & lp() { + return g_lp; +} +format const & rp() { + return g_rp; +} +format const & comma() { + return g_comma; +} +format const & dot() { + return g_dot; +} +// sexpr format::flatten(sexpr const & s) { lean_assert(is_cons(s)); switch (sexpr_kind(s)) { @@ -243,8 +279,7 @@ sexpr format::best(unsigned w, unsigned k, sexpr const & s) { return be(w, k, sexpr{sexpr(0, s)}); } -std::ostream & operator<<(std::ostream & out, format const & f) -{ +std::ostream & operator<<(std::ostream & out, format const & f) { return pretty(out, default_width, f); } @@ -260,4 +295,73 @@ std::ostream & pretty(std::ostream & out, unsigned w, format const & f) { sexpr const & b = format::best(w, 0, f.m_value); return layout_list(out, b); } + +static name g_pp_indent{"pp", "indent"}; + +unsigned get_pp_indent(options const & o) { + return o.get_int(g_pp_indent, LEAN_DEFAULT_INDENTATION); +} + +format pp(name const & n, char const * sep) { + return format(n.to_string(sep)); +} + +format pp(name const & n, options const & o) { + return pp(n, get_name_separator(o)); +} + +format pp(name const & n) { + return pp(n, get_name_separator(options())); +} + +struct sexpr_pp_fn { + char const * m_sep; + + format apply(sexpr const & s) { + switch (s.kind()) { + case sexpr_kind::NIL: return format("nil"); + case sexpr_kind::STRING: { + std::ostringstream ss; + ss << "\"" << escaped(to_string(s).c_str()) << "\""; + return format(ss.str()); + } + case sexpr_kind::BOOL: return format(to_bool(s) ? "true" : "false"); + case sexpr_kind::INT: return format(to_int(s)); + case sexpr_kind::DOUBLE: return format(to_double(s)); + case sexpr_kind::NAME: return pp(to_name(s), m_sep); + case sexpr_kind::MPZ: return format(to_mpz(s)); + case sexpr_kind::MPQ: return format(to_mpq(s)); + case sexpr_kind::CONS: { + sexpr const * curr = &s; + format r; + while (true) { + r += apply(head(*curr)); + curr = &tail(*curr); + if (is_nil(*curr)) { + return group(nest(1, format{lp(), r, rp()})); + } else if (!is_cons(*curr)) { + return group(nest(1, format{lp(), r, space(), dot(), line(), apply(*curr), rp()})); + } else { + r += line(); + } + } + }} + lean_unreachable(); + return format(); + } + + format operator()(sexpr const & s, options const & o) { + m_sep = get_name_separator(o); + return apply(s); + } +}; + +format pp(sexpr const & s, options const & o) { + return sexpr_pp_fn()(s, o); +} + +format pp(sexpr const & s) { + return pp(s, options()); +} + } diff --git a/src/util/format.h b/src/util/format.h index ebbdabf45..ab280dcf9 100644 --- a/src/util/format.h +++ b/src/util/format.h @@ -177,7 +177,7 @@ public: friend format compose(format const & f1, format const & f2); friend format nest(int i, format const & f); friend format highlight(format const & f, format::format_color const c = RED); - friend format line(); + friend format mk_line(); friend format group(format const & f); friend format above(format const & f1, format const & f2); @@ -208,7 +208,12 @@ format wrap(format const & f1, format const & f2); format compose(format const & f1, format const & f2); format nest(int i, format const & f); format highlight(format const & f, format::format_color const c); -format line(); +format const & line(); +format const & space(); +format const & lp(); +format const & rp(); +format const & comma(); +format const & dot(); format group(format const & f); format above(format const & f1, format const & f2); format bracket(std::string const l, format const & x, std::string const r); @@ -275,4 +280,16 @@ format fillwords(InputIterator first, InputIterator last) { inline format fillwords(std::initializer_list const & l) { return fillwords(l.begin(), l.end()); } +class options; +/** \brief Extract indentation from options */ +unsigned get_pp_indent(options const & o); + +/** \brief Format a hierarchical name */ +format pp(name const & n, char const * s); +format pp(name const & n, options const & o); +format pp(name const & n); + +/** \brief Format a S-expression */ +format pp(sexpr const & s, options const & o); +format pp(sexpr const & s); } diff --git a/src/util/name.cpp b/src/util/name.cpp index 96654704c..906286230 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -13,6 +13,11 @@ Author: Leonardo de Moura #include "rc.h" #include "hash.h" #include "trace.h" +#include "options.h" + +#ifndef LEAN_DEFAULT_NAME_SEPARATOR +#define LEAN_DEFAULT_NAME_SEPARATOR "::" +#endif namespace lean { @@ -263,6 +268,10 @@ size_t name::size(char const * sep) const { } } +size_t name::size() const { + return size(LEAN_DEFAULT_NAME_SEPARATOR); +} + unsigned name::hash() const { return m_ptr ? m_ptr->m_hash : 11; } @@ -273,8 +282,12 @@ std::string name::to_string(char const * sep) const { return s.str(); } +std::string name::to_string() const { + return to_string(LEAN_DEFAULT_NAME_SEPARATOR); +} + std::ostream & operator<<(std::ostream & out, name const & n) { - name::imp::display(out, default_name_separator, n.m_ptr); + name::imp::display(out, LEAN_DEFAULT_NAME_SEPARATOR, n.m_ptr); return out; } @@ -284,6 +297,12 @@ std::ostream & operator<<(std::ostream & out, name::sep const & s) { name::imp::display(out, s.m_sep, s.m_name.m_ptr); return out; } + +static name g_name_separator{"name", "separator"}; + +char const * get_name_separator(options const & o) { + return o.get_string(g_name_separator, LEAN_DEFAULT_NAME_SEPARATOR); +} } void print(lean::name const & n) { std::cout << n << std::endl; } diff --git a/src/util/name.h b/src/util/name.h index 29815f852..a225e88d7 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -9,7 +9,7 @@ Author: Leonardo de Moura namespace lean { -constexpr char const * default_name_separator = "\u2055"; +constexpr char const * default_name_separator = "::"; enum class name_kind { ANONYMOUS, STRING, NUMERAL }; /** @@ -53,11 +53,13 @@ public: /** \brief Convert this hierarchical name into a string using the given separator to "glue" the different limbs. */ - std::string to_string(char const * sep = default_name_separator) const; + std::string to_string(char const * sep) const; + std::string to_string() const; /** \brief Size of the this name (in characters) when using the given separator. */ - size_t size(char const * sep = default_name_separator) const; + size_t size(char const * sep) const; + size_t size() const; unsigned hash() const; friend std::ostream & operator<<(std::ostream & out, name const & n); class sep { @@ -71,4 +73,8 @@ public: }; struct name_hash { unsigned operator()(name const & n) const { return n.hash(); } }; struct name_eq { bool operator()(name const & n1, name const & n2) const { return n1 == n2; } }; + +class options; +/** \brief Return the separator for hierarchical names */ +char const * get_name_separator(options const & o); } diff --git a/src/util/options.cpp b/src/util/options.cpp index 114827d24..6e9909846 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -27,7 +27,7 @@ bool options::contains(char const * n) const { sexpr const & options::get_sexpr(name const & n, sexpr const & default_value) const { sexpr const * r = find(m_value, [&](sexpr const & p) { return to_name(head(p)) == n; }); - return r == nullptr ? default_value : *r; + return r == nullptr ? default_value : tail(*r); } int options::get_int(name const & n, int default_value) const { @@ -45,6 +45,11 @@ double options::get_double(name const & n, double default_value) const { return !is_nil(r) && is_double(r) ? to_double(r) : default_value; } +char const * options::get_string(name const & n, char const * default_value) const { + sexpr const & r = get_sexpr(n); + return !is_nil(r) && is_string(r) ? to_string(r).c_str() : default_value; +} + sexpr const & options::get_sexpr(char const * n, sexpr const & default_value) const { sexpr const * r = find(m_value, [&](sexpr const & p) { return to_name(head(p)) == n; }); return r == nullptr ? default_value : *r; @@ -65,27 +70,40 @@ double options::get_double(char const * n, double default_value) const { return !is_nil(r) && is_double(r) ? to_double(r) : default_value; } -constexpr char const * left_angle_bracket = "\u27E8"; -constexpr char const * right_angle_bracket = "\u27E9"; -constexpr char const * arrow = "\u21a6"; +char const * options::get_string(char const * n, char const * default_value) const { + sexpr const & r = get_sexpr(n); + return !is_nil(r) && is_string(r) ? to_string(r).c_str() : default_value; +} + +static char const * g_left_angle_bracket = "\u27E8"; +static char const * g_right_angle_bracket = "\u27E9"; +static char const * g_arrow = "\u21a6"; options options::update(name const & n, sexpr const & v) const { return options(cons(cons(sexpr(n), v), m_value)); } format pp(options const & o) { - // TODO - return format(); + char const * sep = get_name_separator(o); + format r; + bool first = true; + for_each(o.m_value, [&](sexpr const & p) { + if (first) { first = false; } else { r += comma(); r += line(); } + name const & n = to_name(head(p)); + unsigned sz = n.size(sep); + r += group(nest(sz+3, format{pp(head(p), o), space(), format(g_arrow), space(), pp(tail(p), o)})); + }); + return group(nest(1, format{format(g_left_angle_bracket), r, format(g_right_angle_bracket)})); } std::ostream & operator<<(std::ostream & out, options const & o) { - out << left_angle_bracket; + out << g_left_angle_bracket; bool first = true; - foreach(o.m_value, [&](sexpr const & p) { + for_each(o.m_value, [&](sexpr const & p) { if (first) first = false; else out << ", "; - out << head(p) << " " << arrow << " " << tail(p); + out << head(p) << " " << g_arrow << " " << tail(p); }); - out << right_angle_bracket; + out << g_right_angle_bracket; return out; } } diff --git a/src/util/options.h b/src/util/options.h index c51c2c3e8..7fe269077 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #include "sexpr.h" #include "format.h" #include "name.h" @@ -18,6 +19,7 @@ public: options() {} options(options const & o):m_value(o.m_value) {} options(options && o):m_value(std::move(o.m_value)) {} + template options(name const & n, T const & t) { *this = update(n, t); } ~options() {} options & operator=(options const & o) { m_value = o.m_value; return *this; } @@ -30,11 +32,13 @@ public: bool get_bool(name const & n, bool default_value=false) const; int get_int(name const & n, int default_value=0) const; double get_double(name const & n, double default_value=0.0) const; + char const * get_string(name const & n, char const * default_value=nullptr) const; sexpr const & get_sexpr(name const & n, sexpr const & default_value=sexpr()) const; bool get_bool(char const * n, bool default_value=false) const; int get_int(char const * n, int default_value=0) const; double get_double(char const * n, double default_value=0.0) const; + char const * get_string(char const * n, char const * default_value=nullptr) const; sexpr const & get_sexpr(char const * n, sexpr const & default_value=sexpr()) const; options update(name const & n, sexpr const & v) const; diff --git a/src/util/sexpr_funcs.h b/src/util/sexpr_funcs.h index 376070101..6f9326995 100644 --- a/src/util/sexpr_funcs.h +++ b/src/util/sexpr_funcs.h @@ -11,7 +11,7 @@ Author: Leonardo de Moura namespace lean { template -void foreach(sexpr const & l, F f) { +void for_each(sexpr const & l, F f) { static_assert(std::is_same::type, void>::value, "foreach: return type of f is not void"); lean_assert(is_list(l));