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

feat(util/name): add optional<name> helper functions for implementing Lua API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-29 13:33:42 -07:00
parent bfa9b90af0
commit 88440cbb3e
2 changed files with 17 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/util/name.cpp
View file

@ -498,6 +498,20 @@ name to_name_ext(lua_State * L, int idx) {
} }
} }
optional<name> to_optional_name(lua_State * L, int idx) {
if (lua_isnil(L, idx))
return optional<name>();
else
return optional<name>(to_name_ext(L, idx));
}
int push_optional_name(lua_State * L, optional<name> const & n) {
if (n)
return push_name(L, *n);
else
return push_nil(L);
}
static int name_tostring(lua_State * L) { return push_string(L, to_name(L, 1).to_string().c_str()); } static int name_tostring(lua_State * L) { return push_string(L, to_name(L, 1).to_string().c_str()); }
static int name_eq(lua_State * L) { return push_boolean(L, to_name(L, 1) == to_name(L, 2)); } static int name_eq(lua_State * L) { return push_boolean(L, to_name(L, 1) == to_name(L, 2)); }
static int name_lt(lua_State * L) { return push_boolean(L, to_name(L, 1) < to_name(L, 2)); } static int name_lt(lua_State * L) { return push_boolean(L, to_name(L, 1) < to_name(L, 2)); }

3
src/util/name.h
View file

@ -11,6 +11,7 @@ Author: Leonardo de Moura
#include <algorithm> #include <algorithm>
#include "util/lua.h" #include "util/lua.h"
#include "util/serializer.h" #include "util/serializer.h"
#include "util/optional.h"
#include "util/list.h" #include "util/list.h"
namespace lean { namespace lean {
@ -166,6 +167,8 @@ inline deserializer & operator>>(deserializer & d, name & n) { n = read_name(d);
UDATA_DEFS(name) UDATA_DEFS(name)
name to_name_ext(lua_State * L, int idx); name to_name_ext(lua_State * L, int idx);
optional<name> to_optional_name(lua_State * L, int idx);
int push_optional_name(lua_State * L, optional<name> const & n);
bool is_list_name(lua_State * L, int idx); bool is_list_name(lua_State * L, int idx);
list<name> & to_list_name(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); list<name> to_list_name_ext(lua_State * L, int idx);