From b746492ac8c8149454ab9cc66370537f1431a268 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 22 Aug 2014 10:32:01 -0700 Subject: [PATCH] refactor(library/simple_formatter): rename simple_formatter to print Signed-off-by: Leonardo de Moura --- src/frontends/lean/pp.cpp | 2 +- src/library/CMakeLists.txt | 2 +- src/library/io_state.cpp | 4 ++-- src/library/kernel_bindings.cpp | 8 ++++---- src/library/{simple_formatter.cpp => print.cpp} | 4 ++-- src/library/{simple_formatter.h => print.h} | 7 +++++-- src/library/unifier.cpp | 4 ++-- src/shell/lean.cpp | 2 +- src/tests/kernel/environment.cpp | 4 ++-- src/tests/kernel/expr.cpp | 2 +- src/tests/kernel/max_sharing.cpp | 2 +- src/tests/kernel/metavar.cpp | 2 +- src/tests/kernel/replace.cpp | 2 +- 13 files changed, 24 insertions(+), 21 deletions(-) rename src/library/{simple_formatter.cpp => print.cpp} (98%) rename src/library/{simple_formatter.h => print.h} (85%) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index d56281763..2cd2dadc4 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -16,7 +16,7 @@ Author: Leonardo de Moura #include "library/private.h" #include "library/explicit.h" #include "library/num.h" -#include "library/simple_formatter.h" +#include "library/print.h" #include "frontends/lean/pp.h" #include "frontends/lean/pp_options.h" #include "frontends/lean/token_table.h" diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 2abb631dd..fe81461a8 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -8,6 +8,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp explicit.cpp num.cpp string.cpp opaque_hints.cpp head_map.cpp match.cpp definition_cache.cpp declaration_index.cpp - simple_formatter.cpp) + print.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/io_state.cpp b/src/library/io_state.cpp index f313ab4a9..83c6068af 100644 --- a/src/library/io_state.cpp +++ b/src/library/io_state.cpp @@ -5,11 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/kernel_exception.h" -#include "library/simple_formatter.h" +#include "library/print.h" #include "library/io_state.h" namespace lean { -static io_state g_dummy_ios(mk_simple_formatter_factory()); +static io_state g_dummy_ios(mk_print_formatter_factory()); io_state const & get_dummy_ios() { return g_dummy_ios; } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 2961b56dd..9a971d009 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -31,7 +31,7 @@ Author: Leonardo de Moura #include "library/normalize.h" #include "library/module.h" #include "library/opaque_hints.h" -#include "library/simple_formatter.h" +#include "library/print.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. @@ -878,7 +878,7 @@ static const struct luaL_Reg formatter_m[] = { }; static char g_formatter_factory_key; -static formatter_factory g_simple_formatter_factory = mk_simple_formatter_factory(); +static formatter_factory g_print_formatter_factory = mk_print_formatter_factory(); optional get_global_formatter_factory_core(lua_State * L) { io_state * io = get_io_state_ptr(L); @@ -903,7 +903,7 @@ formatter_factory get_global_formatter_factory(lua_State * L) { if (r) return *r; else - return g_simple_formatter_factory; + return g_print_formatter_factory; } void set_global_formatter_factory(lua_State * L, formatter_factory const & fmtf) { @@ -1223,7 +1223,7 @@ io_state to_io_state_ext(lua_State * L, int idx) { int mk_io_state(lua_State * L) { int nargs = lua_gettop(L); if (nargs == 0) - return push_io_state(L, io_state(mk_simple_formatter_factory())); + return push_io_state(L, io_state(mk_print_formatter_factory())); else if (nargs == 1) return push_io_state(L, io_state(to_io_state(L, 1))); else diff --git a/src/library/simple_formatter.cpp b/src/library/print.cpp similarity index 98% rename from src/library/simple_formatter.cpp rename to src/library/print.cpp index ee39ed43d..41f209bf2 100644 --- a/src/library/simple_formatter.cpp +++ b/src/library/print.cpp @@ -11,7 +11,7 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/free_vars.h" #include "kernel/annotation.h" -#include "library/simple_formatter.h" +#include "library/print.h" namespace lean { bool is_used_name(expr const & t, name const & n) { @@ -249,7 +249,7 @@ struct print_expr_fn { } }; -formatter_factory mk_simple_formatter_factory() { +formatter_factory mk_print_formatter_factory() { return [](environment const & env, options const & o) { // NOLINT return formatter(o, [=](expr const & e, options const &) { std::ostringstream s; diff --git a/src/library/simple_formatter.h b/src/library/print.h similarity index 85% rename from src/library/simple_formatter.h rename to src/library/print.h index d63cba0e1..62de98d51 100644 --- a/src/library/simple_formatter.h +++ b/src/library/print.h @@ -22,8 +22,11 @@ pair binding_body_fresh(expr const & b, bool preserve_type = false); /** \brief Return the body of the let-expression \c l, where variable #0 is replaced by a local constant with a "fresh" name. */ pair let_body_fresh(expr const & l, bool preserve_type = false); -/** \brief Create a simple formatter object based on operator */ -formatter_factory mk_simple_formatter_factory(); +/** \brief Create a simple formatter object based on operator for "print" procedure. + + \remark The print procedure is only used for debugging purposes. +*/ +formatter_factory mk_print_formatter_factory(); /** \brief Use simple formatter as the default print function */ void init_default_print_fn(); diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 0fed3cfcc..60c5a0d77 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -26,7 +26,7 @@ Author: Leonardo de Moura #include "library/opaque_hints.h" #include "library/unifier_plugin.h" #include "library/kernel_bindings.h" -#include "library/simple_formatter.h" +#include "library/print.h" #ifndef LEAN_DEFAULT_UNIFIER_MAX_STEPS #define LEAN_DEFAULT_UNIFIER_MAX_STEPS 20000 @@ -993,7 +993,7 @@ struct unifier_fn { void display(std::ostream & out, justification const & j, unsigned indent = 0) { for (unsigned i = 0; i < indent; i++) out << " "; - out << j.pp(mk_simple_formatter_factory()(m_env, options()), nullptr, m_subst) << "\n"; + out << j.pp(mk_print_formatter_factory()(m_env, options()), nullptr, m_subst) << "\n"; if (j.is_composite()) { display(out, composite_child1(j), indent+2); display(out, composite_child2(j), indent+2); diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index e362c5e10..57b92307f 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -26,7 +26,7 @@ Author: Leonardo de Moura #include "library/io_state_stream.h" #include "library/definition_cache.h" #include "library/declaration_index.h" -#include "library/simple_formatter.h" +#include "library/print.h" #include "library/error_handling/error_handling.h" #include "frontends/lean/parser.h" #include "frontends/lean/pp.h" diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index cb334fc62..24dbe99fb 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -12,7 +12,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "kernel/abstract.h" #include "kernel/kernel_exception.h" -#include "library/simple_formatter.cpp" +#include "library/print.h" using namespace lean; static environment add_decl(environment const & env, declaration const & d) { @@ -21,7 +21,7 @@ static environment add_decl(environment const & env, declaration const & d) { } formatter mk_formatter(environment const & env) { - return mk_simple_formatter_factory()(env, options()); + return mk_print_formatter_factory()(env, options()); } static void tst1() { diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index f4338fdc1..a9af0377f 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -16,7 +16,7 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "library/max_sharing.h" -#include "library/simple_formatter.h" +#include "library/print.h" #include "library/deep_copy.h" #include "library/kernel_serializer.h" using namespace lean; diff --git a/src/tests/kernel/max_sharing.cpp b/src/tests/kernel/max_sharing.cpp index ebe973546..b8eb1f8e2 100644 --- a/src/tests/kernel/max_sharing.cpp +++ b/src/tests/kernel/max_sharing.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "util/test.h" #include "kernel/abstract.h" #include "library/max_sharing.h" -#include "library/simple_formatter.h" +#include "library/print.h" using namespace lean; static void tst1() { diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index d653a8c88..9bc0b2348 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -14,7 +14,7 @@ Author: Leonardo de Moura #include "kernel/metavar.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" -#include "library/simple_formatter.h" +#include "library/print.h" using namespace lean; void collect_assumptions(justification const & j, buffer & r) { diff --git a/src/tests/kernel/replace.cpp b/src/tests/kernel/replace.cpp index df895ad6c..7ab5ccad2 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 "library/simple_formatter.h" +#include "library/print.h" using namespace lean; expr mk_big(expr f, unsigned depth, unsigned val) {