feat(frontends/lean): add --flyinfo option

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

src/frontends/lean/elaborator.cpp

@@ -26,6 +26,7 @@ Author: Leonardo de Moura
 #include "library/unifier.h"
 #include "library/opaque_hints.h"
 #include "library/locals.h"
+#include "library/deep_copy.h"
 #include "library/tactic/tactic.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "library/error_handling/error_handling.h"
@@ -149,6 +150,9 @@ class elaborator {
     bool                m_check_unassigned; // if true if display error messages if elaborated term still contains metavariables
     bool                m_use_local_instances; // if true class-instance resolution will use the local context
     bool                m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent
+    bool                m_flyinfo;
+    typedef std::pair<pos_info, expr> flyinfo_data;
+    std::vector<flyinfo_data> m_flyinfo_data;
 
     // Set m_ctx to ctx, and make sure m_ctx_buffer and m_ctx_domain_buffer reflect the contents of the new ctx
     void set_ctx(context const & ctx) {
@@ -375,6 +379,7 @@ public:
         m_tc[1] = mk_type_checker_with_hints(env, m_ngen.mk_child(), true);
         m_check_unassigned = check_unassigned;
         m_use_local_instances = get_elaborator_local_instances(ios.get_options());
+        m_flyinfo = ios.get_options().get_bool("flyinfo", false);
         set_ctx(ctx);
     }
 
@@ -865,6 +870,16 @@ public:
         }
     }
 
+    /** \brief Store the pair (pos(e), type(r)) in the flyinfo_data if m_flyinfo is true. */
+    void save_flyinfo_data(expr const & e, expr const & r) {
+        if (m_flyinfo && m_pos_provider) {
+            auto p = m_pos_provider->get_pos_info(e);
+            type_checker::scope scope(*m_tc[m_relax_main_opaque]);
+            expr t = m_tc[m_relax_main_opaque]->infer(r);
+            m_flyinfo_data.push_back(mk_pair(p, t));
+        }
+    }
+
     expr visit_constant(expr const & e) {
         auto it = m_cache.find(e);
         if (it != m_cache.end()) {
@@ -930,13 +945,39 @@ public:
         m_ctx_buffer.push_back(l);
     }
 
+    /** \brief Similar to instantiate_rev, but assumes that subst contains only local constants.
+        When replacing a variable with a local, we copy the local constant and inherit the tag
+        associated with the variable. This is a trick for getter better error messages */
+    expr instantiate_rev_locals(expr const & a, unsigned n, expr const * subst) {
+        if (closed(a))
+            return a;
+        return replace(a, [=](expr const & m, unsigned offset) -> optional<expr> {
+                if (offset >= get_free_var_range(m))
+                    return some_expr(m); // expression m does not contain free variables with idx >= offset
+                if (is_var(m)) {
+                    unsigned vidx = var_idx(m);
+                    if (vidx >= offset) {
+                        unsigned h = offset + n;
+                        if (h < offset /* overflow, h is bigger than any vidx */ || vidx < h) {
+                            expr local = subst[n - (vidx - offset) - 1];
+                            lean_assert(is_local(local));
+                            return some_expr(copy_tag(m, copy(local)));
+                        } else {
+                            return some_expr(copy_tag(m, mk_var(vidx - n)));
+                        }
+                    }
+                }
+                return none_expr();
+            });
+    }
+
     expr visit_binding(expr e, expr_kind k) {
         scope_ctx scope(*this);
         buffer<expr> ds, ls, es;
         while (e.kind() == k) {
             es.push_back(e);
             expr d   = binding_domain(e);
-            d = instantiate_rev(d, ls.size(), ls.data());
+            d = instantiate_rev_locals(d, ls.size(), ls.data());
             d = ensure_type(visit_expecting_type(d));
             ds.push_back(d);
             expr l   = mk_local(binding_name(e), d, binding_info(e));
@@ -946,7 +987,7 @@ public:
             e = binding_body(e);
         }
         lean_assert(ls.size() == es.size() && ls.size() == ds.size());
-        e = instantiate_rev(e, ls.size(), ls.data());
+        e = instantiate_rev_locals(e, ls.size(), ls.data());
         e = (k == expr_kind::Pi) ? ensure_type(visit_expecting_type(e)) : visit(e);
         e = abstract_locals(e, ls.size(), ls.data());
         unsigned i = ls.size();
@@ -1007,6 +1048,8 @@ public:
                 }
             }
         }
