From 4d3ed6ca43e9f9dae8d671077fb45bf6de33b7de Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 17 Aug 2015 14:10:26 -0700
Subject: [PATCH] feat(init/init): automatically initialize lean shared library

---
 src/CMakeLists.txt          |  2 +-
 src/shared/init.cpp         | 11 +++++++++++
 src/tests/shared/shared.cpp | 36 ++++++++++++++++++++++++++++++++++--
 3 files changed, 46 insertions(+), 3 deletions(-)
 create mode 100644 src/shared/init.cpp

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 5a09a310c..43a8a31e6 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -363,7 +363,7 @@ add_library(leanstatic ${LEAN_OBJS})
 if (${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -Wl,--export-all")
 endif()
-add_library(leanshared SHARED ${LEAN_OBJS})
+add_library(leanshared SHARED shared/init.cpp ${LEAN_OBJS})
 target_link_libraries(leanshared ${EXTRA_LIBS})
 
 add_subdirectory(shell)
diff --git a/src/shared/init.cpp b/src/shared/init.cpp
new file mode 100644
index 000000000..95c7f227c
--- /dev/null
+++ b/src/shared/init.cpp
@@ -0,0 +1,11 @@
+/*
+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 "init/init.h"
+namespace lean {
+// automatic initialization for the shared library
+initializer g_init;
+}
diff --git a/src/tests/shared/shared.cpp b/src/tests/shared/shared.cpp
index a1704741c..c301106a1 100644
--- a/src/tests/shared/shared.cpp
+++ b/src/tests/shared/shared.cpp
@@ -5,11 +5,43 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/environment.h"
+#include "kernel/type_checker.h"
+#include "kernel/abstract.h"
 #include "init/init.h"
+using namespace lean;
+
+static environment add_decl(environment const & env, declaration const & d) {
+    auto cd = check(env, d);
+    return env.add(cd);
+}
 
 int main() {
-    lean::initializer init;
-    lean::environment env;
+    environment env;
     std::cout << "Lean (empty) environment was successfully created\n";
+    name base("base");
+    expr Prop = mk_Prop();
+    env = add_decl(env, mk_constant_assumption(name(base, 0u), level_param_names(), Prop >> (Prop >> Prop)));
+    expr x = Local("x", Prop);
+    expr y = Local("y", Prop);
+    for (unsigned i = 1; i <= 100; i++) {
+        expr prev = Const(name(base, i-1));
+        env = add_decl(env, mk_definition(env, name(base, i), level_param_names(), Prop >> (Prop >> Prop),
+                                          Fun({x, y}, mk_app(prev, mk_app(prev, x, y), mk_app(prev, y, x)))));
+    }
+    expr Type = mk_Type();
+    expr A = Local("A", Type);
+    expr a = Local("a", A);
+    env = add_decl(env, mk_definition("id", level_param_names(),
+                                      Pi(A, A >> A),
+                                      Fun({A, a}, a)));
+    type_checker checker(env, name_generator("tmp"));
+    expr f96 = Const(name(base, 96));
+    expr f97 = Const(name(base, 97));
+    expr f98 = Const(name(base, 98));
+    expr f3  = Const(name(base, 3));
+    expr c1  =  mk_local("c1", Prop);
+    expr c2  = mk_local("c2", Prop);
+    expr id = Const("id");
+    std::cout << checker.whnf(mk_app(f3, c1, c2)).first << "\n";
     return 0;
 }