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

fix(frontends/lean): missing pre_info for type incorrect declarations

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-05 01:12:08 -07:00
parent 5fa1c0a5fb
commit 613c035ff8
4 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/decl_cmds.cpp
View file

@ -318,7 +318,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
if (!found_cached) {
if (is_theorem) {
auto type_pos = p.pos_of(type);
std::tie(type, new_ls) = p.elaborate_type(type);
bool clear_pre_info = false; // we don't want to clear pre_info data until we process the proof.
std::tie(type, new_ls) = p.elaborate_type(type, list<expr>(), clear_pre_info);
check_no_metavar(env, real_n, type, true);
ls = append(ls, new_ls);
expr type_as_is = p.save_pos(mk_as_is(type), type_pos);

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

@ -386,9 +386,8 @@ struct info_manager::imp {
synch_line(i);
if (!overwrite && m_line_valid[i])
continue;
unsigned range = m_line_data[i].empty() ? 0 : m_line_data[i].max()->get_column() + 1;
s.for_each([&](info_data const & d) {
if (overwrite || d.get_column() >= range)
if (overwrite || !m_line_data[i].contains(d))
m_line_data[i].insert(d);
});
}

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

@ -569,14 +569,15 @@ std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e, li
return r;
}
std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e, list<expr> const & ctx) {
std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e, list<expr> const & ctx, bool clear_pre_info) {
bool relax = false;
bool check_unassigned = true;
bool ensure_type = true;
parser_pos_provider pp = get_pos_provider();
elaborator_context env = mk_elaborator_context(pp, check_unassigned);
auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type);
m_pre_info_manager.clear();
if (clear_pre_info)
m_pre_info_manager.clear();
return r;
}

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

@ -324,7 +324,7 @@ public:
/** \brief Elaborate \c e, and tolerate metavariables in the result. */
std::tuple<expr, level_param_names> elaborate_relaxed(expr const & e, list<expr> const & ctx = list<expr>());
/** \brief Elaborate \c e, and ensure it is a type. */
std::tuple<expr, level_param_names> elaborate_type(expr const & e, list<expr> const & ctx = list<expr>());
std::tuple<expr, level_param_names> elaborate_type(expr const & e, list<expr> const & ctx = list<expr>(), bool clear_pre_info = true);
/** \brief Elaborate \c e in the given environment. */
std::tuple<expr, level_param_names> elaborate_at(environment const & env, expr const & e);
/** \brief Elaborate \c e (making sure the result does not have metavariables). */