From ecc5d1bc3a71e924408c1e9a68b6d425dc4117e8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Jan 2014 13:37:50 -0800 Subject: [PATCH] refactor(kernel): move printer to library, cleanup io_state interface Signed-off-by: Leonardo de Moura --- src/frontends/lean/frontend.cpp | 15 ++++++------- src/frontends/lean/frontend.h | 5 ++--- src/frontends/lean/parser.cpp | 3 +-- src/frontends/lean/register_module.cpp | 3 +-- src/frontends/lean/shell.cpp | 3 +-- src/kernel/CMakeLists.txt | 7 +++--- src/kernel/formatter.cpp | 25 --------------------- src/kernel/formatter.h | 5 ----- src/kernel/io_state.cpp | 4 ++-- src/kernel/io_state.h | 2 +- src/library/CMakeLists.txt | 2 +- src/library/elaborator/elaborator.cpp | 1 + src/library/io_state_stream.cpp | 1 + src/library/kernel_bindings.cpp | 5 +++-- src/{kernel => library}/printer.cpp | 29 ++++++++++++++++++++++++- src/{kernel => library}/printer.h | 5 +++++ src/library/rewriter/fo_match.cpp | 2 +- src/library/rewriter/fo_match.h | 2 +- src/library/rewriter/rewriter.cpp | 2 +- src/shell/lean.cpp | 8 +++---- src/tests/frontends/lean/frontend.cpp | 20 ++++++++--------- src/tests/frontends/lean/parser.cpp | 8 +++---- src/tests/frontends/lean/pp.cpp | 14 ++++++------ src/tests/kernel/environment.cpp | 2 +- src/tests/kernel/expr.cpp | 2 +- src/tests/kernel/level.cpp | 2 +- src/tests/kernel/metavar.cpp | 2 +- src/tests/kernel/normalizer.cpp | 2 +- src/tests/kernel/occurs.cpp | 2 +- src/tests/kernel/replace.cpp | 2 +- src/tests/kernel/type_checker.cpp | 2 +- src/tests/library/formatter.cpp | 1 + src/tests/library/max_sharing.cpp | 2 +- src/tests/library/rewriter/fo_match.cpp | 2 +- src/tests/library/rewriter/rewriter.cpp | 2 +- src/tests/library/tactic/tactic.cpp | 1 + 36 files changed, 97 insertions(+), 98 deletions(-) rename src/{kernel => library}/printer.cpp (87%) rename src/{kernel => library}/printer.h (86%) diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index 098dc5ca7..ee02b58a4 100644 --- a/src/frontends/lean/frontend.cpp +++ b/src/frontends/lean/frontend.cpp @@ -557,22 +557,21 @@ static lean_extension & to_ext(environment const & env) { return env->get_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) { diff --git a/src/frontends/lean/frontend.h b/src/frontends/lean/frontend.h index 87b3eacc0..29054d654 100644 --- a/src/frontends/lean/frontend.h +++ b/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. diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index c21383fc5..893779f60 100644 --- a/src/frontends/lean/parser.cpp +++ b/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() { diff --git a/src/frontends/lean/register_module.cpp b/src/frontends/lean/register_module.cpp index f56d9d5b7..99a178dd2 100644 --- a/src/frontends/lean/register_module.cpp +++ b/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); } diff --git a/src/frontends/lean/shell.cpp b/src/frontends/lean/shell.cpp index 504b5776a..af15ec566 100644 --- a/src/frontends/lean/shell.cpp +++ b/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() { diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 900ee3ace..379621d20 100644 --- a/src/kernel/CMakeLists.txt +++ b/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}) diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp index 8044baf34..3e324c97f 100644 --- a/src/kernel/formatter.cpp +++ b/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()); -} } diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h index 4d78a9dab..e30939101 100644 --- a/src/kernel/formatter.h +++ b/src/kernel/formatter.h @@ -60,9 +60,4 @@ public: template formatter mk_formatter(FCell && fcell) { return formatter(new FCell(std::forward(fcell))); } - -/** - \brief Create a simple formatter object based on \c print function. -*/ -formatter mk_simple_formatter(); } diff --git a/src/kernel/io_state.cpp b/src/kernel/io_state.cpp index 11c660be3..375f192b8 100644 --- a/src/kernel/io_state.cpp +++ b/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()), m_diagnostic_channel(std::make_shared()) { } diff --git a/src/kernel/io_state.h b/src/kernel/io_state.h index ac15c9387..8a6d490ff 100644 --- a/src/kernel/io_state.h +++ b/src/kernel/io_state.h @@ -23,7 +23,7 @@ class io_state { std::shared_ptr m_regular_channel; std::shared_ptr m_diagnostic_channel; public: - io_state(); + io_state(formatter const & fmt); io_state(options const & opts, formatter const & fmt); ~io_state(); diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 1a472aa9f..15c95b271 100644 --- a/src/library/CMakeLists.txt +++ b/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}) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 9c2e31edd..f285c1d59 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/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" diff --git a/src/library/io_state_stream.cpp b/src/library/io_state_stream.cpp index a3b1527ab..6e10331ee 100644 --- a/src/library/io_state_stream.cpp +++ b/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; diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 78d05a924..09eaa9f69 100644 --- a/src/library/kernel_bindings.cpp +++ b/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 diff --git a/src/kernel/printer.cpp b/src/library/printer.cpp similarity index 87% rename from src/kernel/printer.cpp rename to src/library/printer.cpp index 97ef93b6d..5affc16a4 100644 --- a/src/kernel/printer.cpp +++ b/src/library/printer.cpp @@ -7,8 +7,9 @@ Author: Leonardo de Moura #include #include #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; } diff --git a/src/kernel/printer.h b/src/library/printer.h similarity index 86% rename from src/kernel/printer.h rename to src/library/printer.h index 0717692c7..67c225d32 100644 --- a/src/kernel/printer.h +++ b/src/library/printer.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include #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 #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" diff --git a/src/library/rewriter/fo_match.h b/src/library/rewriter/fo_match.h index 223d4d25d..e65b456ce 100644 --- a/src/library/rewriter/fo_match.h +++ b/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; diff --git a/src/library/rewriter/rewriter.cpp b/src/library/rewriter/rewriter.cpp index 90b0d58df..05db681c1 100644 --- a/src/library/rewriter/rewriter.cpp +++ b/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" diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 8f5730c90..f8cbd005a 100644 --- a/src/shell/lean.cpp +++ b/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++) { diff --git a/src/tests/frontends/lean/frontend.cpp b/src/tests/frontends/lean/frontend.cpp index bab9443fd..f1073fd06 100644 --- a/src/tests/frontends/lean/frontend.cpp +++ b/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")); diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp index de7b7dd1c..bf16c8f16 100644 --- a/src/tests/frontends/lean/parser.cpp +++ b/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"); diff --git a/src/tests/frontends/lean/pp.cpp b/src/tests/frontends/lean/pp.cpp index 14c72b16c..713fc33cb 100644 --- a/src/tests/frontends/lean/pp.cpp +++ b/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 out(std::make_shared()); 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 out(std::make_shared()); ios.set_regular_channel(out); expr t = mk_deep(10); diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index ffe8552c8..91d92ee8c 100644 --- a/src/tests/kernel/environment.cpp +++ b/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" diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 27528d170..b3e14504e 100644 --- a/src/tests/kernel/expr.cpp +++ b/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" diff --git a/src/tests/kernel/level.cpp b/src/tests/kernel/level.cpp index 1edbad5df..afa1da79a 100644 --- a/src/tests/kernel/level.cpp +++ b/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) { diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index 91c334c1a..cd3f45aa4 100644 --- a/src/tests/kernel/metavar.cpp +++ b/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" diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index 188755a01..6b40a588f 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/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" diff --git a/src/tests/kernel/occurs.cpp b/src/tests/kernel/occurs.cpp index bd23530b3..deb579e97 100644 --- a/src/tests/kernel/occurs.cpp +++ b/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() { diff --git a/src/tests/kernel/replace.cpp b/src/tests/kernel/replace.cpp index 7ad7e8ab8..012127929 100644 --- a/src/tests/kernel/replace.cpp +++ b/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; diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp index 88fead707..a42ef4170 100644 --- a/src/tests/kernel/type_checker.cpp +++ b/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" diff --git a/src/tests/library/formatter.cpp b/src/tests/library/formatter.cpp index 6742c1284..83447efd2 100644 --- a/src/tests/library/formatter.cpp +++ b/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) { diff --git a/src/tests/library/max_sharing.cpp b/src/tests/library/max_sharing.cpp index 4ed522d1b..3ba0f8762 100644 --- a/src/tests/library/max_sharing.cpp +++ b/src/tests/library/max_sharing.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include #include "util/test.h" #include "kernel/abstract.h" -#include "kernel/printer.h" +#include "library/printer.h" #include "library/max_sharing.h" using namespace lean; diff --git a/src/tests/library/rewriter/fo_match.cpp b/src/tests/library/rewriter/fo_match.cpp index 8d05ec6ed..580bbe9cb 100644 --- a/src/tests/library/rewriter/fo_match.cpp +++ b/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" diff --git a/src/tests/library/rewriter/rewriter.cpp b/src/tests/library/rewriter/rewriter.cpp index 6317e45c4..f72605900 100644 --- a/src/tests/library/rewriter/rewriter.cpp +++ b/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" diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp index caef5707f..1b4eb3999 100644 --- a/src/tests/library/tactic/tactic.cpp +++ b/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"