From ef1912eddf47ff217554872471996bde1a44508e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Sep 2014 09:34:13 -0700 Subject: [PATCH] feat(frontends/lean): improve COERCION info Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 23 ++++++++++++++--------- src/frontends/lean/info_manager.cpp | 18 ++++++++++-------- src/frontends/lean/info_manager.h | 2 +- 3 files changed, 25 insertions(+), 18 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index dc1d465aae..cdb940f9f3 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -587,8 +587,10 @@ public: */ void save_coercion_info(expr const & e, expr const & c) { if (!m_noinfo && infom() && pip()) { - if (auto p = pip()->get_pos_info(e)) - m_pre_info_data.add_coercion_info(p->first, p->second, c); + if (auto p = pip()->get_pos_info(e)) { + expr t = m_tc[m_relax_main_opaque]->infer(c).first; + m_pre_info_data.add_coercion_info(p->first, p->second, c, t); + } } } @@ -762,9 +764,10 @@ public: // try coercion to function-class optional c = get_coercion_to_fun(env(), f_type); if (c) { - save_coercion_info(f, *c); + expr old_f = f; f = mk_app(*c, f, f.get_tag()); f_type = infer_type(f, cs); + save_coercion_info(old_f, f); lean_assert(is_pi(f_type)); } else { throw_kernel_exception(env(), f, [=](formatter const & fmt) { return pp_function_expected(fmt, f); }); @@ -792,8 +795,9 @@ public: expr const & d_cls = get_app_fn(d_type); if (is_constant(d_cls)) { if (auto c = get_coercion(env(), a_type, const_name(d_cls))) { - save_coercion_info(a, *c); - return mk_app(*c, a, a.get_tag()); + expr r = mk_app(*c, a, a.get_tag()); + save_coercion_info(a, r); + return r; } else { erase_coercion_info(a); } @@ -822,7 +826,7 @@ public: } else if (m_coercions) { expr c = head(m_coercions); m_coercions = tail(m_coercions); - m_elab.save_coercion_info(m_arg, c); + m_elab.save_coercion_info(m_arg, ::lean::mk_app(c, m_arg)); } auto r = head(m_choices); m_choices = tail(m_choices); @@ -894,8 +898,8 @@ public: expr const & d_cls = get_app_fn(new_d_type); if (is_constant(d_cls)) { if (auto c = get_coercion(env(), new_a_type, const_name(d_cls))) { - save_coercion_info(a, *c); new_a = mk_app(*c, a, a.get_tag()); + save_coercion_info(a, new_a); } else { erase_coercion_info(a); } @@ -1083,8 +1087,9 @@ public: } optional c = get_coercion_to_sort(env(), t); if (c) { - save_coercion_info(e, *c); - return mk_app(*c, e, e.get_tag()); + expr r = mk_app(*c, e, e.get_tag()); + save_coercion_info(e, r); + return r; } throw_kernel_exception(env(), e, [=](formatter const & fmt) { return pp_type_expected(fmt, e); }); } diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index 7c23683cec..ca6992ea68 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -144,9 +144,11 @@ public: }; class coercion_info_data : public info_data_cell { - expr m_coercion; + expr m_expr; + expr m_type; public: - coercion_info_data(unsigned c, expr const & e):info_data_cell(c), m_coercion(e) {} + coercion_info_data(unsigned c, expr const & e, expr const & t): + info_data_cell(c), m_expr(e), m_type(t) {} virtual info_kind kind() const { return info_kind::Coercion; } @@ -154,7 +156,7 @@ public: ios << "-- COERCION|" << line << "|" << get_column() << "\n"; options os = ios.get_options(); os = os.update(get_pp_coercion_option_name(), true); - ios.update_options(os) << m_coercion << endl; + ios.update_options(os) << m_expr << endl << "--" << endl << m_type << endl; ios << "-- ACK" << endl; } }; @@ -190,7 +192,7 @@ public: info_data mk_type_info(unsigned c, expr const & e) { return info_data(new type_info_data(c, e)); } info_data mk_synth_info(unsigned c, expr const & e) { return info_data(new synth_info_data(c, e)); } info_data mk_overload_info(unsigned c, expr const & e) { return info_data(new overload_info_data(c, e)); } -info_data mk_coercion_info(unsigned c, expr const & e) { return info_data(new coercion_info_data(c, e)); } +info_data mk_coercion_info(unsigned c, expr const & e, expr const & t) { return info_data(new coercion_info_data(c, e, t)); } info_data mk_symbol_info(unsigned c, name const & s) { return info_data(new symbol_info_data(c, s)); } info_data mk_identifier_info(unsigned c, name const & full_id) { return info_data(new identifier_info_data(c, full_id)); } @@ -278,12 +280,12 @@ struct info_manager::imp { m_line_data[l].insert(mk_overload_info(c, e)); } - void add_coercion_info(unsigned l, unsigned c, expr const & e) { + void add_coercion_info(unsigned l, unsigned c, expr const & e, expr const & t) { lock_guard lc(m_mutex); if (m_block_new_info) return; synch_line(l); - m_line_data[l].insert(mk_coercion_info(c, e)); + m_line_data[l].insert(mk_coercion_info(c, e, t)); } void erase_coercion_info(unsigned l, unsigned c) { @@ -291,7 +293,7 @@ struct info_manager::imp { if (m_block_new_info) return; synch_line(l); - m_line_data[l].erase(mk_coercion_info(c, expr())); + m_line_data[l].erase(mk_coercion_info(c, expr(), expr())); } void add_symbol_info(unsigned l, unsigned c, name const & s) { @@ -538,7 +540,7 @@ info_manager::~info_manager() {} void info_manager::add_type_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_type_info(l, c, e); } void info_manager::add_synth_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_synth_info(l, c, e); } void info_manager::add_overload_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_overload_info(l, c, e); } -void info_manager::add_coercion_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_coercion_info(l, c, e); } +void info_manager::add_coercion_info(unsigned l, unsigned c, expr const & e, expr const & t) { m_ptr->add_coercion_info(l, c, e, t); } void info_manager::erase_coercion_info(unsigned l, unsigned c) { m_ptr->erase_coercion_info(l, c); } void info_manager::add_symbol_info(unsigned l, unsigned c, name const & s) { m_ptr->add_symbol_info(l, c, s); } void info_manager::add_identifier_info(unsigned l, unsigned c, name const & full_id) { diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h index 92124cca46..08b8e6e5f1 100644 --- a/src/frontends/lean/info_manager.h +++ b/src/frontends/lean/info_manager.h @@ -21,7 +21,7 @@ public: void add_type_info(unsigned l, unsigned c, expr const & e); void add_synth_info(unsigned l, unsigned c, expr const & e); void add_overload_info(unsigned l, unsigned c, expr const & e); - void add_coercion_info(unsigned l, unsigned c, expr const & e); + void add_coercion_info(unsigned l, unsigned c, expr const & e, expr const & t); void erase_coercion_info(unsigned l, unsigned c); void add_symbol_info(unsigned l, unsigned c, name const & n); void add_identifier_info(unsigned l, unsigned c, name const & full_id);