From c6600bdaf42ef1e640b99187e57d0d14883f35fa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 17 Aug 2014 08:28:02 -0700 Subject: [PATCH] refactor(frontends/lean/info_manager): intrusive smart pointer for info_data Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 13 ++- src/frontends/lean/info_manager.cpp | 171 +++++++++++++++++----------- src/frontends/lean/info_manager.h | 79 +++++++------ src/frontends/lean/parser.cpp | 6 +- src/frontends/lean/parser.h | 2 +- 5 files changed, 154 insertions(+), 117 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 66a7141d2..2ce5f289e 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -307,7 +307,7 @@ class elaborator { name_set m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned bool m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent. bool m_noinfo; // when true, we do not collect information when true, we set is to true whenever we find noinfo annotation. - std::vector> m_pre_info_data; + std::vector m_pre_info_data; struct scope_ctx { context::scope m_scope1; @@ -909,11 +909,12 @@ public: if (auto p = pip()->get_pos_info(e)) { type_checker::scope scope(*m_tc[m_relax_main_opaque]); expr t = m_tc[m_relax_main_opaque]->infer(r); + info_data d = mk_type_info(p->first, p->second, t); if (replace) { - while (!m_pre_info_data.empty() && m_pre_info_data.back()->eq_pos(p->first, p->second)) + while (!m_pre_info_data.empty() && m_pre_info_data.back() == d) m_pre_info_data.pop_back(); } - m_pre_info_data.push_back(std::unique_ptr(new type_info_data(p->first, p->second, t))); + m_pre_info_data.push_back(d); } } } @@ -929,7 +930,7 @@ public: void save_synth_data(expr const & e, expr const & r) { if (!m_noinfo && infom() && pip() && is_placeholder(e)) { if (auto p = pip()->get_pos_info(e)) { - m_pre_info_data.push_back(std::unique_ptr(new synth_info_data(p->first, p->second, r))); + m_pre_info_data.push_back(mk_synth_info(p->first, p->second, r)); } } } @@ -1271,9 +1272,9 @@ public: if (!infom()) return; for (auto & p : m_pre_info_data) - p->instantiate(s); + p = p.instantiate(s); // TODO(Leo): implement smarter append - infom()->append(std::move(m_pre_info_data), false); + infom()->append(m_pre_info_data, false); m_pre_info_data.clear(); } diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 88a45d122..e80b1be3a 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -10,12 +10,9 @@ Author: Leonardo de Moura #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 -}; +void info_data_cell::dealloc() { delete this; } -int info_data::compare(info_data const & d) const { +int info_data_cell::compare(info_data_cell const & d) const { if (m_line != d.m_line) return m_line < d.m_line ? -1 : 1; if (m_column != d.m_column) @@ -25,50 +22,107 @@ int info_data::compare(info_data const & d) const { return 0; } -bool operator<(info_data const & i1, info_data const & i2) { - return i1.compare(i2) < 0; -} +info_data_cell * info_data_cell::instantiate(substitution &) const { return nullptr; } -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; -} +struct tmp_info_data : public info_data_cell { + tmp_info_data(unsigned l, unsigned c):info_data_cell(l, c) {} + virtual void display(io_state_stream const &) const { lean_unreachable(); } // LCOV_EXCL_LINE +}; -void synth_info_data::display(io_state_stream const & ios) const { - ios << "-- SYNTH|" << get_line() << "|" << get_column() << "\n"; - ios << m_expr << endl; - ios << "-- ACK" << endl; -} +static info_data g_dummy(new tmp_info_data(0, 0)); -void overload_info_data::display(io_state_stream const & ios) const { - ios << "-- OVERLOAD|" << get_line() << "|" << get_column() << "\n"; - options os = ios.get_options(); - os = os.update(get_pp_full_names_option_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; +info_data::info_data():info_data(g_dummy) {} +info_data info_data::instantiate(substitution & s) const { + if (auto r = m_ptr->instantiate(s)) { + return info_data(r); + } else { + return *this; } - new_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; -} +class type_info_data : public info_data_cell { +protected: + expr m_expr; +public: + type_info_data() {} + type_info_data(unsigned l, unsigned c, expr const & e):info_data_cell(l, c), m_expr(e) {} + + expr const & get_type() const { + return m_expr; + } + + virtual void display(io_state_stream const & ios) const { + ios << "-- TYPE|" << get_line() << "|" << get_column() << "\n"; + ios << m_expr << endl; + ios << "-- ACK" << endl; + } + + virtual info_data_cell * instantiate(substitution & s) const { + expr e = s.instantiate(m_expr); + if (is_eqp(e, m_expr)) + return nullptr; + else + return new type_info_data(get_line(), get_column(), e); + } +}; + +class synth_info_data : public type_info_data { +public: + synth_info_data(unsigned l, unsigned c, expr const & e):type_info_data(l, c, e) {} + virtual void display(io_state_stream const & ios) const { + ios << "-- SYNTH|" << get_line() << "|" << get_column() << "\n"; + ios << m_expr << endl; + ios << "-- ACK" << endl; + } +}; + +class overload_info_data : public info_data_cell { + expr m_choices; +public: + overload_info_data(unsigned l, unsigned c, expr const & e):info_data_cell(l, c), m_choices(e) {} + virtual void display(io_state_stream const & ios) const { + ios << "-- OVERLOAD|" << get_line() << "|" << get_column() << "\n"; + options os = ios.get_options(); + os = os.update(get_pp_full_names_option_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 coercion_info_data : public info_data_cell { + expr m_coercion; +public: + coercion_info_data(unsigned l, unsigned c, expr const & e):info_data_cell(l, c), m_coercion(e) {} + virtual void 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_data mk_type_info(unsigned l, unsigned c, expr const & e) { return info_data(new type_info_data(l, c, e)); } +info_data mk_synth_info(unsigned l, unsigned c, expr const & e) { return info_data(new synth_info_data(l, c, e)); } +info_data mk_overload_info(unsigned l, unsigned c, expr const & e) { return info_data(new overload_info_data(l, c, e)); } +info_data mk_coercion_info(unsigned l, unsigned c, expr const & e) { return info_data(new coercion_info_data(l, c, e)); } + +bool operator<(info_data const & i1, info_data const & i2) { return i1.compare(i2) < 0; } +bool operator==(info_data const & i1, info_data const & i2) { return i1.compare(i2) == 0; } +bool operator!=(info_data const & i1, info_data const & i2) { return i1.compare(i2) != 0; } +bool operator<(info_data const & i1, info_data_cell const & i2) { return i1.compare(i2) < 0; } 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(), - [](std::unique_ptr const & i1, std::unique_ptr const & i2) { return *i1 < *i2; }); + std::stable_sort(m_data.begin() + m_sorted_upto, m_data.end()); m_sorted_upto = m_data.size(); } @@ -90,7 +144,7 @@ unsigned info_manager::find(unsigned line, unsigned column) { 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]; + info_data const & dmid = m_data[mid]; if (dmid < d) { low = mid+1; } else { @@ -108,46 +162,31 @@ void info_manager::invalidate(unsigned sline) { m_sorted_upto = m_data.size(); } -void info_manager::add_core(std::unique_ptr && d) { +void info_manager::add_core(info_data const & d) { if (m_data.empty()) { m_sorted_upto = 1; - } else if (m_sorted_upto == m_data.size() && *m_data.back() < *d) { + } 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-1]) { - m_sorted_upto = find(d->get_line(), d->get_column()); + } else if (m_sorted_upto > 0 && d < m_data[m_sorted_upto-1]) { + m_sorted_upto = find(d.get_line(), d.get_column()); } - m_data.push_back(std::move(d)); + m_data.push_back(d); } -void info_manager::add(std::unique_ptr && d) { +void info_manager::add(info_data const & d) { lock_guard lc(m_mutex); - add_core(std::move(d)); + add_core(d); } -void info_manager::append(std::vector> && vs, bool remove_duplicates) { - lock_guard lc(m_mutex); - std::stable_sort(vs.begin(), vs.end(), [](std::unique_ptr const & v1, std::unique_ptr const & v2) { - return *v1 < *v2; }); - info_data * prev = nullptr; - bool first = true; - for (auto & v : vs) { - if (!remove_duplicates || first || !v->eq_pos(prev->get_line(), prev->get_column())) { - prev = v.get(); - add_core(std::move(v)); - first = false; - } - } -} - -void info_manager::append(std::vector & vs, bool remove_duplicates) { +void info_manager::append(std::vector & vs, bool remove_duplicates) { lock_guard lc(m_mutex); std::stable_sort(vs.begin(), vs.end()); - type_info_data prev; + info_data prev; bool first = true; - for (auto & v : vs) { - if (!remove_duplicates || first || !v.eq_pos(prev.get_line(), prev.get_column())) { + for (auto const & v : vs) { + if (!remove_duplicates || first || v != prev) { prev = v; - add_core(std::unique_ptr(new type_info_data(v))); + add_core(v); first = false; } } @@ -163,7 +202,7 @@ void info_manager::display(io_state_stream const & ios, unsigned line) { sort_core(); unsigned i = find(line, 0); for (; i < m_data.size(); i++) { - auto const & d = *m_data[i]; + auto const & d = m_data[i]; if (d.get_line() > line) break; d.display(ios); diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h index e2da02c41..2faf48f61 100644 --- a/src/frontends/lean/info_manager.h +++ b/src/frontends/lean/info_manager.h @@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include #include #include "util/thread.h" #include "kernel/expr.h" @@ -13,67 +12,65 @@ Author: Leonardo de Moura #include "library/io_state_stream.h" namespace lean { -class info_data { +class info_data; +class info_data_cell { unsigned m_line; unsigned m_column; + MK_LEAN_RC(); + void dealloc(); +protected: + friend info_data; + virtual info_data_cell * instantiate(substitution &) const; public: - info_data():m_line(0), m_column(0) {} - info_data(unsigned l, unsigned c):m_line(l), m_column(c) {} - virtual ~info_data() {} + info_data_cell():m_line(0), m_column(0), m_rc(0) {} + info_data_cell(unsigned l, unsigned c):m_line(l), m_column(c) {} + virtual ~info_data_cell() {} unsigned get_line() const { return m_line; } unsigned get_column() const { return m_column; } - bool eq_pos(unsigned line, unsigned col) const { return m_line == line && m_column == col; } - virtual int compare(info_data const & d) const; + virtual int compare(info_data_cell const & d) const; virtual void display(io_state_stream const & ios) const = 0; - virtual void instantiate(substitution &) {} -}; -bool operator<(info_data const & i1, info_data const & i2); - -class type_info_data : public info_data { -protected: - expr m_expr; -public: - type_info_data() {} - type_info_data(unsigned l, unsigned c, expr const & e):info_data(l, c), m_expr(e) {} - expr const & get_type() const { return m_expr; } - virtual void display(io_state_stream const & ios) const; - virtual void instantiate(substitution & s) { m_expr = s.instantiate(m_expr); } }; -class synth_info_data : public type_info_data { +class info_data { +private: + info_data_cell * m_ptr; public: - synth_info_data(unsigned l, unsigned c, expr const & e):type_info_data(l, c, e) {} - virtual void display(io_state_stream const & ios) const; + 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); } + void display(io_state_stream const & ios) const { m_ptr->display(ios); } + 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); } + info_data instantiate(substitution & s) const; + unsigned get_line() const { return m_ptr->get_line(); } + unsigned get_column() const { return m_ptr->get_column(); } }; +bool operator==(info_data const & i1, info_data const & i2); -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; -}; +info_data mk_type_info(unsigned l, unsigned c, expr const & e); +info_data mk_synth_info(unsigned l, unsigned c, expr const & e); +info_data mk_overload_info(unsigned l, unsigned c, expr const & e); +info_data mk_coercion_info(unsigned l, unsigned c, expr const & e); class info_manager { - typedef std::vector> data_vector; + typedef std::vector data_vector; mutex m_mutex; + unsigned m_sorted_upto; data_vector m_data; - void add_core(std::unique_ptr && d); + void add_core(info_data const & d); unsigned find(unsigned line, unsigned column); void sort_core(); public: info_manager(); void invalidate(unsigned sline); - void add(std::unique_ptr && d); - void append(std::vector> && v, bool remove_duplicates = true); - void append(std::vector & v, bool remove_duplicates); + void add(info_data const & d); + void append(std::vector & v, bool remove_duplicates = true); void sort(); void display(io_state_stream const & ios, unsigned line); }; diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index d7556f0f2..fc569b129 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1268,7 +1268,7 @@ void parser::save_overload(expr const & e) { if (!m_info_manager || !is_choice(e)) return; auto p = pos_of(e); - m_info_manager->add(std::unique_ptr(new overload_info_data(p.first, p.second, e))); + m_info_manager->add(mk_overload_info(p.first, p.second, e)); } void parser::save_type_info(expr const & e) { @@ -1288,13 +1288,13 @@ void parser::save_type_info(expr const & e) { if (!d) return; auto p = pos_of(e); - m_pre_info_data.push_back(type_info_data(p.first, p.second, d->get_type())); + m_pre_info_data.push_back(mk_type_info(p.first, p.second, d->get_type())); } else if (is_local(e)) { auto p = pos_of(e); expr t = mlocal_type(e); if (is_meta(t)) return; - m_pre_info_data.push_back(type_info_data(p.first, p.second, t)); + m_pre_info_data.push_back(mk_type_info(p.first, p.second, t)); } } diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index ba5505ac1..2a8993806 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -91,7 +91,7 @@ class parser { // info support snapshot_vector * m_snapshot_vector; info_manager * m_info_manager; - std::vector m_pre_info_data; // type information before elaboration + std::vector m_pre_info_data; // type information before elaboration // cache support definition_cache * m_cache;