Add output_channel and state abstractions

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

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

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

src/exprlib/formatter.h

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <memory>
 #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<formatter_cell> const & c):m_cell(c) {}
-    format operator()(expr const & e) { return (*m_cell)(e); }
+    format operator()(expr const & e, options const & opts = options()) { return (*m_cell)(e, opts); }
-    format operator()(context const & c) { return (*m_cell)(c); }
+    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) { return (*m_cell)(c, e, format_ctx); }
+    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) { return (*m_cell)(obj); }
+    format operator()(object const & obj, options const & opts = options()) { return (*m_cell)(obj, opts); }
-    format operator()(environment const & env) { return (*m_cell)(env); }
+    format operator()(environment const & env, options const & opts = options()) { return (*m_cell)(env, opts); }
 };
 
 formatter mk_simple_formatter();

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<output_channel> const & out) {
+    m_regular_channel = out;
+}
+
+void state::set_diagnostic_channel(std::shared_ptr<output_channel> 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;
+}
+}

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<output_channel> m_regular_channel;
+    std::shared_ptr<output_channel> 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<output_channel> const & out);
+    void set_diagnostic_channel(std::shared_ptr<output_channel> 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<typename T>
+inline regular const & operator<<(regular const & out, T const & t) {
+    out.m_state.get_regular_channel().get_stream() << t;
+    return out;
+}
+
+template<typename T>
+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;
+}
+}

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<imp> 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<imp> 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<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

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <memory>
 #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<output_channel> const & out);
+    void set_diagnostic_channel(std::shared_ptr<output_channel> const & out);
+    /*@}*/
 };
 }

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) {
+    format pp(expr const & e, options const & opts) {
-        return pp_fn(m_frontend, m_options)(e);
+        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)};
+                            pp(t, opts), space(), g_assign_fmt, line(), pp(v, opts)};
-        return group(nest(m_indent, def));
+        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) {
+    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())};
+        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) {
+    format pp_definition(object const & obj, options const & opts) {
-        return pp_compact_definition(obj.keyword(), obj.get_name(), obj.get_type(), obj.get_value());
+        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<notation_declaration const *>(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):
+    pp_formatter_cell(frontend const & fe):
-        m_frontend(fe),
+        m_frontend(fe) {
-        m_options(opts) {
-        m_indent = get_pp_indent(opts);
     }
 
     virtual ~pp_formatter_cell() {
     }
 
-    virtual format operator()(expr const & e) {
+    virtual format operator()(expr const & e, options const & opts) {
-        return pp(e);
+        return pp(e, opts);
     }
 
-    virtual format operator()(context const & c) {
+    virtual format operator()(context const & c, options const & opts) {
-        return pp(c, Type(), false);
+        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::UVarDeclaration:  return pp_uvar_decl(obj, opts);
-        case object_kind::Postulate:        return pp_postulate(obj);
+        case object_kind::Postulate:        return pp_postulate(obj, opts);
-        case object_kind::Definition:       return pp_definition(obj);
+        case object_kind::Definition:       return pp_definition(obj, opts);
         case object_kind::Neutral:
             if (dynamic_cast<notation_declaration const *>(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) {
+formatter mk_pp_formatter(frontend const & fe) {
-    return formatter(new pp_formatter_cell(fe, opts));
+    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;
 }

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

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));
+    formatter fmt2 = mk_pp_formatter(f);
-    std::cout << fmt2(g(t, t, t)) << std::endl;
+    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;
 }

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 <iostream>
+#include <fstream>
+
+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<output_channel> 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<typename T>
+output_channel & operator<<(output_channel & out, T const & v) {
+    out.get_stream() << v;
+    return out;
+}
+}