refactor(kernel): move printer to library, cleanup io_state interface

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

src/frontends/lean/frontend.cpp

@@ -557,22 +557,21 @@ static lean_extension & to_ext(environment const & env) {
     return env->get_extension<lean_extension>(g_lean_extension_initializer.m_extid);
 }
 
-void init_frontend(environment const & env, io_state & ios, bool no_kernel) {
-    ios.set_formatter(mk_pp_formatter(env));
+io_state init_frontend(environment const & env, bool no_kernel) {
+    io_state ios(mk_pp_formatter(env));
     if (!no_kernel) {
         import_kernel(env, ios);
         import_nat(env, ios);
     }
+    return ios;
 }
-void init_test_frontend(environment const & env, io_state & ios) {
+
+io_state init_test_frontend(environment const & env) {
     env->set_trusted_imported(true);
-    init_frontend(env, ios);
+    io_state ios = init_frontend(env);
     import_int(env, ios);
     import_real(env, ios);
-}
-void init_test_frontend(environment const & env) {
-    io_state ios;
-    init_test_frontend(env, ios);
+    return ios;
 }
 
 void add_infix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d)  {

src/frontends/lean/frontend.h

@@ -16,14 +16,13 @@ namespace lean {
 /**
    \brief Load kernel, nat and set pretty printer.
 */
-void init_frontend(environment const & env, io_state & ios, bool no_kernel = false);
+io_state init_frontend(environment const & env, bool no_kernel = false);
 
 /*
   \brief Load kernel, nat, int, real and set pretty printer.
   It is used for testing.
 */
-void init_test_frontend(environment const & env, io_state & ios);
-void init_test_frontend(environment const & env);
+io_state init_test_frontend(environment const & env);
 
 /**
    @name Notation for parsing and pretty printing.

src/frontends/lean/parser.cpp

@@ -16,8 +16,7 @@ parser::parser(environment const & env, io_state const & ios, std::istream & in,
 }
 
 parser::parser(environment const & env, std::istream & in, script_state * S, bool use_exceptions, bool interactive):
-    parser(env, io_state(), in, S, use_exceptions, interactive) {
-    m_ptr->m_io_state.set_formatter(mk_pp_formatter(m_ptr->m_env));
+    parser(env, io_state(mk_pp_formatter(m_ptr->m_env)), in, S, use_exceptions, interactive) {
 }
 
 parser::~parser() {

src/frontends/lean/register_module.cpp

@@ -127,8 +127,7 @@ static int parse_lean_cmds(lua_State * L) {
 
 static int mk_environment(lua_State * L) {
     environment env;
-    io_state ios;
-    init_frontend(env, ios);
+    io_state ios = init_frontend(env);
     return push_environment(L, env);
 }
 

src/frontends/lean/shell.cpp

@@ -91,8 +91,7 @@ static readline_config g_readline_config;
 shell::shell(environment const & env, io_state const & ios, script_state * S):m_env(env), m_io_state(ios), m_script_state(S) {
 }
 
-shell::shell(environment const & env, script_state * S):m_env(env), m_io_state(), m_script_state(S) {
-    m_io_state.set_formatter(mk_pp_formatter(m_env));
+shell::shell(environment const & env, script_state * S):m_env(env), m_io_state(mk_pp_formatter(m_env)), m_script_state(S) {
 }
 
 shell::~shell() {

src/kernel/CMakeLists.txt

@@ -1,9 +1,8 @@
 add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
   normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
   type_checker.cpp builtin.cpp occurs.cpp metavar.cpp
-  justification.cpp unification_constraint.cpp printer.cpp
-  formatter.cpp kernel_exception.cpp type_checker_justification.cpp
-  pos_info_provider.cpp replace_visitor.cpp update_expr.cpp
-  io_state.cpp)
+  justification.cpp unification_constraint.cpp kernel_exception.cpp
+  type_checker_justification.cpp pos_info_provider.cpp
+  replace_visitor.cpp update_expr.cpp io_state.cpp)
 
 target_link_libraries(kernel ${LEAN_LIBS})

src/kernel/formatter.cpp

@@ -10,29 +10,4 @@ Author: Leonardo de Moura
 #include "kernel/formatter.h"
 
 namespace lean {
-class simple_formatter_cell : public formatter_cell {
-public:
-    virtual format operator()(expr const & e, options const &) {
-        std::ostringstream s; s << e; return format(s.str());
-    }
-    virtual format operator()(context const & c, options const &) {
-        std::ostringstream s; s << c; return format(s.str());
-    }
-    virtual format operator()(context const & c, expr const & e, bool format_ctx, options const &) {
-        std::ostringstream s;
-        if (format_ctx)
-            s << c << " |- ";
-        s << mk_pair(e, c);
-        return format(s.str());
-    }
-    virtual format operator()(object const & obj, options const &) {
-        std::ostringstream s; s << obj; return format(s.str());
-    }
-    virtual format operator()(ro_environment const & env, options const &) {
-        std::ostringstream s; s << env; return format(s.str());
-    }
-};
-formatter mk_simple_formatter() {
-    return mk_formatter(simple_formatter_cell());
-}
 }

src/kernel/formatter.h

@@ -60,9 +60,4 @@ public:
 template<typename FCell> formatter mk_formatter(FCell && fcell) {
     return formatter(new FCell(std::forward<FCell>(fcell)));
 }
-
-/**
-   \brief Create a simple formatter object based on \c print function.
-*/
-formatter mk_simple_formatter();
 }

src/kernel/io_state.cpp

@@ -8,8 +8,8 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 
 namespace lean {
-io_state::io_state():
-    m_formatter(mk_simple_formatter()),
+io_state::io_state(formatter const & fmt):
+    m_formatter(fmt),
     m_regular_channel(std::make_shared<stdout_channel>()),
     m_diagnostic_channel(std::make_shared<stderr_channel>()) {
 }

src/kernel/io_state.h

@@ -23,7 +23,7 @@ class io_state {
     std::shared_ptr<output_channel> m_regular_channel;
     std::shared_ptr<output_channel> m_diagnostic_channel;
 public:
-    io_state();
+    io_state(formatter const & fmt);
     io_state(options const & opts, formatter const & fmt);
     ~io_state();
 

src/library/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_library(library kernel_bindings.cpp deep_copy.cpp max_sharing.cpp
   context_to_lambda.cpp placeholder.cpp expr_lt.cpp substitution.cpp
-  fo_unify.cpp bin_op.cpp eq_heq.cpp io_state_stream.cpp)
+  fo_unify.cpp bin_op.cpp eq_heq.cpp io_state_stream.cpp printer.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/elaborator/elaborator.cpp

@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "kernel/builtin.h"
 #include "kernel/type_checker.h"
 #include "kernel/update_expr.h"
+#include "library/printer.h"
 #include "library/eq_heq.h"
 #include "library/elaborator/elaborator.h"
 #include "library/elaborator/elaborator_justification.h"

src/library/io_state_stream.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "library/io_state_stream.h"
 #include "kernel/kernel_exception.h"
+#include "library/printer.h"
 namespace lean {
 io_state_stream const & operator<<(io_state_stream const & out, endl_class) {
     out.get_stream() << std::endl;

src/library/kernel_bindings.cpp

@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "library/io_state_stream.h"
 #include "library/expr_lt.h"
 #include "library/kernel_bindings.h"
+#include "library/printer.h"
 
 // Lua Bindings for the Kernel classes. We do not include the Lua
 // bindings in the kernel because we do not want to inflate the Kernel.
@@ -1150,7 +1151,7 @@ static int environment_import(lua_State * L) {
         if (ios) {
             env->import(luaL_checkstring(L, 2), *ios);
         } else {
-            io_state ios;
+            io_state ios(mk_simple_formatter());
             ios.set_options(get_global_options(L));
             env->import(luaL_checkstring(L, 2), ios);
         }
@@ -1700,7 +1701,7 @@ DECL_UDATA(io_state)
 int mk_io_state(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 0)
-        return push_io_state(L, io_state());
+        return push_io_state(L, io_state(mk_simple_formatter()));
     else if (nargs == 1)
         return push_io_state(L, io_state(to_io_state(L, 1)));
     else

src/library/printer.cpp

@@ -7,8 +7,9 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include <utility>
 #include "util/exception.h"
-#include "kernel/printer.h"
 #include "kernel/environment.h"
+#include "kernel/formatter.h"
+#include "library/printer.h"
 
 namespace lean {
 bool is_atomic(expr const & e) {
@@ -221,6 +222,32 @@ std::ostream & operator<<(std::ostream & out, ro_environment const & env) {
                   [&](object const & obj) { out << obj << "\n"; });
     return out;
 }
+
+class simple_formatter_cell : public formatter_cell {
+public:
+    virtual format operator()(expr const & e, options const &) {
+        std::ostringstream s; s << e; return format(s.str());
+    }
+    virtual format operator()(context const & c, options const &) {
+        std::ostringstream s; s << c; return format(s.str());
+    }
+    virtual format operator()(context const & c, expr const & e, bool format_ctx, options const &) {
+        std::ostringstream s;
+        if (format_ctx)
+            s << c << " |- ";
+        s << mk_pair(e, c);
+        return format(s.str());
+    }
+    virtual format operator()(object const & obj, options const &) {
+        std::ostringstream s; s << obj; return format(s.str());
+    }
+    virtual format operator()(ro_environment const & env, options const &) {
+        std::ostringstream s; s << env; return format(s.str());
+    }
+};
+formatter mk_simple_formatter() {
+    return mk_formatter(simple_formatter_cell());
+}
 }
 void print(lean::expr const & a) { std::cout << a << std::endl; }
 void print(lean::expr const & a, lean::context const & c) { std::cout << mk_pair(a, c) << std::endl; }

src/library/printer.h

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <utility>
 #include "kernel/expr.h"
 #include "kernel/context.h"
+#include "kernel/formatter.h"
 
 namespace lean {
 class ro_environment;
@@ -18,6 +19,10 @@ std::ostream & operator<<(std::ostream & out, std::pair<expr const &, context co
 class object;
 std::ostream & operator<<(std::ostream & out, object const & obj);
 std::ostream & operator<<(std::ostream & out, ro_environment const & env);
+/**
+   \brief Create a simple formatter object based on \c print function.
+*/
+formatter mk_simple_formatter();
 }
 void print(lean::expr const & a);
 void print(lean::expr const & a, lean::context const & c);

src/library/rewriter/fo_match.cpp

@@ -7,7 +7,7 @@ Author: Soonho Kong
 #include <utility>
 #include "util/trace.h"
 #include "kernel/expr.h"
-#include "kernel/printer.h"
+#include "library/printer.h"
 #include "library/arith/nat.h"
 #include "library/arith/arith.h"
 #include "library/rewriter/fo_match.h"

src/library/rewriter/fo_match.h

@@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Soonho Kong
 */
 #pragma once
-#include "kernel/printer.h"
 #include "util/scoped_map.h"
 #include "kernel/expr.h"
 #include "kernel/context.h"
+#include "library/printer.h"
 
 namespace lean {
 using subst_map = scoped_map<unsigned, expr>;

src/library/rewriter/rewriter.cpp

@@ -11,9 +11,9 @@
 #include "kernel/context.h"
 #include "kernel/environment.h"
 #include "kernel/expr.h"
-#include "kernel/printer.h"
 #include "kernel/replace_fn.h"
 #include "kernel/type_checker.h"
+#include "library/printer.h"
 #include "library/rewriter/fo_match.h"
 #include "library/rewriter/rewriter.h"
 #include "util/buffer.h"

src/shell/lean.cpp

@@ -16,11 +16,11 @@ Author: Leonardo de Moura
 #include "util/script_state.h"
 #include "util/thread.h"
 #include "util/lean_path.h"
-#include "kernel/printer.h"
 #include "kernel/environment.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/formatter.h"
 #include "kernel/io_state.h"
+#include "library/printer.h"
 #include "library/kernel_bindings.h"
 #include "library/io_state_stream.h"
 #include "frontends/lean/parser.h"
@@ -173,8 +173,7 @@ int main(int argc, char ** argv) {
 #endif
                 environment env;
                 env->set_trusted_imported(trust_imported);
-                io_state ios;
-                init_frontend(env, ios, no_kernel);
+                io_state ios = init_frontend(env, no_kernel);
                 script_state S;
                 shell sh(env, &S);
                 int status = sh() ? 0 : 1;
@@ -189,8 +188,7 @@ int main(int argc, char ** argv) {
         } else {
             environment env;
             env->set_trusted_imported(trust_imported);
-            io_state    ios;
-            init_frontend(env, ios, no_kernel);
+            io_state    ios = init_frontend(env, no_kernel);
             script_state S;
             bool ok = true;
             for (int i = optind; i < argc; i++) {

src/tests/frontends/lean/frontend.cpp

@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 #include "kernel/builtin.h"
 #include "kernel/abstract.h"
-#include "kernel/printer.h"
+#include "library/printer.h"
 #include "library/bin_op.h"
 #include "library/io_state_stream.h"
 #include "frontends/lean/frontend.h"
@@ -19,7 +19,7 @@ Author: Leonardo de Moura
 using namespace lean;
 
 static void tst1() {
-    environment env; io_state ios; init_frontend(env, ios);
+    environment env; io_state ios = init_frontend(env);
     env->add_uvar("tst");
     environment c = env->mk_child();
     lean_assert(c->get_uvar("tst") == env->get_uvar("tst"));
@@ -61,7 +61,7 @@ static void tst3() {
 }
 
 static void tst4() {
-    environment env; io_state ios; init_frontend(env, ios);
+    environment env; io_state ios = init_frontend(env);
     formatter fmt = mk_pp_formatter(env);
     context c;
     c = extend(c, "x", Bool);
@@ -75,7 +75,7 @@ static void tst4() {
 
 static void tst5() {
     std::cout << "=================\n";
-    environment env; io_state ios; init_frontend(env, ios);
+    environment env; io_state ios = init_frontend(env);
     formatter fmt = mk_pp_formatter(env);
     env->add_var("A", Type());
     env->add_var("x", Const("A"));
@@ -104,27 +104,27 @@ public:
 
 static void tst6() {
     std::cout << "=================\n";
-    environment env; io_state ios; init_frontend(env, ios);
+    environment env; io_state ios = init_frontend(env);
     env->add_neutral_object(new alien_cell());
     formatter fmt = mk_pp_formatter(env);
     std::cout << fmt(env) << "\n";
 }
 
 static void tst7() {
-    environment env; io_state ios; init_frontend(env, ios);
+    environment env; io_state ios = init_frontend(env);
     formatter fmt = mk_pp_formatter(env);
     std::cout << fmt(And(Const("x"), Const("y"))) << "\n";
 }
 
 static void tst8() {
-    environment env; io_state ios; init_frontend(env, ios);
+    environment env; io_state ios = init_frontend(env);
     formatter fmt = mk_pp_formatter(env);
     add_infixl(env, ios, "<-$->", 10, mk_refl_fn());
     std::cout << fmt(*(env->find_object("Trivial"))) << "\n";
 }
 
 static void tst9() {
-    environment env; io_state ios; init_frontend(env, ios);
+    environment env; io_state ios = init_frontend(env);
     lean_assert(!env->has_children());
     {
         environment c = env->mk_child();
@@ -156,7 +156,7 @@ static void tst9() {
 }
 
 static void tst10() {
-    environment env; io_state ios; init_frontend(env, ios);
+    environment env; io_state ios = init_frontend(env);
     formatter fmt = mk_pp_formatter(env);
     expr x = Const("xxxxxxxxxxxx");
     expr y = Const("y");
@@ -167,7 +167,7 @@ static void tst10() {
 }
 
 static void tst11() {
-    environment env; io_state ios; init_frontend(env, ios);
+    environment env; io_state ios = init_frontend(env);
     expr A = Const("A");
     env->add_var("g", Pi({A, Type()}, A >> (A >> A)));
     lean_assert(!has_implicit_arguments(env, "g"));

src/tests/frontends/lean/parser.cpp

@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "util/exception.h"
 #include "util/numerics/mpq.h"
 #include "kernel/builtin.h"
-#include "kernel/printer.h"
+#include "library/printer.h"
 #include "library/io_state_stream.h"
 #include "library/arith/arith.h"
 #include "frontends/lean/parser.h"
@@ -43,7 +43,7 @@ static void parse_error(environment const & env, io_state const & ios, char cons
 }
 
 static void tst1() {
-    environment env; io_state ios; init_test_frontend(env, ios);
+    environment env; io_state ios = init_test_frontend(env);
     parse(env, ios, "Variable x : Bool Variable y : Bool Axiom H : x && y || x => x");
     parse(env, ios, "Eval true && true");
     parse(env, ios, "Show true && false Eval true && false");
@@ -64,7 +64,7 @@ static void check(environment const & env, io_state & ios, char const * str, exp
 }
 
 static void tst2() {
-    environment env; io_state ios; init_test_frontend(env, ios);
+    environment env; io_state ios = init_test_frontend(env);
     env->add_var("x", Bool);
     env->add_var("y", Bool);
     env->add_var("z", Bool);
@@ -81,7 +81,7 @@ static void tst2() {
 }
 
 static void tst3() {
-    environment env; io_state ios; init_test_frontend(env, ios);
+    environment env; io_state ios = init_test_frontend(env);
     parse(env, ios, "Help");
     parse(env, ios, "Help Options");
     parse_error(env, ios, "Help Echo");

src/tests/frontends/lean/pp.cpp

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include "util/test.h"
 #include "kernel/abstract.h"
 #include "kernel/builtin.h"
-#include "kernel/printer.h"
+#include "library/printer.h"
 #include "library/io_state_stream.h"
 #include "frontends/lean/frontend.h"
 #include "frontends/lean/pp.h"
@@ -23,7 +23,7 @@ static expr mk_shared_expr(unsigned depth) {
 }
 
 static void tst1() {
-    environment env; io_state ios; init_frontend(env, ios);
+    environment env; io_state ios = init_frontend(env);
     formatter fmt = mk_pp_formatter(env);
     std::cout << "Basic printer\n";
     std::cout << mk_shared_expr(10) << std::endl;
@@ -32,7 +32,7 @@ static void tst1() {
 }
 
 static void tst2() {
-    environment env; io_state ios; init_frontend(env, ios);
+    environment env; io_state ios = init_frontend(env);
     formatter fmt = mk_pp_formatter(env);
     expr a = Const("a");
     expr t = Fun({a, Type()}, mk_shared_expr(10));
@@ -43,7 +43,7 @@ static void tst2() {
 }
 
 static void tst3() {
-    environment env; io_state ios; init_frontend(env, ios);
+    environment env; io_state ios = init_frontend(env);
     formatter fmt = mk_pp_formatter(env);
     expr g = Const("g");
     expr a = Const("\u03BA");
@@ -59,7 +59,7 @@ static void tst3() {
 }
 
 static void tst4() {
-    environment env; io_state ios; init_frontend(env, ios);
+    environment env; io_state ios = init_frontend(env);
     io_state const & s1 = ios;
     io_state s2 = ios;
     regular(s1) << And(Const("a"), Const("b")) << "\n";
@@ -72,7 +72,7 @@ static void tst4() {
 }
 
 static void tst5() {
-    environment env; io_state ios; init_frontend(env, ios);
+    environment env; io_state ios = init_frontend(env);
     std::shared_ptr<string_output_channel> out(std::make_shared<string_output_channel>());
     ios.set_regular_channel(out);
     ios.set_option(name{"pp", "unicode"}, true);
@@ -92,7 +92,7 @@ static expr mk_deep(unsigned depth) {
 }
 
 static void tst6() {
-    environment env; io_state ios; init_frontend(env, ios);
+    environment env; io_state ios = init_frontend(env);
     std::shared_ptr<string_output_channel> out(std::make_shared<string_output_channel>());
     ios.set_regular_channel(out);
     expr t = mk_deep(10);

src/tests/kernel/environment.cpp

@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 #include "kernel/builtin.h"
 #include "kernel/normalizer.h"
 #include "kernel/abstract.h"
-#include "kernel/printer.h"
+#include "library/printer.h"
 #include "library/io_state_stream.h"
 #include "library/arith/arith.h"
 #include "frontends/lean/frontend.h"

src/tests/kernel/expr.cpp

@@ -14,7 +14,7 @@ Author: Leonardo de Moura
 #include "kernel/free_vars.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
-#include "kernel/printer.h"
+#include "library/printer.h"
 #include "library/max_sharing.h"
 #include "library/bin_op.h"
 #include "library/arith/arith.h"

src/tests/kernel/level.cpp

@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "util/test.h"
 #include "util/exception.h"
 #include "kernel/environment.h"
-#include "kernel/printer.h"
+#include "library/printer.h"
 using namespace lean;
 
 static void check_serializer(level const & l) {

src/tests/kernel/metavar.cpp

@@ -16,10 +16,10 @@ Author: Leonardo de Moura
 #include "kernel/normalizer.h"
 #include "kernel/environment.h"
 #include "kernel/type_checker.h"
-#include "kernel/printer.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/builtin.h"
 #include "kernel/io_state.h"
+#include "library/printer.h"
 #include "library/io_state_stream.h"
 #include "library/placeholder.h"
 #include "library/arith/arith.h"

src/tests/kernel/normalizer.cpp

@@ -15,9 +15,9 @@ Author: Leonardo de Moura
 #include "kernel/expr_sets.h"
 #include "kernel/abstract.h"
 #include "kernel/kernel_exception.h"
-#include "kernel/printer.h"
 #include "kernel/metavar.h"
 #include "kernel/free_vars.h"
+#include "library/printer.h"
 #include "library/io_state_stream.h"
 #include "library/deep_copy.h"
 #include "library/arith/int.h"

src/tests/kernel/occurs.cpp

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include "util/test.h"
 #include "kernel/occurs.h"
 #include "kernel/abstract.h"
-#include "kernel/printer.h"
+#include "library/printer.h"
 using namespace lean;
 
 static void tst1() {

src/tests/kernel/replace.cpp

@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/expr_maps.h"
 #include "kernel/replace_fn.h"
-#include "kernel/printer.h"
+#include "library/printer.h"
 #include "library/deep_copy.h"
 using namespace lean;
 

src/tests/kernel/type_checker.cpp

@@ -17,10 +17,10 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/builtin.h"
 #include "kernel/normalizer.h"
-#include "kernel/printer.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/type_checker_justification.h"
 #include "kernel/io_state.h"
+#include "library/printer.h"
 #include "library/io_state_stream.h"
 #include "library/arith/arith.h"
 #include "frontends/lean/frontend.h"

src/tests/library/formatter.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/abstract.h"
 #include "kernel/formatter.h"
+#include "library/printer.h"
 using namespace lean;
 
 static void check(format const & f, char const * expected) {

src/tests/library/max_sharing.cpp

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include <iostream>
 #include "util/test.h"
 #include "kernel/abstract.h"
-#include "kernel/printer.h"
+#include "library/printer.h"
 #include "library/max_sharing.h"
 using namespace lean;
 

src/tests/library/rewriter/fo_match.cpp

@@ -9,8 +9,8 @@ Author: Soonho Kong
 #include "kernel/abstract.h"
 #include "kernel/expr.h"
 #include "kernel/metavar.h"
-#include "kernel/printer.h"
 #include "kernel/builtin.h"
+#include "library/printer.h"
 #include "library/arith/arith.h"
 #include "library/arith/nat.h"
 #include "library/rewriter/fo_match.h"

src/tests/library/rewriter/rewriter.cpp

@@ -9,9 +9,9 @@ Author: Soonho Kong
 #include "kernel/abstract.h"
 #include "kernel/context.h"
 #include "kernel/expr.h"
-#include "kernel/printer.h"
 #include "kernel/io_state.h"
 #include "kernel/builtin.h"
+#include "library/printer.h"
 #include "library/io_state_stream.h"
 #include "library/arith/arith.h"
 #include "library/arith/nat.h"

src/tests/library/tactic/tactic.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/builtin.h"
 #include "kernel/kernel_exception.h"
 #include "library/io_state_stream.h"
+#include "library/printer.h"
 #include "library/tactic/goal.h"
 #include "library/tactic/proof_builder.h"
 #include "library/tactic/proof_state.h"