From e769c268007ab294f5e480648410b9374ccb72af Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 25 Apr 2014 18:30:40 -0700
Subject: [PATCH] refactor(kernel): move files that don't need to be in the
 kernel

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/CMakeLists.txt                | 2 +-
 src/library/CMakeLists.txt               | 3 ++-
 src/{kernel => library}/decl_macros.h    | 0
 src/{kernel => library}/io_state.cpp     | 2 +-
 src/{kernel => library}/io_state.h       | 0
 src/{kernel => library}/occurs.cpp       | 2 +-
 src/{kernel => library}/occurs.h         | 0
 src/tests/kernel/CMakeLists.txt          | 3 ---
 src/tests/library/CMakeLists.txt         | 3 +++
 src/tests/{kernel => library}/occurs.cpp | 2 +-
 10 files changed, 9 insertions(+), 8 deletions(-)
 rename src/{kernel => library}/decl_macros.h (100%)
 rename src/{kernel => library}/io_state.cpp (97%)
 rename src/{kernel => library}/io_state.h (100%)
 rename src/{kernel => library}/occurs.cpp (94%)
 rename src/{kernel => library}/occurs.h (100%)
 rename src/tests/{kernel => library}/occurs.cpp (95%)

diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index b4fd1897d..624758d67 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,5 +1,5 @@
 add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp
-for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp
+for_each_fn.cpp replace_fn.cpp free_vars.cpp abstract.cpp
 instantiate.cpp context.cpp formatter.cpp max_sharing.cpp
 definition.cpp replace_visitor.cpp environment.cpp
 justification.cpp pos_info_provider.cpp metavar.cpp
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index d14674a21..6cffde8b2 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,4 +1,5 @@
-add_library(library deep_copy.cpp expr_lt.cpp)
+add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp
+  occurs.cpp)
 # io_state_stream.cpp
 # kernel_bindings.cpp
 # context_to_lambda.cpp placeholder.cpp
diff --git a/src/kernel/decl_macros.h b/src/library/decl_macros.h
similarity index 100%
rename from src/kernel/decl_macros.h
rename to src/library/decl_macros.h
diff --git a/src/kernel/io_state.cpp b/src/library/io_state.cpp
similarity index 97%
rename from src/kernel/io_state.cpp
rename to src/library/io_state.cpp
index 375f192b8..5bf587e97 100644
--- a/src/kernel/io_state.cpp
+++ b/src/library/io_state.cpp
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "kernel/io_state.h"
 #include "kernel/kernel_exception.h"
+#include "library/io_state.h"
 
 namespace lean {
 io_state::io_state(formatter const & fmt):
diff --git a/src/kernel/io_state.h b/src/library/io_state.h
similarity index 100%
rename from src/kernel/io_state.h
rename to src/library/io_state.h
diff --git a/src/kernel/occurs.cpp b/src/library/occurs.cpp
similarity index 94%
rename from src/kernel/occurs.cpp
rename to src/library/occurs.cpp
index 280965043..2c7c64a2f 100644
--- a/src/kernel/occurs.cpp
+++ b/src/library/occurs.cpp
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "kernel/occurs.h"
 #include "kernel/find_fn.h"
+#include "library/occurs.h"
 
 namespace lean {
 bool occurs(expr const & n, expr const & m) {
diff --git a/src/kernel/occurs.h b/src/library/occurs.h
similarity index 100%
rename from src/kernel/occurs.h
rename to src/library/occurs.h
diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt
index cabd1bd7b..cda8bfb0c 100644
--- a/src/tests/kernel/CMakeLists.txt
+++ b/src/tests/kernel/CMakeLists.txt
@@ -28,9 +28,6 @@ add_test(replace ${CMAKE_CURRENT_BINARY_DIR}/replace)
 # target_link_libraries(environment ${EXTRA_LIBS})
 # add_test(environment ${CMAKE_CURRENT_BINARY_DIR}/environment)
 # set_tests_properties(environment PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell")
-add_executable(occurs occurs.cpp)
-target_link_libraries(occurs ${EXTRA_LIBS})
-add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs)
 add_executable(metavar metavar.cpp)
 target_link_libraries(metavar ${EXTRA_LIBS})
 add_test(metavar ${CMAKE_CURRENT_BINARY_DIR}/metavar)
diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt
index bdd1c60e7..51b9b168d 100644
--- a/src/tests/library/CMakeLists.txt
+++ b/src/tests/library/CMakeLists.txt
@@ -7,6 +7,9 @@ add_test(expr_lt ${CMAKE_CURRENT_BINARY_DIR}/expr_lt)
 add_executable(deep_copy deep_copy.cpp)
 target_link_libraries(deep_copy ${EXTRA_LIBS})
 add_test(deep_copy ${CMAKE_CURRENT_BINARY_DIR}/deep_copy)
+add_executable(occurs occurs.cpp)
+target_link_libraries(occurs ${EXTRA_LIBS})
+add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs)
 # add_executable(arith_tst arith.cpp)
 # target_link_libraries(arith_tst ${EXTRA_LIBS})
 # add_test(arith_tst ${CMAKE_CURRENT_BINARY_DIR}/arith_tst)
diff --git a/src/tests/kernel/occurs.cpp b/src/tests/library/occurs.cpp
similarity index 95%
rename from src/tests/kernel/occurs.cpp
rename to src/tests/library/occurs.cpp
index a6927f8e1..d78d3f897 100644
--- a/src/tests/kernel/occurs.cpp
+++ b/src/tests/library/occurs.cpp
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/test.h"
-#include "kernel/occurs.h"
 #include "kernel/abstract.h"
+#include "library/occurs.h"
 using namespace lean;
 
 static void tst1() {