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