diff --git a/src/bindings/lua/CMakeLists.txt b/src/bindings/lua/CMakeLists.txt index fdcdf5599..6f9bf667a 100644 --- a/src/bindings/lua/CMakeLists.txt +++ b/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}) diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp index 8e3544439..c8dc9ee99 100644 --- a/src/bindings/lua/leanlua_state.cpp +++ b/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); diff --git a/tests/lua/localctx1.lua b/tests/lua/localctx1.lua new file mode 100644 index 000000000..6a52c5366 --- /dev/null +++ b/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))