From dbf327bad991e0f3dcb21773192f990a06c9b578 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 30 Apr 2014 16:32:10 -0700
Subject: [PATCH] feat(util): expose list<name> in Lua

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/util/name.cpp | 5 +++++
 src/util/name.h   | 4 ++++
 2 files changed, 9 insertions(+)

diff --git a/src/util/name.cpp b/src/util/name.cpp
index a1c46dd58..089f36a8a 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -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; }
diff --git a/src/util/name.h b/src/util/name.h
index 5e45674f8..2e89ada9b 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -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);
 }