feat(library/script_evaluator): add abstract class that exposes only the API needed by frontend objects

The main motivation is to break the remove the dependency frontends/lean <-- bindings/lua.
This dependency is undesirable because we want to expose the frontends/lean parser and pretty printer objects at bindings/lua.

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

src/CMakeLists.txt

@@ -156,10 +156,10 @@ add_subdirectory(library/rewriter)
 set(LEAN_LIBS ${LEAN_LIBS} rewriter)
 add_subdirectory(library/elaborator)
 set(LEAN_LIBS ${LEAN_LIBS} elaborator)
-add_subdirectory(bindings/lua)
-set(LEAN_LIBS ${LEAN_LIBS} lua)
 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})

src/bindings/lua/leanlua_state.cpp

@@ -178,14 +178,10 @@ struct leanlua_state::imp {
         ::lean::dostring(m_state, str);
     }
 
-    void dostring(char const * str, environment & env) {
-        set_environment set(m_state, env);
-        dostring(str);
-    }
-
     void dostring(char const * str, environment & env, state & st) {
-        set_state set(m_state, st);
-        dostring(str, env);
+        set_state       set1(m_state, st);
+        set_environment set2(m_state, env);
+        dostring(str);
     }
 };
 
@@ -204,10 +200,6 @@ void leanlua_state::dostring(char const * str) {
     m_ptr->dostring(str);
 }
 
-void leanlua_state::dostring(char const * str, environment & env) {
-    m_ptr->dostring(str, env);
-}
-
 void leanlua_state::dostring(char const * str, environment & env, state & st) {
     m_ptr->dostring(str, env, st);
 }

src/bindings/lua/leanlua_state.h

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <memory>
 #include <lua.hpp>
