refactor(lua): move lua_ref to separate file

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

src/bindings/lua/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_library(lua util.cpp lua_exception.cpp name.cpp numerics.cpp
-splay_map.cpp options.cpp sexpr.cpp format.cpp level.cpp
+lua_ref.cpp splay_map.cpp options.cpp sexpr.cpp format.cpp level.cpp
 local_context.cpp expr.cpp context.cpp object.cpp environment.cpp
 formatter.cpp state.cpp leanlua_state.cpp)
 

src/bindings/lua/lua_ref.cpp

@@ -0,0 +1,74 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/debug.h"
+#include "bindings/lua/util.h"
+#include "bindings/lua/lua_ref.h"
+
+namespace lean {
+lua_ref::lua_ref(lua_State * L, int i) {
+    lean_assert(L);
+    m_state = L;
+    lua_pushvalue(m_state, i);
+    m_ref   = luaL_ref(m_state, LUA_REGISTRYINDEX);
+}
+
+lua_ref::lua_ref(lua_ref const & r) {
+    m_state = r.m_state;
+    if (m_state) {
+        r.push();
+        m_ref   = luaL_ref(m_state, LUA_REGISTRYINDEX);
+    }
+}
+
+lua_ref::lua_ref(lua_ref && r) {
+    m_state = r.m_state;
+    m_ref   = r.m_ref;
+    r.m_state = nullptr;
+}
+
+lua_ref::~lua_ref() {
+    if (m_state)
+        luaL_unref(m_state, LUA_REGISTRYINDEX, m_ref);
+}
+
+lua_ref & lua_ref::operator=(lua_ref const & r) {
+    if (m_ref == r.m_ref)
+        return *this;
+    if (m_state)
+        luaL_unref(m_state, LUA_REGISTRYINDEX, m_ref);
+    m_state = r.m_state;
+    if (m_state) {
+        r.push();
+        m_ref   = luaL_ref(m_state, LUA_REGISTRYINDEX);
+    }
+    return *this;
+}
+
+void lua_ref::push() const {
+    lean_assert(m_state);
+    lua_rawgeti(m_state, LUA_REGISTRYINDEX, m_ref);
+}
+
+int lua_ref_lt_proc::operator()(lua_ref const & r1, lua_ref const & r2) const {
+    lean_assert(r1.get_state() == r2.get_state());
+    lua_State * L = r1.get_state();
+    r1.push();
+    r2.push();
+    int r;
+    if (lessthan(L, -2, -1)) {
+        r = -1;
+    } else if (lessthan(L, -1, -2)) {
+        r = 1;
+    } else if (equal(L, -2, -1)) {
+        r = 0;
+    } else {
+        throw exception("'<' is not a total order for the elements inserted on the table");
+    }
+    lua_pop(L, 2);
+    return r;
+}
+}

src/bindings/lua/lua_ref.h

@@ -0,0 +1,36 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <lua.hpp>
+
+namespace lean {
+/**
+   \brief Reference to Lua object.
+*/
+class lua_ref {
+    lua_State * m_state;
+    int         m_ref;
+public:
+    lua_ref():m_state(nullptr) {}
+    /**
+       \brief Create a reference to the Lua object at position \c i on \c L stack.
+    */
+    lua_ref(lua_State * L, int i);
+    lua_ref(lua_ref const & r);
+    lua_ref(lua_ref && r);
+    ~lua_ref();
+    lua_ref & operator=(lua_ref const & r);
+    void push() const;
+    lua_State * get_state() const { return m_state; }
+};
+
+/**
+   \brief '<' functor for lua_ref.
+*/
+struct lua_ref_lt_proc {
+    int operator()(lua_ref const & r1, lua_ref const & r2) const;
+};
+}

src/bindings/lua/splay_map.cpp

@@ -7,91 +7,10 @@ Author: Leonardo de Moura
 #include <lua.hpp>
 #include "util/splay_map.h"
 #include "bindings/lua/util.h"
-
+#include "bindings/lua/lua_ref.h"
-#include "bindings/lua/expr.h"
-#include "library/expr_lt.h"
 
 namespace lean {
-/**
+typedef splay_map<lua_ref, lua_ref, lua_ref_lt_proc> lua_splay_map;
-   \brief Reference to Lua object.
-*/
-class lua_ref {
-    lua_State * m_state;
-    int         m_ref;
-public:
-    lua_ref():m_state(nullptr) {}
-
-    lua_ref(lua_State * L, int i) {
-        lean_assert(L);
-        m_state = L;
-        lua_pushvalue(m_state, i);
-        m_ref   = luaL_ref(m_state, LUA_REGISTRYINDEX);
-    }
-
-    lua_ref(lua_ref const & r) {
-        m_state = r.m_state;
-        if (m_state) {
-            r.push();
-            m_ref   = luaL_ref(m_state, LUA_REGISTRYINDEX);
-        }
-    }
-
-    lua_ref(lua_ref && r) {
-        m_state = r.m_state;
-        m_ref   = r.m_ref;
-        r.m_state = nullptr;
-    }
-
-    ~lua_ref() {
-        if (m_state)
-            luaL_unref(m_state, LUA_REGISTRYINDEX, m_ref);
-    }
-
-    lua_ref & operator=(lua_ref const & r) {
-        if (m_ref == r.m_ref)
-            return *this;
-        if (m_state)
-            luaL_unref(m_state, LUA_REGISTRYINDEX, m_ref);
-        m_state = r.m_state;
-        if (m_state) {
-            r.push();
-            m_ref   = luaL_ref(m_state, LUA_REGISTRYINDEX);
-        }
-        return *this;
-    }
-
-    void push() const {
-        lean_assert(m_state);
-        lua_rawgeti(m_state, LUA_REGISTRYINDEX, m_ref);
-    }
-
-    lua_State * get_state() const {
-        return m_state;
-    }
-};
-
-struct lua_lt_proc {
-    int operator()(lua_ref const & r1, lua_ref const & r2) const {
-        lean_assert(r1.get_state() == r2.get_state());
-        lua_State * L = r1.get_state();
-        r1.push();
-        r2.push();
-        int r;
-        if (lessthan(L, -2, -1)) {
-            r = -1;
-        } else if (lessthan(L, -1, -2)) {
-            r = 1;
-        } else if (equal(L, -2, -1)) {
-            r = 0;
-        } else {
-            throw exception("'<' is not a total order for the elements inserted on the table");
-        }
-        lua_pop(L, 2);
-        return r;
-    }
-};
-
-typedef splay_map<lua_ref, lua_ref, lua_lt_proc> lua_splay_map;
 
 constexpr char const * splay_map_mt = "splay_map.mt";