max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

perf(frontends/lean/elaborator): visit_structure_instance_fn: delay building error message

Browse source
This commit is contained in:
Sebastian Ullrich 2018-02-17 19:03:11 +01:00 • committed by Leonardo de Moura
parent 56dba5b98a
commit 9c5df7875a
1 changed files with 16 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2898,8 +2898,8 @@ class visit_structure_instance_fn {
}
struct field_not_ready_to_synthesize_exception : exception {
format m_fmt;
explicit field_not_ready_to_synthesize_exception(const format & m_fmt) : m_fmt(m_fmt) {}
std::function<format()> m_fmt;
explicit field_not_ready_to_synthesize_exception(std::function<format()> m_fmt) : m_fmt(m_fmt) {}
};
void field_from_default_value(const name & S_fname) {
@ -3070,19 +3070,21 @@ class visit_structure_instance_fn {
return has_expr_metavar(e);
});
if (!deps.empty()) {
format error = format("Failed to insert value for '") + format(full_S_fname) +
format("', it depends on field(s) '");
throw field_not_ready_to_synthesize_exception([=]() {
format error = format("Failed to insert value for '") + format(full_S_fname) +
format("', it depends on field(s) '");
bool first = true;
deps.for_each([&](const name & dep) {
if (!first) error += format("', '");
error += format(dep);
first = false;
deps.for_each([&](const name & dep) {
if (!first) error += format("', '");
error += format(dep);
first = false;
});
error += format("', but the value for these fields is not available.") + line() +
format("Unfolded type/default value:") + line() +
pp_until_meta_visible(m_elab.mk_fmt_ctx(), e) + line() +
line();
return error;
});
error += format("', but the value for these fields is not available.") + line() +
format("Unfolded type/default value:") + line() +
pp_until_meta_visible(m_elab.mk_fmt_ctx(), e) + line() +
line();
throw field_not_ready_to_synthesize_exception(error);
}
}
@ -3155,7 +3157,7 @@ class visit_structure_instance_fn {
} catch (field_not_ready_to_synthesize_exception const & e) {
done = false;
if (!last_progress)
error += e.m_fmt;
error += e.m_fmt();
return true;
}