Add methods for setting options. Add string output channel.

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

src/exprlib/state.cpp

@@ -23,11 +23,13 @@ state::state(options const & opts, formatter const & fmt):
 state::~state() {}
 
 void state::set_regular_channel(std::shared_ptr<output_channel> const & out) {
-    m_regular_channel = out;
+    if (out)
+        m_regular_channel = out;
 }
 
 void state::set_diagnostic_channel(std::shared_ptr<output_channel> const & out) {
-    m_diagnostic_channel = out;
+    if (out)
+        m_diagnostic_channel = out;
 }
 
 void state::set_options(options const & opts) {

src/exprlib/state.h

@@ -36,6 +36,9 @@ public:
     void set_diagnostic_channel(std::shared_ptr<output_channel> const & out);
     void set_options(options const & opts);
     void set_formatter(formatter const & f);
+    template<typename T> void set_option(name const & n, T const & v) {
+        set_options(get_options().update(n, v));
+    }
 };
 
 struct regular {
@@ -61,12 +64,14 @@ inline diagnostic const & operator<<(diagnostic const & out, T const & t) {
 }
 
 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());
+    options const & opts = out.m_state.get_options();
+    out.m_state.get_regular_channel().get_stream() << mk_pair(out.m_state.get_formatter()(e, opts), opts);
     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());
+    options const & opts = out.m_state.get_options();
+    out.m_state.get_diagnostic_channel().get_stream() << mk_pair(out.m_state.get_formatter()(e, opts), opts);
     return out;
 }
 }

src/frontend/frontend.cpp

