From 72761f14e43368b244ce0532a837def435d3c867 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Dec 2013 11:20:23 -0800 Subject: [PATCH] refactor(library/io_state): move to the kernel Signed-off-by: Leonardo de Moura --- src/builtin/cast.olean | Bin 924 -> 941 bytes src/frontends/lean/frontend.cpp | 2 +- src/frontends/lean/frontend.h | 2 +- src/frontends/lean/operator_info.h | 2 +- src/frontends/lean/parser.cpp | 2 +- src/frontends/lean/parser.h | 2 +- src/frontends/lean/register_module.cpp | 2 +- src/kernel/CMakeLists.txt | 9 +- src/kernel/io_state.cpp | 72 ++++++++ src/{library => kernel}/io_state.h | 20 --- src/library/CMakeLists.txt | 4 +- src/library/arith/int.cpp | 2 +- src/library/arith/nat.cpp | 2 +- src/library/arith/real.cpp | 2 +- src/library/arith/special_fn.cpp | 2 +- src/library/basic_thms.cpp | 2 +- src/library/io_state.cpp | 216 ------------------------ src/library/kernel_bindings.cpp | 146 +++++++++++++++- src/library/kernel_bindings.h | 19 +++ src/library/register_module.h | 2 - src/library/tactic/proof_state.h | 2 +- src/library/tactic/tactic.h | 2 +- src/shell/lean.cpp | 2 +- src/tests/kernel/metavar.cpp | 2 +- src/tests/kernel/type_checker.cpp | 2 +- src/tests/library/rewriter/rewriter.cpp | 2 +- 26 files changed, 260 insertions(+), 262 deletions(-) create mode 100644 src/kernel/io_state.cpp rename src/{library => kernel}/io_state.h (86%) delete mode 100644 src/library/io_state.cpp diff --git a/src/builtin/cast.olean b/src/builtin/cast.olean index 59c5f21fcda532bfd1c5e813bfdfd7a42b0b3bce..031ab9ddf921f30e7eff4a461b68ac010d5ebf69 100644 GIT binary patch delta 27 icmbQkzLtH0qkv~_L4HvQLvcZBa%N&qTHZ#77-j&6UK8JmR #include #include "kernel/environment.h" -#include "library/io_state.h" +#include "kernel/io_state.h" #include "library/expr_pair.h" #include "frontends/lean/operator_info.h" diff --git a/src/frontends/lean/operator_info.h b/src/frontends/lean/operator_info.h index c2b3b3155..feb5bb115 100644 --- a/src/frontends/lean/operator_info.h +++ b/src/frontends/lean/operator_info.h @@ -9,7 +9,7 @@ Author: Leonardo de Moura #include "util/name.h" #include "util/list.h" #include "util/sexpr/format.h" -#include "library/io_state.h" +#include "kernel/io_state.h" #include "kernel/object.h" namespace lean { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index d0ab29be5..ae49020bf 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -38,9 +38,9 @@ Author: Leonardo de Moura #include "kernel/for_each_fn.h" #include "kernel/find_fn.h" #include "kernel/type_checker_justification.h" +#include "kernel/io_state.h" #include "library/expr_lt.h" #include "library/arith/arith.h" -#include "library/io_state.h" #include "library/placeholder.h" #include "library/kernel_bindings.h" #include "library/elaborator/elaborator_exception.h" diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 0ab3565ae..0336af0ed 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include #include "util/lua.h" #include "kernel/environment.h" -#include "library/io_state.h" +#include "kernel/io_state.h" namespace lean { class script_state; diff --git a/src/frontends/lean/register_module.cpp b/src/frontends/lean/register_module.cpp index 270718120..9acf85bdd 100644 --- a/src/frontends/lean/register_module.cpp +++ b/src/frontends/lean/register_module.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "util/lua.h" #include "util/script_state.h" #include "util/sexpr/options.h" -#include "library/io_state.h" +#include "kernel/io_state.h" #include "library/kernel_bindings.h" #include "frontends/lean/parser.h" #include "frontends/lean/frontend.h" diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 1105b60d9..900ee3ace 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,8 +1,9 @@ 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) + 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) target_link_libraries(kernel ${LEAN_LIBS}) diff --git a/src/kernel/io_state.cpp b/src/kernel/io_state.cpp new file mode 100644 index 000000000..1ec5872a7 --- /dev/null +++ b/src/kernel/io_state.cpp @@ -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 +*/ +#include "kernel/io_state.h" +#include "kernel/kernel_exception.h" + +namespace lean { +io_state::io_state(): + m_formatter(mk_simple_formatter()), + m_regular_channel(std::make_shared()), + m_diagnostic_channel(std::make_shared()) { +} + +io_state::io_state(options const & opts, formatter const & fmt): + m_options(opts), + m_formatter(fmt), + m_regular_channel(std::make_shared()), + m_diagnostic_channel(std::make_shared()) { +} + +io_state::~io_state() {} + +void io_state::set_regular_channel(std::shared_ptr const & out) { + if (out) + m_regular_channel = out; +} + +void io_state::set_diagnostic_channel(std::shared_ptr const & out) { + if (out) + m_diagnostic_channel = out; +} + +void io_state::set_options(options const & opts) { + m_options = opts; +} + +void io_state::set_formatter(formatter const & f) { + m_formatter = f; +} + +io_state_stream const & operator<<(io_state_stream const & out, endl_class) { + out.get_stream() << std::endl; + return out; +} + +io_state_stream const & operator<<(io_state_stream const & out, expr const & e) { + options const & opts = out.get_options(); + out.get_stream() << mk_pair(out.get_formatter()(e, opts), opts); + return out; +} + +io_state_stream const & operator<<(io_state_stream const & out, object const & obj) { + options const & opts = out.get_options(); + out.get_stream() << mk_pair(out.get_formatter()(obj, opts), opts); + return out; +} + +io_state_stream const & operator<<(io_state_stream const & out, environment const & env) { + options const & opts = out.get_options(); + out.get_stream() << mk_pair(out.get_formatter()(env, opts), opts); + return out; +} + +io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex) { + options const & opts = out.get_options(); + out.get_stream() << mk_pair(ex.pp(out.get_formatter(), opts), opts); + return out; +} +} diff --git a/src/library/io_state.h b/src/kernel/io_state.h similarity index 86% rename from src/library/io_state.h rename to src/kernel/io_state.h index 56f75fa4c..307aa7e3b 100644 --- a/src/library/io_state.h +++ b/src/kernel/io_state.h @@ -90,24 +90,4 @@ template io_state_stream const & operator<<(io_state_stream const & out.get_stream() << t; return out; } - -UDATA_DEFS(io_state) -/** - \brief Auxiliary class for temporarily setting the Lua registry of a Lua state - with a Lean io_state object. -*/ -class set_io_state { - lua_State * m_state; - io_state * m_prev; - options m_prev_options; -public: - set_io_state(lua_State * L, io_state & st); - ~set_io_state(); -}; -/** - \brief Return the Lean state object associated with the given Lua state. - Return nullptr is there is none. -*/ -io_state * get_io_state(lua_State * L); -void open_io_state(lua_State * L); } diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 6b1fa7b59..32d6d96e1 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,5 +1,5 @@ add_library(library kernel_bindings.cpp basic_thms.cpp deep_copy.cpp - max_sharing.cpp context_to_lambda.cpp io_state.cpp placeholder.cpp - expr_lt.cpp substitution.cpp fo_unify.cpp bin_op.cpp) + max_sharing.cpp context_to_lambda.cpp placeholder.cpp expr_lt.cpp + substitution.cpp fo_unify.cpp bin_op.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp index 2af312c88..245803c17 100644 --- a/src/library/arith/int.cpp +++ b/src/library/arith/int.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/environment.h" #include "kernel/value.h" -#include "library/io_state.h" +#include "kernel/io_state.h" #include "library/kernel_bindings.h" #include "library/arith/int.h" #include "library/arith/nat.h" diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp index e5393bdb3..d449fb2e3 100644 --- a/src/library/arith/nat.cpp +++ b/src/library/arith/nat.cpp @@ -8,8 +8,8 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/environment.h" #include "kernel/value.h" +#include "kernel/io_state.h" #include "library/kernel_bindings.h" -#include "library/io_state.h" #include "library/arith/nat.h" namespace lean { diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp index 8d9b765b6..a1d7f3486 100644 --- a/src/library/arith/real.cpp +++ b/src/library/arith/real.cpp @@ -8,8 +8,8 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/environment.h" #include "kernel/value.h" +#include "kernel/io_state.h" #include "library/kernel_bindings.h" -#include "library/io_state.h" #include "library/arith/real.h" #include "library/arith/int.h" #include "library/arith/nat.h" diff --git a/src/library/arith/special_fn.cpp b/src/library/arith/special_fn.cpp index 80aa52ed3..758cff59b 100644 --- a/src/library/arith/special_fn.cpp +++ b/src/library/arith/special_fn.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include "kernel/environment.h" #include "kernel/abstract.h" -#include "library/io_state.h" +#include "kernel/io_state.h" #include "library/arith/special_fn.h" #include "library/arith/real.h" diff --git a/src/library/basic_thms.cpp b/src/library/basic_thms.cpp index e3cab6a97..4d0886473 100644 --- a/src/library/basic_thms.cpp +++ b/src/library/basic_thms.cpp @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/environment.h" -#include "library/io_state.h" +#include "kernel/io_state.h" #include "library/basic_thms.h" namespace lean { diff --git a/src/library/io_state.cpp b/src/library/io_state.cpp deleted file mode 100644 index 989b78284..000000000 --- a/src/library/io_state.cpp +++ /dev/null @@ -1,216 +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 -*/ -#include "kernel/kernel_exception.h" -#include "library/kernel_bindings.h" -#include "library/io_state.h" - -namespace lean { -io_state::io_state(): - m_formatter(mk_simple_formatter()), - m_regular_channel(std::make_shared()), - m_diagnostic_channel(std::make_shared()) { -} - -io_state::io_state(options const & opts, formatter const & fmt): - m_options(opts), - m_formatter(fmt), - m_regular_channel(std::make_shared()), - m_diagnostic_channel(std::make_shared()) { -} - -io_state::~io_state() {} - -void io_state::set_regular_channel(std::shared_ptr const & out) { - if (out) - m_regular_channel = out; -} - -void io_state::set_diagnostic_channel(std::shared_ptr const & out) { - if (out) - m_diagnostic_channel = out; -} - -void io_state::set_options(options const & opts) { - m_options = opts; -} - -void io_state::set_formatter(formatter const & f) { - m_formatter = f; -} - -io_state_stream const & operator<<(io_state_stream const & out, endl_class) { - out.get_stream() << std::endl; - return out; -} - -io_state_stream const & operator<<(io_state_stream const & out, expr const & e) { - options const & opts = out.get_options(); - out.get_stream() << mk_pair(out.get_formatter()(e, opts), opts); - return out; -} - -io_state_stream const & operator<<(io_state_stream const & out, object const & obj) { - options const & opts = out.get_options(); - out.get_stream() << mk_pair(out.get_formatter()(obj, opts), opts); - return out; -} - -io_state_stream const & operator<<(io_state_stream const & out, environment const & env) { - options const & opts = out.get_options(); - out.get_stream() << mk_pair(out.get_formatter()(env, opts), opts); - return out; -} - -io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex) { - options const & opts = out.get_options(); - out.get_stream() << mk_pair(ex.pp(out.get_formatter(), opts), opts); - return out; -} - -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()); - else if (nargs == 1) - return push_io_state(L, io_state(to_io_state(L, 1))); - else - return push_io_state(L, io_state(to_options(L, 1), to_formatter(L, 2))); -} - -int io_state_get_options(lua_State * L) { - return push_options(L, to_io_state(L, 1).get_options()); -} - -int io_state_get_formatter(lua_State * L) { - return push_formatter(L, to_io_state(L, 1).get_formatter()); -} - -int io_state_set_options(lua_State * L) { - to_io_state(L, 1).set_options(to_options(L, 2)); - return 0; -} - -static mutex g_print_mutex; - -static void print(io_state * ios, bool reg, char const * msg) { - if (ios) { - if (reg) - regular(*ios) << msg; - else - diagnostic(*ios) << msg; - } else { - std::cout << msg; - } -} - -/** \brief Thread safe version of print function */ -static int print(lua_State * L, int start, bool reg) { - lock_guard lock(g_print_mutex); - io_state * ios = get_io_state(L); - int n = lua_gettop(L); - int i; - lua_getglobal(L, "tostring"); - for (i = start; i <= n; i++) { - char const * s; - size_t l; - lua_pushvalue(L, -1); - lua_pushvalue(L, i); - lua_call(L, 1, 1); - s = lua_tolstring(L, -1, &l); - if (s == NULL) - throw exception("'to_string' must return a string to 'print'"); - if (i > start) { - print(ios, reg, "\t"); - } - print(ios, reg, s); - lua_pop(L, 1); - } - print(ios, reg, "\n"); - return 0; -} - -static int print(lua_State * L, io_state & ios, int start, bool reg) { - set_io_state set(L, ios); - return print(L, start, reg); -} - -static int print(lua_State * L) { - return print(L, 1, true); -} - -int io_state_print_regular(lua_State * L) { - return print(L, to_io_state(L, 1), 2, true); -} - -int io_state_print_diagnostic(lua_State * L) { - return print(L, to_io_state(L, 1), 2, false); -} - -static const struct luaL_Reg io_state_m[] = { - {"__gc", io_state_gc}, // never throws - {"get_options", safe_function}, - {"set_options", safe_function}, - {"get_formatter", safe_function}, - {"print_diagnostic", safe_function}, - {"print_regular", safe_function}, - {"print", safe_function}, - {"diagnostic", safe_function}, - {0, 0} -}; - -void open_io_state(lua_State * L) { - luaL_newmetatable(L, io_state_mt); - lua_pushvalue(L, -1); - lua_setfield(L, -2, "__index"); - setfuncs(L, io_state_m, 0); - - SET_GLOBAL_FUN(io_state_pred, "is_io_state"); - SET_GLOBAL_FUN(mk_io_state, "io_state"); - SET_GLOBAL_FUN(print, "print"); -} - -static char g_set_state_key; - -set_io_state::set_io_state(lua_State * L, io_state & st) { - m_state = L; - m_prev = get_io_state(L); - lua_pushlightuserdata(m_state, static_cast(&g_set_state_key)); - lua_pushlightuserdata(m_state, &st); - lua_settable(m_state, LUA_REGISTRYINDEX); - if (!m_prev) - m_prev_options = get_global_options(m_state); - set_global_options(m_state, st.get_options()); -} - -set_io_state::~set_io_state() { - lua_pushlightuserdata(m_state, static_cast(&g_set_state_key)); - lua_pushlightuserdata(m_state, m_prev); - lua_settable(m_state, LUA_REGISTRYINDEX); - if (!m_prev) - set_global_options(m_state, m_prev_options); - else - set_global_options(m_state, m_prev->get_options()); -} - -io_state * get_io_state(lua_State * L) { - lua_pushlightuserdata(L, static_cast(&g_set_state_key)); - lua_gettable(L, LUA_REGISTRYINDEX); - if (lua_islightuserdata(L, -1)) { - io_state * r = static_cast(lua_touserdata(L, -1)); - if (r) { - lua_pop(L, 1); - options o = get_global_options(L); - r->set_options(o); - return r; - } - } - lua_pop(L, 1); - return nullptr; -} -} diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index fc6c3aa58..969d15c66 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -18,10 +18,10 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/occurs.h" #include "kernel/builtin.h" +#include "kernel/io_state.h" #include "kernel/type_checker.h" #include "library/expr_lt.h" #include "library/kernel_bindings.h" -#include "library/io_state.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. @@ -1675,6 +1675,149 @@ void open_type_inferer(lua_State * L) { SET_GLOBAL_FUN(type_inferer_pred, "is_type_inferer"); } +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()); + else if (nargs == 1) + return push_io_state(L, io_state(to_io_state(L, 1))); + else + return push_io_state(L, io_state(to_options(L, 1), to_formatter(L, 2))); +} + +int io_state_get_options(lua_State * L) { + return push_options(L, to_io_state(L, 1).get_options()); +} + +int io_state_get_formatter(lua_State * L) { + return push_formatter(L, to_io_state(L, 1).get_formatter()); +} + +int io_state_set_options(lua_State * L) { + to_io_state(L, 1).set_options(to_options(L, 2)); + return 0; +} + +static mutex g_print_mutex; + +static void print(io_state * ios, bool reg, char const * msg) { + if (ios) { + if (reg) + regular(*ios) << msg; + else + diagnostic(*ios) << msg; + } else { + std::cout << msg; + } +} + +/** \brief Thread safe version of print function */ +static int print(lua_State * L, int start, bool reg) { + lock_guard lock(g_print_mutex); + io_state * ios = get_io_state(L); + int n = lua_gettop(L); + int i; + lua_getglobal(L, "tostring"); + for (i = start; i <= n; i++) { + char const * s; + size_t l; + lua_pushvalue(L, -1); + lua_pushvalue(L, i); + lua_call(L, 1, 1); + s = lua_tolstring(L, -1, &l); + if (s == NULL) + throw exception("'to_string' must return a string to 'print'"); + if (i > start) { + print(ios, reg, "\t"); + } + print(ios, reg, s); + lua_pop(L, 1); + } + print(ios, reg, "\n"); + return 0; +} + +static int print(lua_State * L, io_state & ios, int start, bool reg) { + set_io_state set(L, ios); + return print(L, start, reg); +} + +static int print(lua_State * L) { + return print(L, 1, true); +} + +int io_state_print_regular(lua_State * L) { + return print(L, to_io_state(L, 1), 2, true); +} + +int io_state_print_diagnostic(lua_State * L) { + return print(L, to_io_state(L, 1), 2, false); +} + +static const struct luaL_Reg io_state_m[] = { + {"__gc", io_state_gc}, // never throws + {"get_options", safe_function}, + {"set_options", safe_function}, + {"get_formatter", safe_function}, + {"print_diagnostic", safe_function}, + {"print_regular", safe_function}, + {"print", safe_function}, + {"diagnostic", safe_function}, + {0, 0} +}; + +void open_io_state(lua_State * L) { + luaL_newmetatable(L, io_state_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, io_state_m, 0); + + SET_GLOBAL_FUN(io_state_pred, "is_io_state"); + SET_GLOBAL_FUN(mk_io_state, "io_state"); + SET_GLOBAL_FUN(print, "print"); +} + +static char g_set_state_key; + +set_io_state::set_io_state(lua_State * L, io_state & st) { + m_state = L; + m_prev = get_io_state(L); + lua_pushlightuserdata(m_state, static_cast(&g_set_state_key)); + lua_pushlightuserdata(m_state, &st); + lua_settable(m_state, LUA_REGISTRYINDEX); + if (!m_prev) + m_prev_options = get_global_options(m_state); + set_global_options(m_state, st.get_options()); +} + +set_io_state::~set_io_state() { + lua_pushlightuserdata(m_state, static_cast(&g_set_state_key)); + lua_pushlightuserdata(m_state, m_prev); + lua_settable(m_state, LUA_REGISTRYINDEX); + if (!m_prev) + set_global_options(m_state, m_prev_options); + else + set_global_options(m_state, m_prev->get_options()); +} + +io_state * get_io_state(lua_State * L) { + lua_pushlightuserdata(L, static_cast(&g_set_state_key)); + lua_gettable(L, LUA_REGISTRYINDEX); + if (lua_islightuserdata(L, -1)) { + io_state * r = static_cast(lua_touserdata(L, -1)); + if (r) { + lua_pop(L, 1); + options o = get_global_options(L); + r->set_options(o); + return r; + } + } + lua_pop(L, 1); + return nullptr; +} + void open_kernel_module(lua_State * L) { open_level(L); open_local_context(L); @@ -1686,5 +1829,6 @@ void open_kernel_module(lua_State * L) { open_justification(L); open_metavar_env(L); open_type_inferer(L); + open_io_state(L); } } diff --git a/src/library/kernel_bindings.h b/src/library/kernel_bindings.h index 1e710ec86..b99a68453 100644 --- a/src/library/kernel_bindings.h +++ b/src/library/kernel_bindings.h @@ -21,6 +21,7 @@ UDATA_DEFS(object) UDATA_DEFS(environment) UDATA_DEFS(justification) UDATA_DEFS(metavar_env) +UDATA_DEFS(io_state) int push_environment(lua_State * L, ro_environment const & env); int push_optional_expr(lua_State * L, optional const & e); int push_optional_justification(lua_State * L, optional const & j); @@ -73,4 +74,22 @@ public: rw_shared_environment(lua_State * L, int idx); rw_shared_environment(lua_State * L); }; +/** + \brief Auxiliary class for temporarily setting the Lua registry of a Lua state + with a Lean io_state object. +*/ +class set_io_state { + lua_State * m_state; + io_state * m_prev; + options m_prev_options; +public: + set_io_state(lua_State * L, io_state & st); + ~set_io_state(); +}; +/** + \brief Return the Lean state object associated with the given Lua state. + Return nullptr is there is none. +*/ +io_state * get_io_state(lua_State * L); +void open_io_state(lua_State * L); } diff --git a/src/library/register_module.h b/src/library/register_module.h index 4ae52f0b8..a67f19e5e 100644 --- a/src/library/register_module.h +++ b/src/library/register_module.h @@ -7,7 +7,6 @@ Author: Leonardo de Moura #pragma once #include "util/script_state.h" #include "library/kernel_bindings.h" -#include "library/io_state.h" #include "library/substitution.h" #include "library/fo_unify.h" #include "library/placeholder.h" @@ -15,7 +14,6 @@ Author: Leonardo de Moura namespace lean { inline void open_core_module(lua_State * L) { open_kernel_module(L); - open_io_state(L); open_substitution(L); open_fo_unify(L); open_placeholder(L); diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 5cb903ecf..583de731e 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -12,7 +12,7 @@ Author: Leonardo de Moura #include "util/interrupt.h" #include "util/optional.h" #include "util/name_set.h" -#include "library/io_state.h" +#include "kernel/io_state.h" #include "library/tactic/goal.h" #include "library/tactic/proof_builder.h" #include "library/tactic/cex_builder.h" diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 34ce89e38..395f56948 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -11,7 +11,7 @@ Author: Leonardo de Moura #include #include "util/thread.h" #include "util/lazy_list.h" -#include "library/io_state.h" +#include "kernel/io_state.h" #include "library/tactic/proof_state.h" namespace lean { diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index e8c507d9c..e2197f2b5 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -20,7 +20,7 @@ Author: Leonardo de Moura #include "kernel/environment.h" #include "kernel/kernel_exception.h" #include "kernel/formatter.h" -#include "library/io_state.h" +#include "kernel/io_state.h" #include "library/kernel_bindings.h" #include "frontends/lean/parser.h" #include "frontends/lean/frontend.h" diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index f7dbb33de..85e4f2e5c 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -19,8 +19,8 @@ Author: Leonardo de Moura #include "kernel/printer.h" #include "kernel/kernel_exception.h" #include "kernel/builtin.h" +#include "kernel/io_state.h" #include "library/placeholder.h" -#include "library/io_state.h" #include "library/arith/arith.h" #include "frontends/lean/frontend.h" using namespace lean; diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp index 02a8f9743..2190b859a 100644 --- a/src/tests/kernel/type_checker.cpp +++ b/src/tests/kernel/type_checker.cpp @@ -20,9 +20,9 @@ Author: Leonardo de Moura #include "kernel/printer.h" #include "kernel/kernel_exception.h" #include "kernel/type_checker_justification.h" +#include "kernel/io_state.h" #include "library/basic_thms.h" #include "library/arith/arith.h" -#include "library/io_state.h" #include "frontends/lean/frontend.h" using namespace lean; diff --git a/src/tests/library/rewriter/rewriter.cpp b/src/tests/library/rewriter/rewriter.cpp index 20a04249a..960efef43 100644 --- a/src/tests/library/rewriter/rewriter.cpp +++ b/src/tests/library/rewriter/rewriter.cpp @@ -10,7 +10,7 @@ Author: Soonho Kong #include "kernel/context.h" #include "kernel/expr.h" #include "kernel/printer.h" -#include "library/io_state.h" +#include "kernel/io_state.h" #include "library/all/all.h" #include "library/arith/arith.h" #include "library/arith/nat.h"