feat(frontends/lean): add support for embedded Lua scripts in Lean files

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

src/CMakeLists.txt

@@ -154,10 +154,10 @@ add_subdirectory(library/rewriter)
 set(LEAN_LIBS ${LEAN_LIBS} rewriter)
 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)
+add_subdirectory(frontends/lean)
+set(LEAN_LIBS ${LEAN_LIBS} lean_frontend)
 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})

src/bindings/lua/CMakeLists.txt

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

src/bindings/lua/leanlua_state.cpp

@@ -0,0 +1,92 @@
+/*
+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 <iostream>
+#include "bindings/lua/leanlua_state.h"
+
+#ifdef LEAN_USE_LUA
+#include <lua.hpp>
+#include <mutex>
+#include "util/exception.h"
+#include "bindings/lua/name.h"
+#include "bindings/lua/numerics.h"
+#include "bindings/lua/options.h"
+#include "bindings/lua/sexpr.h"
+
+namespace lean {
+struct leanlua_state::imp {
+    lua_State * m_state;
+    std::mutex  m_mutex;
+    imp() {
+        m_state = luaL_newstate();
+        luaL_openlibs(m_state);
+        lean::open_name(m_state);
+        lean::open_mpz(m_state);
+        lean::open_mpq(m_state);
+        lean::open_options(m_state);
+        lean::open_sexpr(m_state);
+    }
+    ~imp() {
+        lua_close(m_state);
+    }
+
+    void exec() {
+        int result = lua_pcall(m_state, 0, LUA_MULTRET, 0);
+        if (result)
+            throw 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 exception(lua_tostring(m_state, -1));
+        exec();
+    }
+
+    void dostring(char const * str) {
+        std::lock_guard<std::mutex> lock(m_mutex);
+        int result = luaL_loadstring(m_state, str);
+        if (result)
+            throw exception(lua_tostring(m_state, -1));
+        exec();
+    }
+};
+
+leanlua_state::leanlua_state():
+    m_ptr(new imp()) {
+}
+
+leanlua_state::~leanlua_state() {
+}
+
+void leanlua_state::dofile(char const * fname) {
+    m_ptr->dofile(fname);
+}
+
+void leanlua_state::dostring(char const * str) {
+    m_ptr->dostring(str);
+}
+}
+#else
+leanlua_state::leanlua_state() {
+}
+
+leanlua_state::~leanlua_state() {
+}
+
+[[ noreturn ]] void throw_lua_not_supported() {
+    throw exception("Lean was compiled without Lua support");
+}
+
+void leanlua_state::dofile(char const * fname) {
+    throw_lua_not_supported();
+}
+
+void leanlua_state::dostring(char const * str) {
+    throw_lua_not_supported();
+}
+#endif

src/bindings/lua/leanlua_state.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
+*/
+#include <memory>
+
+namespace lean {
+/**
+   \brief Wrapper for lua_State objects which contains all Lean bindings.
+*/
+class leanlua_state {
+    struct imp;
+    std::shared_ptr<imp> m_ptr;
+public:
+    leanlua_state();
+    ~leanlua_state();
+
+    /**
+       \brief Execute the file with the given name.
+       This method throws an exception if an error occurs.
+    */
+    void dofile(char const * fname);
+    /**
+       \brief Execute the given string.
+       This method throws an exception if an error occurs.
+    */
+    void dostring(char const * str);
+};
+}

src/frontends/lean/parser.cpp

@@ -37,6 +37,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/scanner.h"
 #include "frontends/lean/notation.h"
 #include "frontends/lean/pp.h"
+#include "bindings/lua/leanlua_state.h"
 
 #ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS
 #define LEAN_DEFAULT_PARSER_SHOW_ERRORS true
