feat(frontends/lean/parser): add 'parse_commands' and 'parse_script'

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

src/frontends/lean/cmd_table.h

@@ -38,6 +38,7 @@ struct cmd_info_tmpl {
 public:
     cmd_info_tmpl(name const & n, char const * d, F const & fn):
         m_name(n), m_descr(d), m_fn(fn) {}
+    cmd_info_tmpl() {}
     name const & get_name() const { return m_name; }
     std::string const & get_descr() const { return m_descr; }
     F const & get_fn() const { return m_fn; }

src/frontends/lean/parser.cpp

@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <string>
 #include "util/interrupt.h"
 #include "util/script_exception.h"
+#include "util/sstream.h"
 #include "library/io_state_stream.h"
 #include "library/parser_nested_exception.h"
 #include "library/error_handling/error_handling.h"
@@ -129,6 +131,14 @@ void parser::save_pos(expr e, pos_info p) {
     m_pos_table->insert(mk_pair(get_tag(e), p));
 }
 
+bool parser::curr_is_token(name const & tk) const {
+    return
+        (curr() == scanner::token_kind::Keyword || curr() == scanner::token_kind::CommandKeyword) &&
+        get_token_info().value() == tk;
+}
+
+static name g_period(".");
+
 expr parser::parse_expr(unsigned /* rbp */) {
     // TODO(Leo):
     return expr();
@@ -147,4 +157,77 @@ tactic parser::parse_tactic(unsigned /* rbp */) {
     // TODO(Leo):
     return tactic();
 }
+
+void parser::parse_command() {
+    lean_assert(curr() == scanner::token_kind::CommandKeyword);
+    name const & cmd_name = get_token_info().value();
+    if (auto it = cmds().find(cmd_name)) {
+        next();
+        m_env = it->get_fn()(*this);
+    } else {
+        auto p = pos();
+        next();
+        throw parser_error(sstream() << "unknown command '" << cmd_name << "'", p);
+    }
+}
+
+void parser::parse_script(bool as_expr) {
+    m_last_script_pos = pos();
+    if (!m_ss)
+        throw exception("failed to execute Lua script, parser does not have a Lua interpreter");
+    std::string script_code = m_scanner.get_str_val();
+    if (as_expr)
+        script_code = "return " + script_code;
+    next();
+    using_script([&](lua_State * L) {
+            dostring(L, script_code.c_str());
+        });
+}
+
+bool parser::parse_commands() {
+    try {
+        bool done = false;
+        while (!done) {
+            protected_call([&]() {
+                    check_interrupted();
+                    switch (curr()) {
+                    case scanner::token_kind::CommandKeyword:
+                        parse_command();
+                        break;
+                    case scanner::token_kind::ScriptBlock:
+                        parse_script();
+                        break;
+                    case scanner::token_kind::Eof:
+                        done = true;
+                        break;
+                    case scanner::token_kind::Keyword:
+                        if (curr_is_token(g_period)) {
+                            next();
+                            break;
+                        }
+                    default:
+                        throw parser_error("command expected", pos());
+                    }
+                },
+                [&]() { sync_command(); });
+        }
+    } catch (interrupt_parser) {}
+    return !m_found_errors;
+}
+
+
+bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, script_state * S, bool use_exceptions) {
+    parser p(env, ios, in, strm_name, S, use_exceptions);
+    bool r = p();
+    ios = p.ios();
+    env = p.env();
+    return r;
+}
+
+bool parse_commands(environment & env, io_state & ios, char const * fname, script_state * S, bool use_exceptions) {
+    std::ifstream in(fname);
+    if (in.bad() || in.fail())
+        throw exception(sstream() << "failed to open file '" << fname << "'");
+    return parse_commands(env, ios, in, fname, S, use_exceptions);
+}
 }

src/frontends/lean/parser.h

@@ -15,8 +15,9 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/expr_maps.h"
 #include "library/io_state.h"
+#include "library/kernel_bindings.h"
 #include "frontends/lean/scanner.h"
