feat(util/interrupt): restore interrupt module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(*): simplify interrupt propagation

Instead of having m_interrupted flags in several components. We use a thread_local global variable.
The new approach is much simpler to get right since there is no risk of "forgetting" to propagate
the set_interrupt method to sub-components.

The plan is to support set_interrupt methods and m_interrupted flags only in tactic objects.
We need to support them in tactics and tacticals because we want to implement combinators/tacticals such as (try_for T M) that fails if tactic T does not finish in M ms.
For example, consider the tactic:

    try-for (T1 ORELSE T2) 5

It tries the tactic (T1 ORELSE T2) for 5ms.
Thus, if T1 does not finish after 5ms an interrupt request is sent, and T1 is interrupted.
Now, if you do not have a m_interrupted flag marking each tactic, the ORELSE combinator will try T2.
The set_interrupt method for ORELSE tactical should turn on the m_interrupted flag.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(lua): cleanup Lua bindings, and add accessor/tester to expr Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
style(util/sexpr): name convetion for enumeration types

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(lua): add fields method to sexpr Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(lua): replace lua_pushfstring with lua_pushstring

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(lua): rename env() to get_env()

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(lua): make objects() and localobjects() methods return iterators in the environment LUA API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(lua): expr LUA API test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(frontends/lean): example mixing Lean and Lua

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): return the operator associated with constant expressions that are names of builtin values

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(lua): add for_each to expr Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(lua): add abstract, instantiate, has_free_vars, lift/lower free_vars to Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/occurs): typos

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(lua): add occurs method to expr Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(lua): luajit incompatibility

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(build): include dl.so when compiling on Linux

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(lua): object Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(lua): copy_values and add tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>