From 2e8ebb6d9eee45dfbcaeeca9c4fc5063b0fc634c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Jun 2014 11:26:17 -0700 Subject: [PATCH] feat(frontends/lean/parser): add 'parse_commands' and 'parse_script' Signed-off-by: Leonardo de Moura --- src/frontends/lean/cmd_table.h | 1 + src/frontends/lean/parser.cpp | 83 +++++++++++++++++++++++++++++++++ src/frontends/lean/parser.h | 32 +++++++++++-- src/shell/CMakeLists.txt | 8 ++-- src/shell/lean.cpp | 57 +++++++++++----------- tests/lean/config.lean | 4 ++ tests/lean/t1.lean | 13 ++++++ tests/lean/t1.lean.expected.out | 2 + 8 files changed, 164 insertions(+), 36 deletions(-) create mode 100644 tests/lean/config.lean create mode 100644 tests/lean/t1.lean create mode 100644 tests/lean/t1.lean.expected.out diff --git a/src/frontends/lean/cmd_table.h b/src/frontends/lean/cmd_table.h index 25ff1c923..18204326c 100644 --- a/src/frontends/lean/cmd_table.h +++ b/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; } diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 9c19c6e33..d42792b4f 100644 --- a/src/frontends/lean/parser.cpp +++ b/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 #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); +} } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 8e4efa311..10aca0072 100644 --- a/src/frontends/lean/parser.h +++ b/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 local_entry; typedef scoped_map local_decls; @@ -73,10 +76,26 @@ class parser { void sync_command(); void protected_call(std::function && f, std::function && sync); + template + typename std::result_of::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); } diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index d6d59338d..9109dca9c 100644 --- a/src/shell/CMakeLists.txt +++ b/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() diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index d9f1b95bc..048f95b5c 100644 --- a/src/shell/lean.cpp +++ b/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; - // bool quiet = false; + unsigned trust_lvl = 0; + 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; - // lean::set_default_trust_imported_for_lua(true); + trust_lvl = atoi(optarg); 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; - // env->set_trusted_imported(trust_imported); - // io_state ios = init_frontend(env, no_kernel); - // if (quiet) - // ios.set_option("verbose", false); + if (quiet) + ios.set_option("verbose", false); script_state S; - - // S.apply([&](lua_State * L) { - // set_global_environment(L, env); - // set_global_io_state(L, ios); - // }); + S.apply([&](lua_State * L) { + set_global_environment(L, env); + 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)) - // ok = false; + if (!parse_commands(env, ios, argv[i], &S, 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; } diff --git a/tests/lean/config.lean b/tests/lean/config.lean new file mode 100644 index 000000000..06cc987ca --- /dev/null +++ b/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 diff --git a/tests/lean/t1.lean b/tests/lean/t1.lean new file mode 100644 index 000000000..5821d7a30 --- /dev/null +++ b/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()) +*) diff --git a/tests/lean/t1.lean.expected.out b/tests/lean/t1.lean.expected.out new file mode 100644 index 000000000..3f13e2241 --- /dev/null +++ b/tests/lean/t1.lean.expected.out @@ -0,0 +1,2 @@ +testing... +Bool