feat(util): name_generator Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/util/name_generator.cpp

@@ -24,4 +24,29 @@ void swap(name_generator & a, name_generator & b) {
     swap(a.m_prefix, b.m_prefix);
     std::swap(a.m_next_idx, b.m_next_idx);
 }
+
+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 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()); }
+static const struct luaL_Reg name_generator_m[] = {
+    {"__gc",     name_generator_gc}, // never throws
+    {"next",     safe_function<name_generator_next>},
+    {"prefix",   safe_function<name_generator_prefix>},
+    {"mk_child", safe_function<name_generator_mk_child>},
+    {0, 0}
+};
+static void name_generator_migrate(lua_State * src, int i, lua_State * tgt) { push_name_generator(tgt, to_name_generator(src, i)); }
+
+void open_name_generator(lua_State * L) {
+    luaL_newmetatable(L, name_generator_mt);
+    set_migrate_fn_field(L, -1, name_generator_migrate);
+    lua_pushvalue(L, -1);
+    lua_setfield(L, -2, "__index");
+    setfuncs(L, name_generator_m, 0);
+
+    SET_GLOBAL_FUN(mk_name_generator,   "name_generator");
+    SET_GLOBAL_FUN(name_generator_pred, "is_name_generator");
+}
 }

src/util/name_generator.h

@@ -36,4 +36,7 @@ public:
     friend void swap(name_generator & a, name_generator & b);
 };
 void swap(name_generator & a, name_generator & b);
+
+UDATA_DEFS(name_generator)
+void open_name_generator(lua_State * L);
 }

src/util/script_state.cpp

@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 #include "util/script_state.h"
 #include "util/script_exception.h"
 #include "util/name.h"
+#include "util/name_generator.h"
 #include "util/rb_map.h"
 #include "util/lean_path.h"
 
@@ -84,6 +85,7 @@ struct script_state::imp {
         luaL_openlibs(m_state);
         open_exception(m_state);
         open_name(m_state);
+        open_name_generator(m_state);
         open_rb_map(m_state);
         open_extra(m_state);
 

tests/lua/name_gen1.lua

@@ -0,0 +1,11 @@
+local g = name_generator("tst")
+assert(g:next() == name("tst", 0))
+assert(g:next() == name("tst", 1))
+assert(g:prefix() == name("tst"))
+local cg = g:mk_child()
+assert(cg:prefix() == name("tst", 2))
+assert(cg:next() == name("tst", 2, 0))
+assert(cg:next() == name("tst", 2, 1))
+assert(cg:next() == name("tst", 2, 2))
+assert(g:next() == name("tst", 3))
+assert(is_name_generator(g))