From 67017cecef25583f40d3dfaaba8a2891e9e9cafb Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 30 Oct 2016 22:13:49 -0400 Subject: [PATCH] chore(shell): add back `info_manager` from master and make it compile --- src/shell/CMakeLists.txt | 2 +- src/shell/info_manager.cpp | 454 +++++++++++++++++++++++++++++++++++++ src/shell/info_manager.h | 42 ++++ src/shell/server.cpp | 1 + 4 files changed, 498 insertions(+), 1 deletion(-) create mode 100644 src/shell/info_manager.cpp create mode 100644 src/shell/info_manager.h diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index ceabbc5898..6ec9656258 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -1,4 +1,4 @@ -add_executable(lean lean.cpp json.cpp server.cpp) +add_executable(lean lean.cpp info_manager.cpp json.cpp server.cpp) target_link_libraries(lean leanstatic) install(TARGETS lean DESTINATION bin) diff --git a/src/shell/info_manager.cpp b/src/shell/info_manager.cpp new file mode 100644 index 0000000000..6671dc44a3 --- /dev/null +++ b/src/shell/info_manager.cpp @@ -0,0 +1,454 @@ +/* +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 "util/thread.h" +#include "kernel/environment.h" +#include "library/choice.h" +#include "library/scoped_ext.h" +#include "library/pp_options.h" +#include "library/type_context.h" +#include "shell/info_manager.h" + +namespace lean { +class info_data; + +enum class info_kind { Type = 0, ExtraType, Synth, Overload, Coercion, Symbol, Identifier, ProofState }; +bool operator<(info_kind k1, info_kind k2) { return static_cast(k1) < static_cast(k2); } + +class info_data_cell { + unsigned m_column; + MK_LEAN_RC(); + void dealloc() { delete this; } +protected: + friend info_data; +public: + info_data_cell():m_column(0), m_rc(0) {} + info_data_cell(unsigned c):m_column(c), m_rc(0) {} + virtual ~info_data_cell() {} + /** \brief Return true iff the information is considered "cheap" + If the column number is not provided in the method info_manager::display, + then only "cheap" information is displayed. + */ + virtual bool is_cheap() const { return true; } + virtual info_kind kind() const = 0; + unsigned get_column() const { return m_column; } + virtual void display(io_state_stream const & ios, unsigned line) const = 0; + virtual int compare(info_data_cell const & d) const { + if (m_column != d.m_column) + return m_column < d.m_column ? -1 : 1; + if (kind() != d.kind()) + return kind() < d.kind() ? -1 : 1; + return 0; + } +}; + +class info_data { +private: + info_data_cell * m_ptr; +public: + info_data(); + info_data(info_data_cell * c):m_ptr(c) { lean_assert(c); m_ptr->inc_ref(); } + info_data(info_data const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } + info_data(info_data && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } + ~info_data() { if (m_ptr) m_ptr->dec_ref(); } + friend void swap(info_data & a, info_data & b) { std::swap(a.m_ptr, b.m_ptr); } + info_data & operator=(info_data const & s) { LEAN_COPY_REF(s); } + info_data & operator=(info_data && s) { LEAN_MOVE_REF(s); } + int compare(info_data const & d) const { return m_ptr->compare(*d.m_ptr); } + int compare(info_data_cell const & d) const { return m_ptr->compare(d); } + unsigned get_column() const { return m_ptr->get_column(); } + bool is_cheap() const { return m_ptr->is_cheap(); } + void display(io_state_stream const & ios, unsigned line) const { m_ptr->display(ios, line); } + info_data_cell const * raw() const { return m_ptr; } + info_kind kind() const { return m_ptr->kind(); } +}; + +struct tmp_info_data : public info_data_cell { + tmp_info_data(unsigned c):info_data_cell(c) {} + virtual info_kind kind() const { lean_unreachable(); } + virtual void display(io_state_stream const &, unsigned) const { lean_unreachable(); } // LCOV_EXCL_LINE +}; + +static info_data * g_dummy = nullptr; +void initialize_info_manager() { + g_dummy = new info_data(new tmp_info_data(0)); +} + +void finalize_info_manager() { + delete g_dummy; +} + +info_data::info_data():info_data(*g_dummy) {} + +class type_info_data : public info_data_cell { +protected: + expr m_expr; +public: + type_info_data() {} + type_info_data(unsigned c, expr const & e):info_data_cell(c), m_expr(e) {} + + expr const & get_type() const { return m_expr; } + + virtual info_kind kind() const { return info_kind::Type; } + + virtual void display(io_state_stream const & ios, unsigned line) const { + ios << "-- TYPE|" << line << "|" << get_column() << "\n"; + ios << m_expr << endl; + ios << "-- ACK" << endl; + } +}; + +class extra_type_info_data : public info_data_cell { +protected: + expr m_expr; + expr m_type; +public: + extra_type_info_data() {} + extra_type_info_data(unsigned c, expr const & e, expr const & t):info_data_cell(c), m_expr(e), m_type(t) {} + + virtual info_kind kind() const { return info_kind::ExtraType; } + virtual bool is_cheap() const { return false; } + + virtual void display(io_state_stream const & ios, unsigned line) const { + ios << "-- EXTRA_TYPE|" << line << "|" << get_column() << "\n"; + ios << m_expr << endl; + ios << "--" << endl; + ios << m_type << endl; + ios << "-- ACK" << endl; + } +}; + +class synth_info_data : public type_info_data { +public: + synth_info_data(unsigned c, expr const & e):type_info_data(c, e) {} + + virtual info_kind kind() const { return info_kind::Synth; } + + virtual void display(io_state_stream const & ios, unsigned line) const { + ios << "-- SYNTH|" << line << "|" << get_column() << "\n"; + ios << m_expr << endl; + ios << "-- ACK" << endl; + } + + expr const & get_expr() const { return m_expr; } +}; + +class overload_info_data : public info_data_cell { + expr m_choices; +public: + overload_info_data(unsigned c, expr const & e):info_data_cell(c), m_choices(e) {} + + virtual info_kind kind() const { return info_kind::Overload; } + + virtual void display(io_state_stream const & ios, unsigned line) const { + ios << "-- OVERLOAD|" << line << "|" << get_column() << "\n"; + options os = ios.get_options(); + os = os.update_if_undef(get_pp_full_names_name(), true); + auto new_ios = ios.update_options(os); + for (unsigned i = 0; i < get_num_choices(m_choices); i++) { + if (i > 0) + ios << "--\n"; + new_ios << get_choice(m_choices, i) << endl; + } + new_ios << "-- ACK" << endl; + } +}; + +class overload_notation_info_data : public info_data_cell { + list m_alts; +public: + overload_notation_info_data(unsigned c, list const & as):info_data_cell(c), m_alts(as) {} + + virtual info_kind kind() const { return info_kind::Overload; } + + virtual void display(io_state_stream const & ios, unsigned line) const { + ios << "-- OVERLOAD|" << line << "|" << get_column() << "\n"; + options os = ios.get_options(); + os = os.update_if_undef(get_pp_full_names_name(), true); + os = os.update_if_undef(get_pp_notation_name(), false); + auto new_ios = ios.update_options(os); + bool first = true; + for (expr const & e : m_alts) { + if (first) first = false; else ios << "--\n"; + new_ios << e << endl; + } + new_ios << "-- ACK" << endl; + } +}; + +class coercion_info_data : public info_data_cell { + expr m_expr; + expr m_type; +public: + coercion_info_data(unsigned c, expr const & e, expr const & t): + info_data_cell(c), m_expr(e), m_type(t) {} + + virtual info_kind kind() const { return info_kind::Coercion; } + + virtual void display(io_state_stream const & ios, unsigned line) const { + ios << "-- COERCION|" << line << "|" << get_column() << "\n"; + options os = ios.get_options(); + os = os.update_if_undef(get_pp_coercions_name(), true); + ios.update_options(os) << m_expr << endl << "--" << endl << m_type << endl; + ios << "-- ACK" << endl; + } +}; + +class symbol_info_data : public info_data_cell { + name m_symbol; +public: + symbol_info_data(unsigned c, name const & s):info_data_cell(c), m_symbol(s) {} + + virtual info_kind kind() const { return info_kind::Symbol; } + + virtual void display(io_state_stream const & ios, unsigned line) const { + ios << "-- SYMBOL|" << line << "|" << get_column() << "\n"; + ios << m_symbol << "\n"; + ios << "-- ACK" << endl; + } +}; + +class identifier_info_data : public info_data_cell { + name m_full_id; +public: + identifier_info_data(unsigned c, name const & full_id):info_data_cell(c), m_full_id(full_id) {} + + virtual info_kind kind() const { return info_kind::Identifier; } + + virtual void display(io_state_stream const & ios, unsigned line) const { + ios << "-- IDENTIFIER|" << line << "|" << get_column() << "\n"; + ios << m_full_id << "\n"; + ios << "-- ACK" << endl; + } +}; + +class proof_state_info_data : public info_data_cell { + tactic_state m_state; +public: + proof_state_info_data(unsigned c, tactic_state const & s):info_data_cell(c), m_state(s) {} + virtual info_kind kind() const { return info_kind::ProofState; } + virtual bool is_cheap() const { return false; } + virtual void display(io_state_stream const & ios, unsigned line) const { + ios << "-- PROOF_STATE|" << line << "|" << get_column() << "\n"; + bool first = true; + for (expr const & g : m_state.goals()) { + if (first) + first = false; + else + ios << "--" << endl; + ios << m_state.pp_goal(g) << endl; + } + ios << "-- ACK" << endl; + } +}; + +info_data mk_type_info(unsigned c, expr const & e) { return info_data(new type_info_data(c, e)); } +info_data mk_extra_type_info(unsigned c, expr const & e, expr const & t) { return info_data(new extra_type_info_data(c, e, t)); } +info_data mk_synth_info(unsigned c, expr const & e) { return info_data(new synth_info_data(c, e)); } +info_data mk_overload_info(unsigned c, expr const & e) { return info_data(new overload_info_data(c, e)); } +info_data mk_overload_notation_info(unsigned c, list const & a) { return info_data(new overload_notation_info_data(c, a)); } +info_data mk_coercion_info(unsigned c, expr const & e, expr const & t) { return info_data(new coercion_info_data(c, e, t)); } +info_data mk_symbol_info(unsigned c, name const & s) { return info_data(new symbol_info_data(c, s)); } +info_data mk_identifier_info(unsigned c, name const & full_id) { return info_data(new identifier_info_data(c, full_id)); } +info_data mk_proof_state_info(unsigned c, tactic_state const & s) { return info_data(new proof_state_info_data(c, s)); } + +struct info_data_cmp { + int operator()(info_data const & i1, info_data const & i2) const { return i1.compare(i2); } +}; + +struct info_manager::imp { + typedef rb_tree info_data_set; + + mutex m_mutex; + std::vector m_line_data; + + void synch_line(unsigned l) { + lean_assert(l > 0); + if (l >= m_line_data.size()) { + m_line_data.resize(l+1); + } + } + + /*static bool is_tactic_type(expr const & e) { + expr const * it = &e; + while (is_pi(*it)) { + it = &binding_body(*it); + } + return *it == get_tactic_type() || *it == get_tactic_expr_type() || *it == get_tactic_expr_list_type(); + }*/ + + void add_type_info(unsigned l, unsigned c, expr const & e) { + //if (is_tactic_type(e)) + // return; + lock_guard lc(m_mutex); + synch_line(l); + m_line_data[l].insert(mk_type_info(c, e)); + } + + void add_extra_type_info(unsigned l, unsigned c, expr const & e, expr const & t) { + //if (is_tactic_type(t)) + // return; + lock_guard lc(m_mutex); + synch_line(l); + m_line_data[l].insert(mk_extra_type_info(c, e, t)); + } + + void add_synth_info(unsigned l, unsigned c, expr const & e) { + lock_guard lc(m_mutex); + synch_line(l); + m_line_data[l].insert(mk_synth_info(c, e)); + } + + void add_overload_info(unsigned l, unsigned c, expr const & e) { + lock_guard lc(m_mutex); + synch_line(l); + m_line_data[l].insert(mk_overload_info(c, e)); + } + + void add_overload_notation_info(unsigned l, unsigned c, list const & a) { + lock_guard lc(m_mutex); + synch_line(l); + m_line_data[l].insert(mk_overload_notation_info(c, a)); + } + + void add_coercion_info(unsigned l, unsigned c, expr const & e, expr const & t) { + lock_guard lc(m_mutex); + synch_line(l); + m_line_data[l].insert(mk_coercion_info(c, e, t)); + } + + void erase_coercion_info(unsigned l, unsigned c) { + lock_guard lc(m_mutex); + synch_line(l); + m_line_data[l].erase(mk_coercion_info(c, expr(), expr())); + } + + void add_symbol_info(unsigned l, unsigned c, name const & s) { + lock_guard lc(m_mutex); + synch_line(l); + m_line_data[l].insert(mk_symbol_info(c, s)); + } + + /*static bool is_tactic_id(name const & id) { + if (id.is_atomic()) + return id == get_tactic_name(); + else + return is_tactic_id(id.get_prefix()); + }*/ + + void add_identifier_info(unsigned l, unsigned c, name const & full_id) { + //if (is_tactic_id(full_id)) + // return; + lock_guard lc(m_mutex); + synch_line(l); + m_line_data[l].insert(mk_identifier_info(c, full_id)); + } + + void add_proof_state_info(unsigned l, unsigned c, tactic_state const & s) { + lock_guard lc(m_mutex); + synch_line(l); + m_line_data[l].insert(mk_proof_state_info(c, s)); + } + + void remove_proof_state_info(unsigned start_line, unsigned start_col, unsigned end_line, unsigned end_col) { + lock_guard lc(m_mutex); + if (m_line_data.empty()) + return; + if (end_line >= m_line_data.size()) + end_line = m_line_data.size() - 1; + for (unsigned i = start_line; i <= end_line; i++) { + info_data_set const & curr_set = m_line_data[i]; + if (curr_set.find_if([](info_data const & info) { return info.kind() == info_kind::ProofState; })) { + info_data_set new_curr_set; + curr_set.for_each([&](info_data const & info) { + if (info.kind() == info_kind::ProofState) { + if ((i == start_line && info.get_column() < start_col) || + (i == end_line && info.get_column() >= end_col)) + new_curr_set.insert(info); + } else { + new_curr_set.insert(info); + } + }); + m_line_data[i] = new_curr_set; + } + } + } + + void invalidate_line_col_core(unsigned l, optional const & c) { + lock_guard lc(m_mutex); + synch_line(l); + if (!c) { + m_line_data[l] = info_data_set(); + } else { + info_data_set new_set; + m_line_data[l].for_each([&](info_data const & d) { + if (d.get_column() < *c) + new_set.insert(d); + }); + m_line_data[l] = new_set; + } + } + + void display(environment const & env, options const & o, io_state const & ios, unsigned line, + optional const & col) { + m_line_data[line].for_each([&](info_data const & d) { + type_context tc(env, o); + io_state_stream out = regular(env, ios, tc).update_options(o); + if ((!col && d.is_cheap()) || (col && d.get_column() == *col)) + d.display(out, line); + }); + } + + optional get_type_at(unsigned line, unsigned col) { + lock_guard lc(m_mutex); + if (line >= m_line_data.size()) + return none_expr(); + if (auto it = m_line_data[line].find(mk_type_info(col, expr()))) + return some_expr(static_cast(it->raw())->get_type()); + else + return none_expr(); + } + + optional get_meta_at(unsigned line, unsigned col) { + lock_guard lc(m_mutex); + if (line >= m_line_data.size()) + return none_expr(); + if (auto it = m_line_data[line].find(mk_synth_info(col, expr()))) + return some_expr(static_cast(it->raw())->get_expr()); + else + return none_expr(); + } +}; + +info_manager::info_manager():m_ptr(new imp()) {} +info_manager::~info_manager() {} +void info_manager::add_type_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_type_info(l, c, e); } +void info_manager::add_extra_type_info(unsigned l, unsigned c, expr const & e, expr const & t) { m_ptr->add_extra_type_info(l, c, e, t); } +void info_manager::add_synth_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_synth_info(l, c, e); } +void info_manager::add_overload_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_overload_info(l, c, e); } +void info_manager::add_overload_notation_info(unsigned l, unsigned c, list const & a) { m_ptr->add_overload_notation_info(l, c, a); } +void info_manager::add_coercion_info(unsigned l, unsigned c, expr const & e, expr const & t) { m_ptr->add_coercion_info(l, c, e, t); } +void info_manager::erase_coercion_info(unsigned l, unsigned c) { m_ptr->erase_coercion_info(l, c); } +void info_manager::add_symbol_info(unsigned l, unsigned c, name const & s) { m_ptr->add_symbol_info(l, c, s); } +void info_manager::add_identifier_info(unsigned l, unsigned c, name const & full_id) { + m_ptr->add_identifier_info(l, c, full_id); +} +void info_manager::add_proof_state_info(unsigned l, unsigned c, tactic_state const & s) { + m_ptr->add_proof_state_info(l, c, s); +} +void info_manager::display(environment const & env, options const & o, io_state const & ios, unsigned line, optional const & col) const { + m_ptr->display(env, o, ios, line, col); +} +optional info_manager::get_type_at(unsigned line, unsigned col) const { return m_ptr->get_type_at(line, col); } +optional info_manager::get_meta_at(unsigned line, unsigned col) const { return m_ptr->get_meta_at(line, col); } +void info_manager::remove_proof_state_info(unsigned start_line, unsigned start_col, unsigned end_line, unsigned end_col) { + m_ptr->remove_proof_state_info(start_line, start_col, end_line, end_col); +} +} diff --git a/src/shell/info_manager.h b/src/shell/info_manager.h new file mode 100644 index 0000000000..daf441116c --- /dev/null +++ b/src/shell/info_manager.h @@ -0,0 +1,42 @@ +/* +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 "kernel/expr.h" +#include "library/io_state_stream.h" + +namespace lean { +class proof_state; +class info_manager { + struct imp; + std::unique_ptr m_ptr; +public: + info_manager(); + ~info_manager(); + + void add_type_info(unsigned l, unsigned c, expr const & e); + void add_extra_type_info(unsigned l, unsigned c, expr const & e, expr const & t); + void add_synth_info(unsigned l, unsigned c, expr const & e); + void add_overload_info(unsigned l, unsigned c, expr const & e); + void add_overload_notation_info(unsigned l, unsigned c, list const & a); + void add_coercion_info(unsigned l, unsigned c, expr const & e, expr const & t); + void erase_coercion_info(unsigned l, unsigned c); + void add_symbol_info(unsigned l, unsigned c, name const & n); + void add_identifier_info(unsigned l, unsigned c, name const & full_id); + void add_proof_state_info(unsigned l, unsigned c, tactic_state const & s); + + /** \brief Remove PROO_STATE info from [(start_line, start_line), (end_line, end_col)) */ + void remove_proof_state_info(unsigned start_line, unsigned start_col, unsigned end_line, unsigned end_col); + + optional get_type_at(unsigned line, unsigned col) const; + optional get_meta_at(unsigned line, unsigned col) const; + void display(environment const & env, options const & o, io_state const & ios, unsigned line, + optional const & col = optional()) const; +}; +void initialize_info_manager(); +void finalize_info_manager(); +} diff --git a/src/shell/server.cpp b/src/shell/server.cpp index 298df4bf7c..9dbf7f5f40 100644 --- a/src/shell/server.cpp +++ b/src/shell/server.cpp @@ -13,6 +13,7 @@ Authors: Gabriel Ebner, Leonardo de Moura, Sebastian Ullrich #include "frontends/lean/parser.h" #include "library/module.h" #include "shell/server.h" +#include "shell/info_manager.h" #include "util/sexpr/option_declarations.h" #include "frontends/lean/util.h" #include "library/protected.h"