From af420782050c9fac007500d5bfee76614ff020d6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Dec 2013 15:09:41 -0800 Subject: [PATCH] fix(kernel): incorrect use of scoped_map This commit also adds a new test that exposes the problem. The scoped_map should not be used for caching values in the normalizer and type_checker. When we extend the context, the meaning of all variables is modified (we are essentially performing a lift). So, the values stored in the cache are not correct in the new context. Signed-off-by: Leonardo de Moura --- src/frontends/lean/frontend_elaborator.cpp | 3 +- src/kernel/normalizer.cpp | 38 +++++++--------------- src/kernel/replace_visitor.cpp | 5 +-- src/kernel/replace_visitor.h | 8 ++--- src/kernel/type_checker.cpp | 13 ++++---- src/tests/kernel/normalizer.cpp | 19 +++++++++++ src/util/freset.h | 38 ++++++++++++++++++++++ 7 files changed, 84 insertions(+), 40 deletions(-) create mode 100644 src/util/freset.h diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp index 4bf2d2b6e..123c4049b 100644 --- a/src/frontends/lean/frontend_elaborator.cpp +++ b/src/frontends/lean/frontend_elaborator.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include #include #include "util/interrupt.h" +#include "util/freset.h" #include "kernel/type_checker.h" #include "kernel/type_checker_justification.h" #include "kernel/normalizer.h" @@ -396,7 +397,7 @@ class frontend_elaborator::imp { } } { - cache::mk_scope sc(m_cache); + freset reset(m_cache); expr new_b = visit(b, extend(ctx, let_name(e), new_t, new_v)); return std::make_tuple(new_t, new_v, new_b); } diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index 2831c26c3..46ed6fb7b 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -6,9 +6,10 @@ Author: Leonardo de Moura */ #include #include -#include "util/scoped_map.h" +#include #include "util/list.h" #include "util/flet.h" +#include "util/freset.h" #include "util/buffer.h" #include "util/interrupt.h" #include "util/sexpr/options.h" @@ -68,7 +69,7 @@ value_stack extend(value_stack const & s, svalue const & v) { return cons(v, s); /** \brief Expression normalizer. */ class normalizer::imp { - typedef scoped_map cache; + typedef std::unordered_map cache; ro_environment::weak_ref m_env; context m_ctx; @@ -87,25 +88,6 @@ class normalizer::imp { return ::lean::add_lift(m, s, n, m_menv.to_some_menv()); } - /** - \brief Auxiliary object for saving the current context. - We need this to be able to process values in the context. - */ - struct save_context { - imp & m_imp; - context m_saved_ctx; - cache m_saved_cache; - save_context(imp & imp): - m_imp(imp), - m_saved_ctx(m_imp.m_ctx) { - m_imp.m_cache.swap(m_saved_cache); - } - ~save_context() { - m_imp.m_ctx = m_saved_ctx; - m_imp.m_cache.swap(m_saved_cache); - } - }; - svalue lookup(value_stack const & s, unsigned i) { unsigned j = i; value_stack const * it1 = &s; @@ -119,7 +101,9 @@ class normalizer::imp { context_entry const & entry = p.first; context const & entry_c = p.second; if (entry.get_body()) { - save_context save(*this); // it restores the context and cache + // Save the current context and cache + freset reset1(m_cache); + freset reset2(m_ctx); m_ctx = entry_c; unsigned k = m_ctx.size(); return svalue(reify(normalize(*(entry.get_body()), value_stack(), k), k)); @@ -133,7 +117,7 @@ class normalizer::imp { lean_assert(is_lambda(a)); expr new_t = reify(normalize(abst_domain(a), s, k), k); { - cache::mk_scope sc(m_cache); + freset reset(m_cache); return mk_lambda(abst_name(a), new_t, reify(normalize(abst_body(a), extend(s, svalue(k)), k+1), k+1)); } } @@ -229,7 +213,7 @@ class normalizer::imp { // beta reduction expr const & fv = to_expr(f); { - cache::mk_scope sc(m_cache); + freset reset(m_cache); value_stack new_s = extend(stack_of(f), normalize(arg(a, i), s, k)); f = normalize(abst_body(fv), new_s, k); } @@ -273,7 +257,7 @@ class normalizer::imp { case expr_kind::Pi: { expr new_t = reify(normalize(abst_domain(a), s, k), k); { - cache::mk_scope sc(m_cache); + freset reset(m_cache); expr new_b = reify(normalize(abst_body(a), extend(s, svalue(k)), k+1), k+1); r = svalue(mk_pi(abst_name(a), new_t, new_b)); } @@ -282,13 +266,13 @@ class normalizer::imp { case expr_kind::Let: { svalue v = normalize(let_value(a), s, k); { - cache::mk_scope sc(m_cache); + freset reset(m_cache); r = normalize(let_body(a), extend(s, v), k+1); } break; }} if (shared) { - m_cache.insert(a, r); + m_cache[a] = r; } return r; } diff --git a/src/kernel/replace_visitor.cpp b/src/kernel/replace_visitor.cpp index 07a4ef370..32343f03c 100644 --- a/src/kernel/replace_visitor.cpp +++ b/src/kernel/replace_visitor.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include "util/interrupt.h" +#include "util/freset.h" #include "kernel/replace_visitor.h" namespace lean { @@ -30,7 +31,7 @@ expr replace_visitor::visit_abst(expr const & e, context const & ctx) { return update_abst(e, [&](expr const & t, expr const & b) { expr new_t = visit(t, ctx); { - cache::mk_scope sc(m_cache); + freset reset(m_cache); expr new_b = visit(b, extend(ctx, abst_name(e), new_t)); return std::make_pair(new_t, new_b); } @@ -51,7 +52,7 @@ expr replace_visitor::visit_let(expr const & e, context const & ctx) { optional new_t = visit(t, ctx); expr new_v = visit(v, ctx); { - cache::mk_scope sc(m_cache); + freset reset(m_cache); expr new_b = visit(b, extend(ctx, let_name(e), new_t, new_v)); return std::make_tuple(new_t, new_v, new_b); } diff --git a/src/kernel/replace_visitor.h b/src/kernel/replace_visitor.h index 1f8dfe71c..f00b82469 100644 --- a/src/kernel/replace_visitor.h +++ b/src/kernel/replace_visitor.h @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include "util/scoped_map.h" +#include #include "kernel/replace_fn.h" #include "kernel/context.h" @@ -21,9 +21,9 @@ namespace lean { */ class replace_visitor { protected: - typedef scoped_map cache; - cache m_cache; - context m_ctx; + typedef std::unordered_map cache; + cache m_cache; + context m_ctx; expr save_result(expr const & e, expr && r, bool shared); virtual expr visit_type(expr const &, context const &); virtual expr visit_value(expr const &, context const &); diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 8b62a8692..b5f1f7517 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "util/scoped_map.h" +#include +#include "util/freset.h" #include "util/flet.h" #include "util/interrupt.h" #include "kernel/type_checker.h" @@ -20,7 +21,7 @@ namespace lean { static name g_x_name("x"); /** \brief Auxiliary functional object used to implement infer_type. */ class type_checker::imp { - typedef scoped_map cache; + typedef std::unordered_map cache; typedef buffer unification_constraints; ro_environment::weak_ref m_env; @@ -93,7 +94,7 @@ class type_checker::imp { expr save_result(expr const & e, expr const & r, bool shared) { if (shared) - m_cache.insert(e, r); + m_cache[e] = r; return r; } @@ -183,7 +184,7 @@ class type_checker::imp { expr d = infer_type_core(abst_domain(e), ctx); check_type(d, abst_domain(e), ctx); { - cache::mk_scope sc(m_cache); + freset reset(m_cache); return save_result(e, mk_pi(abst_name(e), abst_domain(e), infer_type_core(abst_body(e), extend(ctx, abst_name(e), abst_domain(e)))), shared); @@ -194,7 +195,7 @@ class type_checker::imp { optional t2; context new_ctx = extend(ctx, abst_name(e), abst_domain(e)); { - cache::mk_scope sc(m_cache); + freset reset(m_cache); t2 = check_type(infer_type_core(abst_body(e), new_ctx), abst_body(e), new_ctx); } if (is_type(t1) && is_type(*t2)) { @@ -218,7 +219,7 @@ class type_checker::imp { throw def_type_mismatch_exception(env(), ctx, let_name(e), *let_type(e), let_value(e), lt); } { - cache::mk_scope sc(m_cache); + freset reset(m_cache); expr t = infer_type_core(let_body(e), extend(ctx, let_name(e), lt, let_value(e))); return save_result(e, instantiate(t, let_value(e)), shared); } diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index db6200973..620911d0b 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/src/tests/kernel/normalizer.cpp @@ -17,6 +17,8 @@ Author: Leonardo de Moura #include "kernel/kernel_exception.h" #include "kernel/printer.h" #include "kernel/metavar.h" +#include "library/deep_copy.h" +#include "library/arith/int.h" #include "library/all/all.h" using namespace lean; @@ -273,6 +275,22 @@ static void tst7() { lean_assert_eq(proc(F2, context(), menv), add_inst(m2, 0, True)(True)); } +static void tst8() { + environment env; + import_all(env); + env->add_var("P", Int >> (Int >> Bool)); + expr P = Const("P"); + expr v0 = Var(0); + expr v1 = Var(1); + expr F = mk_forall(Int, mk_lambda("x", Int, Not(mk_lambda("x", Int, mk_exists(Int, mk_lambda("y", Int, P(v1, v0))))(v0)))); + normalizer proc(env); + expr N1 = proc(F); + expr N2 = proc(deep_copy(F)); + std::cout << "F: " << F << "\n====>\n"; + std::cout << N1 << "\n"; + lean_assert_eq(N1, N2); +} + int main() { save_stack_info(); tst_church_numbers(); @@ -283,5 +301,6 @@ int main() { tst5(); tst6(); tst7(); + tst8(); return has_violations() ? 1 : 0; } diff --git a/src/util/freset.h b/src/util/freset.h new file mode 100644 index 000000000..8d7e783c4 --- /dev/null +++ b/src/util/freset.h @@ -0,0 +1,38 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once + +namespace lean { +/** + \brief Template for simulating "fluid-resets". + Example: + + { + freset reset(m_cache); // reset the cache inside this scope + + } // restore original value of m_cache + + + \remark The reset is performed by creating a fresh value and performing a swap. +*/ +template +class freset { + T & m_ref; + T m_saved_value; +public: + freset(T & ref): + m_ref(ref) { + using std::swap; + swap(m_ref, m_saved_value); + } + + ~freset() { + using std::swap; + swap(m_ref, m_saved_value); + } +}; +}