refactor(library,library/blast): move context to blast

src/CMakeLists.txt

@@ -353,6 +353,8 @@ add_subdirectory(library/tactic)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:tactic>)
 add_subdirectory(library/definitional)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:definitional>)
+add_subdirectory(library/blast)
+set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:blast>)
 add_subdirectory(library/error_handling)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:error_handling>)
 add_subdirectory(compiler)

src/library/CMakeLists.txt

@@ -15,4 +15,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   unfold_macros.cpp app_builder.cpp projection.cpp abbreviation.cpp
   relation_manager.cpp export.cpp user_recursors.cpp
   class_instance_synth.cpp idx_metavar.cpp composition_manager.cpp
-  tc_multigraph.cpp noncomputable.cpp aux_recursors.cpp context.cpp)
+  tc_multigraph.cpp noncomputable.cpp aux_recursors.cpp)

src/library/blast/CMakeLists.txt

@@ -0,0 +1 @@
+add_library(blast OBJECT state.cpp context.cpp)

src/library/blast/context.cpp

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "library/context.h"
 #include "library/kernel_serializer.h"
+#include "library/blast/context.h"
 
 namespace lean {
 LEAN_THREAD_PTR(context, g_context);

src/library/blast/state.cpp

@@ -0,0 +1,7 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/blast/state.h"

src/library/blast/state.h

@@ -0,0 +1,15 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/expr.h"
+
+namespace lean {
+namespace blast {
+class state {
+
+};
+}}