From d6d221b992cf89b60260cdc75d28ccde36f08745 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 15 Aug 2013 10:04:24 -0700
Subject: [PATCH] Move auxiliary files away from kernel

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/CMakeLists.txt                      | 3 +++
 src/{kernel => exprlib}/basic_thms.cpp  | 0
 src/{kernel => exprlib}/basic_thms.h    | 0
 src/{kernel => exprlib}/deep_copy.cpp   | 0
 src/{kernel => exprlib}/deep_copy.h     | 0
 src/{kernel => exprlib}/max_sharing.cpp | 0
 src/{kernel => exprlib}/max_sharing.h   | 0
 src/{kernel => exprlib}/toplevel.cpp    | 0
 src/{kernel => exprlib}/toplevel.h      | 0
 src/kernel/CMakeLists.txt               | 9 +++++----
 10 files changed, 8 insertions(+), 4 deletions(-)
 rename src/{kernel => exprlib}/basic_thms.cpp (100%)
 rename src/{kernel => exprlib}/basic_thms.h (100%)
 rename src/{kernel => exprlib}/deep_copy.cpp (100%)
 rename src/{kernel => exprlib}/deep_copy.h (100%)
 rename src/{kernel => exprlib}/max_sharing.cpp (100%)
 rename src/{kernel => exprlib}/max_sharing.h (100%)
 rename src/{kernel => exprlib}/toplevel.cpp (100%)
 rename src/{kernel => exprlib}/toplevel.h (100%)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 662f2084c..1aec78508 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -65,6 +65,7 @@ include_directories(${LEAN_SOURCE_DIR}/util/sexpr)
 include_directories(${LEAN_SOURCE_DIR}/interval)
 include_directories(${LEAN_SOURCE_DIR}/kernel)
 include_directories(${LEAN_SOURCE_DIR}/kernel/arith)
+include_directories(${LEAN_SOURCE_DIR}/exprlib)
 include_directories(${LEAN_SOURCE_DIR}/parsers)
 include_directories(${LEAN_SOURCE_DIR}/frontend)
 
@@ -80,6 +81,8 @@ add_subdirectory(kernel)
 set(LEAN_LIBS ${LEAN_LIBS} kernel)
 add_subdirectory(kernel/arith)
 set(LEAN_LIBS ${LEAN_LIBS} kernel_arith)
+add_subdirectory(exprlib)
+set(LEAN_LIBS ${LEAN_LIBS} exprlib)
 add_subdirectory(frontend)
 set(LEAN_LIBS ${LEAN_LIBS} frontend)
 set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}")
diff --git a/src/kernel/basic_thms.cpp b/src/exprlib/basic_thms.cpp
similarity index 100%
rename from src/kernel/basic_thms.cpp
rename to src/exprlib/basic_thms.cpp
diff --git a/src/kernel/basic_thms.h b/src/exprlib/basic_thms.h
similarity index 100%
rename from src/kernel/basic_thms.h
rename to src/exprlib/basic_thms.h
diff --git a/src/kernel/deep_copy.cpp b/src/exprlib/deep_copy.cpp
similarity index 100%
rename from src/kernel/deep_copy.cpp
rename to src/exprlib/deep_copy.cpp
diff --git a/src/kernel/deep_copy.h b/src/exprlib/deep_copy.h
similarity index 100%
rename from src/kernel/deep_copy.h
rename to src/exprlib/deep_copy.h
diff --git a/src/kernel/max_sharing.cpp b/src/exprlib/max_sharing.cpp
similarity index 100%
rename from src/kernel/max_sharing.cpp
rename to src/exprlib/max_sharing.cpp
diff --git a/src/kernel/max_sharing.h b/src/exprlib/max_sharing.h
similarity index 100%
rename from src/kernel/max_sharing.h
rename to src/exprlib/max_sharing.h
diff --git a/src/kernel/toplevel.cpp b/src/exprlib/toplevel.cpp
similarity index 100%
rename from src/kernel/toplevel.cpp
rename to src/exprlib/toplevel.cpp
diff --git a/src/kernel/toplevel.h b/src/exprlib/toplevel.h
similarity index 100%
rename from src/kernel/toplevel.h
rename to src/exprlib/toplevel.h
diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index a05d99d5f..98582fd6f 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,5 +1,6 @@
-add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp abstract.cpp
-  instantiate.cpp deep_copy.cpp normalize.cpp level.cpp environment.cpp
-  type_check.cpp context.cpp builtin.cpp basic_thms.cpp toplevel.cpp
-  object.cpp expr_formatter.cpp expr_locator.cpp occurs.cpp pp.cpp)
+add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
+  normalize.cpp context.cpp level.cpp object.cpp environment.cpp
+  type_check.cpp builtin.cpp expr_formatter.cpp expr_locator.cpp
+  occurs.cpp pp.cpp)
+
 target_link_libraries(kernel ${LEAN_LIBS})