Rename arith library files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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"
 

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"

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})

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);
 }
 }

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);
 }

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);

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);
 }

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);

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);
 }

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");

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();

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");

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);
 }

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;

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;
 

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;
 

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() {

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) {

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); }

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"