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

feat(util): expose list<name> in Lua

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-04-30 16:32:10 -07:00
parent 03a32dcc77
commit dbf327bad9
2 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/util/name.cpp
View file

@ -19,6 +19,7 @@ Author: Leonardo de Moura
#include "util/trace.h"
#include "util/ascii.h"
#include "util/object_serializer.h"
#include "util/list_lua.h"
namespace lean {
constexpr char const * anonymous_str = "[anonymous]";
@ -520,6 +521,8 @@ static void name_migrate(lua_State * src, int i, lua_State * tgt) {
push_name(tgt, to_name(src, i));
}
DEFINE_LUA_LIST(name, push_name, to_name_ext)
void open_name(lua_State * L) {
luaL_newmetatable(L, name_mt);
set_migrate_fn_field(L, -1, name_migrate);
@ -529,6 +532,8 @@ void open_name(lua_State * L) {
SET_GLOBAL_FUN(mk_name, "name");
SET_GLOBAL_FUN(name_pred, "is_name");
open_list_name(L);
}
}
void print(lean::name const & n) { std::cout << n << std::endl; }

4
src/util/name.h
View file

@ -11,6 +11,7 @@ Author: Leonardo de Moura
#include <algorithm>
#include "util/lua.h"
#include "util/serializer.h"
#include "util/list.h"
namespace lean {
constexpr char const * lean_name_separator = "::";
@ -146,5 +147,8 @@ inline deserializer & operator>>(deserializer & d, name & n) { n = read_name(d);
UDATA_DEFS(name)
name to_name_ext(lua_State * L, int idx);
list<name> & to_list_name(lua_State * L, int idx);
list<name> to_list_name_ext(lua_State * L, int idx);
int push_list_name(lua_State * L, list<name> const & l);
void open_name(lua_State * L);
}