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 <leonardo@microsoft.com>

src/frontends/lean/frontend_elaborator.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include <limits>
 #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<cache> 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);
                     }

src/kernel/normalizer.cpp

@@ -6,9 +6,10 @@ Author: Leonardo de Moura
 */
 #include <algorithm>
 #include <limits>
-#include "util/scoped_map.h"
+#include <unordered_map>
 #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<expr, svalue, expr_hash_alloc, expr_eqp> cache;
+    typedef std::unordered_map<expr, svalue, expr_hash_alloc, expr_eqp> 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<cache>    reset1(m_cache);
+            freset<context>  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<cache> 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<cache> 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<cache> 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<cache> 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;
     }

src/kernel/replace_visitor.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <tuple>
 #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<cache> 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<expr> new_t = visit(t, ctx);
             expr new_v = visit(v, ctx);
             {
-                cache::mk_scope sc(m_cache);
+                freset<cache> 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);
             }

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 <unordered_map>
 #include "kernel/replace_fn.h"
 #include "kernel/context.h"
 
@@ -21,7 +21,7 @@ namespace lean {
 */
 class replace_visitor {
 protected:
-    typedef scoped_map<expr, expr, expr_hash_alloc, expr_eqp> cache;
+    typedef std::unordered_map<expr, expr, expr_hash_alloc, expr_eqp> cache;
     cache   m_cache;
     context m_ctx;
     expr save_result(expr const & e, expr && r, bool shared);

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 <unordered_map>
+#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<expr, expr, expr_hash_alloc, expr_eqp> cache;
+    typedef std::unordered_map<expr, expr, expr_hash_alloc, expr_eqp> cache;
     typedef buffer<unification_constraint> 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<cache> 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<expr> t2;
             context new_ctx = extend(ctx, abst_name(e), abst_domain(e));
             {
-                cache::mk_scope sc(m_cache);
+                freset<cache> 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<cache> 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);
             }

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;
 }

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:
+   <code>
+   {
+     freset<cache> reset(m_cache); // reset the cache inside this scope
+
+   } // restore original value of m_cache
+   </code>
+
+   \remark The reset is performed by creating a fresh value and performing a swap.
+*/
+template<typename T>
+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);
+    }
+};
+}