From 3ee59aa17f6322df8d2e928244ec4f4113e0276e Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 6 Sep 2019 13:52:15 +0200
Subject: [PATCH] feat(library/compiler/ir_interpreter): add Windows support

---
 bin/leanc.in                            |  4 ++--
 src/CMakeLists.txt                      |  8 +++++++-
 src/library/compiler/ir_interpreter.cpp | 16 ++++++++++++++--
 3 files changed, 23 insertions(+), 5 deletions(-)

diff --git a/bin/leanc.in b/bin/leanc.in
index af505f0b33..9bed536465 100644
--- a/bin/leanc.in
+++ b/bin/leanc.in
@@ -31,7 +31,7 @@ if [[ $use_c == yes ]]; then
     [ -f $LEAN_CC ] || command -v $LEAN_CC || error "no suitable C compiler found!"
 
     # NOTE: leanstatic and leanstdlib are cyclically dependent
-    $LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp -ldl @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
+    $LEAN_CC -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
 else
     # Check C++ compiler
     for cxx in $LEAN_CXX @CMAKE_CXX_COMPILER@ /usr/bin/g++; do
@@ -42,5 +42,5 @@ else
     [ -f $LEAN_CXX ] || command -v $LEAN_CXX || error "no suitable C++ compiler found!"
 
     # NOTE: leanstatic and leanstdlib are cyclically dependent
-    $LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp -ldl @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
+    $LEAN_CXX -std=c++14 -D LEAN_MULTI_THREAD "-I$bindir/../src" "-I$bindir/../include" "$@" "-L$bindir" "-L$bindir/../lib" -lleanstatic -lleanstdlib -lleanstatic -lleanstdlib -lgmp @LEANC_EXTRA_FLAGS@ -Wno-unused-command-line-argument
 fi
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index fadc23bc5f..4ffa4527cb 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -432,7 +432,13 @@ find_package(PythonInterp)
 include_directories(${LEAN_SOURCE_DIR})
 
 # export all symbols for the interpreter
-set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS} -rdynamic")
+if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
+  set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS} -Wl,--export-all")
+else()
+  set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS} -rdynamic")
+  set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -ldl")
+endif()
+
 if(MULTI_THREAD AND NOT MSVC AND (NOT ("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")))
     set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread")
 endif()
diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp
index 771bd87d10..5a87547028 100644
--- a/src/library/compiler/ir_interpreter.cpp
+++ b/src/library/compiler/ir_interpreter.cpp
@@ -27,7 +27,11 @@ below.
 */
 #include <string>
 #include <vector>
+#ifdef LEAN_WINDOWS
+#include <windows.h>
+#else
 #include <dlfcn.h>
+#endif
 #include "runtime/flet.h"
 #include "runtime/apply.h"
 #include "library/trace.h"
@@ -190,6 +194,14 @@ void print_object(io_state_stream const & ios, object * o) {
     }
 }
 
+void * lookup_symbol_in_cur_exe(char const * sym) {
+#ifdef LEAN_WINDOWS
+    return reinterpret_cast<void *>(GetProcAddress(GetModuleHandle(nullptr), sym));
+#else
+    return dlsym(RTLD_DEFAULT, sym);
+#endif
+}
+
 class interpreter {
     // stack of IR variable slots
     std::vector<object *> m_arg_stack;
@@ -573,9 +585,9 @@ class interpreter {
             string_ref boxed_mangled(string_append(mangled.to_obj_arg(), g_boxed_mangled_suffix->raw()));
             symbol_cache_entry e_new;
             // check for boxed version first
-            if (void *p_boxed = dlsym(RTLD_DEFAULT, boxed_mangled.data())) {
+            if (void *p_boxed = lookup_symbol_in_cur_exe(boxed_mangled.data())) {
                 e_new = symbol_cache_entry { p_boxed, true };
-            } else if (void *p = dlsym(RTLD_DEFAULT, mangled.data())) {
+            } else if (void *p = lookup_symbol_in_cur_exe(mangled.data())) {
                 // if there is no boxed version, there are no unboxed parameters, so use default version
                 e_new = symbol_cache_entry { p, false };
             } else {