From 05f254f605c6664a18d44866008faca95afff113 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 14 Nov 2013 14:41:54 -0800 Subject: [PATCH] refactor(lua): move lua_ref to separate file Signed-off-by: Leonardo de Moura --- src/bindings/lua/CMakeLists.txt | 2 +- src/bindings/lua/lua_ref.cpp | 74 ++++++++++++++++++++++++++++ src/bindings/lua/lua_ref.h | 36 ++++++++++++++ src/bindings/lua/splay_map.cpp | 85 +-------------------------------- 4 files changed, 113 insertions(+), 84 deletions(-) create mode 100644 src/bindings/lua/lua_ref.cpp create mode 100644 src/bindings/lua/lua_ref.h diff --git a/src/bindings/lua/CMakeLists.txt b/src/bindings/lua/CMakeLists.txt index 0ec167bf5..200273892 100644 --- a/src/bindings/lua/CMakeLists.txt +++ b/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) diff --git a/src/bindings/lua/lua_ref.cpp b/src/bindings/lua/lua_ref.cpp new file mode 100644 index 000000000..112d8eb8e --- /dev/null +++ b/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; +} +} diff --git a/src/bindings/lua/lua_ref.h b/src/bindings/lua/lua_ref.h new file mode 100644 index 000000000..7f65817b4 --- /dev/null +++ b/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 + +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; +}; +} diff --git a/src/bindings/lua/splay_map.cpp b/src/bindings/lua/splay_map.cpp index 864d9b794..5c20bc6c8 100644 --- a/src/bindings/lua/splay_map.cpp +++ b/src/bindings/lua/splay_map.cpp @@ -7,91 +7,10 @@ Author: Leonardo de Moura #include #include "util/splay_map.h" #include "bindings/lua/util.h" - -#include "bindings/lua/expr.h" -#include "library/expr_lt.h" +#include "bindings/lua/lua_ref.h" namespace lean { -/** - \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_splay_map; +typedef splay_map lua_splay_map; constexpr char const * splay_map_mt = "splay_map.mt";