refactor(frontends/lean): add 'server' module as a replacement for 'interactive'

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

src/frontends/lean/CMakeLists.txt

@@ -1,7 +1,7 @@
 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_exprs.cpp
-interactive.cpp notation_cmd.cpp calc.cpp
+server.cpp notation_cmd.cpp calc.cpp
 decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp
 dependencies.cpp parser_bindings.cpp proof_qed_ext.cpp
 class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp

src/frontends/lean/interactive.cpp

@@ -1,102 +0,0 @@
-/*
-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 <string>
-#include <iostream>
-#include <sstream>
-#include <vector>
-#include <algorithm>
-#include "frontends/lean/interactive.h"
-
-namespace lean {
-interactive::interactive(environment const & env, io_state const & ios, unsigned num_threads,
-                         char const * ack_cmd, char const * snapshot_cmd, char const * restore_cmd, char const * restart_cmd):
-    m_env(env), m_ios(ios), m_num_threads(num_threads), 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, false, m_num_threads, 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<unsigned>(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);
-}
-}

src/frontends/lean/interactive.h

@@ -1,55 +0,0 @@
-/*
-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 <vector>
-#include <string>
-#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<snapshot>     m_snapshots;
-    std::vector<std::string>  m_lines;
-    environment               m_env;
-    io_state                  m_ios;
-    unsigned                  m_num_threads;
-    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, unsigned num_threads = 1,
-                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);
-};
-}

src/frontends/lean/parser.cpp

@@ -82,12 +82,13 @@ parser::parser(environment const & env, io_state const & ios,
                std::istream & strm, char const * strm_name,
                bool use_exceptions, unsigned num_threads,
                local_level_decls const & lds, local_expr_decls const & eds,
-               unsigned line):
+               unsigned line, snapshot_vector * sv, info_manager * im):
     m_env(env), m_ios(ios), m_ngen(g_tmp_prefix),
     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<pos_info_table>()),
-    m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0) {
+    m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0),
+    m_snapshot_vector(sv), m_info_manager(im) {
     m_scanner.set_line(line);
     m_num_threads = num_threads;
     m_no_undef_id_error    = false;

src/frontends/lean/parser.h

@@ -25,6 +25,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser_config.h"
 #include "frontends/lean/parser_pos_provider.h"
 #include "frontends/lean/theorem_queue.h"
+#include "frontends/lean/info_manager.h"
 
 namespace lean {
 /** \brief Exception used to track parsing erros, it does not leak outside of this class. */
@@ -41,6 +42,21 @@ typedef local_decls<expr>   local_expr_decls;
 typedef local_decls<level>  local_level_decls;
 typedef environment         local_environment;
 
+/** \brief Snapshot of the state of the Lean parser */
+struct snapshot {
+    environment       m_env;
+    local_level_decls m_lds;
+    local_expr_decls  m_eds;
+    options           m_options;
+    unsigned          m_line;
+    snapshot():m_line(0) {}
+    snapshot(environment const & env, options const & o):m_env(env), m_options(o), 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) {}
+};
+
+typedef std::vector<snapshot> snapshot_vector;
+
 class parser {
     environment             m_env;
     io_state                m_ios;
@@ -69,6 +85,10 @@ class parser {
     // We process theorems in parallel
     theorem_queue           m_theorem_queue;
 
+    // info support
+    snapshot_vector *       m_snapshot_vector;
+    info_manager *          m_info_manager;
+
     void display_warning_pos(unsigned line, unsigned pos);
     void display_warning_pos(pos_info p);
     void display_error_pos(unsigned line, unsigned pos);
@@ -137,8 +157,8 @@ public:
            std::istream & strm, char const * str_name,
            bool use_exceptions = false, unsigned num_threads = 1,
            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,
-           unsigned line = 1);
+           snapshot_vector * sv = nullptr, info_manager * im = nullptr);
     ~parser();
 
     environment const & env() const { return m_env; }

src/frontends/lean/server.cpp

