feat(bindings/lua): expose io_state object in the Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(bindings/lua): move Lua bindings to the file associated with them

The directory bindings/lua was getting too big and had too many dependencies.
Moreover, it was getting too painful to edit/maintain two different places.
Now, the bindings for module X are in the directory that defines X.
For example, the bindings for util/name.cpp are located at util/name.cpp.

The only exception is the kernel. We do not want to inflate the kernel
with Lua bindings. The bindings for the kernel classes are located
at bindings/kernel_bindings.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(bindings/lua/leanlua_state): cleanup

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(bindings/lua): move to frontends/lua

Lua API is an integral part of Lean. It does *not* have the same status
of external APIs (e.g., Python) we will add in the future.

We will reserve the directory bindings for external APIs for using Lean
as a library.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(util/lua): remove dead code

I removed lua_module helper class because it does not work.
The problem is that the linker may eliminate ignore a object file that contains a lua_module global object used for initialization. When this happens, the associated Lua bindings will not be exposed in the Lua API.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lua/leanlua_state): minimize the use of 'friend' directive

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lua): add lua_migrate_fn, and make copy_values modular

copy_values is not a big if-then-else anymore.
Before this change, whenever we added a new kind of userdata, we would have to update copy_values.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(util/lua): propagate C++ Lean exceptions in Lua

The following call sequence is possible:
C++ -> Lua -> C++ -> Lua -> C++

The first block of C++ is the Lean main function.
The main function invokes the Lua interpreter.
The Lua interpreter invokes a C++ Lean API.
Then the Lean API invokes a callback implemented in Lua.
The Lua callback invokes another Lean API.
Now, suppose the Lean API throws an exception.
We want the C++ exception to propagate over the mixed C++/Lua call stack.
We use the clone/rethrow exception idiom to achieve this goal.

Before this commit, the C++ exceptions were converted into strings
using the method what(), and then they were propagated over the Lua
stack using lua_error. A lua_error was then converted into a lua_exception when going back to C++.
This solution was very unsatisfactory, since all C++ exceptions were being converted into a lua_exception, and consequently the structure of the exception was being lost.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lua/leanlua_thread): propagate C++ thread over Lua thread boundaries

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lua): remove unnecessary function reference

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(kernel/expr): fix cpplint warning

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lua): make sure Lua 'sleep' function support interruption

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lua): rename leanlua_state to script_state, and move it to util

This commit also minimizes the dependencies of script_state.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(tests/lua/threads): break lua thread tests into individual tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(util/script_state): remove unsafe unguarded_apply

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(util/script_state): replace std::recursive_mutex with std::mutex, and use unlock_guard

The unlock_guard and exec_unprotected will be useful also for implementing the Lua tactic API.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/optional): typo

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): expose tactics in the Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/tactic): use unprotect/protect idiom for callbacks in the tactic API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/rewriter): add skeleton for depth rewriter