From 2a79da1ab667ef4c468a3c2cf0a4c690f08d2ac8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 Jun 2018 16:16:11 -0700 Subject: [PATCH] refactor(kernel): move formatting stuff out of the kernel --- src/checker/checker.cpp | 9 +-------- src/frontends/lean/definition_cmds.cpp | 2 +- src/frontends/lean/elaborator.cpp | 4 ++-- src/frontends/lean/elaborator.h | 4 ++-- src/frontends/lean/parser.cpp | 4 ++-- src/frontends/lean/parser_pos_provider.h | 2 +- src/frontends/lean/scanner.h | 2 +- src/frontends/lean/structure_cmd.cpp | 2 +- src/frontends/lean/tactic_notation.cpp | 2 +- src/frontends/lean/util.cpp | 2 +- src/kernel/CMakeLists.txt | 12 ++++++------ src/kernel/expr.h | 1 - src/kernel/inductive.cpp | 2 ++ src/kernel/init_module.cpp | 6 ------ src/kernel/kernel_exception.cpp | 15 --------------- src/kernel/old_type_checker.cpp | 1 - src/library/CMakeLists.txt | 3 ++- src/library/abstract_parser.h | 2 +- src/library/compiler/lambda_lifting.cpp | 2 +- src/library/compiler/preprocess.cpp | 2 +- src/library/compiler/procedure.h | 2 +- src/library/equations_compiler/equations.cpp | 2 +- src/library/equations_compiler/util.cpp | 4 ++-- src/library/equations_compiler/wf_rec.cpp | 4 ++-- src/{kernel => library}/error_msgs.cpp | 2 +- src/{kernel => library}/error_msgs.h | 2 +- src/library/exception.h | 4 ++-- src/{kernel => library}/ext_exception.h | 2 +- src/{kernel => library}/formatter.cpp | 2 +- src/{kernel => library}/formatter.h | 0 src/library/init_module.cpp | 6 ++++++ src/library/io_state.h | 3 ++- src/library/io_state_stream.h | 2 +- src/library/local_context.h | 1 + src/library/module.h | 2 +- src/{kernel => library}/pos_info_provider.cpp | 2 +- src/{kernel => library}/pos_info_provider.h | 0 src/library/pp_options.cpp | 2 +- src/library/print.cpp | 2 +- src/library/print.h | 2 +- .../scope_pos_info_provider.cpp | 2 +- src/{kernel => library}/scope_pos_info_provider.h | 2 +- src/library/tactic/elaborator_exception.cpp | 2 +- src/library/tactic/eval.cpp | 2 +- src/library/tactic/induction_tactic.cpp | 2 +- src/library/tactic/simp_lemmas.cpp | 2 +- src/library/type_context.cpp | 2 +- src/library/util.cpp | 2 +- src/library/vm/interaction_state.h | 2 +- src/library/vm/vm.h | 2 +- src/library/vm/vm_format.cpp | 2 +- src/shell/lean.cpp | 2 +- src/shell/server.h | 6 +++--- src/shell/simple_pos_info_provider.h | 2 +- 54 files changed, 69 insertions(+), 88 deletions(-) delete mode 100644 src/kernel/kernel_exception.cpp rename src/{kernel => library}/error_msgs.cpp (99%) rename src/{kernel => library}/error_msgs.h (98%) rename src/{kernel => library}/ext_exception.h (96%) rename src/{kernel => library}/formatter.cpp (98%) rename src/{kernel => library}/formatter.h (100%) rename src/{kernel => library}/pos_info_provider.cpp (93%) rename src/{kernel => library}/pos_info_provider.h (100%) rename src/{kernel => library}/scope_pos_info_provider.cpp (96%) rename src/{kernel => library}/scope_pos_info_provider.h (93%) diff --git a/src/checker/checker.cpp b/src/checker/checker.cpp index 8cb363adbe..aa9cfdbf4d 100644 --- a/src/checker/checker.cpp +++ b/src/checker/checker.cpp @@ -13,6 +13,7 @@ Author: Gabriel Ebner #include "kernel/inductive/inductive.h" #include "kernel/standard_kernel.h" #include "kernel/for_each_fn.h" +#include "library/formatter.h" #include "checker/text_import.h" #include "checker/simple_pp.h" @@ -107,14 +108,6 @@ int main(int argc, char ** argv) { } } initer; - set_print_fn([] (std::ostream & out, expr const & e) { - try { - out << simple_pp(environment(), e, lowlevel_notations()); - } catch (throwable & e) { - out << "!!!" << e.what() << "!!!"; - } - }); - try { std::ifstream in(argv[1]); if (!in) throw exception(sstream() << "file not found: " << argv[1]); diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 10f6972db4..fcb46dd9ec 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -27,7 +27,7 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/aux_definition.h" #include "library/documentation.h" -#include "kernel/scope_pos_info_provider.h" +#include "library/scope_pos_info_provider.h" #include "library/replace_visitor.h" #include "library/equations_compiler/util.h" #include "library/equations_compiler/equations.h" diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 88c5941cb4..a8349674e9 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -10,13 +10,13 @@ Author: Leonardo de Moura #include "runtime/flet.h" #include "util/sexpr/option_declarations.h" #include "kernel/find_fn.h" -#include "kernel/error_msgs.h" #include "kernel/for_each_fn.h" #include "kernel/abstract.h" #include "kernel/replace_fn.h" #include "kernel/instantiate.h" -#include "kernel/scope_pos_info_provider.h" #include "kernel/inductive/inductive.h" +#include "library/scope_pos_info_provider.h" +#include "library/error_msgs.h" #include "library/trace.h" #include "library/user_recursors.h" #include "library/aux_recursors.h" diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 4a23877398..1383a0532f 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -6,15 +6,15 @@ Author: Leonardo de Moura */ #pragma once #include -#include "kernel/pos_info_provider.h" +#include "library/pos_info_provider.h" #include "library/local_context.h" #include "library/type_context.h" #include "library/context_cache.h" #include "library/tactic/tactic_state.h" #include "library/tactic/elaborate.h" #include "library/tactic/elaborator_exception.h" -#include "frontends/lean/info_manager.h" #include "library/sorry.h" +#include "frontends/lean/info_manager.h" namespace lean { enum class elaborator_strategy { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index ff8a3ec163..af57caa048 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -18,7 +18,7 @@ Author: Leonardo de Moura #include "kernel/find_fn.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" -#include "kernel/error_msgs.h" +#include "library/error_msgs.h" #include "library/st_task_queue.h" #include "library/profiling.h" #include "library/library_task_builder.h" @@ -48,7 +48,7 @@ Author: Leonardo de Moura #include "library/pp_options.h" #include "library/noncomputable.h" #include "library/replace_visitor.h" -#include "kernel/scope_pos_info_provider.h" +#include "library/scope_pos_info_provider.h" #include "library/type_context.h" #include "library/pattern_attribute.h" #include "library/equations_compiler/equations.h" diff --git a/src/frontends/lean/parser_pos_provider.h b/src/frontends/lean/parser_pos_provider.h index dee9f7e827..fe81342c45 100644 --- a/src/frontends/lean/parser_pos_provider.h +++ b/src/frontends/lean/parser_pos_provider.h @@ -9,7 +9,7 @@ Author: Leonardo de Moura #include #include #include "util/rb_map.h" -#include "kernel/pos_info_provider.h" +#include "library/pos_info_provider.h" namespace lean { typedef rb_map pos_info_table; diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h index bd1012b5be..17eaebd75b 100644 --- a/src/frontends/lean/scanner.h +++ b/src/frontends/lean/scanner.h @@ -12,7 +12,7 @@ Author: Leonardo de Moura #include "runtime/utf8.h" #include "util/name.h" #include "kernel/environment.h" -#include "kernel/pos_info_provider.h" +#include "library/pos_info_provider.h" #include "library/io_state.h" #include "frontends/lean/token_table.h" diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 9b933dc5a1..a7769aaf25 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -15,9 +15,9 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/replace_fn.h" -#include "kernel/error_msgs.h" #include "kernel/old_type_checker.h" #include "kernel/inductive/inductive.h" +#include "library/error_msgs.h" #include "library/replace_visitor.h" #include "library/trace.h" #include "library/attribute_manager.h" diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp index b3a74fd5d8..6c29ccf395 100644 --- a/src/frontends/lean/tactic_notation.cpp +++ b/src/frontends/lean/tactic_notation.cpp @@ -13,7 +13,7 @@ Author: Leonardo de Moura #include "library/trace.h" #include "library/placeholder.h" #include "library/explicit.h" -#include "kernel/scope_pos_info_provider.h" +#include "library/scope_pos_info_provider.h" #include "library/vm/vm_nat.h" #include "library/vm/vm_format.h" #include "library/vm/vm_expr.h" diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 354c510112..1052fbaaf5 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -11,9 +11,9 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "kernel/replace_fn.h" -#include "kernel/error_msgs.h" #include "kernel/for_each_fn.h" #include "kernel/old_type_checker.h" +#include "library/error_msgs.h" #include "library/kernel_serializer.h" #include "library/scoped_ext.h" #include "library/annotation.h" diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 8e84496753..33cc7ed5c1 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -1,6 +1,6 @@ -add_library(kernel OBJECT level.cpp expr.cpp expr_eq_fn.cpp for_each_fn.cpp -replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp local_ctx.cpp -formatter.cpp declaration.cpp environment.cpp pos_info_provider.cpp -old_type_checker.cpp error_msgs.cpp kernel_exception.cpp -normalizer_extension.cpp init_module.cpp expr_cache.cpp scope_pos_info_provider.cpp -equiv_manager.cpp quot.cpp abstract_type_context.cpp inductive.cpp standard_kernel.cpp) +add_library(kernel OBJECT level.cpp expr.cpp expr_eq_fn.cpp +for_each_fn.cpp replace_fn.cpp free_vars.cpp abstract.cpp +instantiate.cpp local_ctx.cpp declaration.cpp environment.cpp +old_type_checker.cpp normalizer_extension.cpp +init_module.cpp expr_cache.cpp equiv_manager.cpp quot.cpp +abstract_type_context.cpp inductive.cpp standard_kernel.cpp) diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 8ed8b38339..ca8382d34f 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -21,7 +21,6 @@ Author: Leonardo de Moura #include "util/list_fn.h" #include "util/sexpr/format.h" #include "kernel/level.h" -#include "kernel/formatter.h" #include "kernel/expr_eq_fn.h" namespace lean { diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp index 8720993f96..18ac218d47 100644 --- a/src/kernel/inductive.cpp +++ b/src/kernel/inductive.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura namespace lean { environment environment::add_inductive_decls(inductive_decls const & decls) const { +#if 0 std::cout << "add_inductive_decls\n"; for (expr const & p : decls.m_params) { std::cout << "param>> " << p << " : " << mlocal_type(p) << "\n"; @@ -19,6 +20,7 @@ environment environment::add_inductive_decls(inductive_decls const & decls) cons std::cout << ">> " << c << " : " << mlocal_type(c) << "\n"; } } +#endif // TODO(Leo) return *this; } diff --git a/src/kernel/init_module.cpp b/src/kernel/init_module.cpp index 3bd197fa51..89afa40cd9 100644 --- a/src/kernel/init_module.cpp +++ b/src/kernel/init_module.cpp @@ -7,22 +7,18 @@ Author: Leonardo de Moura #include "kernel/environment.h" #include "kernel/old_type_checker.h" #include "kernel/expr.h" -#include "kernel/formatter.h" #include "kernel/level.h" #include "kernel/declaration.h" -#include "kernel/error_msgs.h" #include "kernel/local_ctx.h" #include "kernel/quot.h" namespace lean { void initialize_kernel_module() { - initialize_error_msgs(); initialize_level(); initialize_expr(); initialize_declaration(); initialize_old_type_checker(); initialize_environment(); - initialize_formatter(); initialize_quot(); initialize_local_ctx(); } @@ -30,12 +26,10 @@ void initialize_kernel_module() { void finalize_kernel_module() { finalize_local_ctx(); finalize_quot(); - finalize_formatter(); finalize_environment(); finalize_old_type_checker(); finalize_declaration(); finalize_expr(); finalize_level(); - finalize_error_msgs(); } } diff --git a/src/kernel/kernel_exception.cpp b/src/kernel/kernel_exception.cpp deleted file mode 100644 index 4a7693ab12..0000000000 --- a/src/kernel/kernel_exception.cpp +++ /dev/null @@ -1,15 +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 -#include -#include "runtime/sstream.h" -#include "kernel/scope_pos_info_provider.h" -#include "kernel/kernel_exception.h" -#include "kernel/error_msgs.h" - -namespace lean { -} diff --git a/src/kernel/old_type_checker.cpp b/src/kernel/old_type_checker.cpp index b0f047edcb..db92efe0bd 100644 --- a/src/kernel/old_type_checker.cpp +++ b/src/kernel/old_type_checker.cpp @@ -17,7 +17,6 @@ Author: Leonardo de Moura #include "kernel/expr_maps.h" #include "kernel/instantiate.h" #include "kernel/free_vars.h" -#include "kernel/error_msgs.h" #include "kernel/kernel_exception.h" #include "kernel/abstract.h" #include "kernel/replace_fn.h" diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 2536196bb0..0cb3d43807 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -17,4 +17,5 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp eval_helper.cpp messages.cpp message_builder.cpp module_mgr.cpp comp_val.cpp documentation.cpp check.cpp parray.cpp process.cpp pipe.cpp handle.cpp profiling.cpp time_task.cpp abstract_context_cache.cpp - context_cache.cpp unique_id.cpp persistent_context_cache.cpp elab_context.cpp) + context_cache.cpp unique_id.cpp persistent_context_cache.cpp elab_context.cpp + scope_pos_info_provider.cpp error_msgs.cpp formatter.cpp pos_info_provider.cpp) diff --git a/src/library/abstract_parser.h b/src/library/abstract_parser.h index 2d764445be..df7981050d 100644 --- a/src/library/abstract_parser.h +++ b/src/library/abstract_parser.h @@ -8,7 +8,7 @@ Author: Sebastian Ullrich #include #include "util/name_map.h" #include "util/exception_with_pos.h" -#include "kernel/pos_info_provider.h" +#include "library/pos_info_provider.h" namespace lean { /** \brief Exception used to track parsing erros, it does not leak outside of this class. */ diff --git a/src/library/compiler/lambda_lifting.cpp b/src/library/compiler/lambda_lifting.cpp index ade69a91ac..e66c340520 100644 --- a/src/library/compiler/lambda_lifting.cpp +++ b/src/library/compiler/lambda_lifting.cpp @@ -11,7 +11,7 @@ Author: Leonardo de Moura #include "library/normalize.h" #include "library/util.h" #include "library/trace.h" -#include "kernel/scope_pos_info_provider.h" +#include "library/scope_pos_info_provider.h" #include "library/module.h" #include "library/vm/vm.h" #include "library/sorry.h" diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp index c0af7b1f6b..dbaa205408 100644 --- a/src/library/compiler/preprocess.cpp +++ b/src/library/compiler/preprocess.cpp @@ -9,7 +9,7 @@ Author: Leonardo de Moura #include "kernel/replace_fn.h" #include "kernel/instantiate.h" #include "kernel/for_each_fn.h" -#include "kernel/scope_pos_info_provider.h" +#include "library/scope_pos_info_provider.h" #include "library/trace.h" #include "library/projection.h" #include "library/constants.h" diff --git a/src/library/compiler/procedure.h b/src/library/compiler/procedure.h index 72517e0763..4e090282f8 100644 --- a/src/library/compiler/procedure.h +++ b/src/library/compiler/procedure.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/pos_info_provider.h" +#include "library/pos_info_provider.h" namespace lean { struct procedure { name m_name; diff --git a/src/library/equations_compiler/equations.cpp b/src/library/equations_compiler/equations.cpp index cf7d7055db..b2c3dec1f1 100644 --- a/src/library/equations_compiler/equations.cpp +++ b/src/library/equations_compiler/equations.cpp @@ -12,10 +12,10 @@ Author: Leonardo de Moura #include "kernel/expr.h" #include "kernel/abstract.h" #include "kernel/instantiate.h" -#include "kernel/error_msgs.h" #include "kernel/for_each_fn.h" #include "kernel/find_fn.h" #include "kernel/replace_fn.h" +#include "library/error_msgs.h" #include "library/exception.h" #include "library/kernel_serializer.h" #include "library/io_state_stream.h" diff --git a/src/library/equations_compiler/util.cpp b/src/library/equations_compiler/util.cpp index 7a2a1af830..e401a32718 100644 --- a/src/library/equations_compiler/util.cpp +++ b/src/library/equations_compiler/util.cpp @@ -8,10 +8,10 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/find_fn.h" +#include "kernel/free_vars.h" #include "kernel/old_type_checker.h" #include "kernel/inductive/inductive.h" -#include "kernel/scope_pos_info_provider.h" -#include "kernel/free_vars.h" +#include "library/scope_pos_info_provider.h" #include "library/util.h" #include "library/module.h" #include "library/aliases.h" diff --git a/src/library/equations_compiler/wf_rec.cpp b/src/library/equations_compiler/wf_rec.cpp index df21570e6e..b3aa8a9743 100644 --- a/src/library/equations_compiler/wf_rec.cpp +++ b/src/library/equations_compiler/wf_rec.cpp @@ -5,14 +5,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/instantiate.h" -#include "kernel/error_msgs.h" +#include "library/error_msgs.h" #include "library/type_context.h" #include "library/trace.h" #include "library/constants.h" #include "library/pp_options.h" #include "library/app_builder.h" #include "library/aux_definition.h" -#include "frontends/lean/elaborator.h" #include "library/replace_visitor_with_tc.h" #include "library/vm/vm.h" #include "library/vm/vm_list.h" @@ -23,6 +22,7 @@ Author: Leonardo de Moura #include "library/equations_compiler/pack_mutual.h" #include "library/equations_compiler/elim_match.h" #include "library/equations_compiler/util.h" +#include "frontends/lean/elaborator.h" namespace lean { #define trace_wf(Code) lean_trace(name({"eqn_compiler", "wf_rec"}), type_context_old ctx = mk_type_context(); scope_trace_env _scope1(m_env, ctx); Code) diff --git a/src/kernel/error_msgs.cpp b/src/library/error_msgs.cpp similarity index 99% rename from src/kernel/error_msgs.cpp rename to src/library/error_msgs.cpp index 41a2a32527..7becd4de9f 100644 --- a/src/kernel/error_msgs.cpp +++ b/src/library/error_msgs.cpp @@ -9,7 +9,7 @@ Author: Leonardo de Moura #include "util/name_set.h" #include "kernel/replace_fn.h" #include "kernel/for_each_fn.h" -#include "kernel/error_msgs.h" +#include "library/error_msgs.h" namespace lean { format pp_indent_expr(formatter const & fmt, expr const & e) { diff --git a/src/kernel/error_msgs.h b/src/library/error_msgs.h similarity index 98% rename from src/kernel/error_msgs.h rename to src/library/error_msgs.h index 54c907870e..4681504495 100644 --- a/src/kernel/error_msgs.h +++ b/src/library/error_msgs.h @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include "kernel/expr.h" -#include "kernel/formatter.h" +#include "library/formatter.h" namespace lean { format pp_indent_expr(formatter const & fmt, expr const & e); format pp_type_expected(formatter const & fmt, expr const & e, expr const * fn_type = nullptr); diff --git a/src/library/exception.h b/src/library/exception.h index 5c918c4dac..cc634c26ce 100644 --- a/src/library/exception.h +++ b/src/library/exception.h @@ -7,8 +7,8 @@ Author: Leonardo de Moura #pragma once #include #include "runtime/sstream.h" -#include "kernel/ext_exception.h" -#include "kernel/scope_pos_info_provider.h" +#include "library/ext_exception.h" +#include "library/scope_pos_info_provider.h" namespace lean { class generic_exception : public ext_exception { diff --git a/src/kernel/ext_exception.h b/src/library/ext_exception.h similarity index 96% rename from src/kernel/ext_exception.h rename to src/library/ext_exception.h index 235b0fefdb..6f195184b6 100644 --- a/src/kernel/ext_exception.h +++ b/src/library/ext_exception.h @@ -8,8 +8,8 @@ Author: Leonardo de Moura #include "runtime/exception.h" #include "util/exception_with_pos.h" #include "util/sexpr/options.h" -#include "kernel/formatter.h" #include "kernel/expr.h" +#include "library/formatter.h" namespace lean { /** \brief Base class for exceptions with support for pretty printing on demand. */ diff --git a/src/kernel/formatter.cpp b/src/library/formatter.cpp similarity index 98% rename from src/kernel/formatter.cpp rename to src/library/formatter.cpp index a43df5d041..6d852349d0 100644 --- a/src/kernel/formatter.cpp +++ b/src/library/formatter.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include #include "util/sexpr/option_declarations.h" -#include "kernel/formatter.h" +#include "library/formatter.h" #ifndef LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS #define LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS false diff --git a/src/kernel/formatter.h b/src/library/formatter.h similarity index 100% rename from src/kernel/formatter.h rename to src/library/formatter.h diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 1df783755e..ca28ec9f59 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -51,9 +51,13 @@ Author: Leonardo de Moura #include "library/profiling.h" #include "library/time_task.h" #include "library/unique_id.h" +#include "library/error_msgs.h" +#include "library/formatter.h" namespace lean { void initialize_library_core_module() { + initialize_error_msgs(); + initialize_formatter(); initialize_constants(); initialize_profiling(); initialize_trace(); @@ -69,6 +73,8 @@ void finalize_library_core_module() { finalize_trace(); finalize_profiling(); finalize_constants(); + finalize_formatter(); + finalize_error_msgs(); } void initialize_library_module() { diff --git a/src/library/io_state.h b/src/library/io_state.h index fad93b3355..848ead03be 100644 --- a/src/library/io_state.h +++ b/src/library/io_state.h @@ -10,7 +10,8 @@ Author: Leonardo de Moura #include "util/sexpr/options.h" #include "util/exception_with_pos.h" #include "kernel/expr.h" -#include "kernel/scope_pos_info_provider.h" +#include "library/formatter.h" +#include "library/scope_pos_info_provider.h" namespace lean { /** diff --git a/src/library/io_state_stream.h b/src/library/io_state_stream.h index 4af151a478..fa3355fb4e 100644 --- a/src/library/io_state_stream.h +++ b/src/library/io_state_stream.h @@ -7,10 +7,10 @@ Author: Leonardo de Moura #pragma once #include #include "kernel/environment.h" -#include "kernel/ext_exception.h" #include "kernel/abstract_type_context.h" #include "library/exception.h" #include "library/io_state.h" +#include "library/ext_exception.h" namespace lean { /** \brief Base class for \c regular and \c diagnostic wrapper classes. */ diff --git a/src/library/local_context.h b/src/library/local_context.h index 6c3aed8d41..4269bca6ba 100644 --- a/src/library/local_context.h +++ b/src/library/local_context.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "util/name_set.h" #include "kernel/local_ctx.h" #include "kernel/expr.h" +#include "library/formatter.h" #include "library/local_instances.h" #include "library/subscripted_name_set.h" diff --git a/src/library/module.h b/src/library/module.h index 195f092601..c92e421fbb 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -12,9 +12,9 @@ Author: Leonardo de Moura #include "runtime/serializer.h" #include "runtime/optional.h" #include "util/task.h" -#include "kernel/pos_info_provider.h" #include "kernel/inductive/inductive.h" #include "library/io_state.h" +#include "library/pos_info_provider.h" namespace lean { class corrupted_file_exception : public exception { diff --git a/src/kernel/pos_info_provider.cpp b/src/library/pos_info_provider.cpp similarity index 93% rename from src/kernel/pos_info_provider.cpp rename to src/library/pos_info_provider.cpp index 37cc22facd..11966f67b1 100644 --- a/src/kernel/pos_info_provider.cpp +++ b/src/library/pos_info_provider.cpp @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "kernel/pos_info_provider.h" +#include "library/pos_info_provider.h" namespace lean { char const * pos_info_provider::get_file_name() const { diff --git a/src/kernel/pos_info_provider.h b/src/library/pos_info_provider.h similarity index 100% rename from src/kernel/pos_info_provider.h rename to src/library/pos_info_provider.h diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp index 64d448b7d1..e5d8da969e 100644 --- a/src/library/pp_options.cpp +++ b/src/library/pp_options.cpp @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "util/sexpr/option_declarations.h" -#include "kernel/error_msgs.h" +#include "library/error_msgs.h" #include "library/pp_options.h" #ifndef LEAN_DEFAULT_PP_MAX_DEPTH diff --git a/src/library/print.cpp b/src/library/print.cpp index f78aeaebc7..fbd3e26e64 100644 --- a/src/library/print.cpp +++ b/src/library/print.cpp @@ -5,11 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "kernel/formatter.h" #include "kernel/environment.h" #include "kernel/find_fn.h" #include "kernel/instantiate.h" #include "kernel/free_vars.h" +#include "library/formatter.h" #include "library/annotation.h" #include "library/util.h" #include "library/print.h" diff --git a/src/library/print.h b/src/library/print.h index f69b2f8ec0..5efbab2c93 100644 --- a/src/library/print.h +++ b/src/library/print.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/formatter.h" +#include "library/formatter.h" namespace lean { /** \brief Return true iff \c t contains a constant named \c n or a local constant with named (pp or not) \c n */ diff --git a/src/kernel/scope_pos_info_provider.cpp b/src/library/scope_pos_info_provider.cpp similarity index 96% rename from src/kernel/scope_pos_info_provider.cpp rename to src/library/scope_pos_info_provider.cpp index efcfcfd893..3eda691fad 100644 --- a/src/kernel/scope_pos_info_provider.cpp +++ b/src/library/scope_pos_info_provider.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include #include "runtime/sstream.h" -#include "kernel/scope_pos_info_provider.h" +#include "library/scope_pos_info_provider.h" namespace lean { LEAN_THREAD_PTR(pos_info_provider, g_p); diff --git a/src/kernel/scope_pos_info_provider.h b/src/library/scope_pos_info_provider.h similarity index 93% rename from src/kernel/scope_pos_info_provider.h rename to src/library/scope_pos_info_provider.h index 0ae079f4f7..a8de0a5c3d 100644 --- a/src/kernel/scope_pos_info_provider.h +++ b/src/library/scope_pos_info_provider.h @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include -#include "kernel/pos_info_provider.h" +#include "library/pos_info_provider.h" namespace lean { class scope_pos_info_provider { diff --git a/src/library/tactic/elaborator_exception.cpp b/src/library/tactic/elaborator_exception.cpp index 2ce6efeec6..1e4d6a8341 100644 --- a/src/library/tactic/elaborator_exception.cpp +++ b/src/library/tactic/elaborator_exception.cpp @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "kernel/scope_pos_info_provider.h" +#include "library/scope_pos_info_provider.h" #include "library/tactic/elaborator_exception.h" namespace lean { diff --git a/src/library/tactic/eval.cpp b/src/library/tactic/eval.cpp index ee71893e91..b36c644ea2 100644 --- a/src/library/tactic/eval.cpp +++ b/src/library/tactic/eval.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include "util/fresh_name.h" #include "kernel/kernel_exception.h" #include "kernel/old_type_checker.h" -#include "kernel/error_msgs.h" +#include "library/error_msgs.h" #include "library/trace.h" #include "library/util.h" #include "library/vm/vm.h" diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index cee721fa90..0dc92d5028 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "util/fresh_name.h" #include "util/sexpr/option_declarations.h" #include "kernel/instantiate.h" -#include "kernel/error_msgs.h" +#include "library/error_msgs.h" #include "library/trace.h" #include "library/util.h" #include "library/user_recursors.h" diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp index b7ff851c86..f160e38257 100644 --- a/src/library/tactic/simp_lemmas.cpp +++ b/src/library/tactic/simp_lemmas.cpp @@ -6,10 +6,10 @@ Author: Leonardo de Moura */ #include #include -#include "kernel/error_msgs.h" #include "kernel/instantiate.h" #include "kernel/for_each_fn.h" #include "kernel/find_fn.h" +#include "library/error_msgs.h" #include "library/constants.h" #include "library/trace.h" #include "library/util.h" diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 7cadf2820c..07b8397fb6 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -10,11 +10,11 @@ Author: Leonardo de Moura #include "util/sexpr/option_declarations.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" -#include "kernel/error_msgs.h" #include "kernel/replace_fn.h" #include "kernel/for_each_fn.h" #include "kernel/quot.h" #include "kernel/inductive/inductive.h" +#include "library/error_msgs.h" #include "library/trace.h" #include "library/class.h" #include "library/pp_options.h" diff --git a/src/library/util.cpp b/src/library/util.cpp index 720706552d..6a29c7d1a7 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -10,11 +10,11 @@ Author: Leonardo de Moura #include "kernel/find_fn.h" #include "kernel/free_vars.h" #include "kernel/instantiate.h" -#include "kernel/error_msgs.h" #include "kernel/old_type_checker.h" #include "kernel/abstract.h" #include "kernel/abstract_type_context.h" #include "kernel/inductive/inductive.h" +#include "library/error_msgs.h" #include "library/locals.h" #include "library/util.h" #include "library/annotation.h" diff --git a/src/library/vm/interaction_state.h b/src/library/vm/interaction_state.h index d07924f9d4..e2933493c0 100644 --- a/src/library/vm/interaction_state.h +++ b/src/library/vm/interaction_state.h @@ -7,7 +7,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich #pragma once #include #include "kernel/environment.h" -#include "kernel/scope_pos_info_provider.h" +#include "library/scope_pos_info_provider.h" #include "library/type_context.h" #include "library/vm/vm.h" diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index 4ff4038f58..127e7cef21 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -17,7 +17,7 @@ Author: Leonardo de Moura #include "runtime/compiler_hints.h" #include "util/rc.h" #include "kernel/environment.h" -#include "kernel/pos_info_provider.h" +#include "library/pos_info_provider.h" namespace lean { class vm_obj; diff --git a/src/library/vm/vm_format.cpp b/src/library/vm/vm_format.cpp index 8a765b29da..9a59143b90 100644 --- a/src/library/vm/vm_format.cpp +++ b/src/library/vm/vm_format.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "util/sexpr/format.h" #include "library/trace.h" #include "library/parray.h" -#include "kernel/scope_pos_info_provider.h" +#include "library/scope_pos_info_provider.h" #include "library/vm/vm.h" #include "library/vm/vm_array.h" #include "library/vm/vm_io.h" diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 8c58b41466..93388cfb81 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -27,8 +27,8 @@ Author: Leonardo de Moura #include "util/sexpr/option_declarations.h" #include "kernel/environment.h" #include "kernel/kernel_exception.h" -#include "kernel/formatter.h" #include "kernel/standard_kernel.h" +#include "library/formatter.h" #include "library/st_task_queue.h" #include "library/eval_helper.h" #include "library/mt_task_queue.h" diff --git a/src/shell/server.h b/src/shell/server.h index e4379be82f..bfb2e0e4f9 100644 --- a/src/shell/server.h +++ b/src/shell/server.h @@ -7,13 +7,13 @@ Authors: Gabriel Ebner, Sebastian Ullrich #pragma once #include #include -#include "kernel/pos_info_provider.h" +#include "util/cancellable.h" #include "kernel/environment.h" +#include "library/pos_info_provider.h" #include "library/io_state.h" #include "library/module_mgr.h" -#include "frontends/lean/json.h" #include "library/mt_task_queue.h" -#include "util/cancellable.h" +#include "frontends/lean/json.h" namespace lean { diff --git a/src/shell/simple_pos_info_provider.h b/src/shell/simple_pos_info_provider.h index 84285c75dc..815bad4b78 100644 --- a/src/shell/simple_pos_info_provider.h +++ b/src/shell/simple_pos_info_provider.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "kernel/pos_info_provider.h" +#include "library/pos_info_provider.h" namespace lean { class simple_pos_info_provider : public pos_info_provider { char const * m_fname;