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

perf(kernel/type_checker): improve infer_pi performance

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-14 22:56:38 +01:00
parent b72105efff
commit ffdb43da02
1 changed files with 20 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/kernel/type_checker.cpp
View file

@ -253,14 +253,26 @@ expr type_checker::infer_lambda(expr const & _e, bool infer_only) {
return r; return r;
} }
expr type_checker::infer_pi(expr const & e, bool infer_only) { expr type_checker::infer_pi(expr const & _e, bool infer_only) {
expr t1 = ensure_sort_core(infer_type_core(binding_domain(e), infer_only), binding_domain(e)); buffer<expr> ls;
auto b = open_binding_body(e); buffer<level> us;
expr t2 = ensure_sort_core(infer_type_core(b.first, infer_only), binding_body(e)); expr e = _e;
if (m_env.impredicative()) while (is_pi(e)) {
return mk_sort(mk_imax(sort_level(t1), sort_level(t2))); expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data());
else expr t1 = ensure_sort_core(infer_type_core(d, infer_only), d);
return mk_sort(mk_max(sort_level(t1), sort_level(t2))); us.push_back(sort_level(t1));
expr l = mk_local(m_gen.next(), binding_name(e), d, binding_info(e));
ls.push_back(l);
e = binding_body(e);
}
e = instantiate_rev(e, ls.size(), ls.data());
level r = sort_level(ensure_sort_core(infer_type_core(e, infer_only), e));
unsigned i = ls.size();
while (i > 0) {
--i;
r = m_env.impredicative() ? mk_imax(us[i], r) : mk_max(us[i], r);
}
return mk_sort(r);
} }
expr type_checker::infer_app(expr const & e, bool infer_only) { expr type_checker::infer_app(expr const & e, bool infer_only) {