@@ -0,0 +1,138 @@
+/*
+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 <string>
+#include "frontends/lean/server.h"
+#include "frontends/lean/parser.h"
+
+namespace lean {
+server::server(environment const & env, io_state const & ios, unsigned num_threads):
+    m_env(env), m_options(ios.get_options()), m_ios(ios), m_num_threads(num_threads),
+    m_empty_snapshot(m_env, m_options) {
+}
+
+static std::string g_file("FILE");
+static std::string g_replace("REPLACE");
+static std::string g_info("INFO");
+
+static bool is_command(std::string const & cmd, std::string const & line) {
+    return line.compare(0, cmd.size(), cmd) == 0;
+}
+
+static std::string & ltrim(std::string & s) {
+    s.erase(s.begin(), std::find_if(s.begin(), s.end(), std::not1(std::ptr_fun<int, int>(std::isspace))));
+    return s;
+}
+
+static std::string & rtrim(std::string & s) {
+    s.erase(std::find_if(s.rbegin(), s.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), s.end());
+    return s;
+}
+
+static std::string & trim(std::string & s) {
+    return ltrim(rtrim(s));
+}
+
+/**
+   \brief Return index i <= m_snapshots.size() s.t.
+      * forall j < i, m_snapshots[j].m_line < line
+      * forall i <= j < m_snapshots.size(),  m_snapshots[j].m_line >= line
+*/
+unsigned server::find(unsigned linenum) {
+    unsigned low  = 0;
+    unsigned high = m_snapshots.size();
+    while (true) {
+        lean_assert(low <= high);
+        if (low == high)
+            return low;
+        unsigned mid = low + ((high - low)/2);
+        lean_assert(low <= mid && mid < high);
+        lean_assert(mid < m_snapshots.size());
+        snapshot const & s = m_snapshots[mid];
+        if (s.m_line < linenum) {
+            low  = mid+1;
+        } else {
+            high = mid;
+        }
+    }
+}
+
+void server::process_from(unsigned linenum) {
+    m_info.invalidate(linenum);
+    unsigned i = find(linenum);
+    m_snapshots.resize(i);
+    snapshot & s = i == 0 ? m_empty_snapshot : m_snapshots[i-1];
+    std::string block;
+    lean_assert(s.m_line > 0);
+    for (unsigned j = s.m_line-1; j < m_lines.size(); j++) {
+        block += m_lines[j];
+        block += '\n';
+    }
+    std::istringstream strm(block);
+    m_ios.set_options(s.m_options);
+    parser p(s.m_env, m_ios, strm, m_fname.c_str(), false, 1, s.m_lds, s.m_eds, s.m_line,
+             &m_snapshots, &m_info);
+    p();
+}
+
+void server::read_file(std::string const & fname) {
+    std::ifstream in(fname);
+    if (in.bad() || in.fail()) {
+        std::cout << "Error: failed to open file '" << fname << "'";
+    } else {
+        m_lines.clear();
+        for (std::string line; std::getline(in, line);) {
+            m_lines.push_back(line);
+        }
+        process_from(0);
+    }
+}
+
+void server::replace_line(unsigned linenum, std::string const & new_line) {
+    while (linenum >= m_lines.size())
+        m_lines.push_back("");
+    m_lines[linenum] = new_line;
+    process_from(linenum);
+}
+
+void server::show_info(unsigned linenum) {
+    unsigned i = find(linenum);
+    environment const & env = i == 0 ? m_env     : m_snapshots[i-1].m_env;
+    options const & o       = i == 0 ? m_options : m_snapshots[i-1].m_options;
+    m_ios.set_options(o);
+    io_state_stream out(env, m_ios);
+    m_info.display(out, linenum);
+    out << "-- ENDINFO" << endl;
+}
+
+bool server::operator()(std::istream & in) {
+    for (std::string line; std::getline(in, line);) {
+        if (is_command(g_file, line)) {
+            std::string fname = line.substr(g_file.size());
+            trim(fname);
+            read_file(fname);
+        } else if (is_command(g_replace, line)) {
+            std::string data = line.substr(g_replace.size());
+            trim(data);
+            unsigned linenum = atoi(data.c_str());
+            if (std::getline(in, line)) {
+                replace_line(linenum, line);
+            } else {
+                std::cout << "Error: unexpected end of input\n";
+                return false;
+            }
+        } else if (is_command(g_info, line)) {
+            std::string data = line.substr(g_info.size());
+            trim(data);
+            unsigned linenum = atoi(data.c_str());
+            show_info(linenum);
+        } else {
+            std::cout << "Error: unexpected command line: " << line << "\n";
+        }
+    }
+    return true;
+}
+}

