feat(frontends/lean): add info_manager

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

src/frontends/lean/CMakeLists.txt

@@ -5,6 +5,6 @@ interactive.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
-structure_cmd.cpp sorry.cpp)
+structure_cmd.cpp sorry.cpp info_manager.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/info_manager.cpp

@@ -0,0 +1,129 @@
+/*
+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 "library/choice.h"
+#include "frontends/lean/info_manager.h"
+#include "frontends/lean/pp_options.h"
+
+namespace lean {
+struct tmp_info_data : public info_data {
+    tmp_info_data(unsigned l, unsigned c):info_data(l, c) {}
+    virtual void display(io_state_stream const &) const { lean_unreachable(); } // LCOV_EXCL_LINE
+};
+
+bool operator<(info_data const & i1, info_data const & i2) {
+    if (i1.get_line() != i2.get_line())
+        return i1.get_line() < i2.get_line();
+    else
+        return i1.get_column() < i2.get_column();
+}
+
+void type_info_data::display(io_state_stream const & ios) const {
+    ios << "-- TYPE|" << get_line() << "|" << get_column() << "\n";
+    ios << m_expr << endl;
+    ios << "-- ACK" << endl;
+}
+
+void overload_info_data::display(io_state_stream const & ios) const {
+    ios << "-- OVERLOAD|" << get_line() << "|" << get_column() << "\n";
+    for (unsigned i = 0; i < get_num_choices(m_choices); i++) {
+        if (i > 0)
+            ios << "--\n";
+        ios << get_choice(m_choices, i) << endl;
+    }
+    ios << "-- ACK" << endl;
+}
+
+void coercion_info_data::display(io_state_stream const & ios) const {
+    ios << "-- COERCION|" << get_line() << "|" << get_column() << "\n";
+    options os = ios.get_options();
+    os = os.update(get_pp_coercion_option_name(), true);
+    ios.update_options(os) << m_coercion << endl;
+    ios << "-- ACK" << endl;
+}
+
+info_manager::info_manager():m_sorted_upto(0) {}
+
+void info_manager::sort_core() {
+    if (m_sorted_upto == m_data.size())
+        return;
+    std::stable_sort(m_data.begin() + m_sorted_upto, m_data.end());
+    m_sorted_upto = m_data.size();
+}
+
+/**
+   \brief Return index i <= m_sorted_upto s.t.
+      * forall j < i, m_data[j].pos < (line, column)
+      * forall i <= j < m_sorted_upto,  m_data[j].pos >= (line, column)
+*/
+unsigned info_manager::find(unsigned line, unsigned column) {
+    tmp_info_data d(line, column);
+    unsigned low  = 0;
+    unsigned high = m_sorted_upto;
+    while (true) {
+        // forall j < low,                    m_data[j] < d
+        // forall high <= j < m_sorted_upto,  m_data[j] >= d
+        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_sorted_upto);
+        info_data const & dmid = *m_data[mid];
+        if (dmid < d) {
+            low  = mid+1;
+        } else {
+            high = mid;
+        }
+    }
+}
+
+void info_manager::invalidate(unsigned sline) {
+    lock_guard<mutex> lc(m_mutex);
+    sort_core();
+    m_data.resize(find(sline, 0));
+    m_sorted_upto = m_data.size();
+}
+
+void info_manager::add_core(std::unique_ptr<info_data> && d) {
+    if (m_data.empty()) {
+        m_sorted_upto = 1;
+    } else if (m_sorted_upto == m_data.size() && *m_data.back() < *d) {
+        m_sorted_upto++;
+    } else if (m_sorted_upto > 0 && *d < *m_data[m_sorted_upto]) {
+        m_sorted_upto = find(d->get_line(), d->get_column());
+    }
+    m_data.push_back(std::move(d));
+}
+
+void info_manager::add(std::unique_ptr<info_data> && d) {
+    lock_guard<mutex> lc(m_mutex);
+    add_core(std::move(d));
+}
+
+void info_manager::append(std::vector<std::unique_ptr<info_data>> && v) {
+    lock_guard<mutex> lc(m_mutex);
+    for (auto & d : v)
+        add_core(std::move(d));
+}
+
+void info_manager::sort() {
+    lock_guard<mutex> lc(m_mutex);
+    sort_core();
+}
+
+void info_manager::display(io_state_stream const & ios, unsigned line) {
+    lock_guard<mutex> lc(m_mutex);
+    sort_core();
+    unsigned i = find(line, 0);
+    for (; i < m_data.size(); i++) {
+        auto const & d = *m_data[i];
+        if (d.get_line() > line)
+            break;
+        d.display(ios);
+    }
+}
+}