@@ -231,6 +231,7 @@ operator_info frontend::find_nud(name const & n) const { return m_imp->find_nud(
 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; }
+state & frontend::get_state_core() { 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<output_channel> const & out) { return m_imp->m_state.set_regular_channel(out); }
 void frontend::set_diagnostic_channel(std::shared_ptr<output_channel> const & out) { return m_imp->m_state.set_diagnostic_channel(out); }

src/frontend/frontend.h

@@ -20,6 +20,7 @@ class frontend {
     std::shared_ptr<imp> m_imp;
     explicit frontend(imp * new_ptr);
     explicit frontend(std::shared_ptr<imp> const & ptr);
+    state & get_state_core();
 public:
     frontend();
     ~frontend();
@@ -122,6 +123,7 @@ public:
     state const & get_state() const;
     operator state const &() const { return get_state(); }
     void set_options(options const & opts);
+    template<typename T> void set_option(name const & n, T const & v) { get_state_core().set_option(n, v); }
     void set_regular_channel(std::shared_ptr<output_channel> const & out);
     void set_diagnostic_channel(std::shared_ptr<output_channel> const & out);
     /*@}*/

src/frontend/pp.cpp

@@ -688,7 +688,7 @@ class pp_fn {
     }
 
     result pp(expr const & e, unsigned depth, bool main = false) {
-        if (m_num_steps > m_max_steps || depth > m_max_depth) {
+        if (!is_atomic(e) && (m_num_steps > m_max_steps || depth > m_max_depth)) {
             return pp_ellipsis();
         } else {
             m_num_steps++;

src/tests/frontend/pp.cpp

@@ -59,10 +59,44 @@ static void tst3() {
 
 static void tst4() {
     frontend f;
-    state const & s = f.get_state();
-    regular(s) << And(Const("a"), Const("b")) << "\n";
+    state const & s1 = f.get_state();
+    state s2 = f.get_state();
+    regular(s1) << And(Const("a"), Const("b")) << "\n";
     regular(f) << And(Const("a"), Const("b")) << "\n";
     diagnostic(f) << And(Const("a"), Const("b")) << "\n";
+    f.set_option(name{"pp", "notation"}, false);
+    regular(f) << And(Const("a"), Const("b")) << "\n";
+    regular(s1) << And(Const("a"), Const("b")) << "\n";
+    regular(s2) << And(Const("a"), Const("b")) << "\n";
+}
+
+static void tst5() {
+    frontend f;
+    std::shared_ptr<string_output_channel> out(new string_output_channel());
+    f.set_regular_channel(out);
+    regular(f) << And(Const("a"), Const("b"));
+    lean_assert(out->str() == "a ∧ b");
+    f.set_option(name{"pp", "notation"}, false);
+    regular(f) << " " << And(Const("a"), Const("b"));
+    lean_assert(out->str() == "a ∧ b and a b");
+}
+
+static expr mk_deep(unsigned depth) {
+    if (depth == 0)
+        return Const("a");
+    else
+        return Const("f")(mk_deep(depth - 1));
+}
+
+static void tst6() {
+    frontend f;
+    std::shared_ptr<string_output_channel> out(new string_output_channel());
+    f.set_regular_channel(out);
+    expr t = mk_deep(10);
+    f.set_option(name{"pp", "max_depth"}, 5);
+    f.set_option(name{"pp", "colors"}, false);
+    regular(f) << t;
+    lean_assert(out->str() == "f (f (f (f (f (…)))))");
 }
 
 int main() {
@@ -70,5 +104,7 @@ int main() {
     tst2();
     tst3();
     tst4();
+    tst5();
+    tst6();
     return has_violations() ? 1 : 0;
 }

src/tests/util/options.cpp

@@ -28,8 +28,20 @@ static void tst2() {
     std::cout << pp(opt) << "\n";
 }
 
+static void tst3() {
+    options opt;
+    opt = update(opt, name{"test", "foo"}, 10);
+    opt = update(opt, name{"color"}, 20);
+    std::cout << pp(opt) << "\n";
+    opt = update(opt, name{"color"}, 20);
+    std::cout << pp(opt) << "\n";
+    opt = update(opt, name{"color"}, 30);
+    std::cout << pp(opt) << "\n";
+}
+
 int main() {
     tst1();
     tst2();
+    tst3();
     return has_violations() ? 1 : 0;
 }

src/util/output_channel.h

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <iostream>
 #include <fstream>
+#include <sstream>
 
 namespace lean {
 /**
@@ -42,6 +43,14 @@ public:
     virtual ~file_output_channel() {}
     virtual std::ostream & get_stream() { return m_out; }
 };
+class string_output_channel : public output_channel {
+    std::ostringstream m_out;
+public:
+    string_output_channel() {}
+    virtual ~string_output_channel() {}
+    virtual std::ostream & get_stream() { return m_out; }
+    std::string str() const { return m_out.str(); }
+};
 template<typename T>
 output_channel & operator<<(output_channel & out, T const & v) {
     out.get_stream() << v;

src/util/sexpr/options.cpp

@@ -90,7 +90,25 @@ 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));
+    if (contains(n)) {
+        return map(m_value, [&](sexpr const & p) {
+                if (to_name(car(p)) == n)
+                    return cons(car(p), v);
+                else
+                    return p;
+            });
+    } else {
+        return options(cons(cons(sexpr(n), v), m_value));
+    }
+}
+
+options join(options const & opts1, options const & opts2) {
+    sexpr r = opts2.m_value;
+    for_each(opts1.m_value, [&](sexpr const & p) {
+            if (!opts2.contains(to_name(car(p))))
+                r = cons(p, r);
+        });
+    return options(r);
 }
 
 format pp(options const & o) {

src/util/sexpr/options.h

@@ -48,6 +48,12 @@ public:
     options update(char const * n, sexpr const & v) const { return update(name(n), v); }
     template<typename T> options update(char const * n, T v) const { return update(n, sexpr(v)); }
 
+    /**
+       \brief Combine the options opts1 and opts2. The assignment in
+       opts2 overrides the ones in opts1.
+    */
+    friend options join(options const & opts1, options const & opts2);
+
     friend format pp(options const & o);
     friend std::ostream & operator<<(std::ostream & out, options const & o);
 };