fix(replace_using_ctx): fix inconsistent cache bug in replace_using_ctx, and add tests that expose the problem

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/replace_using_ctx.h

@@ -32,6 +32,7 @@ class replace_using_ctx_fn {
                   "The return type of P()(e1, e2) is not void");
     typedef scoped_map<expr, expr, expr_hash, expr_eqp> cache;
     cache                      m_cache;
+    context                    m_ctx;
     F                          m_f;
     P                          m_post;
 
@@ -90,6 +91,13 @@ class replace_using_ctx_fn {
         return r;
     }
 
+    void set_ctx(context const & ctx) {
+        if (!is_eqp(m_ctx, ctx)) {
+            m_ctx = ctx;
+            m_cache.clear();
+        }
+    }
+
 public:
     replace_using_ctx_fn(F const & f, P const & p = P()):
         m_f(f),
@@ -97,7 +105,13 @@ public:
     }
 
     expr operator()(expr const & e, context const & ctx = context()) {
+        set_ctx(ctx);
         return apply(e, ctx, ctx.size());
     }
+
+    void clear() {
+        m_ctx = context();
+        m_cache.clear();
+    }
 };
 }

src/tests/library/CMakeLists.txt

@@ -22,3 +22,6 @@ add_test(reduce ${CMAKE_CURRENT_BINARY_DIR}/reduce)
 add_executable(arith_tst arith.cpp)
 target_link_libraries(arith_tst ${EXTRA_LIBS})
 add_test(arith_tst ${CMAKE_CURRENT_BINARY_DIR}/arith_tst)
+add_executable(replace_using_ctx replace_using_ctx.cpp)
+target_link_libraries(replace_using_ctx ${EXTRA_LIBS})
+add_test(replace_using_ctx ${CMAKE_CURRENT_BINARY_DIR}/replace_using_ctx)

src/tests/library/replace_using_ctx.cpp

@@ -0,0 +1,47 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/test.h"
+#include "kernel/context.h"
+#include "kernel/abstract.h"
+#include "library/replace_using_ctx.h"
+using namespace lean;
+
+static void tst1() {
+    expr f = Const("f");
+    expr a = Const("a");
+    expr b = Const("b");
+    expr N = Const("N");
+    expr M = Const("M");
+    expr x = Var(0);
+    context ctx1;
+    ctx1 = extend(ctx1, "x", N, a);
+    context ctx2;
+    ctx2 = extend(ctx2, "x", M, b);
+    auto proc = [](expr const & e, context const & ctx, unsigned k) -> expr {
+        if (is_var(e) && var_idx(e) < k) {
+            context_entry const & entry = ctx.lookup(var_idx(e));
+            if (entry.get_body())
+                return entry.get_body();
+        }
+        return e;
+    };
+    replace_using_ctx_fn<decltype(proc)> replacer(proc);
+    expr F1 = f(x);
+    expr F1_copy = F1;
+    lean_assert_eq(replacer(F1, ctx1), f(a));
+    lean_assert_eq(replacer(F1, ctx2), f(b));
+    lean_assert(is_eqp(replacer(F1, ctx2), replacer(F1, ctx2)));
+    expr r1 = replacer(F1, ctx2);
+    replacer.clear();
+    lean_assert(!is_eqp(r1, replacer(F1, ctx2)));
+    lean_assert(is_eqp(replacer(F1, ctx1), replacer(F1, ctx1)));
+}
+
+int main() {
+    tst1();
+    return has_violations() ? 1 : 0;
+}