From 070c87bef08f38879919d4362baff2b33ee39bcb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Sep 2013 08:55:09 -0700 Subject: [PATCH] Rename arith library files Signed-off-by: Leonardo de Moura --- src/frontends/lean/notation.cpp | 2 +- src/frontends/lean/parser.cpp | 2 +- src/library/arith/CMakeLists.txt | 2 +- src/library/arith/{arithlibs.cpp => arith.cpp} | 12 ++++++------ src/library/arith/{arithlibs.h => arith.h} | 10 +++++----- src/library/arith/{intlib.cpp => int.cpp} | 8 ++++---- src/library/arith/{intlib.h => int.h} | 2 +- src/library/arith/{natlib.cpp => nat.cpp} | 4 ++-- src/library/arith/{natlib.h => nat.h} | 2 +- src/library/arith/{reallib.cpp => real.cpp} | 12 ++++++------ src/library/arith/{reallib.h => real.h} | 2 +- .../arith/{specialfnlib.cpp => special_fn.cpp} | 8 ++++---- src/library/arith/{specialfnlib.h => special_fn.h} | 2 +- src/library/import_all/import_all.cpp | 4 ++-- src/tests/kernel/arith.cpp | 2 +- src/tests/kernel/environment.cpp | 2 +- src/tests/kernel/expr.cpp | 2 +- src/tests/kernel/threads.cpp | 2 +- src/tests/kernel/type_checker.cpp | 2 +- src/tests/library/light_checker.cpp | 2 +- 20 files changed, 42 insertions(+), 42 deletions(-) rename src/library/arith/{arithlibs.cpp => arith.cpp} (55%) rename src/library/arith/{arithlibs.h => arith.h} (60%) rename src/library/arith/{intlib.cpp => int.cpp} (97%) rename src/library/arith/{intlib.h => int.h} (98%) rename src/library/arith/{natlib.cpp => nat.cpp} (98%) rename src/library/arith/{natlib.h => nat.h} (98%) rename src/library/arith/{reallib.cpp => real.cpp} (96%) rename src/library/arith/{reallib.h => real.h} (98%) rename src/library/arith/{specialfnlib.cpp => special_fn.cpp} (93%) rename src/library/arith/{specialfnlib.h => special_fn.h} (97%) diff --git a/src/frontends/lean/notation.cpp b/src/frontends/lean/notation.cpp index c07d496fa..e36587378 100644 --- a/src/frontends/lean/notation.cpp +++ b/src/frontends/lean/notation.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include "kernel/builtin.h" #include "library/basic_thms.h" -#include "library/arith/arithlibs.h" +#include "library/arith/arith.h" #include "library/cast/castlib.h" #include "frontends/lean/frontend.h" diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 56b368e18..775037d3b 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -25,7 +25,7 @@ Author: Leonardo de Moura #include "kernel/builtin.h" #include "kernel/kernel_exception.h" #include "kernel/expr_maps.h" -#include "library/arith/arithlibs.h" +#include "library/arith/arith.h" #include "library/printer.h" #include "library/state.h" #include "library/kernel_exception_formatter.h" diff --git a/src/library/arith/CMakeLists.txt b/src/library/arith/CMakeLists.txt index 8a67eab8c..8dc8ca686 100644 --- a/src/library/arith/CMakeLists.txt +++ b/src/library/arith/CMakeLists.txt @@ -1,2 +1,2 @@ -add_library(arithlib natlib.cpp intlib.cpp reallib.cpp specialfnlib.cpp arithlibs.cpp) +add_library(arithlib nat.cpp int.cpp real.cpp special_fn.cpp arith.cpp) target_link_libraries(arithlib ${LEAN_LIBS}) diff --git a/src/library/arith/arithlibs.cpp b/src/library/arith/arith.cpp similarity index 55% rename from src/library/arith/arithlibs.cpp rename to src/library/arith/arith.cpp index 6890f1e5c..7bb9431c6 100644 --- a/src/library/arith/arithlibs.cpp +++ b/src/library/arith/arith.cpp @@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "library/arith/arithlibs.h" +#include "library/arith/arith.h" namespace lean { -void import_arithlibs(environment & env) { - import_natlib(env); - import_intlib(env); - import_reallib(env); +void import_arith(environment & env) { + import_nat(env); + import_int(env); + import_real(env); import_int_to_real_coercions(env); - import_specialfnlib(env); + import_special_fn(env); } } diff --git a/src/library/arith/arithlibs.h b/src/library/arith/arith.h similarity index 60% rename from src/library/arith/arithlibs.h rename to src/library/arith/arith.h index 7175b2163..2e328f772 100644 --- a/src/library/arith/arithlibs.h +++ b/src/library/arith/arith.h @@ -5,15 +5,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "library/arith/natlib.h" -#include "library/arith/intlib.h" -#include "library/arith/reallib.h" -#include "library/arith/specialfnlib.h" +#include "library/arith/nat.h" +#include "library/arith/int.h" +#include "library/arith/real.h" +#include "library/arith/special_fn.h" namespace lean { class environment; /** \brief Import all arithmetic related builtin libraries. */ -void import_arithlibs(environment & env); +void import_arith(environment & env); } diff --git a/src/library/arith/intlib.cpp b/src/library/arith/int.cpp similarity index 97% rename from src/library/arith/intlib.cpp rename to src/library/arith/int.cpp index 28e777db7..dd91ba89d 100644 --- a/src/library/arith/intlib.cpp +++ b/src/library/arith/int.cpp @@ -6,8 +6,8 @@ Author: Leonardo de Moura */ #include "kernel/abstract.h" #include "kernel/environment.h" -#include "library/arith/intlib.h" -#include "library/arith/natlib.h" +#include "library/arith/int.h" +#include "library/arith/nat.h" #include "library/arith/numtype.h" namespace lean { @@ -125,10 +125,10 @@ MK_BUILTIN(nat_to_int_fn, nat_to_int_value); MK_CONSTANT(nat_sub_fn, name({"Nat", "sub"})); MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"})); -void import_intlib(environment & env) { +void import_int(environment & env) { if (env.find_object(to_value(Int).get_name())) return; - import_natlib(env); + import_nat(env); expr i_i = Int >> Int; expr ii_b = Int >> (Int >> Bool); expr ii_i = Int >> (Int >> Int); diff --git a/src/library/arith/intlib.h b/src/library/arith/int.h similarity index 98% rename from src/library/arith/intlib.h rename to src/library/arith/int.h index 0fe4775f3..0e4ae37f6 100644 --- a/src/library/arith/intlib.h +++ b/src/library/arith/int.h @@ -89,5 +89,5 @@ class environment; \brief Import Integer number library in the given environment (if it has not been imported already). It will also load the natural number library. */ -void import_intlib(environment & env); +void import_int(environment & env); } diff --git a/src/library/arith/natlib.cpp b/src/library/arith/nat.cpp similarity index 98% rename from src/library/arith/natlib.cpp rename to src/library/arith/nat.cpp index 59bf16836..c52d7bad6 100644 --- a/src/library/arith/natlib.cpp +++ b/src/library/arith/nat.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include "kernel/abstract.h" #include "kernel/environment.h" -#include "library/arith/natlib.h" +#include "library/arith/nat.h" #include "library/arith/numtype.h" namespace lean { @@ -91,7 +91,7 @@ MK_CONSTANT(nat_lt_fn, name({"Nat", "lt"})); MK_CONSTANT(nat_gt_fn, name({"Nat", "gt"})); MK_CONSTANT(nat_id_fn, name({"Nat", "id"})); -void import_natlib(environment & env) { +void import_nat(environment & env) { if (env.find_object(to_value(Nat).get_name())) return; expr nn_b = Nat >> (Nat >> Bool); diff --git a/src/library/arith/natlib.h b/src/library/arith/nat.h similarity index 98% rename from src/library/arith/natlib.h rename to src/library/arith/nat.h index 6c8c31757..19ecc3b32 100644 --- a/src/library/arith/natlib.h +++ b/src/library/arith/nat.h @@ -54,5 +54,5 @@ inline expr nIf(expr const & c, expr const & t, expr const & e) { return mk_if(N class environment; /** \brief Import Natural number library in the given environment (if it has not been imported already). */ -void import_natlib(environment & env); +void import_nat(environment & env); } diff --git a/src/library/arith/reallib.cpp b/src/library/arith/real.cpp similarity index 96% rename from src/library/arith/reallib.cpp rename to src/library/arith/real.cpp index 8c0e98ba9..f9d2a2e81 100644 --- a/src/library/arith/reallib.cpp +++ b/src/library/arith/real.cpp @@ -6,9 +6,9 @@ Author: Leonardo de Moura */ #include "kernel/abstract.h" #include "kernel/environment.h" -#include "library/arith/reallib.h" -#include "library/arith/intlib.h" -#include "library/arith/natlib.h" +#include "library/arith/real.h" +#include "library/arith/int.h" +#include "library/arith/nat.h" #include "library/arith/numtype.h" namespace lean { @@ -107,7 +107,7 @@ MK_CONSTANT(real_ge_fn, name({"Real", "ge"})); MK_CONSTANT(real_lt_fn, name({"Real", "lt"})); MK_CONSTANT(real_gt_fn, name({"Real", "gt"})); -void import_reallib(environment & env) { +void import_real(environment & env) { if (env.find_object(to_value(Real).get_name())) return; expr rr_b = Real >> (Real >> Bool); @@ -149,8 +149,8 @@ MK_CONSTANT(nat_to_real_fn, name("nat_to_real")); void import_int_to_real_coercions(environment & env) { if (env.find_object(to_value(mk_int_to_real_fn()).get_name())) return; - import_intlib(env); - import_reallib(env); + import_int(env); + import_real(env); env.add_builtin(mk_int_to_real_fn()); expr x = Const("x"); diff --git a/src/library/arith/reallib.h b/src/library/arith/real.h similarity index 98% rename from src/library/arith/reallib.h rename to src/library/arith/real.h index a771a6a39..8d8e6761a 100644 --- a/src/library/arith/reallib.h +++ b/src/library/arith/real.h @@ -66,7 +66,7 @@ inline expr rIf(expr const & c, expr const & t, expr const & e) { return mk_if(R class environment; /** \brief Import (basic) Real number library in the given environment (if it has not been imported already). */ -void import_reallib(environment & env); +void import_real(environment & env); /** \brief Coercion from int to real */ expr mk_int_to_real_fn(); diff --git a/src/library/arith/specialfnlib.cpp b/src/library/arith/special_fn.cpp similarity index 93% rename from src/library/arith/specialfnlib.cpp rename to src/library/arith/special_fn.cpp index 0c3b316fe..cb411f4c7 100644 --- a/src/library/arith/specialfnlib.cpp +++ b/src/library/arith/special_fn.cpp @@ -6,8 +6,8 @@ Author: Leonardo de Moura */ #include "kernel/environment.h" #include "kernel/abstract.h" -#include "library/arith/specialfnlib.h" -#include "library/arith/reallib.h" +#include "library/arith/special_fn.h" +#include "library/arith/real.h" namespace lean { MK_CONSTANT(exp_fn, name("exp")); @@ -28,10 +28,10 @@ MK_CONSTANT(coth_fn, name("coth")); MK_CONSTANT(sech_fn, name("sech")); MK_CONSTANT(csch_fn, name("csch")); -void import_specialfnlib(environment & env) { +void import_special_fn(environment & env) { if (env.find_object(const_name(mk_exp_fn()))) return; - import_reallib(env); + import_real(env); expr r_r = Real >> Real; expr x = Const("x"); diff --git a/src/library/arith/specialfnlib.h b/src/library/arith/special_fn.h similarity index 97% rename from src/library/arith/specialfnlib.h rename to src/library/arith/special_fn.h index 525cec510..8c2a96c64 100644 --- a/src/library/arith/specialfnlib.h +++ b/src/library/arith/special_fn.h @@ -59,5 +59,5 @@ class environment; \brief Import the special function library (if it has not been imported already). The (basic) Real Number library is also imported. */ -void import_specialfnlib(environment & env); +void import_special_fn(environment & env); } diff --git a/src/library/import_all/import_all.cpp b/src/library/import_all/import_all.cpp index 77fb27d0a..6f7b4aa7f 100644 --- a/src/library/import_all/import_all.cpp +++ b/src/library/import_all/import_all.cpp @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #include "kernel/builtin.h" #include "library/basic_thms.h" -#include "library/arith/arithlibs.h" +#include "library/arith/arith.h" #include "library/cast/castlib.h" #include "library/import_all/import_all.h" @@ -15,7 +15,7 @@ void import_all(environment & env) { import_basiclib(env); import_basicthms(env); import_castlib(env); - import_arithlibs(env); + import_arith(env); } environment mk_toplevel() { environment r; diff --git a/src/tests/kernel/arith.cpp b/src/tests/kernel/arith.cpp index 12d150dcf..32e1f82e1 100644 --- a/src/tests/kernel/arith.cpp +++ b/src/tests/kernel/arith.cpp @@ -12,7 +12,7 @@ Author: Leonardo de Moura #include "kernel/normalizer.h" #include "kernel/abstract.h" #include "library/printer.h" -#include "library/arith/arithlibs.h" +#include "library/arith/arith.h" #include "library/import_all/import_all.h" using namespace lean; diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index d69319a26..0f74717f7 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -14,7 +14,7 @@ Author: Leonardo de Moura #include "kernel/normalizer.h" #include "kernel/abstract.h" #include "library/printer.h" -#include "library/arith/arithlibs.h" +#include "library/arith/arith.h" #include "library/import_all/import_all.h" using namespace lean; diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 60ec2c0e2..c124aa37d 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -15,7 +15,7 @@ Author: Leonardo de Moura #include "library/max_sharing.h" #include "library/deep_copy.h" #include "library/printer.h" -#include "library/arith/arithlibs.h" +#include "library/arith/arith.h" using namespace lean; void tst1() { diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp index d96a2c615..a100781fc 100644 --- a/src/tests/kernel/threads.cpp +++ b/src/tests/kernel/threads.cpp @@ -15,7 +15,7 @@ Author: Leonardo de Moura #include "library/max_sharing.h" #include "library/deep_copy.h" #include "library/import_all/import_all.h" -#include "library/arith/arithlibs.h" +#include "library/arith/arith.h" using namespace lean; expr norm(expr const & e, environment & env) { diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp index 59a64f787..aa93f8151 100644 --- a/src/tests/kernel/type_checker.cpp +++ b/src/tests/kernel/type_checker.cpp @@ -18,7 +18,7 @@ Author: Leonardo de Moura #include "library/printer.h" #include "library/import_all/import_all.h" #include "library/basic_thms.h" -#include "library/arith/arithlibs.h" +#include "library/arith/arith.h" using namespace lean; expr c(char const * n) { return mk_constant(n); } diff --git a/src/tests/library/light_checker.cpp b/src/tests/library/light_checker.cpp index 392dab945..456907c35 100644 --- a/src/tests/library/light_checker.cpp +++ b/src/tests/library/light_checker.cpp @@ -9,7 +9,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "kernel/environment.h" #include "kernel/abstract.h" -#include "library/arith/arithlibs.h" +#include "library/arith/arith.h" #include "library/import_all/import_all.h" #include "library/light_checker.h" #include "library/printer.h"