src/frontends/lean/info_manager.h

@@ -0,0 +1,62 @@
+/*
+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 <memory>
+#include "util/thread.h"
+#include "kernel/expr.h"
+#include "library/io_state_stream.h"
+
+namespace lean {
+class info_data {
+    unsigned m_line;
+    unsigned m_column;
+public:
+    info_data(unsigned l, unsigned c):m_line(l), m_column(c) {}
+    unsigned get_line() const { return m_line; }
+    unsigned get_column() const { return m_column; }
+    virtual void display(io_state_stream const & ios) const = 0;
+};
+bool operator<(info_data const & i1, info_data const & i2);
+
+class type_info_data : public info_data {
+    expr m_expr;
+public:
+    type_info_data(unsigned l, unsigned c, expr const & e):info_data(l, c), m_expr(e) {}
+    virtual void display(io_state_stream const & ios) const;
+};
+
+class overload_info_data : public info_data {
+    expr m_choices;
+public:
+    overload_info_data(unsigned l, unsigned c, expr const & e):info_data(l, c), m_choices(e) {}
+    virtual void display(io_state_stream const & ios) const;
+};
+
+class coercion_info_data : public info_data {
+    expr m_coercion;
+public:
+    coercion_info_data(unsigned l, unsigned c, expr const & e):info_data(l, c), m_coercion(e) {}
+    virtual void display(io_state_stream const & ios) const;
+};
+
+class info_manager {
+    typedef std::vector<std::unique_ptr<info_data>> data_vector;
+    mutex       m_mutex;
+    unsigned    m_sorted_upto;
+    data_vector m_data;
+    void add_core(std::unique_ptr<info_data> && d);
+    unsigned find(unsigned line, unsigned column);
+    void sort_core();
+public:
+    info_manager();
+    void invalidate(unsigned sline);
+    void add(std::unique_ptr<info_data> && d);
+    void append(std::vector<std::unique_ptr<info_data>> && v);
+    void sort();
+    void display(io_state_stream const & ios, unsigned line);
+};
+}

src/frontends/lean/pp_options.cpp

@@ -53,6 +53,10 @@ static name g_pp_full_names       {"pp", "full_names"};
 static name g_pp_private_names    {"pp", "private_names"};
 static name g_pp_metavar_args     {"pp", "metavar_args"};
 
+name const & get_pp_coercion_option_name() {
+    return g_pp_coercion;
+}
+
 list<options> const & get_distinguishing_pp_options() {
     static options g_universes_true(g_pp_universes, true);
     static options g_implicit_true(g_pp_implicit, true);

src/frontends/lean/pp_options.h

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "util/sexpr/options.h"
 namespace lean {
+name const & get_pp_coercion_option_name();
 unsigned get_pp_max_depth(options const & opts);
 unsigned get_pp_max_steps(options const & opts);
 bool     get_pp_notation(options const & opts);

src/library/io_state_stream.h

@@ -16,6 +16,7 @@ protected:
     environment const &  m_env;
     formatter            m_formatter;
     output_channel &     m_stream;
+    io_state_stream(environment const & env, formatter const & fmt, output_channel & s):m_env(env), m_formatter(fmt), m_stream(s) {}
 public:
     io_state_stream(environment const & env, io_state const & ios, bool regular = true):
         m_env(env), m_formatter(ios.get_formatter_factory()(env, ios.get_options())),
@@ -25,6 +26,7 @@ public:
     formatter const & get_formatter() const { return m_formatter; }
     options get_options() const { return m_formatter.get_options(); }
     environment const & get_environment() const { return m_env; }
+    io_state_stream update_options(options const & o) const { return io_state_stream(m_env, m_formatter.update_options(o), m_stream); }
 };
 
 inline io_state_stream regular(environment const & env, io_state const & ios) { return io_state_stream(env, ios, true); }