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

perf(kernel/type_checker): improve infer_lambda performance

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-16 07:52:53 +01:00
parent c97b4c7725
commit a748e8f858
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/kernel/type_checker.cpp
View file

@ -232,8 +232,8 @@ expr type_checker::infer_lambda(expr const & _e, bool infer_only) {
expr e = _e;
while (is_lambda(e)) {
es.push_back(e);
ds.push_back(binding_domain(e));
expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data());
ds.push_back(d);
expr l = mk_local(m_gen.next(), binding_name(e), d, binding_info(e));
ls.push_back(l);
if (!infer_only) {
@ -247,8 +247,7 @@ expr type_checker::infer_lambda(expr const & _e, bool infer_only) {
unsigned i = es.size();
while (i > 0) {
--i;
expr d = abstract_locals(ds[i], i, ls.data());
r = mk_pi(binding_name(es[i]), d, r, binding_info(es[i]));
r = mk_pi(binding_name(es[i]), ds[i], r, binding_info(es[i]));
}
return r;
}