+#include "library/script_evaluator.h"
 #include "bindings/lua/lua_exception.h"
 
 namespace lean {
@@ -15,7 +16,7 @@ class state;
 /**
    \brief Wrapper for lua_State objects which contains all Lean bindings.
 */
-class leanlua_state {
+class leanlua_state : public script_evaluator {
     struct imp;
     std::shared_ptr<imp> m_ptr;
     friend class leanlua_thread;
@@ -26,7 +27,7 @@ class leanlua_state {
     friend int thread_wait(lua_State * L);
 public:
     leanlua_state();
-    ~leanlua_state();
+    virtual ~leanlua_state();
 
     /**
        \brief Execute the file with the given name.
@@ -37,15 +38,13 @@ public:
        \brief Execute the given string.
        This method throws an exception if an error occurs.
     */
-    void dostring(char const * str);
+    virtual void dostring(char const * str);
 
     /**
        \brief Execute the given script, but sets the registry with the given environment object.
        The registry can be accessed by \str by invoking the function <tt>env()</tt>.
        The script \c str should not store a reference to the environment \c env.
     */
-    void dostring(char const * str, environment & env);
-
-    void dostring(char const * str, environment & env, state & st);
+    virtual void dostring(char const * str, environment & env, state & st);
 };
 }

src/bindings/lua/lua_exception.cpp

@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 #include "bindings/lua/lua_exception.h"
 
 namespace lean {
-lua_exception::lua_exception(char const * lua_error):exception("") {
+lua_exception::lua_exception(char const * lua_error):script_exception() {
     lean_assert(lua_error);
     std::string fname;
     std::string line;
@@ -52,6 +52,9 @@ lua_exception::lua_exception(char const * lua_error):exception("") {
     }
 }
 
+lua_exception::~lua_exception() {
+}
+
 char const * lua_exception::get_filename() const {
     lean_assert(get_source() == source::File);
     return m_file.c_str();
@@ -62,19 +65,7 @@ unsigned lua_exception::get_line() const {
     return m_line;
 }
 
-char const * lua_exception::msg() const noexcept {
+char const * lua_exception::get_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

@@ -7,25 +7,24 @@ Author: Leonardo de Moura
 #pragma once
 #include <string>
 #include "util/exception.h"
+#include "library/script_evaluator.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 };
+class lua_exception : public script_exception {
 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;
+    virtual ~lua_exception();
+    virtual source get_source() const { return m_source; }
+    virtual char const * get_filename() const;
+    virtual unsigned get_line() const;
     /** \brief Return error message without position information */
-    char const * msg() const noexcept;
-    virtual char const * what() const noexcept;
+    virtual char const * get_msg() const noexcept;
 };
 }

src/frontends/lean/parser.cpp

@@ -31,6 +31,7 @@ Author: Leonardo de Moura
 #include "library/arith/arith.h"
 #include "library/state.h"
 #include "library/placeholder.h"
+#include "library/script_evaluator.h"
 #include "library/elaborator/elaborator_exception.h"
 #include "frontends/lean/frontend.h"
 #include "frontends/lean/frontend_elaborator.h"
@@ -38,7 +39,6 @@ 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
@@ -131,7 +131,7 @@ class parser::imp {
     pos_info            m_last_cmd_pos;
     pos_info            m_last_script_pos;
 
-    leanlua_state *     m_leanlua_state;
+    script_evaluator *  m_script_evaluator;
 
     bool                m_verbose;
     bool                m_show_errors;
@@ -1398,7 +1398,7 @@ class parser::imp {
         try {
             if (m_verbose)
                 regular(m_frontend) << "Importing file '" << fname << "'" << endl;
-            parser import_parser(m_frontend, in, m_leanlua_state, true /* use exceptions */, false /* not interactive */);
+            parser import_parser(m_frontend, in, m_script_evaluator, true /* use exceptions */, false /* not interactive */);
             import_parser();
         } catch (interrupted &) {
             throw;
@@ -1554,17 +1554,17 @@ class parser::imp {
         regular(m_frontend) << mk_pair(ex.get_justification().pp(fmt, opts, &pos_provider, true), opts) << endl;
     }
 
-    void display_error(lua_exception const & ex) {
+    void display_error(script_exception const & ex) {
         switch (ex.get_source()) {
-        case lua_exception::source::String:
+        case script_exception::source::String:
             display_error_pos(ex.get_line() + m_last_script_pos.first - 1, static_cast<unsigned>(-1));
-            regular(m_frontend) << " executing script," << ex.msg() << endl;
+            regular(m_frontend) << " executing script," << ex.get_msg() << endl;
             break;
-        case lua_exception::source::File:
+        case script_exception::source::File:
             display_error_pos(m_last_script_pos);
-            regular(m_frontend) << " executing external script (" << ex.get_filename() << ":" << ex.get_line() << ")," << ex.msg() << endl;
+            regular(m_frontend) << " executing external script (" << ex.get_filename() << ":" << ex.get_line() << ")," << ex.get_msg() << endl;
             break;
-        case lua_exception::source::Unknown:
+        case script_exception::source::Unknown:
             display_error_pos(m_last_script_pos);
             regular(m_frontend) << " executing script, but could not decode position information, " << ex.what() << endl;
             break;
@@ -1586,20 +1586,20 @@ class parser::imp {
 
     void parse_script() {
         m_last_script_pos = mk_pair(m_scanner.get_script_block_line(), m_scanner.get_script_block_pos());
-        if (!m_leanlua_state)
+        if (!m_script_evaluator)
             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(), m_frontend.get_environment(), m_frontend.get_state());
+        m_script_evaluator->dostring(m_scanner.get_str_val().c_str(), m_frontend.get_environment(), m_frontend.get_state());
         next();
     }
 
 public:
-    imp(frontend & fe, std::istream & in, leanlua_state * S, bool use_exceptions, bool interactive):
+    imp(frontend & fe, std::istream & in, script_evaluator * 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;
+        m_script_evaluator = S;
         updt_options();
         m_found_errors = false;
         m_num_local_decls = 0;
@@ -1649,7 +1649,7 @@ public:
                     display_error(ex);
                 if (m_use_exceptions)
                     throw;
-            } catch (lua_exception & ex) {
+            } catch (script_exception & ex) {
                 m_found_errors = true;
                 reset_interrupt();
                 if (m_show_errors)
@@ -1683,7 +1683,7 @@ public:
     }
 };
 
-parser::parser(frontend & fe, std::istream & in, leanlua_state * S, bool use_exceptions, bool interactive) {
+parser::parser(frontend & fe, std::istream & in, script_evaluator * S, bool use_exceptions, bool interactive) {
     parser::imp::show_prompt(interactive, fe);
     m_ptr.reset(new imp(fe, in, S, use_exceptions, interactive));
 }
@@ -1699,7 +1699,7 @@ expr parser::parse_expr() {
     return m_ptr->parse_expr_main();
 }
 
-shell::shell(frontend & fe, leanlua_state * S):m_frontend(fe), m_leanlua_state(S) {
+shell::shell(frontend & fe, script_evaluator * S):m_frontend(fe), m_script_evaluator(S) {
 }
 
 shell::~shell() {
@@ -1715,14 +1715,14 @@ bool shell::operator()() {
         add_history(input);
         std::istringstream strm(input);
         {
-            parser p(m_frontend, strm, m_leanlua_state, false, false);
+            parser p(m_frontend, strm, m_script_evaluator, false, false);
             if (!p())
                 errors = true;
         }
         free(input);
     }
 #else
-    parser p(m_frontend, std::cin, m_leanlua_state, false, true);
+    parser p(m_frontend, std::cin, m_script_evaluator, false, true);
     return p();
 #endif
 }

src/frontends/lean/parser.h

@@ -9,13 +9,13 @@ Author: Leonardo de Moura
 #include "frontends/lean/frontend.h"
 
 namespace lean {
-class leanlua_state;
+class script_evaluator;
 /** \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, leanlua_state * S, bool use_exceptions = true, bool interactive = false);
+    parser(frontend & fe, std::istream & in, script_evaluator * S, bool use_exceptions = true, bool interactive = false);
     ~parser();
 
     /** \brief Parse a sequence of commands */
@@ -28,15 +28,15 @@ public:
 /** \brief Implements the Read Eval Print loop */
 class shell {
     frontend &                m_frontend;
-    leanlua_state *           m_leanlua_state;
+    script_evaluator *        m_script_evaluator;
 public:
-    shell(frontend & fe, leanlua_state * S);
+    shell(frontend & fe, script_evaluator * S);
     ~shell();
 
     bool operator()();
 };
 
-inline bool parse_commands(frontend & fe, std::istream & in, leanlua_state * S = nullptr, bool use_exceptions = true, bool interactive = false) {
+inline bool parse_commands(frontend & fe, std::istream & in, script_evaluator * 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) {

src/library/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp
   context_to_lambda.cpp state.cpp update_expr.cpp type_inferer.cpp
-  placeholder.cpp expr_lt.cpp)
+  placeholder.cpp expr_lt.cpp script_evaluator.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/script_evaluator.cpp

@@ -0,0 +1,23 @@
+/*
+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 "library/script_evaluator.h"
+
+namespace lean {
+char const * script_exception::what() const noexcept {
+    static thread_local std::string buffer;
+    std::ostringstream strm;
+    switch (get_source()) {
+    case source::String:  strm << "[string]:" << get_line() << ":" << get_msg() << "\n"; break;
+    case source::File:    strm << get_filename() << ":" << get_line() << ":" << get_msg() << "\n"; break;
+    case source::Unknown: return get_msg();
+    }
+    buffer = strm.str();
+    return buffer.c_str();
+}
+}

src/library/script_evaluator.h

@@ -0,0 +1,37 @@
+/*
+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 "util/exception.h"
+
+namespace lean {
+class environment;
+class state;
+/**
+   \brief Abstract base class for script code evaluators.
+   These evaluators are used to execute user-supplied code embedded in frontend files (.e.g., .lean, .smt2, etc).
+   In the current implementation we only have one implementation of this class based on the Lua programming language. So, the main purpose of this class is to organize the dependencies between modules.
+*/
+class script_evaluator {
+public:
+    virtual ~script_evaluator() {}
+    virtual void dostring(char const * str) = 0;
+    virtual void dostring(char const * str, environment & env, state & st) = 0;
+};
+
+/**
+   \brief Base class for exceptions producing when evaluating scripts.
+*/
+class script_exception : public exception {
+public:
+    enum class source { String, File, Unknown };
+    virtual source get_source() const = 0;
+    virtual char const * get_filename() const = 0;
+    virtual unsigned get_line() const = 0;
+    virtual char const * get_msg() const noexcept = 0;
+    virtual char const * what() const noexcept;
+};
+}