From d98aabe9ab2fac104626cf67a367746ebabb2978 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 10 Dec 2014 11:23:23 -0800 Subject: [PATCH] refactor(library): move library/definitional/util module to library --- src/frontends/lean/builtin_cmds.cpp | 2 +- src/frontends/lean/inductive_cmd.cpp | 2 +- src/frontends/lean/structure_cmd.cpp | 2 +- src/library/CMakeLists.txt | 2 +- src/library/definitional/CMakeLists.txt | 2 +- src/library/definitional/brec_on.cpp | 2 +- src/library/definitional/induction_on.cpp | 2 +- src/library/definitional/init_module.cpp | 4 +--- src/library/definitional/no_confusion.cpp | 2 +- src/library/init_module.cpp | 3 +++ src/library/{definitional => }/util.cpp | 4 ++-- src/library/{definitional => }/util.h | 4 ++-- 12 files changed, 16 insertions(+), 15 deletions(-) rename src/library/{definitional => }/util.cpp (99%) rename src/library/{definitional => }/util.h (98%) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 47acb6398..d0fb5a753 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -23,8 +23,8 @@ Author: Leonardo de Moura #include "library/print.h" #include "library/class.h" #include "library/flycheck.h" +#include "library/util.h" #include "library/definitional/projection.h" -#include "library/definitional/util.h" #include "frontends/lean/util.h" #include "frontends/lean/parser.h" #include "frontends/lean/calc.h" diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 40780125e..f1502d2ba 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -22,12 +22,12 @@ Author: Leonardo de Moura #include "library/explicit.h" #include "library/reducible.h" #include "library/class.h" +#include "library/util.h" #include "library/definitional/rec_on.h" #include "library/definitional/induction_on.h" #include "library/definitional/cases_on.h" #include "library/definitional/brec_on.h" #include "library/definitional/no_confusion.h" -#include "library/definitional/util.h" #include "frontends/lean/decl_cmds.h" #include "frontends/lean/util.h" #include "frontends/lean/parser.h" diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 1278a7d87..34a6a582d 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -27,10 +27,10 @@ Author: Leonardo de Moura #include "library/explicit.h" #include "library/protected.h" #include "library/class.h" +#include "library/util.h" #include "library/definitional/rec_on.h" #include "library/definitional/induction_on.h" #include "library/definitional/cases_on.h" -#include "library/definitional/util.h" #include "library/definitional/projection.h" #include "library/definitional/no_confusion.h" #include "frontends/lean/parser.h" diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 084548a23..40a67c178 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -7,7 +7,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp standard_kernel.cpp sorry.cpp replace_visitor.cpp unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp explicit.cpp num.cpp string.cpp head_map.cpp match.cpp - definition_cache.cpp declaration_index.cpp class.cpp + definition_cache.cpp declaration_index.cpp class.cpp util.cpp print.cpp annotation.cpp typed_expr.cpp let.cpp type_util.cpp protected.cpp metavar_closure.cpp reducible.cpp init_module.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp) diff --git a/src/library/definitional/CMakeLists.txt b/src/library/definitional/CMakeLists.txt index 512f0886f..569c27c5c 100644 --- a/src/library/definitional/CMakeLists.txt +++ b/src/library/definitional/CMakeLists.txt @@ -1,5 +1,5 @@ add_library(definitional rec_on.cpp induction_on.cpp cases_on.cpp - no_confusion.cpp util.cpp projection.cpp brec_on.cpp equations.cpp + no_confusion.cpp projection.cpp brec_on.cpp equations.cpp init_module.cpp) target_link_libraries(definitional ${LEAN_LIBS}) diff --git a/src/library/definitional/brec_on.cpp b/src/library/definitional/brec_on.cpp index 9c1352a36..c4b50602b 100644 --- a/src/library/definitional/brec_on.cpp +++ b/src/library/definitional/brec_on.cpp @@ -14,7 +14,7 @@ Author: Leonardo de Moura #include "library/reducible.h" #include "library/module.h" #include "library/bin_app.h" -#include "library/definitional/util.h" +#include "library/util.h" namespace lean { static void throw_corrupted(name const & n) { diff --git a/src/library/definitional/induction_on.cpp b/src/library/definitional/induction_on.cpp index cfc5b23c6..b1c7c499a 100644 --- a/src/library/definitional/induction_on.cpp +++ b/src/library/definitional/induction_on.cpp @@ -10,7 +10,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "library/module.h" #include "library/protected.h" -#include "library/definitional/util.h" +#include "library/util.h" namespace lean { environment mk_induction_on(environment const & env, name const & n) { diff --git a/src/library/definitional/init_module.cpp b/src/library/definitional/init_module.cpp index 89ab0bd35..fd527cbad 100644 --- a/src/library/definitional/init_module.cpp +++ b/src/library/definitional/init_module.cpp @@ -4,17 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "library/definitional/util.h" +#include "library/util.h" #include "library/definitional/equations.h" namespace lean{ void initialize_definitional_module() { - initialize_definitional_util(); initialize_equations(); } void finalize_definitional_module() { finalize_equations(); - finalize_definitional_util(); } } diff --git a/src/library/definitional/no_confusion.cpp b/src/library/definitional/no_confusion.cpp index d36464457..c01c48774 100644 --- a/src/library/definitional/no_confusion.cpp +++ b/src/library/definitional/no_confusion.cpp @@ -12,7 +12,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "library/protected.h" #include "library/module.h" -#include "library/definitional/util.h" +#include "library/util.h" namespace lean { static void throw_corrupted(name const & n) { diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 00dedd85e..0b5c9da50 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -30,6 +30,7 @@ Author: Leonardo de Moura #include "library/placeholder.h" #include "library/print.h" #include "library/fingerprint.h" +#include "library/util.h" namespace lean { void initialize_library_module() { @@ -59,9 +60,11 @@ void initialize_library_module() { initialize_unifier_plugin(); initialize_sorry(); initialize_class(); + initialize_library_util(); } void finalize_library_module() { + finalize_library_util(); finalize_class(); finalize_sorry(); finalize_unifier_plugin(); diff --git a/src/library/definitional/util.cpp b/src/library/util.cpp similarity index 99% rename from src/library/definitional/util.cpp rename to src/library/util.cpp index cfe8bcb68..afb3880c3 100644 --- a/src/library/definitional/util.cpp +++ b/src/library/util.cpp @@ -155,7 +155,7 @@ static name * g_eq_name = nullptr; static name * g_eq_refl_name = nullptr; static name * g_eq_rec_name = nullptr; -void initialize_definitional_util() { +void initialize_library_util() { g_true = new expr(mk_constant("true")); g_true_intro = new expr(mk_constant(name({"true", "intro"}))); g_and = new expr(mk_constant("and")); @@ -175,7 +175,7 @@ void initialize_definitional_util() { g_eq_rec_name = new name{"eq", "rec"}; } -void finalize_definitional_util() { +void finalize_library_util() { delete g_true; delete g_true_intro; delete g_and; diff --git a/src/library/definitional/util.h b/src/library/util.h similarity index 98% rename from src/library/definitional/util.h rename to src/library/util.h index cd02647af..b3a91814a 100644 --- a/src/library/definitional/util.h +++ b/src/library/util.h @@ -86,6 +86,6 @@ void mk_telescopic_eq(type_checker & tc, buffer const & t, buffer & level mk_max(levels const & ls); -void initialize_definitional_util(); -void finalize_definitional_util(); +void initialize_library_util(); +void finalize_library_util(); }