@@ -132,6 +133,8 @@ class parser::imp {
     interruptable_ptr<parser>     m_import_parser;
     interruptable_ptr<normalizer> m_normalizer;
 
+    leanlua_state *     m_leanlua_state;
+
     bool                m_verbose;
     bool                m_show_errors;
 
@@ -1398,7 +1401,7 @@ class parser::imp {
         try {
             if (m_verbose)
                 regular(m_frontend) << "Importing file '" << fname << "'" << endl;
-            parser import_parser(m_frontend, in, true /* use exceptions */, false /* not interactive */);
+            parser import_parser(m_frontend, in, m_leanlua_state, true /* use exceptions */, false /* not interactive */);
             scoped_set_interruptable_ptr<parser> set(m_import_parser, &import_parser);
             import_parser();
         } catch (interrupted &) {
@@ -1562,13 +1565,21 @@ class parser::imp {
             next();
     }
 
+    void parse_script() {
+        if (!m_leanlua_state)
+            throw exception("failed to execute Lua script, parser does not have a Lua interpreter");
+        m_leanlua_state->dostring(m_scanner.get_str_val().c_str());
+        next();
+    }
+
 public:
-    imp(frontend & fe, std::istream & in, bool use_exceptions, bool interactive):
+    imp(frontend & fe, std::istream & in, leanlua_state * S, bool use_exceptions, bool interactive):
         m_frontend(fe),
         m_scanner(in),
         m_elaborator(fe),
         m_use_exceptions(use_exceptions),
         m_interactive(interactive) {
+        m_leanlua_state = S;
         updt_options();
         m_found_errors = false;
         m_num_local_decls = 0;
@@ -1592,9 +1603,10 @@ public:
         while (true) {
             try {
                 switch (curr()) {
-                case scanner::token::CommandId: parse_command(); break;
-                case scanner::token::Period: show_prompt(); next(); break;
-                case scanner::token::Eof: return !m_found_errors;
+                case scanner::token::CommandId:   parse_command(); break;
+                case scanner::token::ScriptBlock: parse_script(); break;
+                case scanner::token::Period:      show_prompt(); next(); break;
+                case scanner::token::Eof:         return !m_found_errors;
                 default:
                     throw parser_error("Command expected", pos());
                 }
@@ -1655,9 +1667,9 @@ public:
     }
 };
 
-parser::parser(frontend & fe, std::istream & in, bool use_exceptions, bool interactive) {
+parser::parser(frontend & fe, std::istream & in, leanlua_state * S, bool use_exceptions, bool interactive) {
     parser::imp::show_prompt(interactive, fe);
-    m_ptr.reset(new imp(fe, in, use_exceptions, interactive));
+    m_ptr.reset(new imp(fe, in, S, use_exceptions, interactive));
 }
 
 parser::~parser() {
@@ -1675,7 +1687,7 @@ expr parser::parse_expr() {
     return m_ptr->parse_expr_main();
 }
 
-shell::shell(frontend & fe):m_frontend(fe) {
+shell::shell(frontend & fe, leanlua_state * S):m_frontend(fe), m_leanlua_state(S) {
 }
 
 shell::~shell() {
@@ -1691,7 +1703,7 @@ bool shell::operator()() {
         add_history(input);
         std::istringstream strm(input);
         {
-            parser p(m_frontend, strm, false, false);
+            parser p(m_frontend, strm, m_leanlua_state, false, false);
             scoped_set_interruptable_ptr<parser> set(m_parser, &p);
             if (!p())
                 errors = true;
@@ -1699,7 +1711,7 @@ bool shell::operator()() {
         free(input);
     }
 #else
-    parser p(m_frontend, std::cin, false, true);
+    parser p(m_frontend, std::cin, m_leanlua_state, false, true);
     scoped_set_interruptable_ptr<parser> set(m_parser, &p);
     return p();
 #endif

src/frontends/lean/parser.h

@@ -10,12 +10,13 @@ Author: Leonardo de Moura
 #include "frontends/lean/frontend.h"
 
 namespace lean {
+class leanlua_state;
 /** \brief Functional object for parsing commands and expressions */
 class parser {
     class imp;
     std::unique_ptr<imp> m_ptr;
 public:
-    parser(frontend & fe, std::istream & in, bool use_exceptions = true, bool interactive = false);
+    parser(frontend & fe, std::istream & in, leanlua_state * S, bool use_exceptions = true, bool interactive = false);
     ~parser();
 
     /** \brief Parse a sequence of commands */
@@ -32,9 +33,10 @@ public:
 /** \brief Implements the Read Eval Print loop */
 class shell {
     frontend &                m_frontend;
+    leanlua_state *           m_leanlua_state;
     interruptable_ptr<parser> m_parser;
 public:
-    shell(frontend & fe);
+    shell(frontend & fe, leanlua_state * S);
     ~shell();
 
     bool operator()();
@@ -44,10 +46,10 @@ public:
     void reset_interrupt() { set_interrupt(false); }
 };
 
-inline bool parse_commands(frontend & fe, std::istream & in, bool use_exceptions = true, bool interactive = false) {
-    return parser(fe, in, use_exceptions, interactive)();
+inline bool parse_commands(frontend & fe, std::istream & in, leanlua_state * S = nullptr, bool use_exceptions = true, bool interactive = false) {
+    return parser(fe, in, S, use_exceptions, interactive)();
 }
 inline expr parse_expr(frontend & fe, std::istream & in) {
-    return parser(fe, in).parse_expr();
+    return parser(fe, in, nullptr).parse_expr();
 }
 }

src/frontends/lean/scanner.cpp

@@ -334,6 +334,56 @@ scanner::token scanner::read_string() {
     }
 }
 
+scanner::token scanner::read_script_block() {
+    lean_assert(curr() == '{');
+    next();
+    m_buffer.clear();
+    int num_open_blocks = 1;
+    while (true) {
+        char c = curr();
+        if (c == EOF) {
+            throw_exception("unexpected end of script");
+        } else if (c == '{') {
+            m_buffer += '{';
+            next();
+            c = curr();
+            if (c == '{')
+                num_open_blocks++;
+            else if (c == '\n')
+                new_line();
+            else if (c == EOF)
+                throw_exception("unexpected end of script");
+            m_buffer += c;
+            next();
+        } else if (c == '}') {
+            next();
+            char c2 = curr();
+            if (c2 == '}') {
+                next();
+                num_open_blocks--;
+                if (num_open_blocks == 0)
+                    return token::ScriptBlock;
+            } else if (c2 == '\n') {
+                new_line();
+                next();
+            } else if (c2 == EOF) {
+                throw_exception("unexpected end of script");
+            } else {
+                next();
+            }
+            m_buffer += c;
+            m_buffer += c2;
+        } else if (c == '\n') {
+            new_line();
+            m_buffer += '\n';
+            next();
+        } else {
+            m_buffer += c;
+            next();
+        }
+    }
+}
+
 scanner::token scanner::scan() {
     while (true) {
         char c = curr();
@@ -359,7 +409,12 @@ scanner::token scanner::scan() {
                 return token::LeftParen;
             }
         case ')':  next(); return token::RightParen;
-        case '{':  next(); return token::LeftCurlyBracket;
+        case '{':
+            next();
+            if (curr() == '{')
+                return read_script_block();
+            else
+                return token::LeftCurlyBracket;
         case '}':  next(); return token::RightCurlyBracket;
         case 'a':  return read_a_symbol();
         case 'b':  return read_b_symbol();
@@ -397,6 +452,7 @@ std::ostream & operator<<(std::ostream & out, scanner::token const & t) {
     case scanner::token::Assign:            out << ":="; break;
     case scanner::token::Type:              out << "Type"; break;
     case scanner::token::Placeholder:       out << "_"; break;
+    case scanner::token::ScriptBlock:       out << "Script"; break;
     case scanner::token::Eof:               out << "EOF"; break;
     }
     return out;

src/frontends/lean/scanner.h

@@ -20,7 +20,8 @@ class scanner {
 public:
     enum class token {
         LeftParen, RightParen, LeftCurlyBracket, RightCurlyBracket, Colon, Comma, Period, Lambda, Pi, Arrow,
-        Let, In, Forall, Exists, Id, CommandId, NatVal, DecimalVal, StringVal, Eq, Assign, Type, Placeholder, Eof
+        Let, In, Forall, Exists, Id, CommandId, NatVal, DecimalVal, StringVal, Eq, Assign, Type, Placeholder,
+        ScriptBlock, Eof
     };
 protected:
     int                m_spos; // position in the current line of the stream
@@ -49,6 +50,7 @@ protected:
     token read_c_symbol();
     token read_number();
     token read_string();
+    token read_script_block();
     bool  is_command(name const & n) const;
 
 public:

src/shell/lean.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "util/interruptable_ptr.h"
 #include "kernel/printer.h"
 #include "frontends/lean/parser.h"
+#include "bindings/lua/leanlua_state.h"
 #include "version.h"
 
 using lean::interruptable_ptr;
@@ -17,6 +18,7 @@ using lean::shell;
 using lean::frontend;
 using lean::scoped_set_interruptable_ptr;
 using lean::parser;
+using lean::leanlua_state;
 
 static interruptable_ptr<shell> g_lean_shell;
 
@@ -28,7 +30,8 @@ bool lean_shell() {
     std::cout << "Lean (version " << LEAN_VERSION_MAJOR << "." << LEAN_VERSION_MINOR << ")\n";
     std::cout << "Type Ctrl-D to exit or 'Help.' for help."<< std::endl;
     frontend f;
-    shell sh(f);
+    leanlua_state S;
+    shell sh(f, &S);
     scoped_set_interruptable_ptr<shell> set(g_lean_shell, &sh);
     signal(SIGINT, on_ctrl_c);
     return sh();
@@ -40,9 +43,10 @@ int main(int argc, char ** argv) {
     } else {
         bool ok = true;
         frontend f;
+        leanlua_state S;
         for (int i = 1; i < argc; i++) {
             std::ifstream in(argv[i]);
-            parser p(f, in, false, false);
+            parser p(f, in, &S, false, false);
             if (!p())
                 ok = false;
         }

src/shell/lua/leanlua.cpp

@@ -5,46 +5,20 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <iostream>
-#include <cstdlib>
-
-#ifdef LEAN_USE_LUA
-#include <lua.hpp>
-#include "bindings/lua/name.h"
-#include "bindings/lua/numerics.h"
-#include "bindings/lua/options.h"
-#include "bindings/lua/sexpr.h"
+#include "util/exception.h"
+#include "bindings/lua/leanlua_state.h"
 
 int main(int argc, char ** argv) {
-    int status, result;
-    lua_State *L;
+    lean::leanlua_state S;
     int exitcode = 0;
-    L = luaL_newstate();
-    luaL_openlibs(L);
-    lean::open_name(L);
-    lean::open_mpz(L);
-    lean::open_mpq(L);
-    lean::open_options(L);
-    lean::open_sexpr(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";
+        try {
+            S.dofile(argv[i]);
+        } catch (lean::exception & ex) {
+            std::cerr << ex.what() << std::endl;
             exitcode = 1;
-        } else {
-            result = lua_pcall(L, 0, LUA_MULTRET, 0);
-            if (result) {
-                std::cerr << "Failed to run script: " << lua_tostring(L, -1) << "\n";
-                exitcode = 1;
-            }
         }
     }
-    lua_close(L);
     return exitcode;
 }
-#else
-int main() {
-    std::cerr << "Lean was compiled without Lua support\n";
-    return 1;
-}
-#endif

tests/lean/lua1.lean

@@ -0,0 +1,7 @@
+Variable x : Int
+
+{{
+print("hello world from Lua")
+}}
+
+Variable y : Int

tests/lean/lua1.lean.expected.out

@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: x
+hello world from Lua
+  Assumed: y