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>
rewrite_* functions take the rewriting results of the sub-components and
construct the rewriting result for the main component.
For instance, rewrite_app function takes env, ctx, and the value v s.t.
v = (e_0 e_1 ... e_n)
and the rewriting results for e_i's as a vector(buffer)
(e'_0, pf_0 -- proof of e_0 = e'_0)
(e'_1, pf_1 -- proof of e_1 = e'_1)
...
(e'_n, pf_n -- proof of e_n = e'_n).
Then rewrite_app function construct the new v'
v' = (e'_0 e'_1 ... e'_n)
and the proof of v = v' which is constructed with pf_i's.
These functions are used in the component rewriters such as app_RW and
let_type_RW, as well as more complicated rewriters such as depth
rewriter.
For example, after this commit, we can write
simple_tac = REPEAT(ORELSE(imp_tactic, conj_tactic)) .. assumption_tactic
instead of
simple_tac = REPEAT(ORELSE(imp_tactic(), conj_tactic())) .. assumption_tactic()
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P.
For example, consider the constraint
[a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b))
Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet.
So, the elaborator would continue to process the constraint, and convert it into:
[a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true
Now, ?M::1 is assigned to the term
if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true
This is bad, since the original structure was lost.
This commit also contains an example that only works after the commit is applied.
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 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>
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>
Now, it produces the following outcomes:
1- A proof
2- A counterexample
3- A list of (unsolved) final states
Remark: the solve method does not check whether the proof or counterexample is correct.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
