refactor(lua): remove duplicate code, separate lua_exception, add missing #pragma once

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

src/bindings/lua/CMakeLists.txt

@@ -1,4 +1,4 @@
-add_library(lua util.cpp name.cpp numerics.cpp options.cpp sexpr.cpp
+add_library(lua util.cpp lua_exception.cpp name.cpp numerics.cpp options.cpp sexpr.cpp
 format.cpp expr.cpp leanlua_state.cpp)
 
 target_link_libraries(lua ${LEAN_LIBS})

src/bindings/lua/expr.cpp

@@ -119,65 +119,43 @@ static std::pair<expr, expr> get_expr_pair_from_table(lua_State * L, int t, int
     return mk_pair(ai, bi);
 }
 
-static int expr_fun(lua_State * L) {
+typedef expr (*MkAbst1)(expr const & n, expr const & t, expr const & b);
+typedef expr (*MkAbst2)(name const & n, expr const & t, expr const & b);
+
+template<MkAbst1 F1, MkAbst2 F2>
+int expr_abst(lua_State * L, char const * fname) {
     int nargs = lua_gettop(L);
     if (nargs < 2)
-        luaL_error(L, "Lean fun must have at least 2 arguments");
+        luaL_error(L, "Lean %s must have at least 2 arguments", fname);
     if (nargs == 2) {
         if (!lua_istable(L, 1))
-            luaL_error(L, "Lean fun expects arg #1 to be of the form '{{expr, expr}, ...}'");
+            luaL_error(L, "Lean %s expects arg #1 to be of the form '{{expr, expr}, ...}'", fname);
         int len = objlen(L, 1);
         if (len == 0)
-            luaL_error(L, "Lean fun expects arg #1 to be non-empty table");
+            luaL_error(L, "Lean %s expects arg #1 to be non-empty table", fname);
         expr r = to_expr(L, 2);
         for (int i = len; i >= 1; i--) {
             auto p = get_expr_pair_from_table(L, 1, i);
-            r = Fun(p.first, p.second, r);
+            r = F1(p.first, p.second, r);
         }
         return push_expr(L, r);
     } else {
         if (nargs % 2 == 0)
-            luaL_error(L, "Lean fun must have an odd number of arguments");
+            luaL_error(L, "Lean %s must have an odd number of arguments", fname);
         expr r = to_expr(L, nargs);
         for (int i = nargs - 1; i >= 1; i-=2) {
             if (is_expr(L, i - 1))
-                r = Fun(to_expr(L, i - 1), to_expr(L, i), r);
+                r = F1(to_expr(L, i - 1), to_expr(L, i), r);
             else
-                r = Fun(to_name_ext(L, i - 1), to_expr(L, i), r);
+                r = F2(to_name_ext(L, i - 1), to_expr(L, i), r);
         }
         return push_expr(L, r);
     }
 }
 
-static int expr_pi(lua_State * L) {
-    int nargs = lua_gettop(L);
-    if (nargs < 2)
-        luaL_error(L, "Lean Pi must have at least 2 arguments");
-    if (nargs == 2) {
-        if (!lua_istable(L, 1))
-            luaL_error(L, "Lean Pi expects arg #1 to be of the form '{{expr, expr}, ...}'");
-        int len = objlen(L, 1);
-        if (len == 0)
-            luaL_error(L, "Lean Pi expects arg #1 to be non-empty table");
-        expr r = to_expr(L, 2);
-        for (int i = len; i >= 1; i--) {
-            auto p = get_expr_pair_from_table(L, 1, i);
-            r = Pi(p.first, p.second, r);
-        }
-        return push_expr(L, r);
-    } else {
-        if (nargs % 2 == 0)
-            luaL_error(L, "Lean Pi must have an odd number of arguments");
-        expr r = to_expr(L, nargs);
-        for (int i = nargs - 1; i >= 1; i-=2) {
-            if (is_expr(L, i - 1))
-                r = Pi(to_expr(L, i - 1), to_expr(L, i), r);
-            else
-                r = Pi(to_name_ext(L, i - 1), to_expr(L, i), r);
-        }
-        return push_expr(L, r);
-    }
-}
+static int expr_fun(lua_State * L) { return expr_abst<Fun, Fun>(L, "fun"); }
+static int expr_pi(lua_State * L)  { return expr_abst<Pi, Pi>(L, "Pi"); }
+static int expr_let(lua_State * L) { return expr_abst<Let, Let>(L, "Let"); }
 
 static const struct luaL_Reg expr_m[] = {
     {"__gc",       expr_gc}, // never throws
@@ -207,5 +185,6 @@ void open_expr(lua_State * L) {
     set_global_function<expr_fun>(L, "fun");
     set_global_function<expr_fun>(L, "Fun");
     set_global_function<expr_pi>(L, "Pi");
+    set_global_function<expr_let>(L, "Let");
 }
 }

src/bindings/lua/expr.h

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#pragma once
 #include <lua.hpp>
 namespace lean {
 class expr;

src/bindings/lua/format.h

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#pragma once
 #include <lua.hpp>
 namespace lean {
 class format;

src/bindings/lua/leanlua_state.cpp

@@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <iostream>
-#include <sstream>
 #include <mutex>
 #include <string>
 #include <lua.hpp>
@@ -13,6 +12,7 @@ Author: Leonardo de Moura
 #include "util/exception.h"
 #include "util/memory.h"
 #include "bindings/lua/leanlua_state.h"
+#include "bindings/lua/util.h"
 #include "bindings/lua/name.h"
 #include "bindings/lua/numerics.h"
 #include "bindings/lua/options.h"
@@ -49,26 +49,14 @@ struct leanlua_state::imp {
         lua_close(m_state);
     }
 
-    void exec() {
-        int result = lua_pcall(m_state, 0, LUA_MULTRET, 0);
-        if (result)
-            throw lua_exception(lua_tostring(m_state, -1));
-    }
-
     void dofile(char const * fname) {
         std::lock_guard<std::mutex> lock(m_mutex);
-        int result = luaL_loadfile(m_state, fname);
-        if (result)
-            throw lua_exception(lua_tostring(m_state, -1));
-        exec();
+        ::lean::dofile(m_state, fname);
     }
 
     void dostring(char const * str) {
         std::lock_guard<std::mutex> lock(m_mutex);
-        int result = luaL_loadstring(m_state, str);
-        if (result)
-            throw lua_exception(lua_tostring(m_state, -1));
-        exec();
+        ::lean::dostring(m_state, str);
     }
 };
 
@@ -86,71 +74,4 @@ void leanlua_state::dofile(char const * fname) {
 void leanlua_state::dostring(char const * str) {
     m_ptr->dostring(str);
 }
-
-lua_exception::lua_exception(char const * lua_error):exception("") {
-    lean_assert(lua_error);
-    std::string fname;
-    std::string line;
-    std::string msg;
-    int state = 0;
-    char const * it = lua_error;
-    while (*it) {
-        if (state == 0) {
-            if (*it == ':') {
-                state = 1;
-            } else {
-                fname += *it;
-            }
-        } else if (state == 1) {
-            if (*it == ':') {
-                state = 2;
-            } else {
-                line += *it;
-            }
-        } else {
-            msg += *it;
-        }
-        it++;
-    }
-    if (state != 2) {
-        // failed to decode Lua error message
-        m_source = source::Unknown;
-        m_msg = lua_error;
-    } else {
-        if (fname == "[string \"...\"]") {
-            m_source = source::String;
-        } else {
-            m_source = source::File;
-            m_file   = fname;
-        }
-        m_line   = atoi(line.c_str());
-        m_msg = msg;
-    }
-}
-
-char const * lua_exception::get_filename() const {
-    lean_assert(get_source() == source::File);
-    return m_file.c_str();
-}
-
-unsigned lua_exception::get_line() const {
-    lean_assert(get_source() != source::Unknown);
-    return m_line;
-}
-
-char const * lua_exception::msg() const noexcept {
-    return exception::what();
-}
-
-char const * lua_exception::what() const noexcept {
-    static thread_local std::string buffer;
-    std::ostringstream strm;
-    switch (m_source) {
-    case source::String:  strm << "[string]:" << m_line << ":" << msg() << "\n"; break;
-    case source::File:    strm << m_file << ":" << m_line << ":" << msg() << "\n"; break;
-    case source::Unknown: return msg();
-    }
-    buffer = strm.str();
-    return buffer.c_str();
-}
 }

src/bindings/lua/leanlua_state.h

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#pragma once
 #include <memory>
-#include <string>
-#include "util/exception.h"
+#include "bindings/lua/lua_exception.h"
 
 namespace lean {
 /**
@@ -30,24 +30,4 @@ public:
     */
     void dostring(char const * str);
 };
-
-/**
-   \brief Exception for wrapping errors produced by the Lua engine.
-*/
-class lua_exception : public exception {
-public:
-    enum class source { String, File, Unknown };
-private:
-    source      m_source;
-    std::string m_file;   // if source == File, then this field contains the filename that triggered the error.
-    unsigned    m_line;   // line number
-public:
-    lua_exception(char const * lua_error);
-    source get_source() const { return m_source; }
-    char const * get_filename() const;
-    unsigned get_line() const;
-    /** \brief Return error message without position information */
-    char const * msg() const noexcept;
-    virtual char const * what() const noexcept;
-};
 }

src/bindings/lua/lua_exception.cpp

@@ -0,0 +1,79 @@
+/*
+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 <sstream>
+#include <string>
+#include "util/debug.h"
+#include "bindings/lua/lua_exception.h"
+
+namespace lean {
+lua_exception::lua_exception(char const * lua_error):exception("") {
+    lean_assert(lua_error);
+    std::string fname;
+    std::string line;
+    std::string msg;
+    int state = 0;
+    char const * it = lua_error;
+    while (*it) {
+        if (state == 0) {
+            if (*it == ':') {
+                state = 1;
+            } else {
+                fname += *it;
+            }
+        } else if (state == 1) {
+            if (*it == ':') {
+                state = 2;
+            } else {
+                line += *it;
+            }
+        } else {
+            msg += *it;
+        }
+        it++;
+    }
+    if (state != 2) {
+        // failed to decode Lua error message
+        m_source = source::Unknown;
+        m_msg = lua_error;
+    } else {
+        if (fname == "[string \"...\"]") {
+            m_source = source::String;
+        } else {
+            m_source = source::File;
+            m_file   = fname;
+        }
+        m_line   = atoi(line.c_str());
+        m_msg = msg;
+    }
+}
+
+char const * lua_exception::get_filename() const {
+    lean_assert(get_source() == source::File);
+    return m_file.c_str();
+}
+
+unsigned lua_exception::get_line() const {
+    lean_assert(get_source() != source::Unknown);
+    return m_line;
+}
+
+char const * lua_exception::msg() const noexcept {
+    return exception::what();
+}
+
+char const * lua_exception::what() const noexcept {
+    static thread_local std::string buffer;
+    std::ostringstream strm;
+    switch (m_source) {
+    case source::String:  strm << "[string]:" << m_line << ":" << msg() << "\n"; break;
+    case source::File:    strm << m_file << ":" << m_line << ":" << msg() << "\n"; break;
+    case source::Unknown: return msg();
+    }
+    buffer = strm.str();
+    return buffer.c_str();
+}
+}

src/bindings/lua/lua_exception.h

@@ -0,0 +1,31 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <string>
+#include "util/exception.h"
+
+namespace lean {
+/**
+   \brief Exception for wrapping errors produced by the Lua engine.
+*/
+class lua_exception : public exception {
+public:
+    enum class source { String, File, Unknown };
+private:
+    source      m_source;
+    std::string m_file;   // if source == File, then this field contains the filename that triggered the error.
+    unsigned    m_line;   // line number
+public:
+    lua_exception(char const * lua_error);
+    source get_source() const { return m_source; }
+    char const * get_filename() const;
+    unsigned get_line() const;
+    /** \brief Return error message without position information */
+    char const * msg() const noexcept;
+    virtual char const * what() const noexcept;
+};
+}

src/bindings/lua/name.h

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#pragma once
 #include <lua.hpp>
 namespace lean {
 class name;

src/bindings/lua/numerics.h

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#pragma once
 #include <lua.hpp>
 namespace lean {
 class mpz;

src/bindings/lua/options.h

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#pragma once
 #include <lua.hpp>
 namespace lean {
 class options;

src/bindings/lua/sexpr.h

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#pragma once
 #include <lua.hpp>
 namespace lean {
 class sexpr;

src/bindings/lua/util.cpp

@@ -5,10 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <lua.hpp>
-#include <exception>
 #include <string>
-#include "util/exception.h"
-#include "util/debug.h"
+#include "bindings/lua/util.h"
+#include "bindings/lua/lua_exception.h"
 
 namespace lean {
 /**
@@ -51,6 +50,26 @@ size_t objlen(lua_State * L, int idx) {
     #endif
 }
 
+static void exec(lua_State * L) {
+    int result = lua_pcall(L, 0, LUA_MULTRET, 0);
+    if (result)
+        throw lua_exception(lua_tostring(L, -1));
+}
+
+void dofile(lua_State * L, char const * fname) {
+    int result = luaL_loadfile(L, fname);
+    if (result)
+        throw lua_exception(lua_tostring(L, -1));
+    exec(L);
+}
+
+void dostring(lua_State * L, char const * str) {
+    int result = luaL_loadstring(L, str);
+    if (result)
+        throw lua_exception(lua_tostring(L, -1));
+    exec(L);
+}
+
 int safe_function_wrapper(lua_State * L, lua_CFunction f){
     static thread_local std::string _error_msg;
     char const * error_msg;

src/bindings/lua/util.h

@@ -4,11 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#pragma once
 #include <lua.hpp>
+
 namespace lean {
 void setfuncs(lua_State * L, luaL_Reg const * l, int nup);
 bool testudata(lua_State * L, int idx, char const * mt);
 size_t objlen(lua_State * L, int idx);
+void dofile(lua_State * L, char const * fname);
+void dostring(lua_State * L, char const * str);
 /**
    \brief Wrapper for invoking function f, and catching Lean exceptions.
 */