diff --git a/doc/server.org b/doc/server.org index 4e97d5dda..cfe728ca7 100644 --- a/doc/server.org +++ b/doc/server.org @@ -101,6 +101,14 @@ Information for overloaded operators and symbols is of the form -- ACK #+END_SRC +Information for synthesized placeholders is of the form + +#+BEGIN_SRC +-- SYNTH|[line-number]|[column-number] +[synthesized-term] +-- ACK +#+END_SRC + Here is an example of output produced by Lean #+BEGIN_SRC diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 6aa5c9b99..85ce12d35 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -303,9 +303,9 @@ class elaborator { constraint_vect m_constraints; // constraints that must be solved for the elaborated term to be type correct. local_tactic_hints m_local_tactic_hints; // mapping from metavariable name ?m to tactic expression that should be used to solve it. // this mapping is populated by the 'by tactic-expr' expression. - 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 - std::vector m_pre_info_data; + 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 + std::vector> m_pre_info_data; struct scope_ctx { context::scope m_scope1; @@ -652,6 +652,7 @@ public: if (is_placeholder(e) && !placeholder_type(e)) { expr r = m_context.mk_type_meta(e.get_tag()); save_info_data(e, r); + save_synth_data(e, r); return r; } else { return visit(e); @@ -662,6 +663,7 @@ public: if (is_placeholder(e) && !placeholder_type(e)) { expr r = mk_placeholder_meta(some_expr(t), e.get_tag(), is_strict_placeholder(e)); save_info_data(e, r); + save_synth_data(e, r); return r; } else if (is_choice(e)) { return visit_choice(e, some_expr(t)); @@ -864,6 +866,7 @@ public: expr visit_placeholder(expr const & e) { expr r = mk_placeholder_meta(placeholder_type(e), e.get_tag(), is_strict_placeholder(e)); save_info_data(e, r); + save_synth_data(e, r); return r; } @@ -900,10 +903,10 @@ public: type_checker::scope scope(*m_tc[m_relax_main_opaque]); expr t = m_tc[m_relax_main_opaque]->infer(r); 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()->eq_pos(p->first, p->second)) m_pre_info_data.pop_back(); } - m_pre_info_data.push_back(type_info_data(p->first, p->second, t)); + m_pre_info_data.push_back(std::unique_ptr(new type_info_data(p->first, p->second, t))); } } } @@ -916,6 +919,14 @@ public: save_info_data_core(e, r, true); } + void save_synth_data(expr const & e, expr const & r) { + if (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))); + } + } + } + expr visit_constant(expr const & e) { declaration d = env().get(const_name(e)); buffer ls; @@ -1250,8 +1261,10 @@ public: if (!infom()) return; for (auto & p : m_pre_info_data) - p = type_info_data(p.get_line(), p.get_column(), s.instantiate(p.get_type())); - infom()->append(m_pre_info_data); + p->instantiate(s); + // TODO(Leo): implement smarter append + infom()->append(std::move(m_pre_info_data), false); + m_pre_info_data.clear(); } std::tuple operator()(expr const & e, bool _ensure_type, bool relax_main_opaque) { diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 94c41accb..492d05855 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -28,6 +28,12 @@ void type_info_data::display(io_state_stream const & ios) const { ios << "-- ACK" << endl; } +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; +} + void overload_info_data::display(io_state_stream const & ios) const { ios << "-- OVERLOAD|" << get_line() << "|" << get_column() << "\n"; options os = ios.get_options(); @@ -111,26 +117,24 @@ void info_manager::add(std::unique_ptr && d) { add_core(std::move(d)); } -void info_manager::append(std::vector> && v) { +void info_manager::append(std::vector> && vs, bool remove_duplicates) { lock_guard lc(m_mutex); - for (auto & d : v) - add_core(std::move(d)); -} - -void info_manager::append(std::vector & v, bool remove_duplicates) { - lock_guard lc(m_mutex); - std::stable_sort(v.begin(), v.end()); - type_info_data prev; + 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 const & p : v) { - if (!remove_duplicates || first || !p.eq_pos(prev.get_line(), prev.get_column())) { - add_core(std::unique_ptr(new type_info_data(p))); - prev = p; + 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 & v, bool remove_duplicates) { +} + void info_manager::sort() { lock_guard lc(m_mutex); sort_core(); diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h index 3c176a487..dcec244c1 100644 --- a/src/frontends/lean/info_manager.h +++ b/src/frontends/lean/info_manager.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include #include "util/thread.h" #include "kernel/expr.h" +#include "kernel/metavar.h" #include "library/io_state_stream.h" namespace lean { @@ -23,16 +24,25 @@ public: unsigned get_column() const { return m_column; } bool eq_pos(unsigned line, unsigned col) const { return m_line == line && m_column == col; } 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 { +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; }; class overload_info_data : public info_data { @@ -61,8 +71,8 @@ public: info_manager(); void invalidate(unsigned sline); void add(std::unique_ptr && d); - void append(std::vector> && v); - void append(std::vector & v, bool remove_duplicates = true); + void append(std::vector> && v, bool remove_duplicates = true); + void append(std::vector & v, bool remove_duplicates); void sort(); void display(io_state_stream const & ios, unsigned line); };