From 06d2ff021b2125065745515b58b8cbb97f28eb04 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Jun 2014 16:23:24 -0700 Subject: [PATCH] feat(util/thread_script_state): add system_import procedure Signed-off-by: Leonardo de Moura --- src/tests/util/CMakeLists.txt | 12 +++++++++--- src/tests/util/import_test.lua | 4 ++++ src/tests/util/thread.cpp | 4 +++- src/util/thread_script_state.cpp | 30 ++++++++++++++++++++++++++---- src/util/thread_script_state.h | 9 ++++++++- 5 files changed, 50 insertions(+), 9 deletions(-) create mode 100644 src/tests/util/import_test.lua diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt index 6d95ea2b8..d801dce92 100644 --- a/src/tests/util/CMakeLists.txt +++ b/src/tests/util/CMakeLists.txt @@ -22,9 +22,6 @@ add_test(options ${CMAKE_CURRENT_BINARY_DIR}/options) add_executable(scoped_map scoped_map.cpp) target_link_libraries(scoped_map ${EXTRA_LIBS}) add_test(scoped_map ${CMAKE_CURRENT_BINARY_DIR}/scoped_map) -add_executable(thread thread.cpp) -target_link_libraries(thread ${EXTRA_LIBS}) -add_test(thread ${CMAKE_CURRENT_BINARY_DIR}/thread) add_executable(memory memory.cpp) target_link_libraries(memory ${EXTRA_LIBS}) add_test(memory ${CMAKE_CURRENT_BINARY_DIR}/memory) @@ -76,3 +73,12 @@ add_test(trie ${CMAKE_CURRENT_BINARY_DIR}/trie) add_executable(lru_cache lru_cache.cpp) target_link_libraries(lru_cache ${EXTRA_LIBS}) add_test(lru_cache ${CMAKE_CURRENT_BINARY_DIR}/lru_cache) +# thread.cpp used import_test.lua +add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/import_test.lua + COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_SOURCE_DIR}/import_test.lua ${CMAKE_CURRENT_BINARY_DIR}/import_test.lua + DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/import_test.lua) +add_custom_target("import_test" DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/import_test.lua) +add_executable(thread thread.cpp) +target_link_libraries(thread ${EXTRA_LIBS}) +add_test(thread ${CMAKE_CURRENT_BINARY_DIR}/thread) +add_dependencies(thread import_test) \ No newline at end of file diff --git a/src/tests/util/import_test.lua b/src/tests/util/import_test.lua new file mode 100644 index 000000000..9c9656d5e --- /dev/null +++ b/src/tests/util/import_test.lua @@ -0,0 +1,4 @@ +print("importing test...") +function fact(x) + if x == 0 then return 1 else return x * fact(x-1) end +end diff --git a/src/tests/util/thread.cpp b/src/tests/util/thread.cpp index e8b39298c..959a4015a 100644 --- a/src/tests/util/thread.cpp +++ b/src/tests/util/thread.cpp @@ -175,6 +175,7 @@ static void tst6() { static void tst7() { std::cout << "start\n"; + system_import("import_test.lua"); system_dostring("print('hello'); x = 10;"); interruptible_thread t1([]() { script_state S = get_thread_script_state(); @@ -204,7 +205,8 @@ static void tst8() { "for i = 1, 10000 do\n" " x = x + 1\n" "end\n" - "print(x)\n"); + "print(x)\n" + "print(fact(10))\n"); }); t1.join(); } diff --git a/src/util/thread_script_state.cpp b/src/util/thread_script_state.cpp index e50ed4311..3bf1a134a 100644 --- a/src/util/thread_script_state.cpp +++ b/src/util/thread_script_state.cpp @@ -5,13 +5,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include #include #include "util/thread.h" +#include "util/pair.h" #include "util/script_state.h" namespace lean { static mutex g_code_mutex; -static std::vector g_code; +static std::vector> g_code; static mutex g_state_mutex; static std::vector g_states; static std::vector g_available_states; @@ -28,7 +30,23 @@ void system_dostring(char const * code) { { // Save code for future states lock_guard lk(g_code_mutex); - g_code.push_back(code); + g_code.push_back(mk_pair(true, code)); + } +} + +/** \brief Import \c fname in all states in the pool */ +void system_import(char const * fname) { + { + // Import file in all existing states + lock_guard lk(g_state_mutex); + for (auto & s : g_states) { + s.import(fname); + } + } + { + // Save module for future states + lock_guard lk(g_code_mutex); + g_code.push_back(mk_pair(false, fname)); } } @@ -47,8 +65,12 @@ static script_state get_state() { // Execute existing code in new state lock_guard lk(g_code_mutex); script_state r; - for (auto & c : g_code) - r.dostring(c.c_str()); + for (auto const & p : g_code) { + if (p.first) + r.dostring(p.second.c_str()); + else + r.import(p.second.c_str()); + } g_states.push_back(r); { // save new state in vector of all states diff --git a/src/util/thread_script_state.h b/src/util/thread_script_state.h index f1776e929..df735e7ca 100644 --- a/src/util/thread_script_state.h +++ b/src/util/thread_script_state.h @@ -10,12 +10,19 @@ namespace lean { /** \brief Execute the given piece of code in all global/system script_state objects. - \remark The code fragments are saved. If a new thread needs to create a new + \remark The code fragments are saved. If a thread needs to create a new script_state object, all code blocks are executed. \remark System code should be installed when Lean is started. */ void system_dostring(char const * code); +/** + \brief Import the given module in all global/system script_state objects. + + \remark The module name is saved. If a thread needs to create a new + script_state object, all modules are imported. +*/ +void system_import(char const * fname); /** \brief Retrieve a script_state object for the current thread. The thread has exclusive access until the thread is destroyed,