michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(lua): cleanup Lua API, improve performance

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-11-14 17:19:51 -08:00
parent 45858d54ae
commit cd6bd79d63
27 changed files with 142 additions and 542 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

56
src/bindings/lua/context.cpp
View file

@ -17,28 +17,7 @@ Author: Leonardo de Moura
#include "bindings/lua/formatter.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<context_entry*>(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;
}
DECL_UDATA(context_entry)
static int mk_context_entry(lua_State * L) {
int nargs = lua_gettop(L);
@ -48,11 +27,6 @@ static int mk_context_entry(lua_State * L) {
return push_context_entry(L, context_entry(to_name_ext(L, 1), to_nonnull_expr(L, 2), to_nonnull_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()); }
@ -65,28 +39,7 @@ static const struct luaL_Reg context_entry_m[] = {
{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<context*>(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;
}
DECL_UDATA(context)
static int context_tostring(lua_State * L) {
std::ostringstream out;
@ -111,11 +64,6 @@ static int mk_context(lua_State * L) {
}
}
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)

12
src/bindings/lua/context.h
View file

@ -7,15 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include <lua.hpp>
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);
UDATA_DEFS(context_entry)
UDATA_DEFS(context)
void open_context(lua_State * L);
}

28
src/bindings/lua/environment.cpp
View file

@ -19,15 +19,7 @@ Author: Leonardo de Moura
#include "bindings/lua/formatter.h"
namespace lean {
constexpr char const * environment_mt = "environment.mt";
bool is_environment(lua_State * L, int idx) {
return testudata(L, idx, environment_mt);
}
environment & to_environment(lua_State * L, int idx) {
return *static_cast<environment*>(luaL_checkudata(L, idx, environment_mt));
}
DECL_UDATA(environment)
ro_environment::ro_environment(lua_State * L, int idx):
read_only_environment(to_environment(L, idx)) {
@ -37,19 +29,6 @@ rw_environment::rw_environment(lua_State * L, int idx):
read_write_environment(to_environment(L, idx)) {
}
static int environment_gc(lua_State * L) {
to_environment(L, 1).~environment();
return 0;
}
int push_environment(lua_State * L, environment const & env) {
void * mem = lua_newuserdata(L, sizeof(environment));
new (mem) environment(env);
luaL_getmetatable(L, environment_mt);
lua_setmetatable(L, -2);
return 1;
}
static int mk_environment(lua_State * L) {
return push_environment(L, environment());
}
@ -197,11 +176,6 @@ static int environment_local_objects(lua_State * L) {
return environment_objects_core(L, true);
}
static int environment_pred(lua_State * L) {
lua_pushboolean(L, is_environment(L, 1));
return 1;
}
static int environment_tostring(lua_State * L) {
ro_environment env(L, 1);
std::ostringstream out;

5
src/bindings/lua/environment.h
View file

@ -9,11 +9,8 @@ Author: Leonardo de Moura
#include "kernel/threadsafe_environment.h"
namespace lean {
class environment;
UDATA_DEFS(environment)
void open_environment(lua_State * L);
bool is_environment(lua_State * L, int idx);
int push_environment(lua_State * L, environment const & env);
/**
\brief Auxiliary class for setting the Lua registry of a Lua state
with an environment object.

28
src/bindings/lua/expr.cpp
View file

@ -32,15 +32,7 @@ Author: Leonardo de Moura
#include "bindings/lua/numerics.h"
namespace lean {
constexpr char const * expr_mt = "expr.mt";
bool is_expr(lua_State * L, int idx) {
return testudata(L, idx, expr_mt);
}
expr & to_expr(lua_State * L, int idx) {
return *static_cast<expr*>(luaL_checkudata(L, idx, expr_mt));
}
DECL_UDATA(expr)
expr & to_nonnull_expr(lua_State * L, int idx) {
expr & r = to_expr(L, idx);
@ -56,19 +48,6 @@ expr & to_app(lua_State * L, int idx) {
return r;
}
int push_expr(lua_State * L, expr const & e) {
void * mem = lua_newuserdata(L, sizeof(expr));
new (mem) expr(e);
luaL_getmetatable(L, expr_mt);
lua_setmetatable(L, -2);
return 1;
}
static int expr_gc(lua_State * L) {
to_expr(L, 1).~expr();
return 0;
}
static int expr_tostring(lua_State * L) {
std::ostringstream out;
expr & e = to_expr(L, 1);
@ -293,11 +272,6 @@ static int expr_fields(lua_State * L) {
return 0; // LCOV_EXCL_LINE
}
static int expr_pred(lua_State * L) {
lua_pushboolean(L, is_expr(L, 1));
return 1;
}
static int expr_for_each(lua_State * L) {
expr & e = to_nonnull_expr(L, 1); // expr
luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun

7
src/bindings/lua/expr.h
View file

@ -7,10 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include <lua.hpp>
namespace lean {
class expr;
void open_expr(lua_State * L);
bool is_expr(lua_State * L, int idx);
expr & to_expr(lua_State * L, int idx);
UDATA_DEFS(expr);
expr & to_nonnull_expr(lua_State * L, int idx);
int push_expr(lua_State * L, expr const & o);
void open_expr(lua_State * L);
}

28
src/bindings/lua/format.cpp
View file

@ -17,23 +17,7 @@ Author: Leonardo de Moura
#include "bindings/lua/options.h"
namespace lean {
constexpr char const * format_mt = "format.mt";
int push_format(lua_State * L, format const & e) {
void * mem = lua_newuserdata(L, sizeof(format));
new (mem) format(e);
luaL_getmetatable(L, format_mt);
lua_setmetatable(L, -2);
return 1;
}
bool is_format(lua_State * L, int idx) {
return testudata(L, idx, format_mt);
}
format & to_format(lua_State * L, int idx) {
return *static_cast<format*>(luaL_checkudata(L, idx, format_mt));
}
DECL_UDATA(format)
format to_format_elem(lua_State * L, int idx) {
if (is_format(L, idx))
@ -50,11 +34,6 @@ format to_format_elem(lua_State * L, int idx) {
return format(lua_tostring(L, idx));
}
static int format_gc(lua_State * L) {
to_format(L, 1).~format();
return 0;
}
static int format_tostring(lua_State * L) {
std::ostringstream out;
out << mk_pair(to_format(L, 1), get_global_options(L));
@ -114,11 +93,6 @@ static int format_highlight(lua_State * L) {
static int format_line(lua_State * L) { return push_format(L, line()); }
static int format_space(lua_State * L) { return push_format(L, space()); }
static int format_pred(lua_State * L) {
lua_pushboolean(L, is_format(L, 1));
return 1;
}
static const struct luaL_Reg format_m[] = {
{"__gc", format_gc}, // never throws
{"__tostring", safe_function<format_tostring>},

5
src/bindings/lua/format.h
View file

@ -7,9 +7,6 @@ Author: Leonardo de Moura
#pragma once
#include <lua.hpp>
namespace lean {
class format;
UDATA_DEFS(format)
void open_format(lua_State * L);
bool is_format(lua_State * L, int idx);
format & to_format(lua_State * L, int idx);
int push_format(lua_State * L, format const & o);
}

28
src/bindings/lua/formatter.cpp
View file

@ -17,28 +17,7 @@ Author: Leonardo de Moura
#include "bindings/lua/state.h"
namespace lean {
constexpr char const * formatter_mt = "formatter.mt";
bool is_formatter(lua_State * L, int idx) {
return testudata(L, idx, formatter_mt);
}
formatter & to_formatter(lua_State * L, int idx) {
return *static_cast<formatter*>(luaL_checkudata(L, idx, formatter_mt));
}
int push_formatter(lua_State * L, formatter const & o) {
void * mem = lua_newuserdata(L, sizeof(formatter));
new (mem) formatter(o);
luaL_getmetatable(L, formatter_mt);
lua_setmetatable(L, -2);
return 1;
}
static int formatter_gc(lua_State * L) {
to_formatter(L, 1).~formatter();
return 0;
}
DECL_UDATA(formatter)
[[ noreturn ]] void throw_invalid_formatter_call() {
throw exception("invalid formatter invocation, the acceptable arguments are: (expr, options?), (context, options?), (context, expr, bool? options?), (kernel object, options?), (environment, options?)");
@ -78,11 +57,6 @@ static int formatter_call(lua_State * L) {
}
}
static int formatter_pred(lua_State * L) {
lua_pushboolean(L, is_formatter(L, 1));
return 1;
}
static const struct luaL_Reg formatter_m[] = {
{"__gc", formatter_gc}, // never throws
{"__call", safe_function<formatter_call>},

5
src/bindings/lua/formatter.h
View file

@ -7,11 +7,8 @@ Author: Leonardo de Moura
#pragma once
#include <lua.hpp>
namespace lean {
class formatter;
UDATA_DEFS(formatter)
void open_formatter(lua_State * L);
bool is_formatter(lua_State * L, int idx);
formatter & to_formatter(lua_State * L, int idx);
int push_formatter(lua_State * L, formatter const & o);
/**
\brief Return the formatter object associated with the given Lua State.
This procedure checks for options at:

28
src/bindings/lua/level.cpp
View file

@ -14,28 +14,7 @@ Author: Leonardo de Moura
#include "bindings/lua/options.h"
namespace lean {
constexpr char const * level_mt = "level.mt";
bool is_level(lua_State * L, int idx) {
return testudata(L, idx, level_mt);
}
level & to_level(lua_State * L, int idx) {
return *static_cast<level*>(luaL_checkudata(L, idx, level_mt));
}
int push_level(lua_State * L, level const & e) {
void * mem = lua_newuserdata(L, sizeof(level));
new (mem) level(e);
luaL_getmetatable(L, level_mt);
lua_setmetatable(L, -2);
return 1;
}
static int level_gc(lua_State * L) {
to_level(L, 1).~level();
return 0;
}
DECL_UDATA(level)
static int level_tostring(lua_State * L) {
std::ostringstream out;
@ -119,11 +98,6 @@ static int level_max_level(lua_State * L) {
return push_level(L, max_level(to_level(L, 1), luaL_checkinteger(L, 2)));
}
static int level_pred(lua_State * L) {
lua_pushboolean(L, is_level(L, 1));
return 1;
}
static int level_get_kind(lua_State * L) {
lua_pushinteger(L, static_cast<int>(kind(to_level(L, 1))));
return 1;

5
src/bindings/lua/level.h
View file

@ -7,9 +7,6 @@ Author: Leonardo de Moura
#pragma once
#include <lua.hpp>
namespace lean {
class level;
UDATA_DEFS(level)
void open_level(lua_State * L);
bool is_level(lua_State * L, int idx);
level & to_level(lua_State * L, int idx);
int push_level(lua_State * L, level const & o);
}

56
src/bindings/lua/local_context.cpp
View file

@ -12,28 +12,7 @@ Author: Leonardo de Moura
#include "bindings/lua/local_context.h"
namespace lean {
constexpr char const * local_entry_mt = "local_entry.mt";
bool is_local_entry(lua_State * L, int idx) {
return testudata(L, idx, local_entry_mt);
}
local_entry & to_local_entry(lua_State * L, int idx) {
return *static_cast<local_entry*>(luaL_checkudata(L, idx, local_entry_mt));
}
int push_local_entry(lua_State * L, local_entry const & e) {
void * mem = lua_newuserdata(L, sizeof(local_entry));
new (mem) local_entry(e);
luaL_getmetatable(L, local_entry_mt);
lua_setmetatable(L, -2);
return 1;
}
static int local_entry_gc(lua_State * L) {
to_local_entry(L, 1).~local_entry();
return 0;
}
DECL_UDATA(local_entry)
static int local_entry_eq(lua_State * L) {
lua_pushboolean(L, to_local_entry(L, 1) == to_local_entry(L, 2));
@ -48,11 +27,6 @@ static int local_entry_mk_inst(lua_State * L) {
return push_local_entry(L, mk_inst(luaL_checkinteger(L, 1), to_nonnull_expr(L, 2)));
}
static int local_entry_pred(lua_State * L) {
lua_pushboolean(L, is_local_entry(L, 1));
return 1;
}
static int local_entry_is_lift(lua_State * L) {
lua_pushboolean(L, is_local_entry(L, 1) && to_local_entry(L, 1).is_lift());
return 1;
@ -95,28 +69,7 @@ static const struct luaL_Reg local_entry_m[] = {
{0, 0}
};
constexpr char const * local_context_mt = "local_context.mt";
bool is_local_context(lua_State * L, int idx) {
return testudata(L, idx, local_context_mt);
}
local_context & to_local_context(lua_State * L, int idx) {
return *static_cast<local_context*>(luaL_checkudata(L, idx, local_context_mt));
}
int push_local_context(lua_State * L, local_context const & e) {
void * mem = lua_newuserdata(L, sizeof(local_context));
new (mem) local_context(e);
luaL_getmetatable(L, local_context_mt);
lua_setmetatable(L, -2);
return 1;
}
static int local_context_gc(lua_State * L) {
to_local_context(L, 1).~local_context();
return 0;
}
DECL_UDATA(local_context)
static int mk_local_context(lua_State * L) {
int nargs = lua_gettop(L);
@ -140,11 +93,6 @@ static int local_context_is_nil(lua_State * L) {
return 1;
}
static int local_context_pred(lua_State * L) {
lua_pushboolean(L, is_local_context(L, 1));
return 1;
}
static const struct luaL_Reg local_context_m[] = {
{"__gc", local_context_gc},
{"head", local_context_head},

10
src/bindings/lua/local_context.h
View file

@ -8,13 +8,7 @@ Author: Leonardo de Moura
#include <lua.hpp>
#include "kernel/expr.h"
namespace lean {
bool is_local_entry(lua_State * L, int idx);
local_entry & to_local_entry(lua_State * L, int idx);
int push_local_entry(lua_State * L, local_entry const & o);
bool is_local_context(lua_State * L, int idx);
local_context & to_local_context(lua_State * L, int idx);
int push_local_context(lua_State * L, local_context const & o);
UDATA_DEFS(local_entry)
UDATA_DEFS_CORE(local_context)
void open_local_context(lua_State * L);
}

44
src/bindings/lua/name.cpp
View file

@ -7,18 +7,11 @@ Author: Leonardo de Moura
#include <lua.hpp>
#include "util/debug.h"
#include "util/name.h"
#include "util/sstream.h"
#include "bindings/lua/util.h"
namespace lean {
constexpr char const * name_mt = "name.mt";
bool is_name(lua_State * L, int idx) {
return testudata(L, idx, name_mt);
}
name & to_name(lua_State * L, int idx) {
return *static_cast<name*>(luaL_checkudata(L, idx, name_mt));
}
DECL_UDATA(name)
name to_name_ext(lua_State * L, int idx) {
if (lua_isstring(L, idx)) {
@ -45,36 +38,22 @@ name to_name_ext(lua_State * L, int idx) {
}
}
int push_name(lua_State * L, name const & n) {
void * mem = lua_newuserdata(L, sizeof(name));
new (mem) name(n);
luaL_getmetatable(L, name_mt);
lua_setmetatable(L, -2);
return 1;
}
static int mk_name(lua_State * L) {
int nargs = lua_gettop(L);
name r;
for (int i = 1; i <= nargs; i++) {
if (lua_isnil(L, i)) {
// skip
} else if (lua_isuserdata(L, i)) {
r = r + to_name(L, i);
} else if (lua_isstring(L, i)) {
r = name(r, luaL_checkstring(L, i));
} else {
r = name(r, luaL_checkinteger(L, i));
switch (lua_type(L, i)) {
case LUA_TNIL: break; // skip
case LUA_TNUMBER: r = name(r, lua_tointeger(L, i)); break;
case LUA_TSTRING: r = name(r, lua_tostring(L, i)); break;
case LUA_TUSERDATA: r = r + to_name(L, i); break;
default:
throw exception(sstream() << "arg #" << i << " must be a hierarchical name, string, or integer");
}
}
return push_name(L, r);
}
static int name_gc(lua_State * L) {
to_name(L, 1).~name();
return 0;
}
static int name_tostring(lua_State * L) {
lua_pushstring(L, to_name(L, 1).to_string().c_str());
return 1;
@ -90,11 +69,6 @@ static int name_lt(lua_State * L) {
return 1;
}
static int name_pred(lua_State * L) {
lua_pushboolean(L, is_name(L, 1));
return 1;
}
static int name_hash(lua_State * L) {
lua_pushinteger(L, to_name(L, 1).hash());
return 1;

5
src/bindings/lua/name.h
View file

@ -7,10 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include <lua.hpp>
namespace lean {
class name;
UDATA_DEFS(name)
void open_name(lua_State * L);
bool is_name(lua_State * L, int idx);
name & to_name(lua_State * L, int idx);
name to_name_ext(lua_State * L, int idx);
int push_name(lua_State * L, name const & n);
}

58
src/bindings/lua/numerics.cpp
View file

@ -12,7 +12,7 @@ Author: Leonardo de Moura
#include "bindings/lua/util.h"
namespace lean {
constexpr char const * mpz_mt = "mpz.mt";
DECL_UDATA(mpz)
template<unsigned idx>
static mpz const & to_mpz(lua_State * L) {
@ -28,14 +28,6 @@ static mpz const & to_mpz(lua_State * L) {
}
}
bool is_mpz(lua_State * L, int idx) {
return testudata(L, idx, mpz_mt);
}
mpz & to_mpz(lua_State * L, int idx) {
return *static_cast<mpz*>(luaL_checkudata(L, idx, mpz_mt));
}
mpz to_mpz_ext(lua_State * L, int idx) {
if (lua_isuserdata(L, idx)) {
return *static_cast<mpz*>(luaL_checkudata(L, idx, mpz_mt));
@ -46,20 +38,6 @@ mpz to_mpz_ext(lua_State * L, int idx) {
}
}
int push_mpz(lua_State * L, mpz const & val) {
void * mem = lua_newuserdata(L, sizeof(mpz));
new (mem) mpz(val);
luaL_getmetatable(L, mpz_mt);
lua_setmetatable(L, -2);
return 1;
}
static int mpz_gc(lua_State * L) {
mpz * n = static_cast<mpz*>(luaL_checkudata(L, 1, mpz_mt));
n->~mpz();
return 0;
}
static int mpz_tostring(lua_State * L) {
mpz * n = static_cast<mpz*>(luaL_checkudata(L, 1, mpz_mt));
std::ostringstream out;
@ -111,11 +89,6 @@ static int mk_mpz(lua_State * L) {
return push_mpz(L, arg);
}
static int mpz_pred(lua_State * L) {
lua_pushboolean(L, is_mpz(L, 1));
return 1;
}
static const struct luaL_Reg mpz_m[] = {
{"__gc", mpz_gc}, // never throws
{"__tostring", safe_function<mpz_tostring>},
@ -138,7 +111,7 @@ void open_mpz(lua_State * L) {
SET_GLOBAL_FUN(mpz_pred, "is_mpz");
}
constexpr char const * mpq_mt = "mpq.mt";
DECL_UDATA(mpq)
template<unsigned idx>
static mpq const & to_mpq(lua_State * L) {
@ -157,14 +130,6 @@ static mpq const & to_mpq(lua_State * L) {
return arg;
}
bool is_mpq(lua_State * L, int idx) {
return testudata(L, idx, mpq_mt);
}
mpq & to_mpq(lua_State * L, int idx) {
return *static_cast<mpq*>(luaL_checkudata(L, idx, mpq_mt));
}
mpq to_mpq_ext(lua_State * L, int idx) {
if (lua_isuserdata(L, idx)) {
if (is_mpz(L, idx)) {
@ -179,20 +144,6 @@ mpq to_mpq_ext(lua_State * L, int idx) {
}
}
int push_mpq(lua_State * L, mpq const & val) {
void * mem = lua_newuserdata(L, sizeof(mpq));
new (mem) mpq(val);
luaL_getmetatable(L, mpq_mt);
lua_setmetatable(L, -2);
return 1;
}
static int mpq_gc(lua_State * L) {
mpq * n = static_cast<mpq*>(luaL_checkudata(L, 1, mpq_mt));
n->~mpq();
return 0;
}
static int mpq_tostring(lua_State * L) {
mpq * n = static_cast<mpq*>(luaL_checkudata(L, 1, mpq_mt));
std::ostringstream out;
@ -244,11 +195,6 @@ static int mk_mpq(lua_State * L) {
return push_mpq(L, arg);
}
static int mpq_pred(lua_State * L) {
lua_pushboolean(L, is_mpq(L, 1));
return 1;
}
static const struct luaL_Reg mpq_m[] = {
{"__gc", mpq_gc}, // never throws
{"__tostring", safe_function<mpq_tostring>},

14
src/bindings/lua/numerics.h
View file

@ -7,17 +7,11 @@ Author: Leonardo de Moura
#pragma once
#include <lua.hpp>
namespace lean {
class mpz;
void open_mpz(lua_State * L);
bool is_mpz(lua_State * L, int idx);
mpz & to_mpz(lua_State * L, int idx);
UDATA_DEFS(mpz)
mpz to_mpz_ext(lua_State * L, int idx);
int push_mpz(lua_State * L, mpz const & val);
void open_mpz(lua_State * L);
class mpq;
void open_mpq(lua_State * L);
bool is_mpq(lua_State * L, int idx);
mpq & to_mpq(lua_State * L, int idx);
UDATA_DEFS(mpq)
mpq to_mpq_ext(lua_State * L, int idx);
int push_mpq(lua_State * L, mpq const & val);
void open_mpq(lua_State * L);
}

28
src/bindings/lua/object.cpp
View file

@ -17,15 +17,7 @@ Author: Leonardo de Moura
#include "bindings/lua/formatter.h"
namespace lean {
constexpr char const * object_mt = "object.mt";
bool is_object(lua_State * L, int idx) {
return testudata(L, idx, object_mt);
}
object & to_object(lua_State * L, int idx) {
return *static_cast<object*>(luaL_checkudata(L, idx, object_mt));
}
DECL_UDATA(object)
object & to_nonnull_object(lua_State * L, int idx) {
object & r = to_object(L, idx);
@ -34,19 +26,6 @@ object & to_nonnull_object(lua_State * L, int idx) {
return r;
}
int push_object(lua_State * L, object const & o) {
void * mem = lua_newuserdata(L, sizeof(object));
new (mem) object(o);
luaL_getmetatable(L, object_mt);
lua_setmetatable(L, -2);
return 1;
}
static int object_gc(lua_State * L) {
to_object(L, 1).~object();
return 0;
}
static int object_is_null(lua_State * L) {
lua_pushboolean(L, !to_object(L, 1));
return 1;
@ -127,11 +106,6 @@ static int object_in_builtin_set(lua_State * L) {
return 1;
}
static int object_pred(lua_State * L) {
lua_pushboolean(L, is_object(L, 1));
return 1;
}
static int object_tostring(lua_State * L) {
std::ostringstream out;
formatter fmt = get_global_formatter(L);

5
src/bindings/lua/object.h
View file

@ -7,9 +7,6 @@ Author: Leonardo de Moura
#pragma once
#include <lua.hpp>
namespace lean {
class object;
UDATA_DEFS(object)
void open_object(lua_State * L);
bool is_object(lua_State * L, int idx);
object & to_object(lua_State * L, int idx);
int push_object(lua_State * L, object const & o);
}

28
src/bindings/lua/options.cpp
View file

@ -16,23 +16,7 @@ Author: Leonardo de Moura
#include "bindings/lua/state.h"
namespace lean {
constexpr char const * options_mt = "options.mt";
bool is_options(lua_State * L, int idx) {
return testudata(L, idx, options_mt);
}
options & to_options(lua_State * L, int idx) {
return *static_cast<options*>(luaL_checkudata(L, idx, options_mt));
}
int push_options(lua_State * L, options const & o) {
void * mem = lua_newuserdata(L, sizeof(options));
new (mem) options(o);
luaL_getmetatable(L, options_mt);
lua_setmetatable(L, -2);
return 1;
}
DECL_UDATA(options)
static int mk_options(lua_State * L) {
options r;
@ -48,11 +32,6 @@ static name to_key(lua_State * L, int idx) {
}
}
static int options_gc(lua_State * L) {
to_options(L, 1).~options();
return 0;
}
static int options_tostring(lua_State * L) {
std::ostringstream out;
out << to_options(L, 1);
@ -166,11 +145,6 @@ static int options_update(lua_State * L) {
}
}
static int options_pred(lua_State * L) {
lua_pushboolean(L, is_options(L, 1));
return 1;
}
static char g_options_key;
options get_global_options(lua_State * L) {

5
src/bindings/lua/options.h
View file

@ -7,11 +7,8 @@ Author: Leonardo de Moura
#pragma once
#include <lua.hpp>
namespace lean {
class options;
UDATA_DEFS(options)
void open_options(lua_State * L);
bool is_options(lua_State * L, int idx);
options & to_options(lua_State * L, int idx);
int push_options(lua_State * L, options const & o);
/**
\brief Return the set of options associated with the given Lua State.
This procedure checks for options at:

28
src/bindings/lua/sexpr.cpp
View file

@ -13,28 +13,7 @@ Author: Leonardo de Moura
#include "bindings/lua/numerics.h"
namespace lean {
constexpr char const * sexpr_mt = "sexpr.mt";
int push_sexpr(lua_State * L, sexpr const & e) {
void * mem = lua_newuserdata(L, sizeof(sexpr));
new (mem) sexpr(e);
luaL_getmetatable(L, sexpr_mt);
lua_setmetatable(L, -2);
return 1;
}
bool is_sexpr(lua_State * L, int idx) {
return testudata(L, idx, sexpr_mt);
}
sexpr & to_sexpr(lua_State * L, int idx) {
return *static_cast<sexpr*>(lua_touserdata(L, idx));
}
static int sexpr_gc(lua_State * L) {
to_sexpr(L, 1).~sexpr();
return 0;
}
DECL_UDATA(sexpr)
static int sexpr_tostring(lua_State * L) {
std::ostringstream out;
@ -176,11 +155,6 @@ static int sexpr_to_mpq(lua_State * L) {
return push_mpq(L, to_mpq(e));
}
static int sexpr_pred(lua_State * L) {
lua_pushboolean(L, is_sexpr(L, 1));
return 1;
}
static int sexpr_get_kind(lua_State * L) {
lua_pushinteger(L, static_cast<int>(to_sexpr(L, 1).kind()));
return 1;

5
src/bindings/lua/sexpr.h
View file

@ -7,9 +7,6 @@ Author: Leonardo de Moura
#pragma once
#include <lua.hpp>
namespace lean {
class sexpr;
UDATA_DEFS(sexpr)
void open_sexpr(lua_State * L);
bool is_sexpr(lua_State * L, int idx);
sexpr & to_sexpr(lua_State * L, int idx);
int push_sexpr(lua_State * L, sexpr const & e);
}

94
src/bindings/lua/splay_map.cpp
View file

@ -12,61 +12,40 @@ Author: Leonardo de Moura
namespace lean {
typedef splay_map<lref, lref, lref_lt_proc> lua_splay_map;
constexpr char const * splay_map_mt = "splay_map.mt";
DECL_UDATA(lua_splay_map)
bool is_splay_map(lua_State * L, int idx) {
return testudata(L, idx, splay_map_mt);
}
lua_splay_map & to_splay_map(lua_State * L, int idx) {
return *static_cast<lua_splay_map*>(luaL_checkudata(L, idx, splay_map_mt));
}
int push_splay_map(lua_State * L, lua_splay_map const & o) {
void * mem = lua_newuserdata(L, sizeof(lua_splay_map));
new (mem) lua_splay_map(o);
luaL_getmetatable(L, splay_map_mt);
lua_setmetatable(L, -2);
return 1;
}
static int mk_splay_map(lua_State * L) {
static int mk_lua_splay_map(lua_State * L) {
lua_splay_map r;
return push_splay_map(L, r);
return push_lua_splay_map(L, r);
}
static int splay_map_gc(lua_State * L) {
to_splay_map(L, 1).~lua_splay_map();
return 0;
}
static int splay_map_size(lua_State * L) {
lua_pushinteger(L, to_splay_map(L, 1).size());
static int lua_splay_map_size(lua_State * L) {
lua_pushinteger(L, to_lua_splay_map(L, 1).size());
return 1;
}
static int splay_map_contains(lua_State * L) {
lua_pushboolean(L, to_splay_map(L, 1).contains(lref(L, 2)));
static int lua_splay_map_contains(lua_State * L) {
lua_pushboolean(L, to_lua_splay_map(L, 1).contains(lref(L, 2)));
return 1;
}
static int splay_map_empty(lua_State * L) {
lua_pushboolean(L, to_splay_map(L, 1).empty());
static int lua_splay_map_empty(lua_State * L) {
lua_pushboolean(L, to_lua_splay_map(L, 1).empty());
return 1;
}
static int splay_map_insert(lua_State * L) {
to_splay_map(L, 1).insert(lref(L, 2), lref(L, 3));
static int lua_splay_map_insert(lua_State * L) {
to_lua_splay_map(L, 1).insert(lref(L, 2), lref(L, 3));
return 0;
}
static int splay_map_erase(lua_State * L) {
to_splay_map(L, 1).erase(lref(L, 2));
static int lua_splay_map_erase(lua_State * L) {
to_lua_splay_map(L, 1).erase(lref(L, 2));
return 0;
}
static int splay_map_find(lua_State * L) {
lua_splay_map & m = to_splay_map(L, 1);
static int lua_splay_map_find(lua_State * L) {
lua_splay_map & m = to_lua_splay_map(L, 1);
lref * val = m.splay_find(lref(L, 2));
if (val) {
lean_assert(val->get_state() == L);
@ -77,21 +56,16 @@ static int splay_map_find(lua_State * L) {
return 1;
}
static int splay_map_copy(lua_State * L) {
return push_splay_map(L, to_splay_map(L, 1));
static int lua_splay_map_copy(lua_State * L) {
return push_lua_splay_map(L, to_lua_splay_map(L, 1));
}
static int splay_map_pred(lua_State * L) {
lua_pushboolean(L, is_splay_map(L, 1));
return 1;
}
static int splay_map_for_each(lua_State * L) {
static int lua_splay_map_for_each(lua_State * L) {
// Remark: we take a copy of the map to make sure
// for_each will not crash if the map is updated while being
// traversed.
// The copy operation is very cheap O(1).
lua_splay_map m(to_splay_map(L, 1)); // map
lua_splay_map m(to_lua_splay_map(L, 1)); // map
luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
m.for_each([&](lref const & k, lref const & v) {
lua_pushvalue(L, 2); // push user-fun
@ -102,27 +76,27 @@ static int splay_map_for_each(lua_State * L) {
return 0;
}
static const struct luaL_Reg splay_map_m[] = {
{"__gc", splay_map_gc}, // never throws
{"__len", safe_function<splay_map_size> },
{"contains", safe_function<splay_map_contains>},
{"size", safe_function<splay_map_size>},
{"empty", safe_function<splay_map_empty>},
{"insert", safe_function<splay_map_insert>},
{"erase", safe_function<splay_map_erase>},
{"find", safe_function<splay_map_find>},
{"copy", safe_function<splay_map_copy>},
{"for_each", safe_function<splay_map_for_each>},
static const struct luaL_Reg lua_splay_map_m[] = {
{"__gc", lua_splay_map_gc}, // never throws
{"__len", safe_function<lua_splay_map_size> },
{"contains", safe_function<lua_splay_map_contains>},
{"size", safe_function<lua_splay_map_size>},
{"empty", safe_function<lua_splay_map_empty>},
{"insert", safe_function<lua_splay_map_insert>},
{"erase", safe_function<lua_splay_map_erase>},
{"find", safe_function<lua_splay_map_find>},
{"copy", safe_function<lua_splay_map_copy>},
{"for_each", safe_function<lua_splay_map_for_each>},
{0, 0}
};
void open_splay_map(lua_State * L) {
luaL_newmetatable(L, splay_map_mt);
luaL_newmetatable(L, lua_splay_map_mt);
lua_pushvalue(L, -1);
lua_setfield(L, -2, "__index");
setfuncs(L, splay_map_m, 0);
setfuncs(L, lua_splay_map_m, 0);
SET_GLOBAL_FUN(mk_splay_map, "splay_map");
SET_GLOBAL_FUN(splay_map_pred, "is_splay_map");
SET_GLOBAL_FUN(mk_lua_splay_map, "splay_map");
SET_GLOBAL_FUN(lua_splay_map_pred, "is_splay_map");
}
}

63
src/bindings/lua/util.h
View file

@ -33,4 +33,67 @@ template<lua_CFunction F> void set_global_function(lua_State * L, char const * n
// Auxiliary macro for creating a Lua table that stores enumeration values
#define SET_ENUM(N, V) lua_pushstring(L, N); lua_pushinteger(L, static_cast<int>(V)); lua_settable(L, -3)
#define DECL_PUSH_CORE(NAME, T, TREF) \
int push_ ## NAME(lua_State * L, TREF val) { \
void * mem = lua_newuserdata(L, sizeof(T)); \
new (mem) T(val); \
luaL_getmetatable(L, NAME ## _mt); \
lua_setmetatable(L, -2); \
return 1; \
}
#define DECL_PUSH(T) \
DECL_PUSH_CORE(T, T, T const &) \
DECL_PUSH_CORE(T, T, T &&)
#define DECL_GC(T) static int T ## _gc(lua_State * L) { static_cast<T*>(lua_touserdata(L, 1))->~T(); return 0; }
#define DECL_PRED(T) \
bool is_ ## T(lua_State * L, int idx) { return testudata(L, idx, T ## _mt); } \
static int T ## _pred(lua_State * L) { \
lua_pushboolean(L, is_ ## T(L, 1)); \
return 1; \
}
/**
\brief Create basic declarations for adding a new kind of userdata in Lua
T is a Lean object type.
For example, if T == expr, it produces an implementation for the
following declarations
constexpr char const * expr_mt = "expr";
expr & to_expr(lua_State * L, int i);
bool is_expr(lua_State * L, int i);
static int expr_pred(lua_State * L);
static int expr_gc(lua_State * L);
int push_expr(lua_State * L, expr const & e);
int push_expr(lua_State * L, expr && e);
*/
#define DECL_UDATA(T) \
constexpr char const * T ## _mt = #T; \
T & to_ ## T(lua_State * L, int i) { return *static_cast<T*>(luaL_checkudata(L, i, T ## _mt)); } \
DECL_PRED(T) \
DECL_GC(T) \
DECL_PUSH(T)
/**
\brief Similar to DECL_UDATA, but it only declares the functions.
For example, if T == expr, it produces the following declarations:
class expr;
expr & to_expr(lua_State * L, int i);
bool is_expr(lua_State * L, int i);
int push_expr(lua_State * L, expr const & e);
int push_expr(lua_State * L, expr && e);
*/
#define UDATA_DEFS_CORE(T) \
T & to_ ## T(lua_State * L, int i); \
bool is_ ## T(lua_State * L, int i); \
int push_ ## T(lua_State * L, T const & e); \
int push_ ## T(lua_State * L, T && e);
#define UDATA_DEFS(T) \
class T; \
UDATA_DEFS_CORE(T)
}

6
src/tests/kernel/expr.cpp
View file

@ -147,8 +147,8 @@ expr mk_big(expr f, unsigned depth, unsigned val) {
void tst3() {
expr f = Const("f");
expr r1 = mk_big(f, 18, 0);
expr r2 = mk_big(f, 18, 0);
expr r1 = mk_big(f, 20, 0);
expr r2 = mk_big(f, 20, 0);
lean_assert(r1 == r2);
}
@ -376,6 +376,8 @@ int main() {
std::cout << "sizeof(expr): " << sizeof(expr) << "\n";
std::cout << "sizeof(expr_app): " << sizeof(expr_app) << "\n";
std::cout << "sizeof(expr_cell): " << sizeof(expr_cell) << "\n";
tst3();
return 0;
tst1();
tst2();
tst3();