+        if (is_constant(e) || is_local(e))
+            save_flyinfo_data(e, r);
         return r;
     }
 
@@ -1188,6 +1231,16 @@ public:
         return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end()));
     }
 
+    void display_flyinfo(substitution const & _s) {
+        substitution s = _s;
+        for (auto p : m_flyinfo_data) {
+            auto out = regular(m_env, m_ios);
+            flyinfo_scope info(out);
+            out << m_pos_provider->get_file_name() << ":" << p.first.first << ":" << p.first.second << ": type\n";
+            out << s.instantiate(p.second) << endl;
+        }
+    }
+
     std::tuple<expr, level_param_names> operator()(expr const & e, bool _ensure_type, bool relax_main_opaque) {
         flet<bool> set_relax(m_relax_main_opaque, relax_main_opaque && !get_hide_main_opaque(m_env));
         expr r  = visit(e);
@@ -1196,7 +1249,9 @@ public:
         auto p  = solve().pull();
         lean_assert(p);
         substitution s = p->first;
-        return apply(s, r);
+        auto result = apply(s, r);
+        display_flyinfo(s);
+        return result;
     }
 
     std::tuple<expr, expr, level_param_names> operator()(expr const & t, expr const & v, name const & n, bool is_opaque) {
@@ -1218,6 +1273,7 @@ public:
         buffer<name> new_params;
         expr new_r_t = apply(s, r_t, univ_params, new_params);
         expr new_r_v = apply(s, r_v, univ_params, new_params);
+        display_flyinfo(s);
         return std::make_tuple(new_r_t, new_r_v, to_list(new_params.begin(), new_params.end()));
     }
 };

src/library/error_handling/error_handling.cpp

