From c4cd6c4f8407ecfb7dc6043f0fdfdcdac7a29f87 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 22 Jul 2013 13:04:27 -0700
Subject: [PATCH] Add tests for kernel expression

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/expr.cpp             |  4 +--
 src/tests/kernel/CMakeLists.txt |  3 ++
 src/tests/kernel/expr.cpp       | 50 +++++++++++++++++++++++++++++++++
 3 files changed, 55 insertions(+), 2 deletions(-)
 create mode 100644 src/tests/kernel/CMakeLists.txt
 create mode 100644 src/tests/kernel/expr.cpp

diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index c867151d1..09c2bb1e0 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -29,7 +29,7 @@ expr_var::expr_var(unsigned idx):
     m_vidx(idx) {}
 
 expr_const::expr_const(name const & n, unsigned pos):
-    expr_cell(expr_kind::Constant, m_name.hash()),
+    expr_cell(expr_kind::Constant, n.hash()),
     m_name(n),
     m_pos(pos) {}
 
@@ -44,7 +44,7 @@ expr_app::~expr_app() {
 expr app(unsigned num_args, expr const * args) {
     lean_assert(num_args > 1);
     unsigned _num_args;
-    unsigned _num_args0;
+    unsigned _num_args0 = 0;
     expr const & arg0 = args[0];
     // Remark: we represet ((app a b) c) as (app a b c)
     if (is_app(arg0)) {
diff --git a/src/tests/kernel/CMakeLists.txt b/src/tests/kernel/CMakeLists.txt
new file mode 100644
index 000000000..7c97ab44d
--- /dev/null
+++ b/src/tests/kernel/CMakeLists.txt
@@ -0,0 +1,3 @@
+add_executable(expr_tst expr.cpp)
+target_link_libraries(expr_tst ${EXTRA_LIBS})
+add_test(expr ${CMAKE_CURRENT_BINARY_DIR}/expr_tst)
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
new file mode 100644
index 000000000..66a939477
--- /dev/null
+++ b/src/tests/kernel/expr.cpp
@@ -0,0 +1,50 @@
+/*
+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 "expr.h"
+#include "test.h"
+using namespace lean;
+
+static void tst1() {
+    expr a;
+    a = numeral(mpz(10));
+    expr f;
+    f = var(0);
+    expr fa = app({f, a});
+    std::cout << fa << "\n";
+    std::cout << app({fa, a}) << "\n";
+    lean_assert(eqp(get_arg(fa, 0), f));
+    lean_assert(eqp(get_arg(fa, 1), a));
+    lean_assert(!eqp(fa, app({f, a})));
+    lean_assert(app({fa, a}) == app({f, a, a}));
+    std::cout << app({fa, fa, fa}) << "\n";
+    std::cout << lambda(name("x"), prop(), var(0)) << "\n";
+}
+
+expr mk_dag(unsigned depth) {
+    expr f = constant(name("f"));
+    expr a = var(0);
+    while (depth > 0) {
+        depth--;
+        a = app({f, a, a});
+    }
+    return a;
+}
+
+static void tst2() {
+    expr r1 = mk_dag(24);
+    expr r2 = mk_dag(24);
+    lean_verify(r1 == r2);
+}
+
+int main() {
+    // continue_on_violation(true);
+    std::cout << "sizeof(expr):     " << sizeof(expr) << "\n";
+    std::cout << "sizeof(expr_app): " << sizeof(expr_app) << "\n";
+    tst1();
+    tst2();
+    return has_violations() ? 1 : 0;
+}