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

fix(frontends/lean/info_manager): add instantiate method to synth_info_data, fixes #94

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-22 15:55:15 -07:00
parent a5f0593df1
commit 2ada3af405
1 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -78,9 +78,7 @@ public:
type_info_data() {} type_info_data() {}
type_info_data(unsigned c, expr const & e):info_data_cell(c), m_expr(e) {} type_info_data(unsigned c, expr const & e):info_data_cell(c), m_expr(e) {}
expr const & get_type() const { expr const & get_type() const { return m_expr; }
return m_expr;
}
virtual void display(io_state_stream const & ios, unsigned line) const { virtual void display(io_state_stream const & ios, unsigned line) const {
ios << "-- TYPE|" << line << "|" << get_column() << "\n"; ios << "-- TYPE|" << line << "|" << get_column() << "\n";
@ -90,10 +88,7 @@ public:
virtual info_data_cell * instantiate(substitution & s) const { virtual info_data_cell * instantiate(substitution & s) const {
expr e = s.instantiate(m_expr); expr e = s.instantiate(m_expr);
if (is_eqp(e, m_expr)) return is_eqp(e, m_expr) ? nullptr : new type_info_data(get_column(), e);
return nullptr;
else
return new type_info_data(get_column(), e);
} }
}; };
@ -105,6 +100,11 @@ public:
ios << m_expr << endl; ios << m_expr << endl;
ios << "-- ACK" << endl; ios << "-- ACK" << endl;
} }
virtual info_data_cell * instantiate(substitution & s) const {
expr e = s.instantiate(m_expr);
return is_eqp(e, m_expr) ? nullptr : new synth_info_data(get_column(), e);
}
}; };
class overload_info_data : public info_data_cell { class overload_info_data : public info_data_cell {