michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean): improve COERCION info

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-03 09:34:13 -07:00
parent 8c3d839968
commit ef1912eddf
3 changed files with 25 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/frontends/lean/elaborator.cpp
View file

@ -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<expr> 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<expr> 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); });
}

18
src/frontends/lean/info_manager.cpp
View file

@ -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<mutex> 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) {

2
src/frontends/lean/info_manager.h
View file

@ -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);