refactor(kernel): move max_sharing to library

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

src/kernel/CMakeLists.txt

@@ -1,8 +1,7 @@
-add_library(kernel level.cpp expr.cpp expr_eq_fn.cpp
+add_library(kernel level.cpp expr.cpp expr_eq_fn.cpp for_each_fn.cpp
-for_each_fn.cpp replace_fn.cpp free_vars.cpp abstract.cpp
+replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp context.cpp
-instantiate.cpp context.cpp formatter.cpp max_sharing.cpp
+formatter.cpp definition.cpp replace_visitor.cpp environment.cpp
-definition.cpp replace_visitor.cpp environment.cpp justification.cpp
+justification.cpp pos_info_provider.cpp metavar.cpp converter.cpp
-pos_info_provider.cpp metavar.cpp converter.cpp constraint.cpp
+constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp )
-type_checker.cpp error_msgs.cpp kernel_exception.cpp )
 
 target_link_libraries(kernel ${LEAN_LIBS})

src/kernel/expr.cpp

@@ -17,7 +17,6 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 #include "kernel/expr_eq_fn.h"
 #include "kernel/free_vars.h"
-#include "kernel/max_sharing.h"
 
 namespace lean {
 static expr g_dummy(mk_var(0));

src/library/CMakeLists.txt

@@ -1,6 +1,6 @@
 add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   kernel_bindings.cpp io_state_stream.cpp bin_app.cpp
-  resolve_macro.cpp kernel_serializer.cpp)
+  resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp)
 # placeholder.cpp fo_unify.cpp hop_match.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/kernel_serializer.cpp

@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "util/object_serializer.h"
 #include "kernel/expr.h"
 #include "kernel/definition.h"
-#include "kernel/max_sharing.h"
+#include "library/max_sharing.h"
 #include "library/kernel_serializer.h"
 
 // Procedures for serializing and deserializing kernel objects (levels, exprs, definitions)

src/library/max_sharing.cpp

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include <functional>
 #include "util/buffer.h"
 #include "util/interrupt.h"
-#include "kernel/max_sharing.h"
+#include "library/max_sharing.h"
 
 namespace lean {
 /**

src/tests/kernel/expr.cpp

@@ -14,7 +14,7 @@ Author: Leonardo de Moura
 #include "kernel/free_vars.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
-#include "kernel/max_sharing.h"
+#include "library/max_sharing.h"
 #include "library/kernel_serializer.h"
 using namespace lean;
 

src/tests/kernel/max_sharing.cpp

@@ -6,8 +6,8 @@ Author: Leonardo de Moura
 */
 #include <iostream>
 #include "util/test.h"
+#include "library/max_sharing.h"
 #include "kernel/abstract.h"
-#include "kernel/max_sharing.h"
 using namespace lean;
 
 static void tst1() {