-#include "frontends/lean/cmd_table.h"
+#include "frontends/lean/parser_config.h"
 #include "frontends/lean/parser_pos_provider.h"
 
 namespace lean {
@@ -39,6 +40,8 @@ struct parser_error : public exception {
     virtual void rethrow() const { throw *this; }
 };
 
+struct interrupt_parser {};
+
 class parser {
     typedef std::pair<expr, unsigned> local_entry;
     typedef scoped_map<name, local_entry, name_hash, name_eq> local_decls;
@@ -73,10 +76,26 @@ class parser {
 
     void sync_command();
     void protected_call(std::function<void()> && f, std::function<void()> && sync);
+    template<typename F>
+    typename std::result_of<F(lua_State * L)>::type using_script(F && f) {
+        return m_ss->apply([&](lua_State * L) {
+                set_io_state    set1(L, m_ios);
+                set_environment set2(L, m_env);
+                return f(L);
+            });
+    }
 
     tag get_tag(expr e);
 
     void updt_options();
+
+    parser_config const & cfg() const { return get_parser_config(env()); }
+    cmd_table const & cmds() const { return cfg().m_cmds; }
+
+    void parse_command();
+    void parse_script(bool as_expr = false);
+    bool parse_commands();
+
 public:
     parser(environment const & env, io_state const & ios,
            std::istream & strm, char const * str_name,
@@ -95,7 +114,7 @@ public:
     tactic parse_tactic(unsigned rbp = 0);
 
     /** \brief Return the current position information */
-    pos_info pos() const { return mk_pair(m_scanner.get_line(), m_scanner.get_pos()); }
+    pos_info pos() const { return pos_info(m_scanner.get_line(), m_scanner.get_pos()); }
     void save_pos(expr e, pos_info p);
 
     /** \brief Read the next token. */
@@ -104,6 +123,8 @@ public:
     scanner::token_kind curr() const { return m_curr; }
     /** \brief Read the next token if the current one is not End-of-file. */
     void next() { if (m_curr != scanner::token_kind::Eof) scan(); }
+    /** \brief Return true iff the current token is equal to \c tk */
+    bool curr_is_token(name const & tk) const;
 
     mpq const & get_num_val() const { return m_scanner.get_num_val(); }
     name const & get_name_val() const { return m_scanner.get_name_val(); }
@@ -112,6 +133,11 @@ public:
     std::string const & get_stream_name() const { return m_scanner.get_stream_name(); }
 
     /** parse all commands in the input stream */
-    bool operator()();
+    bool operator()() { return parse_commands(); }
 };
+
+bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name,
+                    script_state * S, bool use_exceptions);
+bool parse_commands(environment & env, io_state & ios, char const * fname, script_state * S,
+                    bool use_exceptions);
 }

src/shell/CMakeLists.txt

@@ -73,7 +73,7 @@ FOREACH(T ${LEANLUATESTS})
   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
   add_test(NAME "leanluatest_${T_NAME}"
            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua"
-           COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T_NAME})
+           COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME})
 ENDFOREACH(T)
 
 # LEAN LUA SLOW TESTS
@@ -82,7 +82,7 @@ FOREACH(T ${LEANLUASLOWTESTS})
   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
   add_test(NAME "leanluaslowtest_${T_NAME}"
            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua/slow"
-           COMMAND "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T_NAME})
+           COMMAND "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T_NAME})
   set_tests_properties("leanluaslowtest_${T_NAME}" PROPERTIES LABELS "expensive")
 ENDFOREACH(T)
 
@@ -101,7 +101,7 @@ FOREACH(T ${LEANLUADOCS})
   GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
   add_test(NAME "leanluadoc_${T_NAME}"
            WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/lua"
-           COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T})
+           COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T})
 ENDFOREACH(T)
 
 # LEAN LUA THREAD TESTS
@@ -112,7 +112,7 @@ if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Linux"))
       GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
       add_test(NAME "leanluathreadtest_${T_NAME}"
         WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lua/threads"
-        COMMAND "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t" ${T})
+        COMMAND "../test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean -t 100000" ${T})
     ENDFOREACH(T)
   endif()
 endif()

src/shell/lean.cpp

@@ -19,13 +19,15 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/formatter.h"
+#include "kernel/standard/standard.h"
+#include "library/io_state_stream.h"
 #include "library/error_handling/error_handling.h"
+#include "frontends/lean/parser.h"
 #if 0
 #include "kernel/io_state.h"
 #include "library/printer.h"
 #include "library/kernel_bindings.h"
-#include "library/io_state_stream.h"
+
-#include "frontends/lean/parser.h"
 #include "frontends/lean/shell.h"
 #include "frontends/lean/frontend.h"
 #include "frontends/lean/register_module.h"
@@ -40,6 +42,7 @@ using lean::environment;
 using lean::io_state;
 using lean::io_state_stream;
 using lean::regular;
+using lean::mk_environment;
 
 #if 0
 using lean::shell;
