operator bool() may produce unwanted conversions.
For example, we had the following bug in the code base.
...
object const & obj = find_object(const_name(n));
if (obj && obj.is_builtin() && obj.get_name() == n)
...
obj.get_name() has type lean::name
n has type lean::expr
Both have 'operator bool()', then the compiler uses the operator to
convert them to Boolean, and then compare the result.
Of course, this is not our intention.
After this commit, the compiler correctly signs the error.
The correct code is
...
object const & obj = find_object(const_name(n));
if (obj && obj.is_builtin() && obj.get_name() == const_name(n))
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Recursive functions that may go very deep should invoke the function check_stack. It throws an exception if the amount of stack space is limited.
The function check_system() is syntax sugar for
check_interrupted();
check_stack();
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Proof/Cex builders and tactics implemented in Lua had a "strong reference" to script_state. If they are stored in the Lua state, then we get a cyclic reference.
That is, script_state points to these objects, and they point back to script_state.
To avoid this memory leak, this commit defines a weak reference for script_state objects. The Proof/Cex builders and tactics now store a weak reference to the Lua state.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This is very important when several Lua tactics are implemented in the
same Lua State object. In this case, even if we use the par
combinator, a Lua tactic will block the other Lua tactics running in
the same Lua State object.
With this commit, a Lua tactic can use yield to allow other tactics
in the same State object to execute.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
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>
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>
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>
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>
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>
