Add pretty printer for s-expressions and options

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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;
 }

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;
 }

src/util/format.cpp

@@ -4,12 +4,23 @@
 
   Author: Soonho Kong
 */
+#include <sstream>
 #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());
+}
+
 }

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<std::string> 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);
 }

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; }

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);
 }

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";
+char const * options::get_string(char const * n, char const * default_value) const {
-constexpr char const * right_angle_bracket = "\u27E9";
+    sexpr const & r = get_sexpr(n);
-constexpr char const * arrow               = "\u21a6";
+    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
+    char const * sep = get_name_separator(o);
-    return format();
+    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;
 }
 }

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 <algorithm>
 #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<typename T> 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;

src/util/sexpr_funcs.h

@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 namespace lean {
 
 template<typename F>
-void foreach(sexpr const & l, F f) {
+void for_each(sexpr const & l, F f) {
     static_assert(std::is_same<typename std::result_of<F(sexpr const &)>::type, void>::value,
                   "foreach: return type of f is not void");
     lean_assert(is_list(l));