@@ -75,7 +78,7 @@ static void display_help(std::ostream & out) {
     std::cout << "  --luahook=num -c  how often the Lua interpreter checks the interrupted flag,\n";
     std::cout << "                    it is useful for interrupting non-terminating user scripts,\n";
     std::cout << "                    0 means 'do not check'.\n";
-    std::cout << "  --trust -t        trust imported modules\n";
+    std::cout << "  --trust=num -t    trust level (default: 0) \n";
     std::cout << "  --quiet -q        do not print verbose messages\n";
 #if defined(LEAN_USE_BOOST)
     std::cout << "  --tstack=num -s   thread stack size in Kb\n";
@@ -102,12 +105,11 @@ static struct option g_long_options[] = {
     {"lean",       no_argument,       0, 'l'},
     {"olean",      no_argument,       0, 'b'},
     {"lua",        no_argument,       0, 'u'},
-    {"nokernel",   no_argument,       0, 'n'},
     {"path",       no_argument,       0, 'p'},
     {"luahook",    required_argument, 0, 'c'},
     {"githash",    no_argument,       0, 'g'},
     {"output",     required_argument, 0, 'o'},
-    {"trust",      no_argument,       0, 't'},
+    {"trust",      required_argument, 0, 't'},
     {"quiet",      no_argument,       0, 'q'},
 #if defined(LEAN_USE_BOOST)
     {"tstack",     required_argument, 0, 's'},
@@ -115,17 +117,22 @@ static struct option g_long_options[] = {
     {0, 0, 0, 0}
 };
 
+#if defined(LEAN_USE_BOOST)
+static char const * g_opt_str = "qlupgvhc:012s:012t:012o:";
+#else
+static char const * g_opt_str = "qlupgvhc:012t:012o:";
+#endif
+
 int main(int argc, char ** argv) {
     lean::save_stack_info();
     lean::register_modules();
-    // bool no_kernel      = false;
     // bool export_objects = false;
-    // bool trust_imported = false;
+    unsigned trust_lvl  = 0;
-    // bool quiet          = false;
+    bool quiet          = false;
     std::string output;
     input_kind default_k = input_kind::Lean; // default
     while (true) {
-        int c = getopt_long(argc, argv, "qtnlupgvhc:012s:012o:", g_long_options, NULL);
+        int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL);
         if (c == -1)
             break; // end of command line
         switch (c) {
@@ -156,19 +163,15 @@ int main(int argc, char ** argv) {
         case 's':
             lean::set_thread_stack_size(atoi(optarg)*1024);
             break;
-        case 'n':
-            // no_kernel = true;
-            break;
         case 'o':
             output = optarg;
             // export_objects = true;
             break;
         case 't':
-            // trust_imported = true;
+            trust_lvl = atoi(optarg);
-            // lean::set_default_trust_imported_for_lua(true);
             break;
         case 'q':
-            // quiet = true;
+            quiet = true;
             break;
         default:
             std::cerr << "Unknown command line option\n";
@@ -177,19 +180,16 @@ int main(int argc, char ** argv) {
         }
     }
 
+    environment env = mk_environment(trust_lvl);
     io_state ios(lean::mk_simple_formatter());
-    // environment env;
+    if (quiet)
-    // env->set_trusted_imported(trust_imported);
+        ios.set_option("verbose", false);
-    // io_state ios = init_frontend(env, no_kernel);
-    // if (quiet)
-    //     ios.set_option("verbose", false);
 
     script_state S;
-
+    S.apply([&](lua_State * L) {
-    // S.apply([&](lua_State * L) {
+            set_global_environment(L, env);
-    //         set_global_environment(L, env);
+            set_global_io_state(L, ios);
-    //         set_global_io_state(L, ios);
+        });
-    //     });
 
     try {
         if (optind >= argc) {
@@ -227,8 +227,8 @@ int main(int argc, char ** argv) {
                     }
                 }
                 if (k == input_kind::Lean) {
-                    // if (!parse_commands(env, ios, argv[i], &S, false, false))
+                    if (!parse_commands(env, ios, argv[i], &S, false))
-                    //    ok = false;
+                        ok = false;
                 } else if (k == input_kind::OLean) {
                     // try {
                     //    env->load(std::string(argv[i]), ios);
@@ -240,7 +240,6 @@ int main(int argc, char ** argv) {
                     try {
                         S.dofile(argv[i]);
                     } catch (lean::exception & ex) {
-                        environment env; // TODO(Leo): use global environment
                         ::lean::display_error(regular(env, ios), nullptr, ex);
                         ok = false;
                     }
@@ -253,7 +252,7 @@ int main(int argc, char ** argv) {
             return ok ? 0 : 1;
         }
     } catch (lean::exception & ex) {
-        // ::lean::display_error(ios, nullptr, ex);
+        ::lean::display_error(regular(env, ios), nullptr, ex);
     }
     return 1;
 }

tests/lean/config.lean

@@ -0,0 +1,4 @@
+-- set_option default configuration for tests
+-- TODO(Leo): uncomment
+-- set_option pp.colors  false
+-- set_option pp.unicode true

tests/lean/t1.lean

@@ -0,0 +1,13 @@
+
+(*
+print("testing...")
+local env = get_env()
+env = add_decl(env, mk_var_decl("x", Bool))
+assert(env:find("x"))
+set_env(env)
+*)
+
+(*
+local env = get_env()
+print(env:find("x"):type())
+*)

tests/lean/t1.lean.expected.out

@@ -0,0 +1,2 @@
+testing...
+Bool