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

fix(kernel/normalizer): cache problems

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-17 14:52:14 -08:00
parent 33789fad4c
commit af4a6c9364
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/kernel/normalizer.cpp
View file

@ -106,9 +106,8 @@ class normalizer::imp {
context const & entry_c = p.second; context const & entry_c = p.second;
if (entry.get_body()) { if (entry.get_body()) {
// Save the current context and cache // Save the current context and cache
freset<cache> reset1(m_cache); freset<cache> reset(m_cache);
freset<context> reset2(m_ctx); flet<context> set(m_ctx, entry_c);
m_ctx = entry_c;
unsigned k = m_ctx.size(); unsigned k = m_ctx.size();
return normalize(*(entry.get_body()), value_stack(), k); return normalize(*(entry.get_body()), value_stack(), k);
} else { } else {
@ -149,12 +148,12 @@ class normalizer::imp {
expr const & e = c.get_expr(); expr const & e = c.get_expr();
context const & ctx = c.get_context(); context const & ctx = c.get_context();
value_stack const & s = c.get_stack(); value_stack const & s = c.get_stack();
freset<cache> reset1(m_cache); freset<cache> reset(m_cache);
freset<context> reset2(m_ctx); flet<context> set(m_ctx, ctx);
m_ctx = ctx;
if (is_abstraction(e)) { if (is_abstraction(e)) {
return update_abst(e, [&](expr const & d, expr const & b) { return update_abst(e, [&](expr const & d, expr const & b) {
expr new_d = reify(normalize(d, s, k), k); expr new_d = reify(normalize(d, s, k), k);
m_cache.clear(); // make sure we do not reuse cached values from the previous call
expr new_b = reify(normalize(b, extend(s, mk_var(k)), k+1), k+1); expr new_b = reify(normalize(b, extend(s, mk_var(k)), k+1), k+1);
return mk_pair(new_d, new_b); return mk_pair(new_d, new_b);
}); });
@ -224,6 +223,7 @@ class normalizer::imp {
expr const & fv = to_closure(f).get_expr(); expr const & fv = to_closure(f).get_expr();
{ {
freset<cache> reset(m_cache); freset<cache> reset(m_cache);
flet<context> set(m_ctx, to_closure(f).get_context());
value_stack new_s = extend(to_closure(f).get_stack(), normalize(arg(a, i), s, k)); value_stack new_s = extend(to_closure(f).get_stack(), normalize(arg(a, i), s, k));
f = normalize(abst_body(fv), new_s, k); f = normalize(abst_body(fv), new_s, k);
} }