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

perf(frontends/lean/elaborator): improve visit_binding performance

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-14 16:57:20 +01:00
parent 91e8f0b8fa
commit 7ed373811d
1 changed files with 41 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -161,23 +161,6 @@ class elaborator {
} }
} }
// "Scoped update": add an local constant l to the m_ctx (and m_ctx_buffer, m_ctx_domain_buffer).
// "Undoes" the changes in the end of the scope where this object was defined.
struct update_ctx {
elaborator & m_main;
update_ctx(elaborator & main, expr const & l):m_main(main) {
lean_assert(is_local(l));
m_main.m_ctx = cons(l, m_main.m_ctx);
m_main.m_ctx_domain_buffer.push_back(abstract_locals(l, m_main.m_ctx_buffer.size(), m_main.m_ctx_buffer.data()));
m_main.m_ctx_buffer.push_back(l);
}
~update_ctx() {
m_main.m_ctx = tail(m_main.m_ctx);
m_main.m_ctx_domain_buffer.pop_back();
m_main.m_ctx_buffer.pop_back();
}
};
/** \brief Auxiliary object for creating backtracking points. /** \brief Auxiliary object for creating backtracking points.
\remark A scope can only be created when m_constraints and m_subst are empty, \remark A scope can only be created when m_constraints and m_subst are empty,
and m_accumulated is none. and m_accumulated is none.
@ -886,33 +869,52 @@ public:
throw_kernel_exception(m_env, e, [=](formatter const & fmt) { return pp_type_expected(fmt, e); }); throw_kernel_exception(m_env, e, [=](formatter const & fmt) { return pp_type_expected(fmt, e); });
} }
expr visit_pi(expr const & e) { struct scope_ctx {
expr d = ensure_type(visit_expecting_type(binding_domain(e))); elaborator & m_main;
expr l = mk_local(binding_name(e), d, binding_info(e)); context m_old_ctx;
expr b = instantiate(binding_body(e), l); unsigned m_old_sz;
if (binding_info(e).is_contextual()) { scope_ctx(elaborator & main):m_main(main), m_old_ctx(main.m_ctx), m_old_sz(main.m_ctx_buffer.size()) {}
update_ctx add(*this, l); ~scope_ctx() {
b = ensure_type(visit_expecting_type(b)); m_main.m_ctx = m_old_ctx;
} else { m_main.m_ctx_buffer.shrink(m_old_sz);
b = ensure_type(visit_expecting_type(b)); m_main.m_ctx_domain_buffer.shrink(m_old_sz);
} }
b = abstract_local(b, l); };
return update_binding(e, d, b);
void add_local(expr const & l) {
m_ctx = cons(l, m_ctx);
m_ctx_domain_buffer.push_back(abstract_locals(l, m_ctx_buffer.size(), m_ctx_buffer.data()));
m_ctx_buffer.push_back(l);
} }
expr visit_lambda(expr const & e) { expr visit_binding(expr e, expr_kind k) {
expr d = ensure_type(visit_expecting_type(binding_domain(e))); scope_ctx scope(*this);
expr l = mk_local(binding_name(e), d, binding_info(e)); buffer<expr> ds, ls, es;
expr b = instantiate(binding_body(e), l); while (e.kind() == k) {
if (binding_info(e).is_contextual()) { es.push_back(e);
update_ctx add(*this, l); expr d = binding_domain(e);
b = visit(b); d = instantiate_rev(d, ls.size(), ls.data());
} else { d = ensure_type(visit_expecting_type(d));
b = visit(b); ds.push_back(d);
expr l = mk_local(binding_name(e), d, binding_info(e));
if (binding_info(e).is_contextual())
add_local(l);
ls.push_back(l);
e = binding_body(e);
} }
b = abstract_local(b, l); lean_assert(ls.size() == es.size() && ls.size() == ds.size());
return update_binding(e, d, b); e = instantiate_rev(e, ls.size(), ls.data());
e = (k == expr_kind::Pi) ? ensure_type(visit_expecting_type(e)) : visit(e);
e = abstract_locals(e, ls.size(), ls.data());
unsigned i = ls.size();
while (i > 0) {
--i;
e = update_binding(es[i], abstract_locals(ds[i], i, ls.data()), e);
}
return e;
} }
expr visit_pi(expr const & e) { return visit_binding(e, expr_kind::Pi); }
expr visit_lambda(expr const & e) { return visit_binding(e, expr_kind::Lambda); }
expr visit_core(expr const & e) { expr visit_core(expr const & e) {
if (is_placeholder(e)) { if (is_placeholder(e)) {