Move auxiliary files away from kernel

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

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

src/kernel/CMakeLists.txt

@@ -1,5 +1,6 @@
-add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp abstract.cpp
+add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
-  instantiate.cpp deep_copy.cpp normalize.cpp level.cpp environment.cpp
+  normalize.cpp context.cpp level.cpp object.cpp environment.cpp
-  type_check.cpp context.cpp builtin.cpp basic_thms.cpp toplevel.cpp
+  type_check.cpp builtin.cpp expr_formatter.cpp expr_locator.cpp
-  object.cpp expr_formatter.cpp expr_locator.cpp occurs.cpp pp.cpp)
+  occurs.cpp pp.cpp)
+
 target_link_libraries(kernel ${LEAN_LIBS})