Remove pretty printer from kernel. Add basic printing capability to exprlib module.

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

src/exprlib/CMakeLists.txt

@@ -1,2 +1,2 @@
-add_library(exprlib basic_thms.cpp deep_copy.cpp max_sharing.cpp toplevel.cpp)
+add_library(exprlib basic_thms.cpp deep_copy.cpp max_sharing.cpp toplevel.cpp printer.cpp)
 target_link_libraries(exprlib ${LEAN_LIBS})

src/exprlib/printer.cpp

@@ -4,34 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "expr_formatter.h"
+#include <algorithm>
+#include "printer.h"
+#include "environment.h"
 #include "exception.h"
 
 namespace lean {
-
-format expr_formatter::operator()(char const * kwd, name const & n, expr const & t, expr const & v) {
-    format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(),
-                        operator()(t), space(), highlight_keyword(format(":=")), line(), operator()(v)};
-    return group(nest(def));
-}
-
-format expr_formatter::operator()(char const * kwd, name const & n, expr const & t) {
-    format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(), operator()(t)};
-    return group(nest(def));
-}
-
-void expr_formatter::pp(std::ostream & out, expr const & e, context const & c) {
-    out << mk_pair(operator()(e, c), get_options());
-}
-
-void expr_formatter::pp(std::ostream & out, expr const & e) {
-    pp(out, e, context());
-}
-
-format expr_formatter::nest(format const & f) {
-    return ::lean::nest(get_pp_indent(get_options()), f);
-}
-
 bool is_atomic(expr const & e) {
     switch (e.kind()) {
     case expr_kind::Var: case expr_kind::Constant: case expr_kind::Value: case expr_kind::Type:
@@ -42,10 +20,10 @@ bool is_atomic(expr const & e) {
     return false;
 }
 
-class simple_expr_formatter : public expr_formatter {
+struct print_expr_fn {
-    static thread_local std::ostream * m_out;
+    std::ostream & m_out;
 
-    std::ostream & out() { return *m_out; }
+    std::ostream & out() { return m_out; }
 
     void print_child(expr const & a, context const & c) {
         if (is_atomic(a)) {
@@ -142,42 +120,54 @@ class simple_expr_formatter : public expr_formatter {
         }
     }
 
-public:
+    print_expr_fn(std::ostream & out):m_out(out) {}
-    virtual ~simple_expr_formatter() {}
 
-    virtual format operator()(expr const & e, context const & c) {
+    void operator()(expr const & e, context const & c) {
-        std::ostringstream s;
-        m_out = &s;
         print(e, c);
-        return format(s.str());
-    }
-
-    virtual bool has_location(expr const & e) const { return false; }
-
-    virtual std::pair<unsigned, unsigned> get_location(expr const & e) const { return mk_pair(0,0); }
-
-    virtual options get_options() const { return options(); }
-
-    void print(std::ostream & out, expr const & a, context const & c) {
-        m_out = &out;
-        print(a, c);
     }
 };
-thread_local std::ostream * simple_expr_formatter::m_out = 0;
 
-std::shared_ptr<expr_formatter> mk_simple_expr_formatter() {
+std::ostream & operator<<(std::ostream & out, expr const & e) {
-    return std::shared_ptr<expr_formatter>(new simple_expr_formatter());
+    print_expr_fn pr(out);
-}
+    pr(e, context());
-
-std::ostream & operator<<(std::ostream & out, std::pair<expr_formatter &, expr const &> const & p) {
-    p.first.pp(out, p.second);
     return out;
 }
 
-static simple_expr_formatter g_simple_formatter;
+std::ostream & operator<<(std::ostream & out, std::pair<expr const &, context const &> const & p) {
+    print_expr_fn pr(out);
+    pr(p.first, p.second);
+    return out;
+}
 
-std::ostream & operator<<(std::ostream & out, expr const & a) {
+std::ostream & operator<<(std::ostream & out, context const & ctx) {
-    g_simple_formatter.print(out, a, context());
+    if (ctx) {
+        out << tail(ctx);
+        out << head(ctx).get_name() << " : " << head(ctx).get_domain();
+        if (head(ctx).get_body()) {
+            out << " := " << head(ctx).get_body();
+        }
+        out << "\n";
+    }
+    return out;
+}
+
+std::ostream & operator<<(std::ostream & out, environment const & env) {
+    std::for_each(env.begin_objects(),
+                  env.end_objects(),
+                  [&](object const & obj) {
+                      out << obj.keyword() << " ";
+                      switch (obj.kind()) {
+                      case object_kind::UVarDeclaration:
+                          out << obj.get_name() << " >= " << obj.get_cnstr_level(); break;
+                      case object_kind::Postulate:
+                          out << obj.get_name() << " : " << obj.get_type(); break;
+                      case object_kind::Definition:
+                          out << obj.get_name() << " : " << obj.get_type() << " :=\n    " << obj.get_value(); break;
+                      case object_kind::Neutral:
+                          break;
+                      }
+                      out << "\n";
+                  });
     return out;
 }
 }

src/exprlib/printer.h

@@ -0,0 +1,18 @@
+/*
+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 "expr.h"
+#include "context.h"
+
+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<context const &, expr const &> const & p);
+class environment;
+std::ostream & operator<<(std::ostream & out, environment const & env);
+}

src/frontend/frontend.cpp

@@ -214,7 +214,6 @@ struct frontend::imp {
 frontend::frontend():m_imp(new imp(*this)) {
     init_builtin_notation(*this);
     init_toplevel(m_imp->m_env);
-    m_imp->m_env.set_formatter(mk_pp_expr_formatter(*this, options()));
 }
 frontend::frontend(imp * new_ptr):m_imp(new_ptr) {}
 frontend::frontend(std::shared_ptr<imp> const & ptr):m_imp(ptr) {}

src/frontend/pp.cpp

@@ -6,15 +6,42 @@ Author: Leonardo de Moura
 */
 #include <limits>
 #include <memory>
+#include "pp.h"
 #include "frontend.h"
 #include "context.h"
 #include "scoped_map.h"
-#include "expr_formatter.h"
 #include "occurs.h"
 #include "instantiate.h"
 #include "builtin_notation.h"
 #include "options.h"
 
+namespace lean {
+
+format expr_formatter::operator()(char const * kwd, name const & n, expr const & t, expr const & v) {
+    format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(),
+                        operator()(t), space(), highlight_keyword(format(":=")), line(), operator()(v)};
+    return group(nest(def));
+}
+
+format expr_formatter::operator()(char const * kwd, name const & n, expr const & t) {
+    format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(), operator()(t)};
+    return group(nest(def));
+}
+
+void expr_formatter::pp(std::ostream & out, expr const & e, context const & c) {
+    out << mk_pair(operator()(e, c), get_options());
+}
+
+void expr_formatter::pp(std::ostream & out, expr const & e) {
+    pp(out, e, context());
+}
+
+format expr_formatter::nest(format const & f) {
+    return ::lean::nest(get_pp_indent(get_options()), f);
+}
+
+}
+
 #ifndef LEAN_DEFAULT_PP_MAX_DEPTH
 #define LEAN_DEFAULT_PP_MAX_DEPTH std::numeric_limits<unsigned>::max()
 #endif

src/frontend/pp.h

@@ -5,8 +5,28 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "expr_formatter.h"
+#include "context.h"
 
 namespace lean {
+class frontend;
+class expr_formatter {
+public:
+    virtual ~expr_formatter() {}
+    /** \brief Convert expression in the given context into a format object. */
+    virtual format operator()(expr const & e, context const & c = context()) = 0;
+    /** \brief format a definition. */
+    virtual format operator()(char const * kwd, name const & n, expr const & t, expr const & v);
+    /** \brief format a postulate. */
+    virtual format operator()(char const * kwd, name const & n, expr const & t);
+
+    /** \brief Return options for pretty printing. */
+    virtual options get_options() const = 0;
+
+    void pp(std::ostream & out, expr const & e, context const & c);
+    void pp(std::ostream & out, expr const & e);
+
+    /** \brief Nest the given format object using the setting provided by get_options. */
+    format nest(format const & f);
+};
 std::shared_ptr<expr_formatter> mk_pp_expr_formatter(frontend const & fe, options const & opts);
 }

src/kernel/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
   normalize.cpp context.cpp level.cpp object.cpp environment.cpp
-  type_check.cpp builtin.cpp expr_formatter.cpp occurs.cpp)
+  type_check.cpp builtin.cpp occurs.cpp)
 
 target_link_libraries(kernel ${LEAN_LIBS})

src/kernel/context.cpp

@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #include "context.h"
 #include "occurs.h"
 #include "exception.h"
-#include "expr_formatter.h"
 
 namespace lean {
 context sanitize_names_core(context const & c, context const & r, unsigned sz, expr const * es) {
@@ -35,37 +34,6 @@ context sanitize_names(context const & c, unsigned sz, expr const * es) {
     return sanitize_names_core(c, c, sz, es);
 }
 
-format pp(expr_formatter & fmt, context const & c) {
-    if (c) {
-        format r;
-        if (tail(c))
-            r = format{pp(fmt, tail(c)), line()};
-        context_entry const & e = head(c);
-        format new_entry;
-        unsigned name_sz;
-        if (e.get_name().is_anonymous()) {
-            new_entry = format("_");
-            name_sz = 1;
-        } else {
-            new_entry = format(e.get_name());
-            name_sz = e.get_name().size();
-        }
-        new_entry += format{space(), colon(), space(), nest(name_sz + 3, fmt(e.get_domain(), tail(c)))};
-        if (e.get_body())
-            new_entry += format{space(), format(":="), fmt.nest(format{line(), fmt(e.get_body(), tail(c))})};
-        r += group(new_entry);
-        return r;
-    } else {
-        return format();
-    }
-}
-
-std::ostream & operator<<(std::ostream & out, context const & c) {
-    auto fmt = mk_simple_expr_formatter();
-    out << pp(*fmt, c);
-    return out;
-}
-
 std::pair<context_entry const &, context const &> lookup_ext(context const & c, unsigned i) {
     context const * it1 = &c;
     while (*it1) {

src/kernel/context.h

@@ -57,8 +57,4 @@ inline bool is_empty(context const & c) {
 context sanitize_names(context const & c, unsigned sz, expr const * es);
 inline context sanitize_names(context const & c, expr const & e) { return sanitize_names(c, 1, &e); }
 inline context sanitize_names(context const & c, std::initializer_list<expr> const & l) { return sanitize_names(c, l.size(), l.begin()); }
-
-class expr_formatter;
-format pp(expr_formatter & f, context const & c);
-std::ostream & operator<<(std::ostream & out, context const & c);
 }

src/kernel/environment.cpp

@@ -32,18 +32,6 @@ struct environment::imp {
     // Object management
     std::vector<object>                  m_objects;
     object_dictionary                    m_object_dictionary;
-    // Expression formatter && locator
-    std::shared_ptr<expr_formatter>      m_formatter;
-
-    expr_formatter & get_formatter() {
-        if (m_formatter) {
-            return *m_formatter;
-        } else {
-            // root environments always have a formatter.
-            lean_assert(has_parent());
-            return m_parent->get_formatter();
-        }
-    }
 
     /**
        \brief Return true iff this environment has children.
@@ -317,7 +305,6 @@ struct environment::imp {
     imp():
         m_num_children(0) {
         init_uvars();
-        m_formatter = mk_simple_expr_formatter();
     }
 
     explicit imp(std::shared_ptr<imp> const & parent):
@@ -347,15 +334,6 @@ environment::environment(std::shared_ptr<imp> const & ptr):
 environment::~environment() {
 }
 
-void environment::set_formatter(std::shared_ptr<expr_formatter> const & formatter) {
-    lean_assert(formatter);
-    m_imp->m_formatter = formatter;
-}
-
-expr_formatter & environment::get_formatter() const {
-    return m_imp->get_formatter();
-}
-
 environment environment::mk_child() const {
     return environment(new imp(m_imp));
 }

src/kernel/environment.h

@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 #include <memory>
 #include "object.h"
 #include "level.h"
-#include "expr_formatter.h"
 
 namespace lean {
 /**
@@ -28,13 +27,6 @@ private:
 public:
     environment();
     ~environment();
-
-    /** \brief Set expression formatter. */
-    void set_formatter(std::shared_ptr<expr_formatter> const & formatter);
-
-    /** \brief Return expression formatter. */
-    expr_formatter & get_formatter() const;
-
     // =======================================
     // Parent/Child environment management
     /**
@@ -172,5 +164,4 @@ public:
     /** \brief Display universal variable constraints and objects stored in this environment and its parents. */
     void display(std::ostream & out) const;
 };
-inline std::ostream & operator<<(std::ostream & out, environment const & env) { env.display(out); return out; }
 }

src/kernel/expr_formatter.h

@@ -1,40 +0,0 @@
-/*
-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 <memory>
-#include "context.h"
-#include "options.h"
-
-namespace lean {
-/** \brief Abstract class for formatting expressions. */
-class expr_formatter {
-public:
-    virtual ~expr_formatter() {}
-    /** \brief Convert expression in the given context into a format object. */
-    virtual format operator()(expr const & e, context const & c = context()) = 0;
-    /** \brief format a definition. */
-    virtual format operator()(char const * kwd, name const & n, expr const & t, expr const & v);
-    /** \brief format a postulate. */
-    virtual format operator()(char const * kwd, name const & n, expr const & t);
-
-    /** \brief Return options for pretty printing. */
-    virtual options get_options() const = 0;
-
-    void pp(std::ostream & out, expr const & e, context const & c);
-    void pp(std::ostream & out, expr const & e);
-
-    /** \brief Nest the given format object using the setting provided by get_options. */
-    format nest(format const & f);
-};
-
-/**
-    \brief Create simple expression formatter.
-    It is mainly useful for pretty printing.
-*/
-std::shared_ptr<expr_formatter> mk_simple_expr_formatter();
-std::ostream & operator<<(std::ostream & out, std::pair<expr_formatter &, expr const &> const & p);
-}

src/kernel/type_check.cpp

@@ -35,7 +35,6 @@ bool is_convertible_core(expr const & expected, expr const & given, environment
 }
 
 bool is_convertible(expr const & expected, expr const & given, environment const & env, context const & ctx) {
-    lean_trace("is_convertible", tout << expected << "\n" << given << "\n" << ctx << "\n";);
     if (is_convertible_core(expected, given, env))
         return true;
     expr e_n = normalize(expected, env, ctx);
@@ -82,8 +81,6 @@ struct infer_type_fn {
     }
 
     expr infer_type(expr const & e, context const & ctx) {
-        lean_trace("type_check", tout << "infer type\n" << e << "\n" << ctx << "\n";);
-
         bool shared = false;
         if (is_shared(e)) {
             shared = true;

src/tests/kernel/environment.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "kernel_exception.h"
 #include "environment.h"
 #include "type_check.h"
+#include "printer.h"
 #include "toplevel.h"
 #include "builtin.h"
 #include "arith.h"

src/tests/kernel/level.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <locale>
 #include "environment.h"
 #include "exception.h"
+#include "printer.h"
 #include "test.h"
 using namespace lean;
 

src/tests/kernel/occurs.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "occurs.h"
 #include "abstract.h"
+#include "printer.h"
 using namespace lean;
 
 static void tst1() {
@@ -44,14 +45,15 @@ static void tst2() {
     expr b = Const("b");
     context c;
     c = extend(c, "a", Type());
+    std::cout << c;
     lean_assert(length(c) == 1);
     lean_assert(lookup(c, 0).get_name() == "a");
     auto p = lookup_ext(c, 0);
     lean_assert(p.first.get_name() == "a");
     lean_assert(length(p.second) == 0);
-    std::cout << sanitize_names(c, f(a)) << "\n";
+    std::cout << sanitize_names(c, f(a));
     lean_assert(lookup(sanitize_names(c, f(a)), 0).get_name() != name("a"));
-    std::cout << sanitize_names(c, f(b)) << "\n";
+    std::cout << sanitize_names(c, f(b));
 }
 
 int main() {