refactor(deep_copy): simplify deep_copy implementation, and move unit test to separate file

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

src/library/deep_copy.cpp

@@ -14,6 +14,7 @@ class deep_copy_fn {
     expr_cell_map<expr> m_cache;
 
     expr apply(expr const & a) {
+        if (!a) return a;
         bool sh = false;
         if (is_shared(a)) {
             auto r = m_cache.find(a.raw());
@@ -35,11 +36,7 @@ class deep_copy_fn {
         case expr_kind::Eq:       r = mk_eq(apply(eq_lhs(a)), apply(eq_rhs(a))); break;
         case expr_kind::Lambda:   r = mk_lambda(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))); break;
         case expr_kind::Pi:       r = mk_pi(abst_name(a), apply(abst_domain(a)), apply(abst_body(a))); break;
-        case expr_kind::Let:      {
-            expr new_t = let_type(a) ? apply(let_type(a)) : expr();
-            r = mk_let(let_name(a), new_t, apply(let_value(a)), apply(let_body(a)));
-            break;
-        }
+        case expr_kind::Let:      r = mk_let(let_name(a), apply(let_type(a)), apply(let_value(a)), apply(let_body(a))); break;
         case expr_kind::MetaVar:
             r = update_metavar(a, [&](meta_entry const & e) -> meta_entry {
                     if (e.is_inst())

src/tests/kernel/expr.cpp

@@ -15,7 +15,6 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "library/max_sharing.h"
-#include "library/deep_copy.h"
 #include "library/printer.h"
 #include "library/arith/arith.h"
 using namespace lean;
@@ -317,18 +316,6 @@ void tst11() {
 }
 
 void tst12() {
-    expr f = Const("f");
-    expr a = Const("a");
-    expr x = Var(0);
-    expr t = Type();
-    expr F = mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), x)));
-    expr G = deep_copy(F);
-    lean_assert(F == G);
-    lean_assert(!is_eqp(F, G));
-    lean_assert(count(F) == count(G));
-}
-
-void tst13() {
     expr f  = Const("f");
     expr v  = Var(0);
     expr a1 = max_sharing(f(v, v));
@@ -340,7 +327,7 @@ void tst13() {
     lean_assert(is_eqp(M(a1), M(a2)));
 }
 
-void tst14() {
+void tst13() {
     expr t0 = Type();
     expr t1 = Type(level()+1);
     lean_assert(ty_level(t1) == level()+1);
@@ -348,7 +335,7 @@ void tst14() {
     std::cout << t0 << " " << t1 << "\n";
 }
 
-void tst15() {
+void tst14() {
     expr t = Eq(Const("a"), Const("b"));
     std::cout << t << "\n";
     expr l = mk_let("a", expr(), Const("b"), Var(0));
@@ -356,7 +343,7 @@ void tst15() {
     lean_assert(closed(l));
 }
 
-void tst16() {
+void tst15() {
     expr f = Const("f");
     expr x = Var(0);
     expr a = Const("a");
@@ -404,7 +391,6 @@ int main() {
     tst13();
     tst14();
     tst15();
-    tst16();
     std::cout << "done" << "\n";
     return has_violations() ? 1 : 0;
 }

src/tests/library/CMakeLists.txt

@@ -13,3 +13,6 @@ add_test(max_sharing ${CMAKE_CURRENT_BINARY_DIR}/max_sharing)
 add_executable(expr_lt expr_lt.cpp)
 target_link_libraries(expr_lt ${EXTRA_LIBS})
 add_test(expr_lt ${CMAKE_CURRENT_BINARY_DIR}/expr_lt)
+add_executable(deep_copy deep_copy.cpp)
+target_link_libraries(deep_copy ${EXTRA_LIBS})
+add_test(deep_copy ${CMAKE_CURRENT_BINARY_DIR}/deep_copy)

src/tests/library/deep_copy.cpp

@@ -0,0 +1,30 @@
+/*
+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/for_each.h"
+#include "kernel/abstract.h"
+#include "library/deep_copy.h"
+using namespace lean;
+
+static void tst1() {
+    expr f = Const("f");
+    expr a = Const("a");
+    expr x = Var(0);
+    expr t = Type();
+    expr z = Const("z");
+    meta_ctx ctx{mk_lift(0, 1), mk_inst(0, a)};
+    expr m = mk_metavar(0, ctx);
+    expr F = mk_let("z", Type(), Type(level()+1), mk_pi("y", t, mk_lambda("x", t, f(f(f(x, a), Const("10")), Eq(x, m)))));
+    expr G = deep_copy(F);
+    lean_assert(F == G);
+    lean_assert(!is_eqp(F, G));
+}
+
+int main() {
+    tst1();
+    return has_violations() ? 1 : 0;
+}