src/frontends/lean/server.h

@@ -0,0 +1,39 @@
+/*
+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 <vector>
+#include <string>
+#include "frontends/lean/parser.h"
+#include "frontends/lean/info_manager.h"
+
+namespace lean {
+/**
+   \brief Class for managing an input stream used to communicate with
+   external processes.
+*/
+class server {
+    std::vector<std::string>  m_lines;
+    snapshot_vector           m_snapshots;
+    info_manager              m_info;
+    environment               m_env;
+    options                   m_options;
+    io_state                  m_ios;
+    unsigned                  m_num_threads;
+    snapshot                  m_empty_snapshot;
+    std::string               m_fname;
+
+    void read_file(std::string const & fname);
+    void replace_line(unsigned linenum, std::string const & new_line);
+    void show_info(unsigned linenum);
+    void process_from(unsigned linenum);
+    unsigned find(unsigned linenum);
+
+public:
+    server(environment const & env, io_state const & ios, unsigned num_threads = 1);
+    bool operator()(std::istream & in);
+};
+}

src/shell/lean.cpp

@@ -27,7 +27,7 @@ Author: Leonardo de Moura
 #include "library/error_handling/error_handling.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/pp.h"
-#include "frontends/lean/interactive.h"
+#include "frontends/lean/server.h"
 #include "frontends/lean/dependencies.h"
 #include "frontends/lua/register_modules.h"
 #include "version.h"
@@ -71,7 +71,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";
+    std::cout << "  --server          start Lean in 'server' mode\n";
     std::cout << "  --hott            use Homotopy Type Theory kernel and libraries\n";
     std::cout << "  --threads=num -j  number of threads used to process lean files\n";
     std::cout << "  --deps            just print dependencies of a Lean input\n";
@@ -106,7 +106,7 @@ static struct option g_long_options[] = {
     {"githash",     no_argument,       0, 'g'},
     {"output",      required_argument, 0, 'o'},
     {"trust",       required_argument, 0, 't'},
-    {"interactive", no_argument,       0, 'i'},
+    {"server",      no_argument,       0, 'S'},
     {"quiet",       no_argument,       0, 'q'},
     {"hott",        no_argument,       0, 'H'},
     {"threads",     required_argument, 0, 'j'},
@@ -120,9 +120,9 @@ static struct option g_long_options[] = {
 };
 
 #if defined(LEAN_USE_BOOST)
-static char const * g_opt_str = "IFDHiqlupgvhj:012c:012s:012t:012o:";
+static char const * g_opt_str = "IFDHSqlupgvhj:012c:012s:012t:012o:";
 #else
-static char const * g_opt_str = "IFDHiqlupgvhj:012c:012t:012o:";
+static char const * g_opt_str = "IFDHSqlupgvhj:012c:012t:012o:";
 #endif
 
 enum class lean_mode { Standard, HoTT };
@@ -133,7 +133,7 @@ int main(int argc, char ** argv) {
     bool export_objects  = false;
     unsigned trust_lvl   = 0;
     bool quiet           = false;
-    bool interactive     = false;
+    bool server          = false;
     bool only_deps       = false;
     bool flycheck        = false;
     bool flyinfo         = false;
@@ -153,8 +153,8 @@ int main(int argc, char ** argv) {
             mode = lean_mode::HoTT;
             lean::init_lean_path("hott");
             break;
-        case 'i':
+        case 'S':
-            interactive = true;
+            server = true;
             break;
         case 'v':
             display_header(std::cout);
@@ -247,10 +247,11 @@ int main(int argc, char ** argv) {
                 lean_unreachable(); // LCOV_EXCL_LINE
             }
         }
-        if (ok && interactive && default_k == input_kind::Lean) {
+        if (ok && server && default_k == input_kind::Lean) {
             signal(SIGINT, on_ctrl_c);
-            lean::interactive in(env, ios, num_threads);
+            lean::server Sv(env, ios, num_threads);
-            in(std::cin, "[stdin]");
+            if (!Sv(std::cin))
+                ok = false;
         }
         if (export_objects && ok) {
             std::ofstream out(output, std::ofstream::binary);