diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index d6d2b47e3..d42f6b1c1 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -33,6 +33,7 @@ Author: Leonardo de Moura #include "frontends/lean/local_decls.h" #include "frontends/lean/class.h" #include "frontends/lean/tactic_hint.h" +#include "frontends/lean/info_manager.h" #ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES #define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true @@ -120,16 +121,7 @@ public: expr operator()(expr const & e) { return apply(e); } }; -typedef std::pair flyinfo_data; - -struct flyinfo_data_lt { - bool operator()(flyinfo_data const & d1, flyinfo_data const & d2) const { - if (d1.first.first != d2.first.first) - return d1.first.first < d2.first.first; - else - return d1.first.second < d2.first.second; - } -}; +typedef std::pair pre_info_data; /** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */ list get_local_instances(list const & ctx, name const & cls_name) { @@ -317,8 +309,8 @@ 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; - std::vector m_flyinfo_data; + info_manager * m_info_manager; + std::vector m_info_data; struct scope_ctx { context::scope m_scope1; @@ -536,18 +528,18 @@ class elaborator { public: elaborator(environment const & env, local_decls const & lls, list const & ctx, io_state const & ios, name_generator const & ngen, - pos_info_provider * pp, bool check_unassigned): + pos_info_provider * pp, bool check_unassigned, info_manager * info): m_env(env), m_lls(lls), m_ios(ios), m_ngen(ngen), m_context(m_ngen, m_mvar2meta, ctx), m_full_context(m_ngen, m_mvar2meta, ctx), - m_pos_provider(pp) { + m_pos_provider(pp), + m_info_manager(info) { m_relax_main_opaque = false; m_tc[0] = mk_type_checker_with_hints(env, m_ngen.mk_child(), false); 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); } expr mk_local(name const & n, expr const & t, binder_info const & bi) { @@ -898,8 +890,8 @@ public: first = false; } if (!first) { - // we save the flyinfo data again for application of functions with strict implicit arguments - replace_flyinfo_data(get_app_fn(e), f); + // we save the info data again for application of functions with strict implicit arguments + replace_info_data(get_app_fn(e), f); } } expr d_type = binding_domain(f_type); @@ -949,27 +941,27 @@ public: } } - /** \brief Store the pair (pos(e), type(r)) in the flyinfo_data if m_flyinfo is true. */ - void save_flyinfo_data_core(expr const & e, expr const & r, bool replace) { - if (m_flyinfo && m_pos_provider && (is_constant(e) || is_local(e) || is_placeholder(e))) { + /** \brief Store the pair (pos(e), type(r)) in the info_data if m_info_manager is available. */ + void save_info_data_core(expr const & e, expr const & r, bool replace) { + if (m_info_manager && m_pos_provider && (is_constant(e) || is_local(e) || is_placeholder(e))) { if (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); if (replace) { - while (!m_flyinfo_data.empty() && m_flyinfo_data.back().first == *p) - m_flyinfo_data.pop_back(); + while (!m_info_data.empty() && m_info_data.back().first == *p) + m_info_data.pop_back(); } - m_flyinfo_data.push_back(mk_pair(*p, t)); + m_info_data.push_back(mk_pair(*p, t)); } } } - void save_flyinfo_data(expr const & e, expr const & r) { - save_flyinfo_data_core(e, r, false); + void save_info_data(expr const & e, expr const & r) { + save_info_data_core(e, r, false); } - void replace_flyinfo_data(expr const & e, expr const & r) { - save_flyinfo_data_core(e, r, true); + void replace_info_data(expr const & e, expr const & r) { + save_info_data_core(e, r, true); } expr visit_constant(expr const & e) { @@ -1127,7 +1119,7 @@ public: } } } - save_flyinfo_data(b, r); + save_info_data(b, r); return r; } @@ -1309,30 +1301,12 @@ public: return std::make_tuple(r, to_list(new_ps.begin(), new_ps.end())); } - void instantiate_flyinfo(substitution s) { - for (auto & p : m_flyinfo_data) { + void copy_info_to_manager(substitution s) { + if (!m_info_manager) + return; + for (auto & p : m_info_data) { p.second = s.instantiate(p.second); - } - std::stable_sort(m_flyinfo_data.begin(), m_flyinfo_data.end(), flyinfo_data_lt()); - } - - void display_flyinfo_data(flyinfo_data const & p) { - auto out = regular(m_env, m_ios); - flyinfo_scope info(out); - out << m_pos_provider->get_file_name() << ":" << p.first.first << ":" << p.first.second+1 - << ": type\n" << p.second << endl; - } - - void display_flyinfo(substitution const & s) { - instantiate_flyinfo(s); - flyinfo_data prev; - bool first = true; - for (auto const & p : m_flyinfo_data) { - if (first || p.first != prev.first) { - display_flyinfo_data(p); - prev = p; - } - first = false; + m_info_manager->add(std::unique_ptr(new type_info_data(p.first.first, p.first.second, p.second))); } } @@ -1345,7 +1319,7 @@ public: lean_assert(p); substitution s = p->first; auto result = apply(s, r); - display_flyinfo(s); + copy_info_to_manager(s); return result; } @@ -1368,7 +1342,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); + copy_info_to_manager(s); return std::make_tuple(new_r_t, new_r_v, to_list(new_params.begin(), new_params.end())); } }; @@ -1377,12 +1351,14 @@ static name g_tmp_prefix = name::mk_internal_unique_name(); std::tuple elaborate(environment const & env, local_decls const & lls, list const & ctx, io_state const & ios, expr const & e, bool relax_main_opaque, - pos_info_provider * pp, bool check_unassigned, bool ensure_type) { - return elaborator(env, lls, ctx, ios, name_generator(g_tmp_prefix), pp, check_unassigned)(e, ensure_type, relax_main_opaque); + pos_info_provider * pp, bool check_unassigned, bool ensure_type, + info_manager * info) { + return elaborator(env, lls, ctx, ios, name_generator(g_tmp_prefix), pp, check_unassigned, info)(e, ensure_type, relax_main_opaque); } std::tuple elaborate(environment const & env, local_decls const & lls, io_state const & ios, - name const & n, expr const & t, expr const & v, bool is_opaque, pos_info_provider * pp) { - return elaborator(env, lls, list(), ios, name_generator(g_tmp_prefix), pp, true)(t, v, n, is_opaque); + name const & n, expr const & t, expr const & v, bool is_opaque, pos_info_provider * pp, + info_manager * info) { + return elaborator(env, lls, list(), ios, name_generator(g_tmp_prefix), pp, true, info)(t, v, n, is_opaque); } } diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 128853e3b..742396d50 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -11,12 +11,14 @@ Author: Leonardo de Moura #include "kernel/metavar.h" #include "library/io_state.h" #include "frontends/lean/local_decls.h" +#include "frontends/lean/info_manager.h" namespace lean { std::tuple elaborate(environment const & env, local_decls const & lls, list const & ctx, io_state const & ios, expr const & e, bool relax_main_opaque, - pos_info_provider * pp = nullptr, bool check_unassigned = true, bool ensure_type = false); + pos_info_provider * pp = nullptr, bool check_unassigned = true, + bool ensure_type = false, info_manager * info = nullptr); std::tuple elaborate(environment const & env, local_decls const & lls, io_state const & ios, name const & n, expr const & t, expr const & v, - bool is_opaque, pos_info_provider * pp = nullptr); + bool is_opaque, pos_info_provider * pp = nullptr, info_manager * info = nullptr); } diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index b5c50d7c9..52560596e 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -98,7 +98,7 @@ void info_manager::add_core(std::unique_ptr && d) { m_sorted_upto = 1; } 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]) { + } 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)); diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h index 724a388df..ac5c13694 100644 --- a/src/frontends/lean/info_manager.h +++ b/src/frontends/lean/info_manager.h @@ -17,6 +17,7 @@ class info_data { unsigned m_column; public: info_data(unsigned l, unsigned c):m_line(l), m_column(c) {} + virtual ~info_data() {} unsigned get_line() const { return m_line; } unsigned get_column() const { return m_column; } virtual void display(io_state_stream const & ios) const = 0; diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 7afb30d62..46d3bc0d4 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -506,32 +506,35 @@ std::tuple parser::elaborate_relaxed(expr const & e, li parser_pos_provider pp = get_pos_provider(); bool relax = true; bool check_unassigned = false; - return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, relax, &pp, check_unassigned); + bool ensure_type = false; + return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, relax, &pp, check_unassigned, ensure_type, + m_info_manager); } std::tuple parser::elaborate_type(expr const & e, list const & ctx) { parser_pos_provider pp = get_pos_provider(); bool relax = false; - bool ensure_type = true; bool check_unassigned = true; - return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, relax, &pp, check_unassigned, ensure_type); + bool ensure_type = true; + return ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, relax, &pp, check_unassigned, ensure_type, + m_info_manager); } std::tuple parser::elaborate_at(environment const & env, expr const & e) { parser_pos_provider pp = get_pos_provider(); bool relax = false; - return ::lean::elaborate(env, m_local_level_decls, list(), m_ios, e, relax, &pp); + return ::lean::elaborate(env, m_local_level_decls, list(), m_ios, e, relax, &pp, m_info_manager); } std::tuple parser::elaborate_definition(name const & n, expr const & t, expr const & v, bool is_opaque) { parser_pos_provider pp = get_pos_provider(); - return ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, is_opaque, &pp); + return ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, is_opaque, &pp, m_info_manager); } std::tuple parser::elaborate_definition_at(environment const & env, local_level_decls const & lls, name const & n, expr const & t, expr const & v, bool is_opaque) { parser_pos_provider pp = get_pos_provider(); - return ::lean::elaborate(env, lls, m_ios, n, t, v, is_opaque, &pp); + return ::lean::elaborate(env, lls, m_ios, n, t, v, is_opaque, &pp, m_info_manager); } [[ noreturn ]] void throw_invalid_open_binder(pos_info const & pos) { diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 29634582a..afc90fbc8 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -76,7 +76,6 @@ 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 @@ -112,7 +111,6 @@ 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 @@ -120,9 +118,9 @@ static struct option g_long_options[] = { }; #if defined(LEAN_USE_BOOST) -static char const * g_opt_str = "IFDHSqlupgvhj:012c:012s:012t:012o:"; +static char const * g_opt_str = "FDHSqlupgvhj:012c:012s:012t:012o:"; #else -static char const * g_opt_str = "IFDHSqlupgvhj:012c:012t:012o:"; +static char const * g_opt_str = "FDHSqlupgvhj:012c:012t:012o:"; #endif enum class lean_mode { Standard, HoTT }; @@ -136,7 +134,6 @@ int main(int argc, char ** argv) { bool server = false; bool only_deps = false; bool flycheck = false; - bool flyinfo = false; lean_mode mode = lean_mode::Standard; unsigned num_threads = 1; std::string output; @@ -196,9 +193,6 @@ int main(int argc, char ** argv) { case 'F': flycheck = true; break; - case 'I': - flyinfo = true; - break; default: std::cerr << "Unknown command line option\n"; display_help(std::cerr); @@ -212,8 +206,6 @@ int main(int argc, char ** argv) { ios.set_option("verbose", false); 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);