@@ -18,11 +18,20 @@ Author: Leonardo de Moura
 namespace lean {
 flycheck_scope::flycheck_scope(io_state_stream const & ios, char const * kind):
     m_ios(ios),
-    m_use_flycheck(m_ios.get_options().get_bool("use_flycheck", false)) {
+    m_flycheck(m_ios.get_options().get_bool("flycheck", false)) {
-    if (m_use_flycheck) m_ios << "FLYCHECK_BEGIN " << kind << endl;
+    if (m_flycheck) m_ios << "FLYCHECK_BEGIN " << kind << endl;
 }
 flycheck_scope::~flycheck_scope() {
-    if (m_use_flycheck) m_ios << "FLYCHECK_END" << endl;
+    if (m_flycheck) m_ios << "FLYCHECK_END" << endl;
+}
+
+flyinfo_scope::flyinfo_scope(io_state_stream const & ios):
+    m_ios(ios),
+    m_flyinfo(m_ios.get_options().get_bool("flyinfo", false)) {
+    if (m_flyinfo) m_ios << "FLYCHECK_BEGIN INFO" << endl;
+}
+flyinfo_scope::~flyinfo_scope() {
+    if (m_flyinfo) m_ios << "FLYCHECK_END" << endl;
 }
 
 void display_error_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) {

src/library/error_handling/error_handling.h

@@ -13,7 +13,7 @@ namespace lean {
 /** \brief Auxiliary object for "inserting" delimiters for flycheck */
 class flycheck_scope {
     io_state_stream const & m_ios;
-    bool                    m_use_flycheck;
+    bool                    m_flycheck;
 public:
     flycheck_scope(io_state_stream const & ios, char const * kind);
     ~flycheck_scope();
@@ -27,8 +27,12 @@ struct flycheck_warning : public flycheck_scope {
     flycheck_warning(io_state_stream const & ios):flycheck_scope(ios, "WARNING") {}
 };
 
-struct flycheck_info : public flycheck_scope {
+class flyinfo_scope {
-    flycheck_info(io_state_stream const & ios):flycheck_scope(ios, "INFO") {}
+    io_state_stream const & m_ios;
+    bool                    m_flyinfo;
+public:
+    flyinfo_scope(io_state_stream const & ios);
+    ~flyinfo_scope();
 };
 
 /**

src/library/io_state_stream.cpp

@@ -14,7 +14,7 @@ io_state_stream const & operator<<(io_state_stream const & out, endl_class) {
 
 io_state_stream const & operator<<(io_state_stream const & out, expr const & e) {
     options const & opts = out.get_options();
-    out.get_stream() << mk_pair(out.get_formatter()(e), opts);
+    out.get_stream() << mk_pair(group(out.get_formatter()(e)), opts);
     return out;
 }
 

src/shell/lean.cpp

@@ -76,6 +76,7 @@ static void display_help(std::ostream & out) {
     std::cout << "  --threads=num -j  number of threads used to process lean files\n";
     std::cout << "  --deps            just print dependencies of a Lean input\n";
     std::cout << "  --flycheck        print structured error message for flycheck\n";
+    std::cout << "  --flyinfo         print structured typing information for editor\n";
 #if defined(LEAN_USE_BOOST)
     std::cout << "  --tstack=num -s   thread stack size in Kb\n";
 #endif
@@ -111,6 +112,7 @@ static struct option g_long_options[] = {
     {"threads",     required_argument, 0, 'j'},
     {"deps",        no_argument,       0, 'D'},
     {"flycheck",    no_argument,       0, 'F'},
+    {"flyinfo",     no_argument,       0, 'I'},
 #if defined(LEAN_USE_BOOST)
     {"tstack",      required_argument, 0, 's'},
 #endif
@@ -118,9 +120,9 @@ static struct option g_long_options[] = {
 };
 
 #if defined(LEAN_USE_BOOST)
-static char const * g_opt_str = "FDHiqlupgvhj:012c:012s:012t:012o:";
+static char const * g_opt_str = "IFDHiqlupgvhj:012c:012s:012t:012o:";
 #else
-static char const * g_opt_str = "FDHiqlupgvhj:012c:012t:012o:";
+static char const * g_opt_str = "IFDHiqlupgvhj:012c:012t:012o:";
 #endif
 
 enum class lean_mode { Standard, HoTT };
@@ -133,7 +135,8 @@ int main(int argc, char ** argv) {
     bool quiet           = false;
     bool interactive     = false;
     bool only_deps       = false;
-    bool use_flycheck    = false;
+    bool flycheck        = false;
+    bool flyinfo         = false;
     lean_mode mode       = lean_mode::Standard;
     unsigned num_threads = 1;
     std::string output;
@@ -191,7 +194,10 @@ int main(int argc, char ** argv) {
             only_deps = true;
             break;
         case 'F':
-            use_flycheck = true;
+            flycheck = true;
+            break;
+        case 'I':
+            flyinfo = true;
             break;
         default:
             std::cerr << "Unknown command line option\n";
@@ -204,8 +210,10 @@ int main(int argc, char ** argv) {
     io_state ios(lean::mk_pretty_formatter_factory());
     if (quiet)
         ios.set_option("verbose", false);
-    if (use_flycheck)
+    if (flycheck)
-        ios.set_option("use_flycheck", true);
+        ios.set_option("flycheck", true);
+    if (flyinfo)
+        ios.set_option("flyinfo", true);
     script_state S = lean::get_thread_script_state();
     set_environment set1(S, env);
     set_io_state    set2(S, ios);