feat(lua): expose local_context objects in the Lua bindings

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

src/bindings/lua/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_library(lua util.cpp lua_exception.cpp name.cpp numerics.cpp
-options.cpp sexpr.cpp format.cpp level.cpp expr.cpp context.cpp
-leanlua_state.cpp)
+options.cpp sexpr.cpp format.cpp level.cpp local_context.cpp expr.cpp
+context.cpp leanlua_state.cpp)
 
 target_link_libraries(lua ${LEAN_LIBS})

src/bindings/lua/leanlua_state.cpp

@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "bindings/lua/sexpr.h"
 #include "bindings/lua/format.h"
 #include "bindings/lua/level.h"
+#include "bindings/lua/local_context.h"
 #include "bindings/lua/expr.h"
 #include "bindings/lua/context.h"
 #include "bindings/lua/lean.lua"
@@ -46,6 +47,7 @@ struct leanlua_state::imp {
         lean::open_sexpr(m_state);
         lean::open_format(m_state);
         lean::open_level(m_state);
+        lean::open_local_context(m_state);
         lean::open_expr(m_state);
         lean::open_context(m_state);
         dostring(g_leanlua_extra);

tests/lua/localctx1.lua

@@ -0,0 +1,24 @@
+l = local_context()
+assert(l:is_nil())
+assert(is_local_context(l))
+e = mk_inst(1, Const("a"))
+assert(is_local_entry(e))
+assert(e:is_inst())
+assert(not e:is_lift())
+assert(e:s() == 1)
+assert(e:v() == Const("a"))
+assert(e:v() ~= Const("b"))
+assert(not e:is_lift())
+e2 = mk_lift(0, 2);
+assert(is_local_entry(e2))
+assert(not e2:is_inst())
+assert(e2:is_lift())
+assert(e2:s() == 0)
+assert(e2:n() == 2)
+l = local_context(e, l)
+l2 = local_context(e2, l)
+assert(l2:head() == e2)
+assert(l2:tail():head() == e)
+assert(not l2:is_nil())
+assert(is_local_context(l2))
+assert(not is_local_entry(l2))