feat(frontends/lean): add information about synthesized placeholders, closes #39

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

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

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
+    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_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent
-    std::vector<type_info_data> m_pre_info_data;
+    std::vector<std::unique_ptr<info_data>> 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<info_data>(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<info_data>(new synth_info_data(p->first, p->second, r)));
+            }
+        }
+    }
+
     expr visit_constant(expr const & e) {
         declaration d = env().get(const_name(e));
         buffer<level> 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()));
+            p->instantiate(s);
-        infom()->append(m_pre_info_data);
+        // TODO(Leo): implement smarter append
+        infom()->append(std::move(m_pre_info_data), false);
+        m_pre_info_data.clear();
     }
 
     std::tuple<expr, level_param_names> operator()(expr const & e, bool _ensure_type, bool relax_main_opaque) {

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<info_data> && d) {
     add_core(std::move(d));
 }
 
-void info_manager::append(std::vector<std::unique_ptr<info_data>> && v) {
+void info_manager::append(std::vector<std::unique_ptr<info_data>> && vs, bool remove_duplicates) {
     lock_guard<mutex> lc(m_mutex);
-    for (auto & d : v)
+    std::stable_sort(vs.begin(), vs.end(), [](std::unique_ptr<info_data> const & v1, std::unique_ptr<info_data> const & v2) {
-        add_core(std::move(d));
+            return *v1 < *v2; });
-}
+    info_data * prev = nullptr;
-
-void info_manager::append(std::vector<type_info_data> & v, bool remove_duplicates) {
-    lock_guard<mutex> lc(m_mutex);
-    std::stable_sort(v.begin(), v.end());
-    type_info_data prev;
     bool first = true;
-    for (auto const & p : v) {
+    for (auto & v : vs) {
-        if (!remove_duplicates || first || !p.eq_pos(prev.get_line(), prev.get_column())) {
+        if (!remove_duplicates || first || !v->eq_pos(prev->get_line(), prev->get_column())) {
-            add_core(std::unique_ptr<info_data>(new type_info_data(p)));
+            prev = v.get();
-            prev  = p;
+            add_core(std::move(v));
             first = false;
         }
     }
 }
 
+void info_manager::append(std::vector<type_info_data> & v, bool remove_duplicates) {
+}
+
 void info_manager::sort() {
     lock_guard<mutex> lc(m_mutex);
     sort_core();

src/frontends/lean/info_manager.h

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <vector>
 #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<info_data> && d);
-    void append(std::vector<std::unique_ptr<info_data>> && v);
+    void append(std::vector<std::unique_ptr<info_data>> && v, bool remove_duplicates = true);
-    void append(std::vector<type_info_data> & v, bool remove_duplicates = true);
+    void append(std::vector<type_info_data> & v, bool remove_duplicates);
     void sort();
     void display(io_state_stream const & ios, unsigned line);
 };