From c6f3232f81f2a946f2b638d1fed72f114680140e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 Aug 2014 21:56:57 -0700 Subject: [PATCH] feat(frontends/lean): provide 'partial' type information even when there are type errors Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 14 +----- src/frontends/lean/info_manager.cpp | 14 ++++++ src/frontends/lean/info_manager.h | 1 + src/frontends/lean/parser.cpp | 76 ++++++++++++++++++++++++----- src/frontends/lean/parser.h | 2 + 5 files changed, 83 insertions(+), 24 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 4d323deb1..4d4b9b2be 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1302,19 +1302,9 @@ public: void copy_info_to_manager(substitution s) { if (!m_info_manager) return; - for (auto & p : m_pre_info_data) { + for (auto & p : m_pre_info_data) p = type_info_data(p.get_line(), p.get_column(), s.instantiate(p.get_type())); - } - std::stable_sort(m_pre_info_data.begin(), m_pre_info_data.end()); - type_info_data prev; - bool first = true; - for (auto const & p : m_pre_info_data) { - if (first || !p.eq_pos(prev.get_line(), prev.get_column())) { - m_info_manager->add(std::unique_ptr(new type_info_data(p))); - prev = p; - first = false; - } - } + m_info_manager->append(m_pre_info_data); } 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 52560596e..804a3b07f 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -115,6 +115,20 @@ void info_manager::append(std::vector> && 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; + 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; + first = false; + } + } +} + 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 2d17e426b..3c176a487 100644 --- a/src/frontends/lean/info_manager.h +++ b/src/frontends/lean/info_manager.h @@ -62,6 +62,7 @@ public: 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 sort(); void display(io_state_stream const & ios, unsigned line); }; diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index ccc4694bd..eb6d09b6b 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -507,8 +507,10 @@ std::tuple parser::elaborate_relaxed(expr const & e, li bool relax = true; bool check_unassigned = false; 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); + auto r = ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, relax, &pp, check_unassigned, ensure_type, + m_info_manager); + m_pre_info_data.clear(); + return r; } std::tuple parser::elaborate_type(expr const & e, list const & ctx) { @@ -516,25 +518,33 @@ std::tuple parser::elaborate_type(expr const & e, list< bool relax = false; bool check_unassigned = true; 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); + auto r = ::lean::elaborate(m_env, m_local_level_decls, ctx, m_ios, e, relax, &pp, check_unassigned, ensure_type, + m_info_manager); + m_pre_info_data.clear(); + return r; } 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, m_info_manager); + auto r = ::lean::elaborate(env, m_local_level_decls, list(), m_ios, e, relax, &pp, m_info_manager); + m_pre_info_data.clear(); + return r; } 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, m_info_manager); + auto r = ::lean::elaborate(m_env, m_local_level_decls, m_ios, n, t, v, is_opaque, &pp, m_info_manager); + m_pre_info_data.clear(); + return r; } 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, m_info_manager); + auto r = ::lean::elaborate(env, lls, m_ios, n, t, v, is_opaque, &pp, m_info_manager); + m_pre_info_data.clear(); + return r; } [[ noreturn ]] void throw_invalid_open_binder(pos_info const & pos) { @@ -842,6 +852,7 @@ expr parser::parse_notation(parse_table t, expr * left) { } expr r = save_pos(mk_choice(cs.size(), cs.data()), p); save_overload(r); + save_type_info(r); return r; } @@ -870,18 +881,26 @@ expr parser::id_to_expr(name const & id, pos_info const & p) { if (id.is_atomic()) { // locals - if (auto it1 = m_local_decls.find(id)) - return copy_with_new_pos(propagate_levels(*it1, ls), p); + if (auto it1 = m_local_decls.find(id)) { + auto r = copy_with_new_pos(propagate_levels(*it1, ls), p); + save_type_info(r); + return r; + } } else { lean_assert(!id.is_atomic()); name new_id = remove_root_prefix(id); if (m_env.find(new_id)) { - return save_pos(mk_constant(new_id, ls), p); + auto r = save_pos(mk_constant(new_id, ls), p); + save_type_info(r); + return r; } else { for (name const & ns : get_namespaces(m_env)) { auto new_id = ns + id; - if (m_env.find(new_id)) - return save_pos(mk_constant(new_id, ls), p); + if (m_env.find(new_id)) { + auto r = save_pos(mk_constant(new_id, ls), p); + save_type_info(r); + return r; + } } } } @@ -906,6 +925,7 @@ expr parser::id_to_expr(name const & id, pos_info const & p) { r = save_pos(mk_constant(get_namespace(m_env) + id, ls), p); if (!r) throw parser_error(sstream() << "unknown identifier '" << id << "'", p); + save_type_info(*r); return *r; } @@ -1176,6 +1196,11 @@ void parser::save_snapshot() { return; if (m_snapshot_vector->empty() || static_cast(m_snapshot_vector->back().m_line) != m_scanner.get_line()) m_snapshot_vector->push_back(snapshot(m_env, m_local_level_decls, m_local_decls, m_ios.get_options(), m_scanner.get_line())); + // if elaborator failed, then m_pre_info_data contains type information before elaboration. + if (m_info_manager) { + m_info_manager->append(m_pre_info_data, false); + m_pre_info_data.clear(); + } } void parser::save_overload(expr const & e) { @@ -1185,6 +1210,33 @@ void parser::save_overload(expr const & e) { m_info_manager->add(std::unique_ptr(new overload_info_data(p.first, p.second, e))); } +void parser::save_type_info(expr const & e) { + if (!m_info_manager) + return; + if (is_explicit(e)) { + save_type_info(get_explicit_arg(e)); + } else if (is_implicit(e)) { + save_type_info(get_implicit_arg(e)); + } else if (is_choice(e)) { + for (unsigned i = 0; i < get_num_choices(e); i++) + save_type_info(get_choice(e, i)); + } else if (is_app(e)) { + save_type_info(get_app_fn(e)); + } else if (is_constant(e)) { + auto d = m_env.find(const_name(e)); + if (!d) + return; + auto p = pos_of(e); + m_pre_info_data.push_back(type_info_data(p.first, p.second, d->get_type())); + } else if (is_local(e)) { + auto p = pos_of(e); + expr t = mlocal_type(e); + if (is_meta(t)) + return; + m_pre_info_data.push_back(type_info_data(p.first, p.second, t)); + } +} + bool parse_commands(environment & env, io_state & ios, std::istream & in, char const * strm_name, bool use_exceptions, unsigned num_threads) { parser p(env, ios, in, strm_name, use_exceptions, num_threads); diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 12c6b884d..157be62c9 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -88,6 +88,7 @@ class parser { // info support snapshot_vector * m_snapshot_vector; info_manager * m_info_manager; + std::vector m_pre_info_data; // type information before elaboration void display_warning_pos(unsigned line, unsigned pos); void display_warning_pos(pos_info p); @@ -154,6 +155,7 @@ class parser { void save_snapshot(); void save_overload(expr const & e); + void save_type_info(expr const & e); public: parser(environment const & env, io_state const & ios,