feat(lua/name): expose hierarchical names in the Lua bindings

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

src/CMakeLists.txt

@@ -154,10 +154,13 @@ add_subdirectory(library/elaborator)
 set(LEAN_LIBS ${LEAN_LIBS} elaborator)
 add_subdirectory(frontends/lean)
 set(LEAN_LIBS ${LEAN_LIBS} lean_frontend)
+add_subdirectory(bindings/lua)
+set(LEAN_LIBS ${LEAN_LIBS} lua)
 set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}")
 set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage")
 set(EXTRA_LIBS ${LEAN_LIBS} ${EXTRA_LIBS})
 add_subdirectory(shell)
+add_subdirectory(shell/lua)
 add_subdirectory(tests/util)
 add_subdirectory(tests/util/numerics)
 add_subdirectory(tests/util/interval)

src/bindings/lua/CMakeLists.txt

@@ -0,0 +1 @@
+add_library(lua name.cpp)

src/bindings/lua/name.cpp

@@ -0,0 +1,88 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#ifdef LEAN_USE_LUA
+#include <lua.hpp>
+#include "util/debug.h"
+#include "util/name.h"
+
+namespace lean {
+static int name_gc(lua_State * L);
+static int name_tostring(lua_State * L);
+static int name_eq(lua_State * L);
+static int name_lt(lua_State * L);
+
+static const struct luaL_Reg name_m[] = {
+    {"__gc", name_gc}, {"__tostring", name_tostring}, {"__eq", name_eq}, {"__lt", name_lt}, {0, 0}
+};
+
+static int mk_name(lua_State * L) {
+    int nargs = lua_gettop(L);
+    if (nargs != 1 && nargs != 2)
+        return luaL_error(L, "function 'name' expects 1 or 2 arguments");
+    if (nargs == 1) {
+        char const * str = luaL_checkstring(L, 1);
+        void * mem = lua_newuserdata(L, sizeof(name));
+        new (mem) name(str);
+    } else {
+        lean_assert(nargs == 2);
+        name * prefix;
+        if (lua_isstring(L, 1)) {
+            char const * str = luaL_checkstring(L, 1);
+            prefix = new name(str);
+        } else {
+            prefix = static_cast<name*>(luaL_checkudata(L, 1, "name.mt"));
+        }
+        if (lua_isstring(L, 2)) {
+            char const * str = luaL_checkstring(L, 2);
+            void * mem = lua_newuserdata(L, sizeof(name));
+            new (mem) name(*prefix, str);
+        } else {
+            int idx = luaL_checkinteger(L, 2);
+            void * mem = lua_newuserdata(L, sizeof(name));
+            new (mem) name(*prefix, idx);
+        }
+    }
+    luaL_getmetatable(L, "name.mt");
+    lua_setmetatable(L, -2);
+    return 1;
+}
+
+static int name_gc(lua_State * L) {
+    name * n = static_cast<name*>(luaL_checkudata(L, 1, "name.mt"));
+    n->~name();
+    return 0;
+}
+
+static int name_tostring(lua_State * L) {
+    name * n = static_cast<name*>(luaL_checkudata(L, 1, "name.mt"));
+    lua_pushfstring(L, n->to_string().c_str());
+    return 1;
+}
+
+static int name_eq(lua_State * L) {
+    name * n1 = static_cast<name*>(luaL_checkudata(L, 1, "name.mt"));
+    name * n2 = static_cast<name*>(luaL_checkudata(L, 2, "name.mt"));
+    lua_pushboolean(L, *n1 == *n2);
+    return 1;
+}
+
+static int name_lt(lua_State * L) {
+    name * n1 = static_cast<name*>(luaL_checkudata(L, 1, "name.mt"));
+    name * n2 = static_cast<name*>(luaL_checkudata(L, 2, "name.mt"));
+    lua_pushboolean(L, *n1 < *n2);
+    return 1;
+}
+
+void init_name(lua_State * L) {
+    luaL_newmetatable(L, "name.mt");
+    luaL_setfuncs(L, name_m, 0);
+
+    lua_pushcfunction(L, mk_name);
+    lua_setglobal(L, "name");
+}
+}
+#endif

src/bindings/lua/name.h

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#ifdef LEAN_USE_LUA
+#include <lua.hpp>
+namespace lean {
+void init_name(lua_State * L);
+}
+#endif

src/shell/lua/CMakeLists.txt

@@ -0,0 +1,2 @@
+add_executable(leanlua leanlua.cpp)
+target_link_libraries(leanlua ${EXTRA_LIBS})

src/shell/lua/leanlua.cpp

@@ -0,0 +1,41 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#ifdef LEAN_USE_LUA
+#include <lua.hpp>
+#include <iostream>
+#include <cstdlib>
+#include "bindings/lua/name.h"
+
+int main(int argc, char ** argv) {
+    int status, result;
+    lua_State *L;
+
+    L = luaL_newstate();
+    luaL_openlibs(L);
+    lean::init_name(L);
+
+    for (int i = 1; i < argc; i++) {
+        status = luaL_loadfile(L, argv[i]);
+        if (status) {
+            std::cerr << "Couldn't load file: " << lua_tostring(L, -1) << "\n";
+            return 1;
+        }
+        result = lua_pcall(L, 0, LUA_MULTRET, 0);
+        if (result) {
+            std::cerr << "Failed to run script: " << lua_tostring(L, -1) << "\n";
+            return 1;
+        }
+    }
+    lua_close(L);
+    return 0;
+}
+#else
+int main() {
+    std::cerr << "Lean was compiled without Lua support\n";
+    return 1;
+}
+#endif

tests/lua/n1.lua

@@ -0,0 +1,7 @@
+n = name("foo", 1)
+print(n)
+print(name(n, "bla"))
+print(n == name("foo", 1))
+print(n == name("foo", 2))
+print(n < name("foo", 2))
+print(n < name("foo", 0))