diff --git a/src/bindings/lua/CMakeLists.txt b/src/bindings/lua/CMakeLists.txt index b3bdc6bdf..fdcdf5599 100644 --- a/src/bindings/lua/CMakeLists.txt +++ b/src/bindings/lua/CMakeLists.txt @@ -1,4 +1,5 @@ add_library(lua util.cpp lua_exception.cpp name.cpp numerics.cpp -options.cpp sexpr.cpp format.cpp level.cpp expr.cpp leanlua_state.cpp) +options.cpp sexpr.cpp format.cpp level.cpp expr.cpp context.cpp +leanlua_state.cpp) target_link_libraries(lua ${LEAN_LIBS}) diff --git a/src/bindings/lua/context.cpp b/src/bindings/lua/context.cpp new file mode 100644 index 000000000..d42191e15 --- /dev/null +++ b/src/bindings/lua/context.cpp @@ -0,0 +1,164 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include +#include "kernel/context.h" +#include "bindings/lua/util.h" +#include "bindings/lua/name.h" +#include "bindings/lua/expr.h" +#include "bindings/lua/context.h" + +namespace lean { +constexpr char const * context_entry_mt = "context_entry.mt"; + +bool is_context_entry(lua_State * L, int idx) { + return testudata(L, idx, context_entry_mt); +} + +context_entry & to_context_entry(lua_State * L, int idx) { + return *static_cast(luaL_checkudata(L, idx, context_entry_mt)); +} + +int push_context_entry(lua_State * L, context_entry const & e) { + void * mem = lua_newuserdata(L, sizeof(context_entry)); + new (mem) context_entry(e); + luaL_getmetatable(L, context_entry_mt); + lua_setmetatable(L, -2); + return 1; +} + +static int context_entry_gc(lua_State * L) { + to_context_entry(L, 1).~context_entry(); + return 0; +} + +static int mk_context_entry(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 2) + return push_context_entry(L, context_entry(to_name_ext(L, 1), to_expr(L, 2))); + else + return push_context_entry(L, context_entry(to_name_ext(L, 1), to_expr(L, 2), to_expr(L, 3))); +} + +static int context_entry_pred(lua_State * L) { + lua_pushboolean(L, is_context_entry(L, 1)); + return 1; +} + +static int context_entry_get_name(lua_State * L) { return push_name(L, to_context_entry(L, 1).get_name()); } +static int context_entry_get_domain(lua_State * L) { return push_expr(L, to_context_entry(L, 1).get_domain()); } +static int context_entry_get_body(lua_State * L) { return push_expr(L, to_context_entry(L, 1).get_body()); } + +static const struct luaL_Reg context_entry_m[] = { + {"__gc", context_entry_gc}, // never throws + {"get_name", safe_function}, + {"get_domain", safe_function}, + {"get_body", safe_function}, + {0, 0} +}; + +constexpr char const * context_mt = "context.mt"; + +bool is_context(lua_State * L, int idx) { + return testudata(L, idx, context_mt); +} + +context & to_context(lua_State * L, int idx) { + return *static_cast(luaL_checkudata(L, idx, context_mt)); +} + +int push_context(lua_State * L, context const & e) { + void * mem = lua_newuserdata(L, sizeof(context)); + new (mem) context(e); + luaL_getmetatable(L, context_mt); + lua_setmetatable(L, -2); + return 1; +} + +static int context_gc(lua_State * L) { + to_context(L, 1).~context(); + return 0; +} + +static int context_tostring(lua_State * L) { + std::ostringstream out; + // TODO(Leo): use pretty printer + out << to_context(L, 1); + lua_pushfstring(L, out.str().c_str()); + return 1; +} + +static int mk_context(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 0) { + return push_context(L, context()); + } else if (nargs == 2) { + context_entry & e = to_context_entry(L, 2); + return push_context(L, context(to_context(L, 1), e.get_name(), e.get_domain(), e.get_body())); + } else if (nargs == 3) { + return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_expr(L, 3))); + } else { + return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_expr(L, 3), to_expr(L, 4))); + } +} + +static int context_pred(lua_State * L) { + lua_pushboolean(L, is_context(L, 1)); + return 1; +} + +static int context_extend(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs != 3 && nargs != 4) + luaL_error(L, "extend expect 3 or 4 arguments"); + return mk_context(L); +} + +static int context_is_empty(lua_State * L) { + lua_pushboolean(L, empty(to_context(L, 1))); + return 1; +} + +static int context_lookup(lua_State * L) { + auto p = lookup_ext(to_context(L, 1), luaL_checkinteger(L, 2)); + push_context_entry(L, p.first); + push_context(L, p.second); + return 2; +} + +static int context_size(lua_State * L) { + lua_pushinteger(L, to_context(L, 1).size()); + return 1; +} + +static const struct luaL_Reg context_m[] = { + {"__gc", context_gc}, // never throws + {"__tostring", safe_function}, + {"__len", safe_function}, + {"is_empty", safe_function}, + {"size", safe_function}, + {0, 0} +}; + +void open_context(lua_State * L) { + luaL_newmetatable(L, context_entry_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, context_entry_m, 0); + set_global_function(L, "context_entry"); + set_global_function(L, "is_context_entry"); + + luaL_newmetatable(L, context_mt); + lua_pushvalue(L, -1); + lua_setfield(L, -2, "__index"); + setfuncs(L, context_m, 0); + set_global_function(L, "context"); + set_global_function(L, "is_context"); + set_global_function(L, "extend"); + set_global_function(L, "lookup"); +} +} diff --git a/src/bindings/lua/context.h b/src/bindings/lua/context.h new file mode 100644 index 000000000..8e48569a8 --- /dev/null +++ b/src/bindings/lua/context.h @@ -0,0 +1,21 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +namespace lean { +class context_entry; +bool is_context_entry(lua_State * L, int idx); +context_entry & to_context_entry(lua_State * L, int idx); +int push_context_entry(lua_State * L, context_entry const & o); + +class context; +bool is_context(lua_State * L, int idx); +context & to_context(lua_State * L, int idx); +int push_context(lua_State * L, context const & o); + +void open_context(lua_State * L); +} diff --git a/src/bindings/lua/expr.cpp b/src/bindings/lua/expr.cpp index 39e3b32ad..1d51af8a9 100644 --- a/src/bindings/lua/expr.cpp +++ b/src/bindings/lua/expr.cpp @@ -43,8 +43,13 @@ static int expr_gc(lua_State * L) { static int expr_tostring(lua_State * L) { std::ostringstream out; - // TODO(Leo): use pretty printer - out << to_expr(L, 1); + expr & e = to_expr(L, 1); + if (e) { + // TODO(Leo): use pretty printer + out << to_expr(L, 1); + } else { + out << ""; + } lua_pushfstring(L, out.str().c_str()); return 1; } @@ -166,12 +171,18 @@ static int expr_type(lua_State * L) { return push_expr(L, Type(to_level(L, 1))); } +static int expr_is_null(lua_State * L) { + lua_pushboolean(L, !to_expr(L, 1)); + return 1; +} + static const struct luaL_Reg expr_m[] = { {"__gc", expr_gc}, // never throws {"__tostring", safe_function}, {"__eq", safe_function}, {"__lt", safe_function}, {"__call", safe_function}, + {"is_null", safe_function}, {0, 0} }; diff --git a/src/bindings/lua/leanlua_state.cpp b/src/bindings/lua/leanlua_state.cpp index 5f0a659f3..8e3544439 100644 --- a/src/bindings/lua/leanlua_state.cpp +++ b/src/bindings/lua/leanlua_state.cpp @@ -20,6 +20,7 @@ Author: Leonardo de Moura #include "bindings/lua/format.h" #include "bindings/lua/level.h" #include "bindings/lua/expr.h" +#include "bindings/lua/context.h" #include "bindings/lua/lean.lua" extern "C" void * lua_realloc(void *, void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); } @@ -46,6 +47,7 @@ struct leanlua_state::imp { lean::open_format(m_state); lean::open_level(m_state); lean::open_expr(m_state); + lean::open_context(m_state); dostring(g_leanlua_extra); } diff --git a/src/bindings/lua/options.cpp b/src/bindings/lua/options.cpp index 64d8d8f3b..eb9111364 100644 --- a/src/bindings/lua/options.cpp +++ b/src/bindings/lua/options.cpp @@ -32,7 +32,7 @@ int push_options(lua_State * L, options const & o) { return 1; } -static int mk_option(lua_State * L) { +static int mk_options(lua_State * L) { // int nargs = lua_gettop(L); options r; return push_options(L, r); @@ -199,7 +199,7 @@ void open_options(lua_State * L) { lua_setfield(L, -2, "__index"); setfuncs(L, options_m, 0); - set_global_function(L, "options"); + set_global_function(L, "options"); set_global_function(L, "is_options"); } } diff --git a/tests/lua/context1.lua b/tests/lua/context1.lua new file mode 100644 index 000000000..bbdcf9b9b --- /dev/null +++ b/tests/lua/context1.lua @@ -0,0 +1,25 @@ +c = context() +assert(c:is_empty()) +print(c) +e = context_entry("x", Const("N")) +assert(e:get_name() == name("x")) +assert(e:get_domain() == Const("N")) +assert(e:get_body():is_null()) +print(e:get_body()) +c = context(c, e) +print(c) +assert(not c:is_empty()) +c = context(c, "y", Const("M")) +assert(#c == 2) +assert(c:size() == 2) +e, c1 = lookup(c, 0) +assert(c1:size() == 1) +assert(e:get_name() == name("y")) +c = context(c, "z", Const("N"), Const("a")) +print(c) +check_error(function() lookup(c, 10) end) +assert(lookup(c, 0):get_body() == Const("a")) +assert(not is_context_entry(c)) +assert(is_context(c)) +assert(is_context_entry(e)) +assert(not is_context_entry(c))