From 0c09e4524ad6dbbe2fe1cc9aaadfa127f391f7d0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Sep 2013 08:58:34 -0700 Subject: [PATCH] Use consistent names for import functions, and library files. Signed-off-by: Leonardo de Moura --- src/frontends/lean/notation.cpp | 2 +- src/kernel/builtin.cpp | 2 +- src/kernel/builtin.h | 2 +- src/library/basic_thms.cpp | 2 +- src/library/basic_thms.h | 2 +- src/library/cast/CMakeLists.txt | 2 +- src/library/cast/{castlib.cpp => cast.cpp} | 4 ++-- src/library/cast/{castlib.h => cast.h} | 2 +- src/library/import_all/import_all.cpp | 8 ++++---- 9 files changed, 13 insertions(+), 13 deletions(-) rename src/library/cast/{castlib.cpp => cast.cpp} (98%) rename src/library/cast/{castlib.h => cast.h} (97%) diff --git a/src/frontends/lean/notation.cpp b/src/frontends/lean/notation.cpp index e36587378..e11eaf092 100644 --- a/src/frontends/lean/notation.cpp +++ b/src/frontends/lean/notation.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include "kernel/builtin.h" #include "library/basic_thms.h" #include "library/arith/arith.h" -#include "library/cast/castlib.h" +#include "library/cast/cast.h" #include "frontends/lean/frontend.h" namespace lean { diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index 6af91a98d..74b02124c 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -159,7 +159,7 @@ MK_CONSTANT(subst_fn, name("Subst")); MK_CONSTANT(eta_fn, name("Eta")); MK_CONSTANT(imp_antisym_fn, name("ImpAntisym")); -void import_basiclib(environment & env) { +void import_basic(environment & env) { env.add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION); env.add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION); diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h index 0be24aae6..62f1fad67 100644 --- a/src/kernel/builtin.h +++ b/src/kernel/builtin.h @@ -150,7 +150,7 @@ inline expr ImpAntisym(expr const & a, expr const & b, expr const & H1, expr con class environment; /** \brief Initialize the environment with basic builtin declarations and axioms */ -void import_basiclib(environment & env); +void import_basic(environment & env); /** \brief Helper macro for defining constants such as bool_type, int_type, int_add, etc. diff --git a/src/library/basic_thms.cpp b/src/library/basic_thms.cpp index 66831fad7..fa129a45e 100644 --- a/src/library/basic_thms.cpp +++ b/src/library/basic_thms.cpp @@ -47,7 +47,7 @@ MK_CONSTANT(domain_inj_fn, name("domain_inj")); MK_CONSTANT(range_inj_fn, name("range_inj")); #endif -void import_basicthms(environment & env) { +void import_basic_thms(environment & env) { expr A = Const("A"); expr a = Const("a"); expr b = Const("b"); diff --git a/src/library/basic_thms.h b/src/library/basic_thms.h index 696b02376..58dfb9b96 100644 --- a/src/library/basic_thms.h +++ b/src/library/basic_thms.h @@ -121,7 +121,7 @@ expr mk_forall_elim_fn(); inline expr ForallElim(expr const & A, expr const & P, expr const & H, expr const & a) { return mk_app(mk_forall_elim_fn(), A, P, H, a); } /** \brief Add basic theorems to Environment */ -void import_basicthms(environment & env); +void import_basic_thms(environment & env); #if 0 expr mk_ext_fn(); diff --git a/src/library/cast/CMakeLists.txt b/src/library/cast/CMakeLists.txt index 30dce5773..cdc7abe9d 100644 --- a/src/library/cast/CMakeLists.txt +++ b/src/library/cast/CMakeLists.txt @@ -1,2 +1,2 @@ -add_library(castlib castlib.cpp) +add_library(castlib cast.cpp) target_link_libraries(castlib ${LEAN_LIBS}) diff --git a/src/library/cast/castlib.cpp b/src/library/cast/cast.cpp similarity index 98% rename from src/library/cast/castlib.cpp rename to src/library/cast/cast.cpp index 5f4716959..48ee152e6 100644 --- a/src/library/cast/castlib.cpp +++ b/src/library/cast/cast.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/builtin.h" #include "library/basic_thms.h" -#include "library/cast/castlib.h" +#include "library/cast/cast.h" namespace lean { // Cast builtin operator @@ -104,7 +104,7 @@ MK_CONSTANT(cast_fn, name("cast")); MK_CONSTANT(dom_inj_fn, name("DomInj")); MK_CONSTANT(ran_inj_fn, name("RanInj")); -void import_castlib(environment & env) { +void import_cast(environment & env) { if (env.find_object(to_value(mk_Cast_fn()).get_name())) return; expr x = Const("x"); diff --git a/src/library/cast/castlib.h b/src/library/cast/cast.h similarity index 97% rename from src/library/cast/castlib.h rename to src/library/cast/cast.h index b35000583..03789fe67 100644 --- a/src/library/cast/castlib.h +++ b/src/library/cast/cast.h @@ -41,5 +41,5 @@ inline expr RanInj(expr const & A, expr const & Ap, expr const & B, expr const & class environment; /** \brief Import type "casting" library */ -void import_castlib(environment & env); +void import_cast(environment & env); } diff --git a/src/library/import_all/import_all.cpp b/src/library/import_all/import_all.cpp index 6f7b4aa7f..c3f49e28b 100644 --- a/src/library/import_all/import_all.cpp +++ b/src/library/import_all/import_all.cpp @@ -7,14 +7,14 @@ Author: Leonardo de Moura #include "kernel/builtin.h" #include "library/basic_thms.h" #include "library/arith/arith.h" -#include "library/cast/castlib.h" +#include "library/cast/cast.h" #include "library/import_all/import_all.h" namespace lean { void import_all(environment & env) { - import_basiclib(env); - import_basicthms(env); - import_castlib(env); + import_basic(env); + import_basic_thms(env); + import_cast(env); import_arith(env); } environment mk_toplevel() {