feat(library/inductive_compiler): scaffold for inductive compiler

src/CMakeLists.txt

@@ -341,6 +341,8 @@ add_subdirectory(library/constructions)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:constructions>)
 add_subdirectory(library/equations_compiler)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:equations_compiler>)
+add_subdirectory(library/inductive_compiler)
+set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:inductive_compiler>)
 # add_subdirectory(library/blast)
 # set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:blast>)
 # add_subdirectory(library/blast/backward)

src/init/init.cpp

@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "library/tactic/init_module.h"
 #include "library/constructions/init_module.h"
 #include "library/equations_compiler/init_module.h"
+#include "library/inductive_compiler/init_module.h"
 #include "library/print.h"
 #include "library/vm/init_module.h"
 #include "library/compiler/init_module.h"
@@ -42,6 +43,7 @@ void initialize() {
     initialize_tactic_module();
     initialize_constructions_module();
     initialize_equations_compiler_module();
+    initialize_inductive_compiler_module();
     initialize_frontend_lean_module();
     initialize_frontend_smt2_module();
     initialize_vm_module();
@@ -51,6 +53,7 @@ void finalize() {
     finalize_vm_module();
     finalize_frontend_smt2_module();
     finalize_frontend_lean_module();
+    finalize_inductive_compiler_module();
     finalize_equations_compiler_module();
     finalize_constructions_module();
     finalize_tactic_module();

src/library/inductive_compiler/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_library(inductive_compiler OBJECT
+  init_module.cpp
+  )

src/library/inductive_compiler/init_module.cpp

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Daniel Selsam
+*/
+namespace lean {
+
+void initialize_inductive_compiler_module() {}
+void finalize_inductive_compiler_module() {}
+
+}

src/library/inductive_compiler/init_module.h

@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Daniel Selsam
+*/
+#pragma once
+namespace lean {
+void initialize_inductive_compiler_module();
+void finalize_inductive_compiler_module();
+}