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

fix(frontends/lean): remove duplicate info entries, fix bug in save_overload

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-06 21:23:37 -07:00
parent 8d9ca4c4ea
commit 1cbf40a5d2
3 changed files with 21 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -121,8 +121,6 @@ public:
expr operator()(expr const & e) { return apply(e); }
};
typedef std::pair<pos_info, expr> pre_info_data;
/** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */
list<expr> get_local_instances(list<expr> const & ctx, name const & cls_name) {
buffer<expr> buffer;
@ -310,7 +308,7 @@ class elaborator {
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
info_manager * m_info_manager;
std::vector<pre_info_data> m_info_data;
std::vector<type_info_data> m_pre_info_data;
struct scope_ctx {
context::scope m_scope1;
@ -948,10 +946,10 @@ public:
type_checker::scope scope(*m_tc[m_relax_main_opaque]);
expr t = m_tc[m_relax_main_opaque]->infer(r);
if (replace) {
while (!m_info_data.empty() && m_info_data.back().first == *p)
m_info_data.pop_back();
while (!m_pre_info_data.empty() && m_pre_info_data.back().eq_pos(p->first, p->second))
m_pre_info_data.pop_back();
}
m_info_data.push_back(mk_pair(*p, t));
m_pre_info_data.push_back(type_info_data(p->first, p->second, t));
}
}
}
@ -1304,9 +1302,18 @@ public:
void copy_info_to_manager(substitution s) {
if (!m_info_manager)
return;
for (auto & p : m_info_data) {
p.second = s.instantiate(p.second);
m_info_manager->add(std::unique_ptr<info_data>(new type_info_data(p.first.first, p.first.second, p.second)));
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<info_data>(new type_info_data(p)));
prev = p;
first = false;
}
}
}

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

@ -16,10 +16,12 @@ class info_data {
unsigned m_line;
unsigned m_column;
public:
info_data():m_line(0), m_column(0) {}
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; }
bool eq_pos(unsigned line, unsigned col) const { return m_line == line && m_column == col; }
virtual void display(io_state_stream const & ios) const = 0;
};
bool operator<(info_data const & i1, info_data const & i2);
@ -27,7 +29,9 @@ bool operator<(info_data const & i1, info_data const & i2);
class type_info_data : public info_data {
expr m_expr;
public:
type_info_data() {}
type_info_data(unsigned l, unsigned c, expr const & e):info_data(l, c), m_expr(e) {}
expr const & get_type() const { return m_expr; }
virtual void display(io_state_stream const & ios) const;
};

2
src/frontends/lean/parser.cpp
View file

@ -1179,7 +1179,7 @@ void parser::save_snapshot() {
}
void parser::save_overload(expr const & e) {
if (!m_info_manager)
if (!m_info_manager || !is_choice(e))
return;
auto p = pos_of(e);
m_info_manager->add(std::unique_ptr<info_data>(new overload_info_data(p.first, p.second, e)));