From c2ebe42ca8c8c42e0ccf2924ac4e6e96c804398f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 24 Jul 2013 14:53:45 -0700 Subject: [PATCH] Move numerics and sexpr to util Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 12 ++++++------ src/tests/kernel/expr.cpp | 6 +++--- src/tests/{ => util}/numerics/CMakeLists.txt | 0 src/tests/{ => util}/numerics/mpbq.cpp | 0 src/tests/{ => util}/numerics/mpq.cpp | 0 src/tests/{ => util}/sexpr/CMakeLists.txt | 0 src/tests/{ => util}/sexpr/sexpr.cpp | 0 src/{ => util}/numerics/CMakeLists.txt | 0 src/{ => util}/numerics/gmp_init.cpp | 0 src/{ => util}/numerics/mpbq.cpp | 0 src/{ => util}/numerics/mpbq.h | 0 src/{ => util}/numerics/mpq.cpp | 0 src/{ => util}/numerics/mpq.h | 0 src/{ => util}/numerics/mpz.cpp | 0 src/{ => util}/numerics/mpz.h | 0 src/{ => util}/numerics/numeric_traits.cpp | 0 src/{ => util}/numerics/numeric_traits.h | 0 src/{ => util}/numerics/xnumeral.h | 0 src/{ => util}/sexpr/CMakeLists.txt | 0 src/{ => util}/sexpr/sexpr.cpp | 0 src/{ => util}/sexpr/sexpr.h | 0 src/{ => util}/sexpr/sexpr_funcs.cpp | 0 src/{ => util}/sexpr/sexpr_funcs.h | 0 23 files changed, 9 insertions(+), 9 deletions(-) rename src/tests/{ => util}/numerics/CMakeLists.txt (100%) rename src/tests/{ => util}/numerics/mpbq.cpp (100%) rename src/tests/{ => util}/numerics/mpq.cpp (100%) rename src/tests/{ => util}/sexpr/CMakeLists.txt (100%) rename src/tests/{ => util}/sexpr/sexpr.cpp (100%) rename src/{ => util}/numerics/CMakeLists.txt (100%) rename src/{ => util}/numerics/gmp_init.cpp (100%) rename src/{ => util}/numerics/mpbq.cpp (100%) rename src/{ => util}/numerics/mpbq.h (100%) rename src/{ => util}/numerics/mpq.cpp (100%) rename src/{ => util}/numerics/mpq.h (100%) rename src/{ => util}/numerics/mpz.cpp (100%) rename src/{ => util}/numerics/mpz.h (100%) rename src/{ => util}/numerics/numeric_traits.cpp (100%) rename src/{ => util}/numerics/numeric_traits.h (100%) rename src/{ => util}/numerics/xnumeral.h (100%) rename src/{ => util}/sexpr/CMakeLists.txt (100%) rename src/{ => util}/sexpr/sexpr.cpp (100%) rename src/{ => util}/sexpr/sexpr.h (100%) rename src/{ => util}/sexpr/sexpr_funcs.cpp (100%) rename src/{ => util}/sexpr/sexpr_funcs.h (100%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index af6c71651..7376ef52b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -42,16 +42,16 @@ else() endif() include_directories(${LEAN_SOURCE_DIR}/util) -include_directories(${LEAN_SOURCE_DIR}/numerics) +include_directories(${LEAN_SOURCE_DIR}/util/numerics) +include_directories(${LEAN_SOURCE_DIR}/util/sexpr) include_directories(${LEAN_SOURCE_DIR}/interval) -include_directories(${LEAN_SOURCE_DIR}/sexpr) include_directories(${LEAN_SOURCE_DIR}/kernel) add_subdirectory(util) set(EXTRA_LIBS ${EXTRA_LIBS} util) -add_subdirectory(numerics) +add_subdirectory(util/numerics) set(EXTRA_LIBS ${EXTRA_LIBS} numerics) -add_subdirectory(sexpr) +add_subdirectory(util/sexpr) set(EXTRA_LIBS ${EXTRA_LIBS} sexpr) add_subdirectory(interval) set(EXTRA_LIBS ${EXTRA_LIBS} interval) @@ -60,7 +60,7 @@ set(EXTRA_LIBS ${EXTRA_LIBS} kernel) set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread") add_subdirectory(shell) add_subdirectory(tests/util) -add_subdirectory(tests/numerics) +add_subdirectory(tests/util/numerics) +add_subdirectory(tests/util/sexpr) add_subdirectory(tests/interval) -add_subdirectory(tests/sexpr) add_subdirectory(tests/kernel) diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index 9c9e2378a..433e5d981 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -109,9 +109,9 @@ unsigned depth3(expr const & e) { void tst2() { expr r1 = mk_dag(20); expr r2 = mk_dag(20); - lean_verify(r1 == r2); + lean_assert(r1 == r2); std::cout << depth2(r1) << "\n"; - lean_verify(depth2(r1) == 21); + lean_assert(depth2(r1) == 21); } expr mk_big(expr f, unsigned depth, unsigned val) { @@ -125,7 +125,7 @@ void tst3() { expr f = constant("f"); expr r1 = mk_big(f, 18, 0); expr r2 = mk_big(f, 18, 0); - lean_verify(r1 == r2); + lean_assert(r1 == r2); } void tst4() { diff --git a/src/tests/numerics/CMakeLists.txt b/src/tests/util/numerics/CMakeLists.txt similarity index 100% rename from src/tests/numerics/CMakeLists.txt rename to src/tests/util/numerics/CMakeLists.txt diff --git a/src/tests/numerics/mpbq.cpp b/src/tests/util/numerics/mpbq.cpp similarity index 100% rename from src/tests/numerics/mpbq.cpp rename to src/tests/util/numerics/mpbq.cpp diff --git a/src/tests/numerics/mpq.cpp b/src/tests/util/numerics/mpq.cpp similarity index 100% rename from src/tests/numerics/mpq.cpp rename to src/tests/util/numerics/mpq.cpp diff --git a/src/tests/sexpr/CMakeLists.txt b/src/tests/util/sexpr/CMakeLists.txt similarity index 100% rename from src/tests/sexpr/CMakeLists.txt rename to src/tests/util/sexpr/CMakeLists.txt diff --git a/src/tests/sexpr/sexpr.cpp b/src/tests/util/sexpr/sexpr.cpp similarity index 100% rename from src/tests/sexpr/sexpr.cpp rename to src/tests/util/sexpr/sexpr.cpp diff --git a/src/numerics/CMakeLists.txt b/src/util/numerics/CMakeLists.txt similarity index 100% rename from src/numerics/CMakeLists.txt rename to src/util/numerics/CMakeLists.txt diff --git a/src/numerics/gmp_init.cpp b/src/util/numerics/gmp_init.cpp similarity index 100% rename from src/numerics/gmp_init.cpp rename to src/util/numerics/gmp_init.cpp diff --git a/src/numerics/mpbq.cpp b/src/util/numerics/mpbq.cpp similarity index 100% rename from src/numerics/mpbq.cpp rename to src/util/numerics/mpbq.cpp diff --git a/src/numerics/mpbq.h b/src/util/numerics/mpbq.h similarity index 100% rename from src/numerics/mpbq.h rename to src/util/numerics/mpbq.h diff --git a/src/numerics/mpq.cpp b/src/util/numerics/mpq.cpp similarity index 100% rename from src/numerics/mpq.cpp rename to src/util/numerics/mpq.cpp diff --git a/src/numerics/mpq.h b/src/util/numerics/mpq.h similarity index 100% rename from src/numerics/mpq.h rename to src/util/numerics/mpq.h diff --git a/src/numerics/mpz.cpp b/src/util/numerics/mpz.cpp similarity index 100% rename from src/numerics/mpz.cpp rename to src/util/numerics/mpz.cpp diff --git a/src/numerics/mpz.h b/src/util/numerics/mpz.h similarity index 100% rename from src/numerics/mpz.h rename to src/util/numerics/mpz.h diff --git a/src/numerics/numeric_traits.cpp b/src/util/numerics/numeric_traits.cpp similarity index 100% rename from src/numerics/numeric_traits.cpp rename to src/util/numerics/numeric_traits.cpp diff --git a/src/numerics/numeric_traits.h b/src/util/numerics/numeric_traits.h similarity index 100% rename from src/numerics/numeric_traits.h rename to src/util/numerics/numeric_traits.h diff --git a/src/numerics/xnumeral.h b/src/util/numerics/xnumeral.h similarity index 100% rename from src/numerics/xnumeral.h rename to src/util/numerics/xnumeral.h diff --git a/src/sexpr/CMakeLists.txt b/src/util/sexpr/CMakeLists.txt similarity index 100% rename from src/sexpr/CMakeLists.txt rename to src/util/sexpr/CMakeLists.txt diff --git a/src/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp similarity index 100% rename from src/sexpr/sexpr.cpp rename to src/util/sexpr/sexpr.cpp diff --git a/src/sexpr/sexpr.h b/src/util/sexpr/sexpr.h similarity index 100% rename from src/sexpr/sexpr.h rename to src/util/sexpr/sexpr.h diff --git a/src/sexpr/sexpr_funcs.cpp b/src/util/sexpr/sexpr_funcs.cpp similarity index 100% rename from src/sexpr/sexpr_funcs.cpp rename to src/util/sexpr/sexpr_funcs.cpp diff --git a/src/sexpr/sexpr_funcs.h b/src/util/sexpr/sexpr_funcs.h similarity index 100% rename from src/sexpr/sexpr_funcs.h rename to src/util/sexpr/sexpr_funcs.h