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

feat(util/name_generator): allow name generator to be created without providing any argument in the Lua API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-02 12:39:41 -07:00
parent 6ab46396d8
commit cc3fb0c51f
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/util/name_generator.cpp
View file

@ -26,7 +26,13 @@ void swap(name_generator & a, name_generator & b) {
}
DECL_UDATA(name_generator)
static int mk_name_generator(lua_State * L) { return push_name_generator(L, name_generator(to_name_ext(L, 1))); }
static name g_tmp_prefix = name::mk_internal_unique_name();
static int mk_name_generator(lua_State * L) {
if (lua_gettop(L) == 0)
return push_name_generator(L, name_generator(g_tmp_prefix));
else
return push_name_generator(L, name_generator(to_name_ext(L, 1)));
}
static int name_generator_next(lua_State * L) { return push_name(L, to_name_generator(L, 1).next()); }
static int name_generator_prefix(lua_State * L) { return push_name(L, to_name_generator(L, 1).prefix()); }
static int name_generator_mk_child(lua_State * L) { return push_name_generator(L, to_name_generator(L, 1).mk_child()); }