diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 3ba2b1c59..dc558553a 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/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 flyinfo_data; + std::vector 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 { + 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 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 operator()(expr const & e, bool _ensure_type, bool relax_main_opaque) { flet 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 operator()(expr const & t, expr const & v, name const & n, bool is_opaque) { @@ -1218,6 +1273,7 @@ public: buffer 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())); } }; diff --git a/src/library/error_handling/error_handling.cpp b/src/library/error_handling/error_handling.cpp index 322f6d785..cb6ae9432 100644 --- a/src/library/error_handling/error_handling.cpp +++ b/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)) { - if (m_use_flycheck) m_ios << "FLYCHECK_BEGIN " << kind << endl; + m_flycheck(m_ios.get_options().get_bool("flycheck", false)) { + 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) { diff --git a/src/library/error_handling/error_handling.h b/src/library/error_handling/error_handling.h index a79aee2a7..d00c43111 100644 --- a/src/library/error_handling/error_handling.h +++ b/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 { - flycheck_info(io_state_stream const & ios):flycheck_scope(ios, "INFO") {} +class flyinfo_scope { + io_state_stream const & m_ios; + bool m_flyinfo; +public: + flyinfo_scope(io_state_stream const & ios); + ~flyinfo_scope(); }; /** diff --git a/src/library/io_state_stream.cpp b/src/library/io_state_stream.cpp index a9520047c..3a8fcf234 100644 --- a/src/library/io_state_stream.cpp +++ b/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; } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 592b827f0..a53dca904 100644 --- a/src/shell/lean.cpp +++ b/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) - ios.set_option("use_flycheck", true); + if (flycheck) + 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);