From 891a3fb48b08bfa58db18880aa55db75644d15a3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 14 Jun 2014 10:38:42 -0700 Subject: [PATCH] feat(frontends/lean): add command block reader with snapshot and resume Signed-off-by: Leonardo de Moura --- src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/interactive.cpp | 102 +++++++++++++ src/frontends/lean/interactive.h | 55 +++++++ src/frontends/lean/parser.cpp | 4 +- src/frontends/lean/parser.h | 3 +- src/shell/CMakeLists.txt | 9 ++ src/shell/lean.cpp | 149 ++++++++----------- tests/lean/interactive/t1.input | 8 + tests/lean/interactive/t1.input.expected.out | 5 + tests/lean/interactive/t2.input | 4 + tests/lean/interactive/t2.input.expected.out | 2 + tests/lean/interactive/t3.input | 7 + tests/lean/interactive/t3.input.expected.out | 3 + tests/lean/interactive/t4.input | 26 ++++ tests/lean/interactive/t4.input.expected.out | 11 ++ tests/lean/interactive/test.sh | 48 ------ tests/lean/interactive/test_single.sh | 2 +- 17 files changed, 301 insertions(+), 139 deletions(-) create mode 100644 src/frontends/lean/interactive.cpp create mode 100644 src/frontends/lean/interactive.h create mode 100644 tests/lean/interactive/t1.input create mode 100644 tests/lean/interactive/t1.input.expected.out create mode 100644 tests/lean/interactive/t2.input create mode 100644 tests/lean/interactive/t2.input.expected.out create mode 100644 tests/lean/interactive/t3.input create mode 100644 tests/lean/interactive/t3.input.expected.out create mode 100644 tests/lean/interactive/t4.input create mode 100644 tests/lean/interactive/t4.input.expected.out delete mode 100755 tests/lean/interactive/test.sh diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index eecc286361..53449416cf 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -1,6 +1,6 @@ add_library(lean_frontend register_module.cpp token_table.cpp scanner.cpp parse_table.cpp parser_config.cpp parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_tactic_cmds.cpp -builtin_exprs.cpp) +builtin_exprs.cpp interactive.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/interactive.cpp b/src/frontends/lean/interactive.cpp new file mode 100644 index 0000000000..9c0d37b6f0 --- /dev/null +++ b/src/frontends/lean/interactive.cpp @@ -0,0 +1,102 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include +#include +#include +#include +#include +#include "frontends/lean/interactive.h" + +namespace lean { +interactive::interactive(environment const & env, io_state const & ios, script_state const & ss, + char const * ack_cmd, char const * snapshot_cmd, char const * restore_cmd, char const * restart_cmd): + m_env(env), m_ios(ios), m_ss(ss), m_line(1), + m_ack_cmd(ack_cmd), m_snapshot_cmd(snapshot_cmd), m_restore_cmd(restore_cmd), m_restart_cmd(restart_cmd) { + save_snapshot(); +} + +void interactive::parse_block(std::string const & str, char const * strm_name) { + if (str.size() > 0) { + std::istringstream block(str); + parser p(m_env, m_ios, block, strm_name, &m_ss, false, m_lds, m_eds, m_line); + p(); + m_env = p.env(); + m_ios = p.ios(); + m_lds = p.get_local_level_decls(); + m_eds = p.get_local_expr_decls(); + m_line = p.pos().first; + } +} + +void interactive::save_snapshot() { + m_snapshots.push_back(snapshot(m_env, m_lds, m_eds, m_ios.get_options(), m_line)); +} + +void interactive::restore(unsigned new_line, std::string & block) { + block.clear(); + lean_assert(new_line > 0); + // try to find a snapshop + unsigned i = m_snapshots.size(); + while (i > 0) { + --i; + if (m_snapshots[i].m_line <= new_line) + break; + } + m_snapshots.resize(i+1); + auto & s = m_snapshots[i]; + m_env = s.m_env; + m_lds = s.m_lds; + m_eds = s.m_eds; + m_ios.set_options(s.m_options); + m_line = s.m_line; + unsigned new_sz = std::min(new_line, static_cast(m_lines.size())) - 1; + m_lines.resize(new_sz); + for (unsigned i = s.m_line; i < new_sz; i++) { + block += m_lines[i]; + block += '\n'; + } +} + +void interactive::operator()(std::istream & in, char const * strm_name) { + std::string block; + for (std::string line; std::getline(in, line);) { + if (line == m_ack_cmd) { + parse_block(block, strm_name); + block.clear(); + } else if (line == m_snapshot_cmd) { + parse_block(block, strm_name); + save_snapshot(); + block.clear(); + } else if (line.compare(0, m_restore_cmd.size(), m_restore_cmd) == 0) { + parse_block(block, strm_name); + block.clear(); + std::string rest = line.substr(m_restore_cmd.size()); + restore(std::atoi(rest.c_str()), block); + } else if (line == m_restart_cmd) { + parse_block(block, strm_name); + block.clear(); + // keep consuming lines while they match the m_lines + unsigned i = 0; + while (true) { + if (!std::getline(in, line)) + return; // end of file + if (m_lines[i] != line) + break; + i++; + } + restore(i+1, block); + block += line; + block += '\n'; + } else { + block += line; + block += '\n'; + m_lines.push_back(line); + } + } + parse_block(block, strm_name); +} +} diff --git a/src/frontends/lean/interactive.h b/src/frontends/lean/interactive.h new file mode 100644 index 0000000000..e4281fa631 --- /dev/null +++ b/src/frontends/lean/interactive.h @@ -0,0 +1,55 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include +#include "frontends/lean/parser.h" + +namespace lean { +/** + \brief Class for managing an input stream used to communicate with + external processes. + + It process blocks of Lean commands separated by an ACK string. + The lean commands may create snapshots that can be resumed at the start + of the next block. +*/ +class interactive { + struct snapshot { + environment m_env; + local_level_decls m_lds; + local_expr_decls m_eds; + options m_options; + unsigned m_line; + snapshot():m_line(1) {} + snapshot(environment const & env, local_level_decls const & lds, local_expr_decls const & eds, options const & opts, unsigned line): + m_env(env), m_lds(lds), m_eds(eds), m_options(opts), m_line(line) {} + }; + + std::vector m_snapshots; + std::vector m_lines; + environment m_env; + io_state m_ios; + script_state m_ss; + local_level_decls m_lds; + local_expr_decls m_eds; + unsigned m_line; + std::string m_ack_cmd; + std::string m_snapshot_cmd; + std::string m_restore_cmd; + std::string m_restart_cmd; + void parse_block(std::string const & str, char const * strm_name); + void save_snapshot(); + void restore(unsigned new_line, std::string & block); +public: + interactive(environment const & env, io_state const & ios, script_state const & ss, + char const * ack_cmd = "#ACK", char const * snapshot_cmd = "#SNAPSHOT", + char const * res_cmd = "#RESTORE", char const * restart_cmd = "#RESTART"); + environment const & env() const { return m_env; } + void operator()(std::istream & in, char const * strm_name); +}; +} diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index beb6a2528a..cf4bd67f72 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -41,11 +41,13 @@ bool get_parser_show_errors(options const & opts) { return opts.get_bool(g_ parser::parser(environment const & env, io_state const & ios, std::istream & strm, char const * strm_name, script_state * ss, bool use_exceptions, - local_level_decls const & lds, local_expr_decls const & eds): + local_level_decls const & lds, local_expr_decls const & eds, + unsigned line): m_env(env), m_ios(ios), m_ss(ss), m_verbose(true), m_use_exceptions(use_exceptions), m_scanner(strm, strm_name), m_local_level_decls(lds), m_local_decls(eds), m_pos_table(std::make_shared()) { + m_scanner.set_line(line); m_type_use_placeholder = true; m_found_errors = false; updt_options(); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index d6ac2451f9..230d043f0a 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -127,7 +127,8 @@ public: std::istream & strm, char const * str_name, script_state * ss = nullptr, bool use_exceptions = false, local_level_decls const & lds = local_level_decls(), - local_expr_decls const & eds = local_expr_decls()); + local_expr_decls const & eds = local_expr_decls(), + unsigned line = 1); environment const & env() const { return m_env; } io_state const & ios() const { return m_ios; } diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 058ca6a350..26d736725f 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -49,6 +49,15 @@ FOREACH(T ${LEANRUNTESTS}) COMMAND "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) ENDFOREACH(T) +# LEAN INTERACTIVE TESTS +file(GLOB LEANITTESTS "${LEAN_SOURCE_DIR}/../tests/lean/interactive/*.input") +FOREACH(T ${LEANITTESTS}) + GET_FILENAME_COMPONENT(T_NAME ${T} NAME) + add_test(NAME "leanittest_${T_NAME}" + WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/interactive" + COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME}) +ENDFOREACH(T) + # # LEAN SLOW TESTS # file(GLOB LEANSLOWTESTS "${LEAN_SOURCE_DIR}/../tests/lean/slow/*.lean") # FOREACH(T ${LEANSLOWTESTS}) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index e73b97080c..be67fde4cf 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -24,14 +24,7 @@ Author: Leonardo de Moura #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 "frontends/lean/shell.h" -#include "frontends/lean/frontend.h" -#include "frontends/lean/register_module.h" -#endif +#include "frontends/lean/interactive.h" #include "frontends/lua/register_modules.h" #include "version.h" #include "githash.h" // NOLINT @@ -44,13 +37,6 @@ using lean::io_state_stream; using lean::regular; using lean::mk_environment; -#if 0 -using lean::shell; -using lean::parser; -using lean::invoke_debugger; -using lean::notify_assertion_violation; -#endif - enum class input_kind { Unspecified, Lean, OLean, Lua }; static void on_ctrl_c(int ) { @@ -80,6 +66,7 @@ static void display_help(std::ostream & out) { std::cout << " 0 means 'do not check'.\n"; std::cout << " --trust=num -t trust level (default: 0) \n"; std::cout << " --quiet -q do not print verbose messages\n"; + std::cout << " --interactive -i read blocks of commands from the input stream\n"; #if defined(LEAN_USE_BOOST) std::cout << " --tstack=num -s thread stack size in Kb\n"; #endif @@ -100,27 +87,28 @@ static char const * get_file_extension(char const * fname) { } static struct option g_long_options[] = { - {"version", no_argument, 0, 'v'}, - {"help", no_argument, 0, 'h'}, - {"lean", no_argument, 0, 'l'}, - {"olean", no_argument, 0, 'b'}, - {"lua", no_argument, 0, 'u'}, - {"path", no_argument, 0, 'p'}, - {"luahook", required_argument, 0, 'c'}, - {"githash", no_argument, 0, 'g'}, - {"output", required_argument, 0, 'o'}, - {"trust", required_argument, 0, 't'}, - {"quiet", no_argument, 0, 'q'}, + {"version", no_argument, 0, 'v'}, + {"help", no_argument, 0, 'h'}, + {"lean", no_argument, 0, 'l'}, + {"olean", no_argument, 0, 'b'}, + {"lua", no_argument, 0, 'u'}, + {"path", no_argument, 0, 'p'}, + {"luahook", required_argument, 0, 'c'}, + {"githash", no_argument, 0, 'g'}, + {"output", required_argument, 0, 'o'}, + {"trust", required_argument, 0, 't'}, + {"interactive", no_argument, 0, 'i'}, + {"quiet", no_argument, 0, 'q'}, #if defined(LEAN_USE_BOOST) - {"tstack", required_argument, 0, 's'}, + {"tstack", required_argument, 0, 's'}, #endif {0, 0, 0, 0} }; #if defined(LEAN_USE_BOOST) -static char const * g_opt_str = "qlupgvhc:012s:012t:012o:"; +static char const * g_opt_str = "iqlupgvhc:012s:012t:012o:"; #else -static char const * g_opt_str = "qlupgvhc:012t:012o:"; +static char const * g_opt_str = "iqlupgvhc:012t:012o:"; #endif int main(int argc, char ** argv) { @@ -129,6 +117,7 @@ int main(int argc, char ** argv) { bool export_objects = false; unsigned trust_lvl = 0; bool quiet = false; + bool interactive = false; std::string output; input_kind default_k = input_kind::Lean; // default while (true) { @@ -136,6 +125,9 @@ int main(int argc, char ** argv) { if (c == -1) break; // end of command line switch (c) { + case 'i': + interactive = true; + break; case 'v': display_header(std::cout); return 0; @@ -192,67 +184,50 @@ int main(int argc, char ** argv) { }); try { - if (optind >= argc) { - display_header(std::cout); - signal(SIGINT, on_ctrl_c); - if (default_k == input_kind::Lean) { -#if defined(LEAN_WINDOWS) - std::cout << "Type 'exit.' to exit or 'help.' for help."<< std::endl; -#else - std::cout << "Type Ctrl-D or 'exit.' to exit or 'help.' for help."<< std::endl; -#endif - // shell sh(env, &S); - // int status = sh() ? 0 : 1; - // if (export_objects) - // env->export_objects(output); - // return status; - return 0; + bool ok = true; + for (int i = optind; i < argc; i++) { + char const * ext = get_file_extension(argv[i]); + input_kind k = default_k; + if (ext) { + if (strcmp(ext, "lean") == 0) { + k = input_kind::Lean; + } else if (strcmp(ext, "olean") == 0) { + k = input_kind::OLean; + } else if (strcmp(ext, "lua") == 0) { + k = input_kind::Lua; + } + } + if (k == input_kind::Lean) { + 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); + // } catch (lean::exception & ex) { + // std::cerr << "Failed to load binary file '" << argv[i] << "': " << ex.what() << "\n"; + // ok = false; + // } + } else if (k == input_kind::Lua) { + try { + S.dofile(argv[i]); + } catch (lean::exception & ex) { + ::lean::display_error(regular(env, ios), nullptr, ex); + ok = false; + } } else { - lean_assert(default_k == input_kind::Lua); - S.import("repl"); - return 0; + lean_unreachable(); // LCOV_EXCL_LINE } - } else { - bool ok = true; - for (int i = optind; i < argc; i++) { - char const * ext = get_file_extension(argv[i]); - input_kind k = default_k; - if (ext) { - if (strcmp(ext, "lean") == 0) { - k = input_kind::Lean; - } else if (strcmp(ext, "olean") == 0) { - k = input_kind::OLean; - } else if (strcmp(ext, "lua") == 0) { - k = input_kind::Lua; - } - } - if (k == input_kind::Lean) { - 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); - // } catch (lean::exception & ex) { - // std::cerr << "Failed to load binary file '" << argv[i] << "': " << ex.what() << "\n"; - // ok = false; - // } - } else if (k == input_kind::Lua) { - try { - S.dofile(argv[i]); - } catch (lean::exception & ex) { - ::lean::display_error(regular(env, ios), nullptr, ex); - ok = false; - } - } else { - lean_unreachable(); // LCOV_EXCL_LINE - } - } - if (export_objects) { - std::ofstream out(output, std::ofstream::binary); - export_module(out, env); - } - return ok ? 0 : 1; } + if (ok && interactive && default_k == input_kind::Lean) { + signal(SIGINT, on_ctrl_c); + lean::interactive in(env, ios, S); + in(std::cin, "[stdin]"); + } + if (export_objects) { + std::ofstream out(output, std::ofstream::binary); + export_module(out, env); + } + return ok ? 0 : 1; } catch (lean::exception & ex) { ::lean::display_error(regular(env, ios), nullptr, ex); } diff --git a/tests/lean/interactive/t1.input b/tests/lean/interactive/t1.input new file mode 100644 index 0000000000..dc5057870a --- /dev/null +++ b/tests/lean/interactive/t1.input @@ -0,0 +1,8 @@ +print "hello" +print "block1" +#ACK +print "block2" +-- comment +print "block2b" +#ACK +print "block3" diff --git a/tests/lean/interactive/t1.input.expected.out b/tests/lean/interactive/t1.input.expected.out new file mode 100644 index 0000000000..73de1770c9 --- /dev/null +++ b/tests/lean/interactive/t1.input.expected.out @@ -0,0 +1,5 @@ +hello +block1 +block2 +block2b +block3 diff --git a/tests/lean/interactive/t2.input b/tests/lean/interactive/t2.input new file mode 100644 index 0000000000..c1aecf5091 --- /dev/null +++ b/tests/lean/interactive/t2.input @@ -0,0 +1,4 @@ +print "hello" +#ACK +print pr +#ACK diff --git a/tests/lean/interactive/t2.input.expected.out b/tests/lean/interactive/t2.input.expected.out new file mode 100644 index 0000000000..5550847553 --- /dev/null +++ b/tests/lean/interactive/t2.input.expected.out @@ -0,0 +1,2 @@ +hello +[stdin]:2:7: error: invalid print command diff --git a/tests/lean/interactive/t3.input b/tests/lean/interactive/t3.input new file mode 100644 index 0000000000..5357f91386 --- /dev/null +++ b/tests/lean/interactive/t3.input @@ -0,0 +1,7 @@ +section + parameter A : Type + check A +#ACK + check A +end +print "done" \ No newline at end of file diff --git a/tests/lean/interactive/t3.input.expected.out b/tests/lean/interactive/t3.input.expected.out new file mode 100644 index 0000000000..5376e99a7f --- /dev/null +++ b/tests/lean/interactive/t3.input.expected.out @@ -0,0 +1,3 @@ +A : Type.{l_1} +A : Type.{l_1} +done diff --git a/tests/lean/interactive/t4.input b/tests/lean/interactive/t4.input new file mode 100644 index 0000000000..0a7dbea799 --- /dev/null +++ b/tests/lean/interactive/t4.input @@ -0,0 +1,26 @@ +variable N : Type.{1} +print "block 1" +#SNAPSHOT +variable f : N -> N +variable g : N -> N +#SNAPSHOT +check N +print "before restore" +#RESTORE 3 +-- Restore will remove all lines >= 3 +-- You will be able to reuse the first snapshot +print "after restore" +print "only once" +check N +variable f : N -> N +#RESTORE 6 +-- Restore will remove all lines >= 6 +print "after second restore" +#RESTART +variable N : Type.{1} +print "block 1" +-- Restore will remove all lines >= 3 +-- You will be able to reuse the first snapshot +print "after restore" +check N +print "done" \ No newline at end of file diff --git a/tests/lean/interactive/t4.input.expected.out b/tests/lean/interactive/t4.input.expected.out new file mode 100644 index 0000000000..f9fb8ec8a5 --- /dev/null +++ b/tests/lean/interactive/t4.input.expected.out @@ -0,0 +1,11 @@ +block 1 +N : Type +before restore +after restore +only once +N : Type +after restore +after second restore +after restore +N : Type +done diff --git a/tests/lean/interactive/test.sh b/tests/lean/interactive/test.sh deleted file mode 100755 index 235acc38a3..0000000000 --- a/tests/lean/interactive/test.sh +++ /dev/null @@ -1,48 +0,0 @@ -#!/bin/bash -if [ $# -ne 2 -a $# -ne 1 ]; then - echo "Usage: test.sh [lean-executable-path] [yes/no]?" - exit 1 -fi -ulimit -s unlimited -LEAN=$1 -if [ $# -ne 2 ]; then - INTERACTIVE=no -else - INTERACTIVE=$2 -fi -NUM_ERRORS=0 -for f in `ls *.lean`; do - echo "-- testing $f" - cat config.lean $f | $LEAN --lean | tail -n +3 > $f.produced.out - if test -f $f.expected.out; then - if diff $f.produced.out $f.expected.out; then - echo "-- checked" - else - echo "ERROR: file $f.produced.out does not match $f.expected.out" - NUM_ERRORS=$(($NUM_ERRORS+1)) - if [ $INTERACTIVE == "yes" ]; then - meld $f.produced.out $f.expected.out - if diff $f.produced.out $f.expected.out; then - echo "-- mismath was fixed" - fi - fi - fi - else - echo "ERROR: file $f.expected.out does not exist" - NUM_ERRORS=$(($NUM_ERRORS+1)) - if [ $INTERACTIVE == "yes" ]; then - read -p "copy $f.produced.out (y/n)? " - if [ $REPLY == "y" ]; then - cp $f.produced.out $f.expected.out - echo "-- copied $f.produced.out --> $f.expected.out" - fi - fi - fi -done -if [ $NUM_ERRORS -gt 0 ]; then - echo "-- Number of errors: $NUM_ERRORS" - exit 1 -else - echo "-- Passed" - exit 0 -fi diff --git a/tests/lean/interactive/test_single.sh b/tests/lean/interactive/test_single.sh index 7388424ae9..6910f883e6 100755 --- a/tests/lean/interactive/test_single.sh +++ b/tests/lean/interactive/test_single.sh @@ -12,7 +12,7 @@ else fi f=$2 echo "-- testing $f" -cat config.lean $f | $LEAN --lean | tail -n +3 > $f.produced.out +$LEAN -i < $f > $f.produced.out if test -f $f.expected.out; then if diff $f.produced.out $f.expected.out; then echo "-- checked"